refactor(library/init): move more theorems to logic
This commit is contained in:
Leonardo de Moura
parent
d6c8e23b03
commit
477d79ae47
8 changed files with 79 additions and 71 deletions
|
|
@ -183,7 +183,7 @@ induction_on l
|
|||
|
||||
definition mem.is_decidable [instance] (H : decidable_eq T) (x : T) (l : list T) : decidable (x ∈ l) :=
|
||||
rec_on l
|
||||
(decidable.inr (iff.false_elim !mem.nil))
|
||||
(decidable.inr (not_of_iff_false !mem.nil))
|
||||
(take (h : T) (l : list T) (iH : decidable (x ∈ l)),
|
||||
show decidable (x ∈ h::l), from
|
||||
decidable.rec_on iH
|
||||
|
|
|
|||
|
|
@ -53,15 +53,18 @@ namespace eq
|
|||
notation H1 ▸ H2 := subst H1 H2
|
||||
end ops
|
||||
|
||||
variable {p : Prop}
|
||||
open ops
|
||||
end eq
|
||||
|
||||
theorem true_elim (H : p = true) : p :=
|
||||
section
|
||||
variable {p : Prop}
|
||||
open eq.ops
|
||||
|
||||
theorem of_eq_true (H : p = true) : p :=
|
||||
H⁻¹ ▸ trivial
|
||||
|
||||
theorem false_elim (H : p = false) : ¬p :=
|
||||
theorem not_of_eq_false (H : p = false) : ¬p :=
|
||||
assume Hp, H ▸ Hp
|
||||
end eq
|
||||
end
|
||||
|
||||
calc_subst eq.subst
|
||||
calc_refl eq.refl
|
||||
|
|
@ -140,11 +143,11 @@ namespace heq
|
|||
|
||||
theorem of_eq_of_heq (H₁ : a = a') (H₂ : a' == b) : a == b :=
|
||||
trans (of_eq H₁) H₂
|
||||
|
||||
theorem true_elim {a : Prop} (H : a == true) : a :=
|
||||
eq.true_elim (heq.to_eq H)
|
||||
end heq
|
||||
|
||||
theorem of_heq_true {a : Prop} (H : a == true) : a :=
|
||||
of_eq_true (heq.to_eq H)
|
||||
|
||||
calc_trans heq.trans
|
||||
calc_trans heq.of_heq_of_eq
|
||||
calc_trans heq.of_eq_of_heq
|
||||
|
|
@ -158,16 +161,8 @@ notation a ∧ b := and a b
|
|||
|
||||
variables {a b c d : Prop}
|
||||
|
||||
namespace and
|
||||
theorem elim (H₁ : a ∧ b) (H₂ : a → b → c) : c :=
|
||||
rec H₂ H₁
|
||||
|
||||
definition not_left (b : Prop) (Hna : ¬a) : ¬(a ∧ b) :=
|
||||
assume H : a ∧ b, absurd (elim_left H) Hna
|
||||
|
||||
definition not_right (a : Prop) {b : Prop} (Hnb : ¬b) : ¬(a ∧ b) :=
|
||||
assume H : a ∧ b, absurd (elim_right H) Hnb
|
||||
end and
|
||||
theorem and.elim (H₁ : a ∧ b) (H₂ : a → b → c) : c :=
|
||||
and.rec H₂ H₁
|
||||
|
||||
-- or
|
||||
-- --
|
||||
|
|
@ -183,11 +178,6 @@ namespace or
|
|||
|
||||
theorem elim (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → c) : c :=
|
||||
rec H₂ H₃ H₁
|
||||
|
||||
definition not_intro (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) :=
|
||||
assume H : a ∨ b, or.rec_on H
|
||||
(assume Ha, absurd Ha Hna)
|
||||
(assume Hb, absurd Hb Hnb)
|
||||
end or
|
||||
|
||||
-- iff
|
||||
|
|
@ -233,17 +223,17 @@ namespace iff
|
|||
(assume Hb, elim_right H Hb)
|
||||
(assume Ha, elim_left H Ha)
|
||||
|
||||
theorem true_elim (H : a ↔ true) : a :=
|
||||
mp (symm H) trivial
|
||||
|
||||
theorem false_elim (H : a ↔ false) : ¬a :=
|
||||
assume Ha : a, mp H Ha
|
||||
|
||||
open eq.ops
|
||||
theorem of_eq {a b : Prop} (H : a = b) : a ↔ b :=
|
||||
iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
|
||||
end iff
|
||||
|
||||
theorem of_iff_true (H : a ↔ true) : a :=
|
||||
iff.mp (iff.symm H) trivial
|
||||
|
||||
theorem not_of_iff_false (H : a ↔ false) : ¬a :=
|
||||
assume Ha : a, iff.mp H Ha
|
||||
|
||||
calc_refl iff.refl
|
||||
calc_trans iff.trans
|
||||
|
||||
|
|
@ -307,15 +297,15 @@ section
|
|||
rec_on Hp
|
||||
(assume Hp : p, rec_on Hq
|
||||
(assume Hq : q, inl (and.intro Hp Hq))
|
||||
(assume Hnq : ¬q, inr (and.not_right p Hnq)))
|
||||
(assume Hnp : ¬p, inr (and.not_left q Hnp))
|
||||
(assume Hnq : ¬q, inr (assume H : p ∧ q, and.rec_on H (assume Hp Hq, absurd Hq Hnq))))
|
||||
(assume Hnp : ¬p, inr (assume H : p ∧ q, and.rec_on H (assume Hp Hq, absurd Hp Hnp)))
|
||||
|
||||
definition or.decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p ∨ q) :=
|
||||
rec_on Hp
|
||||
(assume Hp : p, inl (or.inl Hp))
|
||||
(assume Hnp : ¬p, rec_on Hq
|
||||
(assume Hq : q, inl (or.inr Hq))
|
||||
(assume Hnq : ¬q, inr (or.not_intro Hnp Hnq)))
|
||||
(assume Hnq : ¬q, inr (assume H : p ∨ q, or.elim H (assume Hp, absurd Hp Hnp) (assume Hq, absurd Hq Hnq))))
|
||||
|
||||
definition not.decidable [instance] (Hp : decidable p) : decidable (¬p) :=
|
||||
rec_on Hp
|
||||
|
|
@ -390,32 +380,6 @@ decidable.rec
|
|||
(λ Hnc : ¬c, eq.refl (@ite c (decidable.inr Hnc) A t t))
|
||||
H
|
||||
|
||||
definition if_true {A : Type} (t e : A) : (if true then t else e) = t :=
|
||||
if_pos trivial
|
||||
|
||||
definition if_false {A : Type} (t e : A) : (if false then t else e) = e :=
|
||||
if_neg not_false
|
||||
|
||||
theorem if_cond_congr {c₁ c₂ : Prop} [H₁ : decidable c₁] [H₂ : decidable c₂] (Heq : c₁ ↔ c₂) {A : Type} (t e : A)
|
||||
: (if c₁ then t else e) = (if c₂ then t else e) :=
|
||||
decidable.rec_on H₁
|
||||
(λ Hc₁ : c₁, decidable.rec_on H₂
|
||||
(λ Hc₂ : c₂, if_pos Hc₁ ⬝ (if_pos Hc₂)⁻¹)
|
||||
(λ Hnc₂ : ¬c₂, absurd (iff.elim_left Heq Hc₁) Hnc₂))
|
||||
(λ Hnc₁ : ¬c₁, decidable.rec_on H₂
|
||||
(λ Hc₂ : c₂, absurd (iff.elim_right Heq Hc₂) Hnc₁)
|
||||
(λ Hnc₂ : ¬c₂, if_neg Hnc₁ ⬝ (if_neg Hnc₂)⁻¹))
|
||||
|
||||
theorem if_congr_aux {c₁ c₂ : Prop} [H₁ : decidable c₁] [H₂ : decidable c₂] {A : Type} {t₁ t₂ e₁ e₂ : A}
|
||||
(Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) :
|
||||
(if c₁ then t₁ else e₁) = (if c₂ then t₂ else e₂) :=
|
||||
Ht ▸ He ▸ (if_cond_congr Hc t₁ e₁)
|
||||
|
||||
theorem if_congr {c₁ c₂ : Prop} [H₁ : decidable c₁] {A : Type} {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) :
|
||||
(if c₁ then t₁ else e₁) = (@ite c₂ (decidable.decidable_iff_equiv H₁ Hc) A t₂ e₂) :=
|
||||
have H2 [visible] : decidable c₂, from (decidable.decidable_iff_equiv H₁ Hc),
|
||||
if_congr_aux Hc Ht He
|
||||
|
||||
-- We use "dependent" if-then-else to be able to communicate the if-then-else condition
|
||||
-- to the branches
|
||||
definition dite (c : Prop) [H : decidable c] {A : Type} (t : c → A) (e : ¬ c → A) : A :=
|
||||
|
|
|
|||
|
|
@ -23,8 +23,8 @@ cases P H1 H2 a
|
|||
-- this supercedes the em in decidable
|
||||
theorem em (a : Prop) : a ∨ ¬a :=
|
||||
or.elim (prop_complete a)
|
||||
(assume Ht : a = true, or.inl (eq.true_elim Ht))
|
||||
(assume Hf : a = false, or.inr (eq.false_elim Hf))
|
||||
(assume Ht : a = true, or.inl (of_eq_true Ht))
|
||||
(assume Hf : a = false, or.inr (not_of_eq_false Hf))
|
||||
|
||||
theorem prop_complete_swapped (a : Prop) : a = false ∨ a = true :=
|
||||
cases (λ x, x = false ∨ x = true)
|
||||
|
|
@ -36,9 +36,9 @@ theorem propext {a b : Prop} (Hab : a → b) (Hba : b → a) : a = b :=
|
|||
or.elim (prop_complete a)
|
||||
(assume Hat, or.elim (prop_complete b)
|
||||
(assume Hbt, Hat ⬝ Hbt⁻¹)
|
||||
(assume Hbf, false_elim (Hbf ▸ (Hab (eq.true_elim Hat)))))
|
||||
(assume Hbf, false_elim (Hbf ▸ (Hab (of_eq_true Hat)))))
|
||||
(assume Haf, or.elim (prop_complete b)
|
||||
(assume Hbt, false_elim (Haf ▸ (Hba (eq.true_elim Hbt))))
|
||||
(assume Hbt, false_elim (Haf ▸ (Hba (of_eq_true Hbt))))
|
||||
(assume Hbf, Haf ⬝ Hbf⁻¹))
|
||||
|
||||
theorem eq.of_iff {a b : Prop} (H : a ↔ b) : a = b :=
|
||||
|
|
|
|||
|
|
@ -39,6 +39,12 @@ assume not_em : ¬(a ∨ ¬a),
|
|||
-- ---
|
||||
|
||||
namespace and
|
||||
definition not_left (b : Prop) (Hna : ¬a) : ¬(a ∧ b) :=
|
||||
assume H : a ∧ b, absurd (elim_left H) Hna
|
||||
|
||||
definition not_right (a : Prop) {b : Prop} (Hnb : ¬b) : ¬(a ∧ b) :=
|
||||
assume H : a ∧ b, absurd (elim_right H) Hnb
|
||||
|
||||
theorem swap (H : a ∧ b) : b ∧ a :=
|
||||
intro (elim_right H) (elim_left H)
|
||||
|
||||
|
|
@ -68,6 +74,11 @@ end and
|
|||
-- --
|
||||
|
||||
namespace or
|
||||
definition not_intro (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) :=
|
||||
assume H : a ∨ b, or.rec_on H
|
||||
(assume Ha, absurd Ha Hna)
|
||||
(assume Hb, absurd Hb Hnb)
|
||||
|
||||
theorem imp_or (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → d) : c ∨ d :=
|
||||
elim H₁
|
||||
(assume Ha : a, inl (H₂ Ha))
|
||||
|
|
@ -136,3 +147,37 @@ theorem exists_unique_elim {A : Type} {p : A → Prop} {b : Prop}
|
|||
(H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, p y → y = x) → b) : b :=
|
||||
obtain w Hw, from H2,
|
||||
H1 w (and.elim_left Hw) (and.elim_right Hw)
|
||||
|
||||
-- if-then-else
|
||||
-- ------------
|
||||
section
|
||||
open eq.ops
|
||||
|
||||
variables {A : Type} {c₁ c₂ : Prop}
|
||||
|
||||
definition if_true (t e : A) : (if true then t else e) = t :=
|
||||
if_pos trivial
|
||||
|
||||
definition if_false (t e : A) : (if false then t else e) = e :=
|
||||
if_neg not_false
|
||||
|
||||
theorem if_cond_congr [H₁ : decidable c₁] [H₂ : decidable c₂] (Heq : c₁ ↔ c₂) (t e : A)
|
||||
: (if c₁ then t else e) = (if c₂ then t else e) :=
|
||||
decidable.rec_on H₁
|
||||
(λ Hc₁ : c₁, decidable.rec_on H₂
|
||||
(λ Hc₂ : c₂, if_pos Hc₁ ⬝ (if_pos Hc₂)⁻¹)
|
||||
(λ Hnc₂ : ¬c₂, absurd (iff.elim_left Heq Hc₁) Hnc₂))
|
||||
(λ Hnc₁ : ¬c₁, decidable.rec_on H₂
|
||||
(λ Hc₂ : c₂, absurd (iff.elim_right Heq Hc₂) Hnc₁)
|
||||
(λ Hnc₂ : ¬c₂, if_neg Hnc₁ ⬝ (if_neg Hnc₂)⁻¹))
|
||||
|
||||
theorem if_congr_aux [H₁ : decidable c₁] [H₂ : decidable c₂] {t₁ t₂ e₁ e₂ : A}
|
||||
(Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) :
|
||||
(if c₁ then t₁ else e₁) = (if c₂ then t₂ else e₂) :=
|
||||
Ht ▸ He ▸ (if_cond_congr Hc t₁ e₁)
|
||||
|
||||
theorem if_congr [H₁ : decidable c₁] {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) :
|
||||
(if c₁ then t₁ else e₁) = (@ite c₂ (decidable.decidable_iff_equiv H₁ Hc) A t₂ e₂) :=
|
||||
have H2 [visible] : decidable c₂, from (decidable.decidable_iff_equiv H₁ Hc),
|
||||
if_congr_aux Hc Ht He
|
||||
end
|
||||
|
|
|
|||
|
|
@ -143,7 +143,7 @@ theorem false_eq_true : (false ↔ true) ↔ false :=
|
|||
not_false_iff_true ▸ (a_iff_not_a false)
|
||||
|
||||
theorem a_eq_true (a : Prop) : (a ↔ true) ↔ a :=
|
||||
iff.intro (assume H, iff.true_elim H) (assume H, iff_true_intro H)
|
||||
iff.intro (assume H, of_iff_true H) (assume H, iff_true_intro H)
|
||||
|
||||
theorem a_eq_false (a : Prop) : (a ↔ false) ↔ ¬a :=
|
||||
iff.intro (assume H, iff.false_elim H) (assume H, iff_false_intro H)
|
||||
iff.intro (assume H, not_of_iff_false H) (assume H, iff_false_intro H)
|
||||
|
|
|
|||
|
|
@ -9,13 +9,12 @@ false.cases_on|Π (C : Type), false → C
|
|||
false.decidable|decidable false
|
||||
false.induction_on|∀ (C : Prop), false → C
|
||||
true_ne_false|¬ true = false
|
||||
eq.false_elim|?p = false → ¬ ?p
|
||||
not_of_is_false|is_false ?c → ¬ ?c
|
||||
not_of_iff_false|?a ↔ false → ¬ ?a
|
||||
p_ne_false|?p → ?p ≠ false
|
||||
is_false|Π (c : Prop) [H : decidable c], Prop
|
||||
not_of_eq_false|?p = false → ¬ ?p
|
||||
decidable.rec_on_false|Π (H3 : ¬ ?p), ?H2 H3 → decidable.rec_on ?H ?H1 ?H2
|
||||
not_false|¬ false
|
||||
of_not_is_false|¬ is_false ?c → ?c
|
||||
if_false|∀ (t e : ?A), ite false t e = e
|
||||
iff.false_elim|?a ↔ false → ¬ ?a
|
||||
-- ENDFINDP
|
||||
|
|
|
|||
|
|
@ -23,10 +23,10 @@ definition is_zero (x : nat)
|
|||
:= nat.rec true (λ n r, false) x
|
||||
|
||||
theorem is_zero_zero : is_zero zero
|
||||
:= eq.true_elim (refl _)
|
||||
:= of_eq_true (refl _)
|
||||
|
||||
theorem not_is_zero_succ (x : nat) : ¬ is_zero (succ x)
|
||||
:= eq.false_elim (refl _)
|
||||
:= not_of_eq_false (refl _)
|
||||
|
||||
theorem dichotomy (m : nat) : m = zero ∨ (∃ n, m = succ n)
|
||||
:= nat.rec
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@ definition is_nil {A : Type} (l : list A) : Prop
|
|||
:= list.rec true (fun h t r, false) l
|
||||
|
||||
theorem is_nil_nil (A : Type) : is_nil (@nil A)
|
||||
:= eq.true_elim (refl true)
|
||||
:= of_eq_true (refl true)
|
||||
|
||||
theorem cons_ne_nil {A : Type} (a : A) (l : list A) : ¬ cons a l = nil
|
||||
:= not_intro (assume H : cons a l = nil,
|
||||
|
|
|
|||
Loading…
Reference in a new issue