proof of compare added

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

1 files changed, 169 insertions, 0 deletions

diff --git a/theories/Ints/num/Nbasic.v b/theories/Ints/num/Nbasic.v
index 846aabe8ca..c96425cb5d 100644
--- a/theories/Ints/num/Nbasic.v
+++ b/theories/Ints/num/Nbasic.v
@@ -3,6 +3,7 @@ Require Import ZAux.
 Require Import ZDivModAux.
 Require Import Basic_type.
 Require Import Max.
+Require Import GenBase.
 
 (* To compute the necessary height *)
 
@@ -275,6 +276,57 @@ Section CompareRec.
     end
   end.
 
+ Variable wm_base: positive.
+ Variable wm_to_Z: wm -> Z.
+ Variable w_to_Z: w -> Z.
+ Variable w_to_Z_0: w_to_Z w_0 = 0.
+ Variable spec_compare0_m: forall x,
+    match compare0_m x with
+      Eq => w_to_Z w_0 = wm_to_Z x
+    | Lt => w_to_Z w_0 < wm_to_Z x 
+    | Gt => w_to_Z w_0 > wm_to_Z x
+    end.
+ Variable wm_to_Z_pos: forall x, 0 <= wm_to_Z x < base wm_base.
+
+ Let gen_to_Z := gen_to_Z wm_base wm_to_Z.
+ Let gen_wB := gen_wB wm_base.
+
+ Lemma base_xO: forall n, base (xO n) = (base n)^2.
+ Proof.
+ intros n1; unfold base.
+ rewrite (Zpos_xO n1); rewrite Zmult_comm; rewrite ZAux.Zpower_mult; auto with zarith.
+ Qed.
+
+ Let gen_to_Z_pos: forall n x, 0 <= gen_to_Z n x < gen_wB n :=
+   (spec_gen_to_Z wm_base wm_to_Z wm_to_Z_pos).
+
+
+ Lemma spec_compare0_mn: forall n x,
+    match compare0_mn n x with
+      Eq => 0 = gen_to_Z n x
+    | Lt => 0 < gen_to_Z n x
+    | Gt => 0 > gen_to_Z n x
+    end.
+  Proof.
+  intros n; elim n; clear n; auto.
+  intros x; generalize (spec_compare0_m x); rewrite w_to_Z_0; auto.
+  intros n Hrec x; case x; unfold compare0_mn; fold compare0_mn; auto.
+  intros xh xl.
+  generalize (Hrec xh); case compare0_mn; auto.
+  generalize (Hrec xl); case compare0_mn; auto.
+  simpl gen_to_Z; intros H1 H2; rewrite H1; rewrite <- H2; auto.
+  simpl gen_to_Z; intros H1 H2; rewrite <- H2; auto.
+  case (gen_to_Z_pos n xl); auto with zarith.
+  intros H1; simpl gen_to_Z.
+  set (u := GenBase.gen_wB wm_base n).
+  case (gen_to_Z_pos n xl); intros H2 H3.
+  assert (0 < u); auto with zarith.
+  unfold u, GenBase.gen_wB, base; auto with zarith.
+  change 0 with (0 + 0); apply Zplus_lt_le_compat; auto with zarith.
+  apply Zmult_lt_0_compat; auto with zarith.
+  case (gen_to_Z_pos n xh); auto with zarith.
+  Qed.
+
  Fixpoint compare_mn_1 (n:nat) : word wm n -> w -> comparison :=
   match n return word wm n -> w -> comparison with 
   | O => compare_m 
@@ -289,7 +341,124 @@ Section CompareRec.
     end
   end.
 
+ Variable spec_compare: forall x y,
+   match compare x y with
+     Eq => w_to_Z x = w_to_Z y
+   | Lt => w_to_Z x < w_to_Z y
+   | Gt => w_to_Z x > w_to_Z y
+   end.
+ Variable spec_compare_m: forall x y,
+   match compare_m x y with
+     Eq => wm_to_Z x = w_to_Z y
+   | Lt => wm_to_Z x < w_to_Z y
+   | Gt => wm_to_Z x > w_to_Z y
+   end.
+ Variable wm_base_lt: forall x, 
+   0 <= w_to_Z x < base (wm_base).
+
+ Let gen_wB_lt: forall n x,
+   0 <= w_to_Z x < (gen_wB n).
+ Proof.
+ intros n x; elim n; simpl; auto; clear n.
+ intros n (H0, H); split; auto.
+ apply Zlt_le_trans with (1:= H).
+ unfold gen_wB, GenBase.gen_wB; simpl.
+ rewrite base_xO.
+ set (u := base (gen_digits wm_base n)).
+ assert (0 < u).
+  unfold u, base; auto with zarith.
+ replace (u^2) with (u * u); simpl; auto with zarith.
+ apply Zle_trans with (1 * u); auto with zarith.
+ unfold Zpower_pos; simpl; ring.
+ Qed.
+
+ 
+ Lemma spec_compare_mn_1: forall n x y,
+   match compare_mn_1 n x y with
+     Eq => gen_to_Z n x = w_to_Z y
+   | Lt => gen_to_Z n x < w_to_Z y
+   | Gt => gen_to_Z n x > w_to_Z y
+   end.
+ Proof.
+ intros n; elim n; simpl; auto; clear n.
+ intros n Hrec x; case x; clear x; auto.
+ intros y; generalize (spec_compare w_0 y); rewrite w_to_Z_0; case compare; auto.
+ intros xh xl y; simpl; generalize (spec_compare0_mn n xh); case compare0_mn; intros H1b.
+ rewrite <- H1b; rewrite Zmult_0_l; rewrite Zplus_0_l; auto.
+ apply Hrec.
+ apply Zlt_gt.
+ case (gen_wB_lt n y); intros _ H0.
+ apply Zlt_le_trans with (1:= H0).
+ fold gen_wB.
+ case (gen_to_Z_pos n xl); intros H1 H2.
+ apply Zle_trans with (gen_to_Z n xh * gen_wB n); auto with zarith.
+ apply Zle_trans with (1 * gen_wB n); auto with zarith.
+ case (gen_to_Z_pos n xh); auto with zarith.
+ Qed.
+
 End CompareRec.
 
 
+Section AddS.
+
+ Variable  w wm: Set.
+ Variable incr : wm -> carry wm.
+ Variable addr : w -> wm -> carry wm.
+ Variable injr : w -> zn2z wm.
 
+ Variable w_0 u: w.
+ Fixpoint injs  (n:nat): word w (S n) :=
+  match n return (word w (S n)) with
+    O => WW w_0 u
+  | S n1 => (WW W0 (injs n1))
+  end.
+
+ Definition adds x y :=
+   match y with
+    W0 => C0 (injr x)
+  | WW hy ly => match addr x ly with
+                  C0 z => C0 (WW hy z)
+                | C1 z => match incr hy with
+                            C0 z1 => C0 (WW z1 z)
+                          | C1 z1 => C1 (WW z1 z)
+                          end  
+                 end
+   end.
+
+End AddS.
+
+
+ Lemma spec_opp: forall u x y,
+  match u with
+  | Eq => y = x
+  | Lt => y < x
+  | Gt => y > x
+  end ->
+  match opp_compare u with
+  | Eq => x = y
+  | Lt => x < y
+  | Gt => x > y
+  end.
+ Proof.
+ intros u x y; case u; simpl; auto with zarith.
+ Qed.
+
+ Fixpoint length_pos x :=
+  match x with xH => O | xO x1 => S (length_pos x1) | xI x1 => S (length_pos x1) end.
+ 
+ Theorem length_pos_lt: forall x y,
+   (length_pos x < length_pos y)%nat -> Zpos x < Zpos y.
+ Proof.
+ intros x; elim x; clear x; [intros x1 Hrec | intros x1 Hrec | idtac];
+   intros y; case y; clear y; intros y1 H || intros H; simpl length_pos; 
+   try (rewrite (Zpos_xI x1) || rewrite (Zpos_xO x1));
+   try (rewrite (Zpos_xI y1) || rewrite (Zpos_xO y1));
+   try (inversion H; fail);
+   try (assert (Zpos x1 < Zpos y1); [apply Hrec; apply lt_S_n | idtac]; auto with zarith);
+   assert (0 < Zpos y1); auto with zarith; red; auto.
+ Qed.
+
+ Theorem cancel_app: forall A B (f g: A -> B) x, f = g -> f x = g x.
+ Proof.
+ intros A B f g x H; rewrite H; auto.
+ Qed.