feat: subst tactic can substitute let values

This PR adds a feature to the `subst` tactic so that when `x : X := v` is a local definition, `subst x` substitutes `v` for `x` in the goal and removes `x`. Previously the tactic would throw an error.

Author: kmill

src/Init/Tactics.lean

@@ -143,6 +143,8 @@ syntax (name := clear) "clear" (ppSpace colGt term:max)+ : tactic
 `subst x...` substitutes each `x` with `e` in the goal if there is a hypothesis
 of type `x = e` or `e = x`.
 If `x` is itself a hypothesis of type `y = e` or `e = y`, `y` is substituted instead.
+
+If `x` is a local definition `x : α := e`, then `x` is substituted with `e`.
 -/
 syntax (name := subst) "subst" (ppSpace colGt term:max)+ : tactic
 

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -353,7 +353,20 @@ def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) :
 
 @[builtin_tactic Lean.Parser.Tactic.subst] def evalSubst : Tactic := fun stx =>
   match stx with
-  | `(tactic| subst $hs*) => forEachVar hs Meta.subst
+  | `(tactic| subst $hs*) => forEachVar hs fun mvarId fvarId => do
+    let decl ← fvarId.getDecl
+    if decl.isLet then
+      -- Zeta delta reduce the let and eliminate it.
+      let (_, mvarId) ← mvarId.withReverted #[fvarId] fun mvarId' fvars => mvarId'.withContext do
+        let tgt ← mvarId'.getType
+        assert! tgt.isLet
+        let mvarId'' ← mvarId'.replaceTargetDefEq (tgt.letBody!.instantiate1 tgt.letValue!)
+        -- Dropped the let fvar
+        let aliasing := (fvars.extract 1).map some
+        return ((), aliasing, mvarId'')
+      return mvarId
+    else
+      Meta.subst mvarId fvarId
   | _                     => throwUnsupportedSyntax
 
 @[builtin_tactic Lean.Parser.Tactic.substVars] def evalSubstVars : Tactic := fun _ =>

tests/lean/substlet.lean

@@ -22,5 +22,7 @@ theorem ex3 (n : Nat) (h : n = 0) : 0 + n = 0 := by
   let m := n + 1
   let v := m + 1
   have : v = n + 2 := rfl
-  subst v -- error
-  done
+  trace_state
+  subst v -- zeta delta reduces and clears
+  trace_state
+  simp [h]

tests/lean/substlet.lean.expected.out

@@ -18,10 +18,14 @@ case intro
 n : Nat
 m : Nat := n
 ⊢ 0 + n = n
-substlet.lean:25:2-25:9: 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
+n : Nat
+h : n = 0
+m : Nat := n + 1
+this : m + 1 = n + 2
+⊢ 0 + n = 0