diff options
| author | Andres Erbsen | 2019-01-28 18:23:51 -0500 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-14 11:07:42 +0000 |
| commit | b7df34e9bc0959a3c074eeb6f67d932605481441 (patch) | |
| tree | 6245555341b1e1a788f62e88ae705afdbe81e9de | |
| parent | 98914efd4193160d843092461674d6482aeee32e (diff) | |
BinInt: 3 lemmas about testbit, mod _ 2^, ones
| -rw-r--r-- | CHANGES.md | 2 | ||||
| -rw-r--r-- | theories/ZArith/BinInt.v | 24 |
2 files changed, 26 insertions, 0 deletions
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. |