From 0c8a6d89776dcf82d4c11b7f79eef7dc3c88eaea Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 Apr 2022 15:31:54 -0700
Subject: [PATCH] feat: `exists es:term,+` tactic

cc: @fgdorais
---
 RELEASES.md                        |  2 ++
 src/Init/Notation.lean             |  7 +++++--
 src/Lean/Elab/Tactic/ElabTerm.lean |  5 -----
 tests/lean/run/1017.lean           |  2 +-
 tests/lean/run/exists.lean         | 11 +++++++++++
 tests/lean/run/matchGenBug.lean    |  3 +--
 6 files changed, 20 insertions(+), 10 deletions(-)
 create mode 100644 tests/lean/run/exists.lean

diff --git a/RELEASES.md b/RELEASES.md
index c069d59e7b..499725a79a 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -1,6 +1,8 @@
 Unreleased
 ---------
 
+* `exists` tactic is now takes a comma separated list of terms.
+
 * Add `dsimp` and `dsimp!` tactics. They guarantee the result term is definitionally equal, and only apply
   `rfl`-theorems.
 
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index c0c400b60d..5fb6ba1986 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -550,8 +550,6 @@ and one goal with hypothesis `h : P (Nat.succ a)` and target `Q (Nat.succ a)`. H
 -/
 syntax (name := cases) "cases " casesTarget,+ (" using " ident)? (inductionAlts)? : tactic
 
-syntax (name := existsIntro) "exists " term : tactic
-
 /-- `rename_i x_1 ... x_n` renames the last `n` inaccessible names using the given names. -/
 syntax (name := renameI) "rename_i " (colGt (ident <|> "_"))+ : tactic
 
@@ -595,6 +593,7 @@ syntax (name := specialize) "specialize " term : tactic
 macro_rules | `(tactic| trivial) => `(tactic| assumption)
 macro_rules | `(tactic| trivial) => `(tactic| rfl)
 macro_rules | `(tactic| trivial) => `(tactic| contradiction)
+macro_rules | `(tactic| trivial) => `(tactic| decide)
 macro_rules | `(tactic| trivial) => `(tactic| apply True.intro)
 macro_rules | `(tactic| trivial) => `(tactic| apply And.intro <;> trivial)
 
@@ -610,6 +609,10 @@ macro (name := save) "save" : tactic => `(skip)
 /-- The tactic `sleep ms` sleeps for `ms` milliseconds and does nothing. It is used for debugging purposes only. -/
 syntax (name := sleep) "sleep" num : tactic
 
+/-- `exists e₁, e₂, ...` is shorthand for `refine ⟨e₁, e₂, ...⟩; try trivial`. It is useful for existential goals. -/
+macro "exists " es:term,+ : tactic =>
+  `(tactic| (refine ⟨$es,*, ?_⟩; try trivial))
+
 end Tactic
 
 namespace Attr
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index 33fc75bdfb..213554d2f4 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -206,11 +206,6 @@ def getFVarIds (ids : Array Syntax) : TacticM (Array FVarId) := do
     Term.synthesizeSyntheticMVarsNoPostponing
     replaceMainGoal mvarIds'
 
-@[builtinTactic Lean.Parser.Tactic.existsIntro] def evalExistsIntro : Tactic := fun stx =>
-  match stx with
-  | `(tactic| exists $e) => evalApplyLikeTactic (fun mvarId e => return [(← Meta.existsIntro mvarId e)]) e
-  | _ => throwUnsupportedSyntax
-
 @[builtinTactic Lean.Parser.Tactic.withReducible] def evalWithReducible : Tactic := fun stx =>
   withReducible <| evalTactic stx[1]
 
diff --git a/tests/lean/run/1017.lean b/tests/lean/run/1017.lean
index 137b956559..544234472d 100644
--- a/tests/lean/run/1017.lean
+++ b/tests/lean/run/1017.lean
@@ -48,7 +48,7 @@ def mwe [Stream ρ τ] (acc : α) : {l : ρ // isFinite l} → α
     match h:next? l with
     | none => acc
     | some (x,xs) =>
-      have h_next : hasNext l xs := by exists x; simp [hasNext, h]
+      have h_next : hasNext l xs := by exists x
       mwe acc ⟨xs, by sorry⟩
   termination_by _ l => l
 
diff --git a/tests/lean/run/exists.lean b/tests/lean/run/exists.lean
new file mode 100644
index 0000000000..43a544e93f
--- /dev/null
+++ b/tests/lean/run/exists.lean
@@ -0,0 +1,11 @@
+example : ∃ x : Nat, x = x := by
+  exists 0
+
+example : ∃ x : Nat, ∃ y : Nat, x > y := by
+  exists 1, 0
+
+example : (x : Nat) ×' (y : Nat) ×' x > y := by
+  exists 1, 0
+
+example : { x : Nat // x > 2 } := by
+  exists 3
diff --git a/tests/lean/run/matchGenBug.lean b/tests/lean/run/matchGenBug.lean
index 5ad7b174c6..9cb3522499 100644
--- a/tests/lean/run/matchGenBug.lean
+++ b/tests/lean/run/matchGenBug.lean
@@ -16,5 +16,4 @@ theorem mem_split {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a
     | tail b bs h =>
       match bs, ih h with
       | _, ⟨s, t, rfl⟩ =>
-        exists b::s; exists t
-        rw [List.cons_append]
+        exists b::s, t