feat: revert e for arbitrary terms

This PR adds a feature to `revert` where `revert e` is like `have := e; revert this` when `e` is not a local variable. This is sometimes useful for putting a goal into a particular form for other tactics.

Author: kmill

src/Init/Tactics.lean

@@ -130,6 +130,11 @@ syntax (name := rename) "rename " term " => " ident : tactic
 /--
 `revert x...` is the inverse of `intro x...`: it moves the given hypotheses
 into the main goal's target type.
+If the hypothesis has dependencies, those are reverted too.
+
+The terms do not need to be identifiers;
+for example, `revert ‹x = y›` reverts a local hypothesis with the type `x = y`.
+If `e` is not a local hypothesis, then `revert e` is like `have := e; revert this`.
 -/
 syntax (name := revert) "revert" (ppSpace colGt term:max)+ : tactic
 

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -328,10 +328,25 @@ where
 
 @[builtin_tactic Lean.Parser.Tactic.revert] def evalRevert : Tactic := fun stx =>
   match stx with
-  | `(tactic| revert $hs*) => do
-     let (_, mvarId) ← (← getMainGoal).revert (← getFVarIds hs)
-     replaceMainGoal [mvarId]
-  | _                     => throwUnsupportedSyntax
+  | `(tactic| revert $hs*) => withMainContext do
+    let mut fvarIds := #[]
+    let mut toAssertRev := []
+    let mut newGoalsRev := []
+    for h in hs do
+      let (e, gs) ← withCollectingNewGoalsFrom (parentTag := ← getMainTag) (tagSuffix := `revert) do
+        withoutRecover <| elabTermForApply h (mayPostpone := false)
+      newGoalsRev := gs.reverse ++ newGoalsRev
+      if let .fvar fvarId := e then
+        fvarIds := fvarIds.push fvarId
+      else
+        toAssertRev := e :: toAssertRev
+    let mut mvarId ← popMainGoal
+    for e in toAssertRev do
+      mvarId ← mvarId.assert (← Term.mkFreshBinderName) (← inferType e) e
+    mvarId ← Prod.snd <$> mvarId.revert fvarIds
+    pushGoals newGoalsRev.reverse
+    pushGoal mvarId
+  | _ => throwUnsupportedSyntax
 
 @[builtin_tactic Lean.Parser.Tactic.clear] def evalClear : Tactic := fun stx =>
   match stx with

tests/lean/run/revert1.lean

@@ -1,23 +1,132 @@
+/-!
+# Tests of the `revert` tactic
+-/
 
-
-theorem tst1 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-by {
+/-!
+Simple revert/intro test
+-/
+/--
+trace: x y z : Nat
+h1 : y = z
+h3 : x = y
+⊢ x = x → x = z
+-/
+#guard_msgs in
+theorem tst1 (x y z : Nat) : y = z → x = x → x = y → x = z := by {
   intros h1 h2 h3;
   revert h2;
+  trace_state;
   intro h2;
   exact Eq.trans h3 h1
 }
 
+/-!
+Revert reverts dependencies too.
+-/
+/--
+trace: x z : Nat
+h2 : x = x
+⊢ ∀ (y : Nat), y = z → x = y → x = z
+-/
+#guard_msgs in
 theorem tst2 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
   intros h1 h2 h3;
   revert y;
+  trace_state;
   intros y hb ha;
   exact Eq.trans ha hb
 }
 
+/-!
+Can revert a more complex term that evaluates to a hypothesis.
+-/
+/--
+trace: x y z : Nat
+a✝¹ : y = z
+a✝ : x = x
+⊢ x = y → x = z
+-/
+#guard_msgs in
 theorem tst3 (x y z : Nat) : y = z → x = x → x = y → x = z := by
   intros
   revert ‹x = y›
+  trace_state
+  intro ha
+  exact Eq.trans ha ‹y = z›
+
+/-!
+Can revert a more complex term that doesn't evaluate to a hypothesis.
+This time, `a✝` itself isn't reverted.
+-/
+/--
+trace: x y z : Nat
+a✝² : y = z
+a✝¹ : x = x
+a✝ : x = y
+⊢ x = y → x = z
+-/
+#guard_msgs in
+theorem tst4 (x y z : Nat) : y = z → x = x → x = y → x = z := by
+  intros
+  revert (id ‹x = y›)
+  trace_state
   intro ha
   exact Eq.trans ha ‹y = z›
+
+/-!
+Can revert other expressions.
+-/
+/--
+trace: x y : Nat
+h : x = y
+⊢ x ≤ y → x ≤ y
+-/
+#guard_msgs in
+theorem tst5 (x y : Nat) : x = y → x ≤ y := by
+  intro h
+  revert (Nat.le_of_eq h)
+  trace_state
+  exact id
+
+/-!
+New metavariables become new goals after the main one.
+-/
+/--
+trace: x y : Nat
+h : x = y
+⊢ x ≤ y → x ≤ y
+
+case c
+x y : Nat
+h : x = y
+⊢ x ≤ y
+-/
+#guard_msgs in
+theorem test6 (x y : Nat) : x = y → x ≤ y := by
+  intro h
+  revert (?c : x ≤ y)
+  trace_state
+  case c => exact Nat.le_of_eq h
+  exact id
+
+/-!
+Unsolved natural metavariables are not allowed.
+-/
+/--
+error: don't know how to synthesize placeholder
+context:
+x y : Nat
+h : x = y
+⊢ x ≤ y
+---
+error: unsolved goals
+x y : Nat
+h : x = y
+⊢ x ≤ y
+-/
+#guard_msgs in
+theorem test7 (x y : Nat) : x = y → x ≤ y := by
+  intro h
+  revert (_ : x ≤ y)
+  fail "doesn't get here"