feat(CategoryTheory): add a grind propagator that normalizes morphism composition

Mathlib.lean

@@ -3433,6 +3433,7 @@ public import Mathlib.CategoryTheory.Subterminal
 public import Mathlib.CategoryTheory.Sums.Associator
 public import Mathlib.CategoryTheory.Sums.Basic
 public import Mathlib.CategoryTheory.Sums.Products
+public import Mathlib.CategoryTheory.Tactic.GrindCatNorm
 public import Mathlib.CategoryTheory.Thin
 public import Mathlib.CategoryTheory.Topos.Classifier
 public import Mathlib.CategoryTheory.Topos.Sheaf

Mathlib/CategoryTheory/Category/Basic.lean

@@ -240,8 +240,8 @@ class Category (obj : Type u) : Type max u (v + 1) extends CategoryStruct.{v} ob
   assoc : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h := by
     cat_disch
 
-attribute [to_dual existing (attr := simp, grind =) id_comp] Category.comp_id
-attribute [simp, grind _=_] Category.assoc
+attribute [to_dual existing (attr := simp) id_comp] Category.comp_id
+attribute [simp] Category.assoc
 
 initialize_simps_projections Category (-Hom)
 
@@ -394,6 +394,13 @@ variable [Category.{v} C]
 
 universe u'
 
+-- The propagator in `Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean` is loaded
+-- only *after* this file, so the `cat_disch` autoparam in `uliftCategory` below
+-- cannot rely on it. We make the relevant equational lemmas available to
+-- `grind` locally for the rest of this file.
+attribute [local grind =] Category.id_comp Category.comp_id
+attribute [local grind _=_] Category.assoc
+
 /-- The category structure on `ULift C` that is induced from the category
 structure on `C`. This is not made a global instance because of a diamond
 when `C` is a preordered type. -/

Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean

@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2026 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+public import Mathlib.CategoryTheory.Category.Basic
+public import Lean.Meta.Tactic.Grind
+public import Mathlib.Lean.Meta.Simp
+
+/-!
+# A `grind` propagator that normalizes morphism composition
+
+Installs a `grind` upward propagator on `CategoryTheory.CategoryStruct.comp`
+that, every time `grind` internalizes a composition `f ≫ g`, pushes the
+equality `f ≫ g = (right-associated form with identity factors removed)`
+back into the e-graph.
+
+The reason this is a propagator rather than a set of `@[grind]`-tagged
+lemmas: tagging `Category.assoc`, `Category.id_comp`, `Category.comp_id`
+with `@[grind]` causes e-matching to instantiate `Category.assoc` once
+per parenthesization of every composition chain — for a chain of length
+`n` that is Catalan(n − 1) instantiations. The e-graph blows up. (Mathlib
+already has the runaway documented at
+`Mathlib/CategoryTheory/Iso.lean:146`.) A propagator that commits to a
+single canonical representative per fresh composition avoids the blowup:
+the normalized form is a fixed point of itself, so the propagator only
+does work once per user-visible composition.
+
+The rewrite is delegated to `simp` with a three-lemma simp set
+(`Category.id_comp`, `Category.comp_id`, `Category.assoc`); we just feed
+simp's result back into `grind`'s e-graph.
+-/
+
+@[expose] public section
+
+namespace Mathlib.Tactic.CategoryTheory.GrindCatNorm
+
+open Lean Meta
+
+initialize registerTraceClass `grind.catNorm
+
+/-- Cheap syntactic check: `e` is `f ≫ g` already in right-associated
+form with no `𝟙 _` factors. Used to short-circuit before invoking simp. -/
+partial def isNormal (e : Expr) : Bool :=
+  match_expr e with
+  | CategoryTheory.CategoryStruct.comp _ _ _ _ _ l r =>
+    !l.isAppOf ``CategoryTheory.CategoryStruct.comp &&
+    !l.isAppOf ``CategoryTheory.CategoryStruct.id &&
+    !r.isAppOf ``CategoryTheory.CategoryStruct.id &&
+    (!r.isAppOf ``CategoryTheory.CategoryStruct.comp || isNormal r)
+  | _ => true
+
+/-- The propagator body. -/
+def catCompPropagatorImpl (e : Expr) : Grind.GoalM Unit := do
+  unless e.isAppOfArity ``CategoryTheory.CategoryStruct.comp 7 do return ()
+  if isNormal e then return ()
+  -- `simp` may throw if no `Category` instance is available for the
+  -- composition's `CategoryStruct`; we silently skip in that case but
+  -- trace the exception so future regressions aren't invisible.
+  let r ← try
+    simpOnlyNames
+      [``CategoryTheory.Category.id_comp,
+       ``CategoryTheory.Category.comp_id,
+       ``CategoryTheory.Category.assoc] e (config := { decide := false })
+  catch ex =>
+    trace[grind.catNorm] "skipped: {ex.toMessageData}"
+    return ()
+  if Lean.Meta.Sym.isSameExpr e r.expr then return ()
+  trace[grind.catNorm] "{e} ↦ {r.expr}"
+  let e' ← Grind.shareCommon r.expr
+  let proof ← r.getProof' e
+  let gen ← Grind.getGeneration e
+  Grind.internalize e' gen (some e)
+  Grind.pushEq e e' proof
+
+initialize
+  let name := ``CategoryTheory.CategoryStruct.comp
+  Lean.Meta.Grind.registerBuiltinUpwardPropagator name catCompPropagatorImpl
+
+end Mathlib.Tactic.CategoryTheory.GrindCatNorm

MathlibTest/CategoryTheory/GrindCatNorm.lean

@@ -0,0 +1,94 @@
+import Mathlib.CategoryTheory.Tactic.GrindCatNorm
+
+/-!
+# Regression tests for the `grind` category-composition normalizer
+
+The propagator pushes the equality `f ≫ g = (right-associated, identity-free
+form)` into grind's e-graph for each composition it sees. With the
+permanent `@[grind]` attributes on `Category.assoc` / `id_comp` /
+`comp_id` removed, these examples are not solvable by `grind` via
+e-matching alone; they only close because the propagator is loaded.
+-/
+
+open CategoryTheory
+
+universe v u
+
+variable {C : Type u} [Category.{v} C]
+
+section AssociativityOnly
+
+example {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) :
+    (f ≫ g) ≫ h = f ≫ (g ≫ h) := by grind
+
+example {X Y Z W V : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (k : W ⟶ V) :
+    ((f ≫ g) ≫ h) ≫ k = f ≫ g ≫ h ≫ k := by grind
+
+example {X Y Z W V : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (k : W ⟶ V) :
+    (f ≫ g) ≫ (h ≫ k) = f ≫ (g ≫ h) ≫ k := by grind
+
+example {X₁ X₂ X₃ X₄ X₅ X₆ : C}
+    (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (f₃ : X₃ ⟶ X₄) (f₄ : X₄ ⟶ X₅) (f₅ : X₅ ⟶ X₆) :
+    ((f₁ ≫ f₂) ≫ f₃) ≫ (f₄ ≫ f₅) = f₁ ≫ (f₂ ≫ f₃ ≫ f₄) ≫ f₅ := by grind
+
+end AssociativityOnly
+
+section IdentityRemoval
+
+example {X Y : C} (f : X ⟶ Y) : 𝟙 X ≫ f = f := by grind
+example {X Y : C} (f : X ⟶ Y) : f ≫ 𝟙 Y = f := by grind
+example {X : C} : 𝟙 X ≫ 𝟙 X = 𝟙 X := by grind
+
+example {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    f ≫ 𝟙 Y ≫ g = f ≫ g := by grind
+
+example {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    (𝟙 X ≫ f) ≫ (g ≫ 𝟙 Z) = f ≫ g := by grind
+
+end IdentityRemoval
+
+section Mixed
+
+example {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) :
+    (𝟙 X ≫ (f ≫ g)) ≫ h ≫ 𝟙 W = f ≫ g ≫ h := by grind
+
+example {X₁ X₂ X₃ X₄ X₅ : C}
+    (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (f₃ : X₃ ⟶ X₄) (f₄ : X₄ ⟶ X₅) :
+    𝟙 X₁ ≫ ((f₁ ≫ 𝟙 X₂) ≫ f₂) ≫ (𝟙 X₃ ≫ f₃ ≫ 𝟙 X₄) ≫ f₄ ≫ 𝟙 X₅ =
+      f₁ ≫ f₂ ≫ f₃ ≫ f₄ := by grind
+
+end Mixed
+
+section WithHypotheses
+
+/-- Composition with a hypothesis that needs to flow through the normalizer. -/
+example {X Y Z W : C} (f₁ f₂ : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W)
+    (hfg : f₁ ≫ g = f₂ ≫ g) :
+    (f₁ ≫ g) ≫ h = (f₂ ≫ g) ≫ h := by grind
+
+end WithHypotheses
+
+section ReducibleAliases
+
+/-- A reducible alias for the morphism type should not hide the
+underlying composition head from the propagator. -/
+private def MorAlias (Y X : C) := X ⟶ Y
+
+example {X Y Z W : C} (f : MorAlias Y X) (g : MorAlias Z Y) (h : MorAlias W Z) :
+    (f ≫ g) ≫ h = f ≫ (g ≫ h) := by grind
+
+end ReducibleAliases
+
+section LongChain
+
+-- Performance guard: a 10-morphism left-associated chain should
+-- normalize in well under the default heart-beat budget. If this starts
+-- failing, the normalizer's per-prefix work has likely regressed.
+set_option maxHeartbeats 200000 in
+example {X₀ X₁ X₂ X₃ X₄ X₅ X₆ X₇ X₈ X₉ X₁₀ : C}
+    (f₁ : X₀ ⟶ X₁) (f₂ : X₁ ⟶ X₂) (f₃ : X₂ ⟶ X₃) (f₄ : X₃ ⟶ X₄) (f₅ : X₄ ⟶ X₅)
+    (f₆ : X₅ ⟶ X₆) (f₇ : X₆ ⟶ X₇) (f₈ : X₇ ⟶ X₈) (f₉ : X₈ ⟶ X₉) (f₁₀ : X₉ ⟶ X₁₀) :
+    ((((((((f₁ ≫ f₂) ≫ f₃) ≫ f₄) ≫ f₅) ≫ f₆) ≫ f₇) ≫ f₈) ≫ f₉) ≫ f₁₀ =
+      f₁ ≫ f₂ ≫ f₃ ≫ f₄ ≫ f₅ ≫ f₆ ≫ f₇ ≫ f₈ ≫ f₉ ≫ f₁₀ := by grind
+
+end LongChain