Now NMake is proved

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

1 files changed, 62 insertions, 0 deletions

diff --git a/theories/Ints/num/GenLift.v b/theories/Ints/num/GenLift.v
index c1283aefb9..11455b8044 100644
--- a/theories/Ints/num/GenLift.v
+++ b/theories/Ints/num/GenLift.v
@@ -117,8 +117,10 @@ Section GenLift.
        | Gt => [[x]] > [[y]]
        end.
   Variable spec_ww_digits : ww_Digits = xO w_digits.
+  Variable spec_w_head00  : forall x, [|x|] = 0 -> [|w_head0 x|] = Zpos w_digits.
   Variable spec_w_head0  : forall x,  0 < [|x|] ->
 	 wB/ 2 <= 2 ^ ([|w_head0 x|]) * [|x|] < wB.
+  Variable spec_w_tail00  : forall x, [|x|] = 0 -> [|w_tail0 x|] = Zpos w_digits.
   Variable spec_w_tail0 : forall x, 0 < [|x|] -> 
          exists y, 0 <= y /\ [|x|] = (2* y + 1) * (2 ^ [|w_tail0 x|]).
   Variable spec_w_add_mul_div : forall x y p,
@@ -134,13 +136,42 @@ Section GenLift.
  Variable spec_zdigits : [| w_zdigits |] = Zpos w_digits.
  Variable spec_low: forall x, [| low x|] = [[x]] mod wB.
  
+ Variable spec_ww_zdigits : [[ww_zdigits]] = Zpos ww_Digits.
 
   Hint Resolve div_le_0 div_lt w_to_Z_wwB: lift.
   Ltac zarith := auto with zarith lift.
+
+  Lemma spec_ww_head00  : forall x, [[x]] = 0 -> [[ww_head0 x]] = Zpos ww_Digits.
+  Proof.
+  intros x; case x; unfold ww_head0.
+    intros HH; rewrite spec_ww_zdigits; auto.
+  intros xh xl; simpl; intros Hx.
+  case (spec_to_Z xh); intros Hx1 Hx2.
+  case (spec_to_Z xl); intros Hy1 Hy2.
+  assert (F1: [|xh|] = 0).
+    case (Zle_lt_or_eq _ _ Hy1); auto; intros Hy3.
+    absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith.
+    apply Zlt_le_trans with (1 := Hy3); auto with zarith.
+    pattern [|xl|] at 1; rewrite <- (Zplus_0_l [|xl|]).
+    apply Zplus_le_compat_r; auto with zarith.
+    case (Zle_lt_or_eq _ _ Hx1); auto; intros Hx3.
+    absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith.
+    rewrite <- Hy3; rewrite Zplus_0_r; auto with zarith.
+    apply Zmult_lt_0_compat; auto with zarith.
+  generalize (spec_compare w_0 xh); case w_compare.
+    intros H; simpl.
+    rewrite spec_w_add; rewrite spec_w_head00.
+    rewrite spec_zdigits; rewrite spec_ww_digits.
+    rewrite Zpos_xO; auto with zarith.
+  rewrite F1 in Hx; auto with zarith.
+  rewrite spec_w_0; auto with zarith.
+  rewrite spec_w_0; auto with zarith.
+  Qed.
    
   Lemma spec_ww_head0  : forall x,  0 < [[x]] ->
 	 wwB/ 2 <= 2 ^ [[ww_head0 x]] * [[x]] < wwB.
   Proof.
+   clear spec_ww_zdigits.
    rewrite wwB_div_2;rewrite Zmult_comm;rewrite wwB_wBwB.
    assert (U:= lt_0_wB w_digits); destruct x as [ |xh xl];simpl ww_to_Z;intros H.
    unfold Zlt in H;discriminate H.
@@ -182,9 +213,38 @@ Section GenLift.
    assert (H1 := spec_to_Z xh);zarith.
   Qed.
 
+  Lemma spec_ww_tail00  : forall x, [[x]] = 0 -> [[ww_tail0 x]] = Zpos ww_Digits.
+  Proof.
+  intros x; case x; unfold ww_tail0.
+    intros HH; rewrite spec_ww_zdigits; auto.
+  intros xh xl; simpl; intros Hx.
+  case (spec_to_Z xh); intros Hx1 Hx2.
+  case (spec_to_Z xl); intros Hy1 Hy2.
+  assert (F1: [|xh|] = 0).
+    case (Zle_lt_or_eq _ _ Hy1); auto; intros Hy3.
+    absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith.
+    apply Zlt_le_trans with (1 := Hy3); auto with zarith.
+    pattern [|xl|] at 1; rewrite <- (Zplus_0_l [|xl|]).
+    apply Zplus_le_compat_r; auto with zarith.
+    case (Zle_lt_or_eq _ _ Hx1); auto; intros Hx3.
+    absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith.
+    rewrite <- Hy3; rewrite Zplus_0_r; auto with zarith.
+    apply Zmult_lt_0_compat; auto with zarith.
+  assert (F2: [|xl|] = 0).
+    rewrite F1 in Hx; auto with zarith.
+  generalize (spec_compare w_0 xl); case w_compare.
+    intros H; simpl.
+    rewrite spec_w_add; rewrite spec_w_tail00; auto.
+    rewrite spec_zdigits; rewrite spec_ww_digits.
+    rewrite Zpos_xO; auto with zarith.
+  rewrite spec_w_0; auto with zarith.
+  rewrite spec_w_0; auto with zarith.
+  Qed.
+
   Lemma spec_ww_tail0  : forall x,  0 < [[x]] ->
 	 exists y, 0 <= y /\ [[x]] = (2 * y + 1) * 2 ^ [[ww_tail0 x]].
   Proof.
+   clear spec_ww_zdigits.
    destruct x as [ |xh xl];simpl ww_to_Z;intros H.
    unfold Zlt in H;discriminate H.
    assert (H0 := spec_compare w_0 xl);rewrite spec_w_0 in H0.
@@ -251,6 +311,7 @@ Section GenLift.
       ([[WW xh xl]] * (2^[[p]]) +
        [[WW yh yl]] / (2^(Zpos (xO w_digits) - [[p]]))) mod wwB.
   Proof.
+   clear spec_ww_zdigits.
    intros xh xl yh yl p zdigits;assert (HwwB := wwB_pos w_digits).
    case (spec_to_w_Z p); intros Hv1 Hv2.
    replace (Zpos (xO w_digits)) with (Zpos w_digits + Zpos w_digits).
@@ -374,6 +435,7 @@ Section GenLift.
          ([[x]] * (2^[[p]]) +
           [[y]] / (2^(Zpos (xO w_digits) - [[p]]))) mod wwB.
   Proof.
+   clear spec_ww_zdigits.
    intros x y p H.
    destruct x as [ |xh xl];
    [assert (H1 := @spec_ww_add_mul_div_aux w_0 w_0)