From 19ad39159e648ffabd1fe7a418c12489ab9bb03e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 15 Dec 2013 17:35:31 -0800 Subject: [PATCH] feat(library/basic_thms): add ForallIntro theorem Signed-off-by: Leonardo de Moura --- src/frontends/lean/notation.cpp | 1 + src/library/basic_thms.cpp | 28 ++++++++++------------------ src/library/basic_thms.h | 6 +++++- tests/lean/forall1.lean | 3 +++ tests/lean/forall1.lean.expected.out | 5 +++++ 5 files changed, 24 insertions(+), 19 deletions(-) create mode 100644 tests/lean/forall1.lean create mode 100644 tests/lean/forall1.lean.expected.out diff --git a/src/frontends/lean/notation.cpp b/src/frontends/lean/notation.cpp index 74ac9e158c..5ff76c6c8f 100644 --- a/src/frontends/lean/notation.cpp +++ b/src/frontends/lean/notation.cpp @@ -119,6 +119,7 @@ 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_forall_intro_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 bca138c88a..ead8126a56 100644 --- a/src/library/basic_thms.cpp +++ b/src/library/basic_thms.cpp @@ -9,6 +9,8 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "library/basic_thms.h" +#include "kernel/kernel_exception.h" + namespace lean { MK_CONSTANT(trivial, name("Trivial")); @@ -39,6 +41,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(forall_intro_fn, name("ForallIntro")); MK_CONSTANT(exists_intro_fn, name("ExistsIntro")); #if 0 @@ -270,29 +273,18 @@ 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)))); + // ForallIntro : Pi (A : Type u) (P : A -> bool) (H : Pi (x : A), P x), (forall A P) + env->add_theorem(forall_intro_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}}, Forall(A, P)), + Fun({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}}, + Trans(A_pred, P, Fun({x, A}, P(x)), Fun({x, A}, True), + 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))))))); + // 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 - - // foralli : Pi (A : Type u) (P : A -> bool) (H : Pi (x : A), P x), (forall A P) - env->add_axiom(foralli_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}}, Forall(A, P))); - - // ext : Pi (A : Type u) (B : A -> Type u) (f g : Pi (x : A) B x) (H : Pi x : A, (f x) = (g x)), f = g - env->add_axiom(ext_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {H, Pi({x, A}, Eq(f(x), g(x)))}}, Eq(f, g))); - - - // domain_inj : Pi (A A1: Type u) (B : A -> Type u) (B1 : A1 -> Type u) (H : (Pi (x : A), B x) = (Pi (x : A1), B1 x)), A = A1 - expr piA1B1x = Pi({x, A1}, B1(x)); - expr A1_arrow_u = A1 >> TypeU; - env->add_axiom(domain_inj_fn_name, Pi({{A, TypeU}, {A1, TypeU}, {B, A_arrow_u}, {B1, A1_arrow_u}, {H, Eq(piABx, piA1B1x)}}, Eq(A, A1))); - // range_inj : Pi (A A1: Type u) (B : A -> Type u) (B1 : A1 -> Type u) (a : A) (a1 : A1) (H : (Pi (x : A), B x) = (Pi (x : A1), B1 x)), (B a) = (B1 a1) - env->add_axiom(range_inj_fn_name, Pi({{A, TypeU}, {A1, TypeU}, {B, A_arrow_u}, {B1, A1_arrow_u}, {a, A}, {a1, A1}, {H, Eq(piABx, piA1B1x)}}, Eq(B(a), B1(a1)))); -#endif } } diff --git a/src/library/basic_thms.h b/src/library/basic_thms.h index 6f6b0471bd..9c0ecba51f 100644 --- a/src/library/basic_thms.h +++ b/src/library/basic_thms.h @@ -119,9 +119,13 @@ expr mk_congr_fn(); inline expr Congr(expr const & A, expr const & B, expr const & f, expr const & g, expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app({mk_congr_fn(), A, B, f, g, a, b, H1, H2}); } 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 +// \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_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_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); } diff --git a/tests/lean/forall1.lean b/tests/lean/forall1.lean new file mode 100644 index 0000000000..e398033579 --- /dev/null +++ b/tests/lean/forall1.lean @@ -0,0 +1,3 @@ +Variable P : Int -> Bool +Axiom Ax (x : Int) : P x +Check ForallIntro Ax \ No newline at end of file diff --git a/tests/lean/forall1.lean.expected.out b/tests/lean/forall1.lean.expected.out new file mode 100644 index 0000000000..4c2b98211f --- /dev/null +++ b/tests/lean/forall1.lean.expected.out @@ -0,0 +1,5 @@ + Set: pp::colors + Set: pp::unicode + Assumed: P + Assumed: Ax +ForallIntro Ax : ∀ x : ℤ, P x