1 files changed, 136 insertions, 132 deletions

diff --git a/contrib/correctness/Sorted.v b/contrib/correctness/Sorted.v
index 7e656ae1b3..0dafe10109 100644
--- a/contrib/correctness/Sorted.v
+++ b/contrib/correctness/Sorted.v
@@ -11,188 +11,192 @@
 (* $Id$ *)
 
 Require Export Arrays.
-Require ArrayPermut.
+Require Import ArrayPermut.
 
-Require ZArithRing.
-Require Omega.
-V7only [Import Z_scope.].
+Require Import ZArithRing.
+Require Import Omega.
 Open Local Scope Z_scope.
 
 Set Implicit Arguments.
 
 (* Definition *)
 
-Definition sorted_array :=
-  [N:Z][A:(array N Z)][deb:Z][fin:Z]
-     `deb<=fin` -> (x:Z) `x>=deb` -> `x<fin` -> (Zle #A[x] #A[`x+1`]).
+Definition sorted_array (N:Z) (A:array N Z) (deb fin:Z) :=
+  deb <= fin -> forall x:Z, x >= deb -> x < fin -> #A [x] <= #A [x + 1].
 
 (* Elements of a sorted sub-array are in increasing order *)
 
 (* one element and the next one *)
 
 Lemma sorted_elements_1 :
-  (N:Z)(A:(array N Z))(n:Z)(m:Z)
-  (sorted_array A n m)
-  -> (k:Z)`k>=n`
-  -> (i:Z) `0<=i` -> `k+i<=m`
-  -> (Zle (access A k) (access A `k+i`)).
+ forall (N:Z) (A:array N Z) (n m:Z),
+   sorted_array A n m ->
+   forall k:Z,
+     k >= n -> forall i:Z, 0 <= i -> k + i <= m -> #A [k] <= #A [k + i].
 Proof.
-Intros N A n m H_sorted k H_k i H_i.
-Pattern i. Apply natlike_ind.
-Intro.
-Replace `k+0` with k; Omega. (*** Ring `k+0` => BUG ***)
+intros N A n m H_sorted k H_k i H_i.
+pattern i in |- *. apply natlike_ind.
+intro.
+replace (k + 0) with k; omega. (*** Ring `k+0` => BUG ***)
 
-Intros.
-Apply Zle_trans with m:=(access A `k+x`).
-Apply H0 ; Omega.
+intros.
+apply Zle_trans with (m := #A [k + x]).
+apply H0; omega.
 
-Unfold Zs.
-Replace `k+(x+1)` with `(k+x)+1`.
-Unfold sorted_array in H_sorted.
-Apply H_sorted ; Omega.
+unfold Zsucc in |- *.
+replace (k + (x + 1)) with (k + x + 1).
+unfold sorted_array in H_sorted.
+apply H_sorted; omega.
 
-Omega.
+omega.
 
-Assumption.
-Save.
+assumption.
+Qed.
 
 (* one element and any of the following *)
 
 Lemma sorted_elements :
-  (N:Z)(A:(array N Z))(n:Z)(m:Z)(k:Z)(l:Z)
-  (sorted_array A n m)
-  -> `k>=n` -> `l<N` -> `k<=l` -> `l<=m`
-  -> (Zle (access A k) (access A l)).
+ forall (N:Z) (A:array N Z) (n m k l:Z),
+   sorted_array A n m ->
+   k >= n -> l < N -> k <= l -> l <= m -> #A [k] <= #A [l].
 Proof.
-Intros.
-Replace l with `k+(l-k)`.
-Apply sorted_elements_1 with n:=n m:=m; [Assumption | Omega | Omega | Omega].
-Omega.
-Save.
+intros.
+replace l with (k + (l - k)).
+apply sorted_elements_1 with (n := n) (m := m);
+ [ assumption | omega | omega | omega ].
+omega.
+Qed.
 
-Hints Resolve sorted_elements : datatypes v62.
+Hint Resolve sorted_elements: datatypes v62.
 
 (* A sub-array of a sorted array is sorted *)
 
-Lemma sub_sorted_array : (N:Z)(A:(array N Z))(deb:Z)(fin:Z)(i:Z)(j:Z)
-      (sorted_array A deb fin) -> 
-        (`i>=deb` -> `j<=fin` -> `i<=j` -> (sorted_array A i j)).
+Lemma sub_sorted_array :
+ forall (N:Z) (A:array N Z) (deb fin i j:Z),
+   sorted_array A deb fin ->
+   i >= deb -> j <= fin -> i <= j -> sorted_array A i j.
 Proof.
-Unfold sorted_array.
-Intros.
-Apply H ; Omega.
-Save.
+unfold sorted_array in |- *.
+intros.
+apply H; omega.
+Qed.
 
-Hints Resolve sub_sorted_array : datatypes v62.
+Hint Resolve sub_sorted_array: datatypes v62.
 
 (* Extension on the left of the property of being sorted *)
 
-Lemma left_extension : (N:Z)(A:(array N Z))(i:Z)(j:Z)
-   `i>0` -> `j<N` -> (sorted_array A i j) 
-   -> (Zle #A[`i-1`]  #A[i]) -> (sorted_array A `i-1` j).
+Lemma left_extension :
+ forall (N:Z) (A:array N Z) (i j:Z),
+   i > 0 ->
+   j < N ->
+   sorted_array A i j -> #A [i - 1] <= #A [i] -> sorted_array A (i - 1) j.
 Proof.
-(Intros; Unfold sorted_array ; Intros).
-Elim (Z_ge_lt_dec x i).   (* (`x >= i`) + (`x < i`) *)
-Intro Hcut.
-Apply H1 ; Omega.
+intros; unfold sorted_array in |- *; intros.
+elim (Z_ge_lt_dec x i).   (* (`x >= i`) + (`x < i`) *)
+intro Hcut.
+apply H1; omega.
 
-Intro Hcut.
-Replace x with `i-1`.
-Replace `i-1+1` with i ; [Assumption | Omega].
+intro Hcut.
+replace x with (i - 1).
+replace (i - 1 + 1) with i; [ assumption | omega ].
 
-Omega.
-Save.
+omega.
+Qed.
 
 (* Extension on the right *)
 
-Lemma right_extension : (N:Z)(A:(array N Z))(i:Z)(j:Z)
-   `i>=0` -> `j<N-1` -> (sorted_array A i j) 
-   -> (Zle #A[j]  #A[`j+1`]) -> (sorted_array A i `j+1`).
+Lemma right_extension :
+ forall (N:Z) (A:array N Z) (i j:Z),
+   i >= 0 ->
+   j < N - 1 ->
+   sorted_array A i j -> #A [j] <= #A [j + 1] -> sorted_array A i (j + 1).
 Proof.
-(Intros; Unfold sorted_array ; Intros).
-Elim (Z_lt_ge_dec x j).
-Intro Hcut. 
-Apply H1 ; Omega.
+intros; unfold sorted_array in |- *; intros.
+elim (Z_lt_ge_dec x j).
+intro Hcut. 
+apply H1; omega.
 
-Intro HCut.
-Replace x with j ; [Assumption | Omega].
-Save.
+intro HCut.
+replace x with j; [ assumption | omega ].
+Qed.
 
 (* Substitution of the leftmost value by a smaller value *) 
 
-Lemma left_substitution : 
-   (N:Z)(A:(array N Z))(i:Z)(j:Z)(v:Z)
-   `i>=0`  -> `j<N`  -> (sorted_array A i j)
-   -> (Zle v #A[i])
-   -> (sorted_array (store A i v) i j).
+Lemma left_substitution :
+ forall (N:Z) (A:array N Z) (i j v:Z),
+   i >= 0 ->
+   j < N ->
+   sorted_array A i j -> v <= #A [i] -> sorted_array (store A i v) i j.
 Proof.
-Intros N A i j v H_i H_j H_sorted H_v.
-Unfold sorted_array ; Intros.
-
-Cut `x = i`\/`x > i`.
-(Intro Hcut ; Elim Hcut ; Clear Hcut ; Intro).
-Rewrite H2.
-Rewrite store_def_1 ; Try Omega.
-Rewrite store_def_2 ; Try Omega.
-Apply Zle_trans with m:=(access A i) ; [Assumption | Apply H_sorted ; Omega].
-
-(Rewrite store_def_2; Try Omega).
-(Rewrite store_def_2; Try Omega).
-Apply H_sorted ; Omega.
-Omega.
-Save.
+intros N A i j v H_i H_j H_sorted H_v.
+unfold sorted_array in |- *; intros.
+
+cut (x = i \/ x > i).
+intro Hcut; elim Hcut; clear Hcut; intro.
+rewrite H2.
+rewrite store_def_1; try omega.
+rewrite store_def_2; try omega.
+apply Zle_trans with (m := #A [i]); [ assumption | apply H_sorted; omega ].
+
+rewrite store_def_2; try omega.
+rewrite store_def_2; try omega.
+apply H_sorted; omega.
+omega.
+Qed.
 
 (* Substitution of the rightmost value by a larger value *)
 
-Lemma right_substitution : 
-   (N:Z)(A:(array N Z))(i:Z)(j:Z)(v:Z)
-   `i>=0`  -> `j<N`  -> (sorted_array A i j)
-   -> (Zle #A[j] v)
-   -> (sorted_array (store A j v) i j).
+Lemma right_substitution :
+ forall (N:Z) (A:array N Z) (i j v:Z),
+   i >= 0 ->
+   j < N ->
+   sorted_array A i j -> #A [j] <= v -> sorted_array (store A j v) i j.
 Proof.
-Intros N A i j v H_i H_j H_sorted H_v.
-Unfold sorted_array ; Intros.
-
-Cut `x = j-1`\/`x < j-1`.
-(Intro Hcut ; Elim Hcut ; Clear Hcut ; Intro).
-Rewrite H2.
-Replace `j-1+1` with j; [ Idtac | Omega ]. (*** Ring `j-1+1`. => BUG ***)
-Rewrite store_def_2 ; Try Omega.
-Rewrite store_def_1 ; Try Omega.
-Apply Zle_trans with m:=(access A j). 
-Apply sorted_elements with n:=i m:=j ; Try Omega ; Assumption.
-Assumption.
-
-(Rewrite store_def_2; Try Omega).
-(Rewrite store_def_2; Try Omega).
-Apply H_sorted ; Omega.
-
-Omega.
-Save.
+intros N A i j v H_i H_j H_sorted H_v.
+unfold sorted_array in |- *; intros.
+
+cut (x = j - 1 \/ x < j - 1).
+intro Hcut; elim Hcut; clear Hcut; intro.
+rewrite H2.
+replace (j - 1 + 1) with j; [ idtac | omega ]. (*** Ring `j-1+1`. => BUG ***)
+rewrite store_def_2; try omega.
+rewrite store_def_1; try omega.
+apply Zle_trans with (m := #A [j]). 
+apply sorted_elements with (n := i) (m := j); try omega; assumption.
+assumption.
+
+rewrite store_def_2; try omega.
+rewrite store_def_2; try omega.
+apply H_sorted; omega.
+
+omega.
+Qed.
 
 (* Affectation outside of the sorted region *)
 
-Lemma no_effect : 
-   (N:Z)(A:(array N Z))(i:Z)(j:Z)(k:Z)(v:Z)
-   `i>=0`  -> `j<N`  -> (sorted_array A i j)
-   -> `0<=k<i`\/`j<k<N`
-   -> (sorted_array (store A k v) i j).
+Lemma no_effect :
+ forall (N:Z) (A:array N Z) (i j k v:Z),
+   i >= 0 ->
+   j < N ->
+   sorted_array A i j ->
+   0 <= k < i \/ j < k < N -> sorted_array (store A k v) i j.
 Proof.
-Intros.
-Unfold sorted_array ; Intros. 
-Rewrite store_def_2 ; Try Omega.
-Rewrite store_def_2 ; Try Omega.
-Apply H1 ; Assumption.
-Save.
-
-Lemma sorted_array_id : (N:Z)(t1,t2:(array N Z))(g,d:Z)
-  (sorted_array t1 g d) -> (array_id t1 t2 g d) -> (sorted_array t2 g d).
+intros.
+unfold sorted_array in |- *; intros. 
+rewrite store_def_2; try omega.
+rewrite store_def_2; try omega.
+apply H1; assumption.
+Qed.
+
+Lemma sorted_array_id :
+ forall (N:Z) (t1 t2:array N Z) (g d:Z),
+   sorted_array t1 g d -> array_id t1 t2 g d -> sorted_array t2 g d.
 Proof.
-Intros N t1 t2 g d Hsorted Hid.
-Unfold array_id in Hid.
-Unfold sorted_array in Hsorted. Unfold sorted_array.
-Intros Hgd x H1x H2x.
-Rewrite <- (Hid x); [ Idtac | Omega ].
-Rewrite <- (Hid `x+1`); [ Idtac | Omega ].
-Apply Hsorted; Assumption.
-Save.
+intros N t1 t2 g d Hsorted Hid.
+unfold array_id in Hid.
+unfold sorted_array in Hsorted. unfold sorted_array in |- *.
+intros Hgd x H1x H2x.
+rewrite <- (Hid x); [ idtac | omega ].
+rewrite <- (Hid (x + 1)); [ idtac | omega ].
+apply Hsorted; assumption.
+Qed.
\ No newline at end of file