From 860e2d904d97ddeb391f8c4d07edce2d65bb944c Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 29 May 2017 06:20:19 -0400
Subject: [PATCH] feat(init/data/nat): bitwise operations

---
 library/data/bitvec.lean           |  5 +--
 library/init/data/nat/bitwise.lean | 52 ++++++++++++++++++++++++++++++
 library/init/data/nat/default.lean |  1 +
 3 files changed, 54 insertions(+), 4 deletions(-)
 create mode 100644 library/init/data/nat/bitwise.lean

diff --git a/library/data/bitvec.lean b/library/data/bitvec.lean
index 1cd4e811aa..1d9ca29b4d 100644
--- a/library/data/bitvec.lean
+++ b/library/data/bitvec.lean
@@ -89,12 +89,9 @@ section arith
 
   protected def add (x y : bitvec n) : bitvec n := tail (adc x y ff)
 
-  protected def borrow (x y b : bool) :=
-  bnot x && y || bnot x && b || y && b
-
   -- Subtract with borrow
   def sbb (x y : bitvec n) (b : bool) : bool × bitvec n :=
-  let f := λ x y c, (bitvec.borrow x y c, bitvec.xor3 x y c) in
+  let f := λ x y c, (bitvec.carry (bnot x) y c, bitvec.xor3 x y c) in
   vector.map_accumr₂ f x y b
 
   protected def sub (x y : bitvec n) : bitvec n := prod.snd (sbb x y ff)
diff --git a/library/init/data/nat/bitwise.lean b/library/init/data/nat/bitwise.lean
new file mode 100644
index 0000000000..ccfadaa3d5
--- /dev/null
+++ b/library/init/data/nat/bitwise.lean
@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Mario Carneiro
+-/
+
+prelude
+import .lemmas init.meta.well_founded_tactics
+
+universe u
+
+namespace nat
+
+  def shiftl : ℕ → ℕ → ℕ
+  | m 0     := m
+  | m (n+1) := 2 * shiftl m n
+
+  def shiftr : ℕ → ℕ → ℕ
+  | m 0     := m
+  | m (n+1) := shiftr m n / 2
+
+  def bodd (n : ℕ) : bool := n % 2 = 1
+
+  def test_bit (m n : ℕ) : bool := bodd (shiftr m n)
+
+  def binary_rec {α : Type u} (f : bool → ℕ → α → α) (z : α) : ℕ → α
+  | 0     := z
+  | (n+1) := let n' := shiftr (n+1) 1 in
+    have n' < (n+1), from (div_lt_iff_lt_mul _ _ dec_trivial).2 $
+    by note := nat.mul_lt_mul_of_pos_left (dec_trivial : 1 < 2) (succ_pos n);
+       rwa mul_one at this,
+    f (bodd (n+1)) n' (binary_rec n')
+
+  def size : ℕ → ℕ := binary_rec (λ_ _, succ) 0
+
+  def bits : ℕ → list bool := binary_rec (λb _ IH, b :: IH) []
+
+  def bit (b : bool) : ℕ → ℕ := cond b bit1 bit0
+
+  def bitwise (f : bool → bool → bool) : ℕ → ℕ → ℕ :=
+  binary_rec
+    (λa m Ia, binary_rec
+      (λb n _, bit (f a b) (Ia n))
+      (bit (f a ff) (Ia 0)))
+    (binary_rec (λb n Ib, bit (f ff b) Ib) 0)
+
+  def lor   : ℕ → ℕ → ℕ := bitwise bor
+  def land  : ℕ → ℕ → ℕ := bitwise band
+  def ldiff : ℕ → ℕ → ℕ := bitwise (λ a b, a && bnot b)
+  def lxor  : ℕ → ℕ → ℕ := bitwise bxor
+
+end nat
diff --git a/library/init/data/nat/default.lean b/library/init/data/nat/default.lean
index 3d884c5b25..148404126c 100644
--- a/library/init/data/nat/default.lean
+++ b/library/init/data/nat/default.lean
@@ -5,3 +5,4 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.data.nat.basic init.data.nat.div init.data.nat.pow init.data.nat.lemmas
+       init.data.nat.bitwise