tail0

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

5 files changed, 95 insertions, 2 deletions

diff --git a/theories/Ints/BigN.v b/theories/Ints/BigN.v
index 1d2b177df..d7b406d3d 100644
--- a/theories/Ints/BigN.v
+++ b/theories/Ints/BigN.v
@@ -13,6 +13,7 @@ Definition int31_op : znz_op int31.
  exact (phi). (* conversion to Z *)
  exact (positive_to_int31). (* positive -> N*int31 :  p => N,i where p = N*2^31+phi i *)
  exact head031.  (* number of head 0 *)
+ exact tail031.  (* number of tail 0 *)
 
  (* Basic constructors *)
  exact 0. (* 0 *)
diff --git a/theories/Ints/Int31.v b/theories/Ints/Int31.v
index 8a19e878d..59e45c320 100644
--- a/theories/Ints/Int31.v
+++ b/theories/Ints/Int31.v
@@ -394,4 +394,12 @@ Definition head031 (i:int31) :=
                                           | D1 => n
                                           end)
        i On
+.
+
+Definition tail031 (i:int31) :=
+  recr _ (fun _ => T31) (fun b si rec n => match b with 
+                                          | D0 => rec (add31 n In)
+                                          | D1 => n
+                                          end)
+       i On
 .
\ No newline at end of file
diff --git a/theories/Ints/num/GenLift.v b/theories/Ints/num/GenLift.v
index 8b9271e32..c1283aefb 100644
--- a/theories/Ints/num/GenLift.v
+++ b/theories/Ints/num/GenLift.v
@@ -27,6 +27,7 @@ Section GenLift.
  Variable w_compare : w -> w -> comparison.
  Variable ww_compare : zn2z w -> zn2z w -> comparison.
  Variable w_head0 : w -> w.
+ Variable w_tail0 : w -> w.
  Variable w_add: w -> w -> zn2z w.
  Variable w_add_mul_div : w -> w -> w -> w.
  Variable ww_sub: zn2z w -> zn2z w -> zn2z w.
@@ -46,6 +47,18 @@ Section GenLift.
     end
   end.
 
+
+ Definition ww_tail0 x :=
+  match x with
+  | W0 => ww_zdigits
+  | WW xh xl =>
+    match w_compare w_0 xl with
+    | Eq => w_add w_zdigits (w_tail0 xh)
+    | _ => w_0W (w_tail0 xl)
+    end
+  end.
+
+
   (* 0 < p < ww_digits *)
  Definition ww_add_mul_div p x y := 
   let zdigits := w_0W w_zdigits in
@@ -106,6 +119,8 @@ Section GenLift.
   Variable spec_ww_digits : ww_Digits = xO w_digits.
   Variable spec_w_head0  : forall x,  0 < [|x|] ->
 	 wB/ 2 <= 2 ^ ([|w_head0 x|]) * [|x|] < wB.
+  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,
        [|p|] <= Zpos w_digits ->
        [| w_add_mul_div p x y |] =
@@ -167,6 +182,55 @@ Section GenLift.
    assert (H1 := spec_to_Z xh);zarith.
   Qed.
 
+  Lemma spec_ww_tail0  : forall x,  0 < [[x]] ->
+	 exists y, 0 <= y /\ [[x]] = (2 * y + 1) * 2 ^ [[ww_tail0 x]].
+  Proof.
+   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.
+   destruct (w_compare w_0 xl).
+   rewrite <- H0; rewrite Zplus_0_r.
+   case (spec_to_Z (w_tail0 xh)); intros HH1 HH2.
+   generalize H; rewrite <- H0; rewrite Zplus_0_r; clear H; intros H.
+   case (@spec_w_tail0 xh).
+     apply Zmult_lt_reg_r with wB; auto with zarith.
+     unfold base; auto with zarith.
+   intros z (Hz1, Hz2); exists z; split; auto.
+   rewrite spec_w_add; rewrite (fun x => Zplus_comm [|x|]).
+   rewrite spec_zdigits; rewrite Zpower_exp; auto with zarith.
+   rewrite Zmult_assoc; rewrite <- Hz2; auto.
+
+   case (spec_to_Z (w_tail0 xh)); intros HH1 HH2.
+   case (spec_w_tail0 H0); intros z (Hz1, Hz2).
+   assert (Hp: [|w_tail0 xl|] < Zpos w_digits).
+     case (Zle_or_lt (Zpos w_digits) [|w_tail0 xl|]); auto; intros H1.
+     absurd (2 ^  (Zpos w_digits) <= 2 ^ [|w_tail0 xl|]).
+       apply Zlt_not_le.
+       case (spec_to_Z xl); intros HH3 HH4.
+       apply Zle_lt_trans with (2 := HH4).
+       apply Zle_trans with (1 * 2 ^ [|w_tail0 xl|]); auto with zarith.
+       rewrite Hz2.
+       apply Zmult_le_compat_r; auto with zarith.
+     apply Zpower_le_monotone; auto with zarith.
+   exists ([|xh|] * (2 ^ ((Zpos w_digits - [|w_tail0 xl|]) - 1)) + z); split.
+     apply Zplus_le_0_compat; auto.
+     apply Zmult_le_0_compat; auto with zarith.
+     case (spec_to_Z xh); auto.
+   rewrite spec_w_0W.
+   rewrite (Zmult_plus_distr_r 2); rewrite <- Zplus_assoc.
+   rewrite Zmult_plus_distr_l; rewrite <- Hz2.
+   apply f_equal2 with (f := Zplus); auto.
+   rewrite (Zmult_comm 2).
+   repeat rewrite <- Zmult_assoc.
+   apply f_equal2 with (f := Zmult); auto.
+   case (spec_to_Z (w_tail0 xl)); intros HH3 HH4.
+   pattern 2 at 2; rewrite <- Zpower_exp_1.
+   lazy beta; repeat rewrite <- Zpower_exp; auto with zarith.
+   unfold base; apply f_equal with (f := Zpower 2); auto with zarith.
+
+   contradict H0; case (spec_to_Z xl); auto with zarith.
+  Qed.
+
   Hint Rewrite Zdiv_0 Zmult_0_l Zplus_0_l Zmult_0_r Zplus_0_r
     spec_w_W0 spec_w_0W spec_w_WW spec_w_0  
     (wB_div w_digits w_to_Z spec_to_Z) 
diff --git a/theories/Ints/num/Zn2Z.v b/theories/Ints/num/Zn2Z.v
index ac13d6922..78447c75d 100644
--- a/theories/Ints/num/Zn2Z.v
+++ b/theories/Ints/num/Zn2Z.v
@@ -37,6 +37,7 @@ Section Zn2Z.
  Let w_to_Z        := w_op.(znz_to_Z).
  Let w_of_pos      := w_op.(znz_of_pos).
  Let w_head0       := w_op.(znz_head0).
+ Let w_tail0       := w_op.(znz_tail0).
 
  Let w_0            := w_op.(znz_0).
  Let w_1            := w_op.(znz_1).
@@ -119,6 +120,10 @@ Section Zn2Z.
   Eval lazy beta delta [ww_head0] in 
   ww_head0 w_0 w_0W w_compare w_head0 w_add2 w_zdigits _ww_zdigits.
 
+ Let tail0 :=
+  Eval lazy beta delta [ww_tail0] in 
+  ww_tail0 w_0 w_0W w_compare w_tail0 w_add2 w_zdigits _ww_zdigits.
+
  Let ww_WW := Eval lazy beta delta [ww_WW] in (@ww_WW w).
  Let ww_0W := Eval lazy beta delta [ww_0W] in (@ww_0W w).
  Let ww_W0 := Eval lazy beta delta [ww_W0] in (@ww_W0 w).
@@ -284,7 +289,7 @@ Section Zn2Z.
    
  Definition mk_zn2z_op := 
   mk_znz_op _ww_digits _ww_zdigits
-    to_Z ww_of_pos head0
+    to_Z ww_of_pos head0 tail0
     W0 ww_1 ww_Bm1
     ww_WW ww_W0 ww_0W  
     compare eq0
@@ -305,7 +310,7 @@ Section Zn2Z.
 
  Definition mk_zn2z_op_karatsuba := 
    mk_znz_op _ww_digits _ww_zdigits
-    to_Z ww_of_pos head0
+    to_Z ww_of_pos head0 tail0
     W0 ww_1 ww_Bm1
     ww_WW ww_W0 ww_0W  
     compare eq0
@@ -364,6 +369,7 @@ Section Zn2Z.
     (spec_gcd_gt op_spec)
     (spec_gcd op_spec) 
     (spec_head0 op_spec) 
+    (spec_tail0 op_spec) 
     (spec_add_mul_div op_spec)
     (spec_pos_mod)
     (spec_is_even)
@@ -646,6 +652,16 @@ Section Zn2Z.
   exact (spec_zdigits op_spec).
  Qed.
 
+ Let spec_ww_tail0  : forall x,  0 < [|x|] ->
+  exists y, 0 <= y /\ [|x|] = (2 * y + 1) * 2 ^ [|tail0 x|].
+ Proof.
+  refine (spec_ww_tail0 (w_digits := w_digits) w_0 w_0W w_compare w_tail0 
+           w_add2 w_zdigits _ww_zdigits w_to_Z _ _ _ _ _ _ _);auto.
+  exact (spec_0W op_spec).
+  exact (spec_compare op_spec).
+  exact (spec_zdigits op_spec).
+ Qed.
+
  Lemma spec_ww_add_mul_div : forall x y p,
        [|p|] <= Zpos _ww_digits ->
        [| add_mul_div p x y |] =
diff --git a/theories/Ints/num/ZnZ.v b/theories/Ints/num/ZnZ.v
index 5096c81cf..ee4098989 100644
--- a/theories/Ints/num/ZnZ.v
+++ b/theories/Ints/num/ZnZ.v
@@ -27,6 +27,7 @@ Section ZnZ_Op.
     znz_to_Z   : znz -> Z;
     znz_of_pos : positive -> N * znz;
     znz_head0  : znz -> znz;
+    znz_tail0  : znz -> znz;
     (* Basic constructors *)
     znz_0   : znz;
     znz_1   : znz;
@@ -91,6 +92,7 @@ Section Spec.
  Let w_to_Z        := w_op.(znz_to_Z).
  Let w_of_pos      := w_op.(znz_of_pos).
  Let w_head0       := w_op.(znz_head0).
+ Let w_tail0       := w_op.(znz_tail0).
 
  Let w0            := w_op.(znz_0).
  Let w1            := w_op.(znz_1).
@@ -238,6 +240,8 @@ Section Spec.
     (* shift operations *)
     spec_head0  : forall x,  0 < [|x|] ->
 	 wB/ 2 <= 2 ^ ([|w_head0 x|]) * [|x|] < wB;  
+    spec_tail0  : forall x, 0 < [|x|] -> 
+         exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|w_tail0 x|]) ;  
     spec_add_mul_div : forall x y p,
        [|p|] <= Zpos w_digits ->
        [| w_add_mul_div p x y |] =