feat: add conversion-mode clear tactic

src/Init/Conv.lean

@@ -183,6 +183,9 @@ match [a, b] with
 simplifies to `a`. -/
 syntax (name := simpMatch) "simp_match" : conv
 
+/-- Removes one or more hypotheses from the local context. -/
+syntax (name := clear) "clear" (ppSpace colGt term:max)+ : conv
+
 /-- Executes the given tactic block without converting `conv` goal into a regular goal. -/
 syntax (name := nestedTacticCore) "tactic'" " => " tacticSeq : conv
 

src/Lean/Elab/Tactic/Conv/Basic.lean

@@ -98,6 +98,30 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
    withMainContext do
      changeLhs (← zetaReduce (← getLhs))
 
+/-- Removes the hypothesis referred to by `fvarId` from the context of the currently focused `conv`
+goal, provided that `fvarId` is not referenced by another hypothesis or the current `conv`-focused
+target. -/
+def convClear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := do
+  let (lhs, rhs) ← getLhsRhsCore mvarId
+  unless rhs.isMVar do
+    return (← mvarId.clear fvarId)
+  -- Clear from the RHS mvar's context so that it isn't detected as a dependent
+  let rhs' ← rhs.mvarId!.clear fvarId
+  let mvarId' ← mvarId.replaceTargetDefEq (mkLHSGoalRaw (← mkEq lhs (mkMVar rhs')))
+  let mvarIdCleared ← mvarId'.clear fvarId
+  return mvarIdCleared
+
+@[builtin_tactic Lean.Parser.Tactic.Conv.clear] def evalClear : Tactic := fun stx => do
+  match stx with
+  | `(conv| clear $hs*) => do
+    let fvarIds ← getFVarIds hs
+    let fvarIds ← withMainContext <| sortFVarIds fvarIds
+    for fvarId in fvarIds.reverse do
+      withMainContext do
+        let mvarId ← convClear (← getMainGoal) fvarId
+        replaceMainGoal [mvarId]
+  | _ => throwUnsupportedSyntax
+
 /-- Evaluate `sepByIndent conv "; " -/
 def evalSepByIndentConv (stx : Syntax) : TacticM Unit := do
   for arg in stx.getArgs, i in [:stx.getArgs.size] do

src/Lean/Meta/Tactic/Clear.lean

@@ -30,7 +30,7 @@ def _root_.Lean.MVarId.clear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId
     let localInsts := match localInsts.findFinIdx? fun localInst => localInst.fvar.fvarId! == fvarId with
       | none => localInsts
       | some idx => localInsts.eraseIdx idx
-    let newMVar ← mkFreshExprMVarAt lctx localInsts mvarDecl.type MetavarKind.syntheticOpaque tag
+    let newMVar ← mkFreshExprMVarAt lctx localInsts mvarDecl.type mvarDecl.kind tag
     mvarId.assign newMVar
     pure newMVar.mvarId!
 

tests/lean/run/convClear.lean

@@ -0,0 +1,151 @@
+/-!
+# `clear` in conversion mode
+
+Tests the functionality of the `clear` command in conversion mode (i.e., that it clears the
+specified hypotheses in the appropriate scope provided they have no dependents in the current
+proof state).
+-/
+
+/- Test basic `clear` functionality: that it correctly removes hypotheses, that removals persist
+   after focusing a subterm, and that removals do not propagate beyond the `conv` block -/
+/--
+info: α : Type
+x y z : α
+h₂ : y = z
+| x = y ∧ y = z
+---
+info: α : Type
+x y z : α
+| x = y
+---
+info: α : Type
+x y z : α
+h₁ : x = y
+h₂ : y = z
+⊢ x = y ∧ y = z
+-/
+#guard_msgs in
+example (α : Type) (x y z : α) (h₁ : x = y) (h₂ : y = z) : x = y ∧ y = z := by
+  conv =>
+    clear h₁
+    trace_state
+    lhs
+    clear h₂
+    trace_state
+  trace_state
+  exact And.intro h₁ h₂
+
+/- Ensure `clear` behaves correctly when nesting `conv` blocks -/
+/--
+info: α : Type
+w x y z : α
+h₁ : x = y
+h₂ : y = z
+| y = z
+---
+info: α : Type
+w x y z : α
+h₂ : y = z
+| y
+---
+info: α : Type
+w x y z : α
+h₁ : x = y
+h₂ : y = z
+| y = z
+---
+info: α : Type
+w x y z : α
+h₂ : y = z
+| y = z
+-/
+#guard_msgs in
+set_option linter.unusedVariables false in
+example (α : Type) (w x y z : α) (h₀ : z = w) (h₁ : x = y) (h₂ : y = z) : x = y ∧ y = z := by
+  conv =>
+    rhs
+    clear h₀
+    trace_state
+    conv =>
+      lhs
+      clear h₁
+      trace_state
+    trace_state
+    clear h₁
+    trace_state
+  exact And.intro h₁ h₂
+
+/- Ensure `clear` correctly handles multiple arguments, including by removing them in the correct
+   order -/
+/--
+info: α : Type
+y z : α
+h₂ : y = z
+| y = z
+---
+info: α : Type
+z : α
+| z
+-/
+#guard_msgs in
+example (α : Type) (x y z : α) (h₁ : x = y) (h₂ : y = z) : x = y ∧ y = z := by
+  conv =>
+    rhs
+    clear x h₁
+    trace_state
+    rhs
+    clear h₂ y
+    trace_state
+  exact And.intro h₁ h₂
+
+/- Ensure `clear` refuses to remove arguments on which the goal or existing hypotheses depend -/
+/--
+error: tactic 'clear' failed, variable 'h' depends on 'x'
+x : Nat
+h : x = 1
+⊢ Prop
+-/
+#guard_msgs in
+example (x : Nat) (h : x = 1) : True := by
+  conv =>
+    clear x
+
+/--
+error: tactic 'clear' failed, target depends on 'x'
+x : Nat
+| x = 2
+-/
+#guard_msgs in
+example (x : Nat) : x = 2 := by
+  conv =>
+    clear x
+
+/--
+error: tactic 'clear' failed, target depends on 'x'
+y x : Nat
+| x = 2
+-/
+#guard_msgs in
+example (y x : Nat) : x = 2 := by
+  conv =>
+    clear x y
+
+/- Ensure `clear` interacts correctly with/leaves goals in a usable state for other `conv` tactics -/
+/--
+info: y : Nat
+h₂ : y = 3
+| 2 + y
+---
+info: | 2 + 3
+-/
+#guard_msgs in
+example (x y : Nat) (h₁ : x = 2) (h₂ : y = 3) : 2 * (x + y) = 10 := by
+  conv =>
+    enter [1, 2]
+    rw [h₁]
+    clear h₁ x
+    trace_state
+    rw [h₂]
+    clear h₂ y
+    trace_state
+    simp only [Nat.reduceMul]