refactor(builtin): more theorems, fix iff notation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
7d6cd514d1
commit
1da4294793
7 changed files with 98 additions and 65 deletions
|
|
@ -36,7 +36,7 @@ axiom add_zeror (a : Nat) : a + 0 = a
|
|||
axiom add_succr (a b : Nat) : a + (b + 1) = (a + b) + 1
|
||||
axiom mul_zeror (a : Nat) : a * 0 = 0
|
||||
axiom mul_succr (a b : Nat) : a * (b + 1) = a * b + a
|
||||
axiom le_def (a b : Nat) : a ≤ b ⟷ ∃ c, a + c = b
|
||||
axiom le_def (a b : Nat) : a ≤ b ↔ ∃ c, a + c = b
|
||||
axiom induction {P : Nat → Bool} (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : ∀ a, P a
|
||||
|
||||
theorem induction_on {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : P a
|
||||
|
|
|
|||
|
|
@ -45,7 +45,7 @@ theorem hcongr
|
|||
L3 : b == b' := cast_eq L2 b,
|
||||
L4 : a == b' := htrans H2 L3,
|
||||
L5 : f a == f b' := congr2 f L4,
|
||||
S1 : (∀ x, B' x) == (∀ x, B x) := symm (type_eq H1),
|
||||
S1 : (∀ x, B' x) == (∀ x, B x) := symm (type_eq H1),
|
||||
g' : (∀ x, B x) := cast S1 g,
|
||||
L6 : g == g' := cast_eq S1 g,
|
||||
L7 : f == g' := htrans H1 L6,
|
||||
|
|
@ -54,6 +54,17 @@ theorem hcongr
|
|||
L10 : g' b' == g b := cast_app S1 L2 g b
|
||||
in htrans L9 L10
|
||||
|
||||
theorem hfunext
|
||||
{A : TypeM} {B B' : A → TypeM} {f : ∀ x : A, B x} {g : ∀ x : A, B' x} (H : ∀ x : A, f x == g x) : f == g
|
||||
:= let L1 : (∀ x : A, B x = B' x) := λ x : A, type_eq (H x),
|
||||
L2 : (∀ x : A, B x) = (∀ x : A, B' x) := allext L1,
|
||||
g' : (∀ x : A, B x) := cast (symm L2) g,
|
||||
Hgg : g == g' := cast_eq (symm L2) g,
|
||||
Hggx : (∀ x : A, g x == g' x) := λ x : A, hcongr Hgg (refl x) ,
|
||||
L3 : (∀ x : A, f x == g' x) := λ x : A, htrans (H x) (Hggx x),
|
||||
Hfg : f == g' := funext L3
|
||||
in htrans Hfg (hsymm Hgg)
|
||||
|
||||
exit -- Stop here, the following axiom is not sound
|
||||
|
||||
-- The following axiom is unsound when we treat Pi and
|
||||
|
|
|
|||
|
|
@ -30,7 +30,7 @@ definition implies (a b : Bool) := a → b
|
|||
definition iff (a b : Bool) := a == b
|
||||
|
||||
infixr 25 <-> : iff
|
||||
infixr 25 ⟷ : iff
|
||||
infixr 25 ↔ : iff
|
||||
|
||||
-- The Lean parser has special treatment for the constant exists.
|
||||
-- It allows us to write
|
||||
|
|
@ -103,8 +103,8 @@ theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b = c) : a → c
|
|||
theorem eq_imp_trans {a b c : Bool} (H1 : a = b) (H2 : b → c) : a → c
|
||||
:= assume Ha, H2 (H1 ◂ Ha)
|
||||
|
||||
theorem not_not_eq (a : Bool) : ¬ ¬ a ⟷ a
|
||||
:= case (λ x, ¬ ¬ x ⟷ x) trivial trivial a
|
||||
theorem not_not_eq (a : Bool) : ¬ ¬ a ↔ a
|
||||
:= case (λ x, ¬ ¬ x ↔ x) trivial trivial a
|
||||
|
||||
theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a
|
||||
:= (not_not_eq a) ◂ H
|
||||
|
|
@ -174,6 +174,16 @@ theorem eq_ne_trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠
|
|||
theorem ne_eq_trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c
|
||||
:= subst H1 H2
|
||||
|
||||
theorem heq_congr {A : TypeU} {a b c d : A} (H1 : a == c) (H2 : b == d) : (a == b) = (c == d)
|
||||
:= calc (a == b) = (c == b) : { H1 }
|
||||
... = (c == d) : { H2 }
|
||||
|
||||
theorem heq_congrl {A : TypeU} {a : A} (b : A) {c : A} (H : a == c) : (a == b) = (c == b)
|
||||
:= heq_congr H (refl b)
|
||||
|
||||
theorem heq_congrr {A : TypeU} (a : A) {b d : A} (H : b == d) : (a == b) = (a == d)
|
||||
:= heq_congr (refl a) H
|
||||
|
||||
theorem eqt_elim {a : Bool} (H : a = true) : a
|
||||
:= (symm H) ◂ trivial
|
||||
|
||||
|
|
@ -228,14 +238,14 @@ theorem eqf_intro {a : Bool} (H : ¬ a) : a = false
|
|||
:= boolext (assume H1 : a, absurd H1 H)
|
||||
(assume H2 : false, false_elim a H2)
|
||||
|
||||
theorem neq_elim {A : TypeU} {a b : A} (H : a ≠ b) : a = b ⟷ false
|
||||
theorem neq_elim {A : TypeU} {a b : A} (H : a ≠ b) : a = b ↔ false
|
||||
:= eqf_intro H
|
||||
|
||||
theorem or_comm (a b : Bool) : a ∨ b ⟷ b ∨ a
|
||||
theorem or_comm (a b : Bool) : a ∨ b ↔ b ∨ a
|
||||
:= boolext (assume H, or_elim H (λ H1, or_intror b H1) (λ H2, or_introl H2 a))
|
||||
(assume H, or_elim H (λ H1, or_intror a H1) (λ H2, or_introl H2 b))
|
||||
|
||||
theorem or_assoc (a b c : Bool) : (a ∨ b) ∨ c ⟷ a ∨ (b ∨ c)
|
||||
theorem or_assoc (a b c : Bool) : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c)
|
||||
:= boolext (assume H : (a ∨ b) ∨ c,
|
||||
or_elim H (λ H1 : a ∨ b, or_elim H1 (λ Ha : a, or_introl Ha (b ∨ c))
|
||||
(λ Hb : b, or_intror a (or_introl Hb c)))
|
||||
|
|
@ -245,118 +255,118 @@ theorem or_assoc (a b c : Bool) : (a ∨ b) ∨ c ⟷ a ∨ (b ∨ c)
|
|||
(λ H1 : b ∨ c, or_elim H1 (λ Hb : b, or_introl (or_intror a Hb) c)
|
||||
(λ Hc : c, or_intror (a ∨ b) Hc)))
|
||||
|
||||
theorem or_id (a : Bool) : a ∨ a ⟷ a
|
||||
theorem or_id (a : Bool) : a ∨ a ↔ a
|
||||
:= boolext (assume H, or_elim H (λ H1, H1) (λ H2, H2))
|
||||
(assume H, or_introl H a)
|
||||
|
||||
theorem or_falsel (a : Bool) : a ∨ false ⟷ a
|
||||
theorem or_falsel (a : Bool) : a ∨ false ↔ a
|
||||
:= boolext (assume H, or_elim H (λ H1, H1) (λ H2, false_elim a H2))
|
||||
(assume H, or_introl H false)
|
||||
|
||||
theorem or_falser (a : Bool) : false ∨ a ⟷ a
|
||||
theorem or_falser (a : Bool) : false ∨ a ↔ a
|
||||
:= (or_comm false a) ⋈ (or_falsel a)
|
||||
|
||||
theorem or_truel (a : Bool) : true ∨ a ⟷ true
|
||||
theorem or_truel (a : Bool) : true ∨ a ↔ true
|
||||
:= eqt_intro (case (λ x : Bool, true ∨ x) trivial trivial a)
|
||||
|
||||
theorem or_truer (a : Bool) : a ∨ true ⟷ true
|
||||
theorem or_truer (a : Bool) : a ∨ true ↔ true
|
||||
:= (or_comm a true) ⋈ (or_truel a)
|
||||
|
||||
theorem or_tauto (a : Bool) : a ∨ ¬ a ⟷ true
|
||||
theorem or_tauto (a : Bool) : a ∨ ¬ a ↔ true
|
||||
:= eqt_intro (em a)
|
||||
|
||||
theorem and_comm (a b : Bool) : a ∧ b ⟷ b ∧ a
|
||||
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))
|
||||
|
||||
theorem and_id (a : Bool) : a ∧ a ⟷ a
|
||||
theorem and_id (a : Bool) : a ∧ a ↔ a
|
||||
:= boolext (assume H, and_eliml H)
|
||||
(assume H, and_intro H H)
|
||||
|
||||
theorem and_assoc (a b c : Bool) : (a ∧ b) ∧ c ⟷ a ∧ (b ∧ c)
|
||||
theorem and_assoc (a b c : Bool) : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c)
|
||||
:= boolext (assume H, and_intro (and_eliml (and_eliml H)) (and_intro (and_elimr (and_eliml H)) (and_elimr H)))
|
||||
(assume H, and_intro (and_intro (and_eliml H) (and_eliml (and_elimr H))) (and_elimr (and_elimr H)))
|
||||
|
||||
theorem and_truer (a : Bool) : a ∧ true ⟷ a
|
||||
theorem and_truer (a : Bool) : a ∧ true ↔ a
|
||||
:= boolext (assume H : a ∧ true, and_eliml H)
|
||||
(assume H : a, and_intro H trivial)
|
||||
|
||||
theorem and_truel (a : Bool) : true ∧ a ⟷ a
|
||||
theorem and_truel (a : Bool) : true ∧ a ↔ a
|
||||
:= trans (and_comm true a) (and_truer a)
|
||||
|
||||
theorem and_falsel (a : Bool) : a ∧ false ⟷ false
|
||||
theorem and_falsel (a : Bool) : a ∧ false ↔ false
|
||||
:= boolext (assume H, and_elimr H)
|
||||
(assume H, false_elim (a ∧ false) H)
|
||||
|
||||
theorem and_falser (a : Bool) : false ∧ a ⟷ false
|
||||
theorem and_falser (a : Bool) : false ∧ a ↔ false
|
||||
:= (and_comm false a) ⋈ (and_falsel a)
|
||||
|
||||
theorem and_absurd (a : Bool) : a ∧ ¬ a ⟷ false
|
||||
theorem and_absurd (a : Bool) : a ∧ ¬ a ↔ false
|
||||
:= boolext (assume H, absurd (and_eliml H) (and_elimr H))
|
||||
(assume H, false_elim (a ∧ ¬ a) H)
|
||||
|
||||
theorem imp_truer (a : Bool) : (a → true) ⟷ true
|
||||
:= case (λ x, (x → true) ⟷ true) trivial trivial a
|
||||
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_truel (a : Bool) : (true → a) ↔ a
|
||||
:= case (λ x, (true → x) ↔ x) trivial trivial a
|
||||
|
||||
theorem imp_falser (a : Bool) : (a → false) ⟷ ¬ 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 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)
|
||||
(case (λ y, ¬ (false ∧ y) ⟷ ¬ false ∨ ¬ y) trivial trivial b)
|
||||
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)
|
||||
(case (λ y, ¬ (false ∧ y) ↔ ¬ false ∨ ¬ y) trivial trivial b)
|
||||
a
|
||||
|
||||
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
|
||||
:= case (λ x, ¬ (x ∨ b) ⟷ ¬ x ∧ ¬ b)
|
||||
(case (λ y, ¬ (true ∨ y) ⟷ ¬ true ∧ ¬ y) trivial trivial b)
|
||||
(case (λ y, ¬ (false ∨ y) ⟷ ¬ false ∧ ¬ y) trivial trivial b)
|
||||
theorem not_or (a b : Bool) : ¬ (a ∨ b) ↔ ¬ a ∧ ¬ b
|
||||
:= case (λ x, ¬ (x ∨ b) ↔ ¬ x ∧ ¬ b)
|
||||
(case (λ y, ¬ (true ∨ y) ↔ ¬ true ∧ ¬ y) trivial trivial b)
|
||||
(case (λ y, ¬ (false ∨ y) ↔ ¬ false ∧ ¬ y) trivial trivial b)
|
||||
a
|
||||
|
||||
theorem not_or_elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b
|
||||
:= (not_or a b) ◂ H
|
||||
|
||||
theorem not_iff (a b : Bool) : ¬ (a ⟷ b) ⟷ (¬ a ⟷ b)
|
||||
:= case (λ x, ¬ (x ⟷ b) ⟷ ((¬ x) ⟷ b))
|
||||
(case (λ y, ¬ (true ⟷ y) ⟷ ((¬ true) ⟷ y)) trivial trivial b)
|
||||
(case (λ y, ¬ (false ⟷ y) ⟷ ((¬ false) ⟷ y)) trivial trivial b)
|
||||
theorem not_iff (a b : Bool) : ¬ (a ↔ b) ↔ (¬ a ↔ b)
|
||||
:= case (λ x, ¬ (x ↔ b) ↔ ((¬ x) ↔ b))
|
||||
(case (λ y, ¬ (true ↔ y) ↔ ((¬ true) ↔ y)) trivial trivial b)
|
||||
(case (λ y, ¬ (false ↔ y) ↔ ((¬ false) ↔ y)) trivial trivial b)
|
||||
a
|
||||
|
||||
theorem not_iff_elim {a b : Bool} (H : ¬ (a ⟷ b)) : (¬ a) ⟷ b
|
||||
theorem not_iff_elim {a b : Bool} (H : ¬ (a ↔ b)) : (¬ a) ↔ b
|
||||
:= (not_iff a b) ◂ H
|
||||
|
||||
theorem not_implies (a b : Bool) : ¬ (a → b) ⟷ a ∧ ¬ b
|
||||
:= case (λ x, ¬ (x → b) ⟷ x ∧ ¬ b)
|
||||
(case (λ y, ¬ (true → y) ⟷ true ∧ ¬ y) trivial trivial b)
|
||||
(case (λ y, ¬ (false → y) ⟷ false ∧ ¬ y) trivial trivial b)
|
||||
theorem not_implies (a b : Bool) : ¬ (a → b) ↔ a ∧ ¬ b
|
||||
:= case (λ x, ¬ (x → b) ↔ x ∧ ¬ b)
|
||||
(case (λ y, ¬ (true → y) ↔ true ∧ ¬ y) trivial trivial b)
|
||||
(case (λ y, ¬ (false → y) ↔ false ∧ ¬ y) trivial trivial b)
|
||||
a
|
||||
|
||||
theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b
|
||||
:= (not_implies a b) ◂ H
|
||||
|
||||
theorem not_congr {a b : Bool} (H : a ⟷ b) : ¬ a ⟷ ¬ b
|
||||
theorem not_congr {a b : Bool} (H : a ↔ b) : ¬ a ↔ ¬ b
|
||||
:= congr2 not H
|
||||
|
||||
theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x ⟷ Q x) : (∃ x : A, P x) ⟷ (∃ x : A, Q x)
|
||||
theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x ↔ Q x) : (∃ x : A, P x) ↔ (∃ x : A, Q x)
|
||||
:= congr2 (Exists A) (funext H)
|
||||
|
||||
theorem not_forall (A : (Type U)) (P : A → Bool) : ¬ (∀ x : A, P x) ⟷ (∃ x : A, ¬ P x)
|
||||
theorem not_forall (A : (Type U)) (P : A → Bool) : ¬ (∀ x : A, P x) ↔ (∃ x : A, ¬ P x)
|
||||
:= calc (¬ ∀ x : A, P x) = ¬ ∀ x : A, ¬ ¬ P x : not_congr (allext (λ x : A, symm (not_not_eq (P x))))
|
||||
... = ∃ x : A, ¬ P x : refl (∃ x : A, ¬ P x)
|
||||
|
||||
theorem not_forall_elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x
|
||||
:= (not_forall A P) ◂ H
|
||||
|
||||
theorem not_exists (A : (Type U)) (P : A → Bool) : ¬ (∃ x : A, P x) ⟷ (∀ x : A, ¬ P x)
|
||||
theorem not_exists (A : (Type U)) (P : A → Bool) : ¬ (∃ x : A, P x) ↔ (∀ x : A, ¬ P x)
|
||||
:= calc (¬ ∃ x : A, P x) = ¬ ¬ ∀ x : A, ¬ P x : refl (¬ ∃ x : A, P x)
|
||||
... = ∀ x : A, ¬ P x : not_not_eq (∀ x : A, ¬ P x)
|
||||
|
||||
|
|
@ -378,7 +388,7 @@ theorem exists_unfold2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x
|
|||
(λ (w : A) (Hw : w ≠ a ∧ P w),
|
||||
exists_intro w (and_elimr Hw)))
|
||||
|
||||
theorem exists_unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) ⟷ (P a ∨ (∃ x : A, x ≠ a ∧ P x))
|
||||
theorem exists_unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) ↔ (P a ∨ (∃ x : A, x ≠ a ∧ P x))
|
||||
:= boolext (assume H : (∃ x : A, P x), exists_unfold1 a H)
|
||||
(assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists_unfold2 a H)
|
||||
|
||||
|
|
@ -390,10 +400,10 @@ theorem left_comm {A : TypeU} {R : A -> A -> A} (comm : ∀ x y, R x y = R y x)
|
|||
... = R (R y x) z : { comm x y }
|
||||
... = R y (R x z) : assoc y x z
|
||||
|
||||
theorem and_left_comm (a b c : Bool) : a ∧ (b ∧ c) ⟷ b ∧ (a ∧ c)
|
||||
theorem and_left_comm (a b c : Bool) : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c)
|
||||
:= left_comm and_comm and_assoc a b c
|
||||
|
||||
theorem or_left_comm (a b c : Bool) : a ∨ (b ∨ c) ⟷ b ∨ (a ∨ c)
|
||||
theorem or_left_comm (a b c : Bool) : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c)
|
||||
:= left_comm or_comm or_assoc a b c
|
||||
|
||||
-- Congruence theorems for contextual simplification
|
||||
|
|
@ -463,24 +473,24 @@ theorem imp_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = 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
|
||||
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
|
||||
theorem or_congrl {a b c d : Bool} (H_ac : ∀ (H_nd : ¬ d), a = c) (H_bd : ∀ (H_na : ¬ a), b = d) : a ∨ b ⟷ c ∨ d
|
||||
theorem or_congrl {a b c d : Bool} (H_ac : ∀ (H_nd : ¬ d), a = c) (H_bd : ∀ (H_na : ¬ a), b = d) : a ∨ b ↔ c ∨ d
|
||||
:= imp_congrl (λ H_nd : ¬ d, congr2 not (H_ac H_nd)) H_bd
|
||||
-- (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
|
||||
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
|
||||
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)))
|
||||
theorem and_congrl {a b c d : Bool} (H_ac : ∀ (H_d : d), a = c) (H_bd : ∀ (H_a : a), b = d) : a ∧ b ⟷ c ∧ d
|
||||
theorem and_congrl {a b c d : Bool} (H_ac : ∀ (H_d : d), a = c) (H_bd : ∀ (H_a : a), b = d) : a ∧ b ↔ c ∧ d
|
||||
:= congr2 not (imp_congrl (λ (H_nnd : ¬ ¬ d), H_ac (not_not_elim H_nnd)) (λ H_a : a, congr2 not (H_bd H_a)))
|
||||
-- (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
|
||||
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 forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) ⟷ p ∨ ∀ x, φ x
|
||||
theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) ↔ p ∨ ∀ x, φ x
|
||||
:= boolext
|
||||
(assume H : (∀ x, p ∨ φ x),
|
||||
or_elim (em p)
|
||||
|
|
@ -493,19 +503,19 @@ theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x,
|
|||
(λ H1 : p, or_introl H1 (φ x))
|
||||
(λ H2 : (∀ x, φ x), or_intror p (H2 x)))
|
||||
|
||||
theorem forall_or_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, φ x ∨ p) ⟷ (∀ x, φ x) ∨ p
|
||||
theorem forall_or_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, φ x ∨ p) ↔ (∀ x, φ x) ∨ p
|
||||
:= calc (∀ x, φ x ∨ p) = (∀ x, p ∨ φ x) : allext (λ x, or_comm (φ x) p)
|
||||
... = (p ∨ ∀ x, φ x) : forall_or_distributer p φ
|
||||
... = ((∀ x, φ x) ∨ p) : or_comm p (∀ x, φ x)
|
||||
|
||||
theorem forall_and_distribute {A : TypeU} (φ ψ : A → Bool) : (∀ x, φ x ∧ ψ x) ⟷ (∀ x, φ x) ∧ (∀ x, ψ x)
|
||||
theorem forall_and_distribute {A : TypeU} (φ ψ : A → Bool) : (∀ x, φ x ∧ ψ x) ↔ (∀ x, φ x) ∧ (∀ x, ψ x)
|
||||
:= boolext
|
||||
(assume H : (∀ x, φ x ∧ ψ x),
|
||||
and_intro (take x, and_eliml (H x)) (take x, and_elimr (H x)))
|
||||
(assume H : (∀ x, φ x) ∧ (∀ x, ψ x),
|
||||
take x, and_intro (and_eliml H x) (and_elimr H x))
|
||||
|
||||
theorem exists_and_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, p ∧ φ x) ⟷ p ∧ ∃ x, φ x
|
||||
theorem exists_and_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, p ∧ φ x) ↔ p ∧ ∃ x, φ x
|
||||
:= boolext
|
||||
(assume H : (∃ x, p ∧ φ x),
|
||||
obtain (w : A) (Hw : p ∧ φ w), from H,
|
||||
|
|
@ -514,12 +524,12 @@ theorem exists_and_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x
|
|||
obtain (w : A) (Hw : φ w), from (and_elimr H),
|
||||
exists_intro w (and_intro (and_eliml H) Hw))
|
||||
|
||||
theorem exists_and_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, φ x ∧ p) ⟷ (∃ x, φ x) ∧ p
|
||||
theorem exists_and_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, φ x ∧ p) ↔ (∃ x, φ x) ∧ p
|
||||
:= calc (∃ x, φ x ∧ p) = (∃ x, p ∧ φ x) : eq_exists_intro (λ x, and_comm (φ x) p)
|
||||
... = (p ∧ (∃ x, φ x)) : exists_and_distributer p φ
|
||||
... = ((∃ x, φ x) ∧ p) : and_comm p (∃ x, φ x)
|
||||
|
||||
theorem exists_or_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x ∨ ψ x) ⟷ (∃ x, φ x) ∨ (∃ x, ψ x)
|
||||
theorem exists_or_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x ∨ ψ x) ↔ (∃ x, φ x) ∨ (∃ x, ψ x)
|
||||
:= boolext
|
||||
(assume H : (∃ x, φ x ∨ ψ x),
|
||||
obtain (w : A) (Hw : φ w ∨ ψ w), from H,
|
||||
|
|
|
|||
Binary file not shown.
Binary file not shown.
|
|
@ -53,6 +53,9 @@ MK_CONSTANT(trans_fn, name("trans"));
|
|||
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(heq_congr_fn, name("heq_congr"));
|
||||
MK_CONSTANT(heq_congrl_fn, name("heq_congrl"));
|
||||
MK_CONSTANT(heq_congrr_fn, name("heq_congrr"));
|
||||
MK_CONSTANT(eqt_elim_fn, name("eqt_elim"));
|
||||
MK_CONSTANT(eqf_elim_fn, name("eqf_elim"));
|
||||
MK_CONSTANT(congr1_fn, name("congr1"));
|
||||
|
|
|
|||
|
|
@ -151,6 +151,15 @@ inline expr mk_eq_ne_trans_th(expr const & e1, expr const & e2, expr const & e3,
|
|||
expr mk_ne_eq_trans_fn();
|
||||
bool is_ne_eq_trans_fn(expr const & e);
|
||||
inline expr mk_ne_eq_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_ne_eq_trans_fn(), e1, e2, e3, e4, e5, e6}); }
|
||||
expr mk_heq_congr_fn();
|
||||
bool is_heq_congr_fn(expr const & e);
|
||||
inline expr mk_heq_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7) { return mk_app({mk_heq_congr_fn(), e1, e2, e3, e4, e5, e6, e7}); }
|
||||
expr mk_heq_congrl_fn();
|
||||
bool is_heq_congrl_fn(expr const & e);
|
||||
inline expr mk_heq_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_heq_congrl_fn(), e1, e2, e3, e4, e5}); }
|
||||
expr mk_heq_congrr_fn();
|
||||
bool is_heq_congrr_fn(expr const & e);
|
||||
inline expr mk_heq_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_heq_congrr_fn(), e1, e2, e3, e4, e5}); }
|
||||
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}); }
|
||||
|
|
|
|||
Loading…
Reference in a new issue