feat: subst tactic can substitute let values (#8450)

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

@@ -160,9 +160,16 @@ but adds the `hx : x = v` hypothesis first. Having a `with` binding associated t
 syntax (name := clearValue) "clear_value" (ppSpace colGt (clearValueStar <|> term:max))+ (" with" (ppSpace colGt binderIdent)+)? : 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.
+`subst x...` substitutes each hypothesis `x` with a definition found in the local context,
+then eliminates the hypothesis.
+- If `x` is a local definition, then its definition is used.
+- Otherwise, if there is a hypothesis of the form `x = e` or `e = x`,
+  then `e` is used for the definition of `x`.
+
+If `h : a = b`, then `subst h` may be used if either `a` or `b` unfolds to a local hypothesis.
+This is similar to the `cases h` tactic.
+
+See also: `subst_vars` for substituting all local hypotheses that have a defining equation.
 -/
 syntax (name := subst) "subst" (ppSpace colGt term:max)+ : tactic
 

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -403,7 +403,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/run/substlet.lean

@@ -0,0 +1,112 @@
+/-!
+# Tests of the `subst` tactic when `let`s are present.
+-/
+
+/-!
+Eliminates `a` even though `e : id a = m`.
+-/
+/--
+trace: case intro
+n : Nat
+m : Nat := n
+a : Nat
+e : id a = m
+⊢ 0 + n = n
+---
+trace: case intro
+a : Nat
+m : Nat := id a
+⊢ 0 + id a = id a
+-/
+#guard_msgs in
+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 =>
+    trace_state
+    subst e
+    trace_state
+    apply Nat.zero_add
+
+/-!
+Eliminates `a` even though `e : m = id a`.
+-/
+/--
+trace: case intro
+n : Nat
+m : Nat := n
+a : Nat
+e : m = id a
+⊢ 0 + n = n
+---
+trace: case intro
+n : Nat
+m : Nat := n
+⊢ 0 + n = n
+-/
+#guard_msgs in
+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 =>
+    trace_state
+    subst e
+    trace_state
+    apply Nat.zero_add
+
+/-!
+Since `v` is a let binding, the `subst v` tactic instead
+zeta delta reduces it everywhere and then clears it.
+-/
+/--
+trace: n : Nat
+h : n = 0
+m : Nat := n + 1
+v : Nat := m + 1
+this : v = n + 2
+⊢ 0 + n = 0
+---
+trace: n : Nat
+h : n = 0
+m : Nat := n + 1
+this : m + 1 = n + 2
+⊢ 0 + n = 0
+---
+trace: m : Nat := 0 + 1
+this : m + 1 = 0 + 2
+⊢ 0 + 0 = 0
+-/
+#guard_msgs in
+theorem ex3 (n : Nat) (h : n = 0) : 0 + n = 0 := by
+  let m := n + 1
+  let v := m + 1
+  have : v = n + 2 := rfl
+  trace_state
+  subst v
+  trace_state
+  subst n
+  trace_state
+  rfl
+
+/-!
+Can't do `subst this` with `this : v = n + 2` since `v` is a let binding.
+The tactic sees `m + 1 = n + 2` and fails.
+-/
+/--
+error: tactic 'subst' failed, invalid equality proof, it is not of the form (x = t) or (t = x)
+  v = n + 2
+n : Nat
+h : n = 0
+m : Nat := n + 1
+v : Nat := m + 1
+this : v = n + 2
+⊢ 0 + n = 0
+-/
+#guard_msgs in
+theorem ex4 (n : Nat) (h : n = 0) : 0 + n = 0 := by
+  let m := n + 1
+  let v := m + 1
+  have : v = n + 2 := rfl
+  subst this