The `check_compositions` tactic, which checks the typing of categorical compositions in the goal, reporting discrepancies at "instances and reducible" transparency.

Reports from this tactic do not necessarily indicate a problem, although typically `simp` should reduce rather than increase the reported discrepancies.

`check_compositions` may be useful in diagnosing uses of `erw` in the category theory library.

source
def Mathlib.Tactic.CheckCompositions.forEachComposition (e : Lean.Expr) (f : Lean.Expr → Lean.MetaM Unit) :
Lean.MetaM Unit

Find appearances of `CategoryStruct.comp C inst X Y Z f g`, and apply `f` to each.

Equations

- Mathlib.Tactic.CheckCompositions.forEachComposition e f = e.forEach fun (e : Lean.Expr) => if e.isAppOfArity `CategoryTheory.CategoryStruct.comp 7 = true then f e else pure ()

Instances For

source
def Mathlib.Tactic.CheckCompositions.checkComposition (e : Lean.Expr) :
Lean.MetaM Unit

Given a composition `CategoryStruct.comp _ _ X Y Z f g`, infer the types of `f` and `g` and check whether their sources and targets agree, at "instances and reducible" transparency, with `X`, `Y`, and `Z`, reporting any discrepancies.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.CheckCompositions.checkCompositions (e : Lean.Expr) :
Lean.MetaM Unit

Check the typing of categorical compositions in an expression.

Equations

- Mathlib.Tactic.CheckCompositions.checkCompositions e = Mathlib.Tactic.CheckCompositions.forEachComposition e Mathlib.Tactic.CheckCompositions.checkComposition

Instances For

source
def Mathlib.Tactic.CheckCompositions.checkCompositionsTac :
Lean.Elab.Tactic.TacticM Unit

Check the typing of categorical compositions in the goal.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.CheckCompositions.tacticCheck_compositions :
Lean.ParserDescr

For each composition `f ≫ g` in the goal, which internally is represented as `CategoryStruct.comp C inst X Y Z f g`, infer the types of `f` and `g` and check whether their sources and targets agree with `X`, `Y`, and `Z` at "instances and reducible" transparency, reporting any discrepancies.

An example:

    example (j : J) :
        colimit.ι ((F ⋙ G) ⋙ H) j ≫ (preservesColimitIso (G ⋙ H) F).inv =
          H.map (G.map (colimit.ι F j)) := by

      -- We know which lemma we want to use, and it's even a simp lemma, but `rw`
      -- won't let us apply it
      fail_if_success rw [ι_preservesColimitIso_inv]
      fail_if_success rw [ι_preservesColimitIso_inv (G ⋙ H)]
      fail_if_success simp only [ι_preservesColimitIso_inv]

      -- This would work:
      -- erw [ι_preservesColimitIso_inv (G ⋙ H)]

      -- `check_compositions` checks if the two morphisms we're composing are
      -- composed by abusing defeq, and indeed it tells us that we are abusing
      -- definitional associativity of composition of functors here: it prints
      -- the following.

      -- info: In composition
      --   colimit.ι ((F ⋙ G) ⋙ H) j ≫ (preservesColimitIso (G ⋙ H) F).inv
      -- the source of
      --   (preservesColimitIso (G ⋙ H) F).inv
      -- is
      --   colimit (F ⋙ G ⋙ H)
      -- but should be
      --   colimit ((F ⋙ G) ⋙ H)

      check_compositions

      -- In this case, we can "fix" this by reassociating in the goal, but
      -- usually at this point the right thing to do is to back off and
      -- check how we ended up with a bad goal in the first place.
      dsimp only [Functor.assoc]

      -- This would work now, but it is not needed, because simp works as well
      -- rw [ι_preservesColimitIso_inv]

      simp

Equations

- One or more equations did not get rendered due to their size.

Instances For