Meta code in order to do multiple substitutions

Stream: mathlib4

[Joël Riou]

Following the start #12798 of the development of fibered categories by @Calle Sönne and @Paul Lezeau I feel that some meta code would be useful in the following situation:

import Mathlib.CategoryTheory.EqToHom

namespace CategoryTheory.Functor

variable {𝒮 𝒳 : Type*} [Category 𝒮] [Category 𝒳 ] (p :  𝒳 ⥤ 𝒮 )

class IsHomLift {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) : Prop where
  domain_eq : p.obj a = R := by aesop_cat
  codomain_eq : p.obj b = S := by aesop_cat
  fac : f = eqToHom domain_eq.symm ≫ p.map φ ≫ eqToHom codomain_eq := by aesop_cat

lemma test {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] : 0 = 1 := by
  -- initially, we have a morphism `φ` which is "over" a morphism `f` via the functor `p`
  obtain rfl : p.obj a = R := IsHomLift.domain_eq (f := f) (φ := φ)
  obtain rfl : p.obj b = S := IsHomLift.codomain_eq (f := f) (φ := φ)
  obtain rfl : f = p.map φ := by simpa using IsHomLift.fac (p := p) (f := f) (φ := φ)
  -- now, we only have the morphism `φ`
  sorry

end CategoryTheory.Functor

Is there a way to define a tactic subst_hom_lift p f φ which would attempt at doing the three substitutions done by obtain above?

I know that an alternative approach would be to use an inductive type (which could be repackaged in a type-class):

inductive IsHomLift' : ∀ {R S : 𝒮} {a b : 𝒳} (_ : R ⟶ S) (_ : a ⟶ b), Prop
  | map {a b : 𝒳} (φ : a ⟶ b) : IsHomLift' (p.map φ) φ

lemma test' {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (hp : p.IsHomLift' f φ) : 0 = 1 := by
  -- initially, we have a morphism `φ` which is "over" a morphism `f` via the functor `p`
  cases hp
  -- now, we only have the morphism `φ`
  sorry

What would be the recommended ways to do such things?

[Adam Topaz]

Can you get by with something along the following lines?

inductive IsHomLiftAux : {R S : 𝒮} → {a b : 𝒳} → (R ⟶ S) → (a ⟶ b) → Prop where
  | mk {a b} (φ : a ⟶ b) : IsHomLiftAux (p.map φ) φ

class IsHomLift {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) : Prop where
  cond : IsHomLiftAux p f φ

lemma test {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] : 0 = 1 := by
  obtain ⟨⟩ := IsHomLift.cond (p := p) (f := f) (φ := φ)
  sorry

[Adam Topaz]

Alternatively making a tactic is certainly possible, but would require some work.

[Adam Topaz]

Jeez, I seem to have completely missed your second code block :rofl:

[Adam Topaz]

Anyway, I think going with the inductive type is preferable. I think the fact that the first IsHomLift has eqToHoms is a red flag.

[Andrew Yang]

Maybe

lemma test {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [h : p.IsHomLift f φ] : 0 = 1 := by
  obtain ⟨rfl, rfl, rfl⟩ := h
  sorry

[Adam Topaz]

Doesn't that still leave eqToHoms? (yes, they would simplify away with simp, but still...)

[Andrew Yang]

But if p, f, q aren't actually substitutable variables then inductives might be harder to use?

[Adam Topaz]

E.g. this doesn't work:

import Mathlib.CategoryTheory.EqToHom

namespace CategoryTheory.Functor

variable {𝒮 𝒳 : Type*} [Category 𝒮] [Category 𝒳 ] (p :  𝒳 ⥤ 𝒮 )

class IsHomLift {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) : Prop where
  domain_eq : p.obj a = R := by aesop_cat
  codomain_eq : p.obj b = S := by aesop_cat
  fac : f = eqToHom domain_eq.symm ≫ p.map φ ≫ eqToHom codomain_eq := by aesop_cat

lemma test {R S : 𝒮} {a b : 𝒳} (f g : R ⟶ S) (φ : a ⟶ b) [h : p.IsHomLift f φ] [h' : p.IsHomLift g φ] : f = g := by
  obtain ⟨rfl, rfl, rfl⟩ := h
  obtain ⟨rfl, rfl, rfl⟩ := h' -- fails
  sorry

[Adam Topaz]

Well, that fails also with the inductive approach, so I don't know.

[Joël Riou]

Anyway, it seems the better approach is to use a definition using an inductive type, and provide an API (alternate constructors/lemmas) which may have to feature some eqToHom.

[Calle Sönne]

Thanks for this! I didn't know about this technique with using an inductive type, so I will play around with it a bit to see what improvements I can get

[Calle Sönne]

Also with this approach subst_hom_lift, like @Joël Riou suggested, can be very easily defined as a macro (and is imo a lot more readable than obtain ⟨⟩ := IsHomLift.cond (p := p) (f := f) (φ := φ))

[Calle Sönne]

Adam Topaz said:

lemma test {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] : 0 = 1 := by
  obtain ⟨⟩ := IsHomLift.cond (p := p) (f := f) (φ := φ)
  sorry

When using this in more complicated proofs, I am running into the issue that the first line only replaces φ and f, and not also R, S, a, b. So φ : a ⟶ b becomes φ : a✝⟶ b✝ after the first line, and f becomes p.map φ : p.obj a✝ ⟶ p.obj b✝ (and R, S, a, b are still in the context). Is there a way to make this line of code also replace R, S, a, b? Or at least so that I can give other names to a✝, b✝?

[Calle Sönne]

I now found out that I can just do clear a b :)

[Eric Wieser]

Another approach here is to use the non-inductive type, but then write an induction principle to match the one generated by inductive