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, 50 insertions, 0 deletions

diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index 4f1c94e99..5fe105aa5 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -471,6 +471,56 @@ Proof.
  rewrite Z.rem_divide; trivial. split; intros (c,Hc); exists c; auto.
 Qed.
 
+(** Particular case : dividing by 2 is related with parity *)
+
+Lemma Zdiv2_odd_eq : forall a,
+ a = 2 * Zdiv2 a + if Zodd_bool a then Zsgn a else 0.
+Proof.
+ destruct a as [ |p|p]; try destruct p; trivial.
+Qed.
+
+Lemma Zdiv2_odd_remainder : forall a,
+ Remainder a 2 (if Zodd_bool a then Zsgn a else 0).
+Proof.
+ intros [ |p|p]. simpl.
+ left. simpl. auto with zarith.
+ left. destruct p; simpl; auto with zarith.
+ right. destruct p; simpl; split; now auto with zarith.
+Qed.
+
+Lemma Zdiv2_quot : forall a, Zdiv2 a = a÷2.
+Proof.
+ intros.
+ apply Zquot_unique_full with (if Zodd_bool a then Zsgn a else 0).
+ apply Zdiv2_odd_remainder.
+ apply Zdiv2_odd_eq.
+Qed.
+
+Lemma Zrem_odd : forall a, Zrem a 2 = if Zodd_bool a then Zsgn a else 0.
+Proof.
+ intros. symmetry.
+ apply Zrem_unique_full with (Zdiv2 a).
+ apply Zdiv2_odd_remainder.
+ apply Zdiv2_odd_eq.
+Qed.
+
+Lemma Zrem_even : forall a, Zrem a 2 = if Zeven_bool a then 0 else Zsgn a.
+Proof.
+ intros a. rewrite Zrem_odd, Zodd_even_bool. now destruct Zeven_bool.
+Qed.
+
+Lemma Zeven_rem : forall a, Zeven_bool a = Zeq_bool (Zrem a 2) 0.
+Proof.
+ intros a. rewrite Zrem_even.
+ destruct a as [ |p|p]; trivial; now destruct p.
+Qed.
+
+Lemma Zodd_rem : forall a, Zodd_bool a = negb (Zeq_bool (Zrem a 2) 0).
+Proof.
+ intros a. rewrite Zrem_odd.
+ destruct a as [ |p|p]; trivial; now destruct p.
+Qed.
+
 (** * Interaction with "historic" Zdiv *)
 
 (** They agree at least on positive numbers: *)