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

1 files changed, 23 insertions, 1 deletions

diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 1b5d382a32..d2979bcf05 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-Require Import BinPos Ndiv_def Nsqrt_def Ngcd_def.
+Require Import BinPos Ndiv_def Nsqrt_def Ngcd_def Ndigits.
 Require Export BinNat.
 Require Import NAxioms NProperties.
 
@@ -178,6 +178,20 @@ Definition gcd_greatest := Ngcd_greatest.
 Lemma gcd_nonneg : forall a b, 0 <= Ngcd a b.
 Proof. intros. now destruct (Ngcd a b). Qed.
 
+(** Bitwise Operations *)
+
+Definition testbit_spec a n (_:0<=n) := Ntestbit_spec a n.
+Lemma testbit_neg_r a n (H:n<0) : Ntestbit a n = false.
+Proof. now destruct n. Qed.
+Definition shiftl_spec_low := Nshiftl_spec_low.
+Definition shiftl_spec_high a n m (_:0<=m) := Nshiftl_spec_high a n m.
+Definition shiftr_spec a n m (_:0<=m) := Nshiftr_spec a n m.
+Definition lxor_spec := Nxor_spec.
+Definition land_spec := Nand_spec.
+Definition lor_spec := Nor_spec.
+Definition ldiff_spec := Ndiff_spec.
+Definition div2_spec a : Ndiv2 a = Nshiftr a 1 := eq_refl _.
+
 (** The instantiation of operations.
     Placing them at the very end avoids having indirections in above lemmas. *)
 
@@ -207,6 +221,14 @@ Definition sqrt := Nsqrt.
 Definition log2 := Nlog2.
 Definition divide := Ndivide.
 Definition gcd := Ngcd.
+Definition testbit := Ntestbit.
+Definition shiftl := Nshiftl.
+Definition shiftr := Nshiftr.
+Definition lxor := Nxor.
+Definition land := Nand.
+Definition lor := Nor.
+Definition ldiff := Ndiff.
+Definition div2 := Ndiv2.
 
 Include NProp
  <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.