Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

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

1 files changed, 130 insertions, 103 deletions

diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index b8040335e8..f560050804 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -8,10 +8,9 @@
 
 (* $Id$ *)
 
-Require Omega.
+Require Import Omega.
 Require Export ZArith_base.
 Require Export ZArithRing.
-V7only [Import Z_scope.].
 Open Local Scope Z_scope.
 
 (**********************************************************************)
@@ -19,118 +18,146 @@ Open Local Scope Z_scope.
 
 (** The following tactic replaces all instances of (POS (xI ...)) by
     `2*(POS ...)+1` , but only when ... is not made only with xO, XI, or xH. *)
-Tactic Definition compute_POS :=
-  Match Context With
-  | [|- [(POS (xI ?1))]] ->
-    (Match ?1 With
-     | [[xH]] -> Fail
-     | _ -> Rewrite (POS_xI ?1))
-  | [|- [(POS (xO ?1))]] ->
-    (Match ?1 With
-     | [[xH]] -> Fail
-     | _ -> Rewrite (POS_xO ?1)).
+Ltac compute_POS :=
+  match goal with
+  |  |- context [(Zpos (xI ?X1))] =>
+      match constr:X1 with
+      | context [1%positive] => fail
+      | _ => rewrite (BinInt.Zpos_xI X1)
+      end
+  |  |- context [(Zpos (xO ?X1))] =>
+      match constr:X1 with
+      | context [1%positive] => fail
+      | _ => rewrite (BinInt.Zpos_xO X1)
+      end
+  end.
 
-Inductive sqrt_data [n : Z] : Set :=
-  c_sqrt: (s, r :Z)`n=s*s+r`->`0<=r<=2*s`->(sqrt_data n) .
+Inductive sqrt_data (n:Z) : Set :=
+    c_sqrt : forall s r:Z, n = s * s + r -> 0 <= r <= 2 * s -> sqrt_data n.
 
-Definition sqrtrempos: (p : positive)  (sqrt_data (POS p)).
-Refine (Fix sqrtrempos {
-         sqrtrempos [p : positive] : (sqrt_data (POS p)) :=
-            <[p : ?]  (sqrt_data (POS p))> Cases p of
-                xH => (c_sqrt `1` `1` `0` ? ?)
-               | (xO xH) => (c_sqrt `2` `1` `1` ? ?)
-               | (xI xH) => (c_sqrt `3` `1` `2` ? ?)
-               | (xO (xO p')) =>
-                   Cases (sqrtrempos p') of
-                     (c_sqrt s' r' Heq Hint) =>
-                       Cases (Z_le_gt_dec `4*s'+1` `4*r'`) of
-                         (left Hle) =>
-                           (c_sqrt (POS (xO (xO p'))) `2*s'+1` `4*r'-(4*s'+1)` ? ?)
-                        | (right Hgt) =>
-                            (c_sqrt (POS (xO (xO p'))) `2*s'` `4*r'` ? ?)
-                       end
-                   end
-               | (xO (xI p')) =>
-                   Cases (sqrtrempos p') of
-                     (c_sqrt s' r' Heq Hint) =>
-                       Cases
-                        (Z_le_gt_dec `4*s'+1` `4*r'+2`) of
-                         (left Hle) =>
-                           (c_sqrt 
-			     (POS (xO (xI p'))) `2*s'+1` `4*r'+2-(4*s'+1)` ? ?)
-                        | (right Hgt) =>
-                            (c_sqrt (POS (xO (xI p'))) `2*s'` `4*r'+2` ? ?)
-                       end
-                   end
-               | (xI (xO p')) =>
-                   Cases (sqrtrempos p') of
-                     (c_sqrt s' r' Heq Hint) =>
-                       Cases
-                        (Z_le_gt_dec `4*s'+1` `4*r'+1`) of
-                         (left Hle) =>
-                           (c_sqrt
-                            (POS (xI (xO p'))) `2*s'+1` `4*r'+1-(4*s'+1)` ? ?)
-                        | (right Hgt) =>
-                            (c_sqrt (POS (xI (xO p'))) `2*s'` `4*r'+1` ? ?)
-                       end
-                   end
-               | (xI (xI p')) =>
-                   Cases (sqrtrempos p') of
-                     (c_sqrt s' r' Heq Hint) =>
-                       Cases
-                        (Z_le_gt_dec `4*s'+1` `4*r'+3`) of
-                         (left Hle) =>
-                           (c_sqrt
-                            (POS (xI (xI p'))) `2*s'+1` `4*r'+3-(4*s'+1)` ? ?)
-                        | (right Hgt) =>
-                            (c_sqrt (POS (xI (xI p'))) `2*s'` `4*r'+3` ? ?)
-                       end
-                   end
+Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p).
+refine
+ (fix sqrtrempos (p:positive) : sqrt_data (Zpos p) :=
+    match p return sqrt_data (Zpos p) with
+    | xH => c_sqrt 1 1 0 _ _
+    | xO xH => c_sqrt 2 1 1 _ _
+    | xI xH => c_sqrt 3 1 2 _ _
+    | xO (xO p') =>
+        match sqrtrempos p' with
+        | c_sqrt s' r' Heq Hint =>
+            match Z_le_gt_dec (4 * s' + 1) (4 * r') with
+            | left Hle =>
+                c_sqrt (Zpos (xO (xO p'))) (2 * s' + 1)
+                  (4 * r' - (4 * s' + 1)) _ _
+            | right Hgt => c_sqrt (Zpos (xO (xO p'))) (2 * s') (4 * r') _ _
             end
-        }); Clear sqrtrempos; Repeat compute_POS;
- Try (Try Rewrite Heq; Ring; Fail); Try Omega.
+        end
+    | xO (xI p') =>
+        match sqrtrempos p' with
+        | c_sqrt s' r' Heq Hint =>
+            match Z_le_gt_dec (4 * s' + 1) (4 * r' + 2) with
+            | left Hle =>
+                c_sqrt (Zpos (xO (xI p'))) (2 * s' + 1)
+                  (4 * r' + 2 - (4 * s' + 1)) _ _
+            | right Hgt =>
+                c_sqrt (Zpos (xO (xI p'))) (2 * s') (4 * r' + 2) _ _
+            end
+        end
+    | xI (xO p') =>
+        match sqrtrempos p' with
+        | c_sqrt s' r' Heq Hint =>
+            match Z_le_gt_dec (4 * s' + 1) (4 * r' + 1) with
+            | left Hle =>
+                c_sqrt (Zpos (xI (xO p'))) (2 * s' + 1)
+                  (4 * r' + 1 - (4 * s' + 1)) _ _
+            | right Hgt =>
+                c_sqrt (Zpos (xI (xO p'))) (2 * s') (4 * r' + 1) _ _
+            end
+        end
+    | xI (xI p') =>
+        match sqrtrempos p' with
+        | c_sqrt s' r' Heq Hint =>
+            match Z_le_gt_dec (4 * s' + 1) (4 * r' + 3) with
+            | left Hle =>
+                c_sqrt (Zpos (xI (xI p'))) (2 * s' + 1)
+                  (4 * r' + 3 - (4 * s' + 1)) _ _
+            | right Hgt =>
+                c_sqrt (Zpos (xI (xI p'))) (2 * s') (4 * r' + 3) _ _
+            end
+        end
+    end); clear sqrtrempos; repeat compute_POS;
+ try (try rewrite Heq; ring; fail); try omega.
 Defined.
 
 (** Define with integer input, but with a strong (readable) specification. *)
-Definition Zsqrt : (x:Z)`0<=x`->{s:Z & {r:Z | x=`s*s+r` /\ `s*s<=x<(s+1)*(s+1)`}}.
-Refine [x]
-   <[x:Z]`0<=x`->{s:Z & {r:Z | x=`s*s+r` /\ `s*s<=x<(s+1)*(s+1)`}}>Cases x of
-       (POS p) => [h]Cases (sqrtrempos p) of
-                    (c_sqrt s r Heq Hint) =>
-                  (existS ? [s:Z]{r:Z | `(POS p)=s*s+r` /\ 
-		                         `s*s<=(POS p)<(s+1)*(s+1)`}
-		   s
-                    (exist Z [r:Z]((POS p)=`s*s+r` /\ `s*s<=(POS p)<(s+1)*(s+1)`)
-                       r ?))
-                  end
-     | (NEG p) => [h](False_rec 
-		         {s:Z & {r:Z |
-			     (NEG p)=`s*s+r` /\ `s*s<=(NEG p)<(s+1)*(s+1)`}}
-                         (h (refl_equal ? SUPERIEUR)))
-     | ZERO => [h](existS ? [s:Z]{r:Z | `0=s*s+r` /\ `s*s<=0<(s+1)*(s+1)`}
-		     `0` (exist Z [r:Z](`0=0*0+r`/\`0*0<=0<(0+1)*(0+1)`)
-		     `0` ?))
-     end;Try Omega.
-Split;[Omega|Rewrite Heq;Ring `(s+1)*(s+1)`;Omega].
+Definition Zsqrt :
+  forall x:Z,
+    0 <= x ->
+    {s : Z &  {r : Z | x = s * s + r /\ s * s <= x < (s + 1) * (s + 1)}}.
+refine
+ (fun x =>
+    match
+      x
+      return
+        0 <= x ->
+        {s : Z &  {r : Z | x = s * s + r /\ s * s <= x < (s + 1) * (s + 1)}}
+    with
+    | Zpos p =>
+        fun h =>
+          match sqrtrempos p with
+          | c_sqrt s r Heq Hint =>
+              existS
+                (fun s:Z =>
+                   {r : Z |
+                   Zpos p = s * s + r /\ s * s <= Zpos p < (s + 1) * (s + 1)})
+                s
+                (exist
+                   (fun r:Z =>
+                      Zpos p = s * s + r /\
+                      s * s <= Zpos p < (s + 1) * (s + 1)) r _)
+          end
+    | Zneg p =>
+        fun h =>
+          False_rec
+            {s : Z & 
+            {r : Z |
+            Zneg p = s * s + r /\ s * s <= Zneg p < (s + 1) * (s + 1)}}
+            (h (refl_equal Datatypes.Gt))
+    | Z0 =>
+        fun h =>
+          existS
+            (fun s:Z =>
+               {r : Z | 0 = s * s + r /\ s * s <= 0 < (s + 1) * (s + 1)}) 0
+            (exist
+               (fun r:Z => 0 = 0 * 0 + r /\ 0 * 0 <= 0 < (0 + 1) * (0 + 1)) 0
+               _)
+    end); try omega.
+split; [ omega | rewrite Heq; ring ((s + 1) * (s + 1)); omega ].
 Defined.
 
 (** Define a function of type Z->Z that computes the integer square root,
     but only for positive numbers, and 0 for others. *)
-Definition Zsqrt_plain : Z->Z :=
-  [x]Cases x of
-    (POS p)=>Cases (Zsqrt (POS p) (ZERO_le_POS p)) of (existS s _) => s end
-   |(NEG p)=>`0`
-   |ZERO=>`0`
-   end.
+Definition Zsqrt_plain (x:Z) : Z :=
+  match x with
+  | Zpos p =>
+      match Zsqrt (Zpos p) (Zorder.Zle_0_pos p) with
+      | existS s _ => s
+      end
+  | Zneg p => 0
+  | Z0 => 0
+  end.
 
 (** A basic theorem about Zsqrt_plain *)
-Theorem Zsqrt_interval :(x:Z)`0<=x`->
-  `(Zsqrt_plain x)*(Zsqrt_plain x)<= x < ((Zsqrt_plain x)+1)*((Zsqrt_plain x)+1)`.
-Intros x;Case x.
-Unfold Zsqrt_plain;Omega.
-Intros p;Unfold Zsqrt_plain;Case (Zsqrt (POS p) (ZERO_le_POS p)).
-Intros s (r,(Heq,Hint)) Hle;Assumption.
-Intros p Hle;Elim Hle;Auto.
+Theorem Zsqrt_interval :
+ forall n:Z,
+   0 <= n ->
+   Zsqrt_plain n * Zsqrt_plain n <= n <
+   (Zsqrt_plain n + 1) * (Zsqrt_plain n + 1).
+intros x; case x.
+unfold Zsqrt_plain in |- *; omega.
+intros p; unfold Zsqrt_plain in |- *;
+ case (Zsqrt (Zpos p) (Zorder.Zle_0_pos p)).
+intros s [r [Heq Hint]] Hle; assumption.
+intros p Hle; elim Hle; auto.
 Qed.
 
-