feat: exists es:term,+ tactic

cc: @fgdorais

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.
 

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

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]
 

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
 

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

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