From 3f3e197b5640a044df11a2280f7da917d45afb26 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 25 Jun 2024 21:55:45 +0000 Subject: [PATCH 1/2] chore: add `induction_eliminator` and `cases_eliminator` for free objects --- Mathlib/Algebra/Free.lean | 9 +++++---- Mathlib/Algebra/FreeAlgebra.lean | 2 +- Mathlib/Algebra/FreeMonoid/Basic.lean | 10 ++++++---- Mathlib/GroupTheory/FreeGroup/Basic.lean | 2 +- Mathlib/RingTheory/FreeCommRing.lean | 2 +- Mathlib/RingTheory/FreeRing.lean | 2 +- 6 files changed, 15 insertions(+), 12 deletions(-) diff --git a/Mathlib/Algebra/Free.lean b/Mathlib/Algebra/Free.lean index 648067430b633f..3032a5d87c6ddd 100644 --- a/Mathlib/Algebra/Free.lean +++ b/Mathlib/Algebra/Free.lean @@ -72,8 +72,8 @@ attribute [nolint simpNF] FreeAddMagma.add.injEq attribute [nolint simpNF] FreeMagma.mul.injEq /-- Recursor for `FreeMagma` using `x * y` instead of `FreeMagma.mul x y`. -/ -@[to_additive (attr := elab_as_elim) "Recursor for `FreeAddMagma` using `x + y` instead of -`FreeAddMagma.add x y`."] +@[to_additive (attr := elab_as_elim, induction_eliminator) + "Recursor for `FreeAddMagma` using `x + y` instead of `FreeAddMagma.add x y`."] def recOnMul {C : FreeMagma α → Sort l} (x) (ih1 : ∀ x, C (of x)) (ih2 : ∀ x y, C x → C y → C (x * y)) : C x := FreeMagma.recOn x ih1 ih2 @@ -394,7 +394,7 @@ def of : α →ₙ* AssocQuotient α where toFun := Quot.mk _; map_mul' _x _y := @[to_additive] instance [Inhabited α] : Inhabited (AssocQuotient α) := ⟨of default⟩ -@[to_additive (attr := elab_as_elim)] +@[to_additive (attr := elab_as_elim, induction_eliminator)] protected theorem induction_on {C : AssocQuotient α → Prop} (x : AssocQuotient α) (ih : ∀ x, C (of x)) : C x := Quot.induction_on x ih #align magma.assoc_quotient.induction_on Magma.AssocQuotient.induction_on @@ -517,7 +517,8 @@ theorem length_of (x : α) : (of x).length = 1 := rfl instance [Inhabited α] : Inhabited (FreeSemigroup α) := ⟨of default⟩ /-- Recursor for free semigroup using `of` and `*`. -/ -@[to_additive (attr := elab_as_elim) "Recursor for free additive semigroup using `of` and `+`."] +@[to_additive (attr := elab_as_elim, induction_eliminator) + "Recursor for free additive semigroup using `of` and `+`."] protected def recOnMul {C : FreeSemigroup α → Sort l} (x) (ih1 : ∀ x, C (of x)) (ih2 : ∀ x y, C (of x) → C y → C (of x * y)) : C x := FreeSemigroup.recOn x fun f s ↦ diff --git a/Mathlib/Algebra/FreeAlgebra.lean b/Mathlib/Algebra/FreeAlgebra.lean index 1e11d512b8c1a0..d2af0a3ff51d55 100644 --- a/Mathlib/Algebra/FreeAlgebra.lean +++ b/Mathlib/Algebra/FreeAlgebra.lean @@ -563,7 +563,7 @@ namespace FreeAlgebra If `C` holds for the `algebraMap` of `r : R` into `FreeAlgebra R X`, the `ι` of `x : X`, and is preserved under addition and muliplication, then it holds for all of `FreeAlgebra R X`. -/ -@[elab_as_elim] +@[elab_as_elim, induction_eliminator] theorem induction {C : FreeAlgebra R X → Prop} (h_grade0 : ∀ r, C (algebraMap R (FreeAlgebra R X) r)) (h_grade1 : ∀ x, C (ι R x)) (h_mul : ∀ a b, C a → C b → C (a * b)) (h_add : ∀ a b, C a → C b → C (a + b)) diff --git a/Mathlib/Algebra/FreeMonoid/Basic.lean b/Mathlib/Algebra/FreeMonoid/Basic.lean index aa2eec16554d7e..55b30bfc44c2c8 100644 --- a/Mathlib/Algebra/FreeMonoid/Basic.lean +++ b/Mathlib/Algebra/FreeMonoid/Basic.lean @@ -151,8 +151,9 @@ theorem of_injective : Function.Injective (@of α) := List.singleton_injective #align free_add_monoid.of_injective FreeAddMonoid.of_injective /-- Recursor for `FreeMonoid` using `1` and `FreeMonoid.of x * xs` instead of `[]` and `x :: xs`. -/ -@[to_additive (attr := elab_as_elim) "Recursor for `FreeAddMonoid` using `0` and -`FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`."] +@[to_additive (attr := elab_as_elim, induction_eliminator) + "Recursor for `FreeAddMonoid` using `0` and + FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`."] -- Porting note: change from `List.recOn` to `List.rec` since only the latter is computable def recOn {C : FreeMonoid α → Sort*} (xs : FreeMonoid α) (h0 : C 1) (ih : ∀ x xs, C xs → C (of x * xs)) : C xs := List.rec h0 ih xs @@ -174,8 +175,9 @@ theorem recOn_of_mul {C : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α) /-- A version of `List.cases_on` for `FreeMonoid` using `1` and `FreeMonoid.of x * xs` instead of `[]` and `x :: xs`. -/ -@[to_additive (attr := elab_as_elim) "A version of `List.casesOn` for `FreeAddMonoid` using `0` and -`FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`."] +@[to_additive (attr := elab_as_elim, cases_eliminator) + "A version of `List.casesOn` for `FreeAddMonoid` using `0` and + `FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`."] def casesOn {C : FreeMonoid α → Sort*} (xs : FreeMonoid α) (h0 : C 1) (ih : ∀ x xs, C (of x * xs)) : C xs := List.casesOn xs h0 ih #align free_monoid.cases_on FreeMonoid.casesOn diff --git a/Mathlib/GroupTheory/FreeGroup/Basic.lean b/Mathlib/GroupTheory/FreeGroup/Basic.lean index c35692f12b3d43..ede6ac018b3740 100644 --- a/Mathlib/GroupTheory/FreeGroup/Basic.lean +++ b/Mathlib/GroupTheory/FreeGroup/Basic.lean @@ -1027,7 +1027,7 @@ instance : Monad FreeGroup.{u} where map {_α} {_β} {f} := map f bind {_α} {_β} {x} {f} := lift f x -@[to_additive (attr := elab_as_elim)] +@[to_additive (attr := elab_as_elim, induction_eliminator)] protected theorem induction_on {C : FreeGroup α → Prop} (z : FreeGroup α) (C1 : C 1) (Cp : ∀ x, C <| pure x) (Ci : ∀ x, C (pure x) → C (pure x)⁻¹) (Cm : ∀ x y, C x → C y → C (x * y)) : C z := diff --git a/Mathlib/RingTheory/FreeCommRing.lean b/Mathlib/RingTheory/FreeCommRing.lean index c6ab449d76bf96..75367891411401 100644 --- a/Mathlib/RingTheory/FreeCommRing.lean +++ b/Mathlib/RingTheory/FreeCommRing.lean @@ -95,7 +95,7 @@ lemma of_cons (a : α) (m : Multiset α) : (FreeAbelianGroup.of (Multiplicative. rw [← Multiset.singleton_add, ofAdd_add, of, FreeAbelianGroup.of_mul_of] -@[elab_as_elim] +@[elab_as_elim, induction_eliminator] protected theorem induction_on {C : FreeCommRing α → Prop} (z : FreeCommRing α) (hn1 : C (-1)) (hb : ∀ b, C (of b)) (ha : ∀ x y, C x → C y → C (x + y)) (hm : ∀ x y, C x → C y → C (x * y)) : C z := diff --git a/Mathlib/RingTheory/FreeRing.lean b/Mathlib/RingTheory/FreeRing.lean index ef29344c15a9a9..f83cc2d6c1e771 100644 --- a/Mathlib/RingTheory/FreeRing.lean +++ b/Mathlib/RingTheory/FreeRing.lean @@ -56,7 +56,7 @@ theorem of_injective : Function.Injective (of : α → FreeRing α) := FreeAbelianGroup.of_injective.comp FreeMonoid.of_injective #align free_ring.of_injective FreeRing.of_injective -@[elab_as_elim] +@[elab_as_elim, induction_eliminator] protected theorem induction_on {C : FreeRing α → Prop} (z : FreeRing α) (hn1 : C (-1)) (hb : ∀ b, C (of b)) (ha : ∀ x y, C x → C y → C (x + y)) (hm : ∀ x y, C x → C y → C (x * y)) : C z := From bb4a1bbf643e35760c62acb861cea27611de9906 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 25 Jun 2024 22:01:28 +0000 Subject: [PATCH 2/2] clean up uses --- Mathlib/Algebra/FreeAlgebra.lean | 2 +- Mathlib/Algebra/Group/Submonoid/Membership.lean | 2 +- Mathlib/GroupTheory/Coprod/Basic.lean | 4 ++-- Mathlib/RingTheory/FreeCommRing.lean | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/Algebra/FreeAlgebra.lean b/Mathlib/Algebra/FreeAlgebra.lean index d2af0a3ff51d55..9fea13f2f28f94 100644 --- a/Mathlib/Algebra/FreeAlgebra.lean +++ b/Mathlib/Algebra/FreeAlgebra.lean @@ -591,7 +591,7 @@ theorem induction {C : FreeAlgebra R X → Prop} theorem adjoin_range_ι : Algebra.adjoin R (Set.range (ι R : X → FreeAlgebra R X)) = ⊤ := by set S := Algebra.adjoin R (Set.range (ι R : X → FreeAlgebra R X)) refine top_unique fun x hx => ?_; clear hx - induction x using FreeAlgebra.induction with + induction x with | h_grade0 => exact S.algebraMap_mem _ | h_add x y hx hy => exact S.add_mem hx hy | h_mul x y hx hy => exact S.mul_mem hx hy diff --git a/Mathlib/Algebra/Group/Submonoid/Membership.lean b/Mathlib/Algebra/Group/Submonoid/Membership.lean index 6854eaf07baef5..8f0f193d9bcfbc 100644 --- a/Mathlib/Algebra/Group/Submonoid/Membership.lean +++ b/Mathlib/Algebra/Group/Submonoid/Membership.lean @@ -419,7 +419,7 @@ theorem closure_induction_left {s : Set M} {p : (m : M) → m ∈ closure s → p x h := by simp_rw [closure_eq_mrange] at h obtain ⟨l, rfl⟩ := h - induction' l using FreeMonoid.recOn with x y ih + induction' l with x y ih · exact one · simp only [map_mul, FreeMonoid.lift_eval_of] refine mul_left _ x.prop (FreeMonoid.lift Subtype.val y) _ (ih ?_) diff --git a/Mathlib/GroupTheory/Coprod/Basic.lean b/Mathlib/GroupTheory/Coprod/Basic.lean index 63133b524f9a47..074c49ee752d21 100644 --- a/Mathlib/GroupTheory/Coprod/Basic.lean +++ b/Mathlib/GroupTheory/Coprod/Basic.lean @@ -191,7 +191,7 @@ theorem induction_on' {C : M ∗ N → Prop} (m : M ∗ N) (inl_mul : ∀ m x, C x → C (inl m * x)) (inr_mul : ∀ n x, C x → C (inr n * x)) : C m := by rcases mk_surjective m with ⟨x, rfl⟩ - induction x using FreeMonoid.recOn with + induction x with | h0 => exact one | ih x xs ih => cases x with @@ -573,7 +573,7 @@ theorem mk_of_inv_mul : ∀ x : G ⊕ H, mk (of (x.map Inv.inv Inv.inv)) * mk (o theorem con_mul_left_inv (x : FreeMonoid (G ⊕ H)) : coprodCon G H (ofList (x.toList.map (Sum.map Inv.inv Inv.inv)).reverse * x) 1 := by rw [← mk_eq_mk, map_mul, map_one] - induction x using FreeMonoid.recOn with + induction x with | h0 => simp [map_one mk] -- TODO: fails without `[map_one mk]` | ih x xs ihx => simp only [toList_of_mul, map_cons, reverse_cons, ofList_append, map_mul, ihx, ofList_singleton] diff --git a/Mathlib/RingTheory/FreeCommRing.lean b/Mathlib/RingTheory/FreeCommRing.lean index 75367891411401..865c6c8e4f0e6a 100644 --- a/Mathlib/RingTheory/FreeCommRing.lean +++ b/Mathlib/RingTheory/FreeCommRing.lean @@ -360,7 +360,7 @@ protected theorem coe_mul (x y : FreeRing α) : ↑(x * y) = (x : FreeCommRing variable (α) protected theorem coe_surjective : Surjective ((↑) : FreeRing α → FreeCommRing α) := fun x => by - induction x using FreeCommRing.induction_on with + induction x with | hn1 => use -1 rfl