diff options
Diffstat (limited to 'contrib/correctness/Sorted.v')
| -rw-r--r-- | contrib/correctness/Sorted.v | 202 |
1 files changed, 202 insertions, 0 deletions
diff --git a/contrib/correctness/Sorted.v b/contrib/correctness/Sorted.v new file mode 100644 index 00000000..2efe54a4 --- /dev/null +++ b/contrib/correctness/Sorted.v @@ -0,0 +1,202 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Library about sorted (sub-)arrays / Nicolas Magaud, July 1998 *) + +(* $Id: Sorted.v,v 1.7.2.1 2004/07/16 19:30:00 herbelin Exp $ *) + +Require Export Arrays. +Require Import ArrayPermut. + +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 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 : + 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 in |- *. apply natlike_ind. +intro. +replace (k + 0) with k; omega. (*** Ring `k+0` => BUG ***) + +intros. +apply Zle_trans with (m := #A [k + x]). +apply H0; omega. + +unfold Zsucc in |- *. +replace (k + (x + 1)) with (k + x + 1). +unfold sorted_array in H_sorted. +apply H_sorted; omega. + +omega. + +assumption. +Qed. + +(* one element and any of the following *) + +Lemma sorted_elements : + 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. +Qed. + +Hint Resolve sorted_elements: datatypes v62. + +(* A sub-array of a sorted array is sorted *) + +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 in |- *. +intros. +apply H; omega. +Qed. + +Hint Resolve sub_sorted_array: datatypes v62. + +(* Extension on the left of the property of being sorted *) + +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 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 ]. + +omega. +Qed. + +(* Extension on the right *) + +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 in |- *; intros. +elim (Z_lt_ge_dec x j). +intro Hcut. +apply H1; omega. + +intro HCut. +replace x with j; [ assumption | omega ]. +Qed. + +(* Substitution of the leftmost value by a smaller value *) + +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 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 : + 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 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 : + 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 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 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 |