feat: add exists tactic

src/Init/Notation.lean

@@ -176,6 +176,8 @@ syntax[«match»] "match " sepBy1(matchDiscr, ", ") (" : " term)? " with " match
 
 syntax[introMatch] "intro " matchAlts : tactic
 
+syntax[existsIntro] "exists " term : tactic
+
 macro "rfl" : tactic => `(exact rfl)
 macro "decide!" : tactic => `(exact decide!)
 macro "admit" : tactic => `(exact sorry)

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.CollectMVars
 import Lean.Meta.Tactic.Apply
+import Lean.Meta.Tactic.Constructor
 import Lean.Meta.Tactic.Assert
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.SyntheticMVars
@@ -74,18 +75,24 @@ def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : Ta
   | `(tactic| refine! $e) => refineCore e `refine (allowNaturalHoles := true)
   | _                     => throwUnsupportedSyntax
 
+def evalApplyLikeTactic (tac : MVarId → Expr → MetaM (List MVarId)) (e : Syntax) : TacticM Unit := do
+  let (g, gs) ← getMainGoal
+  let gs' ← withMVarContext g do
+    let decl ← getMVarDecl g
+    let val  ← elabTerm e none true
+    let gs'  ← tac g val
+    Term.synthesizeSyntheticMVarsNoPostponing
+    pure gs'
+  setGoals (gs' ++ gs)
+
 @[builtinTactic Lean.Parser.Tactic.apply] def evalApply : Tactic := fun stx =>
   match_syntax stx with
-  | `(tactic| apply $e) => do
-    let (g, gs) ← getMainGoal
-    let gs' ← withMVarContext g do
-      let decl ← getMVarDecl g
-      let val  ← elabTerm e none true
-      let gs'  ← Meta.apply g val
-      Term.synthesizeSyntheticMVarsNoPostponing
-      pure gs'
-    -- TODO: handle optParam and autoParam
-    setGoals (gs' ++ gs)
+  | `(tactic| apply $e) => evalApplyLikeTactic Meta.apply e
+  | _ => throwUnsupportedSyntax
+
+@[builtinTactic Lean.Parser.Tactic.existsIntro] def evalExistsIntro : Tactic := fun stx =>
+  match_syntax stx with
+  | `(tactic| exists $e) => evalApplyLikeTactic (fun mvarId e => return [(← Meta.existsIntro mvarId e)]) e
   | _ => throwUnsupportedSyntax
 
 /--

src/Lean/Meta/Tactic.lean

@@ -16,3 +16,4 @@ import Lean.Meta.Tactic.Induction
 import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.ElimInfo
 import Lean.Meta.Tactic.Delta
+import Lean.Meta.Tactic.Constructor

src/Lean/Meta/Tactic/Constructor.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Check
+import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Apply
+
+namespace Lean.Meta
+
+def existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId := do
+  withMVarContext mvarId do
+    checkNotAssigned mvarId `exists
+    let target ← getMVarType' mvarId
+    matchConstStruct target.getAppFn
+      (fun _ => throwTacticEx `exists mvarId "target is not an inductive datatype with one constructor")
+      fun ival us cval => do
+        if cval.nfields < 2 then
+          throwTacticEx `exists mvarId "constructor must have at least two fields"
+        let ctor := mkAppN (Lean.mkConst cval.name us) target.getAppArgs[:cval.nparams]
+        let ctorType ← inferType ctor
+        let (mvars, _, _) ← forallMetaTelescopeReducing ctorType (some (cval.nfields-2))
+        let f := mkAppN ctor mvars
+        checkApp f w
+        let [mvarId] ← apply mvarId <| mkApp f w
+          | throwTacticEx `exists mvarId "unexpected number of subgoals"
+        pure mvarId
+
+end Lean.Meta