Cyclic31: no more Admitted, but I've cheated: sqrt31 and sqrt312 are

 now dumb wrappers around Zsqrt_plain. Wanted (dead or alive): better
 implemntations _and_ their proofs.



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

4 files changed, 88 insertions, 13 deletions

diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v
index 11e0fe95f..10e208ead 100644
--- a/theories/Numbers/BigNumPrelude.v
+++ b/theories/Numbers/BigNumPrelude.v
@@ -359,3 +359,14 @@ right; auto with zarith.
 unfold Q' in *; intros n H1 H2. destruct (H n H1) as [[H3 H4] | H3].
 assumption. apply Zle_not_lt in H3. false_hyp H2 H3.
 Qed.
+
+Lemma Zsquare_le : forall x, x <= x*x.
+Proof.
+intros.
+destruct (Z_lt_le_dec 0 x).
+pattern x at 1; rewrite <- (Zmult_1_l x).
+apply Zmult_le_compat; auto with zarith.
+apply Zle_trans with 0; auto with zarith.
+rewrite <- Zmult_opp_opp.
+apply Zmult_le_0_compat; auto with zarith.
+Qed.
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index a0f3a253a..591968a86 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -1901,10 +1901,63 @@ Section Int31_Spec.
        let (s,r) := sqrt312 x y in
           [||WW x y||] = [|s|] ^ 2 + [+|r|] /\
           [+|r|] <= 2 * [|s|].
- Admitted. (* TODO !! *)
+ Proof.
+ intros; unfold sqrt312.
+ change base with wB.
+ simpl zn2z_to_Z; change (Zpower_pos 2 31) with wB.
+ remember ([|x|]*wB+[|y|]) as z.
+ destruct z.
+ auto with zarith.
+ destruct sqrtrempos; intros.
+ assert (s < wB).
+  destruct (Z_lt_le_dec s wB); auto.
+  assert (wB * wB <= Zpos p).
+   rewrite e.
+   apply Zle_trans with (s*s); try omega.
+   apply Zmult_le_compat; generalize wB_pos; auto with zarith.
+  assert (Zpos p < wB*wB).
+   rewrite Heqz.
+   replace (wB*wB) with ((wB-1)*wB+wB) by ring.
+   apply Zplus_le_lt_compat; auto with zarith.
+   apply Zmult_le_compat; auto with zarith.
+   generalize (phi_bounded x); auto with zarith.
+   generalize (phi_bounded y); auto with zarith.
+  omega.
+ destruct Z_lt_le_dec; unfold interp_carry.
+ rewrite 2 phi_phi_inv.
+ rewrite 2 Zmod_small by (auto with zarith).
+ rewrite Zpower_2; auto with zarith.
+
+ rewrite 2 phi_phi_inv.
+ rewrite 2 Zmod_small by (auto with zarith).
+ rewrite Zpower_2; auto with zarith.
+ 
+ assert (0<=Zneg p).
+  rewrite Heqz; generalize (phi_bounded x)(phi_bounded y);
+   auto with zarith.
+ compute in H0; elim H0; auto.
+ Qed.
+
  Lemma spec_sqrt : forall x,
        [|sqrt31 x|] ^ 2 <= [|x|] < ([|sqrt31 x|] + 1) ^ 2.
- Admitted. (* TODO !! *)
+ Proof.
+ intros.
+ unfold sqrt31.
+ assert (Hx := phi_bounded x). 
+ rewrite phi_phi_inv.
+ rewrite Zmod_small.
+ repeat rewrite Zpower_2.
+ apply Zsqrt_interval; auto with zarith.
+ split.
+ apply Zsqrt_plain_is_pos; auto with zarith.
+
+ cut (Zsqrt_plain [|x|] <= (wB-1)); try omega.
+ rewrite <- (Zsqrt_square_id (wB-1)) by (auto with zarith).
+ apply Zsqrt_le.
+ split; auto with zarith.
+ apply Zle_trans with (wB-1); auto with zarith.
+ apply Zsquare_le.
+ Qed.
 
  (** [iszero] *)
 
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index b3a985b63..56b010e74 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -354,6 +354,26 @@ Definition gcd31 (i j:int31) :=
    end)
   (2*size)%nat i j.
 
+(** Very naive square root functions, for easy correctness proofs.
+   TODO: replace them someday by efficient code in the spirit of
+   the code commented afterwards. *)
+
+Definition sqrt31 (i:int31) : int31 := phi_inv (Zsqrt_plain (phi i)).
+
+Definition sqrt312 (i j:int31) : int31*(carry int31) := 
+  let z := ((phi i)*base+(phi j))%Z in 
+  match z with 
+   | Z0 => (On, C0 On)
+   | Zpos p => 
+      let (s,r,_,_) := sqrtrempos p in 
+      (phi_inv s, 
+        if Z_lt_le_dec r base 
+        then C0 (phi_inv r) 
+        else C1 (phi_inv (r-base)))
+   | Zneg _ => (On, C0 On)
+  end.
+
+(*
 Definition sqrt31 (i:int31) : int31 :=
   match i ?= On with
   | Eq =>  On
@@ -441,6 +461,8 @@ Definition sqrt312 (ih il:int31) :=
      in
      (root, rem)
   end.
+*)
+
 
 Fixpoint p2i n p : (N*int31)%type := 
   match n with
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index 77f1a57b4..de7e4c6e8 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -587,17 +587,6 @@ Section ZModulo.
  generalize (Z_mod_lt [|x|] 2); omega.
  Qed.
 
- Lemma Zsquare_le : forall x, x <= x*x.
- Proof.
- intros.
- destruct (Z_lt_le_dec 0 x).
- pattern x at 1; rewrite <- (Zmult_1_l x).
- apply Zmult_le_compat; auto with zarith.
- apply Zle_trans with 0; auto with zarith.
- rewrite <- Zmult_opp_opp.
- apply Zmult_le_0_compat; auto with zarith.
- Qed.
-
  Definition znz_sqrt x := Zsqrt_plain [|x|]. 
  Lemma spec_sqrt : forall x,
        [|znz_sqrt x|] ^ 2 <= [|x|] < ([|znz_sqrt x|] + 1) ^ 2.