michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/doc/demo/kernel.lean

628 lines
25 KiB
Text
Raw Normal View History

doc(demo): add files for making demos Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-28 17:59:16 +00:00
import macros
universe U ≥ 1
definition TypeU := (Type U)
variable Bool : Type
-- The following builtin declarations can be removed as soon as Lean supports inductive datatypes and match expressions
builtin true : Bool
builtin false : Bool
definition not (a : Bool) := a → false
notation 40 ¬ _ : not
definition or (a b : Bool) := ¬ a → b
infixr 30 || : or
infixr 30 \/ : or
infixr 30 ∨ : or
definition and (a b : Bool) := ¬ (a → ¬ b)
infixr 35 && : and
infixr 35 /\ : and
infixr 35 ∧ : and
definition implies (a b : Bool) := a → b
builtin eq {A : (Type U)} (a b : A) : Bool
infix 50 = : eq
definition neq {A : TypeU} (a b : A) := ¬ (a = b)
infix 50 ≠ : neq
definition iff (a b : Bool) := a = b
infixr 25 <-> : iff
infixr 25 ↔ : iff
-- The Lean parser has special treatment for the constant exists.
-- It allows us to write
-- exists x y : A, P x y and ∃ x y : A, P x y
-- as syntax sugar for
-- exists A (fun x : A, exists A (fun y : A, P x y))
-- That is, it treats the exists as an extra binder such as fun and forall.
-- It also provides an alias (Exists) that should be used when we
-- want to treat exists as a constant.
definition Exists (A : TypeU) (P : A → Bool) := ¬ (∀ x, ¬ (P x))
definition nonempty (A : TypeU) := ∃ x : A, true
-- If we have an element of type A, then A is nonempty
theorem nonempty_intro {A : TypeU} (a : A) : nonempty A
:= assume H : (∀ x, ¬ true), (H a)
theorem em (a : Bool) : a ∨ ¬ a
:= assume Hna : ¬ a, Hna
axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
axiom refl {A : TypeU} (a : A) : a = a
axiom subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a = b) : P b
-- Function extensionality
axiom funext {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A, f x = g x) : f = g
-- Forall extensionality
axiom allext {A : TypeU} {B C : A → Bool} (H : ∀ x : A, B x = C x) : (∀ x : A, B x) = (∀ x : A, C x)
-- Epsilon (Hilbert's operator)
variable eps {A : TypeU} (H : nonempty A) (P : A → Bool) : A
alias ε : eps
axiom eps_ax {A : TypeU} (H : nonempty A) {P : A → Bool} (a : A) : P a → P (ε H P)
-- Proof irrelevance
axiom proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2
theorem eps_th {A : TypeU} {P : A → Bool} (a : A) : P a → P (ε (nonempty_intro a) P)
:= assume H : P a, @eps_ax A (nonempty_intro a) P a H
-- Alias for subst where we can provide P explicitly, but keep A,a,b implicit
theorem substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a = b) : P b
:= subst H1 H2
-- We will mark not as opaque later
theorem not_intro {a : Bool} (H : a → false) : ¬ a
:= H
theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
:= funext (λ x : A, refl (f x))
-- create default rewrite rule set
(* mk_rewrite_rule_set() *)
theorem trivial : true
:= refl true
theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false
:= H2 H1
theorem eqmp {a b : Bool} (H1 : a = b) (H2 : a) : b
:= subst H2 H1
infixl 100 <| : eqmp
infixl 100 ◂ : eqmp
theorem boolcomplete (a : Bool) : a = true ∨ a = false
:= case (λ x, x = true ∨ x = false) trivial trivial a
theorem false_elim (a : Bool) (H : false) : a
:= case (λ x, x) trivial H a
theorem imp_trans {a b c : Bool} (H1 : a → b) (H2 : b → c) : a → c
:= assume Ha, H2 (H1 Ha)
theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b = c) : a → c
:= assume Ha, H2 ◂ (H1 Ha)
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_elim {a : Bool} (H : ¬ ¬ a) : a
:= (not_not_eq a) ◂ H
theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬ b) : ¬ a
:= assume Ha : a, absurd (H1 Ha) H2
theorem contrapos {a b : Bool} (H : a → b) : ¬ b → ¬ a
:= assume Hnb : ¬ b, mt H Hnb
theorem absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b
:= false_elim b (absurd H1 H2)
theorem not_imp_eliml {a b : Bool} (Hnab : ¬ (a → b)) : a
:= not_not_elim
(have ¬ ¬ a :
assume Hna : ¬ a, absurd (assume Ha : a, absurd_elim b Ha Hna)
Hnab)
theorem not_imp_elimr {a b : Bool} (H : ¬ (a → b)) : ¬ b
:= assume Hb : b, absurd (assume Ha : a, Hb)
H
theorem resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b
:= H1 H2
-- 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)
-- 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
theorem or_intror {b : Bool} (a : Bool) (H : b) : a ∨ b
:= assume H1 : ¬ a, 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 (have c : H3 (have b : resolve1 H1 (have ¬ a : (mt (assume Ha : a, H2 Ha) H))))
H)
theorem refute {a : Bool} (H : ¬ a → false) : a
:= or_elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false_elim a (H H1))
theorem symm {A : TypeU} {a b : A} (H : a = b) : b = a
:= subst (refl a) H
theorem eqmpr {a b : Bool} (H1 : a = b) (H2 : b) : a
:= (symm H1) ◂ H2
theorem trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
:= subst H1 H2
theorem ne_symm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a
:= assume H1 : b = a, H (symm H1)
theorem eq_ne_trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c
:= subst H2 (symm H1)
theorem ne_eq_trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c
:= subst H1 H2
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 B : TypeU} {f g : A → B} (a : A) (H : f = g) : f a = g a
:= substp (fun h : A → B, f a = h a) (refl (f a)) H
theorem congr2 {A B : TypeU} {a b : A} (f : A → B) (H : a = b) : f a = f b
:= substp (fun x : A, f a = f x) (refl (f a)) H
theorem congr {A B : TypeU} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
:= subst (congr2 f H2) (congr1 b H1)
-- Recall that exists is defined as ¬ ∀ x : A, ¬ P x
theorem exists_elim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : ∀ (a : A) (H : P a), B) : B
:= refute (λ R : ¬ B,
absurd (take a : A, mt (assume H : P a, H2 a H) R)
H1)
theorem exists_intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P
:= assume H1 : (∀ x : A, ¬ P x),
absurd H (H1 a)
theorem nonempty_elim {A : TypeU} (H1 : nonempty A) {B : Bool} (H2 : A → B) : B
:= obtain (w : A) (Hw : true), from H1,
H2 w
theorem nonempty_ex_intro {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : nonempty A
:= obtain (w : A) (Hw : P w), from H,
exists_intro w trivial
theorem exists_to_eps {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : P (ε (nonempty_ex_intro H) P)
:= obtain (w : A) (Hw : P w), from H,
eps_ax (nonempty_ex_intro H) w Hw
theorem axiom_of_choice {A : TypeU} {B : A → TypeU} {R : ∀ x : A, B x → Bool} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x)
:= exists_intro
(λ x, ε (nonempty_ex_intro (H x)) (λ y, R x y)) -- witness for f
(λ x, exists_to_eps (H x)) -- proof that witness satisfies ∀ x, R x (f x)
theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b
:= or_elim (boolcomplete a)
(λ Hat : a = true, or_elim (boolcomplete b)
(λ Hbt : b = true, trans Hat (symm Hbt))
(λ Hbf : b = false, false_elim (a = b) (subst (Hab (eqt_elim Hat)) Hbf)))
(λ Haf : a = false, or_elim (boolcomplete b)
(λ Hbt : b = true, false_elim (a = b) (subst (Hba (eqt_elim Hbt)) Haf))
(λ Hbf : b = false, trans Haf (symm Hbf)))
theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a ↔ b
:= boolext Hab Hba
theorem iff_eliml {a b : Bool} (H : a ↔ b) : a → b
:= (λ Ha : a, eqmp H Ha)
theorem iff_elimr {a b : Bool} (H : a ↔ b) : b → a
:= (λ Hb : b, eqmpr H Hb)
theorem skolem_th {A : TypeU} {B : A → TypeU} {P : ∀ x : A, B x → Bool} :
(∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x))
:= iff_intro
(λ H : (∀ x, ∃ y, P x y), axiom_of_choice H)
(λ H : (∃ f, (∀ x, P x (f x))),
take x, obtain (fw : ∀ x, B x) (Hw : ∀ x, P x (fw x)), from H,
exists_intro (fw x) (Hw x))
theorem eqt_intro {a : Bool} (H : a) : a = true
:= boolext (assume H1 : a, trivial)
(assume H2 : true, H)
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
:= eqf_intro H
theorem eq_id {A : TypeU} (a : A) : (a = a) ↔ true
:= eqt_intro (refl a)
theorem iff_id (a : Bool) : (a ↔ a) ↔ true
:= eqt_intro (refl 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)
:= 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)))
(λ Hc : c, or_intror a (or_intror b Hc)))
(assume H : a ∨ (b ∨ c),
or_elim H (λ Ha : a, (or_introl (or_introl Ha 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
:= boolext (assume H, or_elim H (λ H1, H1) (λ H2, H2))
(assume H, or_introl H 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
:= trans (or_comm false a) (or_falsel a)
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
:= trans (or_comm a true) (or_truel a)
theorem or_tauto (a : Bool) : a ∨ ¬ a ↔ true
:= eqt_intro (em 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
:= 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)
:= 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
:= boolext (assume H : a ∧ true, and_eliml H)
(assume H : a, and_intro H trivial)
theorem and_truel (a : Bool) : true ∧ a ↔ a
:= trans (and_comm true a) (and_truer a)
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
:= trans (and_comm false a) (and_falsel a)
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_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 imp_or (a b : Bool) : (a → b) ↔ ¬ a ∨ b
:= iff_intro
(assume H : a → b,
(or_elim (em a)
(λ Ha : a, or_intror (¬ a) (H Ha))
(λ Hna : ¬ a, or_introl Hna b)))
(assume H : ¬ a ∨ b,
assume Ha : a,
resolve1 H ((symm (not_not_eq a)) ◂ Ha))
theorem not_true : ¬ true ↔ false
:= trivial
theorem not_false : ¬ false ↔ true
:= trivial
theorem not_neq {A : TypeU} (a b : A) : ¬ (a ≠ b) ↔ a = b
:= not_not_eq (a = b)
theorem not_neq_elim {A : TypeU} {a b : A} (H : ¬ (a ≠ b)) : a = b
:= (not_neq a b) ◂ H
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)
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)
a
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)
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
:= congr2 not H
theorem exists_rem {A : TypeU} (H : nonempty A) (p : Bool) : (∃ x : A, p) ↔ p
:= iff_intro
(assume Hl : (∃ x : A, p),
obtain (w : A) (Hw : p), from Hl,
Hw)
(assume Hr : p,
nonempty_elim H (λ w, exists_intro w Hr))
theorem forall_rem {A : TypeU} (H : nonempty A) (p : Bool) : (∀ x : A, p) ↔ p
:= iff_intro
(assume Hl : (∀ x : A, p),
nonempty_elim H (λ w, Hl w))
(assume Hr : p,
take x, Hr)
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)
:= 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)
:= 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)
theorem not_exists_elim {A : (Type U)} {P : A → Bool} (H : ¬ ∃ x : A, P x) : ∀ x : A, ¬ P x
:= (not_exists A P) ◂ H
theorem exists_unfold1 {A : TypeU} {P : A → Bool} (a : A) (H : ∃ x : A, P x) : P a ∨ (∃ x : A, x ≠ a ∧ P x)
:= exists_elim H
(λ (w : A) (H1 : P w),
or_elim (em (w = a))
(λ Heq : w = a, or_introl (subst H1 Heq) (∃ x : A, x ≠ a ∧ P x))
(λ Hne : w ≠ a, or_intror (P a) (exists_intro w (and_intro Hne H1))))
theorem exists_unfold2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x : A, x ≠ a ∧ P x)) : ∃ x : A, P x
:= or_elim H
(λ H1 : P a, exists_intro a H1)
(λ H2 : (∃ x : A, x ≠ a ∧ P x),
exists_elim H2
(λ (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))
:= 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)
-- Remark: ordered rewriting + assoc + comm + left_comm sorts a term lexicographically
theorem left_comm {A : TypeU} {R : A -> A -> A} (comm : ∀ x y, R x y = R y x) (assoc : ∀ x y z, R (R x y) z = R x (R y z)) :
∀ x y z, R x (R y z) = R y (R x z)
:= take x y z, calc R x (R y z) = R (R x y) z : symm (assoc x y z)
... = 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)
:= left_comm and_comm and_assoc a b 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
-- Simplify a → b, by first simplifying a to c using the fact that ¬ b is true, and then
-- b to d using the fact that c is true
theorem imp_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_c : c), b = d) : (a → b) = (c → d)
:= or_elim (em b)
(λ H_b : b,
or_elim (em c)
(λ H_c : c,
calc (a → b) = (a → true) : { eqt_intro H_b }
... = true : imp_truer a
... = (c → true) : symm (imp_truer c)
... = (c → b) : { symm (eqt_intro H_b) }
... = (c → d) : { H_bd H_c })
(λ H_nc : ¬ c,
calc (a → b) = (a → true) : { eqt_intro H_b }
... = true : imp_truer a
... = (false → d) : symm (imp_falsel d)
... = (c → d) : { symm (eqf_intro H_nc) }))
(λ H_nb : ¬ b,
or_elim (em c)
(λ H_c : c,
calc (a → b) = (c → b) : { H_ac H_nb }
... = (c → d) : { H_bd H_c })
(λ H_nc : ¬ c,
calc (a → b) = (c → b) : { H_ac H_nb }
... = (false → b) : { eqf_intro H_nc }
... = true : imp_falsel b
... = (false → d) : symm (imp_falsel d)
... = (c → d) : { symm (eqf_intro H_nc) }))
-- Simplify a → b, by first simplifying b to d using the fact that a is true, and then
-- b to d using the fact that ¬ d is true.
-- This kind of congruence seems to be useful in very rare cases.
theorem imp_congrl {a b c d : Bool} (H_bd : ∀ (H_a : a), b = d) (H_ac : ∀ (H_nd : ¬ d), a = c) : (a → b) = (c → d)
:= or_elim (em a)
(λ H_a : a,
or_elim (em d)
(λ H_d : d,
calc (a → b) = (a → d) : { H_bd H_a }
... = (a → true) : { eqt_intro H_d }
... = true : imp_truer a
... = (c → true) : symm (imp_truer c)
... = (c → d) : { symm (eqt_intro H_d) })
(λ H_nd : ¬ d,
calc (a → b) = (c → b) : { H_ac H_nd }
... = (c → d) : { H_bd H_a }))
(λ H_na : ¬ a,
or_elim (em d)
(λ H_d : d,
calc (a → b) = (false → b) : { eqf_intro H_na }
... = true : imp_falsel b
... = (c → true) : symm (imp_truer c)
... = (c → d) : { symm (eqt_intro H_d) })
(λ H_nd : ¬ d,
calc (a → b) = (false → b) : { eqf_intro H_na }
... = true : imp_falsel b
... = (false → d) : symm (imp_falsel d)
... = (a → d) : { symm (eqf_intro H_na) }
... = (c → d) : { H_ac H_nd }))
-- (Common case) simplify a to c, and then b to d using the fact that c is true
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
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))
-- (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)))
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)))
-- (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 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)
(λ Hp : p, or_introl Hp (∀ x, φ x))
(λ Hnp : ¬ p, or_intror p (take x,
resolve1 (H x) Hnp)))
(assume H : (p ∨ ∀ x, φ x),
take x,
or_elim H
(λ H1 : p, or_introl H1 (φ x))
(λ H2 : (∀ x, φ x), or_intror p (H2 x)))
theorem forall_or_distributel {A : Type} (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)
:= 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
:= boolext
(assume H : (∃ x, p ∧ φ x),
obtain (w : A) (Hw : p ∧ φ w), from H,
and_intro (and_eliml Hw) (exists_intro w (and_elimr Hw)))
(assume H : (p ∧ ∃ x, φ 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
:= 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)
:= boolext
(assume H : (∃ x, φ x ∨ ψ x),
obtain (w : A) (Hw : φ w ∨ ψ w), from H,
or_elim Hw
(λ Hw1 : φ w, or_introl (exists_intro w Hw1) (∃ x, ψ x))
(λ Hw2 : ψ w, or_intror (∃ x, φ x) (exists_intro w Hw2)))
(assume H : (∃ x, φ x) ∨ (∃ x, ψ x),
or_elim H
(λ H1 : (∃ x, φ x),
obtain (w : A) (Hw : φ w), from H1,
exists_intro w (or_introl Hw (ψ w)))
(λ H2 : (∃ x, ψ x),
obtain (w : A) (Hw : ψ w), from H2,
exists_intro w (or_intror (φ w) Hw)))
theorem exists_imp_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x → ψ x) ↔ ((∀ x, φ x) → (∃ x, ψ x))
:= calc (∃ x, φ x → ψ x) = (∃ x, ¬ φ x ∨ ψ x) : eq_exists_intro (λ x, imp_or (φ x) (ψ x))
... = (∃ x, ¬ φ x) ∨ (∃ x, ψ x) : exists_or_distribute _ _
... = ¬ (∀ x, φ x) ∨ (∃ x, ψ x) : { symm (not_forall A φ) }
... = (∀ x, φ x) → (∃ x, ψ x) : symm (imp_or _ _)
set_opaque exists true
set_opaque not true
set_opaque or true
set_opaque and true
set_opaque implies true
Reference in a new issue Copy permalink