-
Notifications
You must be signed in to change notification settings - Fork 0
/
search-max.v
242 lines (210 loc) · 8.33 KB
/
search-max.v
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
(* ============================================================================
* Kaldewaij’ search by elimination
* Bedrock implementtaion/proof by Duckki Oe (4/9/2013)
* paper: http://link.springer.com/chapter/10.1007%2F3-540-51305-1_17#page-1
* Dafny version: http://rise4fun.com/dafny/Chqv
* ========================================================================= *)
Set Implicit Arguments.
Require Import AutoSep WordLemmas.
(* ============================================================================
* specification
* ========================================================================= *)
Definition gtAll (x : W) ls := List.Forall (fun y => y <= x) ls.
Definition maxS : spec := SPEC("a", "n") reserving 10
Al ls,
PRE[V] array ls (V "a") * [| wordToNat(V "n") = length ls |]
* [| ls <> nil |]
POST[R] array ls (V "a") * [| (wordToNat R < length ls)%nat |]
* [| gtAll (selN ls (wordToNat R)) ls |].
(* ============================================================================
* implementation
* ========================================================================= *)
Definition gtAll' (x y : W) ls := List.Forall (fun z => z <= x \/ z <= y) ls.
Definition maxInv (x y : nat) ls :=
let a_x := selN ls x in
let a_y := selN ls y in
gtAll' a_x a_y (firstn x ls) /\ gtAll' a_x a_y (skipn y ls).
Inductive loopBody := loopBodyI.
Definition maxM := bmodule "max" {{
bfunction "max"("a", "n", "x", "y", "a_x", "a_y", "offset") [maxS]
"x" <- 0;;
"y" <- "n" - 1;;
[ Al ls,
PRE[V] array ls (V "a")
* [| (V "x" <= V "y")%word |]
* [| (wordToNat (V "y") < length ls)%nat |]
* [| maxInv (wordToNat (V "x")) (wordToNat (V "y")) ls |]
POST[R] array ls (V "a") * [| (wordToNat R < length ls)%nat |]
* [| gtAll (selN ls (wordToNat R)) ls |] ]
While ("x" <> "y") { Note [loopBody];;
"offset" <- 4 * "x";;
"a_x" <-* "a" + "offset";;
"offset" <- 4 * "y";;
"a_y" <-* "a" + "offset";;
If ("a_x" <= "a_y") {
"x" <- "x" + 1
}
else {
"y" <- "y" - 1
}
};;
Return "x"
end
}}.
(* ============================================================================
* Lemmas
* ========================================================================= *)
Lemma max_lem1 : forall A (ls : list A) n, wordToNat n = length ls -> ls <> nil
-> (wordToNat (n ^- natToW 1) < length ls)%nat.
destruct ls; try congruence; simpl; intros.
roundtrip; autorewrite with N; auto.
Qed.
Hint Resolve max_lem1.
Lemma max_lem2 : forall x y : W, x <> y -> x <= y -> x ^+ natToW 1 <= y.
intros; destruct_words; roundtrip; omega.
Qed.
Hint Resolve max_lem2.
Lemma max_lem3 : forall x y : W, x <> y -> x <= y -> x <= y ^- natToW 1.
intros; destruct_words; roundtrip; omega.
Qed.
Hint Resolve max_lem3.
Lemma max_lem4 : forall n (x y : W), x <> y -> x <= y -> (wordToNat y < n)%nat
-> (wordToNat (y ^- natToW 1) < n)%nat.
intros; assert (x < y) by (apply wle_wneq_wlt; auto).
destruct_words; roundtrip; omega.
Qed.
Hint Resolve max_lem4.
Lemma selN_last : forall ls : list W, selN ls (pred (Datatypes.length ls))
= List.last ls $0.
induction ls; simpl; auto.
destruct ls; simpl; auto.
Qed.
Lemma skipn_last : forall ls : list W, ls <> nil
-> skipn (pred (Datatypes.length ls)) ls
= (List.last ls $0 :: nil).
induction ls; simpl; try congruence; intros.
destruct ls; simpl in *; auto.
rewrite IHls; auto; congruence.
Qed.
Lemma maxInv_init : forall n ls, ls <> nil -> wordToNat n = length ls
-> maxInv 0 (wordToNat (n ^- natToW 1)) ls.
unfold maxInv, gtAll'; split; simpl; auto.
assert (wordToNat (n ^- natToW 1) = pred (length ls)).
{
destruct ls; try congruence; simpl in *.
roundtrip; autorewrite with N; auto.
rewrite H0; omega.
}
rewrite H1.
rewrite selN_last, skipn_last by auto.
apply List.Forall_cons; auto.
Qed.
Hint Resolve maxInv_init.
Lemma firstn_S : forall n ls, ls <> nil -> (S n < length ls)%nat
-> firstn (S n) ls
= firstn n ls ++ selN ls n :: nil.
induction n; try congruence; simpl; intros.
destruct ls; try congruence; simpl; auto.
destruct ls; try congruence; simpl; auto.
rewrite <- IHn; auto; simpl in *; try omega.
destruct ls; simpl in *; congruence || omega.
Qed.
Lemma maxInv_plus_h : forall x y ls, maxInv x y ls -> selN ls x <= selN ls y
-> (x < y)%nat -> (y < length ls)%nat
-> maxInv (S x) y ls.
unfold maxInv; unfold gtAll'; intros.
assert (ls <> nil) by (destruct ls; simpl in *; congruence || omega).
destruct H; split.
{
rewrite firstn_S by auto.
apply Forall_app; auto.
eapply Forall_impl, H; simpl; intros.
destruct H5; right; nomega.
}
{
eapply Forall_impl, H4; simpl; intros.
destruct H5; right; nomega.
}
Qed.
Lemma maxInv_plus : forall (x y : W) ls, x <> y -> x <= y
-> (wordToNat y < length ls)%nat
-> selN ls (wordToNat x) <= selN ls (wordToNat y)
-> maxInv (wordToNat x) (wordToNat y) ls
-> maxInv (wordToNat (x ^+ natToW 1)) (wordToNat y) ls.
intros; destruct_words; roundtrip.
replace (w + 1) with (S w) by omega; apply maxInv_plus_h; auto; nomega.
Qed.
Hint Resolve maxInv_plus.
Lemma skipn_pred : forall n ls, ls <> nil -> (n < length ls)%nat -> (0 < n)%nat
-> skipn (pred n) ls
= selN ls (pred n) :: skipn n ls.
induction n; simpl; intros; try omega.
destruct ls; try congruence; simpl; auto.
destruct n; simpl; auto.
rewrite <- IHn; simpl in *; auto.
destruct ls; simpl in *; omega || congruence.
Qed.
Lemma Forall_firstn_skipn : forall A P n (ls : list A),
List.Forall P (firstn n ls)
-> List.Forall P (skipn n ls)
-> List.Forall P ls.
intros; rewrite <- (firstn_skipn n); apply Forall_app; auto.
Qed.
Lemma maxInv_minus_h : forall x y ls, maxInv x y ls -> selN ls y < selN ls x
-> (x < y)%nat -> (y < length ls)%nat
-> maxInv x (pred y) ls.
unfold maxInv; unfold gtAll'; intros.
assert (ls <> nil) by (destruct ls; simpl in *; congruence || omega).
destruct H; split.
{
eapply Forall_impl, H; simpl; intros.
destruct H5; auto; left; nomega.
}
{
rewrite skipn_pred by auto.
eapply Forall_cons.
right; nomega.
eapply Forall_impl, H4; simpl; intros.
destruct H5; auto; left; nomega.
}
Qed.
Lemma maxInv_minus : forall (x y : W) ls, x <> y -> x <= y
-> (wordToNat y < length ls)%nat
-> selN ls (wordToNat y) < selN ls (wordToNat x)
-> maxInv (wordToNat x) (wordToNat y) ls
-> maxInv (wordToNat x) (wordToNat (y ^- natToW 1)) ls.
intros; destruct_words; roundtrip.
replace (w0 - 1) with (pred w0) by omega.
apply maxInv_minus_h; auto; nomega.
Qed.
Hint Resolve maxInv_minus.
Lemma maxInv_gtAll : forall x ls, maxInv x x ls -> gtAll (selN ls x) ls.
unfold maxInv, gtAll, gtAll'; intros; subst.
destruct H.
eapply Forall_impl, Forall_firstn_skipn; try eassumption.
simpl; destruct 1; auto.
Qed.
Hint Resolve maxInv_gtAll.
Lemma maxInv_eq : forall (x y : W) ls, x = y
-> maxInv (wordToNat x) (wordToNat y) ls
-> maxInv (wordToNat x) (wordToNat x) ls.
intros; subst; auto.
Qed.
Hint Resolve maxInv_eq.
(* ============================================================================
* Proof
* ========================================================================= *)
Hint Extern 1 (_ <= _) => nomega.
Ltac unstuck :=
match goal with
| _: loopBody, H: context[Assign] |- _
=> generalize dependent H; evaluate auto_ext
end; intro;
match goal with
| _: ?x <= ?y, _: (wordToNat ?y < length ?ls)%nat |- _
=> assert (x < natToW (length ls)) by nomega;
assert (y < natToW (length ls)) by nomega
end.
Theorem maxM_correct : moduleOk maxM.
vcgen; try enterFunction; post; try unstuck; sep_auto; eauto 3.
Qed.