Numbers and bitwise functions.

 See NatInt/NZBits.v for the common axiomatization of bitwise functions
 over naturals / integers. Some specs aren't pretty, but easier to
 prove, see alternate statements in property functors {N,Z}Bits.
 Negative numbers are considered via the two's complement convention.

 We provide implementations for N (in Ndigits.v), for nat (quite dummy,
 just for completeness), for Z (new file Zdigits_def), for BigN
 (for the moment partly by converting to N, to be improved soon)
 and for BigZ.

 NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in
 the reversed order (for consistency with the rest of the world):
 for instance BigN.shiftl 1 10 is 2^10.

 NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2)
 on negative numbers. For the moment I've kept it intact, and have
 just added a Zdiv2' which is truly equivalent to (Zdiv _ 2).
 To reorganize someday ?

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13689 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 84 insertions, 1 deletions

diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index 1c06b0b8ed..c339154499 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -62,6 +62,14 @@ Module Type ZType.
  Parameter abs : t -> t.
  Parameter even : t -> bool.
  Parameter odd : t -> bool.
+ Parameter testbit : t -> t -> bool.
+ Parameter shiftr : t -> t -> t.
+ Parameter shiftl : t -> t -> t.
+ Parameter land : t -> t -> t.
+ Parameter lor : t -> t -> t.
+ Parameter ldiff : t -> t -> t.
+ Parameter lxor : t -> t -> t.
+ Parameter div2 : t -> t.
 
  Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y].
  Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y].
@@ -94,6 +102,14 @@ Module Type ZType.
  Parameter spec_abs : forall x, [abs x] = Zabs [x].
  Parameter spec_even : forall x, even x = Zeven_bool [x].
  Parameter spec_odd : forall x, odd x = Zodd_bool [x].
+ Parameter spec_testbit: forall x p, testbit x p = Ztestbit [x] [p].
+ Parameter spec_shiftr: forall x p, [shiftr x p] = Zshiftr [x] [p].
+ Parameter spec_shiftl: forall x p, [shiftl x p] = Zshiftl [x] [p].
+ Parameter spec_land: forall x y, [land x y] = Zand [x] [y].
+ Parameter spec_lor: forall x y, [lor x y] = Zor [x] [y].
+ Parameter spec_ldiff: forall x y, [ldiff x y] = Zdiff [x] [y].
+ Parameter spec_lxor: forall x y, [lxor x y] = Zxor [x] [y].
+ Parameter spec_div2: forall x, [div2 x] = Zdiv2' [x].
 
 End ZType.
 
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 62b79fc3a7..f8fa842836 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import ZArith Nnat ZAxioms ZSig.
+Require Import Bool ZArith Nnat ZAxioms ZSig.
 
 (** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *)
 
@@ -17,6 +17,8 @@ Hint Rewrite
  spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_sqrt
  spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
  spec_pow spec_log2 spec_even spec_odd spec_gcd spec_quot spec_rem
+ spec_testbit spec_shiftl spec_shiftr
+ spec_land spec_lor spec_ldiff spec_lxor spec_div2
  : zsimpl.
 
 Ltac zsimpl := autorewrite with zsimpl.
@@ -407,6 +409,71 @@ Proof.
  intros. zify. apply Zgcd_nonneg.
 Qed.
 
+(** Bitwise operations *)
+
+Lemma testbit_spec : forall a n, 0<=n ->
+  exists l, exists h, (0<=l /\ l<2^n) /\
+    a == l + ((if testbit a n then 1 else 0) + 2*h)*2^n.
+Proof.
+ intros a n. zify. intros H.
+ destruct (Ztestbit_spec [a] [n] H) as (l & h & Hl & EQ).
+ exists (of_Z l), (of_Z h).
+ destruct Ztestbit; zify; now split.
+Qed.
+
+Lemma testbit_neg_r : forall a n, n<0 -> testbit a n = false.
+Proof.
+ intros a n. zify. apply Ztestbit_neg_r.
+Qed.
+
+Lemma shiftr_spec : forall a n m, 0<=m ->
+ testbit (shiftr a n) m = testbit a (m+n).
+Proof.
+ intros a n m. zify. apply Zshiftr_spec.
+Qed.
+
+Lemma shiftl_spec_high : forall a n m, 0<=m -> n<=m ->
+ testbit (shiftl a n) m = testbit a (m-n).
+Proof.
+ intros a n m. zify. intros Hn H.
+ now apply Zshiftl_spec_high.
+Qed.
+
+Lemma shiftl_spec_low : forall a n m, m<n ->
+ testbit (shiftl a n) m = false.
+Proof.
+ intros a n m. zify. intros H. now apply Zshiftl_spec_low.
+Qed.
+
+Lemma land_spec : forall a b n,
+ testbit (land a b) n = testbit a n && testbit b n.
+Proof.
+ intros a n m. zify. now apply Zand_spec.
+Qed.
+
+Lemma lor_spec : forall a b n,
+ testbit (lor a b) n = testbit a n || testbit b n.
+Proof.
+ intros a n m. zify. now apply Zor_spec.
+Qed.
+
+Lemma ldiff_spec : forall a b n,
+ testbit (ldiff a b) n = testbit a n && negb (testbit b n).
+Proof.
+ intros a n m. zify. now apply Zdiff_spec.
+Qed.
+
+Lemma lxor_spec : forall a b n,
+ testbit (lxor a b) n = xorb (testbit a n) (testbit b n).
+Proof.
+ intros a n m. zify. now apply Zxor_spec.
+Qed.
+
+Lemma div2_spec : forall a, div2 a == shiftr a 1.
+Proof.
+ intros a. zify. now apply Zdiv2'_spec.
+Qed.
+
 End ZTypeIsZAxioms.
 
 Module ZType_ZAxioms (Z : ZType)