From e2c8b1694bc8d9abf8dff3016a8fd0993132d47e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 31 Dec 2020 10:54:55 -0800
Subject: [PATCH] feat: improve `subst`

---
 src/Lean/Meta/Tactic/Subst.lean       | 27 ++++++++++++++++++++-------
 tests/lean/substlet.lean              | 26 ++++++++++++++++++++++++++
 tests/lean/substlet.lean.expected.out | 27 +++++++++++++++++++++++++++
 3 files changed, 73 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/substlet.lean
 create mode 100644 tests/lean/substlet.lean.expected.out

diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean
index 13062a56a0..4c0a907afc 100644
--- a/src/Lean/Meta/Tactic/Subst.lean
+++ b/src/Lean/Meta/Tactic/Subst.lean
@@ -7,6 +7,7 @@ import Lean.Meta.AppBuilder
 import Lean.Meta.MatchUtil
 import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.Revert
+import Lean.Meta.Tactic.Assert
 import Lean.Meta.Tactic.Intro
 import Lean.Meta.Tactic.Clear
 import Lean.Meta.Tactic.FVarSubst
@@ -25,7 +26,6 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
     | some (α, lhs, rhs) => do
       let a := if symm then rhs else lhs
       let b := if symm then lhs else rhs
-      let a ← whnf a
       match a with
       | Expr.fvar aFVarId _ => do
         let aFVarIdOriginal := aFVarId
@@ -125,16 +125,29 @@ def subst (mvarId : MVarId) (hFVarId : FVarId) : MetaM MVarId :=
     let hLocalDecl ← getLocalDecl hFVarId
     match (← matchEq? hLocalDecl.type) with
     | some (α, lhs, rhs) =>
-      let rhs ← whnf rhs
-      if rhs.isFVar then
-        return (← substCore mvarId hFVarId true).2
+      let substReduced (newType : Expr) (symm : Bool) : MetaM MVarId := do
+        let mvarId ← assert mvarId hLocalDecl.userName newType (mkFVar hFVarId)
+        let (hFVarId', mvarId) ← intro1P mvarId
+        let mvarId ← clear mvarId hFVarId
+        return (← substCore mvarId hFVarId' symm).2
+      let rhs' ← whnf rhs
+      if rhs'.isFVar then
+        if rhs != rhs' then
+          substReduced (← mkEq lhs rhs') true
+        else
+          return (← substCore mvarId hFVarId true).2
       else do
-        let lhs ← whnf lhs
-        if lhs.isFVar then
-          return (← substCore mvarId hFVarId).2
+        let lhs' ← whnf lhs
+        if lhs'.isFVar then
+          if lhs != lhs' then
+            substReduced (← mkEq lhs' rhs) false
+          else
+            return (← substCore mvarId hFVarId).2
         else do
           throwTacticEx `subst mvarId m!"invalid equality proof, it is not of the form (x = t) or (t = x){indentExpr hLocalDecl.type}"
     | none =>
+      if hLocalDecl.isLet then
+        throwTacticEx `subst mvarId m!"variable '{mkFVar hFVarId}' is a let-declaration"
       let mctx ← getMCtx
       let lctx ← getLCtx
       let some (fvarId, symm) ← lctx.findDeclM? fun localDecl => do
diff --git a/tests/lean/substlet.lean b/tests/lean/substlet.lean
new file mode 100644
index 0000000000..d1caa28b3c
--- /dev/null
+++ b/tests/lean/substlet.lean
@@ -0,0 +1,26 @@
+theorem ex1 (n : Nat) : 0 + n = n := by
+  let m := n
+  have h : ∃ k, id k = m := ⟨m, rfl⟩
+  cases h with
+  | intro a e =>
+    traceState
+    subst e
+    traceState
+    apply Nat.zeroAdd
+
+theorem ex2 (n : Nat) : 0 + n = n := by
+  let m := n
+  have h : ∃ k, m = id k := ⟨m, rfl⟩
+  cases h with
+  | intro a e =>
+    traceState
+    subst e
+    traceState
+    apply Nat.zeroAdd
+
+theorem ex3 (n : Nat) (h : n = 0) : 0 + n = 0 := by
+  let m := n + 1
+  let v := m + 1
+  have v = n + 2 from rfl
+  subst v -- error
+  done
diff --git a/tests/lean/substlet.lean.expected.out b/tests/lean/substlet.lean.expected.out
new file mode 100644
index 0000000000..9c278cdafb
--- /dev/null
+++ b/tests/lean/substlet.lean.expected.out
@@ -0,0 +1,27 @@
+case intro
+n : Nat
+m : Nat := n
+a : Nat
+e : id a = m
+⊢ 0 + n = n
+case intro
+a : Nat
+m : Nat := id a
+⊢ 0 + id a = id a
+case intro
+n : Nat
+m : Nat := n
+a : Nat
+e : m = id a
+⊢ 0 + n = n
+case intro
+n : Nat
+m : Nat := n
+⊢ 0 + n = n
+substlet.lean:25:2: error: tactic 'subst' failed, variable 'v' is a let-declaration
+n : Nat
+h : n = 0
+m : Nat := n + 1
+v : Nat := m + 1
+this : v = n + 2
+⊢ 0 + n = 0