From 2eb330e36a491bb3210d01563ebf2385636e6d9b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 29 Aug 2020 20:19:33 -0700
Subject: [PATCH] feat: improve `clear` tactic

---
 src/Lean/Elab/Tactic/Basic.lean | 41 +++++++++++++++++++++++----------
 tests/lean/run/tactic1.lean     | 13 +++++++++++
 2 files changed, 42 insertions(+), 12 deletions(-)
 create mode 100644 tests/lean/run/tactic1.lean

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 525397e853..faf4a37fb6 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -321,32 +321,49 @@ match fvar? with
 | some fvar => pure fvar.fvarId!
 | none      => throwError ("unknown variable '" ++ toString id.getId ++ "'")
 
-def getFVarIds (ids : Array Syntax) : TacticM (Array FVarId) :=
-ids.mapM getFVarId
+def getFVarIds (ids : Array Syntax) : TacticM (Array FVarId) := do
+withMainMVarContext $ ids.mapM getFVarId
 
 @[builtinTactic Lean.Parser.Tactic.revert] def evalRevert : Tactic :=
 fun stx => match_syntax stx with
   | `(tactic| revert $hs*) => do
      (g, gs) ← getMainGoal;
-     withMVarContext g $ do
-       fvarIds ← getFVarIds hs;
-       (_, g) ← liftMetaM $ Meta.revert g fvarIds;
-       setGoals (g :: gs)
+     fvarIds ← getFVarIds hs;
+     (_, g) ← liftMetaM $ Meta.revert g fvarIds;
+     setGoals (g :: gs)
   | _                     => throwUnsupportedSyntax
 
+/- Sort free variables using an order `x < y` iff `x` was defined after `y` -/
+private def sortFVarIds (fvarIds : Array FVarId) : TacticM (Array FVarId) :=
+withMainMVarContext do
+  lctx ← getLCtx;
+  pure $ fvarIds.qsort fun fvarId₁ fvarId₂ =>
+    match lctx.find? fvarId₁, lctx.find? fvarId₂ with
+    | some d₁, some d₂ => d₁.index > d₂.index
+    | some _,  none    => false
+    | none,    some _  => true
+    | none,    none    => Name.quickLt fvarId₁ fvarId₂
+
+@[builtinTactic Lean.Parser.Tactic.clear] def evalClear : Tactic :=
+fun stx => match_syntax stx with
+  | `(tactic| clear $hs*) => do
+    fvarIds ← getFVarIds hs;
+    fvarIds ← sortFVarIds fvarIds;
+    fvarIds.forM fun fvarId => do
+      (g, gs) ← getMainGoal;
+      withMVarContext g do
+        g ← liftMetaM $ clear g fvarId;
+        setGoals (g :: gs)
+  | _ => throwUnsupportedSyntax
+
 def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) : TacticM Unit :=
 hs.forM $ fun h => do
   (g, gs) ← getMainGoal;
-  withMVarContext g $ do
+  withMVarContext g do
     fvarId ← getFVarId h;
     g ← liftMetaM $ tac g fvarId;
     setGoals (g :: gs)
 
-@[builtinTactic Lean.Parser.Tactic.clear] def evalClear : Tactic :=
-fun stx => match_syntax stx with
-  | `(tactic| clear $hs*) => forEachVar hs Meta.clear
-  | _                     => throwUnsupportedSyntax
-
 @[builtinTactic Lean.Parser.Tactic.subst] def evalSubst : Tactic :=
 fun stx => match_syntax stx with
   | `(tactic| subst $hs*) => forEachVar hs Meta.subst
diff --git a/tests/lean/run/tactic1.lean b/tests/lean/run/tactic1.lean
new file mode 100644
index 0000000000..5088f93f5d
--- /dev/null
+++ b/tests/lean/run/tactic1.lean
@@ -0,0 +1,13 @@
+new_frontend
+
+theorem ex1 (x : Nat) (y : { v // v > x }) (z : Nat) : Nat :=
+begin
+  clear y x;
+  exact z
+end
+
+theorem ex2 (x : Nat) (y : { v // v > x }) (z : Nat) : Nat :=
+begin
+  clear x y;
+  exact z
+end