michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/data/bool): use new style

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-05 09:50:55 -07:00
parent 60d8369688
commit 317e910054
4 changed files with 72 additions and 72 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

84
library/data/bool.lean
View file

@ -22,115 +22,115 @@ namespace bool
theorem dichotomy (b : bool) : b = ff ∨ b = tt := theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
cases_on b (or.inl rfl) (or.inr rfl) cases_on b (or.inl rfl) (or.inr rfl)
theorem cond_ff {A : Type} (t e : A) : cond ff t e = e := theorem cond.ff {A : Type} (t e : A) : cond ff t e = e :=
rfl rfl
theorem cond_tt {A : Type} (t e : A) : cond tt t e = t := theorem cond.tt {A : Type} (t e : A) : cond tt t e = t :=
rfl rfl
theorem ff_ne_tt : ¬ ff = tt := theorem ff_ne_tt : ¬ ff = tt :=
assume H : ff = tt, absurd assume H : ff = tt, absurd
(calc true = cond tt true false : (cond_tt _ _)⁻¹ (calc true = cond tt true false : !cond.tt⁻¹
... = cond ff true false : {H⁻¹} ... = cond ff true false : {H⁻¹}
... = false : cond_ff _ _) ... = false : !cond.ff)
true_ne_false true_ne_false
definition or (a b : bool) := definition bor (a b : bool) :=
rec_on a (rec_on b ff tt) tt rec_on a (rec_on b ff tt) tt
theorem or_tt_left (a : bool) : or tt a = tt := theorem bor.tt_left (a : bool) : bor tt a = tt :=
rfl rfl
infixl `||` := or infixl `||` := bor
theorem or_tt_right (a : bool) : a || tt = tt := theorem bor.tt_right (a : bool) : a || tt = tt :=
cases_on a rfl rfl cases_on a rfl rfl
theorem or_ff_left (a : bool) : ff || a = a := theorem bor.ff_left (a : bool) : ff || a = a :=
cases_on a rfl rfl cases_on a rfl rfl
theorem or_ff_right (a : bool) : a || ff = a := theorem bor.ff_right (a : bool) : a || ff = a :=
cases_on a rfl rfl cases_on a rfl rfl
theorem or_id (a : bool) : a || a = a := theorem bor.id (a : bool) : a || a = a :=
cases_on a rfl rfl cases_on a rfl rfl
theorem or_comm (a b : bool) : a || b = b || a := theorem bor.comm (a b : bool) : a || b = b || a :=
cases_on a cases_on a
(cases_on b rfl rfl) (cases_on b rfl rfl)
(cases_on b rfl rfl) (cases_on b rfl rfl)
theorem or_assoc (a b c : bool) : (a || b) || c = a || (b || c) := theorem bor.assoc (a b c : bool) : (a || b) || c = a || (b || c) :=
cases_on a cases_on a
(calc (ff || b) || c = b || c : {or_ff_left b} (calc (ff || b) || c = b || c : {!bor.ff_left}
... = ff || (b || c) : or_ff_left (b || c)⁻¹) ... = ff || (b || c) : !bor.ff_left⁻¹)
(calc (tt || b) || c = tt || c : {or_tt_left b} (calc (tt || b) || c = tt || c : {!bor.tt_left}
... = tt : or_tt_left c ... = tt : !bor.tt_left
... = tt || (b || c) : or_tt_left (b || c)⁻¹) ... = tt || (b || c) : !bor.tt_left⁻¹)
theorem or_to_or {a b : bool} : a || b = tt → a = tt ∨ b = tt := theorem bor.to_or {a b : bool} : a || b = tt → a = tt ∨ b = tt :=
rec_on a rec_on a
(assume H : ff || b = tt, (assume H : ff || b = tt,
have Hb : b = tt, from (or_ff_left b) ▸ H, have Hb : b = tt, from !bor.ff_left ▸ H,
or.inr Hb) or.inr Hb)
(assume H, or.inl rfl) (assume H, or.inl rfl)
definition and (a b : bool) := definition band (a b : bool) :=
rec_on a ff (rec_on b ff tt) rec_on a ff (rec_on b ff tt)
infixl `&&` := and infixl `&&` := band
theorem and_ff_left (a : bool) : ff && a = ff := theorem band.ff_left (a : bool) : ff && a = ff :=
rfl rfl
theorem and_tt_left (a : bool) : tt && a = a := theorem band.tt_left (a : bool) : tt && a = a :=
cases_on a rfl rfl cases_on a rfl rfl
theorem and_ff_right (a : bool) : a && ff = ff := theorem band.ff_right (a : bool) : a && ff = ff :=
cases_on a rfl rfl cases_on a rfl rfl
theorem and_tt_right (a : bool) : a && tt = a := theorem band.tt_right (a : bool) : a && tt = a :=
cases_on a rfl rfl cases_on a rfl rfl
theorem and_id (a : bool) : a && a = a := theorem band.id (a : bool) : a && a = a :=
cases_on a rfl rfl cases_on a rfl rfl
theorem and_comm (a b : bool) : a && b = b && a := theorem band.comm (a b : bool) : a && b = b && a :=
cases_on a cases_on a
(cases_on b rfl rfl) (cases_on b rfl rfl)
(cases_on b rfl rfl) (cases_on b rfl rfl)
theorem and_assoc (a b c : bool) : (a && b) && c = a && (b && c) := theorem band.assoc (a b c : bool) : (a && b) && c = a && (b && c) :=
cases_on a cases_on a
(calc (ff && b) && c = ff && c : {and_ff_left b} (calc (ff && b) && c = ff && c : {!band.ff_left}
... = ff : and_ff_left c ... = ff : !band.ff_left
... = ff && (b && c) : and_ff_left (b && c)⁻¹) ... = ff && (b && c) : !band.ff_left⁻¹)
(calc (tt && b) && c = b && c : {and_tt_left b} (calc (tt && b) && c = b && c : {!band.tt_left}
... = tt && (b && c) : and_tt_left (b && c)⁻¹) ... = tt && (b && c) : !band.tt_left⁻¹)
theorem and_eq_tt_elim_left {a b : bool} (H : a && b = tt) : a = tt := theorem band.eq_tt_elim_left {a b : bool} (H : a && b = tt) : a = tt :=
or.elim (dichotomy a) or.elim (dichotomy a)
(assume H0 : a = ff, (assume H0 : a = ff,
absurd absurd
(calc ff = ff && b : (and_ff_left _)⁻¹ (calc ff = ff && b : !band.ff_left⁻¹
... = a && b : {H0⁻¹} ... = a && b : {H0⁻¹}
... = tt : H) ... = tt : H)
ff_ne_tt) ff_ne_tt)
(assume H1 : a = tt, H1) (assume H1 : a = tt, H1)
theorem and_eq_tt_elim_right {a b : bool} (H : a && b = tt) : b = tt := theorem band.eq_tt_elim_right {a b : bool} (H : a && b = tt) : b = tt :=
and_eq_tt_elim_left (and_comm b a ⬝ H) band.eq_tt_elim_left (!band.comm ⬝ H)
definition not (a : bool) := definition bnot (a : bool) :=
rec_on a tt ff rec_on a tt ff
theorem bnot_bnot (a : bool) : not (not a) = a := theorem bnot.bnot (a : bool) : bnot (bnot a) = a :=
cases_on a rfl rfl cases_on a rfl rfl
theorem bnot_false : not ff = tt := theorem bnot.false : bnot ff = tt :=
rfl rfl
theorem bnot_true : not tt = ff := theorem bnot.true : bnot tt = ff :=
rfl rfl
protected definition is_inhabited [instance] : inhabited bool := protected definition is_inhabited [instance] : inhabited bool :=

2
library/data/num.lean
View file

@ -148,7 +148,7 @@ namespace num
(λp, calc (λp, calc
pred (succ (pos p)) = pred (pos (pos_num.succ p)) : rfl pred (succ (pos p)) = pred (pos (pos_num.succ p)) : rfl
... = cond ff zero (pos (pos_num.pred (pos_num.succ p))) : {succ_not_is_one} ... = cond ff zero (pos (pos_num.pred (pos_num.succ p))) : {succ_not_is_one}
... = pos (pos_num.pred (pos_num.succ p)) : cond_ff _ _ ... = pos (pos_num.pred (pos_num.succ p)) : !cond.ff
... = pos p : {pos_num.pred_succ}) ... = pos p : {pos_num.pred_succ})
definition add (a b : num) : num := definition add (a b : num) : num :=

30
library/data/set.lean
View file

@ -45,26 +45,26 @@ infixl `∩` := inter
theorem mem_inter {T : Type} (x : T) (A B : set T) : x ∈ A ∩ B ↔ (x ∈ A ∧ x ∈ B) := theorem mem_inter {T : Type} (x : T) (A B : set T) : x ∈ A ∩ B ↔ (x ∈ A ∧ x ∈ B) :=
iff.intro iff.intro
(assume H, and.intro (and_eq_tt_elim_left H) (and_eq_tt_elim_right H)) (assume H, and.intro (band.eq_tt_elim_left H) (band.eq_tt_elim_right H))
(assume H, (assume H,
have e1 : A x = tt, from and.elim_left H, have e1 : A x = tt, from and.elim_left H,
have e2 : B x = tt, from and.elim_right H, have e2 : B x = tt, from and.elim_right H,
show A x && B x = tt, from e1⁻¹ ▸ e2⁻¹ ▸ and_tt_left tt) show A x && B x = tt, from e1⁻¹ ▸ e2⁻¹ ▸ band.tt_left tt)
theorem inter_id {T : Type} (A : set T) : A ∩ A ∼ A := theorem inter_id {T : Type} (A : set T) : A ∩ A ∼ A :=
take x, and_id (A x) ▸ iff.rfl take x, band.id (A x) ▸ iff.rfl
theorem inter_empty_right {T : Type} (A : set T) : A ∩ ∅ ∼ ∅ := theorem inter_empty_right {T : Type} (A : set T) : A ∩ ∅ ∼ ∅ :=
take x, and_ff_right (A x) ▸ iff.rfl take x, band.ff_right (A x) ▸ iff.rfl
theorem inter_empty_left {T : Type} (A : set T) : ∅ ∩ A ∼ ∅ := theorem inter_empty_left {T : Type} (A : set T) : ∅ ∩ A ∼ ∅ :=
take x, and_ff_left (A x) ▸ iff.rfl take x, band.ff_left (A x) ▸ iff.rfl
theorem inter_comm {T : Type} (A B : set T) : A ∩ B ∼ B ∩ A := theorem inter_comm {T : Type} (A B : set T) : A ∩ B ∼ B ∩ A :=
take x, and_comm (A x) (B x) ▸ iff.rfl take x, band.comm (A x) (B x) ▸ iff.rfl
theorem inter_assoc {T : Type} (A B C : set T) : (A ∩ B) ∩ C ∼ A ∩ (B ∩ C) := theorem inter_assoc {T : Type} (A B C : set T) : (A ∩ B) ∩ C ∼ A ∩ (B ∩ C) :=
take x, and_assoc (A x) (B x) (C x) ▸ iff.rfl take x, band.assoc (A x) (B x) (C x) ▸ iff.rfl
definition union {T : Type} (A B : set T) : set T := definition union {T : Type} (A B : set T) : set T :=
λx, A x || B x λx, A x || B x
@ -72,26 +72,26 @@ infixl `∪` := union
theorem mem_union {T : Type} (x : T) (A B : set T) : x ∈ A ∪ B ↔ (x ∈ A ∨ x ∈ B) := theorem mem_union {T : Type} (x : T) (A B : set T) : x ∈ A ∪ B ↔ (x ∈ A ∨ x ∈ B) :=
iff.intro iff.intro
(assume H, or_to_or H) (assume H, bor.to_or H)
(assume H, or.elim H (assume H, or.elim H
(assume Ha : A x = tt, (assume Ha : A x = tt,
show A x || B x = tt, from Ha⁻¹ ▸ or_tt_left (B x)) show A x || B x = tt, from Ha⁻¹ ▸ bor.tt_left (B x))
(assume Hb : B x = tt, (assume Hb : B x = tt,
show A x || B x = tt, from Hb⁻¹ ▸ or_tt_right (A x))) show A x || B x = tt, from Hb⁻¹ ▸ bor.tt_right (A x)))
theorem union_id {T : Type} (A : set T) : A ∪ A ∼ A := theorem union_id {T : Type} (A : set T) : A ∪ A ∼ A :=
take x, or_id (A x) ▸ iff.rfl take x, bor.id (A x) ▸ iff.rfl
theorem union_empty_right {T : Type} (A : set T) : A ∪ ∅ ∼ A := theorem union_empty_right {T : Type} (A : set T) : A ∪ ∅ ∼ A :=
take x, or_ff_right (A x) ▸ iff.rfl take x, bor.ff_right (A x) ▸ iff.rfl
theorem union_empty_left {T : Type} (A : set T) : ∅ ∪ A ∼ A := theorem union_empty_left {T : Type} (A : set T) : ∅ ∪ A ∼ A :=
take x, or_ff_left (A x) ▸ iff.rfl take x, bor.ff_left (A x) ▸ iff.rfl
theorem union_comm {T : Type} (A B : set T) : A ∪ B ∼ B ∪ A := theorem union_comm {T : Type} (A B : set T) : A ∪ B ∼ B ∪ A :=
take x, or_comm (A x) (B x) ▸ iff.rfl take x, bor.comm (A x) (B x) ▸ iff.rfl
theorem union_assoc {T : Type} (A B C : set T) : (A ∪ B) ∪ C ∼ A ∪ (B ∪ C) := theorem union_assoc {T : Type} (A B C : set T) : (A ∪ B) ∪ C ∼ A ∪ (B ∪ C) :=
take x, or_assoc (A x) (B x) (C x) ▸ iff.rfl take x, bor.assoc (A x) (B x) (C x) ▸ iff.rfl
end set end set

28
tests/lean/interactive/alias.input.expected.out
View file

@ -3,26 +3,26 @@
-- BEGINWAIT -- BEGINWAIT
-- ENDWAIT -- ENDWAIT
-- BEGINFINDP -- BEGINFINDP
bool.and_tt_left|∀ (a : bool), eq (bool.and bool.tt a) a bool.band.tt_left|∀ (a : bool), eq (bool.band bool.tt a) a
bool.and_tt_right|∀ (a : bool), eq (bool.and a bool.tt) a
bool.tt|bool bool.tt|bool
bool.or_tt_left|∀ (a : bool), eq (bool.or bool.tt a) bool.tt bool.band.eq_tt_elim_right|eq (bool.band ?a ?b) bool.tt → eq ?b bool.tt
bool.and_eq_tt_elim_left|eq (bool.and ?a ?b) bool.tt → eq ?a bool.tt bool.band.eq_tt_elim_left|eq (bool.band ?a ?b) bool.tt → eq ?a bool.tt
bool.and_eq_tt_elim_right|eq (bool.and ?a ?b) bool.tt → eq ?b bool.tt bool.band.tt_right|∀ (a : bool), eq (bool.band a bool.tt) a
bool.cond_tt|∀ (t e : ?A), eq (bool.cond bool.tt t e) t bool.bor.tt_right|∀ (a : bool), eq (bool.bor a bool.tt) bool.tt
bool.or_tt_right|∀ (a : bool), eq (bool.or a bool.tt) bool.tt bool.bor.tt_left|∀ (a : bool), eq (bool.bor bool.tt a) bool.tt
bool.ff_ne_tt|not (eq bool.ff bool.tt) bool.ff_ne_tt|not (eq bool.ff bool.tt)
bool.cond.tt|∀ (t e : ?A), eq (bool.cond bool.tt t e) t
-- ENDFINDP -- ENDFINDP
-- BEGINWAIT -- BEGINWAIT
-- ENDWAIT -- ENDWAIT
-- BEGINFINDP -- BEGINFINDP
tt|bool tt|bool
and_tt_left|∀ (a : bool), eq (and tt a) a band.tt_left|∀ (a : bool), eq (band tt a) a
and_tt_right|∀ (a : bool), eq (and a tt) a band.eq_tt_elim_right|eq (band ?a ?b) tt → eq ?b tt
or_tt_left|∀ (a : bool), eq (or tt a) tt band.eq_tt_elim_left|eq (band ?a ?b) tt → eq ?a tt
and_eq_tt_elim_left|eq (and ?a ?b) tt → eq ?a tt band.tt_right|∀ (a : bool), eq (band a tt) a
and_eq_tt_elim_right|eq (and ?a ?b) tt → eq ?b tt bor.tt_right|∀ (a : bool), eq (bor a tt) tt
cond_tt|∀ (t e : ?A), eq (cond tt t e) t bor.tt_left|∀ (a : bool), eq (bor tt a) tt
or_tt_right|∀ (a : bool), eq (or a tt) tt
ff_ne_tt|not (eq ff tt) ff_ne_tt|not (eq ff tt)
cond.tt|∀ (t e : ?A), eq (cond tt t e) t
-- ENDFINDP -- ENDFINDP