From b7df34e9bc0959a3c074eeb6f67d932605481441 Mon Sep 17 00:00:00 2001
From: Andres Erbsen
Date: Mon, 28 Jan 2019 18:23:51 -0500
Subject: BinInt: 3 lemmas about testbit, mod _ 2^, ones

---
 CHANGES.md               |  2 ++
 theories/ZArith/BinInt.v | 24 ++++++++++++++++++++++++
 2 files changed, 26 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index 59cc17c233..b5161c9fe9 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -175,6 +175,8 @@ Standard Library
 
 - The `Coq.Numbers.Cyclic.Int31` library is deprecated.
 
+- Added lemmas about `Z.testbit`, `Z.ones`, and `Z.modulo`.
+
 Universes
 
 - Added `Print Universes Subgraph` variant of `Print Universes`.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 8fc3ab56c9..542d169e66 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1259,6 +1259,30 @@ Proof.
  f_equal. now rewrite <- add_assoc, add_opp_diag_r, add_0_r.
 Qed.
 
+(** * [testbit] in terms of comparision. *)
+
+Lemma testbit_mod_pow2 a n i (H : 0 <= n)
+  : testbit (a mod 2 ^ n) i = ((i <? n) && testbit a i)%bool.
+Proof.
+  destruct (ltb_spec i n); rewrite
+    ?mod_pow2_bits_low, ?mod_pow2_bits_high by auto; auto.
+Qed.
+
+Lemma testbit_ones n i (H : 0 <= n)
+  : testbit (ones n) i = ((0 <=? i) && (i <? n))%bool.
+Proof.
+  destruct (leb_spec 0 i), (ltb_spec i n); cbn;
+    rewrite ?testbit_neg_r, ?ones_spec_low, ?ones_spec_high by auto; trivial.
+Qed.
+
+Lemma testbit_ones_nonneg n i (Hn : 0 <= n) (Hi: 0 <= i)
+  : testbit (ones n) i = (i <? n).
+Proof.
+  rewrite testbit_ones by auto.
+  destruct (leb_spec 0 i); cbn; solve
+   [ trivial | destruct (proj1 (Z.le_ngt _ _) Hi ltac:(eassumption)) ].
+Qed.
+
 End Z.
 
 Bind Scope Z_scope with Z.t Z.
-- 
cgit v1.2.3