Merge master into nightly-testing

Author: leanprover-community-mathlib4-bot

Mathlib.lean

@@ -5611,6 +5611,7 @@ import Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
 import Mathlib.Tactic.CategoryTheory.Coherence.Normalize
 import Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
 import Mathlib.Tactic.CategoryTheory.Elementwise
+import Mathlib.Tactic.CategoryTheory.IsoReassoc
 import Mathlib.Tactic.CategoryTheory.Monoidal.Basic
 import Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
 import Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Mathlib/Tactic.lean

@@ -36,6 +36,7 @@ import Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
 import Mathlib.Tactic.CategoryTheory.Coherence.Normalize
 import Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
 import Mathlib.Tactic.CategoryTheory.Elementwise
+import Mathlib.Tactic.CategoryTheory.IsoReassoc
 import Mathlib.Tactic.CategoryTheory.Monoidal.Basic
 import Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
 import Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Mathlib/Tactic/CategoryTheory/IsoReassoc.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2025 Robin Carlier. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robin Carlier
+-/
+import Mathlib.CategoryTheory.Iso
+
+/-!
+# Extension of `reassoc` to isomorphisms.
+
+We extend `reassoc` and `reassoc_of%` for equality of isomorphisms.
+Adding `@[reassoc]` to a lemma named `F` of shape `∀ .., f = g`,
+where `f g : X ≅ Y` in some category will create a new lemma named `F_assoc` of shape
+`∀ .. {Z : C} (h : Y ≅ Z), f ≪≫ h = g ≪≫ h`
+but with the conclusions simplified using basic propertions in isomorphisms in a category
+(`Iso.trans_refl`, `Iso.refl_trans`, `Iso.trans_assoc`, `Iso.trans_symm`,
+`Iso.symm_self_id` and `Iso.self_symm_id`).
+
+This is useful for generating lemmas which the simplifier can use even on expressions
+that are already right associated.
+-/
+
+open Lean Meta Elab Tactic
+open Mathlib.Tactic
+
+namespace CategoryTheory
+
+variable {C : Type*} [Category C]
+
+theorem Iso.eq_whisker {X Y : C} {f g : X ≅ Y} (w : f = g) {Z : C} (h : Y ≅ Z) :
+    f ≪≫ h = g ≪≫ h := by rw [w]
+
+/-- Simplify an expression using only the axioms of a groupoid. -/
+def categoryIsoSimp (e : Expr) : MetaM Simp.Result :=
+  simpOnlyNames [``Iso.trans_symm, ``Iso.trans_refl, ``Iso.refl_trans, ``Iso.trans_assoc,
+    ``Iso.symm_self_id, ``Iso.self_symm_id, ``Iso.symm_self_id_assoc, ``Iso.self_symm_id_assoc,
+    ``Functor.mapIso_trans, ``Functor.mapIso_symm, ``Functor.mapIso_refl, ``Functor.id_obj] e
+    (config := { decide := false })
+
+/--
+Given an equation `f = g` between isomorphisms `X ≅ Y` in a category,
+produce the equation `∀ {Z} (h : Y ≅ Z), f ≪≫ h = g ≪≫ h`,
+but with compositions fully right associated, identities removed, and functors applied.
+-/
+def reassocExprIso (e : Expr) : MetaM Expr := do
+  simpType categoryIsoSimp (← mkAppM ``Iso.eq_whisker #[e])
+
+initialize registerReassocExpr reassocExprIso
+
+end CategoryTheory

Mathlib/Tactic/CategoryTheory/Reassoc.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
+Authors: Kim Morrison, Robin Carlier
 -/
 import Mathlib.CategoryTheory.Functor.Basic
 import Mathlib.Lean.Meta.Simp
@@ -22,6 +22,9 @@ This is useful for generating lemmas which the simplifier can use even on expres
 that are already right associated.
 
 There is also a term elaborator `reassoc_of% t` for use within proofs.
+
+The `Mathlib.Tactic.CategoryTheory.IsoReassoc` extends `@[reassoc]` and `reassoc_of%`
+to support creating isomorphism reassociation lemmas.
 -/
 
 open Lean Meta Elab Tactic
@@ -42,12 +45,12 @@ def categorySimp (e : Expr) : MetaM Simp.Result :=
     (config := { decide := false })
 
 /--
-Given an equation `f = g` between morphisms `X ⟶ Y` in a category (possibly after a `∀` binder),
+Given an equation `f = g` between morphisms `X ⟶ Y` in a category,
 produce the equation `∀ {Z} (h : Y ⟶ Z), f ≫ h = g ≫ h`,
 but with compositions fully right associated and identities removed.
 -/
-def reassocExpr (e : Expr) : MetaM Expr := do
-  mapForallTelescope (fun e => do simpType categorySimp (← mkAppM ``eq_whisker' #[e])) e
+def reassocExprHom (e : Expr) : MetaM Expr := do
+  simpType categorySimp (← mkAppM ``eq_whisker' #[e])
 
 /--
 Adding `@[reassoc]` to a lemma named `F` of shape `∀ .., f = g`, where `f g : X ⟶ Y` are
@@ -66,9 +69,44 @@ Note that if you want both the lemma and the reassociated lemma to be
 `simp` lemmas, you should tag the lemma `@[reassoc (attr := simp)]`.
 The variant `@[simp, reassoc]` on a lemma `F` will tag `F` with `@[simp]`,
 but not `F_assoc` (this is sometimes useful).
+
+This attribute also works for lemmas of shape `∀ .., f = g` where `f g : X ≅ Y` are
+isomorphisms, provided that `Tactic.CategoryTheory.IsoReassoc` has been imported.
 -/
 syntax (name := reassoc) "reassoc" (" (" &"attr" " := " Parser.Term.attrInstance,* ")")? : attr
 
+/--
+IO ref for reassociation handlers `reassoc` attribute, so that it can be extended
+with additional handlers. Handlers take a proof of the equation.
+
+The default handler is `reassocExprHom` for morphism reassociation.
+This will be extended in `Tactic.CategoryTheory.IsoReassoc` for isomorphism reassociation.
+-/
+private initialize reassocImplRef : IO.Ref (Array (Expr → MetaM Expr)) ← IO.mkRef #[]
+
+/--
+Registers a handler for `reassocExpr`. The handler takes a proof of an equation
+and returns a proof of the reassociation lemma.
+Handlers are considered in order of registration.
+They are applied directly to the equation in the body of the forall.
+-/
+def registerReassocExpr (f : Expr → MetaM Expr) : IO Unit := do
+  reassocImplRef.modify (·.push f)
+
+initialize registerReassocExpr reassocExprHom
+
+/--
+Reassociates the morphisms in `type?` using the registered handlers,
+using `reassocExprHom` as the default.
+If `type?` is not given, it is assumed to be the type of `pf`.
+-/
+def reassocExpr (pf : Expr) (type? : Option Expr) : MetaM Expr := do
+  let pf ← if let some type := type? then mkExpectedTypeHint pf type else pure pf
+  mapForallTelescope (forallTerm := pf) fun pf => do
+    let handlers ← reassocImplRef.get
+    handlers.firstM (fun h => h pf) <|> do
+      throwError "`reassoc` can only be used on terms about equality of (iso)morphisms"
+
 initialize registerBuiltinAttribute {
   name := `reassoc
   descr := ""
@@ -78,17 +116,19 @@ initialize registerBuiltinAttribute {
     if (kind != AttributeKind.global) then
       throwError "`reassoc` can only be used as a global attribute"
     addRelatedDecl src "_assoc" ref stx? fun type value levels => do
-      pure (← reassocExpr (← mkExpectedTypeHint value type), levels)
+      pure (← reassocExpr value type, levels)
   | _ => throwUnsupportedSyntax }
 
-open Term in
 /--
 `reassoc_of% t`, where `t` is
 an equation `f = g` between morphisms `X ⟶ Y` in a category (possibly after a `∀` binder),
 produce the equation `∀ {Z} (h : Y ⟶ Z), f ≫ h = g ≫ h`,
 but with compositions fully right associated and identities removed.
+This also works for equations between isomorphisms, provided that
+`Tactic.CategoryTheory.IsoReassoc` has been imported.
 -/
 elab "reassoc_of% " t:term : term => do
-  reassocExpr (← elabTerm t none)
+  let e ← Term.elabTerm t none
+  reassocExpr e none
 
 end CategoryTheory

MathlibTest/CategoryTheory/Reassoc.lean

@@ -0,0 +1,71 @@
+import Mathlib.Tactic.CategoryTheory.IsoReassoc
+
+open CategoryTheory
+namespace Tests.Reassoc
+
+universe v₁ v₂ v₃ u₁ u₂ u₃
+
+variable {C : Type u₁} {D : Type u₂} {E : Type u₃}
+  [Category.{v₁} C] [Category.{v₂} D] [Category.{v₃} E]
+  {F : C ⥤ D} {G : D ⥤ E}
+
+@[reassoc]
+lemma foo {x y z : C} (f : x ⟶ y) (g : y ⟶ z) (h : x ⟶ z) (w : f ≫ g = h) :
+    f ≫ g = h := w
+
+@[reassoc]
+lemma foo_iso {x y z : C} (f : x ≅ y) (g : y ≅ z) (h : x ≅ z) (w : f ≪≫ g = h) :
+    f ≪≫ g = h := w
+
+/--
+info: Tests.Reassoc.foo_assoc.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {x y z : C} (f : x ⟶ y) (g : y ⟶ z) (h : x ⟶ z)
+  (w : f ≫ g = h) {Z : C} (h✝ : z ⟶ Z) : f ≫ g ≫ h✝ = h ≫ h✝
+-/
+#guard_msgs in
+#check foo_assoc
+
+/--
+info: Tests.Reassoc.foo_iso_assoc.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {x y z : C} (f : x ≅ y) (g : y ≅ z) (h : x ≅ z)
+  (w : f ≪≫ g = h) {Z : C} (h✝ : z ≅ Z) : f ≪≫ g ≪≫ h✝ = h ≪≫ h✝
+-/
+#guard_msgs in
+#check foo_iso_assoc
+
+/-- error: `reassoc` can only be used on terms about equality of (iso)morphisms -/
+#guard_msgs in
+@[reassoc]
+def one : Nat := 1
+
+/-- error: `reassoc` can only be used on terms about equality of (iso)morphisms -/
+#guard_msgs in
+@[reassoc]
+def one_plus_one : 1 + 1 = 2 := rfl
+
+@[reassoc]
+lemma foo_functor {x y z : C} (f : x ≅ y) (g : y ≅ z) (h : x ≅ z)
+    (w : F.mapIso (f ≪≫ g) = F.mapIso h) :
+    F.mapIso (f ≪≫ g) = F.mapIso h := w
+
+/--
+info: Tests.Reassoc.foo_functor_assoc.{v₁, v₂, u₁, u₂} {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D]
+  {F : C ⥤ D} {x y z : C} (f : x ≅ y) (g : y ≅ z) (h : x ≅ z) (w : F.mapIso (f ≪≫ g) = F.mapIso h) {Z : D}
+  (h✝ : F.obj z ≅ Z) : F.mapIso f ≪≫ F.mapIso g ≪≫ h✝ = F.mapIso h ≪≫ h✝
+-/
+#guard_msgs in
+#check foo_functor_assoc
+
+@[reassoc]
+lemma foo_functor' {x y z : C} (f : x ≅ y) (g : y ≅ z) (h : x ≅ z)
+    (w : F.mapIso (f ≪≫ g) = F.mapIso h) {Z : D} (e : F.obj z ≅ Z) :
+    F.mapIso f ≪≫ F.mapIso g ≪≫ e = F.mapIso h ≪≫ e := (reassoc_of% w) e
+
+-- checking that _assoc expressions are indeed right_associated:
+/--
+info: Tests.Reassoc.foo_functor'_assoc.{v₁, v₂, u₁, u₂} {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C]
+  [Category.{v₂, u₂} D] {F : C ⥤ D} {x y z : C} (f : x ≅ y) (g : y ≅ z) (h : x ≅ z) (w : F.mapIso (f ≪≫ g) = F.mapIso h)
+  {Z : D} (e : F.obj z ≅ Z) {Z✝ : D} (h✝ : Z ≅ Z✝) : F.mapIso f ≪≫ F.mapIso g ≪≫ e ≪≫ h✝ = F.mapIso h ≪≫ e ≪≫ h✝
+-/
+#guard_msgs in
+#check foo_functor'_assoc
+
+end Tests.Reassoc