feat: clear_value tactic

kmill · kmill · commit d98f25c174f5 · 2025-05-23T02:39:10.000-07:00
This PR upstreams and extends the Mathlib `clear_value` tactic. Given a local definition `x : T := v`, the tactic `clear_value x` replaces it with a hypothesis `x : T`, or throws an error if the goal does not depend on the value `v`. The syntax `clear_value x with h` creates a hypothesis `h : x = v` before clearing the value of `x`. Furthermore, `clear_value *` clears all values that can be cleared, or throws an error if none can be cleared.
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
@@ -139,6 +139,21 @@ references to a hypothesis.
 -/
 syntax (name := clear) "clear" (ppSpace colGt term:max)+ : tactic
 
+/--
+Syntax for trying to clear the values of all local definitions.
+-/
+syntax clearValueStar := "*"
+/--
+* `clear_value x...` clears the values of the given local definitions.
+For example, a local definition `x : α := v` becomes a hypothesis `x : α`.
+
+* `clear_value x with h` adds a hypothesis `h : x = v` before clearing the value of `x`.
+
+* `clear_value *` clears values of all hypotheses that can be cleared.
+  Fails if none can be cleared.
+-/
+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`.
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -344,6 +344,54 @@ where
         replaceMainGoal [mvarId]
   | _ => throwUnsupportedSyntax
 
+@[builtin_tactic Lean.Parser.Tactic.clearValue] def evalClearValue : Tactic := fun stx =>
+  match stx with
+  | `(tactic| clear_value $xs* $[with $hs*]?) => withMainContext do
+    let hs := hs.getD #[]
+    if xs.size < hs.size then throwErrorAt hs[xs.size]! "Too many binders provided."
+    -- The bool means "clearing must succeed"
+    let mut fvarIds : Array FVarId := #[]
+    let mut hasStar := false
+    for i in [0:xs.size], x in xs do
+      if x.raw.isOfKind ``clearValueStar then
+        if i < hs.size then
+          throwErrorAt hs[i]! "When using `*`, no binder may be provided for it."
+        hasStar := true
+      else
+        let fvarId ← getFVarId x
+        unless (← fvarId.isLetVar) do
+          throwErrorAt x "Hypothesis `{mkFVar fvarId}` is not a local definition."
+        if fvarIds.contains fvarId then
+          throwErrorAt x "Hypothesis `{mkFVar fvarId}` appears multiple times."
+        fvarIds := fvarIds.push fvarId
+    let mut g ← popMainGoal
+    unless hs.isEmpty do
+      let mut hyps : Array Hypothesis := #[]
+      for fvarId in fvarIds, h in hs do
+        let hName ←
+          match h with
+          | `(binderIdent| $n:ident) => pure n.raw.getId
+          | _ => mkFreshBinderNameForTactic `h
+        let type ← mkEq (mkFVar fvarId) (← fvarId.getValue?).get!
+        let value ← mkEqRefl (mkFVar fvarId)
+        hyps := hyps.push { userName := hName, type, value }
+      g ← Prod.snd <$> g.assertHypotheses hyps
+    let toClear ← g.withContext do
+      if hasStar then (·.map Expr.fvarId!) <$> getLocalHyps
+      else sortFVarIds fvarIds
+    let mut succeeded := false
+    for fvarId in toClear.reverse do
+      try
+        g ← g.clearValue fvarId
+        succeeded := true
+      catch _ =>
+        if fvarIds.contains fvarId then
+          g.withContext do throwError "Tactic `clear_value` could not clear value of `{Expr.fvar fvarId}`.\n{g}"
+    unless succeeded do
+      g.withContext do throwError "Tactic `clear_value` failed to clear any values.\n{g}"
+    pushGoal g
+  | _ => throwUnsupportedSyntax
+
 def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) : TacticM Unit := do
   for h in hs do
     withMainContext do
diff --git a/src/Lean/Meta/Tactic/Replace.lean b/src/Lean/Meta/Tactic/Replace.lean
@@ -216,4 +216,27 @@ def _root_.Lean.MVarId.modifyTargetEqLHS (mvarId : MVarId) (f : Expr → MetaM E
      else
        throwTacticEx `modifyTargetEqLHS mvarId m!"equality expected{indentExpr target}"
 
+
+/--
+Clears the value of the local definition `fvarId`. Ensures that the resulting goal state
+is still type correct. Throws an error if it is a local hypothesis without a value.
+-/
+def _root_.Lean.MVarId.clearValue (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := do
+  mvarId.checkNotAssigned `clear_value
+  let tag ← mvarId.getTag
+  let (_, mvarId) ← mvarId.withReverted #[fvarId] fun mvarId' fvars => mvarId'.withContext do
+    let tgt ← mvarId'.getType
+    unless tgt.isLet do
+      mvarId.withContext <|
+        throwTacticEx `clear_value mvarId m!"hypothesis `{Expr.fvar fvarId}` is not a local definition."
+    let tgt' := Expr.forallE tgt.letName! tgt.letType! tgt.letBody! .default
+    unless ← isTypeCorrect tgt' do
+      mvarId.withContext <|
+        throwTacticEx `clear_value mvarId
+          m!"cannot clear {Expr.fvar fvarId}, the resulting context is not type correct."
+    let mvarId'' ← mkFreshExprSyntheticOpaqueMVar tgt' tag
+    mvarId'.assign <| .app mvarId'' tgt.letValue!
+    return ((), fvars.map .some, mvarId''.mvarId!)
+  return mvarId
+
 end Lean.Meta
diff --git a/tests/lean/run/clear_value.lean b/tests/lean/run/clear_value.lean
@@ -0,0 +1,238 @@
+/-!
+# Tests for `clear_value` tactic
+-/
+
+/-!
+Check that `clear_value` clears the value.
+-/
+/--
+trace: x : Nat
+⊢ 0 ≤ x
+-/
+#guard_msgs in
+example : let x := 22; 0 ≤ x := by
+  intro x
+  clear_value x
+  trace_state
+  exact Nat.zero_le _
+
+/-!
+Test `*` mode.
+-/
+/--
+trace: x : Nat
+⊢ 0 ≤ x
+-/
+#guard_msgs in
+example : let x := 22; 0 ≤ x := by
+  intro x
+  clear_value *
+  trace_state
+  exact Nat.zero_le _
+
+/-!
+Check that `clear_value` fails if there is no value to clear.
+-/
+/-- error: Hypothesis `x` is not a local definition. -/
+#guard_msgs in
+example (x : Nat) : 0 ≤ x := by
+  clear_value x
+
+/-!
+Check that `clear_value *` fails if it does nothing.
+-/
+/--
+error: Tactic `clear_value` failed to clear any values.
+x : Nat
+⊢ 0 ≤ x
+-/
+#guard_msgs in
+example (x : Nat) : 0 ≤ x := by
+  clear_value *
+
+/-!
+Check for validation that hypotheses aren't mentioned multiple times.
+-/
+/-- error: Hypothesis `x` appears multiple times. -/
+#guard_msgs in
+example : let x := 22; 0 ≤ x := by
+  intro x
+  clear_value x x
+
+/-!
+Check that `clear_value ... with` creates an equality hypothesis.
+-/
+/--
+trace: x : Nat
+h : x = 22
+⊢ 0 ≤ 22
+-/
+#guard_msgs in
+example : let x := 22; 0 ≤ x := by
+  intro x
+  clear_value x with h
+  rw [h]
+  trace_state
+  exact Nat.zero_le _
+
+/-!
+Check `clear_value ... with` with `_`.
+-/
+/--
+trace: x : Nat
+h✝ : x = 22
+⊢ 0 ≤ 22
+-/
+#guard_msgs in
+example : let x := 22; 0 ≤ x := by
+  intro x
+  clear_value x with _
+  rw [‹x = 22›]
+  trace_state
+  exact Nat.zero_le _
+
+/-!
+Check `clear_value ... with` with too many `with` binders.
+-/
+/-- error: Too many binders provided. -/
+#guard_msgs in
+example : let x := 22; 0 ≤ x := by
+  intro x
+  clear_value x with h1 h2
+
+/-!
+Check that `clear_value` checks for type correctness.
+-/
+/--
+error: Tactic `clear_value` could not clear value of `x`.
+x : Nat := 22
+y : Fin x := 0
+⊢ ↑y < x
+-/
+#guard_msgs in
+example : let x := 22; let y : Fin x := 0; y.1 < x := by
+  intro x y
+  clear_value x
+
+/-!
+Even though we cannot clear `x` on its own, we can clear it if we clear `y` first.
+-/
+/--
+trace: x : Nat
+y : Fin x
+⊢ ↑y < x
+-/
+#guard_msgs in
+example : let x := 22; let y : Fin x := 0; y.1 < x := by
+  intro x y
+  clear_value y
+  clear_value x
+  trace_state
+  exact y.2
+
+/-!
+We can clear the values `x` and `y` in any order.
+-/
+/--
+trace: x : Nat
+y : Fin x
+⊢ ↑y < x
+-/
+#guard_msgs in
+example : let x := 22; let y : Fin x := 0; y.1 < x := by
+  intro x y
+  clear_value y x
+  trace_state
+  exact y.2
+/--
+trace: x : Nat
+y : Fin x
+⊢ ↑y < x
+-/
+#guard_msgs in
+example : let x := 22; let y : Fin x := 0; y.1 < x := by
+  intro x y
+  clear_value x y
+  trace_state
+  exact y.2
+
+/-!
+Clearing `x` on its own and `y` on its own are OK because `y + 1` is nonzero.
+-/
+/--
+trace: x y : Nat
+z : Fin (y + 1) := 0
+⊢ ↑z < y + 1
+-/
+#guard_msgs in
+example : let x := 22; let y : Nat := x; let z : Fin (y + 1) := 0; z.1 < y + 1 := by
+  intro x y z
+  clear_value x
+  clear_value y
+  trace_state
+  exact z.2
+
+/-!
+Dependence, `clear_value` fails.
+-/
+/--
+error: Tactic `clear_value` could not clear value of `α`.
+α : Type := Nat
+x : α := 1
+⊢ x = x
+-/
+#guard_msgs in
+example : let α := Nat; let x : α := 1; @Eq α x x := by
+  intro α x
+  clear_value α
+
+/-!
+`clear_value *` manages to clear `x` but not `α`
+-/
+/--
+trace: α : Type := Nat
+x : α
+⊢ x = 1
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example : let α := Nat; let x : α := 1; @Eq α x 1 := by
+  intro α x
+  clear_value *
+  trace_state
+  sorry
+
+/-!
+`clear_value *` fails if `x` is already cleared
+-/
+/--
+error: Tactic `clear_value` failed to clear any values.
+α : Type := Nat
+x : α
+⊢ x = 1
+-/
+#guard_msgs in
+example : let α := Nat; let x : α := 1; @Eq α x 1 := by
+  intro α x
+  clear_value x
+  clear_value *
+
+/-!
+Can use `with` clause with `*` so long as it's paired with a local.
+-/
+#guard_msgs in
+example : let α := Nat; let x : α := 1; @Eq α x 1 := by
+  intro α x
+  clear_value x * with h
+  exact h
+
+/-!
+Can't use `with` with `*` directly.
+-/
+/-- error: When using `*`, no binder may be provided for it. -/
+#guard_msgs in
+example : let α := Nat; let x : α := 1; @Eq α x 1 := by
+  intro α x
+  clear_value * with h
+  exact h
