1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
|
(* Load Programs. *)(**********************************************************************)
(* *)
(* FIND, an historical example. *)
(* *)
(* The proof of this program was originally done by C. A. R. Hoare *)
(* and fully detailed in the following paper: *)
(* *)
(* C. A. R. Hoare, , Communications of the *)
(* ACM, 14(1), 39--45, January 1971. *)
(* *)
(**********************************************************************)
(* Jean-Christophe FILLIATRE, February 98 *)
(**********************************************************************)
(* find_proofs.v *)
(**********************************************************************)
Require Import find_spec.
Require Import find_lemmas.
Require Import Why.
Require Import Omega.
Lemma zero_f_SN : (0 <= f < Zsucc N)%Z.
Proof.
generalize le_1_f; generalize le_f_N; intros; omega.
Qed.
(* Lemmas to prove arrays bounds obligations. *)
Lemma bound_3 :
forall (m n i r:Z) (A:array Z),
i_invariant m n i r A ->
(i <= n)%Z -> (access A i < r)%Z -> (Zsucc i <= n)%Z.
Proof.
unfold i_invariant.
intros m n i r A Hi le_i_n lt_Ai_r.
decompose [and] Hi.
case (Z_le_lt_eq_dec i n le_i_n).
intro.
abstract omega.
intro eq_i_n.
elim (H2 le_i_n).
intros.
absurd (access A i < r)%Z.
cut (x = i).
intro eq_x_i.
rewrite eq_x_i in H0.
abstract omega.
abstract omega.
assumption.
Qed.
Lemma bound_4 :
forall (m n j r:Z) (A:array Z),
j_invariant m n j r A ->
(m <= j)%Z -> (r < access A j)%Z -> (m <= Zpred j)%Z.
Proof.
unfold j_invariant.
intros m n j r A Hj le_m_j lt_r_Aj.
decompose [and] Hj.
case (Z_le_lt_eq_dec m j le_m_j).
intro.
unfold Zpred.
abstract omega.
intro eq_m_j.
elim (H2 le_m_j).
intros.
absurd (r < access A j)%Z.
cut (x = j).
intro eq_x_j.
rewrite eq_x_j in H0.
abstract omega.
abstract omega.
assumption.
Qed.
(* Some subgoals of the main proof *)
Lemma subgoal_1 :
forall (m1 n1 i2 j2 i3:Z) (A A0 A1:array Z),
m_invariant m1 A0 /\
n_invariant n1 A0 /\ permut A0 A /\ (1 <= m1)%Z /\ (n1 <= N)%Z ->
(m1 < n1)%Z ->
(0 <= f < Zsucc N)%Z ->
i_invariant m1 n1 i2 (access A0 f) A1 /\
j_invariant m1 n1 j2 (access A0 f) A1 /\
m_invariant m1 A1 /\
n_invariant n1 A1 /\
(0 <= j2)%Z /\
(i2 <= N + 1)%Z /\
termination i2 j2 m1 n1 (access A0 f) A1 /\ permut A1 A ->
(i2 <= j2)%Z ->
i_invariant m1 n1 i3 (access A0 f) A1 /\
(i2 <= i3)%Z /\
(i3 <= n1)%Z /\ termination i3 j2 m1 n1 (access A0 f) A1 ->
(access A1 i3 < access A0 f)%Z ->
i_invariant m1 n1 (Zsucc i3) (access A0 f) A1 /\
(i2 <= Zsucc i3)%Z /\
(Zsucc i3 <= n1)%Z /\ termination (Zsucc i3) j2 m1 n1 (access A0 f) A1.
Proof.
intros m1 n1 i2 j2 i3 A A0 A1 HH_43 HH_42 HH_40 HH_28 HH_27 HH_4 HH_2.
split.
apply Lemma_8_15.
elim HH_4; auto.
decompose [and] HH_4.
elim H.
intros.
abstract omega.
split; [ abstract omega | split ].
cut (Zsucc i3 <= n1)%Z.
abstract omega.
apply bound_3 with (m := m1) (r := access A0 f) (A := A1); auto.
elim HH_4; auto.
abstract omega.
(* term. *)
unfold termination.
decompose [and] HH_4.
elim H3.
intro.
left.
abstract omega.
intro.
right.
decompose [and] H2.
case (Z_le_lt_eq_dec i3 f H6).
intro.
abstract omega.
intro eq_i3_f.
absurd (access A1 i3 < access A0 f)%Z; auto.
rewrite eq_i3_f.
abstract omega.
Qed.
Lemma subgoal_2 :
forall (m1 n1 i2 j2 i3 j3:Z) (A A0 A1:array Z),
m_invariant m1 A0 /\
n_invariant n1 A0 /\ permut A0 A /\ (1 <= m1)%Z /\ (n1 <= N)%Z ->
(m1 < n1)%Z ->
(0 <= f < Zsucc N)%Z ->
i_invariant m1 n1 i2 (access A0 f) A1 /\
j_invariant m1 n1 j2 (access A0 f) A1 /\
m_invariant m1 A1 /\
n_invariant n1 A1 /\
(0 <= j2)%Z /\
(i2 <= N + 1)%Z /\
termination i2 j2 m1 n1 (access A0 f) A1 /\ permut A1 A ->
(i2 <= j2)%Z ->
(i_invariant m1 n1 i3 (access A0 f) A1 /\
(i2 <= i3)%Z /\
(i3 <= n1)%Z /\ termination i3 j2 m1 n1 (access A0 f) A1) /\
(access A1 i3 >= access A0 f)%Z ->
j_invariant m1 n1 j3 (access A0 f) A1 /\
(j3 <= j2)%Z /\
(m1 <= j3)%Z /\ termination i3 j3 m1 n1 (access A0 f) A1 ->
(access A0 f < access A1 j3)%Z ->
j_invariant m1 n1 (Zpred j3) (access A0 f) A1 /\
(Zpred j3 <= j2)%Z /\
(m1 <= Zpred j3)%Z /\
termination i3 (Zpred j3) m1 n1 (access A0 f) A1.
Proof.
intros m1 n1 i2 j2 i3 j3 A A0 A1 HH_43 HH_42 HH_40 HH_28 HH_27 HH_25
HH_9 HH_7.
split.
apply Lemma_9_17.
elim HH_9; auto.
unfold j_invariant in HH_9.
decompose [and] HH_9.
elim H3.
intros.
abstract omega.
assumption.
cut (m1 <= Zpred j3)%Z.
unfold Zpred.
split; [ abstract omega | split; [ abstract omega | idtac ] ].
(* term. *)
unfold termination.
decompose [and] HH_9.
elim H4.
intro.
left.
abstract omega.
intro.
right.
decompose [and] H3.
case (Z_le_lt_eq_dec f j3 H8).
intro.
abstract omega.
intro eq_f_j3.
absurd (access A0 f < access A1 j3)%Z; auto.
rewrite <- eq_f_j3.
abstract omega.
(* *)
apply bound_4 with (n := n1) (r := access A0 f) (A := A1); auto.
elim HH_9; auto.
abstract omega.
Qed.
Lemma subgoal_3 :
forall (m0 n0 i0 j0 i1 j1:Z) (A A0 A1 A2:array Z),
array_length A = (N + 1)%Z ->
m_invariant m0 A0 /\
n_invariant n0 A0 /\ permut A0 A /\ (1 <= m0)%Z /\ (n0 <= N)%Z ->
(m0 < n0)%Z ->
(0 <= f < Zsucc N)%Z ->
i_invariant m0 n0 i0 (access A0 f) A1 /\
j_invariant m0 n0 j0 (access A0 f) A1 /\
m_invariant m0 A1 /\
n_invariant n0 A1 /\
(0 <= j0)%Z /\
(i0 <= N + 1)%Z /\
termination i0 j0 m0 n0 (access A0 f) A1 /\ permut A1 A ->
(i0 <= j0)%Z ->
(i_invariant m0 n0 i1 (access A0 f) A1 /\
(i0 <= i1)%Z /\
(i1 <= n0)%Z /\ termination i1 j0 m0 n0 (access A0 f) A1) /\
(access A1 i1 >= access A0 f)%Z ->
(j_invariant m0 n0 j1 (access A0 f) A1 /\
(j1 <= j0)%Z /\
(m0 <= j1)%Z /\ termination i1 j1 m0 n0 (access A0 f) A1) /\
(access A0 f >= access A1 j1)%Z ->
(access A1 j1 <= access A0 f <= access A1 i1)%Z ->
(i1 <= j1)%Z ->
exchange A2 A1 i1 j1 ->
(access A2 i1 <= access A0 f)%Z ->
(access A0 f <= access A2 j1)%Z ->
Zwf 0 (N + 2 + Zpred j1 - Zsucc i1) (N + 2 + j0 - i0) /\
i_invariant m0 n0 (Zsucc i1) (access A0 f) A2 /\
j_invariant m0 n0 (Zpred j1) (access A0 f) A2 /\
m_invariant m0 A2 /\
n_invariant n0 A2 /\
(0 <= Zpred j1)%Z /\
(Zsucc i1 <= N + 1)%Z /\
termination (Zsucc i1) (Zpred j1) m0 n0 (access A0 f) A2 /\ permut A2 A.
Proof.
intros m0 n0 i0 j0 i1 j1 A A0 A1 A2 HN Inv_mn Test7 Pre12 Inv_ij Test4
Inv_i Inv_j Pre10 Test3 Post7 Pre8 Pre7.
split.
(* [Zwf] *)
unfold Zwf.
decompose [and] Inv_i.
decompose [and] Inv_j.
unfold Zpred.
abstract omega.
split.
(* [i_invariant] *)
apply Lemma_8_10 with (j := j1) (A' := A1); try assumption.
SameLength A2 A1.
intuition; SameLength A1 A.
omega.
decompose [and] Inv_i.
elim H1.
abstract omega.
abstract omega.
abstract omega.
decompose [and] Inv_i.
assumption.
decompose [and] Inv_j.
assumption.
split.
(* [j_invariant] *)
apply Lemma_9_11 with (i := i1) (A' := A1); try assumption.
SameLength A2 A1.
intuition; SameLength A1 A.
omega.
decompose [and] Inv_j.
elim H1.
abstract omega.
decompose [and] Inv_i.
elim H1.
abstract omega.
decompose [and] Inv_mn.
assumption.
decompose [and] Inv_j.
assumption.
decompose [and] Inv_i.
assumption.
split.
(* [m_invariant] *)
apply Lemma_12' with (i := i1) (j := j1) (A := A1).
intuition; SameLength A1 A; omega.
decompose [and] Inv_i.
elim H1.
abstract omega.
auto with datatypes.
decompose [and] Inv_ij.
assumption.
split.
(* [n_invariant] *)
apply Lemma_13' with (i := i1) (j := j1) (A := A1).
intuition; SameLength A1 A.
omega.
decompose [and] Inv_i.
elim H1.
abstract omega.
decompose [and] Inv_j.
elim H1.
abstract omega.
auto with datatypes.
decompose [and] Inv_ij.
assumption.
split.
(* [0<=j-1] *)
unfold Zpred.
abstract omega.
split.
(* [i+1<=N+1] *)
abstract omega.
split.
(* [termination] *)
unfold termination.
left.
unfold Zpred.
decompose [and] Inv_i.
elim H1.
intros.
decompose [and] Inv_j.
elim H8.
intros.
abstract omega.
(* [permut] *)
decompose [and] Inv_ij.
eauto with datatypes.
Qed.
Lemma subgoal_5 :
forall (m1 n1 i2 j2:Z) (A A0 A1:array Z),
m_invariant m1 A0 /\
n_invariant n1 A0 /\ permut A0 A /\ (1 <= m1)%Z /\ (n1 <= N)%Z ->
(m1 < n1)%Z ->
(0 <= f < Zsucc N)%Z ->
(i_invariant m1 n1 i2 (access A0 f) A1 /\
j_invariant m1 n1 j2 (access A0 f) A1 /\
m_invariant m1 A1 /\
n_invariant n1 A1 /\
(0 <= j2)%Z /\
(i2 <= N + 1)%Z /\
termination i2 j2 m1 n1 (access A0 f) A1 /\ permut A1 A) /\
(i2 > j2)%Z ->
(m1 < i2)%Z /\ (j2 < n1)%Z ->
(f <= j2)%Z ->
Zwf 0 (j2 - m1) (n1 - m1) /\
m_invariant m1 A1 /\
n_invariant j2 A1 /\ permut A1 A /\ (1 <= m1)%Z /\ (j2 <= N)%Z.
Proof.
intros m1 n1 i2 j2 A A0 A1 HH_44 HH_43 HH_41 HH_40 HH_39 HH_37.
decompose [and] HH_40.
split;
[ idtac
| split;
[ assumption | split; [ idtac | split; [ assumption | idtac ] ] ] ].
abstract (unfold Zwf; elim H; elim H0; elim H1; elim H2; intros; omega).
apply Lemma_6_a with (m := m1) (n := n1) (i := i2) (r := access A0 f);
auto.
abstract omega.
Qed.
Lemma subgoal_6 :
forall (m1 n1 i2 j2:Z) (A A0 A1:array Z),
m_invariant m1 A0 /\
n_invariant n1 A0 /\ permut A0 A /\ (1 <= m1)%Z /\ (n1 <= N)%Z ->
(m1 < n1)%Z ->
(0 <= f < Zsucc N)%Z ->
(i_invariant m1 n1 i2 (access A0 f) A1 /\
j_invariant m1 n1 j2 (access A0 f) A1 /\
m_invariant m1 A1 /\
n_invariant n1 A1 /\
(0 <= j2)%Z /\
(i2 <= N + 1)%Z /\
termination i2 j2 m1 n1 (access A0 f) A1 /\ permut A1 A) /\
(i2 > j2)%Z ->
(m1 < i2)%Z /\ (j2 < n1)%Z ->
(f > j2)%Z ->
(i2 <= f)%Z ->
Zwf 0 (n1 - i2) (n1 - m1) /\
m_invariant i2 A1 /\
n_invariant n1 A1 /\ permut A1 A /\ (1 <= i2)%Z /\ (n1 <= N)%Z.
Proof.
intros m1 n1 i2 j2 A A0 A1 HH_44 HH_43 HH_41 HH_40 HH_39 HH_36 HH_33.
decompose [and] HH_40.
split;
[ idtac
| split;
[ idtac | split; [ assumption | split; [ assumption | idtac ] ] ] ].
abstract (unfold Zwf; elim H; elim H1; elim H2; elim H3; intros; omega).
apply Lemma_6_b with (m := m1) (n := n1) (j := j2) (r := access A0 f);
auto.
abstract omega.
Qed.
Lemma subgoal_7 :
forall (m1 n1 i2 j2:Z) (A A0 A1:array Z),
m_invariant m1 A0 /\
n_invariant n1 A0 /\ permut A0 A /\ (1 <= m1)%Z /\ (n1 <= N)%Z ->
(m1 < n1)%Z ->
(0 <= f < Zsucc N)%Z ->
(i_invariant m1 n1 i2 (access A0 f) A1 /\
j_invariant m1 n1 j2 (access A0 f) A1 /\
m_invariant m1 A1 /\
n_invariant n1 A1 /\
(0 <= j2)%Z /\
(i2 <= N + 1)%Z /\
termination i2 j2 m1 n1 (access A0 f) A1 /\ permut A1 A) /\
(i2 > j2)%Z ->
(m1 < i2)%Z /\ (j2 < n1)%Z ->
(f > j2)%Z ->
(i2 > f)%Z ->
Zwf 0 (f - f) (n1 - m1) /\
m_invariant f A1 /\
n_invariant f A1 /\ permut A1 A /\ (1 <= f <= N)%Z.
Proof.
intros m1 n1 i2 j2 A A0 A1 HH_44 HH_43 HH_41 HH_40 HH_39 HH_36 HH_32.
decompose [and] HH_40.
split;
[ idtac
| split; [ idtac | split; [ idtac | split; [ assumption | idtac ] ] ] ].
abstract (unfold Zwf; elim H; elim H0; elim H1; elim H2; intros; omega).
apply Lemma_6_c1 with
(m := m1) (n := n1) (i := i2) (j := j2) (r := access A0 f); auto.
abstract omega.
apply Lemma_6_c2 with
(m := m1) (n := n1) (i := i2) (j := j2) (r := access A0 f); auto.
abstract omega.
abstract omega.
Qed.
|
