From 317e9100540013d5cff24baaf926f7f4ceb42f6e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 5 Oct 2014 09:50:55 -0700 Subject: [PATCH] refactor(library/data/bool): use new style --- library/data/bool.lean | 84 +++++++++---------- library/data/num.lean | 2 +- library/data/set.lean | 30 +++---- .../lean/interactive/alias.input.expected.out | 28 +++---- 4 files changed, 72 insertions(+), 72 deletions(-) diff --git a/library/data/bool.lean b/library/data/bool.lean index 1b5fb5eb0..c714ccf91 100644 --- a/library/data/bool.lean +++ b/library/data/bool.lean @@ -22,115 +22,115 @@ namespace bool theorem dichotomy (b : bool) : b = ff ∨ b = tt := 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 - 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 theorem ff_ne_tt : ¬ ff = tt := 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⁻¹} - ... = false : cond_ff _ _) + ... = false : !cond.ff) true_ne_false - definition or (a b : bool) := + definition bor (a b : bool) := 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 - 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 - theorem or_ff_left (a : bool) : ff || a = a := + theorem bor.ff_left (a : bool) : ff || a = a := 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 - theorem or_id (a : bool) : a || a = a := + theorem bor.id (a : bool) : a || a = a := 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 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 - (calc (ff || b) || c = b || c : {or_ff_left b} - ... = ff || (b || c) : or_ff_left (b || c)⁻¹) - (calc (tt || b) || c = tt || c : {or_tt_left b} - ... = tt : or_tt_left c - ... = tt || (b || c) : or_tt_left (b || c)⁻¹) + (calc (ff || b) || c = b || c : {!bor.ff_left} + ... = ff || (b || c) : !bor.ff_left⁻¹) + (calc (tt || b) || c = tt || c : {!bor.tt_left} + ... = tt : !bor.tt_left + ... = 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 (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) (assume H, or.inl rfl) - definition and (a b : bool) := + definition band (a b : bool) := 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 - theorem and_tt_left (a : bool) : tt && a = a := + theorem band.tt_left (a : bool) : tt && a = a := 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 - theorem and_tt_right (a : bool) : a && tt = a := + theorem band.tt_right (a : bool) : a && tt = a := 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 - 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 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 - (calc (ff && b) && c = ff && c : {and_ff_left b} - ... = ff : and_ff_left c - ... = ff && (b && c) : and_ff_left (b && c)⁻¹) - (calc (tt && b) && c = b && c : {and_tt_left b} - ... = tt && (b && c) : and_tt_left (b && c)⁻¹) + (calc (ff && b) && c = ff && c : {!band.ff_left} + ... = ff : !band.ff_left + ... = ff && (b && c) : !band.ff_left⁻¹) + (calc (tt && b) && c = b && c : {!band.tt_left} + ... = 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) (assume H0 : a = ff, absurd - (calc ff = ff && b : (and_ff_left _)⁻¹ + (calc ff = ff && b : !band.ff_left⁻¹ ... = a && b : {H0⁻¹} ... = tt : H) ff_ne_tt) (assume H1 : a = tt, H1) - theorem and_eq_tt_elim_right {a b : bool} (H : a && b = tt) : b = tt := - and_eq_tt_elim_left (and_comm b a ⬝ H) + theorem band.eq_tt_elim_right {a b : bool} (H : a && b = tt) : b = tt := + band.eq_tt_elim_left (!band.comm ⬝ H) - definition not (a : bool) := + definition bnot (a : bool) := 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 - theorem bnot_false : not ff = tt := + theorem bnot.false : bnot ff = tt := rfl - theorem bnot_true : not tt = ff := + theorem bnot.true : bnot tt = ff := rfl protected definition is_inhabited [instance] : inhabited bool := diff --git a/library/data/num.lean b/library/data/num.lean index 961c4fc05..f12ade6d5 100644 --- a/library/data/num.lean +++ b/library/data/num.lean @@ -148,7 +148,7 @@ namespace num (λp, calc 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} - ... = 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}) definition add (a b : num) : num := diff --git a/library/data/set.lean b/library/data/set.lean index 5d7aee4e2..b18df00cf 100644 --- a/library/data/set.lean +++ b/library/data/set.lean @@ -45,26 +45,26 @@ infixl `∩` := inter theorem mem_inter {T : Type} (x : T) (A B : set T) : x ∈ A ∩ B ↔ (x ∈ A ∧ x ∈ B) := 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, have e1 : A x = tt, from and.elim_left 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 := -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 ∩ ∅ ∼ ∅ := -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 ∼ ∅ := -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 := -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) := -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 := λ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) := iff.intro - (assume H, or_to_or H) + (assume H, bor.to_or H) (assume H, or.elim H (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, - 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 := -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 := -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 := -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 := -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) := -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 diff --git a/tests/lean/interactive/alias.input.expected.out b/tests/lean/interactive/alias.input.expected.out index 658e32983..cb4f273c0 100644 --- a/tests/lean/interactive/alias.input.expected.out +++ b/tests/lean/interactive/alias.input.expected.out @@ -3,26 +3,26 @@ -- BEGINWAIT -- ENDWAIT -- BEGINFINDP -bool.and_tt_left|∀ (a : bool), eq (bool.and bool.tt a) a -bool.and_tt_right|∀ (a : bool), eq (bool.and a bool.tt) a +bool.band.tt_left|∀ (a : bool), eq (bool.band bool.tt a) a bool.tt|bool -bool.or_tt_left|∀ (a : bool), eq (bool.or bool.tt a) bool.tt -bool.and_eq_tt_elim_left|eq (bool.and ?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.cond_tt|∀ (t e : ?A), eq (bool.cond bool.tt t e) t -bool.or_tt_right|∀ (a : bool), eq (bool.or a bool.tt) bool.tt +bool.band.eq_tt_elim_right|eq (bool.band ?a ?b) bool.tt → eq ?b bool.tt +bool.band.eq_tt_elim_left|eq (bool.band ?a ?b) bool.tt → eq ?a bool.tt +bool.band.tt_right|∀ (a : bool), eq (bool.band a bool.tt) a +bool.bor.tt_right|∀ (a : bool), eq (bool.bor 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.cond.tt|∀ (t e : ?A), eq (bool.cond bool.tt t e) t -- ENDFINDP -- BEGINWAIT -- ENDWAIT -- BEGINFINDP tt|bool -and_tt_left|∀ (a : bool), eq (and tt a) a -and_tt_right|∀ (a : bool), eq (and a tt) a -or_tt_left|∀ (a : bool), eq (or tt a) tt -and_eq_tt_elim_left|eq (and ?a ?b) tt → eq ?a tt -and_eq_tt_elim_right|eq (and ?a ?b) tt → eq ?b tt -cond_tt|∀ (t e : ?A), eq (cond tt t e) t -or_tt_right|∀ (a : bool), eq (or a tt) tt +band.tt_left|∀ (a : bool), eq (band tt a) a +band.eq_tt_elim_right|eq (band ?a ?b) tt → eq ?b tt +band.eq_tt_elim_left|eq (band ?a ?b) tt → eq ?a tt +band.tt_right|∀ (a : bool), eq (band a tt) a +bor.tt_right|∀ (a : bool), eq (bor a tt) tt +bor.tt_left|∀ (a : bool), eq (bor tt a) tt ff_ne_tt|not (eq ff tt) +cond.tt|∀ (t e : ?A), eq (cond tt t e) t -- ENDFINDP