From b52edf125967c879d09ddc3e49e844109ab1f8ec Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 10 May 2021 17:26:20 -0700
Subject: [PATCH] fix: fixes #452

The new syntax is similar to `matchAlts` and uses `colGe`.
The first `|` is not optional anymore.
---
 src/Init/Notation.lean          |  7 +++----
 src/Init/NotationExtra.lean     |  6 +++---
 src/Lean/Elab/Tactic/Basic.lean | 17 +----------------
 tests/lean/run/452.lean         | 14 ++++++++++++++
 tests/lean/run/allGoals.lean    |  2 +-
 tests/lean/run/elab_cmd.lean    |  2 +-
 6 files changed, 23 insertions(+), 25 deletions(-)
 create mode 100644 tests/lean/run/452.lean

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 9f1b49f9a9..a5152225d6 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -226,11 +226,10 @@ syntax (name := generalize) "generalize " atomic(ident " : ")? term:51 " = " ide
 syntax (name := paren) "(" tacticSeq ")" : tactic
 syntax (name := withReducible) "withReducible " tacticSeq : tactic
 syntax (name := withReducibleAndInstances) "withReducibleAndInstances " tacticSeq : tactic
-syntax (name := first) "first " "|"? sepBy1(tacticSeq, "|") : tactic
-syntax (name := firstNew) "firstNew " withPosition((group(colGe "|" tacticSeq))+) : tactic
+syntax (name := first) "first " withPosition((group(colGe "|" tacticSeq))+) : tactic
 syntax (name := rotateLeft) "rotateLeft" (num)? : tactic
 syntax (name := rotateRight) "rotateRight" (num)? : tactic
-macro "try " t:tacticSeq : tactic => `(first $t | skip)
+macro "try " t:tacticSeq : tactic => `(first | $t | skip)
 macro:1 x:tactic " <;> " y:tactic:0 : tactic => `(tactic| focus ($x:tactic; allGoals $y:tactic))
 
 macro "rfl" : tactic => `(exact rfl)
@@ -309,7 +308,7 @@ syntax (name := existsIntro) "exists " term : tactic
 
 syntax "repeat " tacticSeq : tactic
 macro_rules
-  | `(tactic| repeat $seq) => `(tactic| first ($seq); repeat $seq | skip)
+  | `(tactic| repeat $seq) => `(tactic| first | ($seq); repeat $seq | skip)
 
 syntax "trivial" : tactic
 
diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 773dcba8eb..a66aed27bd 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -177,9 +177,9 @@ macro_rules
         @ $ctor:ident $ctorArgs*)
 
 /-
-  Similar to `first`, but succeeds only if one the given tactics solves the curretn goal.
+  Similar to `first`, but succeeds only if one the given tactics solves the current goal.
 -/
-syntax "solve " "|"? sepBy1(tacticSeq, "|") : tactic
+syntax (name := solve) "solve " withPosition((group(colGe "|" tacticSeq))+) : tactic
 
 macro_rules
-  | `(tactic| solve $[|]? $ts:tacticSeq|*) => `(tactic| focus first $[($ts); done]|*)
+  | `(tactic| solve $[| $ts]* ) => `(tactic| focus first $[| ($ts); done]*)
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index d5bcbf4e91..dd417796e8 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -622,8 +622,7 @@ def withCaseRef [Monad m] [MonadRef m] (arrow body : Syntax) (x : m α) : m α :
     setGoals gs
   | _ => throwUnsupportedSyntax
 
--- syntax (name := firstNew) "firstNew " withPosition((colGe "|" tacticSeq)+) : tactic
-@[builtinTactic «firstNew»] partial def evalFirstNew : Tactic := fun stx => do
+@[builtinTactic «first»] partial def evalFirst : Tactic := fun stx => do
   let tacs := stx[1].getArgs
   if tacs.isEmpty then throwUnsupportedSyntax
   loop tacs 0
@@ -634,20 +633,6 @@ where
     else
       evalTactic tacs[i][1] <|> loop tacs (i+1)
 
-@[builtinTactic «first»] partial def evalFirst : Tactic := fun stx => do
-  if stx.getNumArgs == 2 then
-    evalFirstNew stx
-  else
-    let tacs := stx[2].getSepArgs
-    if tacs.isEmpty then throwUnsupportedSyntax
-    loop tacs 0
-where
-  loop (tacs : Array Syntax) (i : Nat) :=
-    if i == tacs.size - 1 then
-      evalTactic tacs[i]
-    else
-      evalTactic tacs[i] <|> loop tacs (i+1)
-
 builtin_initialize registerTraceClass `Elab.tactic
 
 end Lean.Elab.Tactic
diff --git a/tests/lean/run/452.lean b/tests/lean/run/452.lean
new file mode 100644
index 0000000000..157e7d0a0f
--- /dev/null
+++ b/tests/lean/run/452.lean
@@ -0,0 +1,14 @@
+example (h : x ∨ y) : y ∨ x := by
+  cases h with
+  | inl hx => first
+    | apply Or.inr; assumption
+    | apply Or.inl; assumption
+  | inr hy => exact Or.inl hy
+
+
+example (h : x ∨ y) : y ∨ x := by
+  cases h with
+  | inl hx => first
+    | apply Or.inl; assumption
+    | apply Or.inr; assumption
+  | inr hy => exact Or.inl hy
diff --git a/tests/lean/run/allGoals.lean b/tests/lean/run/allGoals.lean
index cb848e9615..7309ad62d8 100644
--- a/tests/lean/run/allGoals.lean
+++ b/tests/lean/run/allGoals.lean
@@ -42,7 +42,7 @@ open Lean.Parser.Tactic in
 macro "rwd " x:term : tactic => `(rw [$x:term]; done)
 
 theorem ex (a b c : α) (h₁ : a = b) (h₂ : a = c) : b = a ∧ c = a := by
-  apply And.intro <;> first rwd h₁ | rwd h₂
+  apply And.intro <;> first | rwd h₁ | rwd h₂
 
 theorem idEq (a : α) : id a = a :=
   rfl
diff --git a/tests/lean/run/elab_cmd.lean b/tests/lean/run/elab_cmd.lean
index c835a71537..7d598eb60d 100644
--- a/tests/lean/run/elab_cmd.lean
+++ b/tests/lean/run/elab_cmd.lean
@@ -20,7 +20,7 @@ elab "#check2" b:term : command => do
 #check2 10
 
 elab "try" t:tactic : tactic => do
-  let t' ← `(tactic| first $t | skip);
+  let t' ← `(tactic| first | $t | skip);
   Lean.Elab.Tactic.evalTactic t'
 
 theorem tst (x y z : Nat) : y = z → x = x → x = y → x = z :=