Processor integers + Print assumption (see coqdev mailing list for the

details).




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

1 files changed, 278 insertions, 0 deletions

diff --git a/theories/Ints/num/GenLift.v b/theories/Ints/num/GenLift.v
new file mode 100644
index 0000000000..14aa869796
--- /dev/null
+++ b/theories/Ints/num/GenLift.v
@@ -0,0 +1,278 @@
+
+(*************************************************************)
+(*      This file is distributed under the terms of the      *)
+(*      GNU Lesser General Public License Version 2.1        *)
+(*************************************************************)
+(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
+(*************************************************************)
+
+Set Implicit Arguments.
+
+Require Import ZArith.
+Require Import ZAux.
+Require Import ZPowerAux.
+Require Import ZDivModAux.
+Require Import Basic_type.
+Require Import GenBase.
+
+Open Local Scope Z_scope.
+
+Section GenLift.
+ Variable w : Set.
+ Variable w_0 : w.
+ Variable w_WW : w -> w -> zn2z w.
+ Variable w_W0 : w ->  zn2z w.
+ Variable w_0W : w ->  zn2z w.
+ Variable w_compare : w -> w -> comparison.
+ Variable w_head0 : w -> N.
+ Variable w_add_mul_div : positive -> w -> w -> w.
+ Variable w_digits : positive.
+ Variable ww_Digits : positive.
+
+ Definition ww_head0 x :=
+  match x with
+  | W0 => Npos ww_Digits
+  | WW xh xl =>
+    match w_compare w_0 xh with
+    | Eq => Nplus (Npos w_digits) (w_head0 xl)
+    | _ => w_head0 xh
+    end
+  end.
+
+  (* 0 < p < ww_digits *)
+ Definition ww_add_mul_div p x y := 
+  match x, y with
+  | W0, W0 => W0
+  | W0, WW yh yl =>
+    match Pcompare p w_digits Eq with
+    | Eq => w_0W yh 
+    | Lt => w_0W (w_add_mul_div p w_0 yh)
+    | Gt =>
+      let n := Pminus p w_digits in
+      w_WW (w_add_mul_div n w_0 yh) (w_add_mul_div n yh yl)
+    end
+  | WW xh xl, W0 =>
+    match Pcompare p w_digits Eq with
+    | Eq => w_W0 xl 
+    | Lt => w_WW (w_add_mul_div p xh xl) (w_add_mul_div p xl w_0)
+    | Gt =>
+      let n := Pminus p w_digits in
+      w_W0 (w_add_mul_div n xl w_0) 
+    end
+  | WW xh xl, WW yh yl =>
+    match Pcompare p w_digits Eq with
+    | Eq => w_WW xl yh 
+    | Lt => w_WW (w_add_mul_div p xh xl) (w_add_mul_div p xl yh)
+    | Gt =>
+      let n := Pminus p w_digits in
+      w_WW (w_add_mul_div n xl yh) (w_add_mul_div n yh yl)
+    end
+  end.
+
+ Section GenProof.
+  Variable w_to_Z : w -> Z.
+ 
+  Notation wB  := (base w_digits).
+  Notation wwB := (base (ww_digits w_digits)).
+  Notation "[| x |]" := (w_to_Z x)  (at level 0, x at level 99).
+  Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99).
+
+  Variable spec_w_0   : [|w_0|] = 0.
+  Variable spec_to_Z  : forall x, 0 <= [|x|] < wB.
+  Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|].
+  Variable spec_w_W0 : forall h, [[w_W0 h]] = [|h|] * wB.
+  Variable spec_w_0W : forall l, [[w_0W l]] = [|l|].
+  Variable spec_compare : forall x y,
+       match w_compare x y with
+       | Eq => [|x|] = [|y|]
+       | Lt => [|x|] < [|y|]
+       | Gt => [|x|] > [|y|]
+       end.
+  Variable spec_ww_digits : ww_Digits = xO w_digits.
+  Variable spec_w_head0  : forall x,  0 < [|x|] ->
+	 wB/ 2 <= 2 ^ (Z_of_N (w_head0 x)) * [|x|] < wB.
+  Variable spec_w_add_mul_div : forall x y p,
+       Zpos p < Zpos w_digits ->
+       [| w_add_mul_div p x y |] =
+         ([|x|] * (Zpower 2 (Zpos p)) +
+          [|y|] / (Zpower 2 ((Zpos w_digits) - (Zpos p)))) mod wB.
+ 
+
+  Hint Resolve div_le_0 div_lt w_to_Z_wwB: lift.
+  Ltac zarith := auto with zarith lift.
+   
+  Lemma spec_ww_head0  : forall x,  0 < [[x]] ->
+	 wwB/ 2 <= 2 ^ (Z_of_N (ww_head0 x)) * [[x]] < wwB.
+  Proof.
+   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.
+   assert (H0 := spec_compare w_0 xh);rewrite spec_w_0 in H0.
+   simpl Z_of_N; destruct (w_compare w_0 xh).
+   rewrite <- H0. simpl Zplus. rewrite <- H0 in H;simpl in H.
+   generalize (spec_w_head0 H);destruct (w_head0 xl) as [ |q].
+   intros H1;simpl Zpower in H1;rewrite Zmult_1_l in H1.
+   change (2 ^ Z_of_N (Npos w_digits)) with wB;split;zarith.
+   rewrite Zpower_2; apply Zmult_lt_compat_l;zarith.
+   unfold Z_of_N;intros.
+   change (Zpos(w_digits + q))with (Zpos w_digits + Zpos q);rewrite Zpower_exp.
+   fold wB;rewrite <- Zmult_assoc;split;zarith.
+   rewrite Zpower_2; apply Zmult_lt_compat_l;zarith.
+   intro H2;discriminate H2. intro H2;discriminate H2.
+   assert (H1 := spec_w_head0 H0).
+   split.
+   rewrite Zmult_plus_distr_r;rewrite Zmult_assoc.
+   apply Zle_trans with (2 ^ Z_of_N (w_head0 xh) * [|xh|] * wB).
+   rewrite Zmult_comm;zarith.
+   assert (0 <= 2 ^ Z_of_N (w_head0 xh) * [|xl|]);zarith.
+   assert (H2:=spec_to_Z xl);apply Zmult_le_0_compat;zarith.
+   assert (0<= Z_of_N (w_head0 xh)).
+    case (w_head0 xh);intros;simpl;intro H2;discriminate H2.
+   generalize (Z_of_N (w_head0 xh)) H1 H2;clear H1 H2;intros p H1 H2.
+   assert (Eq1 : 2^p < wB).
+     rewrite <- (Zmult_1_r (2^p));apply Zle_lt_trans with (2^p*[|xh|]);zarith.
+   assert (Eq2: p < Zpos w_digits).
+    destruct (Zle_or_lt (Zpos w_digits) p);trivial;contradict  Eq1.
+   apply Zle_not_lt;unfold base;apply Zpower_le_monotone;zarith.
+   assert (Zpos w_digits = p + (Zpos w_digits - p)). ring.
+   rewrite Zpower_2.
+   unfold base at 2;rewrite H3;rewrite Zpower_exp;zarith.
+   rewrite <- Zmult_assoc; apply Zmult_lt_compat_l; zarith.
+   rewrite <- (Zplus_0_r (2^(Zpos w_digits - p)*wB));apply beta_lex_inv;zarith.
+   apply Zmult_lt_reg_r with (2 ^ p); zarith.
+   rewrite <- Zpower_exp;zarith. 
+   rewrite Zmult_comm;ring_simplify (Zpos w_digits - p + p);fold wB;zarith.
+   assert (H1 := spec_to_Z xh);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) 
+    (wB_div_plus w_digits w_to_Z spec_to_Z) : w_rewrite.
+  Ltac w_rewrite := autorewrite with w_rewrite;trivial.
+ 
+  Lemma spec_ww_add_mul_div_aux : forall xh xl yh yl p,
+     Zpos p < Zpos (xO w_digits) ->
+      [[match (p ?= w_digits)%positive Eq with
+        | Eq => w_WW xl yh
+        | Lt => w_WW (w_add_mul_div p xh xl) (w_add_mul_div p xl yh)
+        | Gt =>
+            let n := (p - w_digits)%positive in
+            w_WW (w_add_mul_div n xl yh) (w_add_mul_div n yh yl)
+        end]] =  
+      ([[WW xh xl]] * (2^Zpos p) +
+       [[WW yh yl]] / (2^(Zpos (xO w_digits) - Zpos p))) mod wwB.
+  Proof.
+   intros xh xl yh yl p;assert (HwwB := wwB_pos w_digits).
+   assert (0 < Zpos p). unfold Zlt;reflexivity.
+   replace (Zpos (xO w_digits)) with (Zpos w_digits + Zpos w_digits).
+   2 : rewrite Zpos_xO;ring.
+   replace (Zpos w_digits + Zpos w_digits - Zpos p) with 
+     (Zpos w_digits + (Zpos w_digits - Zpos p)). 2:ring.
+   intros Hp; assert (Hxh := spec_to_Z xh);assert (Hxl:=spec_to_Z xl);
+   assert (Hx := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xh xl));
+   simpl in Hx;assert (Hyh := spec_to_Z yh);assert (Hyl:=spec_to_Z yl);
+   assert (Hy:=spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW yh yl));simpl in Hy.
+   case_eq  ((p ?= w_digits)%positive Eq);intros;w_rewrite;
+    match goal with 
+    | [H: (p ?= w_digits)%positive Eq = Eq |- _] =>
+      let H1:= fresh "H" in
+      (assert (H1 : Zpos p = Zpos w_digits);
+       [ rewrite Pcompare_Eq_eq with (1:= H);trivial
+       | rewrite H1;try rewrite Zminus_diag;try rewrite Zplus_0_r]);
+      fold wB
+    | [H: (p ?= w_digits)%positive Eq = Lt |- _] =>
+      change ((p ?= w_digits)%positive Eq = Lt) with 
+      (Zpos p < Zpos w_digits) in H;
+      repeat rewrite spec_w_add_mul_div;zarith
+    | [H: (p ?= w_digits)%positive Eq = Gt |- _] =>
+      change ((p ?= w_digits)%positive Eq=Gt)with(Zpos p > Zpos w_digits) in H;
+      let H1 := fresh "H" in
+      assert (H1 := Zpos_minus _ _ (Zgt_lt _ _ H));
+      replace (Zpos w_digits + (Zpos w_digits - Zpos p)) with
+       (Zpos w_digits - Zpos (p - w_digits));
+      [ repeat rewrite spec_w_add_mul_div;zarith
+      | zarith ] 
+    | _ => idtac
+    end;simpl ww_to_Z;w_rewrite;zarith.
+   rewrite Zmult_plus_distr_l;rewrite <- Zmult_assoc;rewrite <- Zplus_assoc.
+   rewrite <- Zpower_2.
+   rewrite <- wwB_wBwB;apply Zmod_unique with [|xh|]. apply lt_0_wwB. 
+   exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xl yh)). ring.
+   rewrite Zmult_plus_distr_l.
+   pattern ([|xl|] * 2 ^ Zpos p) at 2;
+   rewrite shift_unshift_mod with (n:= Zpos w_digits);fold wB;zarith.
+   replace ([|xh|] * wB * 2^Zpos p) with ([|xh|] * 2^Zpos p * wB). 2:ring. 
+   rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. rewrite <- Zplus_assoc.
+   unfold base at 5;rewrite <- Zmod_shift_r;zarith.
+   unfold base;rewrite Zmod_shift_r with (b:= Zpos (ww_digits w_digits));
+   fold wB;fold wwB;zarith.
+   rewrite wwB_wBwB;rewrite Zpower_2; rewrite  Zmult_mod_distr_r;zarith.
+   unfold ww_digits;rewrite Zpos_xO;zarith. apply Z_mod_lt;zarith.
+   split;zarith. apply Zdiv_lt_upper_bound;zarith.
+   rewrite <- Zpower_exp;zarith.
+   ring_simplify (Zpos p + (Zpos w_digits - Zpos p));fold wB;zarith.
+   pattern wB at 5;replace wB with 
+    (2^(Zpos (p - w_digits) + (Zpos w_digits - Zpos (p - w_digits)))).
+   rewrite Zpower_exp;zarith. rewrite Zmult_assoc.
+   rewrite Z_div_plus_l;zarith.
+   rewrite shift_unshift_mod with (a:= [|yh|]) (p:= Zpos (p - w_digits))
+    (n := Zpos w_digits);zarith. fold wB.
+   replace (Zpos p) with (Zpos (p - w_digits) + Zpos w_digits);zarith.
+   rewrite Zpower_exp;zarith. rewrite Zmult_assoc. fold wB.
+   repeat rewrite Zplus_assoc. rewrite <- Zmult_plus_distr_l.
+   repeat rewrite <- Zplus_assoc.
+   unfold base;rewrite Zmod_shift_r with (b:= Zpos (ww_digits w_digits));
+   fold wB;fold wwB;zarith.
+   unfold base;rewrite Zmod_shift_r with (a:= Zpos w_digits) 
+   (b:= Zpos w_digits);fold wB;fold wwB;zarith.
+   rewrite wwB_wBwB; rewrite Zpower_2; rewrite  Zmult_mod_distr_r;zarith.
+   rewrite Zmult_plus_distr_l.
+   replace ([|xh|] * wB * 2 ^ Zpos (p - w_digits)) with 
+     ([|xh|]*2^Zpos(p - w_digits)*wB). 2:ring.
+   repeat rewrite <- Zplus_assoc. 
+   rewrite (Zplus_comm ([|xh|] * 2 ^ Zpos (p - w_digits) * wB)).
+   rewrite Z_mod_plus;zarith. rewrite Zmod_mult_0;zarith.
+   unfold base;rewrite <- Zmod_shift_r;zarith. fold base;apply Z_mod_lt;zarith.
+   split;zarith. apply Zdiv_lt_upper_bound;zarith.
+   rewrite <- Zpower_exp;zarith. 
+   ring_simplify (Zpos (p - w_digits) + (Zpos w_digits - Zpos (p - w_digits))); fold 
+   wB;zarith. unfold ww_digits;rewrite Zpos_xO;zarith.
+   unfold base;rewrite <- Zmod_shift_r;zarith. fold base;apply Z_mod_lt;zarith.
+   split;zarith. apply Zdiv_lt_upper_bound;zarith.
+   rewrite <- Zpower_exp;zarith. 
+   ring_simplify (Zpos (p - w_digits) + (Zpos w_digits - Zpos (p - w_digits))); fold 
+   wB;zarith. 
+   ring_simplify (Zpos (p - w_digits) + (Zpos w_digits - Zpos (p - w_digits))); fold 
+   wB;trivial.
+  Qed.
+
+  Lemma spec_ww_add_mul_div : forall x y p,
+       Zpos p < Zpos (xO w_digits) ->
+       [[ ww_add_mul_div p x y ]] =
+         ([[x]] * (2^Zpos p) +
+          [[y]] / (2^(Zpos (xO w_digits) - Zpos p))) mod wwB.
+  Proof.
+   intros x y p H.
+   destruct x as [ |xh xl];
+   [assert (H1 := @spec_ww_add_mul_div_aux w_0 w_0)
+   |assert (H1 := @spec_ww_add_mul_div_aux xh xl)];
+   (destruct y as [ |yh yl];
+    [generalize (H1 w_0 w_0 p H) | generalize (H1 yh yl p H)];
+    clear H1;w_rewrite);simpl ww_add_mul_div.
+   replace [[WW w_0 w_0]] with 0;[w_rewrite|simpl;w_rewrite;trivial].
+   intros Heq;rewrite <- Heq;clear Heq.
+   case_eq ((p ?= w_digits)%positive Eq);w_rewrite;intros;trivial.
+   rewrite (spec_w_add_mul_div w_0 w_0);w_rewrite;zarith.
+   replace [[WW w_0 w_0]] with 0;[w_rewrite|simpl;w_rewrite;trivial].
+   intros Heq;rewrite <- Heq;clear Heq.
+   case_eq ((p ?= w_digits)%positive Eq);w_rewrite;intros;trivial.
+   rewrite (spec_w_add_mul_div w_0 w_0);w_rewrite;zarith.
+   change ((p ?= w_digits)%positive Eq = Gt)with(Zpos p > Zpos w_digits) in H0.
+   rewrite Zpos_minus;zarith. rewrite Zpos_xO in H;zarith.
+  Qed.
+
+ End GenProof.
+
+End GenLift.
+