refactor(builtin/kernel): use standard definition for 'or' and 'and'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
4692e04d70
commit
e9dada5e14
10 changed files with 253 additions and 204 deletions
|
|
@ -11,13 +11,6 @@ import macros
|
|||
import tactic
|
||||
using Nat
|
||||
|
||||
--
|
||||
-- could go in kernel
|
||||
--
|
||||
|
||||
theorem or_imp (p q : Bool) : (p ∨ q) ↔ (¬ p → q)
|
||||
:= subst (symm (imp_or (¬ p) q)) (not_not_eq p)
|
||||
|
||||
--
|
||||
-- fundamental properties of Nat
|
||||
--
|
||||
|
|
|
|||
|
|
@ -43,12 +43,14 @@ alias ⊥ : false
|
|||
definition not (a : Bool) := a → false
|
||||
notation 40 ¬ _ : not
|
||||
|
||||
definition or (a b : Bool) := ¬ a → b
|
||||
definition or (a b : Bool)
|
||||
:= ∀ c : Bool, (a → c) → (b → c) → c
|
||||
infixr 30 || : or
|
||||
infixr 30 \/ : or
|
||||
infixr 30 ∨ : or
|
||||
|
||||
definition and (a b : Bool) := ¬ (a → ¬ b)
|
||||
definition and (a b : Bool)
|
||||
:= ∀ c : Bool, (a → b → c) → c
|
||||
infixr 35 && : and
|
||||
infixr 35 /\ : and
|
||||
infixr 35 ∧ : and
|
||||
|
|
@ -65,9 +67,6 @@ definition iff (a b : Bool) := a = b
|
|||
infixr 25 <-> : iff
|
||||
infixr 25 ↔ : iff
|
||||
|
||||
theorem em (a : Bool) : a ∨ ¬ a
|
||||
:= assume Hna : ¬ a, Hna
|
||||
|
||||
theorem not_intro {a : Bool} (H : a → false) : ¬ a
|
||||
:= H
|
||||
|
||||
|
|
@ -102,15 +101,40 @@ theorem contrapos {a b : Bool} (H : a → b) : ¬ b → ¬ a
|
|||
theorem absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b
|
||||
:= false_elim b (absurd H1 H2)
|
||||
|
||||
-- Recall that or is defined as ¬ a → b
|
||||
theorem or_introl {a : Bool} (H : a) (b : Bool) : a ∨ b
|
||||
:= assume H1 : ¬ a, absurd_elim b H H1
|
||||
:= take c : Bool,
|
||||
assume (H1 : a → c) (H2 : b → c),
|
||||
H1 H
|
||||
|
||||
theorem or_intror {b : Bool} (a : Bool) (H : b) : a ∨ b
|
||||
:= assume H1 : ¬ a, H
|
||||
:= take c : Bool,
|
||||
assume (H1 : a → c) (H2 : b → c),
|
||||
H2 H
|
||||
|
||||
theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
|
||||
:= H1 c H2 H3
|
||||
|
||||
theorem resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b
|
||||
:= H1 H2
|
||||
:= H1 b (assume Ha : a, absurd_elim b Ha H2) (assume Hb : b, Hb)
|
||||
|
||||
theorem resolve2 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ b) : a
|
||||
:= H1 a (assume Ha : a, Ha) (assume Hb : b, absurd_elim a Hb H2)
|
||||
|
||||
theorem or_flip {a b : Bool} (H : a ∨ b) : b ∨ a
|
||||
:= take c : Bool,
|
||||
assume (H1 : b → c) (H2 : a → c),
|
||||
H c H2 H1
|
||||
|
||||
theorem and_intro {a b : Bool} (H1 : a) (H2 : b) : a ∧ b
|
||||
:= take c : Bool,
|
||||
assume H : a → b → c,
|
||||
H H1 H2
|
||||
|
||||
theorem and_eliml {a b : Bool} (H : a ∧ b) : a
|
||||
:= H a (assume (Ha : a) (Hb : b), Ha)
|
||||
|
||||
theorem and_elimr {a b : Bool} (H : a ∧ b) : b
|
||||
:= H b (assume (Ha : a) (Hb : b), Hb)
|
||||
|
||||
axiom subst {A : (Type U)} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a = b) : P b
|
||||
|
||||
|
|
@ -195,13 +219,17 @@ 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
|
||||
axiom boolcomplete (a : Bool) : a = true ∨ a = false
|
||||
|
||||
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 case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
|
||||
:= or_elim (boolcomplete a)
|
||||
(assume Ht : a = true, subst H1 (symm Ht))
|
||||
(assume Hf : a = false, subst H2 (symm Hf))
|
||||
|
||||
theorem em (a : Bool) : a ∨ ¬ a
|
||||
:= or_elim (boolcomplete a)
|
||||
(assume Ht : a = true, or_introl (eqt_elim Ht) (¬ a))
|
||||
(assume Hf : a = false, or_intror a (eqf_elim Hf))
|
||||
|
||||
theorem boolcomplete_swapped (a : Bool) : a = false ∨ a = true
|
||||
:= case (λ x, x = false ∨ x = true)
|
||||
|
|
@ -254,25 +282,6 @@ theorem not_imp_elimr {a b : Bool} (H : ¬ (a → b)) : ¬ b
|
|||
:= assume Hb : b, absurd (assume Ha : a, Hb)
|
||||
H
|
||||
|
||||
-- Recall that and is defined as ¬ (a → ¬ b)
|
||||
theorem and_intro {a b : Bool} (H1 : a) (H2 : b) : a ∧ b
|
||||
:= assume H : a → ¬ b, absurd H2 (H H1)
|
||||
|
||||
theorem and_eliml {a b : Bool} (H : a ∧ b) : a
|
||||
:= not_imp_eliml H
|
||||
|
||||
theorem and_elimr {a b : Bool} (H : a ∧ b) : b
|
||||
:= not_not_elim (not_imp_elimr H)
|
||||
|
||||
theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
|
||||
:= not_not_elim
|
||||
(assume H : ¬ c,
|
||||
absurd (H3 (resolve1 H1 (mt (assume Ha : a, H2 Ha) H)))
|
||||
H)
|
||||
|
||||
theorem by_contradiction {a : Bool} (H : ¬ a → false) : a
|
||||
:= or_elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false_elim a (H H1))
|
||||
|
||||
theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b
|
||||
:= or_elim (boolcomplete a)
|
||||
(λ Hat : a = true, or_elim (boolcomplete b)
|
||||
|
|
@ -294,6 +303,9 @@ theorem eqf_intro {a : Bool} (H : ¬ a) : a = false
|
|||
:= boolext (assume H1 : a, absurd H1 H)
|
||||
(assume H2 : false, false_elim a H2)
|
||||
|
||||
theorem by_contradiction {a : Bool} (H : ¬ a → false) : a
|
||||
:= or_elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false_elim a (H H1))
|
||||
|
||||
theorem a_neq_a {A : (Type U)} (a : A) : (a ≠ a) ↔ false
|
||||
:= boolext (assume H, a_neq_a_elim H)
|
||||
(assume H, false_elim (a ≠ a) H)
|
||||
|
|
@ -362,9 +374,6 @@ theorem or_left_comm (a b c : Bool) : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c)
|
|||
|
||||
add_rewrite or_comm or_assoc or_id or_falsel or_falser or_truel or_truer or_tauto or_left_comm
|
||||
|
||||
theorem resolve2 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ b) : a
|
||||
:= resolve1 ((or_comm a b) ◂ H1) H2
|
||||
|
||||
theorem and_comm (a b : Bool) : a ∧ b ↔ b ∧ a
|
||||
:= boolext (assume H, and_intro (and_elimr H) (and_eliml H))
|
||||
(assume H, and_intro (and_elimr H) (and_eliml H))
|
||||
|
|
@ -430,6 +439,17 @@ theorem imp_or (a b : Bool) : (a → b) ↔ ¬ a ∨ b
|
|||
assume Ha : a,
|
||||
resolve1 H ((symm (not_not_eq a)) ◂ Ha))
|
||||
|
||||
theorem or_imp (a b : Bool) : a ∨ b ↔ (¬ a → b)
|
||||
:= boolext
|
||||
(assume H : a ∨ b,
|
||||
(or_elim H
|
||||
(assume (Ha : a) (Hna : ¬ a), absurd_elim b Ha Hna)
|
||||
(assume (Hb : b) (Hna : ¬ a), Hb)))
|
||||
(assume H : ¬ a → b,
|
||||
(or_elim (em a)
|
||||
(assume Ha : a, or_introl Ha b)
|
||||
(assume Hna : ¬ a, or_intror a (H Hna))))
|
||||
|
||||
theorem not_congr {a b : Bool} (H : a ↔ b) : ¬ a ↔ ¬ b
|
||||
:= congr2 not H
|
||||
|
||||
|
|
@ -509,6 +529,94 @@ theorem forall_rem {A : (Type U)} (H : inhabited A) (p : Bool) : (∀ x : A, p)
|
|||
(assume Hr : p,
|
||||
take x, Hr)
|
||||
|
||||
|
||||
theorem not_and (a b : Bool) : ¬ (a ∧ b) ↔ ¬ a ∨ ¬ b
|
||||
:= boolext (assume H, or_elim (em a)
|
||||
(assume Ha, or_elim (em b)
|
||||
(assume Hb, absurd_elim (¬ a ∨ ¬ b) (and_intro Ha Hb) H)
|
||||
(assume Hnb, or_intror (¬ a) Hnb))
|
||||
(assume Hna, or_introl Hna (¬ b)))
|
||||
(assume (H : ¬ a ∨ ¬ b) (N : a ∧ b),
|
||||
or_elim H
|
||||
(assume Hna, absurd (and_eliml N) Hna)
|
||||
(assume Hnb, absurd (and_elimr N) Hnb))
|
||||
|
||||
theorem not_and_elim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b
|
||||
:= (not_and a b) ◂ H
|
||||
|
||||
theorem not_or (a b : Bool) : ¬ (a ∨ b) ↔ ¬ a ∧ ¬ b
|
||||
:= boolext (assume H, or_elim (em a)
|
||||
(assume Ha, absurd_elim (¬ a ∧ ¬ b) (or_introl Ha b) H)
|
||||
(assume Hna, or_elim (em b)
|
||||
(assume Hb, absurd_elim (¬ a ∧ ¬ b) (or_intror a Hb) H)
|
||||
(assume Hnb, and_intro Hna Hnb)))
|
||||
(assume (H : ¬ a ∧ ¬ b) (N : a ∨ b),
|
||||
or_elim N
|
||||
(assume Ha, absurd Ha (and_eliml H))
|
||||
(assume Hb, absurd Hb (and_elimr H)))
|
||||
|
||||
theorem not_or_elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b
|
||||
:= (not_or a b) ◂ H
|
||||
|
||||
theorem not_implies (a b : Bool) : ¬ (a → b) ↔ a ∧ ¬ b
|
||||
:= calc (¬ (a → b)) = ¬ (¬ a ∨ b) : { imp_or a b }
|
||||
... = ¬ ¬ a ∧ ¬ b : not_or (¬ a) b
|
||||
... = a ∧ ¬ b : congr2 (λ x, x ∧ ¬ b) (not_not_eq a)
|
||||
|
||||
theorem and_imp (a b : Bool) : a ∧ b ↔ ¬ (a → ¬ b)
|
||||
:= have H1 : a ∧ ¬ ¬ b ↔ ¬ (a → ¬ b),
|
||||
from symm (not_implies a (¬ b)),
|
||||
subst H1 (not_not_eq b)
|
||||
|
||||
theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b
|
||||
:= (not_implies a b) ◂ H
|
||||
|
||||
theorem a_eq_not_a (a : Bool) : (a = ¬ a) ↔ false
|
||||
:= boolext (λ H, or_elim (em a)
|
||||
(λ Ha, absurd Ha (subst Ha H))
|
||||
(λ Hna, absurd (subst Hna (symm H)) Hna))
|
||||
(λ H, false_elim (a = ¬ a) H)
|
||||
|
||||
theorem a_iff_not_a (a : Bool) : (a ↔ ¬ a) ↔ false
|
||||
:= a_eq_not_a a
|
||||
|
||||
theorem true_eq_false : (true = false) ↔ false
|
||||
:= subst (a_eq_not_a true) not_true
|
||||
|
||||
theorem true_iff_false : (true ↔ false) ↔ false
|
||||
:= true_eq_false
|
||||
|
||||
theorem false_eq_true : (false = true) ↔ false
|
||||
:= subst (a_eq_not_a false) not_false
|
||||
|
||||
theorem false_iff_true : (false ↔ true) ↔ false
|
||||
:= false_eq_true
|
||||
|
||||
theorem a_iff_true (a : Bool) : (a ↔ true) ↔ a
|
||||
:= boolext (λ H, eqt_elim H)
|
||||
(λ H, eqt_intro H)
|
||||
|
||||
theorem a_iff_false (a : Bool) : (a ↔ false) ↔ ¬ a
|
||||
:= boolext (λ H, eqf_elim H)
|
||||
(λ H, eqf_intro H)
|
||||
|
||||
add_rewrite a_eq_not_a a_iff_not_a true_eq_false true_iff_false false_eq_true false_iff_true a_iff_true a_iff_false
|
||||
|
||||
theorem not_iff (a b : Bool) : ¬ (a ↔ b) ↔ (¬ a ↔ b)
|
||||
:= or_elim (em b)
|
||||
(λ Hb, calc (¬ (a ↔ b)) = (¬ (a ↔ true)) : { eqt_intro Hb }
|
||||
... = ¬ a : { a_iff_true a }
|
||||
... = ¬ a ↔ true : { symm (a_iff_true (¬ a)) }
|
||||
... = ¬ a ↔ b : { symm (eqt_intro Hb) })
|
||||
(λ Hnb, calc (¬ (a ↔ b)) = (¬ (a ↔ false)) : { eqf_intro Hnb }
|
||||
... = ¬ ¬ a : { a_iff_false a }
|
||||
... = ¬ a ↔ false : { symm (a_iff_false (¬ a)) }
|
||||
... = ¬ a ↔ b : { symm (eqf_intro Hnb) })
|
||||
|
||||
theorem not_iff_elim {a b : Bool} (H : ¬ (a ↔ b)) : (¬ a) ↔ b
|
||||
:= (not_iff a b) ◂ H
|
||||
|
||||
|
||||
-- Congruence theorems for contextual simplification
|
||||
|
||||
-- Simplify a → b, by first simplifying a to c using the fact that ¬ b is true, and then
|
||||
|
|
@ -575,105 +683,41 @@ theorem imp_congrl {a b c d : Bool} (H_bd : ∀ (H_a : a), b = d) (H_ac : ∀ (H
|
|||
theorem imp_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : (a → b) = (c → d)
|
||||
:= imp_congrr (λ H, H_ac) H_bd
|
||||
|
||||
-- In the following theorems we are using the fact that a ∨ b is defined as ¬ a → b
|
||||
theorem or_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : a ∨ b ↔ c ∨ d
|
||||
:= imp_congrr (λ H_nb : ¬ b, congr2 not (H_ac H_nb)) H_bd
|
||||
:= have H1 : (¬ a → b) ↔ (¬ c → d),
|
||||
from imp_congrr (λ H_nb : ¬ b, congr2 not (H_ac H_nb)) H_bd,
|
||||
calc (a ∨ b) = (¬ a → b) : or_imp _ _
|
||||
... = (¬ c → d) : H1
|
||||
... = c ∨ d : symm (or_imp _ _)
|
||||
|
||||
theorem or_congrl {a b c d : Bool} (H_bd : ∀ (H_na : ¬ a), b = d) (H_ac : ∀ (H_nd : ¬ d), a = c) : a ∨ b ↔ c ∨ d
|
||||
:= imp_congrl H_bd (λ H_nd : ¬ d, congr2 not (H_ac H_nd))
|
||||
:= have H1 : (¬ a → b) ↔ (¬ c → d),
|
||||
from imp_congrl H_bd (λ H_nd : ¬ d, congr2 not (H_ac H_nd)),
|
||||
calc (a ∨ b) = (¬ a → b) : or_imp _ _
|
||||
... = (¬ c → d) : H1
|
||||
... = c ∨ d : symm (or_imp _ _)
|
||||
-- (Common case) simplify a to c, and then b to d using the fact that ¬ c is true
|
||||
theorem or_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : a ∨ b ↔ c ∨ d
|
||||
:= or_congrr (λ H, H_ac) H_bd
|
||||
|
||||
-- In the following theorems we are using the fact hat a ∧ b is defined as ¬ (a → ¬ b)
|
||||
theorem and_congrr {a b c d : Bool} (H_ac : ∀ (H_b : b), a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ↔ c ∧ d
|
||||
:= congr2 not (imp_congrr (λ (H_nnb : ¬ ¬ b), H_ac (not_not_elim H_nnb)) (λ H_c : c, congr2 not (H_bd H_c)))
|
||||
:= have H1 : ¬ (a → ¬ b) ↔ ¬ (c → ¬ d),
|
||||
from congr2 not (imp_congrr (λ (H_nnb : ¬ ¬ b), H_ac (not_not_elim H_nnb)) (λ H_c : c, congr2 not (H_bd H_c))),
|
||||
calc (a ∧ b) = ¬ (a → ¬ b) : and_imp _ _
|
||||
... = ¬ (c → ¬ d) : H1
|
||||
... = c ∧ d : symm (and_imp _ _)
|
||||
|
||||
theorem and_congrl {a b c d : Bool} (H_bd : ∀ (H_a : a), b = d) (H_ac : ∀ (H_d : d), a = c) : a ∧ b ↔ c ∧ d
|
||||
:= congr2 not (imp_congrl (λ H_a : a, congr2 not (H_bd H_a)) (λ (H_nnd : ¬ ¬ d), H_ac (not_not_elim H_nnd)))
|
||||
:= have H1 : ¬ (a → ¬ b) ↔ ¬ (c → ¬ d),
|
||||
from congr2 not (imp_congrl (λ H_a : a, congr2 not (H_bd H_a)) (λ (H_nnd : ¬ ¬ d), H_ac (not_not_elim H_nnd))),
|
||||
calc (a ∧ b) = ¬ (a → ¬ b) : and_imp _ _
|
||||
... = ¬ (c → ¬ d) : H1
|
||||
... = c ∧ d : symm (and_imp _ _)
|
||||
|
||||
-- (Common case) simplify a to c, and then b to d using the fact that c is true
|
||||
theorem and_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ↔ c ∧ d
|
||||
:= and_congrr (λ H, H_ac) H_bd
|
||||
|
||||
theorem not_and (a b : Bool) : ¬ (a ∧ b) ↔ ¬ a ∨ ¬ b
|
||||
:= boolext (assume H, or_elim (em a)
|
||||
(assume Ha, or_elim (em b)
|
||||
(assume Hb, absurd_elim (¬ a ∨ ¬ b) (and_intro Ha Hb) H)
|
||||
(assume Hnb, or_intror (¬ a) Hnb))
|
||||
(assume Hna, or_introl Hna (¬ b)))
|
||||
(assume (H : ¬ a ∨ ¬ b) (N : a ∧ b),
|
||||
or_elim H
|
||||
(assume Hna, absurd (and_eliml N) Hna)
|
||||
(assume Hnb, absurd (and_elimr N) Hnb))
|
||||
|
||||
theorem not_and_elim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b
|
||||
:= (not_and a b) ◂ H
|
||||
|
||||
theorem not_or (a b : Bool) : ¬ (a ∨ b) ↔ ¬ a ∧ ¬ b
|
||||
:= boolext (assume H, or_elim (em a)
|
||||
(assume Ha, absurd_elim (¬ a ∧ ¬ b) (or_introl Ha b) H)
|
||||
(assume Hna, or_elim (em b)
|
||||
(assume Hb, absurd_elim (¬ a ∧ ¬ b) (or_intror a Hb) H)
|
||||
(assume Hnb, and_intro Hna Hnb)))
|
||||
(assume (H : ¬ a ∧ ¬ b) (N : a ∨ b),
|
||||
or_elim N
|
||||
(assume Ha, absurd Ha (and_eliml H))
|
||||
(assume Hb, absurd Hb (and_elimr H)))
|
||||
|
||||
theorem not_or_elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b
|
||||
:= (not_or a b) ◂ H
|
||||
|
||||
theorem not_implies (a b : Bool) : ¬ (a → b) ↔ a ∧ ¬ b
|
||||
:= calc (¬ (a → b)) = ¬ (¬ a ∨ b) : { imp_or a b }
|
||||
... = ¬ ¬ a ∧ ¬ b : not_or (¬ a) b
|
||||
... = a ∧ ¬ b : congr2 (λ x, x ∧ ¬ b) (not_not_eq a)
|
||||
|
||||
theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b
|
||||
:= (not_implies a b) ◂ H
|
||||
|
||||
theorem a_eq_not_a (a : Bool) : (a = ¬ a) ↔ false
|
||||
:= boolext (λ H, or_elim (em a)
|
||||
(λ Ha, absurd Ha (subst Ha H))
|
||||
(λ Hna, absurd (subst Hna (symm H)) Hna))
|
||||
(λ H, false_elim (a = ¬ a) H)
|
||||
|
||||
theorem a_iff_not_a (a : Bool) : (a ↔ ¬ a) ↔ false
|
||||
:= a_eq_not_a a
|
||||
|
||||
theorem true_eq_false : (true = false) ↔ false
|
||||
:= subst (a_eq_not_a true) not_true
|
||||
|
||||
theorem true_iff_false : (true ↔ false) ↔ false
|
||||
:= true_eq_false
|
||||
|
||||
theorem false_eq_true : (false = true) ↔ false
|
||||
:= subst (a_eq_not_a false) not_false
|
||||
|
||||
theorem false_iff_true : (false ↔ true) ↔ false
|
||||
:= false_eq_true
|
||||
|
||||
theorem a_iff_true (a : Bool) : (a ↔ true) ↔ a
|
||||
:= boolext (λ H, eqt_elim H)
|
||||
(λ H, eqt_intro H)
|
||||
|
||||
theorem a_iff_false (a : Bool) : (a ↔ false) ↔ ¬ a
|
||||
:= boolext (λ H, eqf_elim H)
|
||||
(λ H, eqf_intro H)
|
||||
|
||||
add_rewrite a_eq_not_a a_iff_not_a true_eq_false true_iff_false false_eq_true false_iff_true a_iff_true a_iff_false
|
||||
|
||||
theorem not_iff (a b : Bool) : ¬ (a ↔ b) ↔ (¬ a ↔ b)
|
||||
:= or_elim (em b)
|
||||
(λ Hb, calc (¬ (a ↔ b)) = (¬ (a ↔ true)) : { eqt_intro Hb }
|
||||
... = ¬ a : { a_iff_true a }
|
||||
... = ¬ a ↔ true : { symm (a_iff_true (¬ a)) }
|
||||
... = ¬ a ↔ b : { symm (eqt_intro Hb) })
|
||||
(λ Hnb, calc (¬ (a ↔ b)) = (¬ (a ↔ false)) : { eqf_intro Hnb }
|
||||
... = ¬ ¬ a : { a_iff_false a }
|
||||
... = ¬ a ↔ false : { symm (a_iff_false (¬ a)) }
|
||||
... = ¬ a ↔ b : { symm (eqf_intro Hnb) })
|
||||
|
||||
theorem not_iff_elim {a b : Bool} (H : ¬ (a ↔ b)) : (¬ a) ↔ b
|
||||
:= (not_iff a b) ◂ H
|
||||
|
||||
theorem forall_or_distributer {A : (Type U)} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) = (p ∨ ∀ x, φ x)
|
||||
:= boolext
|
||||
(assume H : (∀ x, p ∨ φ x),
|
||||
|
|
|
|||
Binary file not shown.
|
|
@ -22,7 +22,6 @@ MK_CONSTANT(implies_fn, name("implies"));
|
|||
MK_CONSTANT(neq_fn, name("neq"));
|
||||
MK_CONSTANT(a_neq_a_elim_fn, name("a_neq_a_elim"));
|
||||
MK_CONSTANT(iff_fn, name("iff"));
|
||||
MK_CONSTANT(em_fn, name("em"));
|
||||
MK_CONSTANT(not_intro_fn, name("not_intro"));
|
||||
MK_CONSTANT(absurd_fn, name("absurd"));
|
||||
MK_CONSTANT(exists_fn, name("exists"));
|
||||
|
|
@ -33,7 +32,13 @@ 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(or_elim_fn, name("or_elim"));
|
||||
MK_CONSTANT(resolve1_fn, name("resolve1"));
|
||||
MK_CONSTANT(resolve2_fn, name("resolve2"));
|
||||
MK_CONSTANT(or_flip_fn, name("or_flip"));
|
||||
MK_CONSTANT(and_intro_fn, name("and_intro"));
|
||||
MK_CONSTANT(and_eliml_fn, name("and_eliml"));
|
||||
MK_CONSTANT(and_elimr_fn, name("and_elimr"));
|
||||
MK_CONSTANT(subst_fn, name("subst"));
|
||||
MK_CONSTANT(substp_fn, name("substp"));
|
||||
MK_CONSTANT(symm_fn, name("symm"));
|
||||
|
|
@ -60,8 +65,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(case_fn, name("case"));
|
||||
MK_CONSTANT(em_fn, name("em"));
|
||||
MK_CONSTANT(boolcomplete_swapped_fn, name("boolcomplete_swapped"));
|
||||
MK_CONSTANT(not_true, name("not_true"));
|
||||
MK_CONSTANT(not_false, name("not_false"));
|
||||
|
|
@ -71,15 +77,11 @@ MK_CONSTANT(not_neq_elim_fn, name("not_neq_elim"));
|
|||
MK_CONSTANT(not_not_elim_fn, name("not_not_elim"));
|
||||
MK_CONSTANT(not_imp_eliml_fn, name("not_imp_eliml"));
|
||||
MK_CONSTANT(not_imp_elimr_fn, name("not_imp_elimr"));
|
||||
MK_CONSTANT(and_intro_fn, name("and_intro"));
|
||||
MK_CONSTANT(and_eliml_fn, name("and_eliml"));
|
||||
MK_CONSTANT(and_elimr_fn, name("and_elimr"));
|
||||
MK_CONSTANT(or_elim_fn, name("or_elim"));
|
||||
MK_CONSTANT(by_contradiction_fn, name("by_contradiction"));
|
||||
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(by_contradiction_fn, name("by_contradiction"));
|
||||
MK_CONSTANT(a_neq_a_fn, name("a_neq_a"));
|
||||
MK_CONSTANT(eq_id_fn, name("eq_id"));
|
||||
MK_CONSTANT(iff_id_fn, name("iff_id"));
|
||||
|
|
@ -96,7 +98,6 @@ MK_CONSTANT(or_truel_fn, name("or_truel"));
|
|||
MK_CONSTANT(or_truer_fn, name("or_truer"));
|
||||
MK_CONSTANT(or_tauto_fn, name("or_tauto"));
|
||||
MK_CONSTANT(or_left_comm_fn, name("or_left_comm"));
|
||||
MK_CONSTANT(resolve2_fn, name("resolve2"));
|
||||
MK_CONSTANT(and_comm_fn, name("and_comm"));
|
||||
MK_CONSTANT(and_id_fn, name("and_id"));
|
||||
MK_CONSTANT(and_assoc_fn, name("and_assoc"));
|
||||
|
|
@ -112,6 +113,7 @@ MK_CONSTANT(imp_falser_fn, name("imp_falser"));
|
|||
MK_CONSTANT(imp_falsel_fn, name("imp_falsel"));
|
||||
MK_CONSTANT(imp_id_fn, name("imp_id"));
|
||||
MK_CONSTANT(imp_or_fn, name("imp_or"));
|
||||
MK_CONSTANT(or_imp_fn, name("or_imp"));
|
||||
MK_CONSTANT(not_congr_fn, name("not_congr"));
|
||||
MK_CONSTANT(exists_elim_fn, name("exists_elim"));
|
||||
MK_CONSTANT(exists_intro_fn, name("exists_intro"));
|
||||
|
|
@ -127,20 +129,12 @@ MK_CONSTANT(inhabited_ex_intro_fn, name("inhabited_ex_intro"));
|
|||
MK_CONSTANT(inhabited_range_fn, name("inhabited_range"));
|
||||
MK_CONSTANT(exists_rem_fn, name("exists_rem"));
|
||||
MK_CONSTANT(forall_rem_fn, name("forall_rem"));
|
||||
MK_CONSTANT(imp_congrr_fn, name("imp_congrr"));
|
||||
MK_CONSTANT(imp_congrl_fn, name("imp_congrl"));
|
||||
MK_CONSTANT(imp_congr_fn, name("imp_congr"));
|
||||
MK_CONSTANT(or_congrr_fn, name("or_congrr"));
|
||||
MK_CONSTANT(or_congrl_fn, name("or_congrl"));
|
||||
MK_CONSTANT(or_congr_fn, name("or_congr"));
|
||||
MK_CONSTANT(and_congrr_fn, name("and_congrr"));
|
||||
MK_CONSTANT(and_congrl_fn, name("and_congrl"));
|
||||
MK_CONSTANT(and_congr_fn, name("and_congr"));
|
||||
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"));
|
||||
MK_CONSTANT(not_or_elim_fn, name("not_or_elim"));
|
||||
MK_CONSTANT(not_implies_fn, name("not_implies"));
|
||||
MK_CONSTANT(and_imp_fn, name("and_imp"));
|
||||
MK_CONSTANT(not_implies_elim_fn, name("not_implies_elim"));
|
||||
MK_CONSTANT(a_eq_not_a_fn, name("a_eq_not_a"));
|
||||
MK_CONSTANT(a_iff_not_a_fn, name("a_iff_not_a"));
|
||||
|
|
@ -152,6 +146,15 @@ MK_CONSTANT(a_iff_true_fn, name("a_iff_true"));
|
|||
MK_CONSTANT(a_iff_false_fn, name("a_iff_false"));
|
||||
MK_CONSTANT(not_iff_fn, name("not_iff"));
|
||||
MK_CONSTANT(not_iff_elim_fn, name("not_iff_elim"));
|
||||
MK_CONSTANT(imp_congrr_fn, name("imp_congrr"));
|
||||
MK_CONSTANT(imp_congrl_fn, name("imp_congrl"));
|
||||
MK_CONSTANT(imp_congr_fn, name("imp_congr"));
|
||||
MK_CONSTANT(or_congrr_fn, name("or_congrr"));
|
||||
MK_CONSTANT(or_congrl_fn, name("or_congrl"));
|
||||
MK_CONSTANT(or_congr_fn, name("or_congr"));
|
||||
MK_CONSTANT(and_congrr_fn, name("and_congrr"));
|
||||
MK_CONSTANT(and_congrl_fn, name("and_congrl"));
|
||||
MK_CONSTANT(and_congr_fn, name("and_congr"));
|
||||
MK_CONSTANT(forall_or_distributer_fn, name("forall_or_distributer"));
|
||||
MK_CONSTANT(forall_or_distributel_fn, name("forall_or_distributel"));
|
||||
MK_CONSTANT(forall_and_distribute_fn, name("forall_and_distribute"));
|
||||
|
|
|
|||
|
|
@ -55,9 +55,6 @@ expr mk_iff_fn();
|
|||
bool is_iff_fn(expr const & e);
|
||||
inline bool is_iff(expr const & e) { return is_app(e) && is_iff_fn(arg(e, 0)) && num_args(e) == 3; }
|
||||
inline expr mk_iff(expr const & e1, expr const & e2) { return mk_app({mk_iff_fn(), e1, e2}); }
|
||||
expr mk_em_fn();
|
||||
bool is_em_fn(expr const & e);
|
||||
inline expr mk_em_th(expr const & e1) { return mk_app({mk_em_fn(), e1}); }
|
||||
expr mk_not_intro_fn();
|
||||
bool is_not_intro_fn(expr const & e);
|
||||
inline expr mk_not_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_not_intro_fn(), e1, e2}); }
|
||||
|
|
@ -90,9 +87,27 @@ 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_or_elim_fn();
|
||||
bool is_or_elim_fn(expr const & e);
|
||||
inline expr mk_or_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_elim_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
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}); }
|
||||
expr mk_resolve2_fn();
|
||||
bool is_resolve2_fn(expr const & e);
|
||||
inline expr mk_resolve2_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_resolve2_fn(), e1, e2, e3, e4}); }
|
||||
expr mk_or_flip_fn();
|
||||
bool is_or_flip_fn(expr const & e);
|
||||
inline expr mk_or_flip_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_or_flip_fn(), e1, e2, e3}); }
|
||||
expr mk_and_intro_fn();
|
||||
bool is_and_intro_fn(expr const & e);
|
||||
inline expr mk_and_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_and_intro_fn(), e1, e2, e3, e4}); }
|
||||
expr mk_and_eliml_fn();
|
||||
bool is_and_eliml_fn(expr const & e);
|
||||
inline expr mk_and_eliml_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_eliml_fn(), e1, e2, e3}); }
|
||||
expr mk_and_elimr_fn();
|
||||
bool is_and_elimr_fn(expr const & e);
|
||||
inline expr mk_and_elimr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_elimr_fn(), e1, e2, e3}); }
|
||||
expr mk_subst_fn();
|
||||
bool is_subst_fn(expr const & e);
|
||||
inline expr mk_subst_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_subst_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
|
|
@ -169,12 +184,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_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_em_fn();
|
||||
bool is_em_fn(expr const & e);
|
||||
inline expr mk_em_th(expr const & e1) { return mk_app({mk_em_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}); }
|
||||
|
|
@ -200,21 +218,6 @@ inline expr mk_not_imp_eliml_th(expr const & e1, expr const & e2, expr const & e
|
|||
expr mk_not_imp_elimr_fn();
|
||||
bool is_not_imp_elimr_fn(expr const & e);
|
||||
inline expr mk_not_imp_elimr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_imp_elimr_fn(), e1, e2, e3}); }
|
||||
expr mk_and_intro_fn();
|
||||
bool is_and_intro_fn(expr const & e);
|
||||
inline expr mk_and_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_and_intro_fn(), e1, e2, e3, e4}); }
|
||||
expr mk_and_eliml_fn();
|
||||
bool is_and_eliml_fn(expr const & e);
|
||||
inline expr mk_and_eliml_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_eliml_fn(), e1, e2, e3}); }
|
||||
expr mk_and_elimr_fn();
|
||||
bool is_and_elimr_fn(expr const & e);
|
||||
inline expr mk_and_elimr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_elimr_fn(), e1, e2, e3}); }
|
||||
expr mk_or_elim_fn();
|
||||
bool is_or_elim_fn(expr const & e);
|
||||
inline expr mk_or_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_elim_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_by_contradiction_fn();
|
||||
bool is_by_contradiction_fn(expr const & e);
|
||||
inline expr mk_by_contradiction_th(expr const & e1, expr const & e2) { return mk_app({mk_by_contradiction_fn(), e1, e2}); }
|
||||
expr mk_boolext_fn();
|
||||
bool is_boolext_fn(expr const & e);
|
||||
inline expr mk_boolext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_boolext_fn(), e1, e2, e3, e4}); }
|
||||
|
|
@ -227,6 +230,9 @@ inline expr mk_eqt_intro_th(expr const & e1, expr const & e2) { return mk_app({m
|
|||
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_by_contradiction_fn();
|
||||
bool is_by_contradiction_fn(expr const & e);
|
||||
inline expr mk_by_contradiction_th(expr const & e1, expr const & e2) { return mk_app({mk_by_contradiction_fn(), e1, e2}); }
|
||||
expr mk_a_neq_a_fn();
|
||||
bool is_a_neq_a_fn(expr const & e);
|
||||
inline expr mk_a_neq_a_th(expr const & e1, expr const & e2) { return mk_app({mk_a_neq_a_fn(), e1, e2}); }
|
||||
|
|
@ -275,9 +281,6 @@ inline expr mk_or_tauto_th(expr const & e1) { return mk_app({mk_or_tauto_fn(), e
|
|||
expr mk_or_left_comm_fn();
|
||||
bool is_or_left_comm_fn(expr const & e);
|
||||
inline expr mk_or_left_comm_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_or_left_comm_fn(), e1, e2, e3}); }
|
||||
expr mk_resolve2_fn();
|
||||
bool is_resolve2_fn(expr const & e);
|
||||
inline expr mk_resolve2_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_resolve2_fn(), e1, e2, e3, e4}); }
|
||||
expr mk_and_comm_fn();
|
||||
bool is_and_comm_fn(expr const & e);
|
||||
inline expr mk_and_comm_th(expr const & e1, expr const & e2) { return mk_app({mk_and_comm_fn(), e1, e2}); }
|
||||
|
|
@ -323,6 +326,9 @@ inline expr mk_imp_id_th(expr const & e1) { return mk_app({mk_imp_id_fn(), e1});
|
|||
expr mk_imp_or_fn();
|
||||
bool is_imp_or_fn(expr const & e);
|
||||
inline expr mk_imp_or_th(expr const & e1, expr const & e2) { return mk_app({mk_imp_or_fn(), e1, e2}); }
|
||||
expr mk_or_imp_fn();
|
||||
bool is_or_imp_fn(expr const & e);
|
||||
inline expr mk_or_imp_th(expr const & e1, expr const & e2) { return mk_app({mk_or_imp_fn(), e1, e2}); }
|
||||
expr mk_not_congr_fn();
|
||||
bool is_not_congr_fn(expr const & e);
|
||||
inline expr mk_not_congr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_congr_fn(), e1, e2, e3}); }
|
||||
|
|
@ -369,33 +375,6 @@ inline expr mk_exists_rem_th(expr const & e1, expr const & e2, expr const & e3)
|
|||
expr mk_forall_rem_fn();
|
||||
bool is_forall_rem_fn(expr const & e);
|
||||
inline expr mk_forall_rem_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_forall_rem_fn(), e1, e2, e3}); }
|
||||
expr mk_imp_congrr_fn();
|
||||
bool is_imp_congrr_fn(expr const & e);
|
||||
inline expr mk_imp_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congrr_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_imp_congrl_fn();
|
||||
bool is_imp_congrl_fn(expr const & e);
|
||||
inline expr mk_imp_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congrl_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_imp_congr_fn();
|
||||
bool is_imp_congr_fn(expr const & e);
|
||||
inline expr mk_imp_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congr_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_or_congrr_fn();
|
||||
bool is_or_congrr_fn(expr const & e);
|
||||
inline expr mk_or_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congrr_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_or_congrl_fn();
|
||||
bool is_or_congrl_fn(expr const & e);
|
||||
inline expr mk_or_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congrl_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_or_congr_fn();
|
||||
bool is_or_congr_fn(expr const & e);
|
||||
inline expr mk_or_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congr_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_and_congrr_fn();
|
||||
bool is_and_congrr_fn(expr const & e);
|
||||
inline expr mk_and_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congrr_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_and_congrl_fn();
|
||||
bool is_and_congrl_fn(expr const & e);
|
||||
inline expr mk_and_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congrl_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_and_congr_fn();
|
||||
bool is_and_congr_fn(expr const & e);
|
||||
inline expr mk_and_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congr_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
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}); }
|
||||
|
|
@ -411,6 +390,9 @@ inline expr mk_not_or_elim_th(expr const & e1, expr const & e2, expr const & e3)
|
|||
expr mk_not_implies_fn();
|
||||
bool is_not_implies_fn(expr const & e);
|
||||
inline expr mk_not_implies_th(expr const & e1, expr const & e2) { return mk_app({mk_not_implies_fn(), e1, e2}); }
|
||||
expr mk_and_imp_fn();
|
||||
bool is_and_imp_fn(expr const & e);
|
||||
inline expr mk_and_imp_th(expr const & e1, expr const & e2) { return mk_app({mk_and_imp_fn(), e1, e2}); }
|
||||
expr mk_not_implies_elim_fn();
|
||||
bool is_not_implies_elim_fn(expr const & e);
|
||||
inline expr mk_not_implies_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_implies_elim_fn(), e1, e2, e3}); }
|
||||
|
|
@ -440,6 +422,33 @@ inline expr mk_not_iff_th(expr const & e1, expr const & e2) { return mk_app({mk_
|
|||
expr mk_not_iff_elim_fn();
|
||||
bool is_not_iff_elim_fn(expr const & e);
|
||||
inline expr mk_not_iff_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_iff_elim_fn(), e1, e2, e3}); }
|
||||
expr mk_imp_congrr_fn();
|
||||
bool is_imp_congrr_fn(expr const & e);
|
||||
inline expr mk_imp_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congrr_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_imp_congrl_fn();
|
||||
bool is_imp_congrl_fn(expr const & e);
|
||||
inline expr mk_imp_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congrl_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_imp_congr_fn();
|
||||
bool is_imp_congr_fn(expr const & e);
|
||||
inline expr mk_imp_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congr_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_or_congrr_fn();
|
||||
bool is_or_congrr_fn(expr const & e);
|
||||
inline expr mk_or_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congrr_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_or_congrl_fn();
|
||||
bool is_or_congrl_fn(expr const & e);
|
||||
inline expr mk_or_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congrl_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_or_congr_fn();
|
||||
bool is_or_congr_fn(expr const & e);
|
||||
inline expr mk_or_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congr_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_and_congrr_fn();
|
||||
bool is_and_congrr_fn(expr const & e);
|
||||
inline expr mk_and_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congrr_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_and_congrl_fn();
|
||||
bool is_and_congrl_fn(expr const & e);
|
||||
inline expr mk_and_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congrl_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_and_congr_fn();
|
||||
bool is_and_congr_fn(expr const & e);
|
||||
inline expr mk_and_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congr_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_forall_or_distributer_fn();
|
||||
bool is_forall_or_distributer_fn(expr const & e);
|
||||
inline expr mk_forall_or_distributer_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_forall_or_distributer_fn(), e1, e2, e3}); }
|
||||
|
|
|
|||
|
|
@ -1,3 +1,3 @@
|
|||
theorem or_imp (p q : Bool) : (p ∨ q) ↔ (¬ p → q)
|
||||
theorem or_imp2 (p q : Bool) : (p ∨ q) ↔ (¬ p → q)
|
||||
:= subst (symm (imp_or (¬ p) q)) (not_not_eq p)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,3 +1,3 @@
|
|||
Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Proved: or_imp
|
||||
Proved: or_imp2
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
theorem symm_iff (p q : Bool) (H : p ↔ q) : (q ↔ p)
|
||||
:= symm H
|
||||
|
||||
theorem or_imp (p q : Bool) : (p ∨ q) ↔ (¬ p → q)
|
||||
theorem or_imp2 (p q : Bool) : (p ∨ q) ↔ (¬ p → q)
|
||||
:= let H1 := symm_iff _ _ (imp_or (¬ p) q) in
|
||||
let H2 := not_not_eq p in
|
||||
let H3 := subst H1 H2 in
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Proved: symm_iff
|
||||
Proved: or_imp
|
||||
Proved: or_imp2
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ Nat::add_comm : ∀ a b : ℕ, a + b = b + a
|
|||
Nat::add_zeror : ∀ a : ℕ, a + 0 = a
|
||||
forall_rem [check] : ∀ (A : (Type U)) (H : inhabited A) (p : Bool), (A → p) ↔ p
|
||||
eq_id : ∀ (A : (Type U)) (a : A), a = a ↔ ⊤
|
||||
exists_rem : ∀ (A : (Type U)) (H : inhabited A) (p : Bool), (∃ x : A, p) ↔ p
|
||||
exists_rem : ∀ (A : (Type U)) (H : inhabited A) (p : Bool), (∃ Hb : A, p) ↔ p
|
||||
exists_and_distributel : ∀ (A : (Type U)) (p : Bool) (φ : A → Bool),
|
||||
(∃ x : A, φ x ∧ p) ↔ (∃ x : A, φ x) ∧ p
|
||||
exists_or_distribute : ∀ (A : (Type U)) (φ ψ : A → Bool),
|
||||
|
|
|
|||
Loading…
Reference in a new issue