feat(library/basic_thms): add ExistsElim theorem

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

src/frontends/lean/notation.cpp

@@ -121,6 +121,7 @@ void init_builtin_notation(frontend & f) {
     f.mark_implicit_arguments(mk_congr_fn(),  6);
     f.mark_implicit_arguments(mk_forall_elim_fn(), 2);
     f.mark_implicit_arguments(mk_forall_intro_fn(), 2);
+    f.mark_implicit_arguments(mk_exists_elim_fn(), 3);
     f.mark_implicit_arguments(mk_exists_intro_fn(), 2);
 }
 }

src/library/basic_thms.cpp

@@ -43,6 +43,7 @@ MK_CONSTANT(eqt_elim_fn,        name("EqTElim"));
 MK_CONSTANT(eqt_intro_fn,       name("EqTIntro"));
 MK_CONSTANT(forall_elim_fn,     name("ForallElim"));
 MK_CONSTANT(forall_intro_fn,    name("ForallIntro"));
+MK_CONSTANT(exists_elim_fn,     name("ExistsElim"));
 MK_CONSTANT(exists_intro_fn,    name("ExistsIntro"));
 
 #if 0
@@ -74,6 +75,7 @@ void import_basic_thms(environment const & env) {
     expr A1 = Const("A1");
     expr B1 = Const("B1");
     expr a1 = Const("a1");
+    expr R  = Const("R");
 
     expr A_pred    = A >> Bool;
     expr q_type    = Pi({A, TypeU}, A_pred >> Bool);
@@ -286,6 +288,14 @@ void import_basic_thms(environment const & env) {
                                Symm(A_pred, Fun({x, A}, P(x)), P, Eta(A, Fun({x, A}, Bool), P)), // P == fun x : A, P x
                                Abst(A, Fun({x, A}, Bool), Fun({x, A}, P(x)), Fun({x, A}, True), Fun({x, A}, EqTIntro(P(x), H(x)))))));
 
+    // ExistsElim : Pi (A : Type U) (P : A -> Bool) (B : Bool) (H1 : exists x : A, P x) (H2 : Pi (a : A) (H : P a), B) : B :=
+    env->add_theorem(exists_elim_fn_name, Pi({{A, TypeU}, {P, A_pred}, {B, Bool}, {H1, mk_exists(A, P)}, {H2, Pi({{a, A}, {H, P(a)}}, B)}}, B),
+                     Fun({{A, TypeU}, {P, A_pred}, {B, Bool}, {H1, mk_exists(A, P)}, {H2, Pi({{a, A}, {H, P(a)}}, B)}},
+                         Refute(B, Fun({R, Not(B)},
+                                       Absurd(mk_forall(A, Fun({x, A}, Not(P(x)))),
+                                              ForallIntro(A, Fun({x, A}, Not(P(x))), Fun({a, A}, MT(P(a), B, Discharge(P(a), B, Fun({H, P(a)}, H2(a, H))), R))),
+                                              H1)))));
+
     // 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)}},

src/library/basic_thms.h

@@ -130,21 +130,14 @@ expr mk_forall_intro_fn();
 // \brief (Theorem) {A : Type u} {P : A -> bool} (H : Pi (x : A), P x) |- ForallIntro(A, P, H) : forall x : A, P
 inline expr ForallIntro(expr const & A, expr const & P, expr const & H) { return mk_app(mk_forall_intro_fn(), A, P, H); }
 
+expr mk_exists_elim_fn();
+// \brief (Theorem) {A : Type U} {P : A -> Bool} {B : Bool} (H1 : exists x : A, P x) (H2 : Pi (a : A) (H : P a) |- ExistsElim(A, P, B, H1, H2) : B
+inline expr ExistsElim(expr const & A, expr const & P, expr const & B, expr const & H1, expr const & H2) { return mk_app({mk_exists_elim_fn(), A, P, B, H1, H2}); }
+
 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);
-
-#if 0
-expr mk_ext_fn();
-bool is_ext_fn(expr const & e);
-expr mk_foralli_fn();
-bool is_foralli_fn(expr const & e);
-expr mk_domain_inj_fn();
-bool is_domain_inj_fn(expr const & e);
-expr mk_range_inj_fn();
-bool is_range_inj_fn(expr const & e);
-#endif
 }