feat(library/basic_thms): add ExistsIntro theorem

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/notation.cpp

@@ -119,5 +119,6 @@ void init_builtin_notation(frontend & f) {
     f.mark_implicit_arguments(mk_congr2_fn(), 4);
     f.mark_implicit_arguments(mk_congr_fn(),  6);
     f.mark_implicit_arguments(mk_forall_elim_fn(), 2);
+    f.mark_implicit_arguments(mk_exists_intro_fn(), 2);
 }
 }

src/library/basic_thms.cpp

@@ -39,6 +39,7 @@ MK_CONSTANT(congr_fn,           name("Congr"));
 MK_CONSTANT(eqt_elim_fn,        name("EqTElim"));
 MK_CONSTANT(eqt_intro_fn,       name("EqTIntro"));
 MK_CONSTANT(forall_elim_fn,     name("ForallElim"));
+MK_CONSTANT(exists_intro_fn,    name("ExistsIntro"));
 
 #if 0
 MK_CONSTANT(ext_fn,            name("ext"));
@@ -269,6 +270,13 @@ void import_basic_thms(environment const & env) {
                      Fun({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}},
                          EqTElim(P(a), Congr1(A, Fun({x, A}, Bool), P, Fun({x, A}, True), a, H))));
 
+    // ExistsIntro : Pi (A : Type u) (P : A -> bool) (a : A) (H : P a), exists A P
+    env->add_theorem(exists_intro_fn_name, Pi({{A, TypeU}, {P, A_pred}, {a, A}, {H, P(a)}}, mk_exists(A, P)),
+                     Fun({{A, TypeU}, {P, A_pred}, {a, A}, {H, P(a)}},
+                         Discharge(mk_forall(A, Fun({x, A}, Not(P(x)))), False,
+                                   Fun({H2, mk_forall(A, Fun({x, A}, Not(P(x))))},
+                                       Absurd(P(a), H, ForallElim(A, Fun({x, A}, Not(P(x))), H2, a))))));
+
 #if 0
     // STOPPED HERE
 

src/library/basic_thms.h

@@ -122,6 +122,10 @@ expr mk_forall_elim_fn();
 // \brief (Theorem) {A : Type u}, {P : A -> Bool}, H : (Forall A P), a : A |- Forallelim(A, P, H, a) : P a
 inline expr ForallElim(expr const & A, expr const & P, expr const & H, expr const & a) { return mk_app(mk_forall_elim_fn(), A, P, H, a); }
 
+expr mk_exists_intro_fn();
+// \brief (Theorem) {A : Type u}, {P : A -> Bool}, a : A,  H : P a |- ExistsIntro(A, P, a, H) : exists x : A, P
+inline expr ExistsIntro(expr const & A, expr const & P, expr const & a, expr const & H) { return mk_app(mk_exists_intro_fn(), A, P, a, H); }
+
 /** \brief Add basic theorems to Environment */
 void import_basic_thms(environment const & env);
 

tests/lean/exists1.lean

@@ -0,0 +1,5 @@
+Variable a : Int
+Variable P : Int -> Int -> Bool
+Axiom H : P a a
+Theorem T : exists x : Int, P a a := ExistsIntro a H.
+Show Environment 1.

tests/lean/exists1.lean.expected.out

@@ -0,0 +1,7 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: a
+  Assumed: P
+  Assumed: H
+  Proved: T
+Theorem T : ∃ x : ℤ, P a a := ExistsIntro a H