feat: equation theorems at rw

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`.

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
 

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]

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