diff options
| author | Vincent Laporte | 2019-03-15 12:48:51 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-15 12:48:51 +0000 |
| commit | a44c4a34202fa6834520fcd6842cc98eecf044ec (patch) | |
| tree | 8c2fa10f96e527a8b4c9131568cf59bdff8388f8 | |
| parent | 710a7cad94dcc9c734ab9ccc425f7a080dddc5f8 (diff) | |
| parent | b7df34e9bc0959a3c074eeb6f67d932605481441 (diff) | |
Merge PR #9425: BinInt: 3 lemmas about testbit, mod _ 2^, ones
Reviewed-by: vbgl
| -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. |