Correct height computation

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

3 files changed, 105 insertions, 13 deletions

diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v
index dbc893c84..0b5e72295 100644
--- a/theories/Ints/num/NMake.v
+++ b/theories/Ints/num/NMake.v
@@ -8,15 +8,6 @@ Require Import GenDivn1.
 
 
 
-Fixpoint plength (p: positive) : positive :=
-  match p with 
-    xH => xH
-  | xO p1 => Psucc (plength p1)
-  | xI p1 => Psucc (plength p1)
-  end.
-
-Definition pheight p := plength (Ppred (plength (Ppred p))).
-
 Module Type W0Type.
  Parameter w : Set.
  Parameter w_op : znz_op w.
@@ -3450,8 +3441,10 @@ Module Make (W0:W0Type).
   | Gt => gcd_gt (digits a) gcd_cont a b
   end.
 
+ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (plength p))). 
+
  Definition of_pos x :=
-  let h := nat_of_P (pheight x) in
+  let h := pheight x in
   match h with
   | O => reduce_0 (snd (w0_op.(znz_of_pos) x))
   | (S O) => reduce_1 (snd (w1_op.(znz_of_pos) x))
diff --git a/theories/Ints/num/Nbasic.v b/theories/Ints/num/Nbasic.v
index 23229b52c..e2ce06425 100644
--- a/theories/Ints/num/Nbasic.v
+++ b/theories/Ints/num/Nbasic.v
@@ -1,6 +1,102 @@
 Require Import ZArith.
+Require Import ZAux.
+Require Import ZDivModAux.
 Require Import Basic_type.
 
+(* To compute the necessary height *)
+
+Fixpoint plength (p: positive) : positive :=
+  match p with 
+    xH => xH
+  | xO p1 => Psucc (plength p1)
+  | xI p1 => Psucc (plength p1)
+  end.
+
+Theorem plength_correct: forall p, (Zpos p < 2 ^ Zpos (plength p))%Z.
+assert (F: (forall p, 2 ^ (Zpos (Psucc p)) = 2 * 2 ^ Zpos p)%Z).
+intros p; replace (Zpos (Psucc p)) with (1 + Zpos p)%Z.
+rewrite Zpower_exp; auto with zarith.
+rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith.
+intros p; elim p; simpl plength; auto.
+intros p1 Hp1; rewrite F; repeat rewrite Zpos_xI.
+assert (tmp: (forall p, 2 * p = p + p)%Z); 
+  try repeat rewrite tmp; auto with zarith.
+intros p1 Hp1; rewrite F; rewrite (Zpos_xO p1).
+assert (tmp: (forall p, 2 * p = p + p)%Z); 
+  try repeat rewrite tmp; auto with zarith.
+rewrite ZPowerAux.Zpower_exp_1; auto with zarith.
+Qed.
+
+Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Ppred p)))%Z.
+intros p; case (Psucc_pred p); intros H1.
+subst; simpl plength.
+rewrite ZPowerAux.Zpower_exp_1; auto with zarith.
+pattern p at 1; rewrite <- H1.
+rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith.
+generalize (plength_correct (Ppred p)); auto with zarith.
+Qed.
+
+Definition Pdiv p q :=
+  match Zdiv (Zpos p) (Zpos q) with
+    Zpos q1 => match (Zpos p) - (Zpos q) * (Zpos q1) with
+                 Z0 => q1
+               | _ => (Psucc q1)
+               end
+  |  _ => xH
+  end.
+
+Theorem Pdiv_le: forall p q,
+  Zpos p <= Zpos q * Zpos (Pdiv p q).
+intros p q.
+unfold Pdiv.
+assert (H1: Zpos q > 0); auto with zarith.
+assert (H1b: Zpos p >= 0); auto with zarith.
+generalize (Z_div_ge0 (Zpos p) (Zpos q) H1 H1b).
+generalize (Z_div_mod_eq (Zpos p) (Zpos q) H1); case Zdiv.
+  intros HH _; rewrite HH; rewrite Zmult_0_r; rewrite Zmult_1_r; simpl.
+case (Z_mod_lt (Zpos p) (Zpos q) H1); auto with zarith.
+intros q1 H2.
+replace (Zpos p - Zpos q * Zpos q1) with (Zpos p mod Zpos q).
+  2: pattern (Zpos p) at 2; rewrite H2; auto with zarith.
+generalize H2 (Z_mod_lt (Zpos p) (Zpos q) H1); clear H2; 
+  case Zmod.
+  intros HH _; rewrite HH; auto with zarith.
+  intros r1 HH (_,HH1); rewrite HH; rewrite Zpos_succ_morphism.
+  unfold Zsucc; rewrite Zmult_plus_distr_r; auto with zarith.
+  intros r1 _ (HH,_); case HH; auto.
+intros q1 HH; rewrite HH.
+unfold Zge; simpl Zcompare; intros HH1; case HH1; auto.
+Qed.
+
+Definition is_one p := match p with xH => true | _ => false end.
+
+Theorem is_one_one: forall p, is_one p = true -> p = xH.
+intros p; case p; auto; intros p1 H1; discriminate H1.
+Qed.
+
+Definition get_height digits p :=
+  let r := Pdiv p digits in
+   if is_one r then xH else Psucc (plength (Ppred r)).
+
+Theorem get_height_correct:
+  forall digits N,
+   Zpos N <= Zpos digits * (2 ^ (Zpos (get_height digits N) -1)).
+intros digits N.
+unfold get_height.
+assert (H1 := Pdiv_le N digits).
+case_eq (is_one (Pdiv N digits)); intros H2.
+rewrite (is_one_one _ H2) in H1.
+rewrite Zmult_1_r in H1.
+change (2^(1-1))%Z with 1; rewrite Zmult_1_r; auto.
+clear H2.
+apply Zle_trans with (1 := H1).
+apply Zmult_le_compat_l; auto with zarith.
+rewrite Zpos_succ_morphism; unfold Zsucc.
+rewrite Zplus_comm; rewrite Zminus_plus.
+apply plength_pred_correct.
+Qed.
+
+
 
 Definition zn2z_word_comm : forall w n, zn2z (word w n) = word (zn2z w) n.
  fix zn2z_word_comm 2.
@@ -115,7 +211,7 @@ Section CompareRec.
 
  Fixpoint compare0_mn (n:nat) : word wm n -> comparison :=
   match n return word wm n -> comparison with 
-  | 0 => compare0_m 
+  | O => compare0_m 
   | S m => fun x =>
     match x with
     | W0 => Eq
@@ -129,7 +225,7 @@ Section CompareRec.
 
  Fixpoint compare_mn_1 (n:nat) : word wm n -> w -> comparison :=
   match n return word wm n -> w -> comparison with 
-  | 0 => compare_m 
+  | O => compare_m 
   | S m => fun x y => 
     match x with
     | W0 => compare w_0 y
diff --git a/theories/Ints/num/genN.ml b/theories/Ints/num/genN.ml
index bf6bf6535..775237f6a 100644
--- a/theories/Ints/num/genN.ml
+++ b/theories/Ints/num/genN.ml
@@ -770,8 +770,11 @@ let print_Make () =
   fprintf fmt "  end.\n";
   fprintf fmt "\n";
 
+  fprintf fmt "Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (plength p))).";
+  fprintf fmt "\n";
+
   fprintf fmt " Definition of_pos x :=\n";
-  fprintf fmt "  let h := nat_of_P (pheight x) in\n"; 
+  fprintf fmt "  let h := pheight x in\n"; 
   fprintf fmt "  match h with\n";
   let rec print_S s fmt i =
    if i = 0 then fprintf fmt "%s" s