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

4 files changed, 389 insertions, 0 deletions

diff --git a/theories/Numbers/NatInt/NZBits.v b/theories/Numbers/NatInt/NZBits.v
new file mode 100644
index 000000000..072daa273
--- /dev/null
+++ b/theories/Numbers/NatInt/NZBits.v
@@ -0,0 +1,76 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Bool NZAxioms NZMulOrder NZParity NZPow NZDiv NZLog.
+
+(** Axiomatization of some bitwise operations *)
+
+Module Type Bits (Import A : Typ).
+ Parameter Inline testbit : t -> t -> bool.
+ Parameters Inline shiftl shiftr land lor ldiff lxor : t -> t -> t.
+ Parameter Inline div2 : t -> t.
+End Bits.
+
+Module Type BitsNotation (Import A : Typ)(Import B : Bits A).
+ Notation "a .[ n ]" := (testbit a n) (at level 5, format "a .[ n ]").
+ Infix ">>" := shiftr (at level 30, no associativity).
+ Infix "<<" := shiftl (at level 30, no associativity).
+End BitsNotation.
+
+Module Type Bits' (A:Typ) := Bits A <+ BitsNotation A.
+
+(** For specifying [testbit], we do not rely on division and modulo,
+  since such a specification won't be easy to prove for particular
+  implementations: advanced properties of / and mod won't be
+  available at that moment. Instead, we decompose the number in
+  low and high part, with the considered bit in the middle.
+
+  Interestingly, this specification also holds for negative numbers,
+  (with a positive low part and a negative high part), and this will
+  correspond to a two's complement representation.
+
+  Moreover, we arbitrary choose false as result of [testbit] at
+  negative bit indexes (if they exist).
+*)
+
+Module Type NZBitsSpec
+ (Import A : NZOrdAxiomsSig')(Import B : Pow' A)(Import C : Bits' A).
+
+ Axiom testbit_spec : forall a n, 0<=n ->
+  exists l, exists h, 0<=l<2^n /\
+    a == l + ((if a.[n] then 1 else 0) + 2*h)*2^n.
+ Axiom testbit_neg_r : forall a n, n<0 -> a.[n] = false.
+
+ Axiom shiftr_spec : forall a n m, 0<=m -> (a >> n).[m] = a.[m+n].
+ Axiom shiftl_spec_high : forall a n m, 0<=m -> n<=m -> (a << n).[m] = a.[m-n].
+ Axiom shiftl_spec_low : forall a n m, m<n -> (a << n).[m] = false.
+
+ Axiom land_spec : forall a b n, (land a b).[n] = a.[n] && b.[n].
+ Axiom lor_spec : forall a b n, (lor a b).[n] = a.[n] || b.[n].
+ Axiom ldiff_spec : forall a b n, (ldiff a b).[n] = a.[n] && negb b.[n].
+ Axiom lxor_spec : forall a b n, (lxor a b).[n] = xorb a.[n] b.[n].
+ Axiom div2_spec : forall a, div2 a == a >> 1.
+
+End NZBitsSpec.
+
+Module Type NZBits (A:NZOrdAxiomsSig)(B:Pow A) := Bits A <+ NZBitsSpec A B.
+Module Type NZBits' (A:NZOrdAxiomsSig)(B:Pow A) := Bits' A <+ NZBitsSpec A B.
+
+(** In the functor of properties will also be defined:
+   - [setbit : t -> t -> t ] defined as [lor a (1<<n)].
+   - [clearbit : t -> t -> t ] defined as [ldiff a (1<<n)].
+   - [ones : t -> t], the number with [n] initial true bits,
+     corresponding to [2^n - 1].
+   - a logical complement [lnot]. For integer numbers it will
+     be a [t->t], doing a swap of all bits, while on natural
+     numbers, it will be a bounded complement [t->t->t], swapping
+     only the first [n] bits.
+*)
+
+(** For the moment, no shared properties about NZ here,
+  since properties and proofs for N and Z are quite different *)
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 0807013eb..aa7ad824c 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -506,6 +506,18 @@ Proof.
  apply div_mod; order.
 Qed.
 
+Lemma mod_mul_r : forall a b c, 0<=a -> 0<b -> 0<c ->
+ a mod (b*c) == a mod b + b*((a/b) mod c).
+Proof.
+ intros a b c Ha Hb Hc.
+ apply add_cancel_l with (b*c*(a/(b*c))).
+ rewrite <- div_mod by (apply neq_mul_0; split; order).
+ rewrite <- div_div by trivial.
+ rewrite add_assoc, add_shuffle0, <- mul_assoc, <- mul_add_distr_l.
+ rewrite <- div_mod by order.
+ apply div_mod; order.
+Qed.
+
 (** A last inequality: *)
 
 Theorem div_mul_le:
diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v
new file mode 100644
index 000000000..29b85724e
--- /dev/null
+++ b/theories/Numbers/NatInt/NZParity.v
@@ -0,0 +1,263 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Bool NZAxioms NZMulOrder.
+
+(** Parity functions *)
+
+Module Type NZParity (Import A : NZAxiomsSig').
+ Parameter Inline even odd : t -> bool.
+ Definition Even n := exists m, n == 2*m.
+ Definition Odd n := exists m, n == 2*m+1.
+ Axiom even_spec : forall n, even n = true <-> Even n.
+ Axiom odd_spec : forall n, odd n = true <-> Odd n.
+End NZParity.
+
+Module Type NZParityProp
+ (Import A : NZOrdAxiomsSig')
+ (Import B : NZParity A)
+ (Import C : NZMulOrderProp A).
+
+(** Morphisms *)
+
+Instance Even_wd : Proper (eq==>iff) Even.
+Proof. unfold Even. solve_predicate_wd. Qed.
+
+Instance Odd_wd : Proper (eq==>iff) Odd.
+Proof. unfold Odd. solve_predicate_wd. Qed.
+
+Instance even_wd : Proper (eq==>Logic.eq) even.
+Proof.
+ intros x x' EQ. rewrite eq_iff_eq_true, 2 even_spec. now apply Even_wd.
+Qed.
+
+Instance odd_wd : Proper (eq==>Logic.eq) odd.
+Proof.
+ intros x x' EQ. rewrite eq_iff_eq_true, 2 odd_spec. now apply Odd_wd.
+Qed.
+
+(** Evenness and oddity are dual notions *)
+
+Lemma Even_or_Odd : forall x, Even x \/ Odd x.
+Proof.
+ nzinduct x.
+ left. exists 0. now nzsimpl.
+ intros x.
+ split; intros [(y,H)|(y,H)].
+ right. exists y. rewrite H. now nzsimpl.
+ left. exists (S y). rewrite H. now nzsimpl'.
+ right.
+ assert (LT : exists z, z<y).
+  destruct (lt_ge_cases 0 y) as [LT|GT]; [now exists 0 | exists x].
+  rewrite <- le_succ_l, H. nzsimpl'.
+  rewrite <- (add_0_r y) at 3. now apply add_le_mono_l.
+ destruct LT as (z,LT).
+ destruct (lt_exists_pred z y LT) as (y' & Hy' & _).
+ exists y'. rewrite <- succ_inj_wd, H, Hy'. now nzsimpl'.
+ left. exists y. rewrite <- succ_inj_wd. rewrite H. now nzsimpl.
+Qed.
+
+Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1.
+Proof.
+ intros. nzsimpl'. apply lt_succ_r. now apply add_le_mono.
+Qed.
+
+Lemma double_above : forall n m, n<m -> 2*n+1 < 2*m.
+Proof.
+ intros. nzsimpl'.
+ rewrite <- le_succ_l, <- add_succ_l, <- add_succ_r.
+ apply add_le_mono; now apply le_succ_l.
+Qed.
+
+Lemma Even_Odd_False : forall x, Even x -> Odd x -> False.
+Proof.
+intros x (y,E) (z,O). rewrite O in E; clear O.
+destruct (le_gt_cases y z) as [LE|GT].
+generalize (double_below _ _ LE); order.
+generalize (double_above _ _ GT); order.
+Qed.
+
+Lemma orb_even_odd : forall n, orb (even n) (odd n) = true.
+Proof.
+ intros.
+ destruct (Even_or_Odd n) as [H|H].
+ rewrite <- even_spec in H. now rewrite H.
+ rewrite <- odd_spec in H. now rewrite H, orb_true_r.
+Qed.
+
+Lemma negb_odd : forall n, negb (odd n) = even n.
+Proof.
+ intros.
+ generalize (Even_or_Odd n) (Even_Odd_False n).
+ rewrite <- even_spec, <- odd_spec.
+ destruct (odd n), (even n); simpl; intuition.
+Qed.
+
+Lemma negb_even : forall n, negb (even n) = odd n.
+Proof.
+ intros. rewrite <- negb_odd. apply negb_involutive.
+Qed.
+
+(** Constants *)
+
+Lemma even_0 : even 0 = true.
+Proof.
+ rewrite even_spec. exists 0. now nzsimpl.
+Qed.
+
+Lemma odd_0 : odd 0 = false.
+Proof.
+ now rewrite <- negb_even, even_0.
+Qed.
+
+Lemma odd_1 : odd 1 = true.
+Proof.
+ rewrite odd_spec. exists 0. now nzsimpl'.
+Qed.
+
+Lemma even_1 : even 1 = false.
+Proof.
+ now rewrite <- negb_odd, odd_1.
+Qed.
+
+Lemma even_2 : even 2 = true.
+Proof.
+ rewrite even_spec. exists 1. now nzsimpl'.
+Qed.
+
+Lemma odd_2 : odd 2 = false.
+Proof.
+ now rewrite <- negb_even, even_2.
+Qed.
+
+(** Parity and successor *)
+
+Lemma Odd_succ : forall n, Odd (S n) <-> Even n.
+Proof.
+ split; intros (m,H).
+ exists m. apply succ_inj. now rewrite add_1_r in H.
+ exists m. rewrite add_1_r. now apply succ_wd.
+Qed.
+
+Lemma odd_succ : forall n, odd (S n) = even n.
+Proof.
+ intros. apply eq_iff_eq_true. rewrite even_spec, odd_spec.
+ apply Odd_succ.
+Qed.
+
+Lemma even_succ : forall n, even (S n) = odd n.
+Proof.
+ intros. now rewrite <- negb_odd, odd_succ, negb_even.
+Qed.
+
+Lemma Even_succ : forall n, Even (S n) <-> Odd n.
+Proof.
+ intros. now rewrite <- even_spec, even_succ, odd_spec.
+Qed.
+
+(** Parity and successor of successor *)
+
+Lemma Even_succ_succ : forall n, Even (S (S n)) <-> Even n.
+Proof.
+ intros. now rewrite Even_succ, Odd_succ.
+Qed.
+
+Lemma Odd_succ_succ : forall n, Odd (S (S n)) <-> Odd n.
+Proof.
+ intros. now rewrite Odd_succ, Even_succ.
+Qed.
+
+Lemma even_succ_succ : forall n, even (S (S n)) = even n.
+Proof.
+ intros. now rewrite even_succ, odd_succ.
+Qed.
+
+Lemma odd_succ_succ : forall n, odd (S (S n)) = odd n.
+Proof.
+ intros. now rewrite odd_succ, even_succ.
+Qed.
+
+(** Parity and addition *)
+
+Lemma even_add : forall n m, even (n+m) = Bool.eqb (even n) (even m).
+Proof.
+ intros.
+ case_eq (even n); case_eq (even m);
+  rewrite <- ?negb_true_iff, ?negb_even, ?odd_spec, ?even_spec;
+  intros (m',Hm) (n',Hn).
+ exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm.
+ exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc.
+ exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0.
+ exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1.
+Qed.
+
+Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m).
+Proof.
+ intros. rewrite <- !negb_even. rewrite even_add.
+ now destruct (even n), (even m).
+Qed.
+
+(** Parity and multiplication *)
+
+Lemma even_mul : forall n m, even (mul n m) = even n || even m.
+Proof.
+ intros.
+ case_eq (even n); simpl; rewrite ?even_spec.
+ intros (n',Hn). exists (n'*m). now rewrite Hn, mul_assoc.
+ case_eq (even m); simpl; rewrite ?even_spec.
+ intros (m',Hm). exists (n*m'). now rewrite Hm, !mul_assoc, (mul_comm 2).
+ (* odd / odd *)
+ rewrite <- !negb_true_iff, !negb_even, !odd_spec.
+ intros (m',Hm) (n',Hn). exists (n'*2*m' +n'+m').
+ rewrite Hn,Hm, !mul_add_distr_l, !mul_add_distr_r, !mul_1_l, !mul_1_r.
+ now rewrite add_shuffle1, add_assoc, !mul_assoc.
+Qed.
+
+Lemma odd_mul : forall n m, odd (mul n m) = odd n && odd m.
+Proof.
+ intros. rewrite <- !negb_even. rewrite even_mul.
+ now destruct (even n), (even m).
+Qed.
+
+(** A particular case : adding by an even number *)
+
+Lemma even_add_even : forall n m, Even m -> even (n+m) = even n.
+Proof.
+ intros n m Hm. apply even_spec in Hm.
+ rewrite even_add, Hm. now destruct (even n).
+Qed.
+
+Lemma odd_add_even : forall n m, Even m -> odd (n+m) = odd n.
+Proof.
+ intros n m Hm. apply even_spec in Hm.
+ rewrite odd_add, <- (negb_even m), Hm. now destruct (odd n).
+Qed.
+
+Lemma even_add_mul_even : forall n m p, Even m -> even (n+m*p) = even n.
+Proof.
+ intros n m p Hm. apply even_spec in Hm.
+ apply even_add_even. apply even_spec. now rewrite even_mul, Hm.
+Qed.
+
+Lemma odd_add_mul_even : forall n m p, Even m -> odd (n+m*p) = odd n.
+Proof.
+ intros n m p Hm. apply even_spec in Hm.
+ apply odd_add_even. apply even_spec. now rewrite even_mul, Hm.
+Qed.
+
+Lemma even_add_mul_2 : forall n m, even (n+2*m) = even n.
+Proof.
+ intros. apply even_add_mul_even. apply even_spec, even_2.
+Qed.
+
+Lemma odd_add_mul_2 : forall n m, odd (n+2*m) = odd n.
+Proof.
+ intros. apply odd_add_mul_even. apply even_spec, even_2.
+Qed.
+
+End NZParityProp.
\ No newline at end of file
diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v
index 76b745bf0..23c27777a 100644
--- a/theories/Numbers/NatInt/NZPow.v
+++ b/theories/Numbers/NatInt/NZPow.v
@@ -54,6 +54,14 @@ Proof.
  rewrite EQ. now nzsimpl.
 Qed.
 
+Lemma pow_0_l' : forall a, a~=0 -> 0^a == 0.
+Proof.
+ intros a Ha.
+ destruct (lt_trichotomy a 0) as [LT|[EQ|GT]]; try order.
+ now rewrite pow_neg_r.
+ now apply pow_0_l.
+Qed.
+
 Lemma pow_1_r : forall a, a^1 == a.
 Proof.
  intros. now nzsimpl'.
@@ -75,6 +83,36 @@ Qed.
 
 Hint Rewrite pow_2_r : nz.
 
+(** Power and nullity *)
+
+Lemma pow_eq_0 : forall a b, 0<=b -> a^b == 0 -> a == 0.
+Proof.
+ intros a b Hb. apply le_ind with (4:=Hb).
+ solve_predicate_wd.
+ rewrite pow_0_r. order'.
+ clear b Hb. intros b Hb IH.
+ rewrite pow_succ_r by trivial.
+ intros H. apply eq_mul_0 in H. destruct H; trivial.
+ now apply IH.
+Qed.
+
+Lemma pow_nonzero : forall a b, a~=0 -> 0<=b -> a^b ~= 0.
+Proof.
+ intros a b Ha Hb. contradict Ha. now apply pow_eq_0 with b.
+Qed.
+
+Lemma pow_eq_0_iff : forall a b, a^b == 0 <-> b<0 \/ (0<b /\ a==0).
+Proof.
+ intros a b. split.
+ intros H.
+ destruct (lt_trichotomy b 0) as [Hb|[Hb|Hb]].
+ now left.
+ rewrite Hb, pow_0_r in H; order'.
+ right. split; trivial. apply pow_eq_0 with b; order.
+ intros [Hb|[Hb Ha]]. now rewrite pow_neg_r.
+ rewrite Ha. apply pow_0_l'. order.
+Qed.
+
 (** Power and addition, multiplication *)
 
 Lemma pow_add_r : forall a b c, 0<=b -> 0<=c ->