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

feat(builtin/kernel): 'implication' simplification theorems

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-11 13:35:20 -08:00
parent 50f281b430
commit 53537d0684
4 changed files with 28 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/builtin/kernel.lean
View file

@ -278,6 +278,18 @@ theorem and_absurd (a : Bool) : (a ∧ ¬ a) == false
:= boolext (λ H, absurd (and_eliml H) (and_elimr H))
(λ H, false_elim (a ∧ ¬ a) H)
theorem imp_truer (a : Bool) : (a → true) == true
:= case (λ x, (x → true) == true) trivial trivial a
theorem imp_truel (a : Bool) : (true → a) == a
:= case (λ x, (true → x) == x) trivial trivial a
theorem imp_falser (a : Bool) : (a → false) == ¬ a
:= refl _
theorem imp_falsel (a : Bool) : (false → a) == true
:= case (λ x, (false → x) == true) trivial trivial a
theorem not_and (a b : Bool) : (¬ (a ∧ b)) == (¬ a ∨ ¬ b)
:= case (λ x, (¬ (x ∧ b)) == (¬ x ∨ ¬ b))
(case (λ y, (¬ (true ∧ y)) == (¬ true ∨ ¬ y)) trivial trivial b)

BIN
src/builtin/obj/kernel.olean
View file

Binary file not shown.

4
src/kernel/kernel_decls.cpp
View file

@ -79,6 +79,10 @@ MK_CONSTANT(and_truel_fn, name("and_truel"));
MK_CONSTANT(and_falsel_fn, name("and_falsel"));
MK_CONSTANT(and_falser_fn, name("and_falser"));
MK_CONSTANT(and_absurd_fn, name("and_absurd"));
MK_CONSTANT(imp_truer_fn, name("imp_truer"));
MK_CONSTANT(imp_truel_fn, name("imp_truel"));
MK_CONSTANT(imp_falser_fn, name("imp_falser"));
MK_CONSTANT(imp_falsel_fn, name("imp_falsel"));
MK_CONSTANT(not_and_fn, name("not_and"));
MK_CONSTANT(not_and_elim_fn, name("not_and_elim"));
MK_CONSTANT(not_or_fn, name("not_or"));

12
src/kernel/kernel_decls.h
View file

@ -228,6 +228,18 @@ inline expr mk_and_falser_th(expr const & e1) { return mk_app({mk_and_falser_fn(
expr mk_and_absurd_fn();
bool is_and_absurd_fn(expr const & e);
inline expr mk_and_absurd_th(expr const & e1) { return mk_app({mk_and_absurd_fn(), e1}); }
expr mk_imp_truer_fn();
bool is_imp_truer_fn(expr const & e);
inline expr mk_imp_truer_th(expr const & e1) { return mk_app({mk_imp_truer_fn(), e1}); }
expr mk_imp_truel_fn();
bool is_imp_truel_fn(expr const & e);
inline expr mk_imp_truel_th(expr const & e1) { return mk_app({mk_imp_truel_fn(), e1}); }
expr mk_imp_falser_fn();
bool is_imp_falser_fn(expr const & e);
inline expr mk_imp_falser_th(expr const & e1) { return mk_app({mk_imp_falser_fn(), e1}); }
expr mk_imp_falsel_fn();
bool is_imp_falsel_fn(expr const & e);
inline expr mk_imp_falsel_th(expr const & e1) { return mk_app({mk_imp_falsel_fn(), e1}); }
expr mk_not_and_fn();
bool is_not_and_fn(expr const & e);
inline expr mk_not_and_th(expr const & e1, expr const & e2) { return mk_app({mk_not_and_fn(), e1, e2}); }