Cyclic31: cleanup, 2 Admitted killed (6 remaining)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10993 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 265 insertions, 249 deletions

diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 044883ec6..d327e13b3 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -1136,7 +1136,7 @@ Let w_iszero i := match i ?= 0 with Eq => true | _ => false end.
 
 (** Modulo [2^p] *)
 Let w_pos_mod p i :=
-  match compare31 p 32 with
+  match compare31 p 31 with
     | Lt => addmuldiv31 p 0 (addmuldiv31 (31-p) i 0)
     | _ => i
   end.
@@ -1227,9 +1227,7 @@ Section Int31_Spec.
  Notation "[|| x ||]" :=
    (zn2z_to_Z wB phi x)  (at level 0, x at level 99).
 
- Definition spec_to_Z := phi_bounded.
-
- Lemma spec_zdigits : [| 31%int31 |] = 31.
+ Lemma spec_zdigits : [| 31 |] = 31.
  Proof.
   reflexivity.
  Qed.
@@ -1239,23 +1237,23 @@ Section Int31_Spec.
   auto with zarith.
  Qed.
 
- Lemma spec_0   : [|0%int31|] = 0.
+ Lemma spec_0   : [| 0 |] = 0.
  Proof.
   reflexivity.
  Qed.
  
- Lemma spec_1   : [|1%int31|] = 1.
+ Lemma spec_1   : [| 1 |] = 1.
  Proof.
   reflexivity.
  Qed.
     
- Lemma spec_Bm1 : [|Tn|] = wB - 1.
+ Lemma spec_Bm1 : [| Tn |] = wB - 1.
  Proof.
   reflexivity.
  Qed.
 
  Lemma spec_compare : forall x y,
-   match compare31 x y with
+   match (x ?= y)%int31 with
      | Eq => [|x|] = [|y|]
      | Lt => [|x|] < [|y|]
      | Gt => [|x|] > [|y|]
@@ -1266,65 +1264,12 @@ Section Int31_Spec.
  intros; apply Zcompare_Eq_eq; auto.
  Qed.
 
- Let w_eq0         := int31_op.(znz_eq0).
-
- Lemma spec_eq0 : forall x, w_eq0 x = true -> [|x|] = 0.
- Proof.
- clear; unfold w_eq0, znz_eq0; simpl.
- unfold compare31; simpl; intros.
- change [|0|] with 0 in H.
- apply Zcompare_Eq_eq.
- now destruct ([|x|] ?= 0).
- Qed.
-
- Let wWW           := int31_op.(znz_WW).
- Let w0W           := int31_op.(znz_0W).
- Let wW0           := int31_op.(znz_W0).
-
- Lemma spec_WW  : forall h l, [||wWW h l||] = [|h|] * wB + [|l|].
- Proof.
- clear; unfold wWW; simpl; intros.
- unfold compare31 in *.
- change [|0|] with 0.
- case_eq ([|h|] ?= 0); simpl; auto.
- case_eq ([|l|] ?= 0); simpl; auto.
- intros.
- rewrite (Zcompare_Eq_eq _ _ H); simpl.
- rewrite (Zcompare_Eq_eq _ _ H0); simpl; auto.
- Qed.
-
- Lemma spec_0W  : forall l, [||w0W l||] = [|l|].
- Proof.
- clear; unfold w0W; simpl; intros.
- unfold compare31 in *.
- change [|0|] with 0.
- case_eq ([|l|] ?= 0); simpl; auto.
- intros; symmetry; apply Zcompare_Eq_eq; auto.
- Qed.
-
- Lemma spec_W0  : forall h, [||wW0 h||] = [|h|]*wB.
- Proof.
- clear; unfold wW0; simpl; intros.
- unfold compare31 in *.
- change [|0|] with 0.
- case_eq ([|h|] ?= 0); simpl; auto with zarith.
- intro H; rewrite (Zcompare_Eq_eq _ _ H); auto.
- Qed.
-
  (** Addition *)
 
- Let w_add_c       := int31_op.(znz_add_c).
- Let w_add_carry_c := int31_op.(znz_add_carry_c).
- Let w_add         := int31_op.(znz_add).
- Let w_add_carry   := int31_op.(znz_add_carry).
- Let w_succ        := int31_op.(znz_succ).
- Let w_succ_c      := int31_op.(znz_succ_c).
-
- Lemma spec_add_c  : forall x y, [+|w_add_c x y|] = [|x|] + [|y|].
+ Lemma spec_add_c  : forall x y, [+|add31c x y|] = [|x|] + [|y|].
  Proof.
- clear; unfold w_add_c, znz_add_c; simpl; intros.
- unfold add31c, add31, interp_carry; rewrite phi_phi_inv.
- generalize (spec_to_Z x)(spec_to_Z y); intros.
+ intros; unfold add31c, add31, interp_carry; rewrite phi_phi_inv.
+ generalize (phi_bounded x)(phi_bounded y); intros.
  set (X:=[|x|]) in *; set (Y:=[|y|]) in *; clearbody X Y.
 
  assert ((X+Y) mod wB ?= X+Y <> Eq -> [+|C1 (phi_inv (X+Y))|] = X+Y).
@@ -1332,24 +1277,23 @@ Section Int31_Spec.
   destruct (Z_lt_le_dec (X+Y) wB).
   contradict H1; auto using Zmod_small with zarith.
   rewrite <- (Z_mod_plus_full (X+Y) (-1) wB).
-  rewrite Zmod_small; romega. (* omega : BUG !! (peut-etre a cause du clear) *)
+  rewrite Zmod_small; romega. 
 
  generalize (Zcompare_Eq_eq ((X+Y) mod wB) (X+Y)); intros Heq.
  destruct Zcompare; intros; 
   [ rewrite phi_phi_inv; auto | now apply H1 | now apply H1].
  Qed.
 
- Lemma spec_succ_c : forall x, [+|w_succ_c x|] = [|x|] + 1.
+ Lemma spec_succ_c : forall x, [+|add31c x 1|] = [|x|] + 1.
  Proof.
- clear - w_add_c; unfold w_succ_c, znz_succ_c; simpl; intros.
- apply spec_add_c. (* erreur gore si clear trop violent *)
+ intros; apply spec_add_c. 
  Qed.
 
- Lemma spec_add_carry_c : forall x y, [+|w_add_carry_c x y|] = [|x|] + [|y|] + 1.
+ Lemma spec_add_carry_c : forall x y, [+|add31carryc x y|] = [|x|] + [|y|] + 1.
  Proof.
- clear; unfold w_add_carry_c, znz_add_carry_c, int31_op; intros.
+ intros.
  unfold add31carryc, interp_carry; rewrite phi_phi_inv.
- generalize (spec_to_Z x)(spec_to_Z y); intros.
+ generalize (phi_bounded x)(phi_bounded y); intros.
  set (X:=[|x|]) in *; set (Y:=[|y|]) in *; clearbody X Y.
 
  assert ((X+Y+1) mod wB ?= X+Y+1 <> Eq -> [+|C1 (phi_inv (X+Y+1))|] = X+Y+1).
@@ -1364,45 +1308,31 @@ Section Int31_Spec.
   [ rewrite phi_phi_inv; auto | now apply H1 | now apply H1].
  Qed.
 
- Lemma spec_add : forall x y, [|w_add x y|] = ([|x|] + [|y|]) mod wB.
+ Lemma spec_add : forall x y, [|x+y|] = ([|x|] + [|y|]) mod wB.
  Proof.
- clear; unfold w_add; simpl; intros.
- apply phi_phi_inv.
+ intros; apply phi_phi_inv.
  Qed.
 
  Lemma spec_add_carry :
-	 forall x y, [|w_add_carry x y|] = ([|x|] + [|y|] + 1) mod wB.
+	 forall x y, [|x+y+1|] = ([|x|] + [|y|] + 1) mod wB.
  Proof.
- clear; unfold w_add_carry, znz_add_carry, int31_op, add31; intros.
+ unfold add31; intros.
  repeat rewrite phi_phi_inv.
  apply Zplus_mod_idemp_l.
  Qed.
 
- Lemma spec_succ : forall x, [|w_succ x|] = ([|x|] + 1) mod wB.
+ Lemma spec_succ : forall x, [|x+1|] = ([|x|] + 1) mod wB.
  Proof.
- clear - w_add; unfold w_succ, znz_succ, int31_op; intros.
- change 1 with [|1|].
- apply spec_add.
+ intros; rewrite <- spec_1; apply spec_add.
  Qed.
 
  (** Substraction *)
 
- Let w_sub_c       := int31_op.(znz_sub_c).
- Let w_sub_carry_c := int31_op.(znz_sub_carry_c).
- Let w_sub         := int31_op.(znz_sub).
- Let w_sub_carry   := int31_op.(znz_sub_carry).
- Let w_pred_c      := int31_op.(znz_pred_c).
- Let w_pred        := int31_op.(znz_pred).
- Let w_opp_c       := int31_op.(znz_opp_c).
- Let w_opp         := int31_op.(znz_opp).
- Let w_opp_carry   := int31_op.(znz_opp_carry).
-
- Lemma spec_sub_c : forall x y, [-|w_sub_c x y|] = [|x|] - [|y|].
+ Lemma spec_sub_c : forall x y, [-|sub31c x y|] = [|x|] - [|y|].
  Proof. 
- clear; unfold w_sub_c; simpl; intros.
  unfold sub31c, sub31, interp_carry; intros.
  rewrite phi_phi_inv.
- generalize (spec_to_Z x)(spec_to_Z y); intros.
+ generalize (phi_bounded x)(phi_bounded y); intros.
  set (X:=[|x|]) in *; set (Y:=[|y|]) in *; clearbody X Y.
 
  assert ((X-Y) mod wB ?= X-Y <> Eq -> [-|C1 (phi_inv (X-Y))|] = X-Y).
@@ -1417,12 +1347,11 @@ Section Int31_Spec.
   [ rewrite phi_phi_inv; auto | now apply H1 | now apply H1].
  Qed.
 
- Lemma spec_sub_carry_c : forall x y, [-|w_sub_carry_c x y|] = [|x|] - [|y|] - 1.
+ Lemma spec_sub_carry_c : forall x y, [-|sub31carryc x y|] = [|x|] - [|y|] - 1.
  Proof.
- clear; unfold w_sub_carry_c; simpl; intros.
  unfold sub31carryc, sub31, interp_carry; intros.
  rewrite phi_phi_inv.
- generalize (spec_to_Z x)(spec_to_Z y); intros.
+ generalize (phi_bounded x)(phi_bounded y); intros.
  set (X:=[|x|]) in *; set (Y:=[|y|]) in *; clearbody X Y.
 
  assert ((X-Y-1) mod wB ?= X-Y-1 <> Eq -> [-|C1 (phi_inv (X-Y-1))|] = X-Y-1).
@@ -1437,62 +1366,51 @@ Section Int31_Spec.
   [ rewrite phi_phi_inv; auto | now apply H1 | now apply H1].
  Qed.
 
- Lemma spec_sub : forall x y, [|w_sub x y|] = ([|x|] - [|y|]) mod wB.
+ Lemma spec_sub : forall x y, [|x-y|] = ([|x|] - [|y|]) mod wB.
  Proof.
- clear; unfold w_sub; simpl; intros.
- apply phi_phi_inv.
+ intros; apply phi_phi_inv.
  Qed.
 
  Lemma spec_sub_carry :
-   forall x y, [|w_sub_carry x y|] = ([|x|] - [|y|] - 1) mod wB.
+   forall x y, [|x-y-1|] = ([|x|] - [|y|] - 1) mod wB.
  Proof.
- clear; unfold w_sub_carry; simpl; intros.
- unfold sub31.
+ unfold sub31; intros.
  repeat rewrite phi_phi_inv.
  apply Zminus_mod_idemp_l.
  Qed.
 
- Lemma spec_opp_c : forall x, [-|w_opp_c x|] = -[|x|].
+ Lemma spec_opp_c : forall x, [-|sub31c 0 x|] = -[|x|].
  Proof. 
- clear - w_sub_c; unfold w_opp_c; simpl; intros.
- apply spec_sub_c.
+ intros; apply spec_sub_c.
  Qed.
 
- Lemma spec_opp : forall x, [|w_opp x|] = (-[|x|]) mod wB.
+ Lemma spec_opp : forall x, [|0 - x|] = (-[|x|]) mod wB.
  Proof.
- clear; unfold w_opp; simpl; intros.
- apply phi_phi_inv.
+ intros; apply phi_phi_inv.
  Qed.
 
- Lemma spec_opp_carry : forall x, [|w_opp_carry x|] = wB - [|x|] - 1.
+ Lemma spec_opp_carry : forall x, [|0 - x - 1|] = wB - [|x|] - 1.
  Proof.
- clear; unfold w_opp_carry, znz_opp_carry, int31_op; intros.
- unfold sub31.
+ unfold sub31; intros.
  repeat rewrite phi_phi_inv.
  change [|1|] with 1; change [|0|] with 0.
  rewrite <- (Z_mod_plus_full (0-[|x|]) 1 wB).
  rewrite Zminus_mod_idemp_l.
- rewrite Zmod_small; generalize (spec_to_Z x); romega.
+ rewrite Zmod_small; generalize (phi_bounded x); romega.
  Qed.
 
- Lemma spec_pred_c : forall x, [-|w_pred_c x|] = [|x|] - 1.
+ Lemma spec_pred_c : forall x, [-|sub31c x 1|] = [|x|] - 1.
  Proof.
- clear -w_sub_c; unfold w_pred_c; simpl; intros.
- apply spec_sub_c.
+ intros; apply spec_sub_c.
  Qed.
 
- Lemma spec_pred : forall x, [|w_pred x|] = ([|x|] - 1) mod wB.
+ Lemma spec_pred : forall x, [|x-1|] = ([|x|] - 1) mod wB.
  Proof.
- clear -w_sub; unfold w_pred; simpl; intros.
- apply spec_sub.
+ intros; apply spec_sub.
  Qed.
 
  (** Multiplication *)
 
- Let w_mul_c       := int31_op.(znz_mul_c).
- Let w_mul         := int31_op.(znz_mul).
- Let w_square_c    := int31_op.(znz_square_c).
-
  Lemma phi2_phi_inv2 : forall x, [||phi_inv2 x||] = x mod (wB^2).
  Proof.
  assert (forall z, (z / wB) mod wB * wB + z mod wB = z mod wB ^ 2).
@@ -1513,54 +1431,37 @@ Section Int31_Spec.
   change base with wB; auto.
  Qed.
 
- Lemma spec_mul_c : forall x y, [|| w_mul_c x y ||] = [|x|] * [|y|].
+ Lemma spec_mul_c : forall x y, [|| mul31c x y ||] = [|x|] * [|y|].
  Proof.
- clear; unfold w_mul_c; simpl; intros.
- unfold mul31c.
+ unfold mul31c; intros.
  rewrite phi2_phi_inv2.
  apply Zmod_small.
- generalize (spec_to_Z x)(spec_to_Z y); intros.
+ generalize (phi_bounded x)(phi_bounded y); intros.
  change (wB^2) with (wB * wB).
  auto using Zmult_lt_compat with zarith.
  Qed.
 
- Lemma spec_mul : forall x y, [|w_mul x y|] = ([|x|] * [|y|]) mod wB.
+ Lemma spec_mul : forall x y, [|x*y|] = ([|x|] * [|y|]) mod wB.
  Proof.
- clear; unfold w_mul; simpl; intros.
- apply phi_phi_inv.
+ intros; apply phi_phi_inv.
  Qed.
 
- Lemma spec_square_c : forall x, [|| w_square_c x||] = [|x|] * [|x|].
+ Lemma spec_square_c : forall x, [|| mul31c x x ||] = [|x|] * [|x|].
  Proof.
- clear -w_mul_c; unfold w_square_c; simpl; intros.
- apply spec_mul_c.
+ intros; apply spec_mul_c.
  Qed.
 
  (** Division *) 
 
- Let w_div21       := int31_op.(znz_div21).
- Let w_div_gt      := int31_op.(znz_div_gt).
- Let w_div         := int31_op.(znz_div).
-
- Let w_mod_gt      := int31_op.(znz_mod_gt).
- Let w_mod         := int31_op.(znz_mod).
- Let w_gcd_gt      := int31_op.(znz_gcd_gt).
- Let w_gcd         := int31_op.(znz_gcd).
-
- Let w_add_mul_div := int31_op.(znz_add_mul_div).
-
- Let w_pos_mod     := int31_op.(znz_pos_mod).
-
  Lemma spec_div21 : forall a1 a2 b,
       wB/2 <= [|b|] ->
       [|a1|] < [|b|] ->
-      let (q,r) := w_div21 a1 a2 b in
+      let (q,r) := div3121 a1 a2 b in
       [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\
       0 <= [|r|] < [|b|].
  Proof.
- unfold w_div21, znz_div21; simpl; unfold div3121.
- intros.
- generalize (spec_to_Z a1)(spec_to_Z a2)(spec_to_Z b); intros.
+ unfold div3121; intros.
+ generalize (phi_bounded a1)(phi_bounded a2)(phi_bounded b); intros.
  assert ([|b|]>0) by (auto with zarith).
  generalize (Z_div_mod (phi2 a1 a2) [|b|] H4) (Z_div_pos (phi2 a1 a2) [|b|] H4).
  unfold Zdiv; destruct (Zdiv_eucl (phi2 a1 a2) [|b|]); simpl.
@@ -1589,19 +1490,18 @@ Section Int31_Spec.
  Qed.
 
  Lemma spec_div : forall a b, 0 < [|b|] ->
-      let (q,r) := w_div a b in
+      let (q,r) := div31 a b in
       [|a|] = [|q|] * [|b|] + [|r|] /\
       0 <= [|r|] < [|b|].
  Proof.
- intros.
- unfold w_div, znz_div; simpl; unfold div31.
+ unfold div31; intros.
  assert ([|b|]>0) by (auto with zarith).
  generalize (Z_div_mod [|a|] [|b|] H0) (Z_div_pos [|a|] [|b|] H0).
  unfold Zdiv; destruct (Zdiv_eucl [|a|] [|b|]); simpl.
  rewrite ?phi_phi_inv.
  destruct 1; intros.
  rewrite H1, Zmult_comm.
- generalize (spec_to_Z a)(spec_to_Z b); intros.
+ generalize (phi_bounded a)(phi_bounded b); intros.
  replace (z0 mod wB) with z0 by (symmetry; apply Zmod_small; omega).
  replace (z mod wB) with z; auto with zarith.
   symmetry; apply Zmod_small.
@@ -1612,61 +1512,118 @@ Section Int31_Spec.
   rewrite <- (Zmult_1_l z) at 1.
   apply Zmult_le_compat; auto with zarith.
  Qed.
- Lemma spec_div_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] ->
-      let (q,r) := w_div_gt a b in
-      [|a|] = [|q|] * [|b|] + [|r|] /\
-      0 <= [|r|] < [|b|].
- Proof.
- intros; apply spec_div; auto.
- Qed.
 
  Lemma spec_mod :  forall a b, 0 < [|b|] ->
-      [|w_mod a b|] = [|a|] mod [|b|].
+      [|let (_,r) := (a/b)%int31 in r|] = [|a|] mod [|b|].
  Proof.
- intros.
- unfold w_mod, znz_mod; simpl; unfold div31.
+ unfold div31; intros.
  assert ([|b|]>0) by (auto with zarith).
  unfold Zmod.
  generalize (Z_div_mod [|a|] [|b|] H0).
  destruct (Zdiv_eucl [|a|] [|b|]); simpl.
  rewrite ?phi_phi_inv.
  destruct 1; intros.
- generalize (spec_to_Z b); intros.
+ generalize (phi_bounded b); intros.
  apply Zmod_small; omega.
  Qed.
- Lemma spec_mod_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] ->
-      [|w_mod_gt a b|] = [|a|] mod [|b|].
- Proof.
- intros; apply spec_mod; auto.
- Qed.
 
- Lemma spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|w_gcd a b|].
+ Lemma spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd31 a b|].
  Proof.
  Admitted. (* TODO !! *)
  Opaque gcd31.
- Lemma spec_gcd_gt : forall a b, [|a|] > [|b|] ->
-      Zis_gcd [|a|] [|b|] [|w_gcd_gt a b|].
- Proof. 
- intros; apply spec_gcd; auto.
+
+ Lemma Zmod_eq_full : forall a b, b<>0 -> 
+  a mod b = a - (a/b)*b.
+ Proof.
+ intros.
+ rewrite <- Zeq_plus_swap, Zplus_comm, Zmult_comm; symmetry.
+ apply Z_div_mod_eq_full; auto.
+ Qed.
+
+ Lemma Zmod_eq : forall a b, b>0 -> 
+  a mod b = a - (a/b)*b.
+ Proof.
+ intros.
+ rewrite <- Zeq_plus_swap, Zplus_comm, Zmult_comm; symmetry.
+ apply Z_div_mod_eq; auto.
+ Qed.
+
+ Lemma shift_unshift_mod_2 : forall n p a, (0<=p<=n)%Z -> 
+   ((a * 2 ^ (n - p)) mod (2^n) / 2 ^ (n - p)) mod (2^n) = 
+   a mod 2 ^ p.
+ Proof.
+ intros.
+ rewrite Zmod_small.
+ rewrite Zmod_eq by (auto with zarith).
+ unfold Zminus at 1.
+ rewrite BigNumPrelude.Z_div_plus_l by (auto with zarith).
+ assert (2^n = 2^(n-p)*2^p).
+  rewrite <- Zpower_exp by (auto with zarith).
+  replace (n-p+p) with n; auto with zarith.
+ rewrite H0.
+ rewrite <- Zdiv_Zdiv, Z_div_mult by (auto with zarith).
+ rewrite (Zmult_comm (2^(n-p))), Zmult_assoc.
+ rewrite Zopp_mult_distr_l.
+ rewrite Z_div_mult by (auto with zarith).
+ symmetry; apply Zmod_eq; auto with zarith.
+
+ remember (a * 2 ^ (n - p)) as b.
+ destruct (Z_mod_lt b (2^n)); auto with zarith.
+ split.
+ apply Z_div_pos; auto with zarith.
+ apply Zdiv_lt_upper_bound; auto with zarith.
+ apply Zlt_le_trans with (2^n); auto with zarith.
+ rewrite <- (Zmult_1_r (2^n)) at 1.
+ apply Zmult_le_compat; auto with zarith.
+ cut (0 < 2 ^ (n-p)); auto with zarith.
  Qed.
 
  Lemma spec_add_mul_div : forall x y p,
        [|p|] <= Zpos 31 ->
-       [| w_add_mul_div p x y |] =
+       [| addmuldiv31 p x y |] =
          ([|x|] * (2 ^ [|p|]) +
           [|y|] / (2 ^ ((Zpos 31) - [|p|]))) mod wB.
  Admitted. (* TODO !! *)
+
+ Let w_pos_mod     := int31_op.(znz_pos_mod).
+
  Lemma spec_pos_mod : forall w p,
        [|w_pos_mod p w|] = [|w|] mod (2 ^ [|p|]).
- Admitted. (* TODO !! *)
+ Proof.
+ unfold w_pos_mod, znz_pos_mod, int31_op, compare31.
+ change [|31|] with 31%Z.
+ assert (forall w p, 31<=p -> [|w|] = [|w|] mod 2^p).
+  intros.
+  generalize (phi_bounded w).
+  symmetry; apply Zmod_small.
+  split; auto with zarith.
+  apply Zlt_le_trans with wB; auto with zarith.
+  apply Zpow_facts.Zpower_le_monotone; auto with zarith.
+ intros.
+ case_eq ([|p|] ?= 31); intros; 
+  [ apply H; rewrite (Zcompare_Eq_eq _ _ H0); auto with zarith | | 
+    apply H; change ([|p|]>31)%Z in H0; auto with zarith ].
+ change ([|p|]<31) in H0.
+ rewrite spec_add_mul_div by auto with zarith.
+ change [|0|] with 0%Z; rewrite Zmult_0_l, Zplus_0_l.
+ generalize (phi_bounded p)(phi_bounded w); intros.
+ assert (31-[|p|]<wB).
+  apply Zle_lt_trans with 31%Z; auto with zarith.
+  compute; auto.
+ assert ([|31-p|]=31-[|p|]).
+  unfold sub31; rewrite phi_phi_inv.
+  change [|31|] with 31%Z.
+  apply Zmod_small; auto with zarith.
+ rewrite spec_add_mul_div by (rewrite H4; auto with zarith).
+ change [|0|] with 0%Z; rewrite Zdiv_0_l, Zplus_0_r.
+ rewrite H4.
+ apply shift_unshift_mod_2; auto with zarith.
+ Qed.
 
- (** Shift operations *)
 
- Let w_head0       := int31_op.(znz_head0).
- Let w_tail0       := int31_op.(znz_tail0).
- 
+ (** Shift operations *)
 
- Lemma spec_head00:  forall x, [|x|] = 0 -> [|w_head0 x|] = Zpos 31.
+ Lemma spec_head00:  forall x, [|x|] = 0 -> [|head031 x|] = Zpos 31.
  Proof.
   intros.
   generalize (phi_inv_phi x).
@@ -1675,9 +1632,9 @@ Section Int31_Spec.
   simpl; auto.
  Qed.
  Lemma spec_head0  : forall x,  0 < [|x|] ->
-	 wB/ 2 <= 2 ^ ([|w_head0 x|]) * [|x|] < wB.
+	 wB/ 2 <= 2 ^ ([|head031 x|]) * [|x|] < wB.
  Admitted. (* TODO !! *)
- Lemma spec_tail00:  forall x, [|x|] = 0 -> [|w_tail0 x|] = Zpos 31.
+ Lemma spec_tail00:  forall x, [|x|] = 0 -> [|tail031 x|] = Zpos 31.
  Proof.
   intros.
   generalize (phi_inv_phi x).
@@ -1686,23 +1643,69 @@ Section Int31_Spec.
   simpl; auto.
  Qed.
  Lemma spec_tail0  : forall x, 0 < [|x|] -> 
-         exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|w_tail0 x|]).
+         exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail031 x|]).
  Admitted. (* TODO !! *)
     
  (* Sqrt *)
 
- Let w_sqrt2       := int31_op.(znz_sqrt2).
- Let w_sqrt        := int31_op.(znz_sqrt).
-
  Lemma spec_sqrt2 : forall x y,
        wB/ 4 <= [|x|] ->
-       let (s,r) := w_sqrt2 x y in
+       let (s,r) := sqrt312 x y in
           [||WW x y||] = [|s|] ^ 2 + [+|r|] /\
           [+|r|] <= 2 * [|s|].
  Admitted. (* TODO !! *)
  Lemma spec_sqrt : forall x,
-       [|w_sqrt x|] ^ 2 <= [|x|] < ([|w_sqrt x|] + 1) ^ 2.
+       [|sqrt31 x|] ^ 2 <= [|x|] < ([|sqrt31 x|] + 1) ^ 2.
  Admitted. (* TODO !! *)
+
+ (** [iszero] *)
+
+ Let w_eq0         := int31_op.(znz_eq0).
+
+ Lemma spec_eq0 : forall x, w_eq0 x = true -> [|x|] = 0.
+ Proof.
+ clear; unfold w_eq0, znz_eq0; simpl.
+ unfold compare31; simpl; intros.
+ change [|0|] with 0 in H.
+ apply Zcompare_Eq_eq.
+ now destruct ([|x|] ?= 0).
+ Qed.
+
+ (** [WW] and variants *) 
+
+ Let wWW           := int31_op.(znz_WW).
+ Let w0W           := int31_op.(znz_0W).
+ Let wW0           := int31_op.(znz_W0).
+
+ Lemma spec_WW  : forall h l, [||wWW h l||] = [|h|] * wB + [|l|].
+ Proof.
+ clear; unfold wWW; simpl; intros.
+ unfold compare31 in *.
+ change [|0|] with 0.
+ case_eq ([|h|] ?= 0); simpl; auto.
+ case_eq ([|l|] ?= 0); simpl; auto.
+ intros.
+ rewrite (Zcompare_Eq_eq _ _ H); simpl.
+ rewrite (Zcompare_Eq_eq _ _ H0); simpl; auto.
+ Qed.
+
+ Lemma spec_0W  : forall l, [||w0W l||] = [|l|].
+ Proof.
+ clear; unfold w0W; simpl; intros.
+ unfold compare31 in *.
+ change [|0|] with 0.
+ case_eq ([|l|] ?= 0); simpl; auto.
+ intros; symmetry; apply Zcompare_Eq_eq; auto.
+ Qed.
+
+ Lemma spec_W0  : forall h, [||wW0 h||] = [|h|]*wB.
+ Proof.
+ clear; unfold wW0; simpl; intros.
+ unfold compare31 in *.
+ change [|0|] with 0.
+ case_eq ([|h|] ?= 0); simpl; auto with zarith.
+ intro H; rewrite (Zcompare_Eq_eq _ _ H); auto.
+ Qed.
   
  (* Even *)
  
@@ -1711,8 +1714,21 @@ Section Int31_Spec.
  Lemma spec_is_even : forall x,
       if w_is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1.
  Proof.
- clear; unfold w_is_even; simpl; intros.
- Admitted. (* TODO !! *)
+ unfold w_is_even; simpl; intros.
+ generalize (spec_div x 2).
+ destruct (x/2)%int31 as (q,r); intros.
+ unfold compare31.
+ change [|2|] with 2 in H.
+ change [|0|] with 0.
+ destruct H; auto with zarith.
+ replace ([|x|] mod 2) with [|r|].
+ destruct H; auto with zarith.
+ case_eq ([|r|] ?= 0)%Z; intros.
+ apply Zcompare_Eq_eq; auto.
+ change ([|r|] < 0)%Z in H; auto with zarith.
+ change ([|r|] > 0)%Z in H; auto with zarith.
+ apply Zmod_unique with [|q|]; auto with zarith.
+ Qed.
 
  (* The following definition is verrry slooow  
     without the two Opaque  (??) *)
@@ -1721,64 +1737,64 @@ Section Int31_Spec.
 
  Definition int31_spec : znz_spec int31_op.
   split.
-  exact    spec_to_Z.
-  exact    positive_to_int31_spec.
-  exact    spec_zdigits.
-  exact    spec_more_than_1_digit.
-
-  exact    spec_0.
-  exact    spec_1.  
-  exact    spec_Bm1.
-  exact    spec_WW.
-  exact    spec_0W. 
-  exact    spec_W0.
-
-  exact    spec_compare.
-  exact    spec_eq0.
-
-  exact    spec_opp_c. 
-  exact    spec_opp.
-  exact    spec_opp_carry.
-
-  exact    spec_succ_c.
-  exact    spec_add_c.
-  exact    spec_add_carry_c.
-  exact    spec_succ.
-  exact    spec_add.
-  exact    spec_add_carry.
-
-  exact    spec_pred_c.
-  exact    spec_sub_c.
-  exact    spec_sub_carry_c.
-  exact    spec_pred.
-  exact    spec_sub.
-  exact    spec_sub_carry.
-
-  exact    spec_mul_c.
-  exact    spec_mul.
-  exact    spec_square_c.
-
-  exact    spec_div21.
-  exact    spec_div_gt. 
-  exact    spec_div.
-
-  exact    spec_mod_gt.
-  exact    spec_mod.
-
-  exact    spec_gcd_gt.
-  exact    spec_gcd.
-
-  exact    spec_head00.
-  exact    spec_head0.
-  exact    spec_tail00. 
-  exact    spec_tail0.
-
-  exact    spec_add_mul_div.
-  exact    spec_pos_mod.
-
-  exact    spec_is_even.
-  exact    spec_sqrt2.
-  exact    spec_sqrt.
+  exact phi_bounded.
+  exact positive_to_int31_spec.
+  exact spec_zdigits.
+  exact spec_more_than_1_digit.
+
+  exact spec_0.
+  exact spec_1.  
+  exact spec_Bm1.
+  exact spec_WW.
+  exact spec_0W. 
+  exact spec_W0.
+
+  exact spec_compare.
+  exact spec_eq0.
+
+  exact spec_opp_c. 
+  exact spec_opp.
+  exact spec_opp_carry.
+
+  exact spec_succ_c.
+  exact spec_add_c.
+  exact spec_add_carry_c.
+  exact spec_succ.
+  exact spec_add.
+  exact spec_add_carry.
+
+  exact spec_pred_c.
+  exact spec_sub_c.
+  exact spec_sub_carry_c.
+  exact spec_pred.
+  exact spec_sub.
+  exact spec_sub_carry.
+
+  exact spec_mul_c.
+  exact spec_mul.
+  exact spec_square_c.
+
+  exact spec_div21.
+  intros; apply spec_div; auto.
+  exact spec_div.
+
+  intros; unfold int31_op; simpl; apply spec_mod; auto.
+  exact spec_mod.
+
+  intros; apply spec_gcd; auto.
+  exact spec_gcd.
+
+  exact spec_head00.
+  exact spec_head0.
+  exact spec_tail00. 
+  exact spec_tail0.
+
+  exact spec_add_mul_div.
+  exact spec_pos_mod.
+
+  exact spec_is_even.
+  exact spec_sqrt2.
+  exact spec_sqrt.
  Qed.
 
  Transparent gcd31.