feat(builtin/kernel): prove false_elim without using case

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-15 14:26:13 -08:00
parent 1739b5c153
commit c526e5ec00
4 changed files with 29 additions and 28 deletions

View file

@ -37,7 +37,6 @@ set_opaque true true
definition false : Bool
:= ∀ x : Bool, x
set_opaque false true
alias : true
alias ⊥ : false
@ -89,10 +88,10 @@ definition Exists (A : (Type U)) (P : A → Bool)
definition exists_unique {A : (Type U)} (p : A → Bool)
:= ∃ x, p x ∧ ∀ y, y ≠ x → ¬ p y
axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
theorem false_elim (a : Bool) (H : false) : a
:= case (λ x, x) trivial H a
:= H a
set_opaque false true
theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬ b) : ¬ a
:= assume Ha : a, absurd (H1 Ha) H2
@ -110,18 +109,6 @@ theorem or_introl {a : Bool} (H : a) (b : Bool) : a b
theorem or_intror {b : Bool} (a : Bool) (H : b) : a b
:= assume H1 : ¬ a, H
theorem boolcomplete (a : Bool) : a = true a = false
:= case (λ x, x = true x = false)
(or_introl (refl true) (true = false))
(or_intror (false = true) (refl false))
a
theorem boolcomplete_swapped (a : Bool) : a = false a = true
:= case (λ x, x = false x = true)
(or_intror (true = false) (refl true))
(or_introl (refl false) (false = true))
a
theorem resolve1 {a b : Bool} (H1 : a b) (H2 : ¬ a) : b
:= H1 H2
@ -208,6 +195,20 @@ theorem eqf_elim {a : Bool} (H : a = false) : ¬ a
theorem heqt_elim {a : Bool} (H : a == true) : a
:= eqt_elim (to_eq H)
axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
theorem boolcomplete (a : Bool) : a = true a = false
:= case (λ x, x = true x = false)
(or_introl (refl true) (true = false))
(or_intror (false = true) (refl false))
a
theorem boolcomplete_swapped (a : Bool) : a = false a = true
:= case (λ x, x = false x = true)
(or_intror (true = false) (refl true))
(or_introl (refl false) (false = true))
a
theorem not_true : (¬ true) = false
:= let aux : ¬ (¬ true) = true
:= assume H : (¬ true) = true,

Binary file not shown.

View file

@ -27,15 +27,12 @@ MK_CONSTANT(not_intro_fn, name("not_intro"));
MK_CONSTANT(absurd_fn, name("absurd"));
MK_CONSTANT(exists_fn, name("exists"));
MK_CONSTANT(exists_unique_fn, name("exists_unique"));
MK_CONSTANT(case_fn, name("case"));
MK_CONSTANT(false_elim_fn, name("false_elim"));
MK_CONSTANT(mt_fn, name("mt"));
MK_CONSTANT(contrapos_fn, name("contrapos"));
MK_CONSTANT(absurd_elim_fn, name("absurd_elim"));
MK_CONSTANT(or_introl_fn, name("or_introl"));
MK_CONSTANT(or_intror_fn, name("or_intror"));
MK_CONSTANT(boolcomplete_fn, name("boolcomplete"));
MK_CONSTANT(boolcomplete_swapped_fn, name("boolcomplete_swapped"));
MK_CONSTANT(resolve1_fn, name("resolve1"));
MK_CONSTANT(subst_fn, name("subst"));
MK_CONSTANT(substp_fn, name("substp"));
@ -63,6 +60,9 @@ 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(heqt_elim_fn, name("heqt_elim"));
MK_CONSTANT(case_fn, name("case"));
MK_CONSTANT(boolcomplete_fn, name("boolcomplete"));
MK_CONSTANT(boolcomplete_swapped_fn, name("boolcomplete_swapped"));
MK_CONSTANT(not_true, name("not_true"));
MK_CONSTANT(not_false, name("not_false"));
MK_CONSTANT(not_not_eq_fn, name("not_not_eq"));

View file

@ -72,9 +72,6 @@ expr mk_exists_unique_fn();
bool is_exists_unique_fn(expr const & e);
inline bool is_exists_unique(expr const & e) { return is_app(e) && is_exists_unique_fn(arg(e, 0)) && num_args(e) == 3; }
inline expr mk_exists_unique(expr const & e1, expr const & e2) { return mk_app({mk_exists_unique_fn(), e1, e2}); }
expr mk_case_fn();
bool is_case_fn(expr const & e);
inline expr mk_case_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_case_fn(), e1, e2, e3, e4}); }
expr mk_false_elim_fn();
bool is_false_elim_fn(expr const & e);
inline expr mk_false_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_false_elim_fn(), e1, e2}); }
@ -93,12 +90,6 @@ inline expr mk_or_introl_th(expr const & e1, expr const & e2, expr const & e3) {
expr mk_or_intror_fn();
bool is_or_intror_fn(expr const & e);
inline expr mk_or_intror_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_or_intror_fn(), e1, e2, e3}); }
expr mk_boolcomplete_fn();
bool is_boolcomplete_fn(expr const & e);
inline expr mk_boolcomplete_th(expr const & e1) { return mk_app({mk_boolcomplete_fn(), e1}); }
expr mk_boolcomplete_swapped_fn();
bool is_boolcomplete_swapped_fn(expr const & e);
inline expr mk_boolcomplete_swapped_th(expr const & e1) { return mk_app({mk_boolcomplete_swapped_fn(), e1}); }
expr mk_resolve1_fn();
bool is_resolve1_fn(expr const & e);
inline expr mk_resolve1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_resolve1_fn(), e1, e2, e3, e4}); }
@ -178,6 +169,15 @@ inline expr mk_eqf_elim_th(expr const & e1, expr const & e2) { return mk_app({mk
expr mk_heqt_elim_fn();
bool is_heqt_elim_fn(expr const & e);
inline expr mk_heqt_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_heqt_elim_fn(), e1, e2}); }
expr mk_case_fn();
bool is_case_fn(expr const & e);
inline expr mk_case_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_case_fn(), e1, e2, e3, e4}); }
expr mk_boolcomplete_fn();
bool is_boolcomplete_fn(expr const & e);
inline expr mk_boolcomplete_th(expr const & e1) { return mk_app({mk_boolcomplete_fn(), e1}); }
expr mk_boolcomplete_swapped_fn();
bool is_boolcomplete_swapped_fn(expr const & e);
inline expr mk_boolcomplete_swapped_th(expr const & e1) { return mk_app({mk_boolcomplete_swapped_fn(), e1}); }
expr mk_not_true();
bool is_not_true(expr const & e);
expr mk_not_false();