From f6cd604a44f0fc23dfe762c612bbd9c673f1b9e5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Mar 2015 19:20:48 -0800
Subject: [PATCH] chore(library/data/bool): enforce naming conventions

---
 library/data/bool.lean                        | 70 +++++++++----------
 .../lean/interactive/alias.input.expected.out | 24 +++----
 2 files changed, 43 insertions(+), 51 deletions(-)

diff --git a/library/data/bool.lean b/library/data/bool.lean
index df54e62870..4b64f06cde 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -16,17 +16,17 @@ namespace bool
   theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
   bool.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⁻¹
-            ... = cond ff true false : {H⁻¹}
-            ... = false              : cond.ff)
+    (calc true  = cond tt true false : cond_tt
+            ... = cond ff true false : H
+            ... = false              : cond_ff)
     true_ne_false
 
   theorem eq_tt_of_ne_ff : ∀ {a : bool}, a ≠ ff → a = tt
@@ -40,21 +40,21 @@ namespace bool
   theorem absurd_of_eq_ff_of_eq_tt {B : Prop} {a : bool} (H₁ : a = ff) (H₂ : a = tt) : B :=
   absurd (H₁⁻¹ ⬝ H₂) ff_ne_tt
 
-  theorem bor.tt_left (a : bool) : bor tt a = tt :=
+  theorem tt_bor (a : bool) : bor tt a = tt :=
   rfl
 
   notation a || b := bor a b
 
-  theorem bor.tt_right (a : bool) : a || tt = tt :=
+  theorem bor_tt (a : bool) : a || tt = tt :=
   bool.cases_on a rfl rfl
 
-  theorem bor.ff_left (a : bool) : ff || a = a :=
+  theorem ff_bor (a : bool) : ff || a = a :=
   bool.cases_on a rfl rfl
 
-  theorem bor.ff_right (a : bool) : a || ff = a :=
+  theorem bor_ff (a : bool) : a || ff = a :=
   bool.cases_on a rfl rfl
 
-  theorem bor.id (a : bool) : a || a = a :=
+  theorem bor_self (a : bool) : a || a = a :=
   bool.cases_on a rfl rfl
 
   theorem bor.comm (a b : bool) : a || b = b || a :=
@@ -63,33 +63,31 @@ namespace bool
     (bool.cases_on b rfl rfl)
 
   theorem bor.assoc (a b c : bool) : (a || b) || c = a || (b || c) :=
-  bool.cases_on a
-    (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⁻¹)
+  match a with
+  | ff := by rewrite *ff_bor
+  | tt := by rewrite *tt_bor
+  end
 
-  theorem bor.to_or {a b : bool} : a || b = tt → a = tt ∨ b = tt :=
+  theorem or_of_bor_eq {a b : bool} : a || b = tt → a = tt ∨ b = tt :=
   bool.rec_on a
     (assume H : ff || b = tt,
-      have Hb : b = tt, from !bor.ff_left ▸ H,
+      have Hb : b = tt, from !ff_bor ▸ H,
       or.inr Hb)
     (assume H, or.inl rfl)
 
-  theorem band.ff_left (a : bool) : ff && a = ff :=
+  theorem ff_band (a : bool) : ff && a = ff :=
   rfl
 
-  theorem band.tt_left (a : bool) : tt && a = a :=
+  theorem tt_band (a : bool) : tt && a = a :=
   bool.cases_on a rfl rfl
 
-  theorem band.ff_right (a : bool) : a && ff = ff :=
+  theorem band_ff (a : bool) : a && ff = ff :=
   bool.cases_on a rfl rfl
 
-  theorem band.tt_right (a : bool) : a && tt = a :=
+  theorem band_tt (a : bool) : a && tt = a :=
   bool.cases_on a rfl rfl
 
-  theorem band.id (a : bool) : a && a = a :=
+  theorem band_self (a : bool) : a && a = a :=
   bool.cases_on a rfl rfl
 
   theorem band.comm (a b : bool) : a && b = b && a :=
@@ -98,33 +96,31 @@ namespace bool
     (bool.cases_on b rfl rfl)
 
   theorem band.assoc (a b c : bool) : (a && b) && c = a && (b && c) :=
-  bool.cases_on a
-    (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⁻¹)
+  match a with
+  | ff := by rewrite *ff_band
+  | tt := by rewrite *tt_band
+  end
 
-  theorem band.eq_tt_elim_left {a b : bool} (H : a && b = tt) : a = tt :=
+  theorem band_elim_left {a b : bool} (H : a && b = tt) : a = tt :=
   or.elim (dichotomy a)
     (assume H0 : a = ff,
       absurd
-        (calc ff = ff && b : !band.ff_left⁻¹
-             ... = a && b  : {H0⁻¹}
+        (calc ff = ff && b : ff_band
+             ... = a && b  : H0
              ... = tt      : H)
         ff_ne_tt)
     (assume H1 : a = tt, H1)
 
-  theorem band.eq_tt_elim_right {a b : bool} (H : a && b = tt) : b = tt :=
-  band.eq_tt_elim_left (!band.comm ⬝ H)
+  theorem band_elim_right {a b : bool} (H : a && b = tt) : b = tt :=
+  band_elim_left (!band.comm ⬝ H)
 
-  theorem bnot.bnot (a : bool) : bnot (bnot a) = a :=
+  theorem bnot_bnot (a : bool) : bnot (bnot a) = a :=
   bool.cases_on a rfl rfl
 
-  theorem bnot.false : bnot ff = tt :=
+  theorem bnot_false : bnot ff = tt :=
   rfl
 
-  theorem bnot.true  : bnot tt = ff :=
+  theorem bnot_true  : bnot tt = ff :=
   rfl
 
 end bool
diff --git a/tests/lean/interactive/alias.input.expected.out b/tests/lean/interactive/alias.input.expected.out
index a4d3ba1b9d..e8b6fa2b2b 100644
--- a/tests/lean/interactive/alias.input.expected.out
+++ b/tests/lean/interactive/alias.input.expected.out
@@ -3,32 +3,28 @@
 -- BEGINWAIT
 -- ENDWAIT
 -- BEGINFINDP
-bool.band.tt_left|∀ (a : bool), eq (bool.band bool.tt a) a
+bool.bor_tt|∀ (a : bool), eq (bool.bor a bool.tt) bool.tt
+bool.band_tt|∀ (a : bool), eq (bool.band a bool.tt) a
 bool.tt|bool
-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.absurd_of_eq_ff_of_eq_tt|eq ?a bool.ff → eq ?a bool.tt → ?B
 bool.eq_tt_of_ne_ff|ne ?a bool.ff → eq ?a bool.tt
+bool.tt_band|∀ (a : bool), eq (bool.band bool.tt a) a
+bool.cond_tt|∀ (t e : ?A), eq (bool.cond bool.tt t e) t
 bool.ff_ne_tt|not (eq bool.ff bool.tt)
 bool.eq_ff_of_ne_tt|ne ?a bool.tt → eq ?a bool.ff
-bool.cond.tt|∀ (t e : ?A), eq (bool.cond bool.tt t e) t
+bool.tt_bor|∀ (a : bool), eq (bool.bor bool.tt a) bool.tt
 -- ENDFINDP
 -- BEGINWAIT
 -- ENDWAIT
 -- BEGINFINDP
 tt|bool
-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
+tt_bor|∀ (a : bool), eq (bor tt a) tt
+tt_band|∀ (a : bool), eq (band tt a) a
+bor_tt|∀ (a : bool), eq (bor a tt) tt
+band_tt|∀ (a : bool), eq (band a tt) a
 absurd_of_eq_ff_of_eq_tt|eq ?a ff → eq ?a tt → ?B
 eq_tt_of_ne_ff|ne ?a ff → eq ?a tt
+cond_tt|∀ (t e : ?A), eq (cond tt t e) t
 ff_ne_tt|not (eq ff tt)
 eq_ff_of_ne_tt|ne ?a tt → eq ?a ff
-cond.tt|∀ (t e : ?A), eq (cond tt t e) t
 -- ENDFINDP