From 383fdb645cf41f8ef6a788ad3d12d3d3da5e6725 Mon Sep 17 00:00:00 2001 From: Anne Baanen Date: Fri, 17 Jan 2025 18:04:09 +0000 Subject: [PATCH] feat(Tactic): basic ConcreteCategory support for elementwise (#20811) This is a step towards a concrete category redesign, as outlined in this Zulip post: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign/near/493903980 This PR adds basic support for `ConcreteCategory` to the `elementwise` attribute and elaborator: it still uses `HasForget` when a fresh instance is needed, but now will replace the `forget`-based operations with `ConcreteCategory`-based ones. So as long as there is only a `HasForget` instance, or no instance at all, in scope, `elementwise` will behave the same. But when there is a `ConcreteCategory` instance, all the `(forget C).obj X`es turn into `ToType X` and `(forget C).map f`s turn into `hom f`. In the future, when we have replaced enough `HasForget` instances with `ConcreteCategory`, we can apply the changes from the branch `redesign-ConcreteCategory` to make `elementwise` use `ConcreteCategory` when it creates fresh instances. --- .../ConcreteCategory/Basic.lean | 7 + .../Tactic/CategoryTheory/Elementwise.lean | 10 +- MathlibTest/CategoryTheory/Elementwise.lean | 174 ++++++++++++++++++ 3 files changed, 189 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean index 55f2c36323721..5057020dc6114 100644 --- a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean +++ b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean @@ -355,6 +355,13 @@ theorem hom_id {X : C} : (𝟙 X : ToType X → ToType X) = id := theorem hom_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g : ToType X → ToType Z) = g ∘ f := (forget _).map_comp f g +/-- Using the `FunLike` coercion of `HasForget` does the same as the original coercion. +-/ +theorem coe_toHasForget_instFunLike {C : Type*} [Category C] {FC : C → C → Type*} {CC : C → Type*} + [inst : ∀ X Y : C, FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X Y : C} + (f : X ⟶ Y) : + @DFunLike.coe (X ⟶ Y) (ToType X) (fun _ => ToType Y) HasForget.instFunLike f = f := rfl + section variable (C) diff --git a/Mathlib/Tactic/CategoryTheory/Elementwise.lean b/Mathlib/Tactic/CategoryTheory/Elementwise.lean index ff726b22fa41d..dc62fc50607d5 100644 --- a/Mathlib/Tactic/CategoryTheory/Elementwise.lean +++ b/Mathlib/Tactic/CategoryTheory/Elementwise.lean @@ -56,10 +56,16 @@ end theorems /-- List of simp lemmas to apply to the elementwise theorem. -/ def elementwiseThms : List Name := - [``CategoryTheory.coe_id, ``CategoryTheory.coe_comp, ``CategoryTheory.comp_apply, + [ -- HasForget lemmas + ``CategoryTheory.coe_id, ``CategoryTheory.coe_comp, ``CategoryTheory.comp_apply, ``CategoryTheory.id_apply, + -- ConcreteCategory lemmas + ``CategoryTheory.hom_id, ``CategoryTheory.hom_comp, ``id_eq, ``Function.comp_apply, -- further simplifications if the category is `Type` - ``forget_hom_Type, ``forall_congr_forget_Type, + ``forget_hom_Type, ``forall_congr_forget_Type, ``types_comp_apply, ``types_id_apply, + -- further simplifications to turn `HasForget` definitions into `ConcreteCategory` ones + -- (if available) + ``forget_obj, ``ConcreteCategory.forget_map_eq_coe, ``coe_toHasForget_instFunLike, -- simp can itself simplify trivial equalities into `true`. Adding this lemma makes it -- easier to detect when this has occurred. ``implies_true] diff --git a/MathlibTest/CategoryTheory/Elementwise.lean b/MathlibTest/CategoryTheory/Elementwise.lean index fd9a3578265a6..b2c18b4f5064c 100644 --- a/MathlibTest/CategoryTheory/Elementwise.lean +++ b/MathlibTest/CategoryTheory/Elementwise.lean @@ -6,6 +6,8 @@ set_option autoImplicit true namespace ElementwiseTest open CategoryTheory +namespace HasForget + attribute [simp] Iso.hom_inv_id Iso.inv_hom_id IsIso.hom_inv_id IsIso.inv_hom_id attribute [local instance] HasForget.instFunLike HasForget.hasCoeToSort @@ -134,4 +136,176 @@ variable (X : C) [HasForget C] (x : X) #guard_msgs in #check fh_apply X x +end HasForget + +namespace ConcreteCategory + +attribute [simp] Iso.hom_inv_id Iso.inv_hom_id IsIso.hom_inv_id IsIso.inv_hom_id + +attribute [simp] Iso.hom_inv_id Iso.inv_hom_id IsIso.hom_inv_id IsIso.inv_hom_id + +variable {C : Type*} {FC : C → C → Type*} {CC : C → Type*} +variable [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] + +@[elementwise] +theorem ex1 [Category C] [ConcreteCategory C FC] (X : C) (f g h : X ⟶ X) (h' : g ≫ h = h ≫ g) : + f ≫ g ≫ h = f ≫ h ≫ g := by rw [h'] + +-- If there is already a `ConcreteCategory` instance, do not add a new argument. +example : ∀ C {FC : C → C → Type*} {CC : C → Type*} [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] [Category C] [ConcreteCategory C FC] (X : C) (f g h : X ⟶ X) (_ : g ≫ h = h ≫ g) + (x : ToType X), h (g (f x)) = g (h (f x)) := @ex1_apply + +/- +-- TODO: `elementwise` currently uses `HasForget` to generate its lemmas. +-- Enable the commented-out tests below (and replace the corresponding tests above) +-- when we switch to `ConcreteCategory`. + +@[elementwise] +theorem ex2 [Category C] (X : C) (f g h : X ⟶ X) (h' : g ≫ h = h ≫ g) : + f ≫ g ≫ h = f ≫ h ≫ g := by rw [h'] + +-- If there is not already a `ConcreteCategory` instance, insert a new argument. +example : ∀ C [Category C] (X : C) (f g h : X ⟶ X) (_ : g ≫ h = h ≫ g) + {FC : C → C → Type _} {CC : C → Type _} [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] + [ConcreteCategory C FC] + (x : ToType X), h (g (f x)) = g (h (f x)) := @ex2_apply + +-- Need nosimp on the following `elementwise` since the lemma can be proved by simp anyway. +@[elementwise nosimp] +theorem ex3 [Category C] {X Y : C} (f : X ≅ Y) : f.hom ≫ f.inv = 𝟙 X := + Iso.hom_inv_id _ + +example : ∀ C [Category C] (X Y : C) (f : X ≅ Y) + {FC : C → C → Type _} {CC : C → Type _} [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] + [ConcreteCategory C FC] + (x : ToType X), + f.inv (f.hom x) = x := @ex3_apply + +-- Make sure there's no `id x` in there: +example : ∀ C [Category C] (X Y : C) (f : X ≅ Y) + {FC : C → C → Type _} {CC : C → Type _} [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] + [ConcreteCategory C FC] + (x : ToType X), + f.inv (f.hom x) = x := by intros; simp only [ex3_apply] +-/ + +@[elementwise] +lemma foo [Category C] + {M N K : C} {f : M ⟶ N} {g : N ⟶ K} {h : M ⟶ K} (w : f ≫ g = h) : f ≫ 𝟙 N ≫ g = h := by + simp [w] + +@[elementwise] +lemma foo' [Category C] + {M N K : C} {f : M ⟶ N} {g : N ⟶ K} {h : M ⟶ K} (w : f ≫ g = h) : f ≫ 𝟙 N ≫ g = h := by + simp [w] + +lemma bar [Category C] + {FC : C → C → Type _} {CC : C → Type _} [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] + [ConcreteCategory C FC] + {M N K : C} {f : M ⟶ N} {g : N ⟶ K} {h : M ⟶ K} (w : f ≫ g = h) (x : ToType M) : g (f x) = h x := by + apply foo_apply w + +example {M N K : Type} {f : M ⟶ N} {g : N ⟶ K} {h : M ⟶ K} (w : f ≫ g = h) (x : M) : + g (f x) = h x := by + have := elementwise_of% w + guard_hyp this : ∀ (x : M), g (f x) = h x + exact this x + +example {M N K : Type} {f : M ⟶ N} {g : N ⟶ K} {h : M ⟶ K} (w : f ≫ g = h) (x : M) : + g (f x) = h x := (elementwise_of% w) x + +example [Category C] {FC : C → C → Type _} {CC : C → Type _} + [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] + {M N K : C} {f : M ⟶ N} {g : N ⟶ K} {h : M ⟶ K} (w : f ≫ g = h) (x : ToType M) : + g (f x) = h x := by + have := elementwise_of% w + guard_hyp this : ∀ (x : ToType M), g (f x) = h x + exact this x + +/- +-- TODO: `elementwise` currently uses `HasForget` to generate its lemmas. +-- Enable the commented-out tests below (and replace the corresponding tests above) +-- when we switch to `ConcreteCategory`. + +-- `elementwise_of%` allows level metavariables for its `ConcreteCategory` instance. +-- Previously this example did not specify that the universe levels of `C` and `D` (inside `h`) +-- were the same, and this constraint was added post-hoc by the proof term. +-- After https://github.com/leanprover/lean4/pull/4493 this no longer works (happily!). +example {C : Type u} [Category.{v} C] {FC : C → C → Type _} {CC : C → Type w} + [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] + [ConcreteCategory C FC] + (h : ∀ (D : Type u) [Category.{v} D] (X Y : D) (f : X ⟶ Y) (g : Y ⟶ X), f ≫ g = 𝟙 X) + {M N : C} {f : M ⟶ N} {g : N ⟶ M} (x : ToType M) : g (f x) = x := by + have := elementwise_of% h + guard_hyp this : ∀ D [Category D] (X Y : D) (f : X ⟶ Y) (g : Y ⟶ X) {FD : D → D → Type*} + {CD : D → Type*} [∀ X Y, FunLike (FD X Y) (CD X) (CD Y)] + [ConcreteCategory D FD] + (x : ToType X), g (f x) = x + rw [this] +-/ + +section Mon + +lemma bar' {M N K : MonCat} {f : M ⟶ N} {g : N ⟶ K} {h : M ⟶ K} (w : f ≫ g = h) (x : M) : + g (f x) = h x := by exact foo_apply w x + +lemma bar'' {M N K : MonCat} {f : M ⟶ N} {g : N ⟶ K} {h : M ⟶ K} (w : f ≫ g = h) (x : M) : + g (f x) = h x := by apply foo_apply w + +lemma bar''' {M N K : MonCat} {f : M ⟶ N} {g : N ⟶ K} {h : M ⟶ K} (w : f ≫ g = h) (x : M) : + g (f x) = h x := by apply foo_apply w + +example (M N K : MonCat) (f : M ⟶ N) (g : N ⟶ K) (h : M ⟶ K) (w : f ≫ g = h) (m : M) : + g (f m) = h m := by rw [elementwise_of% w] + +example (M N K : MonCat) (f : M ⟶ N) (g : N ⟶ K) (h : M ⟶ K) (w : f ≫ g = h) (m : M) : + g (f m) = h m := by + -- Porting note: did not port `elementwise!` tactic + replace w := elementwise_of% w + apply w + +end Mon + +example {α β : Type} (f g : α ⟶ β) (w : f = g) (a : α) : f a = g a := by + -- Porting note: did not port `elementwise!` tactic + replace w := elementwise_of% w + guard_hyp w : ∀ (x : α), f x = g x + rw [w] + + +example {α β : Type} (f g : α ⟶ β) (w : f ≫ 𝟙 β = g) (a : α) : f a = g a := by + -- Porting note: did not port `elementwise!` tactic + replace w := elementwise_of% w + guard_hyp w : ∀ (x : α), f x = g x + rw [w] + +/- +-- TODO: `elementwise` currently uses `HasForget` to generate its lemmas. +-- Enable the commented-out tests below (and replace the corresponding tests above) +-- when we switch to `ConcreteCategory`. + +variable {C : Type*} [Category C] + +def f (X : C) : X ⟶ X := 𝟙 X +def g (X : C) : X ⟶ X := 𝟙 X +def h (X : C) : X ⟶ X := 𝟙 X + +lemma gh (X : C) : g X = h X := rfl + +@[elementwise] +theorem fh (X : C) : f X = h X := gh X + +variable (X : C) {FC : C → C → Type*} {CC : C → Type*} +variable [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] +variable (x : ToType X) + +-- Prior to https://github.com/leanprover-community/mathlib4/pull/13413 this would produce +-- `fh_apply X x : (g X) x = (h X) x`. +/-- info: fh_apply X x : (ConcreteCategory.hom (f X)) x = (ConcreteCategory.hom (h X)) x -/ +#guard_msgs in +#check fh_apply X x +-/ + +end ConcreteCategory + end ElementwiseTest