From 82dfb553d5fd8adf514cc37cc2477290ca78c56c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 15 Dec 2013 16:26:23 -0800
Subject: [PATCH] feat(library/basic_thms): add ExistsIntro theorem

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/notation.cpp      | 1 +
 src/library/basic_thms.cpp           | 8 ++++++++
 src/library/basic_thms.h             | 4 ++++
 tests/lean/exists1.lean              | 5 +++++
 tests/lean/exists1.lean.expected.out | 7 +++++++
 5 files changed, 25 insertions(+)
 create mode 100644 tests/lean/exists1.lean
 create mode 100644 tests/lean/exists1.lean.expected.out

diff --git a/src/frontends/lean/notation.cpp b/src/frontends/lean/notation.cpp
index 12eda36a4..74ac9e158 100644
--- a/src/frontends/lean/notation.cpp
+++ b/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);
 }
 }
diff --git a/src/library/basic_thms.cpp b/src/library/basic_thms.cpp
index 20491fc6a..bca138c88 100644
--- a/src/library/basic_thms.cpp
+++ b/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
 
diff --git a/src/library/basic_thms.h b/src/library/basic_thms.h
index c0254cbec..6f6b0471b 100644
--- a/src/library/basic_thms.h
+++ b/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);
 
diff --git a/tests/lean/exists1.lean b/tests/lean/exists1.lean
new file mode 100644
index 000000000..f5b9594db
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/tests/lean/exists1.lean.expected.out b/tests/lean/exists1.lean.expected.out
new file mode 100644
index 000000000..4f1a031ce
--- /dev/null
+++ b/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