From e6aee1e463524b18bb61d5a95de28ee4a8ecb654 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 18 Apr 2022 11:45:36 -0700
Subject: [PATCH] feat: make sure `cases` and `induction` alternatives are
 processed using the order provided by the user

Motivation: improve the effectiveness of the `save` and `checkpoint` tactics.
---
 src/Lean/Elab/Tactic/Induction.lean          | 34 ++++++++++++++++++++
 tests/lean/690.lean.expected.out             |  6 ++--
 tests/lean/inductionErrors.lean.expected.out | 12 +++----
 tests/lean/run/casesUsing.lean               |  2 +-
 tests/playground/sleep_save.lean             | 22 +++++++++++++
 5 files changed, 66 insertions(+), 10 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index ef307bcf86..0c00fe1e4e 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -202,6 +202,39 @@ private def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Ar
           Term.addLocalVarInfo altVars[i] (mkFVar fvarId)
           i := i + 1
 
+/--
+  If `altsSyntax` is not empty we reorder `alts` using the order the alternatives have been provided
+  in `altsSyntax`. Motivations:
+
+  1- It improves the effectiveness of the `checkpoint` and `save` tactics. Consider the following example:
+  ```lean
+  example (h₁ : p ∨ q) (h₂ : p → x = 0) (h₃ : q → y = 0) : x * y = 0 := by
+    cases h₁ with
+    | inr h =>
+      sleep 5000 -- sleeps for 5 seconds
+      save
+      have : y = 0 := h₃ h
+      -- We can confortably work here
+    | inl h => stop ...
+  ```
+  If we do reorder, the `inl` alternative will be executed first. Moreover, as we type in the `inr` alternative,
+  type errors will "swallow" the `inl` alternative and affect the tactic state at `save` making it ineffective.
+
+  2- The errors are produced in the same order the appear in the code above. This is not super important when using IDEs.
+-/
+def reorderAlts (alts : Array (Name × MVarId)) (altsSyntax : Array Syntax) : Array (Name × MVarId) := Id.run do
+  if altsSyntax.isEmpty then
+    return alts
+  else
+    let mut alts := alts
+    let mut result := #[]
+    for altStx in altsSyntax do
+      let altName := getAltName altStx
+      let some i := alts.findIdx? (·.1 == altName) | return result ++ alts
+      result := result.push alts[i]
+      alts := alts.eraseIdx i
+    return result ++ alts
+
 def evalAlts (elimInfo : ElimInfo) (alts : Array (Name × MVarId)) (optPreTac : Syntax) (altsSyntax : Array Syntax)
     (initialInfo : Info)
     (numEqs : Nat := 0) (numGeneralized : Nat := 0) (toClear : Array FVarId := #[]) : TacticM Unit := do
@@ -213,6 +246,7 @@ def evalAlts (elimInfo : ElimInfo) (alts : Array (Name × MVarId)) (optPreTac :
   else go
 where
   go := do
+    let alts := reorderAlts alts altsSyntax
     let hasAlts := altsSyntax.size > 0
     let mut usedWildcard := false
     let mut subgoals := #[] -- when alternatives are not provided, we accumulate subgoals here
diff --git a/tests/lean/690.lean.expected.out b/tests/lean/690.lean.expected.out
index cb770487bf..00198aded3 100644
--- a/tests/lean/690.lean.expected.out
+++ b/tests/lean/690.lean.expected.out
@@ -1,15 +1,15 @@
-690.lean:4:12-4:17: warning: declaration uses 'sorry'
 690.lean:3:2-3:29: error: too many variable names provided at alternative 'step', #3 provided, but #2 expected
 690.lean:3:24-3:29: warning: declaration uses 'sorry'
-690.lean:9:12-9:17: warning: declaration uses 'sorry'
+690.lean:4:12-4:17: warning: declaration uses 'sorry'
 690.lean:8:34-8:39: warning: declaration uses 'sorry'
+690.lean:9:12-9:17: warning: declaration uses 'sorry'
 case step
 a b m✝ : Nat
 hStep : Nat.le a m✝
 ih : Nat.le a (m✝ + 1)
 ⊢ Nat.le a (Nat.succ m✝ + 1)
-690.lean:14:12-14:17: warning: declaration uses 'sorry'
 690.lean:13:37-13:42: warning: declaration uses 'sorry'
+690.lean:14:12-14:17: warning: declaration uses 'sorry'
 case step
 a b x : Nat
 hStep : Nat.le a x
diff --git a/tests/lean/inductionErrors.lean.expected.out b/tests/lean/inductionErrors.lean.expected.out
index 0a63efbc38..7be2279d9a 100644
--- a/tests/lean/inductionErrors.lean.expected.out
+++ b/tests/lean/inductionErrors.lean.expected.out
@@ -1,11 +1,11 @@
-inductionErrors.lean:12:12-12:27: error: unsolved goals
-case upper.h
-q d : Nat
-⊢ q + Nat.succ d > q
 inductionErrors.lean:11:12-11:27: error: unsolved goals
 case lower.h
 p d : Nat
 ⊢ p ≤ p + Nat.succ d
+inductionErrors.lean:12:12-12:27: error: unsolved goals
+case upper.h
+q d : Nat
+⊢ q + Nat.succ d > q
 inductionErrors.lean:16:19-16:26: error: unknown constant 'elimEx2'
 inductionErrors.lean:22:2-25:45: error: insufficient number of targets for 'elimEx'
 inductionErrors.lean:28:16-28:23: error: unexpected eliminator resulting type
@@ -27,9 +27,9 @@ inductionErrors.lean:50:2-50:16: error: alternative 'cons' is not needed
 inductionErrors.lean:55:2-55:16: error: alternative 'cons' is not needed
 inductionErrors.lean:60:2-60:40: error: invalid alternative name 'upper2'
 inductionErrors.lean:66:2-66:28: error: invalid occurrence of wildcard alternative, it must be the last alternative
-inductionErrors.lean:72:29-72:34: warning: declaration uses 'sorry'
 inductionErrors.lean:71:29-71:34: warning: declaration uses 'sorry'
+inductionErrors.lean:72:29-72:34: warning: declaration uses 'sorry'
 inductionErrors.lean:74:2-74:34: error: unused alternative
-inductionErrors.lean:79:29-79:34: warning: declaration uses 'sorry'
 inductionErrors.lean:78:29-78:34: warning: declaration uses 'sorry'
+inductionErrors.lean:79:29-79:34: warning: declaration uses 'sorry'
 inductionErrors.lean:80:2-80:53: error: unused alternative
diff --git a/tests/lean/run/casesUsing.lean b/tests/lean/run/casesUsing.lean
index 0dbe9edda3..b5f070709d 100644
--- a/tests/lean/run/casesUsing.lean
+++ b/tests/lean/run/casesUsing.lean
@@ -139,8 +139,8 @@ theorem ex15 (p q : Nat) : p ≤ q ∨ p > q := by
   | lower d => _
   | upper d => ?hupper
   { apply Or.inl; apply Nat.le_refl }
-  { apply Or.inr; show q + d.succ > q; admit }
   { apply Or.inl; show p ≤ p + d.succ; admit }
+  { apply Or.inr; show q + d.succ > q; admit }
 
 theorem ex16 {p q : Prop} (h : p ∨ q) : q ∨ p := by
   induction h
diff --git a/tests/playground/sleep_save.lean b/tests/playground/sleep_save.lean
index 598dfd4498..d432f1db9f 100644
--- a/tests/playground/sleep_save.lean
+++ b/tests/playground/sleep_save.lean
@@ -8,3 +8,25 @@ example (h₁ : x = y) (h₂ : y = z) : z = x := by
   trace "hello world"
   apply this.trans
   exact ‹y = x›
+
+example (h₁ : p ∨ q) (h₂ : p → x = 0) (h₃ : q → y = 0) : x * y = 0 := by
+  expensive_tactic
+  save
+  match h₁ with
+  | .inr h =>
+    expensive_tactic
+    save
+    have : y = 0 := h₃ h
+    simp [*]
+  | .inl h => stop done
+
+example (h₁ : p ∨ q) (h₂ : p → x = 0) (h₃ : q → y = 0) : x * y = 0 := by
+  expensive_tactic
+  save
+  cases h₁ with
+  | inr h =>
+    expensive_tactic
+    save
+    have : y = 0 := h₃ h
+    simp [*]
+  | inl h => stop done