From e0f1b166042a4f9c21bf6db4b9d688f68bd5ae3a Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 10 Dec 2016 22:21:33 +0100
Subject: [PATCH] chore(library): minor library changes

---
 library/algebra/order.lean        |  4 +++-
 library/algebra/ordered_ring.lean |  3 +--
 library/data/bv.lean              | 40 +++++++++++++------------------
 library/data/tuple.lean           |  9 ++++---
 4 files changed, 25 insertions(+), 31 deletions(-)

diff --git a/library/algebra/order.lean b/library/algebra/order.lean
index 0ef206de4..be70d9e0c 100644
--- a/library/algebra/order.lean
+++ b/library/algebra/order.lean
@@ -286,7 +286,7 @@ structure decidable_linear_order [class] (A : Type) extends linear_strong_order_
 
 section
   variable [s : decidable_linear_order A]
-  variables {a b c d : A}
+  variables (a b c d : A)
   include s
   open decidable
 
@@ -302,6 +302,8 @@ section
         (assume H2 : b < a, inr (not_le_of_gt H2))
         (assume H2 : ¬ b < a, inl (le_of_not_gt H2)))
 
+  variables {a b c d}
+
   definition has_decidable_eq [instance] : decidable (a = b) :=
   by_cases
     (assume H : a ≤ b,
diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean
index c349149dd..38531ffbc 100644
--- a/library/algebra/ordered_ring.lean
+++ b/library/algebra/ordered_ring.lean
@@ -118,6 +118,7 @@ section
   include s
 
   theorem zero_lt_one : 0 < (1:A) := linear_ordered_semiring.zero_lt_one A
+  theorem zero_le_one : 0 ≤ (1:A) := le_of_lt zero_lt_one
 
   theorem lt_of_mul_lt_mul_left (H : c * a < c * b) (Hc : c ≥ 0) : a < b :=
   lt_of_not_ge
@@ -394,8 +395,6 @@ section
     (assume H : a ≥ 0, mul_nonneg H H)
     (assume H : a ≤ 0, mul_nonneg_of_nonpos_of_nonpos H H)
 
-  theorem zero_le_one : 0 ≤ (1:A) := one_mul 1 ▸ mul_self_nonneg 1
-
   theorem pos_and_pos_or_neg_and_neg_of_mul_pos {a b : A} (Hab : a * b > 0) :
     (a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0) :=
   lt.by_cases
diff --git a/library/data/bv.lean b/library/data/bv.lean
index 2907beb2f..625d46fee 100644
--- a/library/data/bv.lean
+++ b/library/data/bv.lean
@@ -22,12 +22,12 @@ open tuple
 definition bv [reducible] (n : ℕ) := tuple bool n
 
 -- Create a zero bitvector
-definition bv_zero (n : ℕ) : bv n := replicate ff
+definition bv_zero (n : ℕ) : bv n := replicate n ff
 
 -- Create  a bitvector with the constant one.
 definition bv_one  : Π (n : ℕ), bv n
-  | 0 := replicate ff
-  | (succ n) := (replicate ff : bv n) ++ (tt :: nil)
+  | 0 := nil
+  | (succ n) := (replicate n ff : bv n) ++ (tt :: nil)
 
 definition bv_cong {a b : ℕ} : (a = b) → bv a → bv b
 | c (tag x p) := tag x (c ▸ p)
@@ -38,36 +38,30 @@ section shift
   definition bv_shl {n:ℕ} : bv n → ℕ → bv n
     | x i :=
        if le : i ≤ n then
-         let r := dropn i x ++ replicate ff in
+         let r := dropn i x ++ replicate i ff in
          let eq := calc (n-i) + i = n : nat.sub_add_cancel le in
          bv_cong eq r
        else
          bv_zero n
 
-  -- unsigned shift right
+  definition fill_shr {n:ℕ} (x : bv n) (i : ℕ) (fill : bool) : bv n :=
+  let y := replicate (min n i) fill ++ firstn (n-i) x in
+  have min n i + min (n-i) n = n, from if h : i ≤ n then
+    by rewrite [min_eq_right h, min_eq_left !sub_le, -nat.add_sub_assoc h,
+      nat.add_sub_cancel_left]
+  else
+    have h : i ≥ n, from le_of_not_ge h,
+    by rewrite [min_eq_left h, sub_eq_zero_of_le h, min_eq_left !zero_le],
+  bv_cong this y
+
+ -- unsigned shift right
   definition bv_ushr {n:ℕ} : bv n → ℕ → bv n
     | x i :=
-      if le : i ≤ n then
-        let y : bv (n-i) := @firstn _ _ (n - i) (sub_le n i) x in
-        let eq := calc (i+(n-i)) = (n - i) + i : add.comm
-                            ...  = n           : nat.sub_add_cancel le in
-        bv_cong eq (replicate ff ++ y)
-      else
-        bv_zero n
+  fill_shr x i ff
 
   -- signed shift right
   definition bv_sshr {m:ℕ} : bv (succ m) → ℕ → bv (succ m)
-    | x i :=
-      let n := succ m in
-      if le : i ≤ n then
-        let z : bv i := replicate (head x) in
-        let y : bv (n-i) := @firstn _ _ (n - i) (sub_le n i) x in
-        let eq := calc (i+(n-i)) = (n-i) + i : add.comm
-                            ...  = n         : nat.sub_add_cancel le in
-        bv_cong eq (z ++ y)
-      else
-        bv_zero n
-
+    | x i := head x :: fill_shr (tail x) i (head x)
 end shift
 
 section bitwise
diff --git a/library/data/tuple.lean b/library/data/tuple.lean
index 471c20b11..b03130c2b 100644
--- a/library/data/tuple.lean
+++ b/library/data/tuple.lean
@@ -272,18 +272,17 @@ namespace tuple
 
   variable {n : ℕ}
 
-  definition replicate : A → tuple A n
+  definition replicate (n : ℕ) : A → tuple A n
   | a := tag (list.replicate n a) (length_replicate n a)
 
   definition dropn : Π (i:ℕ), tuple A n → tuple A (n - i)
   | i (tag l p) := tag (list.dropn i l) (p ▸ list.length_dropn i l)
 
-  definition firstn : Π (i:ℕ) {p:i ≤ n}, tuple A n → tuple A i
-  | i isLe (tag l p) :=
+  definition firstn : Π (i:ℕ), tuple A n → tuple A (min i n)
+  | i (tag l p) :=
     let q := calc list.length (list.firstn i l)
                      = min i (list.length l)  : list.length_firstn_eq
-                 ... = min i n : p
-                 ... = i : min_eq_left isLe in
+                 ... = min i n : p in
     tag (list.firstn i l) q
 
   definition map₂ : (A → B → C) → tuple A n → tuple B n → tuple C n