michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Define Lean forall. Prove forall elimination.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-06 16:44:58 -07:00
parent 4c28cb933b
commit d1388f5e3c
2 changed files with 16 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/kernel/builtin.cpp
View file

@ -202,7 +202,7 @@ void add_basic_theory(environment & env) {
env.add_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True)));
// forall : Pi (A : Type u), (A -> Bool) -> Bool
env.add_var(forall_fn_name, q_type);
env.add_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True))));
env.add_definition(exists_fn_name, q_type, Fun({{A,TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x)))))));
// refl : Pi (A : Type u) (a : A), a = a
@ -265,11 +265,14 @@ void add_basic_theory(environment & env) {
Fun({{a, Bool}, {H, Eq(a, True)}},
EqMP(True, a, Symm(Bool, a, True, H), Truth)));
// foralle : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a
env.add_theorem(foralle_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, P(a)),
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))));
// 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)));
// foralle : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a
env.add_axiom(foralle_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, P(a)));
// 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)));

10
src/kernel/builtin.h
View file

@ -158,6 +158,16 @@ bool is_truth(expr const & e);
/** \brief (Theorem) Truth : True */
#define Truth mk_truth()
expr mk_eqt_elim_fn();
bool is_eqt_elim(expr const & e);
// \brief (Theorem) a : Bool, H : a = True |- EqT(a, H) : a
inline expr EqTElim(expr const & a, expr const & H) { return mk_app(mk_eqt_elim_fn(), a, H); }
expr mk_foralle_fn();
bool is_foralle_fn(expr const & e);
// \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_foralle_fn(), A, P, H, a); }
expr mk_ext_fn();
bool is_ext_fn(expr const & e);
expr mk_foralle_fn();