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

feat(builtin/kernel): add eqf_intro and eqf_elim theorems

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

7
src/builtin/kernel.lean
View file

@ -172,6 +172,9 @@ theorem ne_eq_trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠
theorem eqt_elim {a : Bool} (H : a == true) : a
:= (symm H) ◂ trivial
theorem eqf_elim {a : Bool} (H : a == false) : ¬ a
:= not_intro (λ Ha : a, H ◂ Ha)
theorem congr1 {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (a : A) (H : f == g) : f a == g a
:= substp (fun h : (∀ x : A, B x), f a == h a) (refl (f a)) H
@ -207,6 +210,10 @@ theorem eqt_intro {a : Bool} (H : a) : a == true
:= boolext (λ H1 : a, trivial)
(λ H2 : true, H)
theorem eqf_intro {a : Bool} (H : ¬ a) : a == false
:= boolext (λ H1 : a, absurd H1 H)
(λ H2 : false, false_elim a H2)
theorem or_comm (a b : Bool) : (a ∨ b) == (b ∨ a)
:= boolext (λ H, or_elim H (λ H1, or_intror b H1) (λ H2, or_introl H2 a))
(λ H, or_elim H (λ H1, or_intror a H1) (λ H2, or_introl H2 b))

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

Binary file not shown.

2
src/kernel/kernel_decls.cpp
View file

@ -53,6 +53,7 @@ MK_CONSTANT(ne_symm_fn, name("ne_symm"));
MK_CONSTANT(eq_ne_trans_fn, name("eq_ne_trans"));
MK_CONSTANT(ne_eq_trans_fn, name("ne_eq_trans"));
MK_CONSTANT(eqt_elim_fn, name("eqt_elim"));
MK_CONSTANT(eqf_elim_fn, name("eqf_elim"));
MK_CONSTANT(congr1_fn, name("congr1"));
MK_CONSTANT(congr2_fn, name("congr2"));
MK_CONSTANT(congr_fn, name("congr"));
@ -61,6 +62,7 @@ MK_CONSTANT(exists_intro_fn, name("exists_intro"));
MK_CONSTANT(boolext_fn, name("boolext"));
MK_CONSTANT(iff_intro_fn, name("iff_intro"));
MK_CONSTANT(eqt_intro_fn, name("eqt_intro"));
MK_CONSTANT(eqf_intro_fn, name("eqf_intro"));
MK_CONSTANT(or_comm_fn, name("or_comm"));
MK_CONSTANT(or_assoc_fn, name("or_assoc"));
MK_CONSTANT(or_id_fn, name("or_id"));

6
src/kernel/kernel_decls.h
View file

@ -150,6 +150,9 @@ inline expr mk_ne_eq_trans_th(expr const & e1, expr const & e2, expr const & e3,
expr mk_eqt_elim_fn();
bool is_eqt_elim_fn(expr const & e);
inline expr mk_eqt_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_eqt_elim_fn(), e1, e2}); }
expr mk_eqf_elim_fn();
bool is_eqf_elim_fn(expr const & e);
inline expr mk_eqf_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_eqf_elim_fn(), e1, e2}); }
expr mk_congr1_fn();
bool is_congr1_fn(expr const & e);
inline expr mk_congr1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_congr1_fn(), e1, e2, e3, e4, e5, e6}); }
@ -174,6 +177,9 @@ inline expr mk_iff_intro_th(expr const & e1, expr const & e2, expr const & e3, e
expr mk_eqt_intro_fn();
bool is_eqt_intro_fn(expr const & e);
inline expr mk_eqt_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_eqt_intro_fn(), e1, e2}); }
expr mk_eqf_intro_fn();
bool is_eqf_intro_fn(expr const & e);
inline expr mk_eqf_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_eqf_intro_fn(), e1, e2}); }
expr mk_or_comm_fn();
bool is_or_comm_fn(expr const & e);
inline expr mk_or_comm_th(expr const & e1, expr const & e2) { return mk_app({mk_or_comm_fn(), e1, e2}); }