feat: @[eqns] attribute to override equation lemmas (#3024)

This is to help with #2960 and work around leanprover/lean4#2042.

Ideally we would inspect the function to find that it was declared as `| i, j => A j i` and generate `transpose_apply`, but that's not something I know how to do.



Co-authored-by: Scott Morrison <[email protected]>
Co-authored-by: Jeremy Tan Jie Rui <[email protected]>

Mathlib.lean

@@ -1567,6 +1567,7 @@ import Mathlib.Tactic.Conv
 import Mathlib.Tactic.Convert
 import Mathlib.Tactic.Core
 import Mathlib.Tactic.Elementwise
+import Mathlib.Tactic.Eqns
 import Mathlib.Tactic.Existsi
 import Mathlib.Tactic.FailIfNoProgress
 import Mathlib.Tactic.FieldSimp

Mathlib/Tactic/Eqns.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2023 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import Lean.Meta.Eqns
+import Mathlib.Lean.Expr
+import Std.Lean.NameMapAttribute
+
+/-! # 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
+
+syntax (name := eqns) "eqns" ident* : attr
+
+initialize eqnsAttribute : NameMapExtension (Array Name) ←
+  registerNameMapAttribute {
+    name  := `eqns
+    descr := "Overrides the equation lemmas for a declation to the provided list"
+    add   :=  fun
+    | _, `(attr| eqns $[$names]*) =>
+      pure <| names.map (fun n => n.getId)
+    | _, _ => Lean.Elab.throwUnsupportedSyntax }
+
+initialize Lean.Meta.registerGetEqnsFn (fun name => do
+  pure (eqnsAttribute.find? (← getEnv) name))

test/eqns.lean

@@ -0,0 +1,17 @@
+import Mathlib.Tactic.Eqns
+
+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
+  fail_if_success {rw [transpose]}
+  fail_if_success {simp [transpose]}
+  funext i j -- the rw below does not work without this line
+  rw [transpose]