From 4eb2cfec466bfebfdca7633fce24e6b0f5cba68c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 May 2022 07:25:45 -0700
Subject: [PATCH] feat: make sure `case' ... => tac` does not use `done` after
 `tac`

---
 src/Init/Notation.lean                  |  5 ++--
 src/Lean/Elab/Tactic/BuiltinTactic.lean | 39 +++++++++++++------------
 tests/lean/run/casePrime.lean           | 15 ++++++++++
 3 files changed, 38 insertions(+), 21 deletions(-)
 create mode 100644 tests/lean/run/casePrime.lean

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 76914797fb..0a12e12884 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -315,8 +315,9 @@ syntax (name := constructor) "constructor" : tactic
 `case tag x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with inaccessible names to the given names. -/
 syntax (name := case) "case " (ident <|> "_") (ident <|> "_")* " => " tacticSeq : tactic
 /--
-Similar to the `case tag => tac` tactic but for writing macros. Recall that `case` closes the goal using `sorry` when it fails,
-and the tactic execution is not interrupted.
+Similar to the `case tag => tac` tactic, but `cases'` does not ensures the goal has been solved after applying `tac`, nor
+admits the goal if `tac` failed. Recall that `case` closes the goal using `sorry` when `tac` fails, and
+the tactic execution is not interrupted.
 -/
 syntax (name := case') "case' " (ident <|> "_") (ident <|> "_")* " => " tacticSeq : tactic
 
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index abf1516fe0..4f2521bec5 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -303,8 +303,7 @@ def renameInaccessibles (mvarId : MVarId) (hs : Array Syntax) : TacticM MVarId :
     assignExprMVar mvarId mvarNew
     return mvarNew.mvarId!
 
-private def evalCaseCore (stx : Syntax) (tag : Syntax) (hs : Array Syntax) (arr : Syntax) (tac : Syntax)
-    (closeOnFailure : Bool) : TacticM Unit := do
+private def getCaseGoals (tag : Syntax) : TacticM (MVarId × List MVarId) := do
   let gs ← getUnsolvedGoals
   let g ←
     if tag.isIdent then
@@ -313,28 +312,30 @@ private def evalCaseCore (stx : Syntax) (tag : Syntax) (hs : Array Syntax) (arr
       pure g
     else
       getMainGoal
-  let gs := gs.erase g
-  let g ← renameInaccessibles g hs
-  setGoals [g]
-  let savedTag ← getMVarTag g
-  setMVarTag g Name.anonymous
-  try
-    if closeOnFailure then
-      withCaseRef arr tac do
-        closeUsingOrAdmit (withTacticInfoContext stx (evalTactic tac))
-    else
-      evalTactic tac
-  finally
-    setMVarTag g savedTag
-  done
-  setGoals gs
+  return (g, gs.erase g)
 
 @[builtinTactic «case»] def evalCase : Tactic
-  | stx@`(tactic| case $tag $hs* =>%$arr $tac:tacticSeq) => evalCaseCore stx tag hs arr tac (closeOnFailure := true)
+  | stx@`(tactic| case $tag $hs* =>%$arr $tac:tacticSeq) => do
+    let (g, gs) ← getCaseGoals tag
+    let g ← renameInaccessibles g hs
+    setGoals [g]
+    setMVarTag g Name.anonymous
+    withCaseRef arr tac do
+      closeUsingOrAdmit (withTacticInfoContext stx (evalTactic tac))
+    setGoals gs
   | _ => throwUnsupportedSyntax
 
 @[builtinTactic «case'»] def evalCase' : Tactic
-  | stx@`(tactic| case' $tag $hs* =>%$arr $tac:tacticSeq) => evalCaseCore stx tag hs arr tac (closeOnFailure := false)
+  | stx@`(tactic| case' $tag $hs* =>%$arr $tac:tacticSeq) => do
+    let (g, gs) ← getCaseGoals tag
+    let g ← renameInaccessibles g hs
+    let mvarTag ← getMVarTag g
+    setGoals [g]
+    withCaseRef arr tac (evalTactic tac)
+    let gs' ← getUnsolvedGoals
+    if let [g'] := gs' then
+      setMVarTag g' mvarTag
+    setGoals (gs' ++ gs)
   | _ => throwUnsupportedSyntax
 
 @[builtinTactic «renameI»] def evalRenameInaccessibles : Tactic
diff --git a/tests/lean/run/casePrime.lean b/tests/lean/run/casePrime.lean
new file mode 100644
index 0000000000..913b1fc7c1
--- /dev/null
+++ b/tests/lean/run/casePrime.lean
@@ -0,0 +1,15 @@
+example (hp : p) (hq : p → q) (hr : p → r) : (s ∨ q) ∧ (r ∨ s) := by
+  constructor
+  case' left  => apply Or.inr
+  case' right => apply Or.inl
+  case' left  => apply hq
+  case' right => apply hr
+  all_goals assumption
+
+example (hp : p) (hq : p → q) (hr : p → r) : (p ∧ q) ∧ (r ∧ p) := by
+  constructor
+  case' left  => constructor
+  case' right => constructor
+  case' right.left => apply hr
+  case' left.right => apply hq
+  all_goals assumption