refactor(library/standard): rename bit to bool

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

library/standard/bool.lean

@@ -3,23 +3,23 @@
 -- Author: Leonardo de Moura
 import logic decidable
 
-namespace bit
+namespace bool
-inductive bit : Type :=
+inductive bool : Type :=
-| b0 : bit
+| b0 : bool
-| b1 : bit
+| 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
+theorem induction_on {p : bool → Prop} (b : bool) (H0 : p '0) (H1 : p '1) : p b
-:= bit_rec H0 H1 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)
+definition cond {A : Type} (b : bool) (t e : A)
-:= bit_rec e t b
+:= 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)
+definition bor (a b : bool)
-:= bit_rec (bit_rec '0 '1 b) '1 a
+:= 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)
+definition band (a b : bool)
-:= bit_rec '0 (bit_rec '0 '1 b) a
+:= 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)
+theorem decidable_eq [instance] (a b : bool) : decidable (a = b)
-:= bit_rec
+:= bool_rec
-    (bit_rec (inl (refl '0)) (inr b0_ne_b1) b)
+    (bool_rec (inl (refl '0)) (inr b0_ne_b1) b)
-    (bit_rec (inr (not_eq_symm b0_ne_b1)) (inl (refl '1)) b)
+    (bool_rec (inr (not_eq_symm b0_ne_b1)) (inl (refl '1)) b)
     a
 end

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)
+:= or_elim (prop_complete a)
-    (assume Hat,  or_elim (propcomplete b)
+    (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)))
 

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)

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
+import bool
-using bit
+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

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_bool(Const(name("bool", "bool")));
-static expr g_b0(Const(name("bit", "b0")));
+static expr g_b0(Const(name("bool", "b0")));
-static expr g_b1(Const(name("bit", "b1")));
+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_b0)    == g_bool &&
-            tc.infer(g_b1)    == g_bit &&
+            tc.infer(g_b1)    == g_bool &&
-            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_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 (...) {

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