1 files changed, 340 insertions, 35 deletions

diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 48db793c..0142b36b 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -8,8 +8,6 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: ZMake.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Import ZArith.
 Require Import BigNumPrelude.
 Require Import NSig.
@@ -31,8 +29,11 @@ Module Make (N:NType) <: ZType.
 
  Definition t := t_.
 
+ Bind Scope abstract_scope with t t_.
+
  Definition zero := Pos N.zero.
  Definition one  := Pos N.one.
+ Definition two := Pos N.two.
  Definition minus_one := Neg N.one.
 
  Definition of_Z x :=
@@ -66,6 +67,10 @@ Module Make (N:NType) <: ZType.
  exact N.spec_1.
  Qed.
 
+ Theorem spec_2: to_Z two = 2.
+ exact N.spec_2.
+ Qed.
+
  Theorem spec_m1: to_Z minus_one = -1.
  simpl; rewrite N.spec_1; auto.
  Qed.
@@ -104,21 +109,49 @@ Module Make (N:NType) <: ZType.
   exfalso. omega.
  Qed.
 
- Definition eq_bool x y :=
+ Definition eqb x y :=
   match compare x y with
   | Eq => true
   | _ => false
   end.
 
- Theorem spec_eq_bool:
-  forall x y, eq_bool x y = Zeq_bool (to_Z x) (to_Z y).
+ Theorem spec_eqb x y : eqb x y = Z.eqb (to_Z x) (to_Z y).
  Proof.
- unfold eq_bool, Zeq_bool; intros; rewrite spec_compare; reflexivity.
+ apply Bool.eq_iff_eq_true.
+ unfold eqb. rewrite Z.eqb_eq, <- Z.compare_eq_iff, spec_compare.
+ split; [now destruct Z.compare | now intros ->].
  Qed.
 
  Definition lt n m := to_Z n < to_Z m.
  Definition le n m := to_Z n <= to_Z m.
 
+
+ Definition ltb (x y : t) : bool :=
+  match compare x y with
+  | Lt => true
+  | _  => false
+  end.
+
+ Theorem spec_ltb x y : ltb x y = Z.ltb (to_Z x) (to_Z y).
+ Proof.
+ apply Bool.eq_iff_eq_true.
+ rewrite Z.ltb_lt. unfold Z.lt, ltb. rewrite spec_compare.
+ split; [now destruct Z.compare | now intros ->].
+ Qed.
+
+ Definition leb (x y : t) : bool :=
+  match compare x y with
+  | Gt => false
+  | _  => true
+  end.
+
+ Theorem spec_leb x y : leb x y = Z.leb (to_Z x) (to_Z y).
+ Proof.
+ apply Bool.eq_iff_eq_true.
+ rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare.
+ destruct Z.compare; split; try easy. now destruct 1.
+ Qed.
+
  Definition min n m := match compare n m with Gt => m | _ => n end.
  Definition max n m := match compare n m with Lt => m | _ => n end.
 
@@ -273,23 +306,23 @@ Module Make (N:NType) <: ZType.
  unfold square, to_Z; intros [x | x]; rewrite N.spec_square; ring.
  Qed.
 
- Definition power_pos x p :=
+ Definition pow_pos x p :=
   match x with
-  | Pos nx => Pos (N.power_pos nx p)
+  | Pos nx => Pos (N.pow_pos nx p)
   | Neg nx =>
     match p with
     | xH => x
-    | xO _ => Pos (N.power_pos nx p)
-    | xI _ => Neg (N.power_pos nx p)
+    | xO _ => Pos (N.pow_pos nx p)
+    | xI _ => Neg (N.pow_pos nx p)
     end
   end.
 
- Theorem spec_power_pos: forall x n, to_Z (power_pos x n) = to_Z x ^ Zpos n.
+ Theorem spec_pow_pos: forall x n, to_Z (pow_pos x n) = to_Z x ^ Zpos n.
  Proof.
  assert (F0: forall x, (-x)^2 = x^2).
    intros x; rewrite Zpower_2; ring.
- unfold power_pos, to_Z; intros [x | x] [p | p |];
-   try rewrite N.spec_power_pos; try ring.
+ unfold pow_pos, to_Z; intros [x | x] [p | p |];
+   try rewrite N.spec_pow_pos; try ring.
  assert (F: 0 <= 2 * Zpos p).
   assert (0 <= Zpos p); auto with zarith.
  rewrite Zpos_xI; repeat rewrite Zpower_exp; auto with zarith.
@@ -302,18 +335,47 @@ Module Make (N:NType) <: ZType.
  rewrite F0; ring.
  Qed.
 
- Definition power x n :=
+ Definition pow_N x n :=
   match n with
   | N0 => one
-  | Npos p => power_pos x p
+  | Npos p => pow_pos x p
+  end.
+
+ Theorem spec_pow_N: forall x n, to_Z (pow_N x n) = to_Z x ^ Z_of_N n.
+ Proof.
+ destruct n; simpl. apply N.spec_1.
+ apply spec_pow_pos.
+ Qed.
+
+ Definition pow x y :=
+  match to_Z y with
+  | Z0 => one
+  | Zpos p => pow_pos x p
+  | Zneg p => zero
   end.
 
- Theorem spec_power: forall x n, to_Z (power x n) = to_Z x ^ Z_of_N n.
+ Theorem spec_pow: forall x y, to_Z (pow x y) = to_Z x ^ to_Z y.
  Proof.
- destruct n; simpl. rewrite N.spec_1; reflexivity.
- apply spec_power_pos.
+ intros. unfold pow. destruct (to_Z y); simpl.
+ apply N.spec_1.
+ apply spec_pow_pos.
+ apply N.spec_0.
  Qed.
 
+ Definition log2 x :=
+  match x with
+  | Pos nx => Pos (N.log2 nx)
+  | Neg nx => zero
+  end.
+
+ Theorem spec_log2: forall x, to_Z (log2 x) = Z.log2 (to_Z x).
+ Proof.
+  intros. destruct x as [p|p]; simpl. apply N.spec_log2.
+  rewrite N.spec_0.
+  destruct (Z_le_lt_eq_dec _ _ (N.spec_pos p)) as [LT|EQ].
+  rewrite Z.log2_nonpos; auto with zarith.
+  now rewrite <- EQ.
+ Qed.
 
  Definition sqrt x :=
   match x with
@@ -321,15 +383,14 @@ Module Make (N:NType) <: ZType.
   | Neg nx => Neg N.zero
   end.
 
- Theorem spec_sqrt: forall x, 0 <= to_Z x ->
-   to_Z (sqrt x) ^ 2 <= to_Z x < (to_Z (sqrt x) + 1) ^ 2.
+ Theorem spec_sqrt: forall x, to_Z (sqrt x) = Z.sqrt (to_Z x).
  Proof.
- unfold to_Z, sqrt; intros [x | x] H.
-   exact (N.spec_sqrt x).
- replace (N.to_Z x) with 0.
-   rewrite N.spec_0; simpl Zpower; unfold Zpower_pos, iter_pos;
-    auto with zarith.
- generalize (N.spec_pos x); auto with zarith.
+  destruct x as [p|p]; simpl.
+  apply N.spec_sqrt.
+  rewrite N.spec_0.
+  destruct (Z_le_lt_eq_dec _ _ (N.spec_pos p)) as [LT|EQ].
+  rewrite Z.sqrt_neg; auto with zarith.
+  now rewrite <- EQ.
  Qed.
 
  Definition div_eucl x y :=
@@ -339,12 +400,12 @@ Module Make (N:NType) <: ZType.
     (Pos q, Pos r)
   | Pos nx, Neg ny =>
     let (q, r) := N.div_eucl nx ny in
-    if N.eq_bool N.zero r
+    if N.eqb N.zero r
     then (Neg q, zero)
     else (Neg (N.succ q), Neg (N.sub ny r))
   | Neg nx, Pos ny =>
     let (q, r) := N.div_eucl nx ny in
-    if N.eq_bool N.zero r
+    if N.eqb N.zero r
     then (Neg q, zero)
     else (Neg (N.succ q), Pos (N.sub ny r))
   | Neg nx, Neg ny =>
@@ -368,32 +429,32 @@ Module Make (N:NType) <: ZType.
  (* Pos Neg *)
  generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
  break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite N.spec_eq_bool, N.spec_0, Hr;
+ try (injection 1; intros Hr Hq; rewrite N.spec_eqb, N.spec_0, Hr;
       simpl; rewrite Hq, N.spec_0; auto).
  change (- Zpos py) with (Zneg py).
  assert (GT : Zpos py > 0) by (compute; auto).
  generalize (Z_div_mod (Zpos px) (Zpos py) GT).
  unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r').
  intros (EQ,MOD). injection 1. intros Hr' Hq'.
- rewrite N.spec_eq_bool, N.spec_0, Hr'.
+ rewrite N.spec_eqb, N.spec_0, Hr'.
  break_nonneg r pr EQr.
  subst; simpl. rewrite N.spec_0; auto.
- subst. lazy iota beta delta [Zeq_bool Zcompare].
+ subst. lazy iota beta delta [Z.eqb].
  rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *.
  (* Neg Pos *)
  generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
  break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite N.spec_eq_bool, N.spec_0, Hr;
+ try (injection 1; intros Hr Hq; rewrite N.spec_eqb, N.spec_0, Hr;
       simpl; rewrite Hq, N.spec_0; auto).
  change (- Zpos px) with (Zneg px).
  assert (GT : Zpos py > 0) by (compute; auto).
  generalize (Z_div_mod (Zpos px) (Zpos py) GT).
  unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r').
  intros (EQ,MOD). injection 1. intros Hr' Hq'.
- rewrite N.spec_eq_bool, N.spec_0, Hr'.
+ rewrite N.spec_eqb, N.spec_0, Hr'.
  break_nonneg r pr EQr.
  subst; simpl. rewrite N.spec_0; auto.
- subst. lazy iota beta delta [Zeq_bool Zcompare].
+ subst. lazy iota beta delta [Z.eqb].
  rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *.
  (* Neg Neg *)
  generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
@@ -422,6 +483,50 @@ Module Make (N:NType) <: ZType.
  intros q r q11 r1 H; injection H; auto.
  Qed.
 
+ Definition quot x y :=
+  match x, y with
+  | Pos nx, Pos ny => Pos (N.div nx ny)
+  | Pos nx, Neg ny => Neg (N.div nx ny)
+  | Neg nx, Pos ny => Neg (N.div nx ny)
+  | Neg nx, Neg ny => Pos (N.div nx ny)
+  end.
+
+ Definition rem x y :=
+  if eqb y zero then x
+  else
+    match x, y with
+      | Pos nx, Pos ny => Pos (N.modulo nx ny)
+      | Pos nx, Neg ny => Pos (N.modulo nx ny)
+      | Neg nx, Pos ny => Neg (N.modulo nx ny)
+      | Neg nx, Neg ny => Neg (N.modulo nx ny)
+    end.
+
+ Lemma spec_quot : forall x y, to_Z (quot x y) = (to_Z x) ÷ (to_Z y).
+ Proof.
+  intros [x|x] [y|y]; simpl; symmetry; rewrite N.spec_div;
+  (* Nota: we rely here on [forall a b, a ÷ 0 = b / 0] *)
+  destruct (Z.eq_dec (N.to_Z y) 0) as [EQ|NEQ];
+    try (rewrite EQ; now destruct (N.to_Z x));
+  rewrite ?Z.quot_opp_r, ?Z.quot_opp_l, ?Z.opp_involutive, ?Z.opp_inj_wd;
+  trivial; apply Z.quot_div_nonneg;
+   generalize (N.spec_pos x) (N.spec_pos y); Z.order.
+ Qed.
+
+ Lemma spec_rem : forall x y,
+   to_Z (rem x y) = Z.rem (to_Z x) (to_Z y).
+ Proof.
+  intros x y. unfold rem. rewrite spec_eqb, spec_0.
+  case Z.eqb_spec; intros Hy.
+  (* Nota: we rely here on [Z.rem a 0 = a] *)
+  rewrite Hy. now destruct (to_Z x).
+  destruct x as [x|x], y as [y|y]; simpl in *; symmetry;
+   rewrite ?Z.eq_opp_l, ?Z.opp_0 in Hy;
+   rewrite N.spec_modulo, ?Z.rem_opp_r, ?Z.rem_opp_l, ?Z.opp_involutive,
+    ?Z.opp_inj_wd;
+   trivial; apply Z.rem_mod_nonneg;
+    generalize (N.spec_pos x) (N.spec_pos y); Z.order.
+ Qed.
+
  Definition gcd x y :=
   match x, y with
   | Pos nx, Pos ny => Pos (N.gcd nx ny)
@@ -453,4 +558,204 @@ Module Make (N:NType) <: ZType.
  rewrite spec_0, spec_m1. symmetry. rewrite Zsgn_neg; auto with zarith.
  Qed.
 
+ Definition even z :=
+  match z with
+   | Pos n => N.even n
+   | Neg n => N.even n
+  end.
+
+ Definition odd z :=
+  match z with
+   | Pos n => N.odd n
+   | Neg n => N.odd n
+  end.
+
+ Lemma spec_even : forall z, even z = Zeven_bool (to_Z z).
+ Proof.
+  intros [n|n]; simpl; rewrite N.spec_even; trivial.
+  destruct (N.to_Z n) as [|p|p]; now try destruct p.
+ Qed.
+
+ Lemma spec_odd : forall z, odd z = Zodd_bool (to_Z z).
+ Proof.
+  intros [n|n]; simpl; rewrite N.spec_odd; trivial.
+  destruct (N.to_Z n) as [|p|p]; now try destruct p.
+ Qed.
+
+ Definition norm_pos z :=
+   match z with
+     | Pos _ => z
+     | Neg n => if N.eqb n N.zero then Pos n else z
+   end.
+
+ Definition testbit a n :=
+   match norm_pos n, norm_pos a with
+     | Pos p, Pos a => N.testbit a p
+     | Pos p, Neg a => negb (N.testbit (N.pred a) p)
+     | Neg p, _ => false
+   end.
+
+ Definition shiftl a n :=
+   match norm_pos a, n with
+     | Pos a, Pos n => Pos (N.shiftl a n)
+     | Pos a, Neg n => Pos (N.shiftr a n)
+     | Neg a, Pos n => Neg (N.shiftl a n)
+     | Neg a, Neg n => Neg (N.succ (N.shiftr (N.pred a) n))
+   end.
+
+ Definition shiftr a n := shiftl a (opp n).
+
+ Definition lor a b :=
+   match norm_pos a, norm_pos b with
+     | Pos a, Pos b => Pos (N.lor a b)
+     | Neg a, Pos b => Neg (N.succ (N.ldiff (N.pred a) b))
+     | Pos a, Neg b => Neg (N.succ (N.ldiff (N.pred b) a))
+     | Neg a, Neg b => Neg (N.succ (N.land (N.pred a) (N.pred b)))
+   end.
+
+ Definition land a b :=
+   match norm_pos a, norm_pos b with
+     | Pos a, Pos b => Pos (N.land a b)
+     | Neg a, Pos b => Pos (N.ldiff b (N.pred a))
+     | Pos a, Neg b => Pos (N.ldiff a (N.pred b))
+     | Neg a, Neg b => Neg (N.succ (N.lor (N.pred a) (N.pred b)))
+   end.
+
+ Definition ldiff a b :=
+   match norm_pos a, norm_pos b with
+     | Pos a, Pos b => Pos (N.ldiff a b)
+     | Neg a, Pos b => Neg (N.succ (N.lor (N.pred a) b))
+     | Pos a, Neg b => Pos (N.land a (N.pred b))
+     | Neg a, Neg b => Pos (N.ldiff (N.pred b) (N.pred a))
+   end.
+
+ Definition lxor a b :=
+   match norm_pos a, norm_pos b with
+     | Pos a, Pos b => Pos (N.lxor a b)
+     | Neg a, Pos b => Neg (N.succ (N.lxor (N.pred a) b))
+     | Pos a, Neg b => Neg (N.succ (N.lxor a (N.pred b)))
+     | Neg a, Neg b => Pos (N.lxor (N.pred a) (N.pred b))
+   end.
+
+ Definition div2 x := shiftr x one.
+
+ Lemma Zlnot_alt1 : forall x, -(x+1) = Z.lnot x.
+ Proof.
+  unfold Z.lnot, Zpred; auto with zarith.
+ Qed.
+
+ Lemma Zlnot_alt2 : forall x, Z.lnot (x-1) = -x.
+ Proof.
+  unfold Z.lnot, Zpred; auto with zarith.
+ Qed.
+
+ Lemma Zlnot_alt3 : forall x, Z.lnot (-x) = x-1.
+ Proof.
+  unfold Z.lnot, Zpred; auto with zarith.
+ Qed.
+
+ Lemma spec_norm_pos : forall x, to_Z (norm_pos x) = to_Z x.
+ Proof.
+  intros [x|x]; simpl; trivial.
+  rewrite N.spec_eqb, N.spec_0.
+  case Z.eqb_spec; simpl; auto with zarith.
+ Qed.
+
+ Lemma spec_norm_pos_pos : forall x y, norm_pos x = Neg y ->
+  0 < N.to_Z y.
+ Proof.
+  intros [x|x] y; simpl; try easy.
+  rewrite N.spec_eqb, N.spec_0.
+  case Z.eqb_spec; simpl; try easy.
+  inversion 2. subst. generalize (N.spec_pos y); auto with zarith.
+ Qed.
+
+ Ltac destr_norm_pos x :=
+  rewrite <- (spec_norm_pos x);
+  let H := fresh in
+  let x' := fresh x in
+  assert (H := spec_norm_pos_pos x);
+  destruct (norm_pos x) as [x'|x'];
+   specialize (H x' (eq_refl _)) || clear H.
+
+ Lemma spec_testbit: forall x p, testbit x p = Z.testbit (to_Z x) (to_Z p).
+ Proof.
+  intros x p. unfold testbit.
+  destr_norm_pos p; simpl. destr_norm_pos x; simpl.
+  apply N.spec_testbit.
+  rewrite N.spec_testbit, N.spec_pred, Zmax_r by auto with zarith.
+  symmetry. apply Z.bits_opp. apply N.spec_pos.
+  symmetry. apply Z.testbit_neg_r; auto with zarith.
+ Qed.
+
+ Lemma spec_shiftl: forall x p, to_Z (shiftl x p) = Z.shiftl (to_Z x) (to_Z p).
+ Proof.
+  intros x p. unfold shiftl.
+  destr_norm_pos x; destruct p as [p|p]; simpl;
+   assert (Hp := N.spec_pos p).
+  apply N.spec_shiftl.
+  rewrite Z.shiftl_opp_r. apply N.spec_shiftr.
+  rewrite !N.spec_shiftl.
+  rewrite !Z.shiftl_mul_pow2 by apply N.spec_pos.
+  apply Zopp_mult_distr_l.
+  rewrite Z.shiftl_opp_r, N.spec_succ, N.spec_shiftr, N.spec_pred, Zmax_r
+   by auto with zarith.
+  now rewrite Zlnot_alt1, Z.lnot_shiftr, Zlnot_alt2.
+ Qed.
+
+ Lemma spec_shiftr: forall x p, to_Z (shiftr x p) = Z.shiftr (to_Z x) (to_Z p).
+ Proof.
+  intros. unfold shiftr. rewrite spec_shiftl, spec_opp.
+  apply Z.shiftl_opp_r.
+ Qed.
+
+ Lemma spec_land: forall x y, to_Z (land x y) = Z.land (to_Z x) (to_Z y).
+ Proof.
+  intros x y. unfold land.
+  destr_norm_pos x; destr_norm_pos y; simpl;
+   rewrite ?N.spec_succ, ?N.spec_land, ?N.spec_ldiff, ?N.spec_lor,
+    ?N.spec_pred, ?Zmax_r, ?Zlnot_alt1; auto with zarith.
+  now rewrite Z.ldiff_land, Zlnot_alt2.
+  now rewrite Z.ldiff_land, Z.land_comm, Zlnot_alt2.
+  now rewrite Z.lnot_lor, !Zlnot_alt2.
+ Qed.
+
+ Lemma spec_lor: forall x y, to_Z (lor x y) = Z.lor (to_Z x) (to_Z y).
+ Proof.
+  intros x y. unfold lor.
+  destr_norm_pos x; destr_norm_pos y; simpl;
+   rewrite ?N.spec_succ, ?N.spec_land, ?N.spec_ldiff, ?N.spec_lor,
+    ?N.spec_pred, ?Zmax_r, ?Zlnot_alt1; auto with zarith.
+  now rewrite Z.lnot_ldiff, Z.lor_comm, Zlnot_alt2.
+  now rewrite Z.lnot_ldiff, Zlnot_alt2.
+  now rewrite Z.lnot_land, !Zlnot_alt2.
+ Qed.
+
+ Lemma spec_ldiff: forall x y, to_Z (ldiff x y) = Z.ldiff (to_Z x) (to_Z y).
+ Proof.
+  intros x y. unfold ldiff.
+  destr_norm_pos x; destr_norm_pos y; simpl;
+   rewrite ?N.spec_succ, ?N.spec_land, ?N.spec_ldiff, ?N.spec_lor,
+    ?N.spec_pred, ?Zmax_r, ?Zlnot_alt1; auto with zarith.
+  now rewrite Z.ldiff_land, Zlnot_alt3.
+  now rewrite Z.lnot_lor, Z.ldiff_land, <- Zlnot_alt2.
+  now rewrite 2 Z.ldiff_land, Zlnot_alt2, Z.land_comm, Zlnot_alt3.
+ Qed.
+
+ Lemma spec_lxor: forall x y, to_Z (lxor x y) = Z.lxor (to_Z x) (to_Z y).
+ Proof.
+  intros x y. unfold lxor.
+  destr_norm_pos x; destr_norm_pos y; simpl;
+   rewrite ?N.spec_succ, ?N.spec_lxor, ?N.spec_pred, ?Zmax_r, ?Zlnot_alt1;
+   auto with zarith.
+  now rewrite !Z.lnot_lxor_r, Zlnot_alt2.
+  now rewrite !Z.lnot_lxor_l, Zlnot_alt2.
+  now rewrite <- Z.lxor_lnot_lnot, !Zlnot_alt2.
+ Qed.
+
+ Lemma spec_div2: forall x, to_Z (div2 x) = Z.div2 (to_Z x).
+ Proof.
+  intros x. unfold div2. now rewrite spec_shiftr, Z.div2_spec, spec_1.
+ Qed.
+
 End Make.