Class inference inferring propositional arguments

Stream: mathlib4

[joseph hua]

In the following example I define a class foo a which I assume can be proven given some (variable) predicate P holds on a.

variable {A : Type}

class foo (a : A) : Prop where
  bar : a = sorry

variable (P : A → Prop)

instance {a} (ha : P a) : foo a := sorry

instance {a} (ha : P a) : foo a := by infer_instance -- failed to synthesize

instance (x : (a : A) ×' P a) : foo x.1 := sorry

instance (x : (a : A) ×' P a) : foo x.1 := by infer_instance -- works

Lean fails to infer that foo a given P a after I have established this fact already. The second way I phrased it works, but maybe will lead to class inference problems later on?

[Aaron Liu]

Typeclass instance isn't able to just pull stuff out of the context

[Aaron Liu]

in the first part it doesn't know about ha : P a

[Aaron Liu]

but in the second part it's looking for a foo x.1 so it can unify x

[Aaron Liu]

if you're really sure you want to use typeclass you might want to try out docs#Fact

[Aaron Liu]

so basically typeclass doesn't know about ha and it can't find it, and it doesn't know about x but it can find it because the typeclass goal contains an x

[joseph hua]

Ooh, I forgot out Fact. I will experiment and see how well it works. Thanks!

[Violeta Hernández]

I think using Fact is strongly discouraged outside of a few "standard" usages. Can you instead make P into its own typeclass? Can you somehow tweak your junk values or whatnot to not require the usage of P? It's hard to say what the best solution is without knowing what exactly you're trying to do.

[joseph hua]

Sorry yes, here is the use case

I would like that any CategoryTheory.MorphismProperty satisfying CategoryTheory.MorphismProperty.HasPullbacks to have some inference support such as

/-- `P` has pullbacks if for every `f` satisfying `P`, pullbacks of arbitrary morphisms along `f`
exist. -/
protected class HasPullbacks : Prop where
  hasPullback {X Y S : C} {f : X ⟶ S} (g : Y ⟶ S) : P f → HasPullback f g := by infer_instance

instance [P.HasPullbacks] {X Y S : C} {f : X ⟶ S} (g : Y ⟶ S) : HasPullback f g :=
  HasPullbacks.hasPullback g -- error cannot find synthesization order for instances

-- The following works though
notation E " ⟶("P") " B => { p : E ⟶ B // P p }

protected class HasPullbacks' : Prop where
  hasPullback {X Y S : C} {f : X ⟶(P) S} (g : Y ⟶ S) : HasPullback f.1 g := by infer_instance

instance [P.HasPullbacks'] {X Y S : C} {f : X ⟶(P) S} (g : Y ⟶ S) : HasPullback f.1 g :=
  HasPullbacks'.hasPullback g

[Aaron Liu]

what kind of P are you intending to use it with

[joseph hua]

Aaron Liu said:

what kind of P are you intending to use it with

Eventually, isofibrations in the category of groupoids, but I would like to reason about a general variable P to develop some theory

[Aaron Liu]

could you perhaps no that doesn't work

[Aaron Liu]

hmm

[Aaron Liu]

how many pullbacks do you expect to see

[Aaron Liu]

if it's not too much then you could just assume the necessary pullbacks for each theorem

[joseph hua]

I'm not too sure how many pullbacks I will need, but I feel like we shouldn't be using HasPullback f g if we cannot infer it

[Aaron Liu]

you can infer it if P is a typeclass

[Aaron Liu]

but free variables are not typeclasses so...

[Kenny Lau]

joseph hua said:

I would like to reason about a general variable P

I'm afraid you might have to insert let := pullbackOfP hp in each theorem

[Kenny Lau]

https://github.com/leanprover-community/mathlib4/blob/432a037a7f67dfd6d390629429706ca5180ade56/Mathlib/Analysis/Seminorm.lean#L1087