Lean4
/-- Coherence tactic for monoidal categories. -/
def monoidal_coherence (g : MVarId) : TermElabM Unit :=
g.withContext do
withOptions (fun opts => synthInstance.maxSize.set opts (max 512 (synthInstance.maxSize.get opts))) do
let thms :=
[``MonoidalCoherence.iso, ``Iso.trans, ``Iso.symm, ``Iso.refl, ``MonoidalCategory.whiskerRightIso,
``MonoidalCategory.whiskerLeftIso].foldl
(·.addDeclToUnfoldCore ·) { }
let (ty, _) ← dsimp (← g.getType) (← Simp.mkContext (simpTheorems := #[thms]))
let some (_, lhs, rhs) := (← whnfR ty).eq? |
exception g "Not an equation of morphisms."
let projectMap_lhs ← mkProjectMapExpr lhs
let projectMap_rhs ← mkProjectMapExpr rhs
let g₁ ← g.change (← mkEq projectMap_lhs projectMap_rhs)
let [g₂] ← g₁.applyConst ``congrArg |
exception g "congrArg failed in coherence"
let [] ← g₂.applyConst ``Subsingleton.elim |
exception g "This shouldn't happen; Subsingleton.elim does not create goals."
