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

7 files changed, 646 insertions, 44 deletions

diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index 26d700773..e532e4ad9 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -12,7 +12,8 @@ Require Export ZArith_base.
 
 (** Extra definitions *)
 
-Require Export Zpow_def Zsqrt_def Zlog_def Zgcd_def Zdiv_def.
+Require Export
+ Zpow_def Zsqrt_def Zlog_def Zgcd_def Zdiv_def Zdigits_def.
 
 (** Extra modules using [Omega] or [Ring]. *)
 
diff --git a/theories/ZArith/Zdigits_def.v b/theories/ZArith/Zdigits_def.v
new file mode 100644
index 000000000..a31ef8c98
--- /dev/null
+++ b/theories/ZArith/Zdigits_def.v
@@ -0,0 +1,420 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** Bitwise operations for ZArith *)
+
+Require Import Bool BinPos BinNat BinInt Ndigits Znat Zeven Zpow_def
+ Zorder Zcompare.
+
+Local Open Scope Z_scope.
+
+(** When accessing the bits of negative numbers, all functions
+  below will use the two's complement representation. For instance,
+  [-1] will correspond to an infinite stream of true bits. If this
+  isn't what you're looking for, you can use [Zabs] first and then
+  access the bits of the absolute value.
+*)
+
+(** [Ztestbit] : accessing the [n]-th bit of a number [a].
+    For negative [n], we arbitrarily answer [false]. *)
+
+Definition Ztestbit a n :=
+ match n with
+   | 0 => Zodd_bool a
+   | Zpos p => match a with
+                 | 0 => false
+                 | Zpos a => Ptestbit a (Npos p)
+                 | Zneg a => negb (Ntestbit (Ppred_N a) (Npos p))
+               end
+   | Zneg _ => false
+ end.
+
+(** Shifts
+
+   Nota: a shift to the right by [-n] will be a shift to the left
+   by [n], and vice-versa.
+
+   For fulfilling the two's complement convention, shifting to
+   the right a negative number should correspond to a division
+   by 2 with rounding toward bottom, hence the use of [Zdiv2']
+   instead of [Zdiv2].
+*)
+
+Definition Zshiftl a n :=
+ match n with
+   | 0 => a
+   | Zpos p => iter_pos p _ (Zmult 2) a
+   | Zneg p => iter_pos p _ Zdiv2' a
+ end.
+
+Definition Zshiftr a n := Zshiftl a (-n).
+
+(** Bitwise operations Zor Zand Zdiff Zxor *)
+
+Definition Zor a b :=
+ match a, b with
+   | 0, _ => b
+   | _, 0 => a
+   | Zpos a, Zpos b => Zpos (Por a b)
+   | Zneg a, Zpos b => Zneg (Nsucc_pos (Ndiff (Ppred_N a) (Npos b)))
+   | Zpos a, Zneg b => Zneg (Nsucc_pos (Ndiff (Ppred_N b) (Npos a)))
+   | Zneg a, Zneg b => Zneg (Nsucc_pos (Nand (Ppred_N a) (Ppred_N b)))
+ end.
+
+Definition Zand a b :=
+ match a, b with
+   | 0, _ => 0
+   | _, 0 => 0
+   | Zpos a, Zpos b => Z_of_N (Pand a b)
+   | Zneg a, Zpos b => Z_of_N (Ndiff (Npos b) (Ppred_N a))
+   | Zpos a, Zneg b => Z_of_N (Ndiff (Npos a) (Ppred_N b))
+   | Zneg a, Zneg b => Zneg (Nsucc_pos (Nor (Ppred_N a) (Ppred_N b)))
+ end.
+
+Definition Zdiff a b :=
+ match a, b with
+   | 0, _ => 0
+   | _, 0 => a
+   | Zpos a, Zpos b => Z_of_N (Pdiff a b)
+   | Zneg a, Zpos b => Zneg (Nsucc_pos (Nor (Ppred_N a) (Npos b)))
+   | Zpos a, Zneg b => Z_of_N (Nand (Npos a) (Ppred_N b))
+   | Zneg a, Zneg b => Z_of_N (Ndiff (Ppred_N b) (Ppred_N a))
+ end.
+
+Definition Zxor a b :=
+ match a, b with
+   | 0, _ => b
+   | _, 0 => a
+   | Zpos a, Zpos b => Z_of_N (Pxor a b)
+   | Zneg a, Zpos b => Zneg (Nsucc_pos (Nxor (Ppred_N a) (Npos b)))
+   | Zpos a, Zneg b => Zneg (Nsucc_pos (Nxor (Npos a) (Ppred_N b)))
+   | Zneg a, Zneg b => Z_of_N (Nxor (Ppred_N a) (Ppred_N b))
+ end.
+
+(** Proofs of specifications *)
+
+Lemma Zdiv2'_spec : forall a, Zdiv2' a = Zshiftr a 1.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma Ztestbit_neg_r : forall a n, n<0 -> Ztestbit a n = false.
+Proof.
+ now destruct n.
+Qed.
+
+Lemma Ztestbit_spec : forall a n, 0<=n ->
+  exists l, exists h, 0<=l<2^n /\
+    a = l + ((if Ztestbit a n then 1 else 0) + 2*h)*2^n.
+Proof.
+ intros a [ |n|n] Hn; (now destruct Hn) || clear Hn.
+ (* n = 0 *)
+ simpl Ztestbit.
+ exists 0. exists (Zdiv2' a). repeat split. easy.
+ now rewrite Zplus_0_l, Zmult_1_r, Zplus_comm, <- Zdiv2'_odd.
+ (* n > 0 *)
+ destruct a.
+ (* ... a = 0 *)
+ exists 0. exists 0. repeat split; try easy. now rewrite Zpower_Ppow.
+ (* ... a > 0 *)
+ simpl Ztestbit.
+ destruct (Ntestbit_spec (Npos p) (Npos n)) as (l & h & (_,Hl) & EQ).
+ exists (Z_of_N l). exists (Z_of_N h).
+ simpl Npow in *; simpl Ntestbit in *. rewrite Zpower_Ppow.
+ repeat split.
+ apply Z_of_N_le_0.
+ rewrite <-Z_of_N_pos. now apply Z_of_N_lt.
+ rewrite <-Z_of_N_pos, EQ.
+ rewrite Z_of_N_plus, Z_of_N_mult. f_equal. f_equal.
+ destruct Ptestbit; now rewrite Z_of_N_plus, Z_of_N_mult.
+ (* ... a < 0 *)
+ simpl Ztestbit.
+ destruct (Ntestbit_spec (Ppred_N p) (Npos n)) as (l & h & (_,Hl) & EQ).
+ exists (2^Zpos n - (Z_of_N l) - 1). exists (-Z_of_N h - 1).
+ simpl Npow in *. rewrite Zpower_Ppow.
+ repeat split.
+ apply Zle_minus_le_0.
+ change 1 with (Zsucc 0). apply Zle_succ_l.
+ apply Zlt_plus_swap. simpl. rewrite <-Z_of_N_pos. now apply Z_of_N_lt.
+ apply Zlt_plus_swap. unfold Zminus. rewrite Zopp_involutive.
+ fold (Zsucc (Zpos (2^n))). apply Zlt_succ_r.
+ apply Zle_plus_swap. unfold Zminus. rewrite Zopp_involutive.
+ rewrite <- (Zplus_0_r (Zpos (2^n))) at 1. apply Zplus_le_compat_l.
+ apply Z_of_N_le_0.
+ apply Zopp_inj. unfold Zminus.
+ rewrite Zopp_neg, !Zopp_plus_distr, !Zopp_involutive.
+ rewrite Zopp_mult_distr_l, Zopp_plus_distr, Zopp_mult_distr_r,
+  Zopp_plus_distr, !Zopp_involutive.
+ rewrite Ppred_N_spec in EQ at 1.
+ apply (f_equal Nsucc) in EQ. rewrite Nsucc_pred in EQ by easy.
+ rewrite <-Z_of_N_pos, EQ.
+ rewrite Z_of_N_succ, Z_of_N_plus, Z_of_N_mult, Z_of_N_pos. unfold Zsucc.
+ rewrite <- (Zplus_assoc _ 1), (Zplus_comm 1), Zplus_assoc. f_equal.
+ rewrite (Zplus_comm (- _)), <- Zplus_assoc. f_equal.
+ change (- Zpos (2^n)) with ((-1)*(Zpos (2^n))). rewrite <- Zmult_plus_distr_l.
+ f_equal.
+ rewrite Z_of_N_plus, Z_of_N_mult.
+ rewrite Zmult_plus_distr_r, Zmult_1_r, (Zplus_comm _ 2), !Zplus_assoc.
+ rewrite (Zplus_comm _ 2), Zplus_assoc. change (2+-1) with 1.
+ f_equal.
+ now destruct Ntestbit.
+Qed.
+
+(** Conversions between [Ztestbit] and [Ntestbit] *)
+
+Lemma Ztestbit_of_N : forall a n,
+ Ztestbit (Z_of_N a) (Z_of_N n) = Ntestbit a n.
+Proof.
+ intros [ |a] [ |n]; simpl; trivial. now destruct a.
+Qed.
+
+Lemma Ztestbit_of_N' : forall a n, 0<=n ->
+ Ztestbit (Z_of_N a) n = Ntestbit a (Zabs_N n).
+Proof.
+ intros. now rewrite <- Ztestbit_of_N, Z_of_N_abs, Zabs_eq.
+Qed.
+
+Lemma Ztestbit_Zpos : forall a n, 0<=n ->
+ Ztestbit (Zpos a) n = Ntestbit (Npos a) (Zabs_N n).
+Proof.
+ intros. now rewrite <- Ztestbit_of_N'.
+Qed.
+
+Lemma Ztestbit_Zneg : forall a n, 0<=n ->
+ Ztestbit (Zneg a) n = negb (Ntestbit (Ppred_N a) (Zabs_N n)).
+Proof.
+ intros a n Hn.
+ rewrite <- Ztestbit_of_N' by trivial.
+ destruct n as [ |n|n];
+  [ | simpl; now destruct (Ppred_N a) | now destruct Hn].
+ unfold Ztestbit.
+ replace (Z_of_N (Ppred_N a)) with (Zpred (Zpos a))
+  by (destruct a; trivial).
+ now rewrite Zodd_bool_pred, <- Zodd_even_bool.
+Qed.
+
+Lemma Ztestbit_0_l : forall n, Ztestbit 0 n = false.
+Proof.
+ now destruct n.
+Qed.
+
+Lemma Ppred_div2_up : forall p,
+ Ppred_N (Pdiv2_up p) = Ndiv2 (Ppred_N p).
+Proof.
+ intros [p|p| ]; trivial.
+ simpl. rewrite Ppred_N_spec. apply (Npred_succ (Npos p)).
+ destruct p; simpl; trivial.
+Qed.
+
+Lemma Z_of_N_div2' : forall n, Z_of_N (Ndiv2 n) = Zdiv2' (Z_of_N n).
+Proof.
+ intros [|p]; trivial. now destruct p.
+Qed.
+
+Lemma Z_of_N_div2 : forall n, Z_of_N (Ndiv2 n) = Zdiv2 (Z_of_N n).
+Proof.
+ intros [|p]; trivial. now destruct p.
+Qed.
+
+(** Auxiliary results about right shift on positive numbers *)
+
+Lemma Ppred_Pshiftl_low : forall p n m, (m<n)%nat ->
+ Nbit (Ppred_N (iter_nat n _ xO p)) m = true.
+Proof.
+ induction n.
+ inversion 1.
+ intros m H. simpl.
+ destruct m.
+ now destruct (iter_nat n _ xO p).
+ apply lt_S_n in H.
+ specialize (IHn m H).
+ now destruct (iter_nat n _ xO p).
+Qed.
+
+Lemma Ppred_Pshiftl_high : forall p n m, (n<=m)%nat ->
+ Nbit (Ppred_N (iter_nat n _ xO p)) m =
+ Nbit (Nshiftl_nat (Ppred_N p) n) m.
+Proof.
+ induction n.
+ now unfold Nshiftl_nat.
+ intros m H.
+ destruct m.
+ inversion H.
+ apply le_S_n in H.
+ rewrite Nshiftl_nat_S.
+ specialize (IHn m H).
+ simpl in *.
+ unfold Nbit.
+ now destruct (Nshiftl_nat (Ppred_N p) n), (iter_nat n positive xO p).
+Qed.
+
+(** Correctness proofs about [Zshiftr] and [Zshiftl] *)
+
+Lemma Zshiftr_spec_aux : forall a n m, 0<=n -> 0<=m ->
+ Ztestbit (Zshiftr a n) m = Ztestbit a (m+n).
+Proof.
+ intros a n m Hn Hm. unfold Zshiftr.
+ destruct n as [ |n|n]; (now destruct Hn) || clear Hn; simpl.
+ now rewrite Zplus_0_r.
+ destruct a as [ |a|a].
+ (* a = 0 *)
+ replace (iter_pos n _ Zdiv2' 0) with 0
+  by (apply iter_pos_invariant; intros; subst; trivial).
+ now rewrite 2 Ztestbit_0_l.
+ (* a > 0 *)
+ rewrite <- (Z_of_N_pos a) at 1.
+ rewrite <- (iter_pos_swap_gen _ _ _ Ndiv2) by exact Z_of_N_div2'.
+ rewrite Ztestbit_Zpos, Ztestbit_of_N'; trivial.
+ rewrite Zabs_N_plus; try easy. simpl Zabs_N.
+ exact (Nshiftr_spec (Npos a) (Npos n) (Zabs_N m)).
+ now apply Zplus_le_0_compat.
+ (* a < 0 *)
+ rewrite <- (iter_pos_swap_gen _ _ _ Pdiv2_up) by trivial.
+ rewrite 2 Ztestbit_Zneg; trivial. f_equal.
+ rewrite Zabs_N_plus; try easy. simpl Zabs_N.
+ rewrite (iter_pos_swap_gen _ _ _ _ Ndiv2) by exact Ppred_div2_up.
+ exact (Nshiftr_spec (Ppred_N a) (Npos n) (Zabs_N m)).
+ now apply Zplus_le_0_compat.
+Qed.
+
+Lemma Zshiftl_spec_low : forall a n m, m<n ->
+ Ztestbit (Zshiftl a n) m = false.
+Proof.
+ intros a [ |n|n] [ |m|m] H; try easy; simpl Zshiftl.
+ rewrite iter_nat_of_P.
+ destruct (nat_of_P_is_S n) as (n' & ->).
+ simpl. now destruct (iter_nat n' _  (Zmult 2) a).
+ destruct a as [ |a|a].
+ (* a = 0 *)
+ replace (iter_pos n _ (Zmult 2) 0) with 0
+  by (apply iter_pos_invariant; intros; subst; trivial).
+ apply Ztestbit_0_l.
+ (* a > 0 *)
+ rewrite <- (iter_pos_swap_gen _ _ _ xO) by trivial.
+ rewrite Ztestbit_Zpos by easy.
+ exact (Nshiftl_spec_low (Npos a) (Npos n) (Npos m) H).
+ (* a < 0 *)
+ rewrite <- (iter_pos_swap_gen _ _ _ xO) by trivial.
+ rewrite Ztestbit_Zneg by easy.
+ simpl Zabs_N.
+ rewrite <- Nbit_Ntestbit, iter_nat_of_P. simpl nat_of_N.
+ rewrite Ppred_Pshiftl_low; trivial.
+ now apply Plt_lt.
+Qed.
+
+Lemma Zshiftl_spec_high : forall a n m, 0<=m -> n<=m ->
+ Ztestbit (Zshiftl a n) m = Ztestbit a (m-n).
+Proof.
+ intros a n m Hm H.
+ destruct n as [ |n|n]. simpl. now rewrite Zminus_0_r.
+ (* n > 0 *)
+ destruct m as [ |m|m]; try (now destruct H).
+ assert (0 <= Zpos m - Zpos n) by (now apply Zle_minus_le_0).
+ assert (EQ : Zabs_N (Zpos m - Zpos n) =  (Npos m - Npos n)%N).
+  apply Z_of_N_eq_rev. rewrite Z_of_N_abs, Zabs_eq by trivial.
+  now rewrite Z_of_N_minus, !Z_of_N_pos, Zmax_r.
+ destruct a; unfold Zshiftl.
+ (* ... a = 0 *)
+ replace (iter_pos n _ (Zmult 2) 0) with 0
+  by (apply iter_pos_invariant; intros; subst; trivial).
+ now rewrite 2 Ztestbit_0_l.
+ (* ... a > 0 *)
+ rewrite <- (iter_pos_swap_gen _ _ _ xO) by trivial.
+ rewrite 2 Ztestbit_Zpos, EQ by easy.
+ exact (Nshiftl_spec_high (Npos p) (Npos n) (Npos m) H).
+ (* ... a < 0 *)
+ rewrite <- (iter_pos_swap_gen _ _ _ xO) by trivial.
+ rewrite 2 Ztestbit_Zneg, EQ by easy. f_equal.
+ simpl Zabs_N.
+ rewrite <- Nshiftl_spec_high by easy.
+ rewrite <- 2 Nbit_Ntestbit, iter_nat_of_P, <- Nshiftl_nat_equiv.
+ simpl nat_of_N.
+ apply Ppred_Pshiftl_high.
+ now apply Ple_le.
+ (* n < 0 *)
+ unfold Zminus. simpl.
+ now apply (Zshiftr_spec_aux a (Zpos n) m).
+Qed.
+
+Lemma Zshiftr_spec : forall a n m, 0<=m ->
+ Ztestbit (Zshiftr a n) m = Ztestbit a (m+n).
+Proof.
+ intros a n m Hm.
+ destruct (Zle_or_lt 0 n).
+ now apply Zshiftr_spec_aux.
+ destruct (Zle_or_lt (-n) m).
+ unfold Zshiftr.
+ rewrite (Zshiftl_spec_high a (-n) m); trivial.
+ unfold Zminus. now rewrite Zopp_involutive.
+ unfold Zshiftr.
+ rewrite (Zshiftl_spec_low a (-n) m); trivial.
+ rewrite Ztestbit_neg_r; trivial.
+ now apply Zlt_plus_swap.
+Qed.
+
+(** Correctness proofs for bitwise operations *)
+
+Lemma Zor_spec : forall a b n,
+ Ztestbit (Zor a b) n = Ztestbit a n || Ztestbit b n.
+Proof.
+ intros a b n.
+ destruct (Zle_or_lt 0 n) as [Hn|Hn]; [|now rewrite !Ztestbit_neg_r].
+ destruct a as [ |a|a], b as [ |b|b];
+  rewrite ?Ztestbit_0_l, ?orb_false_r; trivial; unfold Zor;
+  rewrite ?Ztestbit_Zpos, ?Ztestbit_Zneg, ?Ppred_Nsucc
+   by trivial.
+ now rewrite <- Nor_spec.
+ now rewrite Ndiff_spec, negb_andb, negb_involutive, orb_comm.
+ now rewrite Ndiff_spec, negb_andb, negb_involutive.
+ now rewrite Nand_spec, negb_andb.
+Qed.
+
+Lemma Zand_spec : forall a b n,
+ Ztestbit (Zand a b) n = Ztestbit a n && Ztestbit b n.
+Proof.
+ intros a b n.
+ destruct (Zle_or_lt 0 n) as [Hn|Hn]; [|now rewrite !Ztestbit_neg_r].
+ destruct a as [ |a|a], b as [ |b|b];
+  rewrite ?Ztestbit_0_l, ?andb_false_r; trivial; unfold Zand;
+  rewrite ?Ztestbit_Zpos, ?Ztestbit_Zneg, ?Ztestbit_of_N', ?Ppred_Nsucc
+   by trivial.
+ now rewrite <- Nand_spec.
+ now rewrite Ndiff_spec.
+ now rewrite Ndiff_spec, andb_comm.
+ now rewrite Nor_spec, negb_orb.
+Qed.
+
+Lemma Zdiff_spec : forall a b n,
+ Ztestbit (Zdiff a b) n = Ztestbit a n && negb (Ztestbit b n).
+Proof.
+ intros a b n.
+ destruct (Zle_or_lt 0 n) as [Hn|Hn]; [|now rewrite !Ztestbit_neg_r].
+ destruct a as [ |a|a], b as [ |b|b];
+  rewrite ?Ztestbit_0_l, ?andb_true_r; trivial; unfold Zdiff;
+  rewrite ?Ztestbit_Zpos, ?Ztestbit_Zneg, ?Ztestbit_of_N', ?Ppred_Nsucc
+   by trivial.
+ now rewrite <- Ndiff_spec.
+ now rewrite Nand_spec, negb_involutive.
+ now rewrite Nor_spec, negb_orb.
+ now rewrite Ndiff_spec, negb_involutive, andb_comm.
+Qed.
+
+Lemma Zxor_spec : forall a b n,
+ Ztestbit (Zxor a b) n = xorb (Ztestbit a n) (Ztestbit b n).
+Proof.
+ intros a b n.
+ destruct (Zle_or_lt 0 n) as [Hn|Hn]; [|now rewrite !Ztestbit_neg_r].
+ destruct a as [ |a|a], b as [ |b|b];
+  rewrite ?Ztestbit_0_l, ?xorb_false_l, ?xorb_false_r; trivial; unfold Zxor;
+  rewrite ?Ztestbit_Zpos, ?Ztestbit_Zneg, ?Ztestbit_of_N', ?Ppred_Nsucc
+   by trivial.
+ now rewrite <- Nxor_spec.
+ now rewrite Nxor_spec, negb_xorb_r.
+ now rewrite Nxor_spec, negb_xorb_l.
+ now rewrite Nxor_spec, xorb_negb_negb.
+Qed.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index a14f29308..c9397db8b 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -356,7 +356,7 @@ Proof. intros a b. zero_or_not b. intros; rewrite Z.div_opp_r_nz; auto. Qed.
 
 (** Cancellations. *)
 
-Lemma Zdiv_mult_cancel_r : forall a b c:Z,
+Lemma  Zdiv_mult_cancel_r : forall a b c:Z,
  c <> 0 -> (a*c)/(b*c) = a/b.
 Proof. intros. zero_or_not b. apply Z.div_mul_cancel_r; auto. Qed.
 
@@ -521,6 +521,33 @@ Proof.
  split; intros (c,Hc); exists c; auto.
 Qed.
 
+(** Particular case : dividing by 2 is related with parity *)
+
+Lemma Zdiv2'_div : forall a, Zdiv2' a = a/2.
+Proof.
+ apply Z.div2_div.
+Qed.
+
+Lemma Zmod_odd : forall a, a mod 2 = if Zodd_bool a then 1 else 0.
+Proof.
+ intros a. now rewrite <- Z.bit0_odd, <- Z.bit0_mod.
+Qed.
+
+Lemma Zmod_even : forall a, a mod 2 = if Zeven_bool a then 0 else 1.
+Proof.
+ intros a. rewrite Zmod_odd, Zodd_even_bool. now destruct Zeven_bool.
+Qed.
+
+Lemma Zodd_mod : forall a, Zodd_bool a = Zeq_bool (a mod 2) 1.
+Proof.
+ intros a. rewrite Zmod_odd. now destruct Zodd_bool.
+Qed.
+
+Lemma Zeven_mod : forall a, Zeven_bool a = Zeq_bool (a mod 2) 0.
+Proof.
+ intros a. rewrite Zmod_even. now destruct Zeven_bool.
+Qed.
+
 (** * Compatibility *)
 
 (** Weaker results kept only for compatibility *)
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 74e2e6fbf..70ab4dacc 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -59,128 +59,183 @@ Proof.
  destruct n as [|p|p]; try destruct p; simpl in *; split; easy.
 Qed.
 
+Lemma Zodd_even_bool : forall n, Zodd_bool n = negb (Zeven_bool n).
+Proof.
+ destruct n as [|p|p]; trivial; now destruct p.
+Qed.
+
+Lemma Zeven_odd_bool : forall n, Zeven_bool n = negb (Zodd_bool n).
+Proof.
+ destruct n as [|p|p]; trivial; now destruct p.
+Qed.
+
 Definition Zeven_odd_dec : forall z:Z, {Zeven z} + {Zodd z}.
 Proof.
   intro z. case z;
-  [ left; compute in |- *; trivial
+  [ left; compute; trivial
     | intro p; case p; intros;
-      (right; compute in |- *; exact I) || (left; compute in |- *; exact I)
+      (right; compute; exact I) || (left; compute; exact I)
     | intro p; case p; intros;
-      (right; compute in |- *; exact I) || (left; compute in |- *; exact I) ].
+      (right; compute; exact I) || (left; compute; exact I) ].
 Defined.
 
 Definition Zeven_dec : forall z:Z, {Zeven z} + {~ Zeven z}.
 Proof.
   intro z. case z;
-  [ left; compute in |- *; trivial
+  [ left; compute; trivial
     | intro p; case p; intros;
-      (left; compute in |- *; exact I) || (right; compute in |- *; trivial)
+      (left; compute; exact I) || (right; compute; trivial)
     | intro p; case p; intros;
-      (left; compute in |- *; exact I) || (right; compute in |- *; trivial) ].
+      (left; compute; exact I) || (right; compute; trivial) ].
 Defined.
 
 Definition Zodd_dec : forall z:Z, {Zodd z} + {~ Zodd z}.
 Proof.
   intro z. case z;
-  [ right; compute in |- *; trivial
+  [ right; compute; trivial
     | intro p; case p; intros;
-      (left; compute in |- *; exact I) || (right; compute in |- *; trivial)
+      (left; compute; exact I) || (right; compute; trivial)
     | intro p; case p; intros;
-      (left; compute in |- *; exact I) || (right; compute in |- *; trivial) ].
+      (left; compute; exact I) || (right; compute; trivial) ].
 Defined.
 
 Lemma Zeven_not_Zodd : forall n:Z, Zeven n -> ~ Zodd n.
 Proof.
-  intro z; destruct z; [ idtac | destruct p | destruct p ]; compute in |- *;
+  intro z; destruct z; [ idtac | destruct p | destruct p ]; compute;
     trivial.
 Qed.
 
 Lemma Zodd_not_Zeven : forall n:Z, Zodd n -> ~ Zeven n.
 Proof.
-  intro z; destruct z; [ idtac | destruct p | destruct p ]; compute in |- *;
+  intro z; destruct z; [ idtac | destruct p | destruct p ]; compute;
     trivial.
 Qed.
 
 Lemma Zeven_Sn : forall n:Z, Zodd n -> Zeven (Zsucc n).
 Proof.
-  intro z; destruct z; unfold Zsucc in |- *;
-    [ idtac | destruct p | destruct p ]; simpl in |- *;
+  intro z; destruct z; unfold Zsucc;
+    [ idtac | destruct p | destruct p ]; simpl;
       trivial.
-  unfold Pdouble_minus_one in |- *; case p; simpl in |- *; auto.
+  unfold Pdouble_minus_one; case p; simpl; auto.
 Qed.
 
 Lemma Zodd_Sn : forall n:Z, Zeven n -> Zodd (Zsucc n).
 Proof.
-  intro z; destruct z; unfold Zsucc in |- *;
-    [ idtac | destruct p | destruct p ]; simpl in |- *;
+  intro z; destruct z; unfold Zsucc;
+    [ idtac | destruct p | destruct p ]; simpl;
       trivial.
-  unfold Pdouble_minus_one in |- *; case p; simpl in |- *; auto.
+  unfold Pdouble_minus_one; case p; simpl; auto.
 Qed.
 
 Lemma Zeven_pred : forall n:Z, Zodd n -> Zeven (Zpred n).
 Proof.
-  intro z; destruct z; unfold Zpred in |- *;
-    [ idtac | destruct p | destruct p ]; simpl in |- *;
+  intro z; destruct z; unfold Zpred;
+    [ idtac | destruct p | destruct p ]; simpl;
       trivial.
-  unfold Pdouble_minus_one in |- *; case p; simpl in |- *; auto.
+  unfold Pdouble_minus_one; case p; simpl; auto.
 Qed.
 
 Lemma Zodd_pred : forall n:Z, Zeven n -> Zodd (Zpred n).
 Proof.
-  intro z; destruct z; unfold Zpred in |- *;
-    [ idtac | destruct p | destruct p ]; simpl in |- *;
+  intro z; destruct z; unfold Zpred;
+    [ idtac | destruct p | destruct p ]; simpl;
       trivial.
-  unfold Pdouble_minus_one in |- *; case p; simpl in |- *; auto.
+  unfold Pdouble_minus_one; case p; simpl; auto.
 Qed.
 
 Hint Unfold Zeven Zodd: zarith.
 
+Lemma Zeven_bool_succ : forall n, Zeven_bool (Zsucc n) = Zodd_bool n.
+Proof.
+ destruct n as [ |p|p]; trivial; destruct p as [p|p| ]; trivial.
+ now destruct p.
+Qed.
+
+Lemma Zeven_bool_pred : forall n, Zeven_bool (Zpred n) = Zodd_bool n.
+Proof.
+ destruct n as [ |p|p]; trivial; destruct p as [p|p| ]; trivial.
+ now destruct p.
+Qed.
+
+Lemma Zodd_bool_succ : forall n, Zodd_bool (Zsucc n) = Zeven_bool n.
+Proof.
+ destruct n as [ |p|p]; trivial; destruct p as [p|p| ]; trivial.
+ now destruct p.
+Qed.
+
+Lemma Zodd_bool_pred : forall n, Zodd_bool (Zpred n) = Zeven_bool n.
+Proof.
+ destruct n as [ |p|p]; trivial; destruct p as [p|p| ]; trivial.
+ now destruct p.
+Qed.
 
 (******************************************************************)
 (** * Definition of [Zdiv2] and properties wrt [Zeven] and [Zodd] *)
 
 (** [Zdiv2] is defined on all [Z], but notice that for odd negative
-    integers it is not the euclidean quotient: in that case we have
-      [n = 2*(n/2)-1] *)
+  integers we have [n = 2*(Zdiv2 n)-1], hence it does not
+  correspond to the usual Coq division [Zdiv], for which we would
+  have here [n = 2*(n/2)+1]. Since [Zdiv2] performs rounding
+  toward zero, it is rather a particular case of the alternative
+  division [Zquot].
+*)
 
 Definition Zdiv2 (z:Z) :=
   match z with
-    | Z0 => 0
-    | Zpos xH => 0
+    | 0 => 0
+    | Zpos 1 => 0
     | Zpos p => Zpos (Pdiv2 p)
-    | Zneg xH => 0
+    | Zneg 1 => 0
     | Zneg p => Zneg (Pdiv2 p)
   end.
 
+(** We also provide an alternative [Zdiv2'] performing round toward
+  bottom, and hence corresponding to [Zdiv]. *)
+
+Definition Zdiv2' a :=
+ match a with
+   | 0 => 0
+   | Zpos 1 => 0
+   | Zpos p => Zpos (Pdiv2 p)
+   | Zneg p => Zneg (Pdiv2_up p)
+ end.
+
+Lemma Zdiv2'_odd : forall a,
+ a = 2*(Zdiv2' a) + if Zodd_bool a then 1 else 0.
+Proof.
+ intros [ |[p|p| ]|[p|p|  ]]; simpl; trivial.
+ f_equal. now rewrite xO_succ_permute, <-Ppred_minus, Ppred_succ.
+Qed.
+
 Lemma Zeven_div2 : forall n:Z, Zeven n -> n = 2 * Zdiv2 n.
 Proof.
   intro x; destruct x.
   auto with arith.
   destruct p; auto with arith.
-  intros. absurd (Zeven (Zpos (xI p))); red in |- *; auto with arith.
-  intros. absurd (Zeven 1); red in |- *; auto with arith.
+  intros. absurd (Zeven (Zpos (xI p))); red; auto with arith.
+  intros. absurd (Zeven 1); red; auto with arith.
   destruct p; auto with arith.
-  intros. absurd (Zeven (Zneg (xI p))); red in |- *; auto with arith.
-  intros. absurd (Zeven (-1)); red in |- *; auto with arith.
+  intros. absurd (Zeven (Zneg (xI p))); red; auto with arith.
+  intros. absurd (Zeven (-1)); red; auto with arith.
 Qed.
 
 Lemma Zodd_div2 : forall n:Z, n >= 0 -> Zodd n -> n = 2 * Zdiv2 n + 1.
 Proof.
   intro x; destruct x.
-  intros. absurd (Zodd 0); red in |- *; auto with arith.
+  intros. absurd (Zodd 0); red; auto with arith.
   destruct p; auto with arith.
-  intros. absurd (Zodd (Zpos (xO p))); red in |- *; auto with arith.
-  intros. absurd (Zneg p >= 0); red in |- *; auto with arith.
+  intros. absurd (Zodd (Zpos (xO p))); red; auto with arith.
+  intros. absurd (Zneg p >= 0); red; auto with arith.
 Qed.
 
 Lemma Zodd_div2_neg :
   forall n:Z, n <= 0 -> Zodd n -> n = 2 * Zdiv2 n - 1.
 Proof.
   intro x; destruct x.
-  intros. absurd (Zodd 0); red in |- *; auto with arith.
-  intros. absurd (Zneg p >= 0); red in |- *; auto with arith.
+  intros. absurd (Zodd 0); red; auto with arith.
+  intros. absurd (Zneg p >= 0); red; auto with arith.
   destruct p; auto with arith.
-  intros. absurd (Zodd (Zneg (xO p))); red in |- *; auto with arith.
+  intros. absurd (Zodd (Zneg (xO p))); red; auto with arith.
 Qed.
 
 Lemma Z_modulo_2 :
@@ -192,10 +247,10 @@ Proof.
   right. generalize b; clear b; case x.
   intro b; inversion b.
   intro p; split with (Zdiv2 (Zpos p)). apply (Zodd_div2 (Zpos p)); trivial.
-  unfold Zge, Zcompare in |- *; simpl in |- *; discriminate.
+  unfold Zge, Zcompare; simpl; discriminate.
   intro p; split with (Zdiv2 (Zpred (Zneg p))).
-  pattern (Zneg p) at 1 in |- *; rewrite (Zsucc_pred (Zneg p)).
-  pattern (Zpred (Zneg p)) at 1 in |- *; rewrite (Zeven_div2 (Zpred (Zneg p))).
+  pattern (Zneg p) at 1; rewrite (Zsucc_pred (Zneg p)).
+  pattern (Zpred (Zneg p)) at 1; rewrite (Zeven_div2 (Zpred (Zneg p))).
   reflexivity.
   apply Zeven_pred; assumption.
 Qed.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 5f4a6e38d..8f4a69b1e 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -13,7 +13,7 @@ Require Export Arith_base.
 Require Import BinPos BinInt BinNat Zcompare Zorder.
 Require Import Decidable Peano_dec Min Max Compare_dec.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Definition neq (x y:nat) := x <> y.
 
@@ -341,3 +341,51 @@ Proof.
  intros. unfold Zmax, Nmax. rewrite Z_of_N_compare.
  case Ncompare_spec; intros; subst; trivial.
 Qed.
+
+(** Results about the [Zabs_N] function, converting from Z to N *)
+
+Lemma Zabs_of_N : forall n, Zabs_N (Z_of_N n) = n.
+Proof.
+ now destruct n.
+Qed.
+
+Lemma Zabs_N_succ_abs : forall n,
+ Zabs_N (Zsucc (Zabs n)) = Nsucc (Zabs_N n).
+Proof.
+ intros [ |n|n]; simpl; trivial; now rewrite Pplus_one_succ_r.
+Qed.
+
+Lemma Zabs_N_succ : forall n, 0<=n ->
+ Zabs_N (Zsucc n) = Nsucc (Zabs_N n).
+Proof.
+ intros n Hn. rewrite <- Zabs_N_succ_abs. repeat f_equal.
+ symmetry; now apply Zabs_eq.
+Qed.
+
+Lemma Zabs_N_plus_abs : forall n m,
+ Zabs_N (Zabs n + Zabs m) = (Zabs_N n + Zabs_N m)%N.
+Proof.
+ intros [ |n|n] [ |m|m]; simpl; trivial.
+Qed.
+
+Lemma Zabs_N_plus : forall n m, 0<=n -> 0<=m ->
+ Zabs_N (n + m) = (Zabs_N n + Zabs_N m)%N.
+Proof.
+ intros n m Hn Hm.
+ rewrite <- Zabs_N_plus_abs; repeat f_equal;
+  symmetry; now apply Zabs_eq.
+Qed.
+
+Lemma Zabs_N_mult_abs : forall n m,
+ Zabs_N (Zabs n * Zabs m) = (Zabs_N n * Zabs_N m)%N.
+Proof.
+ intros [ |n|n] [ |m|m]; simpl; trivial.
+Qed.
+
+Lemma Zabs_N_mult : forall n m, 0<=n -> 0<=m ->
+ Zabs_N (n * m) = (Zabs_N n * Zabs_N m)%N.
+Proof.
+ intros n m Hn Hm.
+ rewrite <- Zabs_N_mult_abs; repeat f_equal;
+  symmetry; now apply Zabs_eq.
+Qed.
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: *)
diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget
index ef18d67c7..8dc8e9276 100644
--- a/theories/ZArith/vo.itarget
+++ b/theories/ZArith/vo.itarget
@@ -33,3 +33,4 @@ Zsqrt_def.vo
 Zlog_def.vo
 Zgcd_def.vo
 Zeuclid.vo
+Zdigits_def.vo
\ No newline at end of file