BigZ now are proved

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

3 files changed, 378 insertions, 41 deletions

diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v
index 03402c53f..7ac69fb02 100644
--- a/theories/Ints/num/NMake.v
+++ b/theories/Ints/num/NMake.v
@@ -8,12 +8,12 @@ Require Import GenMul.
 Require Import GenDivn1.
 Require Import Wf_nat.
 
- (***************************************************************)
- (*                                                             *)
- (*        File automatically generated DO NOT EDIT             *)
- (*        Constructors: 13  Generated Proofs: false            *)
- (*                                                             *)
- (***************************************************************)
+(***************************************************************)
+(*                                                             *)
+(*        File automatically generated DO NOT EDIT             *)
+(*        Constructors: 13  Generated Proofs: false            *)
+(*                                                             *)
+(***************************************************************)
 
 Module Type W0Type.
  Parameter w : Set.
@@ -212,7 +212,7 @@ Module Make (W0:W0Type).
  Admitted.
 
 
- Theorem to_Z_pos: forall x, 0 <= [x].
+ Theorem spec_pos: forall x, 0 <= [x].
  Admitted.
 
  Section LevelAndIter.
@@ -1729,7 +1729,7 @@ Module Make (W0:W0Type).
     end
   end.
 
- Theorem succ_spec: forall n, [succ n] = [n] + 1.
+ Theorem spec_succ: forall n, [succ n] = [n] + 1.
  Admitted.
 
  (***************************************************************)
@@ -1949,7 +1949,7 @@ Module Make (W0:W0Type).
     end
   end.
 
- Let spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1.
+ Theorem spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1.
  Admitted.
  
  (***************************************************************)
@@ -2912,7 +2912,7 @@ Admitted.
  Theorem spec_div_eucl: forall x y,
       0 < [y] ->
       let (q,r) := div_eucl x y in
-      [q] = [x] / [y] /\ [r] = [x] mod [y].
+      ([q], [r]) = Zdiv_eucl [x] [y].
  Admitted.
 
  Definition div x y := fst (div_eucl x y).
@@ -3460,5 +3460,11 @@ Admitted.
    if is_even x then [x] mod 2 = 0 else [x] mod 2 = 1.
  Admitted.
 
+ Theorem spec_0: [zero] = 0.
+ Admitted.
+
+ Theorem spec_1: [one] = 1.
+ Admitted.
+
 End Make.
 
diff --git a/theories/Ints/num/ZMake.v b/theories/Ints/num/ZMake.v
index f79b5478b..7fe5b1088 100644
--- a/theories/Ints/num/ZMake.v
+++ b/theories/Ints/num/ZMake.v
@@ -1,4 +1,8 @@
 Require Import ZArith.
+Require Import ZAux.
+Require Import ZDivModAux.
+
+Open Scope Z_scope.
 
 Module Type NType.
 
@@ -9,25 +13,79 @@ Module Type NType.
 
  Parameter of_N : N -> t.
  Parameter to_Z : t -> Z.
+ Parameter spec_pos: forall x, 0 <= to_Z x.
+ Parameter spec_0: to_Z zero = 0.
+ Parameter spec_1: to_Z one = 1.
+ Parameter spec_of_N: forall x, to_Z (of_N x) = Z_of_N x.
 
  Parameter compare : t -> t -> comparison.
+
+ Parameter spec_compare: forall x y,
+    match compare x y with
+      Eq => to_Z x = to_Z y
+    | Lt => to_Z x < to_Z y
+    | Gt => to_Z x > to_Z y
+    end.
+
  Parameter eq_bool : t -> t -> bool.
 
+ Parameter spec_eq_bool: forall x y,
+    if eq_bool x y then to_Z x = to_Z y else to_Z x <> to_Z y.
+ 
  Parameter succ : t -> t.
+
+ Parameter spec_succ: forall n, to_Z (succ n) = to_Z n + 1.
+
  Parameter add  : t -> t -> t.
+
+ Parameter spec_add: forall x y, to_Z (add x y) = to_Z x +  to_Z y.
+
  Parameter pred : t -> t.
+
+ Parameter spec_pred: forall x, 0 < to_Z x -> to_Z (pred x) = to_Z x - 1.
+
  Parameter sub  : t -> t -> t.
 
+ Parameter spec_sub: forall x y, to_Z y <= to_Z x ->
+   to_Z (sub x y) = to_Z x - to_Z y.
+
  Parameter mul       : t -> t -> t.
+
+ Parameter spec_mul: forall x y, to_Z (mul x y) = to_Z x * to_Z y.
+
  Parameter square    : t -> t.
+
+ Parameter spec_square: forall x, to_Z (square x) = to_Z x *  to_Z x.
+
  Parameter power_pos : t -> positive -> t.
+
+ Parameter spec_power_pos: forall x n, to_Z (power_pos x n) = to_Z x ^ Zpos n.
+
  Parameter sqrt      : t -> t.
 
+ Parameter spec_sqrt: forall x, to_Z (sqrt x) ^ 2 <= to_Z x < (to_Z (sqrt x) + 1) ^ 2.
+
  Parameter div_eucl : t -> t -> t * t.
+
+ Parameter spec_div_eucl: forall x y,
+      0 < to_Z y ->
+      let (q,r) := div_eucl x y in (to_Z q, to_Z r) = (Zdiv_eucl (to_Z x) (to_Z y)).
+ 
  Parameter div      : t -> t -> t.
+
+ Parameter spec_div: forall x y,
+      0 < to_Z y -> to_Z (div x y) = to_Z x / to_Z y.
+
  Parameter modulo   : t -> t -> t.
+
+ Parameter spec_modulo:
+   forall x y, 0 < to_Z y -> to_Z (modulo x y) = to_Z x mod to_Z y.
+
  Parameter gcd      : t -> t -> t.
 
+ Parameter spec_gcd: forall a b, to_Z (gcd a b) = Zgcd (to_Z a) (to_Z b).
+
+
 End NType.
 
 Module Make (N:NType).
@@ -55,6 +113,18 @@ Module Make (N:NType).
   | Neg nx => Zopp (N.to_Z nx)
   end.
 
+ Theorem spec_0: to_Z zero = 0.
+ exact N.spec_0.
+ Qed.
+
+ Theorem spec_1: to_Z one = 1.
+ exact N.spec_1.
+ Qed.
+
+ Theorem spec_m1: to_Z minus_one = -1.
+ simpl; rewrite N.spec_1; auto.
+ Qed.
+
  Definition compare x y :=
   match x, y with
   | Pos nx, Pos ny => N.compare nx ny
@@ -71,12 +141,43 @@ Module Make (N:NType).
   | Neg nx, Neg ny => N.compare ny nx
   end.
 
+
+ Theorem spec_compare: forall x y,
+    match compare x y with
+      Eq => to_Z x = to_Z y
+    | Lt => to_Z x < to_Z y
+    | Gt => to_Z x > to_Z y
+    end.
+  unfold compare, to_Z; intros x y; case x; case y; clear x y;
+    intros x y; auto; generalize (N.spec_pos x) (N.spec_pos y).
+  generalize (N.spec_compare y x); case N.compare; auto with zarith.
+  generalize (N.spec_compare y N.zero); case N.compare; 
+     try rewrite N.spec_0; auto with zarith.
+  generalize (N.spec_compare x N.zero); case N.compare;
+   rewrite N.spec_0; auto with zarith.
+  generalize (N.spec_compare x N.zero); case N.compare;
+   rewrite N.spec_0; auto with zarith.
+  generalize (N.spec_compare N.zero y); case N.compare; 
+     try rewrite N.spec_0; auto with zarith.
+  generalize (N.spec_compare N.zero x); case N.compare;
+   rewrite N.spec_0; auto with zarith.
+  generalize (N.spec_compare N.zero x); case N.compare;
+   rewrite N.spec_0; auto with zarith.
+  generalize (N.spec_compare x y); case N.compare; auto with zarith.
+  Qed.
+
  Definition eq_bool x y := 
   match compare x y with
   | Eq => true
   | _ => false
   end.
 
+ Theorem spec_eq_bool: forall x y,
+    if eq_bool x y then to_Z x = to_Z y else to_Z x <> to_Z y.
+ intros x y; unfold eq_bool;
+   generalize (spec_compare x y); case compare; auto with zarith.
+ Qed.
+
  Definition cmp_sign x y :=
   match x, y with
   | Pos nx, Neg ny => 
@@ -93,12 +194,22 @@ Module Make (N:NType).
   end.
 
  Definition abs x := Pos (to_N x).
+
+ Theorem spec_abs: forall x, to_Z (abs x) = Zabs (to_Z x).
+ intros x; case x; clear x; intros x; assert (F:=N.spec_pos x).
+    simpl; rewrite Zabs_eq; auto.
+ simpl; rewrite Zabs_non_eq; simpl; auto with zarith.
+ Qed.
  
  Definition opp x := 
   match x with 
   | Pos nx => Neg nx
   | Neg nx => Pos nx
   end.
+
+ Theorem spec_opp: forall x, to_Z (opp x) = - to_Z x.
+ intros x; case x; simpl; auto with zarith.
+ Qed.
     
  Definition succ x :=
   match x with
@@ -110,6 +221,16 @@ Module Make (N:NType).
     end
   end.
 
+ Theorem spec_succ: forall n, to_Z (succ n) = to_Z n + 1.
+ intros x; case x; clear x; intros x.
+   exact (N.spec_succ x).
+ simpl; generalize (N.spec_compare N.zero x); case N.compare; 
+   rewrite N.spec_0; simpl.
+  intros HH; rewrite <- HH; rewrite N.spec_1; ring.
+  intros HH; rewrite N.spec_pred; auto with zarith.
+ generalize (N.spec_pos x); auto with zarith.
+ Qed.
+
  Definition add x y :=
   match x, y with
   | Pos nx, Pos ny => Pos (N.add nx ny)
@@ -127,6 +248,20 @@ Module Make (N:NType).
     end
   | Neg nx, Neg ny => Neg (N.add nx ny)
   end.
+  
+ Theorem spec_add: forall x y, to_Z (add x y) = to_Z x +  to_Z y.
+ unfold add, to_Z; intros [x | x] [y | y].
+   exact (N.spec_add x y).
+ unfold zero; generalize (N.spec_compare x y); case N.compare.
+   rewrite N.spec_0; auto with zarith.
+ intros; rewrite N.spec_sub; try ring; auto with zarith.
+ intros; rewrite N.spec_sub; try ring; auto with zarith.
+ unfold zero; generalize (N.spec_compare x y); case N.compare.
+   rewrite N.spec_0; auto with zarith.
+ intros; rewrite N.spec_sub; try ring; auto with zarith.
+ intros; rewrite N.spec_sub; try ring; auto with zarith.
+ intros; rewrite N.spec_add; try ring; auto with zarith.
+ Qed.
 
  Definition pred x :=
   match x with
@@ -138,6 +273,15 @@ Module Make (N:NType).
   | Neg nx => Neg (N.succ nx)
   end.
 
+ Theorem spec_pred: forall x, to_Z (pred x) = to_Z x - 1.
+ unfold pred, to_Z, minus_one; intros [x | x].
+   generalize (N.spec_compare N.zero x); case N.compare; 
+     rewrite N.spec_0; try rewrite N.spec_1; auto with zarith.
+   intros H; exact (N.spec_pred _ H).
+ generalize (N.spec_pos x); auto with zarith.
+ rewrite N.spec_succ; ring.
+ Qed.
+
  Definition sub x y :=
   match x, y with
   | Pos nx, Pos ny => 
@@ -156,6 +300,20 @@ Module Make (N:NType).
     end
   end.
 
+ Theorem spec_sub: forall x y, to_Z (sub x y) = to_Z x - to_Z y.
+ unfold sub, to_Z; intros [x | x] [y | y].
+ unfold zero; generalize (N.spec_compare x y); case N.compare.
+   rewrite N.spec_0; auto with zarith.
+ intros; rewrite N.spec_sub; try ring; auto with zarith.
+ intros; rewrite N.spec_sub; try ring; auto with zarith.
+ rewrite N.spec_add; ring.
+ rewrite N.spec_add; ring.
+ unfold zero; generalize (N.spec_compare x y); case N.compare.
+   rewrite N.spec_0; auto with zarith.
+ intros; rewrite N.spec_sub; try ring; auto with zarith.
+ intros; rewrite N.spec_sub; try ring; auto with zarith.
+ Qed.
+
  Definition mul x y := 
   match x, y with
   | Pos nx, Pos ny => Pos (N.mul nx ny)
@@ -164,12 +322,21 @@ Module Make (N:NType).
   | Neg nx, Neg ny => Pos (N.mul nx ny)
   end.
 
+
+ Theorem spec_mul: forall x y, to_Z (mul x y) = to_Z x * to_Z y.
+ unfold mul, to_Z; intros [x | x] [y | y]; rewrite N.spec_mul; ring.
+ Qed.
+
  Definition square x := 
   match x with
   | Pos nx => Pos (N.square nx)
   | Neg nx => Pos (N.square nx)
   end.
 
+ Theorem spec_square: forall x, to_Z (square x) = to_Z x *  to_Z x.
+ unfold square, to_Z; intros [x | x]; rewrite N.spec_square; ring.
+ Qed.
+
  Definition power_pos x p :=
   match x with
   | Pos nx => Pos (N.power_pos nx p)
@@ -181,12 +348,40 @@ Module Make (N:NType).
     end
   end.
 
+ Theorem spec_power_pos: forall x n, to_Z (power_pos x n) = to_Z x ^ Zpos n.
+ 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.
+ assert (F: 0 <= 2 * Zpos p).
+  assert (0 <= Zpos p); auto with zarith.
+ rewrite Zpos_xI; repeat rewrite Zpower_exp; auto with zarith.
+ repeat rewrite Zpower_mult; auto with zarith.
+ rewrite F0; ring.
+ assert (F: 0 <= 2 * Zpos p).
+  assert (0 <= Zpos p); auto with zarith.
+ rewrite Zpos_xO; repeat rewrite Zpower_exp; auto with zarith.
+ repeat rewrite Zpower_mult; auto with zarith.
+ rewrite F0; ring.
+ Qed.
+
  Definition sqrt x :=
   match x with
   | Pos nx => Pos (N.sqrt nx)
   | 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.
+ 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.
+ Qed.
+
  Definition div_eucl x y :=
   match x, y with
   | Pos nx, Pos ny =>
@@ -194,7 +389,10 @@ Module Make (N:NType).
     (Pos q, Pos r)
   | Pos nx, Neg ny =>
     let (q, r) := N.div_eucl nx ny in
-    (Neg q, Pos r)
+    match N.compare N.zero r with
+    | Eq => (Neg q, zero)
+    | _ => (Neg (N.succ q), Neg (N.sub ny r))
+    end
   | Neg nx, Pos ny =>
     let (q, r) := N.div_eucl nx ny in
     match N.compare N.zero r with
@@ -203,16 +401,114 @@ Module Make (N:NType).
     end
   | Neg nx, Neg ny =>
     let (q, r) := N.div_eucl nx ny in
-    match N.compare N.zero r with
-    | Eq => (Pos q, zero)
-    | _ => (Pos (N.succ q), Pos (N.sub ny r))
-    end
+    (Pos q, Neg r)
   end.
 
+
+ Theorem spec_div_eucl: forall x y,
+      to_Z y <> 0 ->
+      let (q,r) := div_eucl x y in
+      (to_Z q, to_Z r) = Zdiv_eucl (to_Z x) (to_Z y).
+ unfold div_eucl, to_Z; intros [x | x] [y | y] H.
+ assert (H1: 0 < N.to_Z y).
+   generalize (N.spec_pos y); auto with zarith.
+ generalize (N.spec_div_eucl x y H1); case N.div_eucl; auto.
+ assert (HH: 0 < N.to_Z y).
+   generalize (N.spec_pos y); auto with zarith.
+ generalize (N.spec_div_eucl x y HH); case N.div_eucl; auto.
+ intros q r; generalize (N.spec_pos x) HH; unfold Zdiv_eucl;
+   case_eq (N.to_Z x); case_eq (N.to_Z y); 
+     try (intros; apply False_ind; auto with zarith; fail).
+ intros p He1 He2 _ _ H1; injection H1; intros H2 H3.
+ generalize (N.spec_compare N.zero r); case N.compare;
+   unfold zero; rewrite N.spec_0; try rewrite H3; auto.
+ rewrite H2; intros; apply False_ind; auto with zarith.
+ rewrite H2; intros; apply False_ind; auto with zarith.
+ intros p _ _ _ H1; discriminate H1.
+ intros p He p1 He1 H1 _.
+ generalize (N.spec_compare N.zero r); case N.compare.
+ change (- Zpos p) with (Zneg p).
+ unfold zero; lazy zeta.
+ rewrite N.spec_0; intros H2; rewrite <- H2.
+ intros H3; rewrite <- H3; auto.
+ rewrite N.spec_0; intros H2.
+ change (- Zpos p) with (Zneg p); lazy iota beta.
+ intros H3; rewrite <- H3; auto.
+ rewrite N.spec_succ; rewrite N.spec_sub.
+ generalize H2; case (N.to_Z r).
+ intros; apply False_ind; auto with zarith.
+ intros p2 _; rewrite He; auto with zarith.
+ change (Zneg p) with (- (Zpos p)); apply f_equal2 with (f := @pair Z Z); ring.
+ intros p2 H4; discriminate H4.
+ assert (N.to_Z r = (Zpos p1 mod (Zpos p))).
+   unfold Zmod, Zdiv_eucl; rewrite <- H3; auto.
+ case (Z_mod_lt (Zpos p1) (Zpos p)); auto with zarith.
+ rewrite N.spec_0; intros H2; generalize (N.spec_pos r); 
+   intros; apply False_ind; auto with zarith.
+ assert (HH: 0 < N.to_Z y).
+   generalize (N.spec_pos y); auto with zarith.
+ generalize (N.spec_div_eucl x y HH); case N.div_eucl; auto.
+ intros q r; generalize (N.spec_pos x) HH; unfold Zdiv_eucl;
+   case_eq (N.to_Z x); case_eq (N.to_Z y); 
+     try (intros; apply False_ind; auto with zarith; fail).
+ intros p He1 He2 _ _ H1; injection H1; intros H2 H3.
+ generalize (N.spec_compare N.zero r); case N.compare;
+   unfold zero; rewrite N.spec_0; try rewrite H3; auto.
+ rewrite H2; intros; apply False_ind; auto with zarith.
+ rewrite H2; intros; apply False_ind; auto with zarith.
+ intros p _ _ _ H1; discriminate H1.
+ intros p He p1 He1 H1 _.
+ generalize (N.spec_compare N.zero r); case N.compare.
+ change (- Zpos p1) with (Zneg p1).
+ unfold zero; lazy zeta.
+ rewrite N.spec_0; intros H2; rewrite <- H2.
+ intros H3; rewrite <- H3; auto.
+ rewrite N.spec_0; intros H2.
+ change (- Zpos p1) with (Zneg p1); lazy iota beta.
+ intros H3; rewrite <- H3; auto.
+ rewrite N.spec_succ; rewrite N.spec_sub.
+ generalize H2; case (N.to_Z r).
+ intros; apply False_ind; auto with zarith.
+ intros p2 _; rewrite He; auto with zarith.
+ intros p2 H4; discriminate H4.
+ assert (N.to_Z r = (Zpos p1 mod (Zpos p))).
+   unfold Zmod, Zdiv_eucl; rewrite <- H3; auto.
+ case (Z_mod_lt (Zpos p1) (Zpos p)); auto with zarith.
+ rewrite N.spec_0; generalize (N.spec_pos r); intros; apply False_ind; auto with zarith.
+ assert (H1: 0 < N.to_Z y).
+   generalize (N.spec_pos y); auto with zarith.
+ generalize (N.spec_div_eucl x y H1); case N.div_eucl; auto.
+ intros q r; generalize (N.spec_pos x) H1; unfold Zdiv_eucl;
+   case_eq (N.to_Z x); case_eq (N.to_Z y); 
+     try (intros; apply False_ind; auto with zarith; fail).
+ change (-0) with 0; lazy iota beta; auto.
+ intros p _ _ _ _ H2; injection H2.
+ intros H3 H4; rewrite H3; rewrite H4; auto.
+ intros p _ _ _ H2; discriminate H2.
+ intros p He p1 He1 _ _  H2.
+ change (- Zpos p1) with (Zneg p1); lazy iota beta.
+ change (- Zpos p) with (Zneg p); lazy iota beta.
+ rewrite <- H2; auto.
+ Qed.
+
  Definition div x y := fst (div_eucl x y).
 
+ Definition spec_div: forall x y,
+     to_Z y <> 0 -> to_Z (div x y) = to_Z x / to_Z y.
+ intros x y H1; generalize (spec_div_eucl x y H1); unfold div, Zdiv.
+ case div_eucl; case Zdiv_eucl; simpl; auto.
+ intros q r q11 r1 H; injection H; auto.
+ Qed.
+
  Definition modulo x y := snd (div_eucl x y).
 
+ Theorem spec_modulo:
+   forall x y, to_Z y <> 0  -> to_Z (modulo x y) = to_Z x mod to_Z y.
+ intros x y H1; generalize (spec_div_eucl x y H1); unfold modulo, Zmod.
+ case div_eucl; case Zdiv_eucl; simpl; auto.
+ intros q r q11 r1 H; injection H; auto.
+ Qed.
+
  Definition gcd x y :=
   match x, y with
   | Pos nx, Pos ny => Pos (N.gcd nx ny)
@@ -221,4 +517,11 @@ Module Make (N:NType).
   | Neg nx, Neg ny => Pos (N.gcd nx ny) 
   end.
 
+ Theorem spec_gcd: forall a b, to_Z (gcd a b) = Zgcd (to_Z a) (to_Z b).
+ unfold gcd, Zgcd, to_Z; intros [x | x] [y | y]; rewrite N.spec_gcd; unfold Zgcd;
+  auto; case N.to_Z; simpl; auto with zarith;
+  try rewrite Zabs_Zopp; auto;
+  case N.to_Z; simpl; auto with zarith.
+ Qed.
+
 End Make.
diff --git a/theories/Ints/num/genN.ml b/theories/Ints/num/genN.ml
index 928a60402..936c61a65 100644
--- a/theories/Ints/num/genN.ml
+++ b/theories/Ints/num/genN.ml
@@ -44,12 +44,12 @@ let start_file post l =
 let print_Make () =
   let fmt = start_file "Make" [] in
 
-  fprintf fmt " (***************************************************************)\n";
-  fprintf fmt " (*                                                             *)\n";
-  fprintf fmt " (*        File automatically generated DO NOT EDIT             *)\n";
-  fprintf fmt " (*        Constructors: %i  Generated Proofs: %b          %s %s *)\n" size gen_proof (if size < 10 then " " else  "") (if gen_proof then " " else "");
-  fprintf fmt " (*                                                             *)\n";
-  fprintf fmt " (***************************************************************)\n\n";
+  fprintf fmt "(***************************************************************)\n";
+  fprintf fmt "(*                                                             *)\n";
+  fprintf fmt "(*        File automatically generated DO NOT EDIT             *)\n";
+  fprintf fmt "(*        Constructors: %i  Generated Proofs: %b          %s %s *)\n" size gen_proof (if size < 10 then " " else  "") (if gen_proof then " " else "");
+  fprintf fmt "(*                                                             *)\n";
+  fprintf fmt "(***************************************************************)\n\n";
 
 
   fprintf fmt "Module Type W0Type.\n";
@@ -138,6 +138,8 @@ let print_Make () =
   fprintf fmt " \n";
 
 
+
+
   if gen_proof then
   begin
   fprintf fmt " (* Regular make op (no karatsuba) *)\n";
@@ -454,7 +456,7 @@ let print_Make () =
 
 
 
-  fprintf fmt " Theorem to_Z_pos: forall x, 0 <= [x].\n";
+  fprintf fmt " Theorem spec_pos: forall x, 0 <= [x].\n";
   if gen_proof then
   begin
   fprintf fmt " Proof.\n";
@@ -1022,7 +1024,7 @@ let print_Make () =
   fprintf fmt "  end.\n";
   fprintf fmt "\n";
 
-  fprintf fmt " Theorem succ_spec: forall n, [succ n] = [n] + 1.\n";
+  fprintf fmt " Theorem spec_succ: forall n, [succ n] = [n] + 1.\n";
   if gen_proof then
   begin
   fprintf fmt " Proof.\n";
@@ -1157,7 +1159,7 @@ let print_Make () =
   fprintf fmt "  end.\n";
   fprintf fmt "\n";
 
-  fprintf fmt " Let spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1.\n";
+  fprintf fmt " Theorem spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1.\n";
   if gen_proof then
   begin
   fprintf fmt " Proof.\n";
@@ -2039,7 +2041,7 @@ let print_Make () =
   fprintf fmt " Theorem spec_div_eucl: forall x y,\n";
   fprintf fmt "      0 < [y] ->\n";
   fprintf fmt "      let (q,r) := div_eucl x y in\n";
-  fprintf fmt "      [q] = [x] / [y] /\\ [r] = [x] mod [y].\n";
+  fprintf fmt "      ([q], [r]) = Zdiv_eucl [x] [y].\n";
   if gen_proof then 
   begin
   fprintf fmt " Proof.\n";
@@ -2049,14 +2051,18 @@ let print_Make () =
   fprintf fmt "   exact (spec_1 w0_spec).\n";
   fprintf fmt " intros x y H; generalize (spec_compare x y);\n";
   fprintf fmt "   unfold div_eucl; case compare; try rewrite F0;\n";
-  fprintf fmt "   try rewrite F1; intros; try split; auto with zarith.\n";
-  fprintf fmt " rewrite H0; apply sym_equal; apply Z_div_same; auto with zarith.\n";
-  fprintf fmt " rewrite H0; apply sym_equal; apply Z_mod_same; auto with zarith.\n";
-  fprintf fmt " apply sym_equal; apply ZDivModAux.Zdiv_lt_0.\n";
-  fprintf fmt " generalize (to_Z_pos x); auto with zarith.\n";
-  fprintf fmt " apply sym_equal; apply ZAux.Zmod_def_small; auto with zarith.\n";
-  fprintf fmt " generalize (to_Z_pos x); auto with zarith.\n";
-  fprintf fmt " apply (spec_div_gt x y); auto.\n";
+  fprintf fmt "   try rewrite F1; intros; auto with zarith.\n";
+  fprintf fmt " rewrite H0; generalize (Z_div_same [y] (Zlt_gt _ _ H))\n";
+  fprintf fmt "                        (Z_mod_same [y] (Zlt_gt _ _ H));\n";
+  fprintf fmt "  unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto.\n";
+  fprintf fmt " assert (F2: 0 <= [x] < [y]).\n";
+  fprintf fmt "   generalize (spec_pos x); auto.\n";
+  fprintf fmt " generalize (ZDivModAux.Zdiv_lt_0 _ _ F2)\n";
+  fprintf fmt "            (Zmod_def_small _ _ F2);\n";
+  fprintf fmt "  unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto.\n";
+  fprintf fmt " generalize (spec_div_gt _ _ H0 H); auto.\n";
+  fprintf fmt " unfold Zdiv, Zmod; case Zdiv_eucl; case div_gt.\n";
+  fprintf fmt " intros a b c d (H1, H2); subst; auto.\n";
   fprintf fmt " Qed.\n";
   end
   else
@@ -2073,7 +2079,8 @@ let print_Make () =
   fprintf fmt " Proof.\n";
   fprintf fmt " intros x y H1; unfold div; generalize (spec_div_eucl x y H1);\n";
   fprintf fmt "   case div_eucl; simpl fst.\n";
-  fprintf fmt " intros xx yy (H2, H3); auto with zarith.\n";
+  fprintf fmt " intros xx yy; unfold Zdiv; case Zdiv_eucl; intros qq rr H; \n";
+  fprintf fmt "  injection H; auto.\n";
   fprintf fmt " Qed.\n";
   end
   else
@@ -2202,7 +2209,7 @@ let print_Make () =
   fprintf fmt "   try rewrite F1; intros; try split; auto with zarith.\n";
   fprintf fmt " rewrite H0; apply sym_equal; apply Z_mod_same; auto with zarith.\n";
   fprintf fmt " apply sym_equal; apply ZAux.Zmod_def_small; auto with zarith.\n";
-  fprintf fmt " generalize (to_Z_pos x); auto with zarith.\n";
+  fprintf fmt " generalize (spec_pos x); auto with zarith.\n";
   fprintf fmt " apply spec_mod_gt; auto.\n";
   fprintf fmt " Qed.\n";
   end
@@ -3122,10 +3129,10 @@ let print_Make () =
   begin
   fprintf fmt " Proof.\n";
   fprintf fmt " intros x.\n";
-  fprintf fmt " assert (F1:= to_Z_pos (head0 x)).\n";
+  fprintf fmt " assert (F1:= spec_pos (head0 x)).\n";
   fprintf fmt " assert (F2: 0 < Zpos (digits x)).\n";
   fprintf fmt "   red; auto.\n";
-  fprintf fmt " case (Zle_lt_or_eq _ _ (to_Z_pos x)); intros HH.\n";
+  fprintf fmt " case (Zle_lt_or_eq _ _ (spec_pos x)); intros HH.\n";
   fprintf fmt " generalize HH; rewrite <- (spec_double_size x); intros HH1.\n";
   fprintf fmt " case (spec_head0 x HH); intros _ HH2.\n";
   fprintf fmt " case (spec_head0 _ HH1).\n";
@@ -3136,7 +3143,7 @@ let print_Make () =
   fprintf fmt " apply Zle_not_lt.\n";
   fprintf fmt " apply Zmult_le_compat_r; auto with zarith.\n";
   fprintf fmt " apply Zpower_le_monotone; auto; auto with zarith.\n";
-  fprintf fmt " generalize (to_Z_pos (head0 (double_size x))); auto with zarith.\n";
+  fprintf fmt " generalize (spec_pos (head0 (double_size x))); auto with zarith.\n";
   fprintf fmt " assert (HH5: 2 ^[head0 x] <= 2 ^(Zpos (digits x) - 1)).\n";
   fprintf fmt "   case (Zle_lt_or_eq 1 [x]); auto with zarith; intros HH5.\n";
   fprintf fmt "   apply Zmult_le_reg_r with (2 ^ 1); auto with zarith.\n";
@@ -3182,10 +3189,10 @@ let print_Make () =
   fprintf fmt " intros x.\n";
   fprintf fmt " assert (F: 0 < Zpos (digits x)).\n";
   fprintf fmt "  red; auto.\n";
-  fprintf fmt " case (Zle_lt_or_eq _ _ (to_Z_pos (head0 (double_size x)))); auto; intros F0.\n";
-  fprintf fmt " case (Zle_lt_or_eq _ _ (to_Z_pos (head0 x))); intros F1.\n";
+  fprintf fmt " case (Zle_lt_or_eq _ _ (spec_pos (head0 (double_size x)))); auto; intros F0.\n";
+  fprintf fmt " case (Zle_lt_or_eq _ _ (spec_pos (head0 x))); intros F1.\n";
   fprintf fmt "   apply Zlt_le_trans with (2 := (spec_double_size_head0 x)); auto with zarith.\n";
-  fprintf fmt " case (Zle_lt_or_eq _ _ (to_Z_pos x)); intros F3.\n";
+  fprintf fmt " case (Zle_lt_or_eq _ _ (spec_pos x)); intros F3.\n";
   fprintf fmt " generalize F3; rewrite <- (spec_double_size x); intros F4.\n";
   fprintf fmt " absurd (2 ^ (Zpos (xO (digits x)) - 1) < 2 ^ (Zpos (digits x))).\n";
   fprintf fmt "   apply Zle_not_lt.\n";
@@ -3352,6 +3359,27 @@ let print_Make () =
   fprintf fmt " Admitted.\n";
   fprintf fmt "\n";
 
+  fprintf fmt " Theorem spec_0: [zero] = 0.\n";
+  if gen_proof then
+  begin
+  fprintf fmt " Proof.\n";
+  fprintf fmt " exact (spec_0 w0_spec).\n";
+  fprintf fmt " Qed.\n";
+  end
+  else
+  fprintf fmt " Admitted.\n";
+  fprintf fmt "\n";
+
+  fprintf fmt " Theorem spec_1: [one] = 1.\n";
+  if gen_proof then
+  begin
+  fprintf fmt " Proof.\n";
+  fprintf fmt " exact (spec_1 w0_spec).\n";
+  fprintf fmt " Qed.\n";
+  end
+  else
+  fprintf fmt " Admitted.\n";
+  fprintf fmt "\n";
 
 
   fprintf fmt "End Make.\n";