Adapt eqns

nomeata · nomeata · commit 34f1f7fe93bf · 2025-06-04T12:46:40.000+02:00
diff --git a/Mathlib/Tactic/Eqns.lean b/Mathlib/Tactic/Eqns.lean
@@ -1,49 +0,0 @@
-/-
-Copyright (c) 2023 Eric Wieser. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Eric Wieser
--/
-import Mathlib.Init
-import Lean.Meta.Eqns
-import Batteries.Lean.NameMapAttribute
-import Lean.Elab.Exception
-import Lean.Elab.InfoTree.Main
-
-/-! # The `@[eqns]` attribute
-
-This file provides the `eqns` attribute as a way of overriding the default equation lemmas. For
-example
-
-```lean4
-def transpose {m n} (A : m → n → ℕ) : n → m → ℕ
-  | i, j => A j i
-
-theorem transpose_apply {m n} (A : m → n → ℕ) (i j) :
-    transpose A i j = A j i := rfl
-
-attribute [eqns transpose_apply] transpose
-
-theorem transpose_const {m n} (c : ℕ) :
-    transpose (fun (i : m) (j : n) => c) = fun j i => c := by
-  funext i j -- the rw below does not work without this line
-  rw [transpose]
-```
--/
-open Lean Elab
-
-syntax (name := eqns) "eqns" (ppSpace ident)* : attr
-
-initialize eqnsAttribute : NameMapExtension (Array Name) ←
-  registerNameMapAttribute {
-    name  := `eqns
-    descr := "Overrides the equation lemmas for a declaration to the provided list"
-    add   := fun
-    | declName, `(attr| eqns $[$names]*) => do
-      if let some _ := Meta.eqnsExt.getState (← getEnv) |>.map.find? declName then
-        throwError "There already exist stored eqns for '{declName}'; registering new equations \
-          will not have the desired effect."
-      names.mapM realizeGlobalConstNoOverloadWithInfo
-    | _, _ => Lean.Elab.throwUnsupportedSyntax }
-
-initialize Lean.Meta.registerGetEqnsFn (fun name => do
-  pure (eqnsAttribute.find? (← getEnv) name))
diff --git a/Mathlib/Tactic/IrreducibleDef.lean b/Mathlib/Tactic/IrreducibleDef.lean
@@ -61,6 +61,23 @@ open Command in elab_rules : command
 
 syntax irredDefLemma := atomic(" (" &"lemma" " := ") ident ")"
 
+/-- Like `theorem`, but allows defining reserved names. -/
+local elab "reserved_theorem_alias" declIdent:ident suffix:str " := " srcIdent:ident : command => do
+  let declName ← resolveGlobalConstNoOverload declIdent
+  let src ← resolveGlobalConstNoOverload srcIdent
+  let info ← getConstVal src
+  let tgt := .str declName suffix.getString
+  liftTermElabM do
+    realizeConst declName tgt do
+      addDecl <| Declaration.thmDecl {
+        name := tgt,
+        type := info.type,
+        value := .const src (info.levelParams.map mkLevelParam),
+        levelParams := info.levelParams
+      }
+  pure ()
+
+
 /--
 Introduces an irreducible definition.
 `irreducible_def foo := 42` generates
@@ -100,8 +117,9 @@ elab mods:declModifiers "irreducible_def" n_id:declId n_def:(irredDefLemma)?
       delta $n:ident
       rw [show wrapped = ⟨@definition.{$us',*}, rfl⟩ from Subtype.ext wrapped.2.symm]
       rfl
+    reserved_theorem_alias $n "eq_def" := $n_def:ident
+    reserved_theorem_alias $n "eq_1" := $n_def:ident
     attribute [irreducible] $n definition
-    attribute [eqns $n_def] $n
     attribute [$attrs:attrInstance,*] $n)
   if prot.isSome then
     modifyEnv (addProtected · ((← getCurrNamespace) ++ n.getId))
diff --git a/Mathlib/Tactic/ToAdditive/Frontend.lean b/Mathlib/Tactic/ToAdditive/Frontend.lean
@@ -18,7 +18,6 @@ import Lean.Meta.AbstractNestedProofs
 import Batteries.Lean.NameMapAttribute
 import Batteries.Tactic.Lint -- useful to lint this file and for DiscrTree.elements
 import Batteries.Tactic.Trans
-import Mathlib.Tactic.Eqns -- just to copy the attribute
 import Mathlib.Tactic.Simps.Basic
 
 /-!
@@ -1287,16 +1286,11 @@ partial def applyAttributes (stx : Syntax) (rawAttrs : Array Syntax) (thisAttr s
 Copies equation lemmas and attributes from `src` to `tgt`
 -/
 partial def copyMetaData (cfg : Config) (src tgt : Name) : CoreM (Array Name) := do
-  if let some eqns := eqnsAttribute.find? (← getEnv) src then
-    unless (eqnsAttribute.find? (← getEnv) tgt).isSome do
-      for eqn in eqns do _ ← addToAdditiveAttr eqn cfg
-      eqnsAttribute.add tgt (eqns.map (findTranslation? (← getEnv) · |>.get!))
-  else
-    /- We need to generate all equation lemmas for `src` and `tgt`, even for non-recursive
-    definitions. If we don't do that, the equation lemma for `src` might be generated later
-    when doing a `rw`, but it won't be generated for `tgt`. -/
-    additivizeLemmas #[src, tgt] "equation lemmas" fun nm ↦
-      (·.getD #[]) <$> MetaM.run' (getEqnsFor? nm)
+  /- We need to generate all equation lemmas for `src` and `tgt`, even for non-recursive
+  definitions. If we don't do that, the equation lemma for `src` might be generated later
+  when doing a `rw`, but it won't be generated for `tgt`. -/
+  additivizeLemmas #[src, tgt] "equation lemmas" fun nm ↦
+    (·.getD #[]) <$> MetaM.run' (getEqnsFor? nm)
   MetaM.run' <| Elab.Term.TermElabM.run' <|
     applyAttributes cfg.ref cfg.attrs `to_additive src tgt
 
diff --git a/MathlibTest/eqns.lean b/MathlibTest/eqns.lean
@@ -1,36 +0,0 @@
-import Mathlib.Tactic.Eqns
-def transpose {m n} (A : m → n → Nat) : n → m → Nat
-  | i, j => A j i
-
-theorem transpose_apply {m n} (A : m → n → Nat) (i j) : transpose A i j = A j i := rfl
-
-attribute [eqns transpose_apply] transpose
-
-theorem transpose_const {m n} (c : Nat) :
-    transpose (fun (_i : m) (_j : n) => c) = fun _j _i => c := by
-  fail_if_success {rw [transpose]}
-  fail_if_success {simp [transpose]}
-  funext i j -- the rw below does not work without this line
-  rw [transpose]
-
-def t : Nat := 0 + 1
-
-theorem t_def : t = 1 := rfl
--- this rw causes lean to generate equations itself for t before the user can register them
-theorem t_def' : t = 1 := by rw [t]
-
--- We used to test that this generated an error,
--- but with asynchronous elaboration, it now longer does!
--- `eqns` still seems to work (via `irreducible_def`) as expected,
--- so for now we just comment out the test...
--- #guard_msgs(error) in
--- attribute [eqns t_def] t
-
-/--
-warning: declaration uses 'sorry'
--/
-#guard_msgs in
--- the above should error as the above equation would not have changed the output of the below
-example (n : Nat) : t = n := by
-  rw [t]
-  admit
