feat: irreducible_def: support protected, equation lemmas (#3395)

Mathlib/GroupTheory/MonoidLocalization.lean

@@ -256,25 +256,23 @@ protected def npow : ℕ → Localization S → Localization S := (r S).commMono
 #align localization.npow Localization.npow
 #align add_localization.nsmul addLocalization.nsmul
 
--- Porting note: remove the attribute `local` because of error:
--- invalid attribute 'semireducible', must be global
-attribute [semireducible] Localization.mul Localization.one Localization.npow
-
 @[to_additive]
 instance : CommMonoid (Localization S) where
   mul := (· * ·)
   one := 1
-  mul_assoc :=
-    show ∀ x y z : Localization S, x * y * z = x * (y * z) from (r S).commMonoid.mul_assoc
-  mul_comm := show ∀ x y : Localization S, x * y = y * x from (r S).commMonoid.mul_comm
-  mul_one := show ∀ x : Localization S, x * 1 = x from (r S).commMonoid.mul_one
-  one_mul := show ∀ x : Localization S, 1 * x = x from (r S).commMonoid.one_mul
+  mul_assoc x y z := show (x.mul S y).mul S z = x.mul S (y.mul S z) by
+    delta Localization.mul; apply (r S).commMonoid.mul_assoc
+  mul_comm x y := show x.mul S y = y.mul S x by
+    delta Localization.mul; apply (r S).commMonoid.mul_comm
+  mul_one x := show x.mul S (.one S) = x by
+    delta Localization.mul Localization.one; apply (r S).commMonoid.mul_one
+  one_mul x := show (Localization.one S).mul S x = x by
+    delta Localization.mul Localization.one; apply (r S).commMonoid.one_mul
   npow := Localization.npow S
-  npow_zero :=
-    show ∀ x : Localization S, Localization.npow S 0 x = 1 from (r S).commMonoid.npow_zero
-  npow_succ :=
-    show ∀ (n : ℕ) (x : Localization S), Localization.npow S n.succ x = x * Localization.npow S n x
-      from (r S).commMonoid.npow_succ
+  npow_zero x := show Localization.npow S 0 x = .one S by
+    delta Localization.npow Localization.one; apply (r S).commMonoid.npow_zero
+  npow_succ n x := show .npow S n.succ x = x.mul S (.npow S n x) by
+    delta Localization.npow Localization.mul; apply (r S).commMonoid.npow_succ
 
 variable {S}
 
@@ -309,17 +307,20 @@ def rec {p : Localization S → Sort u} (f : ∀ (a : M) (b : S), p (mk a b))
 #align add_localization.rec addLocalization.rec
 
 @[to_additive]
-theorem mk_mul (a c : M) (b d : S) : mk a b * mk c d = mk (a * c) (b * d) := rfl
+theorem mk_mul (a c : M) (b d : S) : mk a b * mk c d = mk (a * c) (b * d) :=
+  show Localization.mul S _ _ = _ by rw [Localization.mul]; rfl
 #align localization.mk_mul Localization.mk_mul
 #align add_localization.mk_add addLocalization.mk_add
 
 @[to_additive]
-theorem mk_one : mk 1 (1 : S) = 1 := rfl
+theorem mk_one : mk 1 (1 : S) = 1 :=
+  show mk _ _ = .one S by rw [Localization.one]; rfl
 #align localization.mk_one Localization.mk_one
 #align add_localization.mk_zero addLocalization.mk_zero
 
 @[to_additive]
-theorem mk_pow (n : ℕ) (a : M) (b : S) : mk a b ^ n = mk (a ^ n) (b ^ n) := rfl
+theorem mk_pow (n : ℕ) (a : M) (b : S) : mk a b ^ n = mk (a ^ n) (b ^ n) :=
+  show Localization.npow S _ _ = _ by rw [Localization.npow]; rfl
 #align localization.mk_pow Localization.mk_pow
 #align add_localization.mk_nsmul addLocalization.mk_nsmul
 
@@ -424,9 +425,7 @@ section Scalar
 variable {R R₁ R₂ : Type _}
 
 /-- Scalar multiplication in a monoid localization is defined as `c • ⟨a, b⟩ = ⟨c • a, b⟩`. -/
--- Porting note: replaced irreducible_def by @[irreducible] to prevent an error with protected
-@[irreducible]
-protected def smul [SMul R M] [IsScalarTower R M M] (c : R) (z : Localization S) :
+protected irreducible_def smul [SMul R M] [IsScalarTower R M M] (c : R) (z : Localization S) :
   Localization S :=
     Localization.liftOn z (fun a b ↦ mk (c • a) b)
       (fun {a a' b b'} h ↦ mk_eq_mk_iff.2 (by
@@ -447,7 +446,7 @@ instance [SMul R M] [IsScalarTower R M M] : SMul R (Localization S) where smul :
 
 theorem smul_mk [SMul R M] [IsScalarTower R M M] (c : R) (a b) :
     c • (mk a b : Localization S) = mk (c • a) b := by
- delta HSMul.hSMul instHSMul SMul.smul instSMulLocalization Localization.smul
+ simp only [HSMul.hSMul, instHSMul, SMul.smul, instSMulLocalization, Localization.smul]
  show liftOn (mk a b) (fun a b => mk (c • a) b) _ = _
  exact liftOn_mk (fun a b => mk (c • a) b) _ a b
 #align localization.smul_mk Localization.smul_mk
@@ -1811,37 +1810,27 @@ end Submonoid
 
 namespace Localization
 
--- Porting note: removed local since attribute 'semireducible' must be global
-attribute [semireducible] Localization
-
 /-- The zero element in a Localization is defined as `(0, 1)`.
 
 Should not be confused with `AddLocalization.zero` which is `(0, 0)`. -/
--- Porting note: replaced irreducible_def by @[irreducible] to prevent an error with protected
-@[irreducible]
-protected def zero : Localization S :=
+protected irreducible_def zero : Localization S :=
   mk 0 1
 #align localization.zero Localization.zero
 
 instance : Zero (Localization S) := ⟨Localization.zero S⟩
 
--- Porting note: removed local since attribute 'semireducible' must be global
-attribute [semireducible] Localization.zero Localization.mul
-
-instance : CommMonoidWithZero (Localization S) :=
-{ zero_mul := fun x ↦ Localization.induction_on x <| by
-      intro
-      refine mk_eq_mk_iff.mpr (r_of_eq (by simp [zero_mul, mul_zero]))
-  mul_zero := fun x ↦ Localization.induction_on x <| by
-      intro
-      refine mk_eq_mk_iff.mpr (r_of_eq (by simp [zero_mul, mul_zero])) }
-
 variable {S}
 
 theorem mk_zero (x : S) : mk 0 (x : S) = 0 :=
   calc
     mk 0 x = mk 0 1 := mk_eq_mk_iff.mpr (r_of_eq (by simp))
-    _ = 0 := rfl
+    _ = Localization.zero S := (Localization.zero_def S).symm
+
+instance : CommMonoidWithZero (Localization S) where
+  zero_mul := fun x ↦ Localization.induction_on x fun y => by
+    simp only [← Localization.mk_zero y.2, mk_mul, mk_eq_mk_iff, mul_zero, zero_mul, r_of_eq]
+  mul_zero := fun x ↦ Localization.induction_on x fun y => by
+    simp only [← Localization.mk_zero y.2, mk_mul, mk_eq_mk_iff, mul_zero, zero_mul, r_of_eq]
 
 #align localization.mk_zero Localization.mk_zero
 

Mathlib/RingTheory/Localization/Basic.lean

@@ -852,14 +852,10 @@ open IsLocalization
 
 section
 
-instance [Subsingleton R] : Unique (Localization M) :=
-  ⟨⟨1⟩, by
-    intro a; refine Localization.induction_on a ?_; intro a;
-    refine Localization.induction_on default ?_
-    intro b;
-    congr
-    exact Subsingleton.elim _ _
-    exact Subsingleton.elim _ _⟩
+instance [Subsingleton R] : Unique (Localization M) where
+  uniq a := show a = mk 1 1 from
+    Localization.induction_on a fun _ => by
+      congr <;> apply Subsingleton.elim
 
 /-- Addition in a ring localization is defined as `⟨a, b⟩ + ⟨c, d⟩ = ⟨b * c + d * a, b * d⟩`.
 

Mathlib/RingTheory/Localization/FractionRing.lean

@@ -113,11 +113,8 @@ protected theorem isDomain : IsDomain K :=
   isDomain_of_le_nonZeroDivisors _ (le_refl (nonZeroDivisors A))
 #align is_fraction_ring.is_domain IsFractionRing.isDomain
 
-attribute [local instance] Classical.decEq
-
 /-- The inverse of an element in the field of fractions of an integral domain. -/
--- Porting note: Had to replace `irreducible_def` with the `@[irreducible]` attribute.
-@[irreducible] protected noncomputable def inv (z : K) : K :=
+protected noncomputable irreducible_def inv (z : K) : K := open Classical in
   if h : z = 0 then 0
   else
     mk' K ↑(sec (nonZeroDivisors A) z).2

Mathlib/Tactic/Eqns.lean

@@ -37,7 +37,7 @@ initialize eqnsAttribute : NameMapExtension (Array Name) ←
     descr := "Overrides the equation lemmas for a declation to the provided list"
     add   :=  fun
     | _, `(attr| eqns $[$names]*) =>
-      pure <| names.map (fun n => n.getId)
+      names.mapM resolveGlobalConstNoOverload
     | _, _ => Lean.Elab.throwUnsupportedSyntax }
 
 initialize Lean.Meta.registerGetEqnsFn (fun name => do

Mathlib/Tactic/IrreducibleDef.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
 import Lean
+import Mathlib.Tactic.Eqns
 
 /-!
 # Irreducible definitions
@@ -71,24 +72,37 @@ Introduces an irreducible definition.
 a constant `foo : Nat` as well as
 a theorem `foo_def : foo = 42`.
 -/
-macro mods:declModifiers "irreducible_def" n_id:declId declSig:optDeclSig val:declVal :
+elab mods:declModifiers "irreducible_def" n_id:declId declSig:optDeclSig val:declVal :
     command => do
   let (n, us) ← match n_id with
     | `(Parser.Command.declId| $n:ident $[.{$us,*}]?) => pure (n, us)
-    | _ => Macro.throwUnsupported
+    | _ => throwUnsupportedSyntax
   let us' := us.getD { elemsAndSeps := #[] }
   let n_def := mkIdent <| (·.review) <|
     let scopes := extractMacroScopes n.getId
     { scopes with name := scopes.name.appendAfter "_def" }
-  `(stop_at_first_error
-    def definition$[.{$us,*}]? $declSig:optDeclSig $val
+  let `(Parser.Command.declModifiersF|
+      $[$doc:docComment]? $[$attrs:attributes]?
+      $[$vis]? $[$nc:noncomputable]? $[$uns:unsafe]?) := mods
+    | throwError "unsupported modifiers {format mods}"
+  let prot := vis.filter (· matches `(Parser.Command.visibility| protected))
+  let priv := vis.filter (· matches `(Parser.Command.visibility| private))
+  elabCommand <|<- `(stop_at_first_error
+    $[$nc:noncomputable]? $[$uns]? def definition$[.{$us,*}]? $declSig:optDeclSig $val
     set_option genInjectivity false in -- generates awful simp lemmas
-    structure Wrapper$[.{$us,*}]? where
+    $[$uns:unsafe]? structure Wrapper$[.{$us,*}]? where
       value : type_of% @definition.{$us',*}
       prop : Eq @value @(delta% @definition)
-    opaque wrapped$[.{$us,*}]? : Wrapper.{$us',*} := ⟨_, rfl⟩
-    $mods:declModifiers def $n:ident$[.{$us,*}]? := value_proj @wrapped.{$us',*}
-    theorem $n_def:ident $[.{$us,*}]? : eta_helper Eq @$n.{$us',*} @(delta% @definition) := by
+    $[$nc:noncomputable]? $[$uns]? opaque wrapped$[.{$us,*}]? : Wrapper.{$us',*} := ⟨_, rfl⟩
+    $[$doc:docComment]? $[$attrs:attributes]? $[private%$priv]? $[$nc:noncomputable]? $[$uns]?
+    def $n:ident$[.{$us,*}]? :=
+      value_proj @wrapped.{$us',*}
+    $[private%$priv]? $[$uns:unsafe]? theorem $n_def:ident $[.{$us,*}]? :
+        eta_helper Eq @$n.{$us',*} @(delta% @definition) := by
       intros
       simp only [$n:ident]
-      rw [wrapped.prop])
+      rw [wrapped.prop]
+    attribute [irreducible] $n
+    attribute [eqns $n_def] $n)
+  if prot.isSome then
+    modifyEnv (addProtected · ((← getCurrNamespace) ++ n.getId))

test/irreducibleDef.lean

@@ -5,7 +5,10 @@ irreducible_def frobnicate (a b : Nat) :=
   a + b
 
 example : frobnicate a 0 = a := by
-  simp [frobnicate_def]
+  simp [frobnicate]
+
+example : frobnicate a 0 = a :=
+  frobnicate_def a 0
 
 irreducible_def justAsArbitrary [Inhabited α] : α :=
   default
@@ -17,4 +20,18 @@ irreducible_def withEquations : Nat → Nat
   | _n+1 => 314
 
 irreducible_def withUniv.{u, v} := (Type v, Type u)
-example : withUniv.{u, v} = (Type v, Type u) := by rw [withUniv_def]
+example : withUniv.{u, v} = (Type v, Type u) := by rw [withUniv]
+
+namespace Foo
+protected irreducible_def foo : Nat := 42
+end Foo
+
+example : Foo.foo = 42 := by rw [Foo.foo]
+
+protected irreducible_def Bar.bar : Nat := 42
+
+protected noncomputable irreducible_def Nat.evenMoreArbitrary : Nat :=
+  Classical.choice inferInstance
+
+private irreducible_def Real.zero := 42
+example : Real.zero = 42 := Real.zero_def