From 0c711c23143baa71fc0f75cfd89fc51703cdb78b Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Tue, 11 Apr 2023 18:38:49 +0000
Subject: [PATCH] feat: `@[eqns]` attribute to override equation lemmas (#3024)

This is to help with #2960 and work around https://github.com/leanprover/lean4/issues/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 <scott.morrison@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
---
 Mathlib.lean             |  1 +
 Mathlib/Tactic/Eqns.lean | 44 ++++++++++++++++++++++++++++++++++++++++
 test/eqns.lean           | 17 ++++++++++++++++
 3 files changed, 62 insertions(+)
 create mode 100644 Mathlib/Tactic/Eqns.lean
 create mode 100644 test/eqns.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 99e4c705b8a7a..4470ec84abc30 100644
--- a/Mathlib.lean
+++ b/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
diff --git a/Mathlib/Tactic/Eqns.lean b/Mathlib/Tactic/Eqns.lean
new file mode 100644
index 0000000000000..ec62940a600d7
--- /dev/null
+++ b/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))
diff --git a/test/eqns.lean b/test/eqns.lean
new file mode 100644
index 0000000000000..d59bb8c1bdf1f
--- /dev/null
+++ b/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]