diff options
| -rw-r--r-- | CHANGES.md | 2 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.mli | 6 | ||||
| -rw-r--r-- | theories/ZArith/BinInt.v | 24 |
3 files changed, 32 insertions, 0 deletions
diff --git a/CHANGES.md b/CHANGES.md index 240daf6fe9..3e50a13e9e 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/plugins/micromega/coq_micromega.mli b/plugins/micromega/coq_micromega.mli index b91feb3984..d1776b8ca4 100644 --- a/plugins/micromega/coq_micromega.mli +++ b/plugins/micromega/coq_micromega.mli @@ -20,3 +20,9 @@ val sos_Q : unit Proofview.tactic -> unit Proofview.tactic val sos_R : unit Proofview.tactic -> unit Proofview.tactic val lra_Q : unit Proofview.tactic -> unit Proofview.tactic val lra_R : unit Proofview.tactic -> unit Proofview.tactic + + +(** {5 Use Micromega independently from tactics. } *) + +(** [dump_proof_term] generates the Coq representation of a Micromega proof witness *) +val dump_proof_term : Micromega.zArithProof -> EConstr.t 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. |