From cf0ca026fb2ae24723f325de1cceaaeaeccf3001 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 12 Mar 2022 13:53:02 -0800
Subject: [PATCH] feat: equation theorems at `rw`

---
 RELEASES.md                           | 10 ++++++++++
 src/Lean/Elab/Tactic/Rewrite.lean     | 14 +++++++++++++-
 tests/lean/rwEqThms.lean              | 16 ++++++++++++++++
 tests/lean/rwEqThms.lean.expected.out | 27 +++++++++++++++++++++++++++
 4 files changed, 66 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/rwEqThms.lean
 create mode 100644 tests/lean/rwEqThms.lean.expected.out

diff --git a/RELEASES.md b/RELEASES.md
index 1138186881..ba27391a5f 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -1,6 +1,16 @@
 v4.0.0-m4 (WIP)
 ---------
 
+* `rw` tactic can now apply auto-generated equation theorems for a given definition. Example:
+```lean
+example (a : Nat) (h : n = 1) : [a].length = n := by
+  rw [List.length]
+  trace_state -- .. |- [].length + 1 = n
+  rw [List.length]
+  trace_state -- .. |- 0 + 1 = n
+  rw [h]
+```
+
 * [Fuzzy matching for auto completion](https://github.com/leanprover/lean4/pull/1023)
 
 * Extend dot-notation `x.field` for arrow types. If type of `x` is an arrow, we look up for `Function.field`.
diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean
index 1cebe2d4e4..eb484bd244 100644
--- a/src/Lean/Elab/Tactic/Rewrite.lean
+++ b/src/Lean/Elab/Tactic/Rewrite.lean
@@ -43,7 +43,19 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool)
       withRef rule do
         let symm := !rule[0].isNone
         let term := rule[1]
-        x symm term
+        let processId (id : Syntax) : TacticM Unit := do
+          -- Try to get equation theorems for `id` first
+          let declName ← try resolveGlobalConstNoOverload id catch _ => return (← x symm term)
+          let some eqThms ← getEqnsFor? declName | x symm term
+          let rec go : List Name →  TacticM Unit
+            | [] => throwError "failed to rewrite using equation theorems for '{declName}'"
+            | eqThm::eqThms => (x symm (mkIdentFrom id eqThm)) <|> go eqThms
+          go eqThms.toList
+        match term with
+        | `($id:ident)  => processId id
+        | `(@$id:ident) => processId id
+        | _ => x symm term
+
 
 declare_config_elab elabRewriteConfig Rewrite.Config
 
diff --git a/tests/lean/rwEqThms.lean b/tests/lean/rwEqThms.lean
new file mode 100644
index 0000000000..218082ae0f
--- /dev/null
+++ b/tests/lean/rwEqThms.lean
@@ -0,0 +1,16 @@
+example {a : α} {as bs : List α} (h : bs = a::as) : as.length + 1 = bs.length := by
+  rw [← List.length]
+  trace_state -- lhs was folded
+  rw [h]
+
+example {a : α} {as bs : List α} (h : as = bs) : (a::b::as).length = bs.length + 2 := by
+  rw [List.length, List.length]
+  trace_state -- lhs was unfolded
+  rw [h]
+
+example {a : α} {as bs : List α} (h : as = bs) : (a::b::as).length = (b::bs).length + 1 := by
+  conv => lhs; rw [List.length, List.length]
+  trace_state -- lhs was unfolded
+  conv => rhs; rw [List.length]
+  trace_state -- rhs was unfolded
+  rw [h]
diff --git a/tests/lean/rwEqThms.lean.expected.out b/tests/lean/rwEqThms.lean.expected.out
new file mode 100644
index 0000000000..9511f6b048
--- /dev/null
+++ b/tests/lean/rwEqThms.lean.expected.out
@@ -0,0 +1,27 @@
+α : Type ?u
+a : α
+as bs : List α
+h : bs = a :: as
+⊢ List.length (?a_1 :: as) = List.length bs
+
+case a_1
+α : Type ?u
+a : α
+as bs : List α
+h : bs = a :: as
+⊢ α
+α : Type ?u
+b a : α
+as bs : List α
+h : as = bs
+⊢ List.length as + 1 + 1 = List.length bs + 2
+α : Type ?u
+b a : α
+as bs : List α
+h : as = bs
+⊢ List.length as + 1 + 1 = List.length (b :: bs) + 1
+α : Type ?u
+b a : α
+as bs : List α
+h : as = bs
+⊢ List.length as + 1 + 1 = List.length bs + 1 + 1