← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to contrib/correctness/Sorted.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
contrib/correctness/Sorted.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*  Library about sorted (sub-)arrays / Nicolas Magaud, July 1998 *)
 
10
 
 
11
(* $Id: Sorted.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
12
 
 
13
Require Export Arrays.
 
14
Require Import ArrayPermut.
 
15
 
 
16
Require Import ZArithRing.
 
17
Require Import Omega.
 
18
Open Local Scope Z_scope.
 
19
 
 
20
Set Implicit Arguments.
 
21
 
 
22
(* Definition *)
 
23
 
 
24
Definition sorted_array (N:Z) (A:array N Z) (deb fin:Z) :=
 
25
  deb <= fin -> forall x:Z, x >= deb -> x < fin -> #A [x] <= #A [x + 1].
 
26
 
 
27
(* Elements of a sorted sub-array are in increasing order *)
 
28
 
 
29
(* one element and the next one *)
 
30
 
 
31
Lemma sorted_elements_1 :
 
32
 forall (N:Z) (A:array N Z) (n m:Z),
 
33
   sorted_array A n m ->
 
34
   forall k:Z,
 
35
     k >= n -> forall i:Z, 0 <= i -> k + i <= m -> #A [k] <= #A [k + i].
 
36
Proof.
 
37
intros N A n m H_sorted k H_k i H_i.
 
38
pattern i in |- *. apply natlike_ind.
 
39
intro.
 
40
replace (k + 0) with k; omega. (*** Ring `k+0` => BUG ***)
 
41
 
 
42
intros.
 
43
apply Zle_trans with (m := #A [k + x]).
 
44
apply H0; omega.
 
45
 
 
46
unfold Zsucc in |- *.
 
47
replace (k + (x + 1)) with (k + x + 1).
 
48
unfold sorted_array in H_sorted.
 
49
apply H_sorted; omega.
 
50
 
 
51
omega.
 
52
 
 
53
assumption.
 
54
Qed.
 
55
 
 
56
(* one element and any of the following *)
 
57
 
 
58
Lemma sorted_elements :
 
59
 forall (N:Z) (A:array N Z) (n m k l:Z),
 
60
   sorted_array A n m ->
 
61
   k >= n -> l < N -> k <= l -> l <= m -> #A [k] <= #A [l].
 
62
Proof.
 
63
intros.
 
64
replace l with (k + (l - k)).
 
65
apply sorted_elements_1 with (n := n) (m := m);
 
66
 [ assumption | omega | omega | omega ].
 
67
omega.
 
68
Qed.
 
69
 
 
70
Hint Resolve sorted_elements: datatypes v62.
 
71
 
 
72
(* A sub-array of a sorted array is sorted *)
 
73
 
 
74
Lemma sub_sorted_array :
 
75
 forall (N:Z) (A:array N Z) (deb fin i j:Z),
 
76
   sorted_array A deb fin ->
 
77
   i >= deb -> j <= fin -> i <= j -> sorted_array A i j.
 
78
Proof.
 
79
unfold sorted_array in |- *.
 
80
intros.
 
81
apply H; omega.
 
82
Qed.
 
83
 
 
84
Hint Resolve sub_sorted_array: datatypes v62.
 
85
 
 
86
(* Extension on the left of the property of being sorted *)
 
87
 
 
88
Lemma left_extension :
 
89
 forall (N:Z) (A:array N Z) (i j:Z),
 
90
   i > 0 ->
 
91
   j < N ->
 
92
   sorted_array A i j -> #A [i - 1] <= #A [i] -> sorted_array A (i - 1) j.
 
93
Proof.
 
94
intros; unfold sorted_array in |- *; intros.
 
95
elim (Z_ge_lt_dec x i).   (* (`x >= i`) + (`x < i`) *)
 
96
intro Hcut.
 
97
apply H1; omega.
 
98
 
 
99
intro Hcut.
 
100
replace x with (i - 1).
 
101
replace (i - 1 + 1) with i; [ assumption | omega ].
 
102
 
 
103
omega.
 
104
Qed.
 
105
 
 
106
(* Extension on the right *)
 
107
 
 
108
Lemma right_extension :
 
109
 forall (N:Z) (A:array N Z) (i j:Z),
 
110
   i >= 0 ->
 
111
   j < N - 1 ->
 
112
   sorted_array A i j -> #A [j] <= #A [j + 1] -> sorted_array A i (j + 1).
 
113
Proof.
 
114
intros; unfold sorted_array in |- *; intros.
 
115
elim (Z_lt_ge_dec x j).
 
116
intro Hcut. 
 
117
apply H1; omega.
 
118
 
 
119
intro HCut.
 
120
replace x with j; [ assumption | omega ].
 
121
Qed.
 
122
 
 
123
(* Substitution of the leftmost value by a smaller value *) 
 
124
 
 
125
Lemma left_substitution :
 
126
 forall (N:Z) (A:array N Z) (i j v:Z),
 
127
   i >= 0 ->
 
128
   j < N ->
 
129
   sorted_array A i j -> v <= #A [i] -> sorted_array (store A i v) i j.
 
130
Proof.
 
131
intros N A i j v H_i H_j H_sorted H_v.
 
132
unfold sorted_array in |- *; intros.
 
133
 
 
134
cut (x = i \/ x > i).
 
135
intro Hcut; elim Hcut; clear Hcut; intro.
 
136
rewrite H2.
 
137
rewrite store_def_1; try omega.
 
138
rewrite store_def_2; try omega.
 
139
apply Zle_trans with (m := #A [i]); [ assumption | apply H_sorted; omega ].
 
140
 
 
141
rewrite store_def_2; try omega.
 
142
rewrite store_def_2; try omega.
 
143
apply H_sorted; omega.
 
144
omega.
 
145
Qed.
 
146
 
 
147
(* Substitution of the rightmost value by a larger value *)
 
148
 
 
149
Lemma right_substitution :
 
150
 forall (N:Z) (A:array N Z) (i j v:Z),
 
151
   i >= 0 ->
 
152
   j < N ->
 
153
   sorted_array A i j -> #A [j] <= v -> sorted_array (store A j v) i j.
 
154
Proof.
 
155
intros N A i j v H_i H_j H_sorted H_v.
 
156
unfold sorted_array in |- *; intros.
 
157
 
 
158
cut (x = j - 1 \/ x < j - 1).
 
159
intro Hcut; elim Hcut; clear Hcut; intro.
 
160
rewrite H2.
 
161
replace (j - 1 + 1) with j; [ idtac | omega ]. (*** Ring `j-1+1`. => BUG ***)
 
162
rewrite store_def_2; try omega.
 
163
rewrite store_def_1; try omega.
 
164
apply Zle_trans with (m := #A [j]). 
 
165
apply sorted_elements with (n := i) (m := j); try omega; assumption.
 
166
assumption.
 
167
 
 
168
rewrite store_def_2; try omega.
 
169
rewrite store_def_2; try omega.
 
170
apply H_sorted; omega.
 
171
 
 
172
omega.
 
173
Qed.
 
174
 
 
175
(* Affectation outside of the sorted region *)
 
176
 
 
177
Lemma no_effect :
 
178
 forall (N:Z) (A:array N Z) (i j k v:Z),
 
179
   i >= 0 ->
 
180
   j < N ->
 
181
   sorted_array A i j ->
 
182
   0 <= k < i \/ j < k < N -> sorted_array (store A k v) i j.
 
183
Proof.
 
184
intros.
 
185
unfold sorted_array in |- *; intros. 
 
186
rewrite store_def_2; try omega.
 
187
rewrite store_def_2; try omega.
 
188
apply H1; assumption.
 
189
Qed.
 
190
 
 
191
Lemma sorted_array_id :
 
192
 forall (N:Z) (t1 t2:array N Z) (g d:Z),
 
193
   sorted_array t1 g d -> array_id t1 t2 g d -> sorted_array t2 g d.
 
194
Proof.
 
195
intros N t1 t2 g d Hsorted Hid.
 
196
unfold array_id in Hid.
 
197
unfold sorted_array in Hsorted. unfold sorted_array in |- *.
 
198
intros Hgd x H1x H2x.
 
199
rewrite <- (Hid x); [ idtac | omega ].
 
200
rewrite <- (Hid (x + 1)); [ idtac | omega ].
 
201
apply Hsorted; assumption.
 
202
Qed.
 
 
b'\\ No newline at end of file'