From b522ea6f2d1738cc06b1c286e69a3af22c42429d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Jul 2014 09:49:54 -0700 Subject: [PATCH] refactor(library/standard): rename bit to bool Signed-off-by: Leonardo de Moura --- library/standard/{bit.lean => bool.lean} | 68 ++++++++++++------------ library/standard/classical.lean | 18 +++---- library/standard/if.lean | 2 +- library/standard/string.lean | 6 +-- src/library/string.cpp | 12 ++--- tests/lean/run/decidable.lean | 4 +- 6 files changed, 55 insertions(+), 55 deletions(-) rename library/standard/{bit.lean => bool.lean} (58%) diff --git a/library/standard/bit.lean b/library/standard/bool.lean similarity index 58% rename from library/standard/bit.lean rename to library/standard/bool.lean index bbabe1911..3675b9640 100644 --- a/library/standard/bit.lean +++ b/library/standard/bool.lean @@ -3,23 +3,23 @@ -- Author: Leonardo de Moura import logic decidable -namespace bit -inductive bit : Type := -| b0 : bit -| b1 : bit +namespace bool +inductive bool : Type := +| b0 : bool +| b1 : bool notation `'0`:max := b0 notation `'1`:max := b1 -theorem induction_on {p : bit → Prop} (b : bit) (H0 : p '0) (H1 : p '1) : p b -:= bit_rec H0 H1 b +theorem induction_on {p : bool → Prop} (b : bool) (H0 : p '0) (H1 : p '1) : p b +:= bool_rec H0 H1 b -theorem inhabited_bit [instance] : inhabited bit +theorem inhabited_bool [instance] : inhabited bool := inhabited_intro b0 -definition cond {A : Type} (b : bit) (t e : A) -:= bit_rec e t b +definition cond {A : Type} (b : bool) (t e : A) +:= bool_rec e t b -theorem dichotomy (b : bit) : b = '0 ∨ b = '1 +theorem dichotomy (b : bool) : b = '0 ∨ b = '1 := induction_on b (or_intro_left _ (refl '0)) (or_intro_right _ (refl '1)) theorem cond_b0 {A : Type} (t e : A) : cond '0 t e = e @@ -35,57 +35,57 @@ theorem b0_ne_b1 : ¬ '0 = '1 ... = false : cond_b0 _ _) true_ne_false) -definition bor (a b : bit) -:= bit_rec (bit_rec '0 '1 b) '1 a +definition bor (a b : bool) +:= bool_rec (bool_rec '0 '1 b) '1 a -theorem bor_b1_left (a : bit) : bor '1 a = '1 +theorem bor_b1_left (a : bool) : bor '1 a = '1 := refl (bor '1 a) infixl `||`:65 := bor -theorem bor_b1_right (a : bit) : a || '1 = '1 +theorem bor_b1_right (a : bool) : a || '1 = '1 := induction_on a (refl ('0 || '1)) (refl ('1 || '1)) -theorem bor_b0_left (a : bit) : '0 || a = a +theorem bor_b0_left (a : bool) : '0 || a = a := induction_on a (refl ('0 || '0)) (refl ('0 || '1)) -theorem bor_b0_right (a : bit) : a || '0 = a +theorem bor_b0_right (a : bool) : a || '0 = a := induction_on a (refl ('0 || '0)) (refl ('1 || '0)) -theorem bor_id (a : bit) : a || a = a +theorem bor_id (a : bool) : a || a = a := induction_on a (refl ('0 || '0)) (refl ('1 || '1)) -theorem bor_swap (a b : bit) : a || b = b || a +theorem bor_swap (a b : bool) : a || b = b || a := induction_on a (induction_on b (refl ('0 || '0)) (refl ('0 || '1))) (induction_on b (refl ('1 || '0)) (refl ('1 || '1))) -definition band (a b : bit) -:= bit_rec '0 (bit_rec '0 '1 b) a +definition band (a b : bool) +:= bool_rec '0 (bool_rec '0 '1 b) a infixl `&&`:75 := band -theorem band_b0_left (a : bit) : '0 && a = '0 +theorem band_b0_left (a : bool) : '0 && a = '0 := refl ('0 && a) -theorem band_b1_left (a : bit) : '1 && a = a +theorem band_b1_left (a : bool) : '1 && a = a := induction_on a (refl ('1 && '0)) (refl ('1 && '1)) -theorem band_b0_right (a : bit) : a && '0 = '0 +theorem band_b0_right (a : bool) : a && '0 = '0 := induction_on a (refl ('0 && '0)) (refl ('1 && '0)) -theorem band_b1_right (a : bit) : a && '1 = a +theorem band_b1_right (a : bool) : a && '1 = a := induction_on a (refl ('0 && '1)) (refl ('1 && '1)) -theorem band_id (a : bit) : a && a = a +theorem band_id (a : bool) : a && a = a := induction_on a (refl ('0 && '0)) (refl ('1 && '1)) -theorem band_swap (a b : bit) : a && b = b && a +theorem band_swap (a b : bool) : a && b = b && a := induction_on a (induction_on b (refl ('0 && '0)) (refl ('0 && '1))) (induction_on b (refl ('1 && '0)) (refl ('1 && '1))) -theorem band_eq_b1_elim_left {a b : bit} (H : a && b = '1) : a = '1 +theorem band_eq_b1_elim_left {a b : bool} (H : a && b = '1) : a = '1 := or_elim (dichotomy a) (assume H0 : a = '0, absurd_elim (a = '1) @@ -95,14 +95,14 @@ theorem band_eq_b1_elim_left {a b : bit} (H : a && b = '1) : a = '1 b0_ne_b1) (assume H1 : a = '1, H1) -theorem band_eq_b1_elim_right {a b : bit} (H : a && b = '1) : b = '1 +theorem band_eq_b1_elim_right {a b : bool} (H : a && b = '1) : b = '1 := band_eq_b1_elim_left (trans (band_swap b a) H) -definition bnot (a : bit) := bit_rec '1 '0 a +definition bnot (a : bool) := bool_rec '1 '0 a prefix `!`:85 := bnot -theorem bnot_bnot (a : bit) : !!a = a +theorem bnot_bnot (a : bool) : !!a = a := induction_on a (refl (!!'0)) (refl (!!'1)) theorem bnot_false : !'0 = '1 @@ -112,9 +112,9 @@ theorem bnot_true : !'1 = '0 := refl _ using decidable -theorem decidable_eq [instance] (a b : bit) : decidable (a = b) -:= bit_rec - (bit_rec (inl (refl '0)) (inr b0_ne_b1) b) - (bit_rec (inr (not_eq_symm b0_ne_b1)) (inl (refl '1)) b) +theorem decidable_eq [instance] (a b : bool) : decidable (a = b) +:= bool_rec + (bool_rec (inl (refl '0)) (inr b0_ne_b1) b) + (bool_rec (inr (not_eq_symm b0_ne_b1)) (inl (refl '1)) b) a end diff --git a/library/standard/classical.lean b/library/standard/classical.lean index 6a10dba6c..71cd9621c 100644 --- a/library/standard/classical.lean +++ b/library/standard/classical.lean @@ -3,19 +3,19 @@ -- Author: Leonardo de Moura import logic cast -axiom propcomplete (a : Prop) : a = true ∨ a = false +axiom prop_complete (a : Prop) : a = true ∨ a = false theorem case (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a -:= or_elim (propcomplete a) +:= or_elim (prop_complete a) (assume Ht : a = true, subst (symm Ht) H1) (assume Hf : a = false, subst (symm Hf) H2) theorem em (a : Prop) : a ∨ ¬a -:= or_elim (propcomplete a) +:= or_elim (prop_complete a) (assume Ht : a = true, or_intro_left (¬ a) (eqt_elim Ht)) (assume Hf : a = false, or_intro_right a (eqf_elim Hf)) -theorem propcomplete_swapped (a : Prop) : a = false ∨ a = true +theorem prop_complete_swapped (a : Prop) : a = false ∨ a = true := case (λ x, x = false ∨ x = true) (or_intro_right (true = false) (refl true)) (or_intro_left (false = true) (refl false)) @@ -25,13 +25,13 @@ theorem not_true : (¬true) = false := have aux : ¬ (¬true) = true, from not_intro (assume H : (¬true) = true, absurd_not_true (subst (symm H) trivial)), - resolve_right (propcomplete (¬true)) aux + resolve_right (prop_complete (¬true)) aux theorem not_false : (¬false) = true := have aux : ¬ (¬false) = false, from not_intro (assume H : (¬false) = false, subst H not_false_trivial), - resolve_right (propcomplete_swapped (¬ false)) aux + resolve_right (prop_complete_swapped (¬ false)) aux theorem not_not_eq (a : Prop) : (¬¬a) = a := case (λ x, (¬¬x) = x) @@ -45,11 +45,11 @@ theorem not_not_elim {a : Prop} (H : ¬¬a) : a := (not_not_eq a) ◂ H theorem propext {a b : Prop} (Hab : a → b) (Hba : b → a) : a = b -:= or_elim (propcomplete a) - (assume Hat, or_elim (propcomplete b) +:= or_elim (prop_complete a) + (assume Hat, or_elim (prop_complete b) (assume Hbt, trans Hat (symm Hbt)) (assume Hbf, false_elim (a = b) (subst Hbf (Hab (eqt_elim Hat))))) - (assume Haf, or_elim (propcomplete b) + (assume Haf, or_elim (prop_complete b) (assume Hbt, false_elim (a = b) (subst Haf (Hba (eqt_elim Hbt)))) (assume Hbf, trans Haf (symm Hbf))) diff --git a/library/standard/if.lean b/library/standard/if.lean index 8a15aec17..a93592189 100644 --- a/library/standard/if.lean +++ b/library/standard/if.lean @@ -2,7 +2,7 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura import decidable tactic -using bit decidable tactic +using decidable tactic definition ite (c : Prop) {H : decidable c} {A : Type} (t e : A) : A := rec H (assume Hc, t) (assume Hnc, e) diff --git a/library/standard/string.lean b/library/standard/string.lean index 96b29ec97..18d67d3a5 100644 --- a/library/standard/string.lean +++ b/library/standard/string.lean @@ -1,12 +1,12 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura -import bit -using bit +import bool +using bool namespace string inductive char : Type := -| ascii : bit → bit → bit → bit → bit → bit → bit → bit → char +| ascii : bool → bool → bool → bool → bool → bool → bool → bool → char inductive string : Type := | empty : string diff --git a/src/library/string.cpp b/src/library/string.cpp index f3b6ad21c..7c89e8b43 100644 --- a/src/library/string.cpp +++ b/src/library/string.cpp @@ -14,9 +14,9 @@ namespace lean { static name g_string_macro("string_macro"); static std::string g_string_opcode("Str"); -static expr g_bit(Const(name("bit", "bit"))); -static expr g_b0(Const(name("bit", "b0"))); -static expr g_b1(Const(name("bit", "b1"))); +static expr g_bool(Const(name("bool", "bool"))); +static expr g_b0(Const(name("bool", "b0"))); +static expr g_b1(Const(name("bool", "b1"))); static expr g_char(Const(name("string", "char"))); static expr g_ascii(Const(name("string", "ascii"))); static expr g_string(Const(name("string", "string"))); @@ -101,9 +101,9 @@ bool has_string_decls(environment const & env) { try { type_checker tc(env); return - tc.infer(g_b0) == g_bit && - tc.infer(g_b1) == g_bit && - tc.infer(g_ascii) == g_bit >> (g_bit >> (g_bit >> (g_bit >> (g_bit >> (g_bit >> (g_bit >> (g_bit >> g_char))))))) && + tc.infer(g_b0) == g_bool && + tc.infer(g_b1) == g_bool && + tc.infer(g_ascii) == g_bool >> (g_bool >> (g_bool >> (g_bool >> (g_bool >> (g_bool >> (g_bool >> (g_bool >> g_char))))))) && tc.infer(g_empty) == g_string && tc.infer(g_str) == g_char >> (g_string >> g_string); } catch (...) { diff --git a/tests/lean/run/decidable.lean b/tests/lean/run/decidable.lean index f2a450a7e..636a605b5 100644 --- a/tests/lean/run/decidable.lean +++ b/tests/lean/run/decidable.lean @@ -1,7 +1,7 @@ import standard unit decidable if -using bit unit decidable +using bool unit decidable -variables a b c : bit +variables a b c : bool variables u v : unit set_option pp.implicit true check if ((a = b) ∧ (b = c) → ¬ (u = v) ∨ (a = c) → (a = c) ↔ a = '1 ↔ true) then a else b