chore(Tactic/CategoryTheory): fix meta code for monoidal categories (#…

…15335)

Several bug fixes and simple refactoring. The main changes:

- `Monoidal.lean`: In `structural?`, the number of arguments in `getAppFnArgs` matching was wrong (I only considered explicit ones there). Infact, `structural?` is no longer needed since the matching is performed in `eval`. Now the `monoidalCoherence` is `StructuralAtom`, not `Structural`.
- `Coherence.lean`: Unfolding `MonoidalCoherence.hom` by `dsimp` at the beginning of the coherence tactic.

Mathlib/Tactic/CategoryTheory/BicategoryCoherence.lean

@@ -112,8 +112,8 @@ def mkLiftMap₂LiftExpr (e : Expr) : TermElabM Expr := do
 def bicategory_coherence (g : MVarId) : TermElabM Unit := g.withContext do
   withOptions (fun opts => synthInstance.maxSize.set opts
     (max 256 (synthInstance.maxSize.get opts))) do
-  -- TODO: is this `dsimp only` step necessary? It doesn't appear to be in the tests below.
-  let (ty, _) ← dsimp (← g.getType) (← Simp.Context.ofNames [] true)
+  let (ty, _) ← dsimp (← g.getType)
+    { simpTheorems := #[.addDeclToUnfoldCore {} ``BicategoricalCoherence.hom] }
   let some (_, lhs, rhs) := (← whnfR ty).eq? | exception g "Not an equation of morphisms."
   let lift_lhs ← mkLiftMap₂LiftExpr lhs
   let lift_rhs ← mkLiftMap₂LiftExpr rhs

Mathlib/Tactic/CategoryTheory/Coherence.lean

@@ -121,8 +121,8 @@ def mkProjectMapExpr (e : Expr) : TermElabM Expr := do
 def monoidal_coherence (g : MVarId) : TermElabM Unit := g.withContext do
   withOptions (fun opts => synthInstance.maxSize.set opts
     (max 512 (synthInstance.maxSize.get opts))) do
-  -- TODO: is this `dsimp only` step necessary? It doesn't appear to be in the tests below.
-  let (ty, _) ← dsimp (← g.getType) (← Simp.Context.ofNames [] true)
+  let (ty, _) ← dsimp (← g.getType)
+    { simpTheorems := #[.addDeclToUnfoldCore {} ``MonoidalCoherence.hom] }
   let some (_, lhs, rhs) := (← whnfR ty).eq? | exception g "Not an equation of morphisms."
   let projectMap_lhs ← mkProjectMapExpr lhs
   let projectMap_rhs ← mkProjectMapExpr rhs
@@ -184,7 +184,7 @@ elab (name := liftable_prefixes) "liftable_prefixes" : tactic => do
     (max 256 (synthInstance.maxSize.get opts))) do
   evalTactic (← `(tactic|
     (simp (config := {failIfUnchanged := false}) only
-      [monoidalComp, Category.assoc, MonoidalCoherence.hom]) <;>
+      [monoidalComp, Category.assoc, MonoidalCoherence.hom, BicategoricalCoherence.hom]) <;>
     (apply (cancel_epi (𝟙 _)).1 <;> try infer_instance) <;>
     (simp (config := {failIfUnchanged := false}) only
       [assoc_liftHom, Mathlib.Tactic.BicategoryCoherence.assoc_liftHom₂])))
@@ -284,9 +284,7 @@ syntax (name := coherence) "coherence" : tactic
 elab_rules : tactic
 | `(tactic| coherence) => do
   evalTactic (← `(tactic|
-    (simp (config := {failIfUnchanged := false}) only [bicategoricalComp,
-      BicategoricalCoherence.hom,
-      monoidalComp]);
+    (simp (config := {failIfUnchanged := false}) only [bicategoricalComp, monoidalComp]);
     whisker_simps (config := {failIfUnchanged := false});
     monoidal_simps (config := {failIfUnchanged := false})))
   coherence_loop

Mathlib/Tactic/CategoryTheory/Monoidal.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Yuma Mizuno. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yuma Mizuno
 -/
-import Mathlib.Tactic.CategoryTheory.Coherence
+import Mathlib.Tactic.CategoryTheory.MonoidalComp
 
 /-!
 # Normalization of morphisms in monoidal categories
@@ -53,11 +53,10 @@ and `pf` is a proof that `e = e'`.
 
 -/
 
-namespace Mathlib.Tactic.Monoidal
-
 open Lean Meta Elab
 open CategoryTheory
-open Mathlib.Tactic.Coherence
+
+namespace Mathlib.Tactic.Monoidal
 
 /-- The context for evaluating expressions. -/
 structure Context where
@@ -149,6 +148,8 @@ inductive StructuralAtom : Type
   | rightUnitor (f : Mor₁) : StructuralAtom
   /-- The expression for the inverse of the right unitor `(ρ_ f).inv`. -/
   | rightUnitorInv (f : Mor₁) : StructuralAtom
+  /-- Expressions for `α` in the monoidal composition `η ⊗≫ θ := η ≫ α ≫ θ`. -/
+  | monoidalCoherence (f g : Mor₁) (e : Expr) : StructuralAtom
   deriving Inhabited
 
 /-- Construct a `StructuralAtom` expression from a Lean expression. -/
@@ -172,7 +173,11 @@ def structuralAtom? (e : Expr) : MetaM (Option StructuralAtom) := do
     | (``MonoidalCategoryStruct.rightUnitor, #[_, _, _, f]) =>
       return some <| .rightUnitorInv (← toMor₁ f)
     | _ => return none
-  | _ => return none
+  | _ =>
+    match (← whnfR e).getAppFnArgs with
+    | (``MonoidalCoherence.hom, #[_, _, f, g, inst]) =>
+      return some <| .monoidalCoherence (← toMor₁ f) (← toMor₁ g) inst
+    | _ => return none
 
 /-- Expressions for atomic non-structural 2-morphisms. -/
 structure Atom where
@@ -208,8 +213,6 @@ inductive Structural : Type
   | whiskerLeft (f : Mor₁) (η : Structural) : Structural
   /-- Expressions for the right whiskering `η ▷ f`. -/
   | whiskerRight (η : Structural) (f : Mor₁) : Structural
-  /-- Expressions for `α` in the monoidal composition `η ⊗≫ θ := η ≫ α ≫ θ`. -/
-  | monoidalCoherence (f g : Mor₁) (e : Expr) : Structural
   deriving Inhabited
 
 /-- Normalized expressions for 2-morphisms. -/
@@ -266,6 +269,7 @@ def StructuralAtom.src : StructuralAtom → Mor₁
   | .leftUnitorInv f => f
   | .rightUnitor f => f.comp Mor₁.id
   | .rightUnitorInv f => f
+  | .monoidalCoherence f _ _ => f
 
 /-- The codomain of a 2-morphism. -/
 def StructuralAtom.tgt : StructuralAtom → Mor₁
@@ -275,6 +279,7 @@ def StructuralAtom.tgt : StructuralAtom → Mor₁
   | .leftUnitorInv f => Mor₁.id.comp f
   | .rightUnitor f => f
   | .rightUnitorInv f => f.comp Mor₁.id
+  | .monoidalCoherence _ g _ => g
 
 /-- The domain of a 2-morphism. -/
 def Structural.src : Structural → Mor₁
@@ -283,7 +288,6 @@ def Structural.src : Structural → Mor₁
   | .comp α _ => α.src
   | .whiskerLeft f η => f.comp η.src
   | .whiskerRight η f => η.src.comp f
-  | .monoidalCoherence f _ _ => f
 
 /-- The codomain of a 2-morphism. -/
 def Structural.tgt : Structural → Mor₁
@@ -292,7 +296,6 @@ def Structural.tgt : Structural → Mor₁
   | .comp _ β => β.tgt
   | .whiskerLeft f η => f.comp η.tgt
   | .whiskerRight η f => η.tgt.comp f
-  | .monoidalCoherence _ g _ => g
 
 /-- The domain of a 2-morphism. -/
 def NormalExpr.src : NormalExpr → Mor₁
@@ -328,32 +331,6 @@ def NormalExpr.rightUnitor (f : Mor₁) : NormalExpr :=
 def NormalExpr.rightUnitorInv (f : Mor₁) : NormalExpr :=
   .nil <| .atom <| .rightUnitorInv f
 
-/-- Return `η` for `η ▷ g₁ ▷ ... ▷ gₙ`. -/
-def WhiskerRightExpr.atom : WhiskerRightExpr → Atom
-  | WhiskerRightExpr.of η => η
-  | WhiskerRightExpr.whisker η _ => η.atom
-
-/-- Return `η` for `f₁ ◁ ... ◁ fₙ ◁ η ▷ g₁ ▷ ... ▷ gₙ`. -/
-def WhiskerLeftExpr.atom : WhiskerLeftExpr → Atom
-  | WhiskerLeftExpr.of η => η.atom
-  | WhiskerLeftExpr.whisker _ η => η.atom
-
-/-- Construct a `Structural` expression from a Lean expression for a structural 2-morphism. -/
-partial def structural? (e : Expr) : MetaM Structural := do
-  match (← whnfR e).getAppFnArgs with
-  | (``CategoryStruct.comp, #[_, _, _, α, β]) =>
-    return .comp (← structural? α) (← structural? β)
-  | (``CategoryStruct.id, #[_, f]) => return .id (← toMor₁ f)
-  | (``MonoidalCategoryStruct.whiskerLeft, #[f, η]) =>
-    return .whiskerLeft (← toMor₁ f) (← structural? η)
-  | (``MonoidalCategoryStruct.whiskerRight, #[η, f]) =>
-    return .whiskerRight (← structural? η) (← toMor₁ f)
-  | (``MonoidalCoherence.hom, #[_, _, f, g, inst]) =>
-    return .monoidalCoherence (← toMor₁ f) (← toMor₁ g) inst
-  | _ => match ← structuralAtom? e with
-    | some η => return .atom η
-    | none => throwError "not a structural 2-morphism"
-
 /-- Construct a `NormalExpr` expression from a `WhiskerLeftExpr` expression. -/
 def NormalExpr.of (η : WhiskerLeftExpr) : MetaM NormalExpr := do
   return .cons (.id (← η.src)) η (.nil (.id (← η.tgt)))
@@ -380,7 +357,9 @@ def structuralOfMonoidalComp (C e : Expr) : MetaM Structural := do
   let αg := mkAppN (.const ``CategoryStruct.comp [v, u]) #[C, instC, X, Y, Z, α₀, g]
   let fαg := mkAppN (.const ``CategoryStruct.comp [v, u]) #[C, instC, W, X, Z, f, αg]
   _ ← isDefEq e fαg
-  structural? α₀
+  match ← structuralAtom? α₀ with
+  | some η => return .atom η
+  | none => throwError "not a structural 2-morphism"
 
 section
 
@@ -521,6 +500,8 @@ def StructuralAtom.e : StructuralAtom → MonoidalM Expr
     mkAppM ``Iso.hom #[← mkAppM ``MonoidalCategoryStruct.rightUnitor #[← f.e]]
   | .rightUnitorInv f => do
     mkAppM ``Iso.inv #[← mkAppM ``MonoidalCategoryStruct.rightUnitor #[← f.e]]
+  | .monoidalCoherence _ _ e => do
+    mkAppOptM ``MonoidalCoherence.hom #[none, none, none, none, e]
 
 /-- Extract a Lean expression from a `Structural` expression. -/
 partial def Structural.e : Structural → MonoidalM Expr
@@ -529,8 +510,6 @@ partial def Structural.e : Structural → MonoidalM Expr
   | .comp α β => do mkAppM ``CategoryStruct.comp #[← α.e, ← β.e]
   | .whiskerLeft f η => do mkAppM ``MonoidalCategoryStruct.whiskerLeft #[← f.e, ← η.e]
   | .whiskerRight η f => do mkAppM ``MonoidalCategoryStruct.whiskerRight #[← η.e, ← f.e]
-  | .monoidalCoherence _ _ e => do
-    mkAppOptM ``MonoidalCoherence.hom #[none, none, none, none, e]
 
 /-- Extract a Lean expression from a `WhiskerRightExpr` expression. -/
 def WhiskerRightExpr.e : WhiskerRightExpr → MonoidalM Expr
@@ -679,7 +658,7 @@ open Mathlib.Tactic.Monoidal
 elab "normalize% " t:term:51 : term => do
   let e ← Lean.Elab.Term.elabTerm t none
   let some ctx ← mkContext? e
-    | throwError "not a morphism"
+    | throwError "{← ppExpr e} is not a morphism"
   MonoidalM.run ctx do (← eval e).expr.e
 
 theorem mk_eq {α : Type _} (a b a' b' : α) (ha : a = a') (hb : b = b') (h : a' = b') : a = b := by

Mathlib/Tactic/Widget/StringDiagram.lean

@@ -54,7 +54,6 @@ namespace Mathlib.Tactic
 
 open Lean Meta Elab
 open CategoryTheory
-open Mathlib.Tactic.Coherence
 
 open Mathlib.Tactic.Monoidal
 
@@ -183,10 +182,8 @@ def NormalExpr.nodes (e : NormalExpr) : MetaM (List (List Node)) := do
   | NormalExpr.cons _ η _ => return (← topNodes η) :: (← e.nodesAux 1)
 
 /-- `pairs [a, b, c, d]` is `[(a, b), (b, c), (c, d)]`. -/
-def pairs {α : Type} : List α → List (α × α)
-  | [] => []
-  | [_] => []
-  | (x :: y :: ys) => (x, y) :: pairs (y :: ys)
+def pairs {α : Type} : List α → List (α × α) :=
+  fun l => l.zip (l.drop 1)
 
 /-- The list of strands associated with a 2-morphism. -/
 def NormalExpr.strands (e : NormalExpr) : MetaM (List (List Strand)) := do

scripts/noshake.json

@@ -273,6 +273,8 @@
   ["Mathlib.CategoryTheory.Category.Basic"],
   "Mathlib.Tactic.CategoryTheory.Reassoc":
   ["Mathlib.CategoryTheory.Functor.Basic"],
+  "Mathlib.Tactic.CategoryTheory.Monoidal":
+  ["Mathlib.Tactic.CategoryTheory.MonoidalComp"],
   "Mathlib.Tactic.CategoryTheory.Coherence":
   ["Mathlib.CategoryTheory.Monoidal.Free.Coherence",
    "Mathlib.Tactic.CategoryTheory.MonoidalComp"],

test/CategoryTheory/Coherence.lean

@@ -4,7 +4,7 @@ open CategoryTheory
 
 universe w v u
 
-section monoidal
+section Monoidal
 variable {C : Type u} [Category.{v} C] [MonoidalCategory C]
 open scoped MonoidalCategory
 
@@ -79,7 +79,7 @@ example (X₁ X₂ : C) :
     (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).inv) := by
   coherence
 
-end monoidal
+end Monoidal
 
 section Bicategory
 
@@ -106,6 +106,7 @@ example (f : a ⟶ b) (g : b ⟶ c) :
 example : 𝟙 (𝟙 a ≫ 𝟙 a) ≫ (λ_ (𝟙 a)).hom = 𝟙 (𝟙 a ≫ 𝟙 a) ≫ (ρ_ (𝟙 a)).hom := by
   bicategory_coherence
 
+set_option linter.unusedVariables false in
 example (f g : a ⟶ a) (η : 𝟙 a ⟶ f) (θ : f ⟶ g) (w : false) :
   (λ_ (𝟙 a)).hom ≫ η ≫ θ = (ρ_ (𝟙 a)).hom ≫ η ≫ θ := by
   coherence

test/CategoryTheory/Monoidal.lean

@@ -1,4 +1,5 @@
 import Mathlib.Tactic.CategoryTheory.Monoidal
+import Mathlib.Tactic.CategoryTheory.Coherence
 
 open CategoryTheory
 open scoped MonoidalCategory
@@ -31,14 +32,21 @@ example (f : U ⟶ V ⊗ (W ⊗ X)) (g : (V ⊗ W) ⊗ X ⟶ Y) :
     f ⊗≫ g = f ≫ 𝟙 _ ≫ (α_ _ _ _).inv ≫ g := by
   monoidal_nf
   repeat' apply congrArg₂ (· ≫ ·) ?_ <| congrArg₂ (· ≫ ·) rfl ?_
-  all_goals simp
+  all_goals pure_coherence
 
 example : (X ⊗ Y) ◁ f = (α_ _ _ _).hom ≫ X ◁ Y ◁ f ≫ (α_ _ _ _).inv := by
   monoidal_nf
   repeat' apply congrArg₂ (· ≫ ·) ?_ <| congrArg₂ (· ≫ ·) rfl ?_
-  all_goals simp
+  all_goals pure_coherence
 
 example : f ≫ g = f ≫ g := by
   monoidal_nf
   repeat' apply congrArg₂ (· ≫ ·) ?_ <| congrArg₂ (· ≫ ·) rfl ?_
-  all_goals simp
+  all_goals pure_coherence
+
+example {V₁ V₂ V₃ : C} (R : ∀ V₁ V₂ : C, V₁ ⊗ V₂ ⟶ V₂ ⊗ V₁) :
+    R V₁ V₂ ▷ V₃ ⊗≫ V₂ ◁ R V₁ V₃ =
+      R V₁ V₂ ▷ V₃ ≫ (α_ _ _ _).hom ⊗≫ 𝟙 _ ≫ V₂ ◁ R V₁ V₃ := by
+  monoidal_nf
+  repeat' apply congrArg₂ (· ≫ ·) ?_ <| congrArg₂ (· ≫ ·) rfl ?_
+  all_goals pure_coherence