diff options
Diffstat (limited to 'contrib/correctness/Sorted.v')
| -rw-r--r-- | contrib/correctness/Sorted.v | 202 |
1 files changed, 0 insertions, 202 deletions
diff --git a/contrib/correctness/Sorted.v b/contrib/correctness/Sorted.v deleted file mode 100644 index ca4ed880..00000000 --- a/contrib/correctness/Sorted.v +++ /dev/null @@ -1,202 +0,0 @@ -(************************************************************************) -(* 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 5920 2004-07-16 20:01:26Z herbelin $ *) - -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 |