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
|
Require Import compcert.backend.Registers.
Require Import compcert.common.AST.
Require Import compcert.common.Errors.
Require Import compcert.common.Linking.
Require Import compcert.common.Globalenvs.
Require Import compcert.common.Memory.
Require Import compcert.common.Values.
Require Import compcert.lib.Maps.
Require Import vericert.common.Vericertlib.
Require Import vericert.hls.GibleSeq.
Require Import vericert.hls.GiblePar.
Require Import vericert.hls.Gible.
Require Import vericert.hls.GiblePargenproofEquiv.
Require Import vericert.hls.GiblePargen.
Require Import vericert.hls.Predicate.
Require Import vericert.hls.Abstr.
Require Import vericert.common.Monad.
#[local] Open Scope positive.
#[local] Open Scope forest.
#[local] Open Scope pred_op.
#[local] Opaque simplify.
#[local] Opaque deep_simplify.
Definition evaluable {A B C} (sem: ctx -> B -> C -> Prop) (ctx: @ctx A) p := exists b, sem ctx p b.
Definition p_evaluable {A} := @evaluable A _ _ sem_pexpr.
Definition evaluable_expr {A} := @evaluable A _ _ sem_pred.
Definition all_evaluable {A B} (ctx: @ctx A) f_p (l: predicated B) :=
forall p y, NE.In (p, y) l -> p_evaluable ctx (from_pred_op f_p p).
Definition all_evaluable2 {A B C} (ctx: @ctx A) (sem: Abstr.ctx -> B -> C -> Prop) (l: predicated B) :=
forall p y, NE.In (p, y) l -> evaluable sem ctx y.
Definition pred_forest_evaluable {A} (ctx: @ctx A) (ps: PTree.t pred_pexpr) :=
forall i p, ps ! i = Some p -> p_evaluable ctx p.
Definition forest_evaluable {A} (ctx: @ctx A) (f: forest) :=
pred_forest_evaluable ctx f.(forest_preds).
Lemma all_evaluable_cons :
forall A B pr ctx b a,
all_evaluable ctx pr (NE.cons a b) ->
@all_evaluable A B ctx pr b.
Proof.
unfold all_evaluable; intros.
enough (NE.In (p, y) (NE.cons a b)); eauto.
constructor; tauto.
Qed.
Lemma all_evaluable2_cons :
forall A B C sem ctx b a,
all_evaluable2 ctx sem (NE.cons a b) ->
@all_evaluable2 A B C ctx sem b.
Proof.
unfold all_evaluable2; intros.
enough (NE.In (p, y) (NE.cons a b)); eauto.
constructor; tauto.
Qed.
Lemma all_evaluable_cons2 :
forall A B pr ctx b a p,
@all_evaluable A B ctx pr (NE.cons (p, a) b) ->
p_evaluable ctx (from_pred_op pr p).
Proof.
unfold all_evaluable; intros.
eapply H. constructor; eauto.
Qed.
Lemma all_evaluable2_cons2 :
forall A B C sem ctx b a p,
@all_evaluable2 A B C ctx sem (NE.cons (p, a) b) ->
evaluable sem ctx a.
Proof.
unfold all_evaluable; intros.
eapply H. constructor; eauto.
Qed.
Lemma all_evaluable_cons3 :
forall A B pr ctx b p a,
all_evaluable ctx pr b ->
p_evaluable ctx (from_pred_op pr p) ->
@all_evaluable A B ctx pr (NE.cons (p, a) b).
Proof.
unfold all_evaluable; intros. inv H1. inv H3. inv H1. auto.
eauto.
Qed.
Lemma all_evaluable_singleton :
forall A B pr ctx b p,
@all_evaluable A B ctx pr (NE.singleton (p, b)) ->
p_evaluable ctx (from_pred_op pr p).
Proof.
unfold all_evaluable; intros. eapply H. constructor.
Qed.
Lemma get_forest_p_evaluable :
forall A (ctx: @ctx A) f r,
forest_evaluable ctx f ->
p_evaluable ctx (f #p r).
Proof.
intros. unfold "#p", get_forest_p'.
destruct_match. unfold forest_evaluable in *.
unfold pred_forest_evaluable in *. eauto.
unfold p_evaluable, evaluable. eexists.
constructor. constructor.
Qed.
Lemma set_forest_p_evaluable :
forall A (ctx: @ctx A) f r p,
forest_evaluable ctx f ->
p_evaluable ctx p ->
forest_evaluable ctx (f #p r <- p).
Proof.
unfold forest_evaluable, pred_forest_evaluable; intros.
destruct (peq i r); subst.
- rewrite forest_pred_gss2 in H1. now inv H1.
- rewrite forest_pred_gso2 in H1 by auto; eauto.
Qed.
Lemma evaluable_singleton :
forall A B ctx fp r,
@all_evaluable A B ctx fp (NE.singleton (T, r)).
Proof.
unfold all_evaluable, evaluable; intros.
inv H. simpl. exists true. constructor.
Qed.
Lemma evaluable_negate :
forall G (ctx: @ctx G) p,
p_evaluable ctx p ->
p_evaluable ctx (¬ p).
Proof.
unfold p_evaluable, evaluable in *; intros.
inv H. eapply sem_pexpr_negate in H0. econstructor; eauto.
Qed.
Lemma predicated_evaluable :
forall G (ctx: @ctx G) ps (p: pred_op),
pred_forest_evaluable ctx ps ->
p_evaluable ctx (from_pred_op ps p).
Proof.
unfold pred_forest_evaluable; intros. induction p; intros; cbn.
- repeat destruct_match; subst; unfold get_forest_p'.
destruct_match. eapply H; eauto. econstructor. constructor. constructor.
eapply evaluable_negate.
destruct_match. eapply H; eauto. econstructor. constructor. constructor.
- repeat econstructor.
- repeat econstructor.
- inv IHp1. inv IHp2. econstructor. apply sem_pexpr_Pand; eauto.
- inv IHp1. inv IHp2. econstructor. apply sem_pexpr_Por; eauto.
Qed.
Lemma predicated_evaluable_all :
forall A G (ctx: @ctx G) ps (p: predicated A),
pred_forest_evaluable ctx ps ->
all_evaluable ctx ps p.
Proof.
unfold all_evaluable; intros.
eapply predicated_evaluable. eauto.
Qed.
Lemma predicated_evaluable_all_list :
forall A G (ctx: @ctx G) ps (p: list (predicated A)),
pred_forest_evaluable ctx ps ->
Forall (all_evaluable ctx ps) p.
Proof.
induction p.
- intros. constructor.
- intros. constructor; eauto. apply predicated_evaluable_all; auto.
Qed.
#[local] Hint Resolve evaluable_singleton : core.
#[local] Hint Resolve predicated_evaluable : core.
#[local] Hint Resolve predicated_evaluable_all : core.
#[local] Hint Resolve predicated_evaluable_all_list : core.
Lemma evaluable_and_true :
forall G (ctx: @ctx G) ps p,
p_evaluable ctx (from_pred_op ps p) ->
p_evaluable ctx (from_pred_op ps (p ∧ T)).
Proof.
intros. unfold evaluable in *. inv H. exists (x && true). cbn.
apply sem_pexpr_Pand; auto. constructor.
Qed.
Lemma all_evaluable_predicated_map :
forall A B G (ctx: @ctx G) ps (f: A -> B) p,
all_evaluable ctx ps p ->
all_evaluable ctx ps (predicated_map f p).
Proof.
induction p.
- unfold all_evaluable; intros.
exploit NEin_map; eauto; intros. inv H1. inv H2.
eapply H; eauto.
- intros. cbn.
eapply all_evaluable_cons3. eapply IHp. eapply all_evaluable_cons; eauto.
cbn. destruct a. cbn in *. eapply all_evaluable_cons2; eauto.
Qed.
Lemma all_evaluable_predicated_map2 :
forall A B G (ctx: @ctx G) ps (f: A -> B) p,
all_evaluable ctx ps (predicated_map f p) ->
all_evaluable ctx ps p.
Proof.
induction p.
- unfold all_evaluable in *; intros.
eapply H. eapply NEin_map2; eauto.
- intros. cbn. destruct a.
cbn in H. pose proof H. eapply all_evaluable_cons in H; eauto.
eapply all_evaluable_cons2 in H0; eauto.
unfold all_evaluable. specialize (IHp H).
unfold all_evaluable in IHp.
intros. inv H1. inv H3. inv H1; eauto.
specialize (IHp _ _ H1). eauto.
Qed.
Lemma all_evaluable_map_and :
forall A B G (ctx: @ctx G) ps (a: NE.non_empty ((pred_op * A) * (pred_op * B))),
(forall p1 x p2 y,
NE.In ((p1, x), (p2, y)) a ->
p_evaluable ctx (from_pred_op ps p1)
/\ p_evaluable ctx (from_pred_op ps p2)) ->
all_evaluable ctx ps (NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end) a).
Proof.
induction a.
- intros. cbn. repeat destruct_match. inv Heqp.
unfold all_evaluable; intros. inv H0.
unfold evaluable.
exploit H. constructor.
intros [Ha Hb]. inv Ha. inv Hb.
exists (x && x0). apply sem_pexpr_Pand; auto.
- intros. unfold all_evaluable; cbn; intros. inv H0. inv H2.
+ repeat destruct_match. inv Heqp0. inv H0.
specialize (H p2 a1 p3 b ltac:(constructor; eauto)).
inv H. inv H0. inv H1. exists (x && x0).
apply sem_pexpr_Pand; eauto.
+ eapply IHa; intros. eapply H. econstructor. right. eauto.
eauto.
Qed.
Lemma all_evaluable_map_add :
forall A B G (ctx: @ctx G) ps (a: pred_op * A) (b: predicated B) p1 x p2 y,
p_evaluable ctx (from_pred_op ps (fst a)) ->
all_evaluable ctx ps b ->
NE.In (p1, x, (p2, y)) (NE.map (fun x : pred_op * B => (a, x)) b) ->
p_evaluable ctx (from_pred_op ps p1) /\ p_evaluable ctx (from_pred_op ps p2).
Proof.
induction b; intros.
- cbn in *. inv H1. unfold all_evaluable in *. specialize (H0 _ _ ltac:(constructor)).
auto.
- cbn in *. inv H1. inv H3.
+ inv H1. unfold all_evaluable in H0. specialize (H0 _ _ ltac:(constructor; eauto)); auto.
+ eapply all_evaluable_cons in H0. specialize (IHb _ _ _ _ H H0 H1). auto.
Qed.
Lemma all_evaluable_non_empty_prod :
forall A B G (ctx: @ctx G) ps p1 x p2 y (a: predicated A) (b: predicated B),
all_evaluable ctx ps a ->
all_evaluable ctx ps b ->
NE.In ((p1, x), (p2, y)) (NE.non_empty_prod a b) ->
p_evaluable ctx (from_pred_op ps p1)
/\ p_evaluable ctx (from_pred_op ps p2).
Proof.
induction a; intros.
- cbn in *. eapply all_evaluable_map_add; eauto. destruct a; cbn in *. eapply H; constructor.
- cbn in *. eapply NE.in_NEapp5 in H1. inv H1. eapply all_evaluable_map_add; eauto.
destruct a; cbn in *. eapply all_evaluable_cons2; eauto.
eapply all_evaluable_cons in H. eauto.
Qed.
Lemma all_evaluable_predicated_prod :
forall A B G (ctx: @ctx G) ps (a: predicated A) (b: predicated B),
all_evaluable ctx ps a ->
all_evaluable ctx ps b ->
all_evaluable ctx ps (predicated_prod a b).
Proof.
intros. unfold all_evaluable; intros.
unfold predicated_prod in *. exploit all_evaluable_map_and.
2: { eauto. }
intros. 2: { eauto. }
Abort. (* Requires simple lemma to prove, but this lemma is not needed. *)
Lemma cons_pred_expr_evaluable :
forall G (ctx: @ctx G) ps a b,
all_evaluable ctx ps a ->
all_evaluable ctx ps b ->
all_evaluable ctx ps (cons_pred_expr a b).
Proof.
unfold cons_pred_expr; intros.
apply all_evaluable_predicated_map.
(*now apply all_evaluable_predicated_prod.*)
Abort.
Lemma fold_right_all_evaluable :
forall G (ctx: @ctx G) ps n,
Forall (all_evaluable ctx ps) (NE.to_list n) ->
all_evaluable ctx ps (NE.fold_right cons_pred_expr (NE.singleton (T, Enil)) n).
Proof.
induction n; cbn in *; intros.
- unfold cons_pred_expr. eapply all_evaluable_predicated_map. (*eapply all_evaluable_predicated_prod.
inv H. auto. unfold all_evaluable; intros. inv H0. exists true. constructor.*) admit.
- inv H. specialize (IHn H3). (*now eapply cons_pred_expr_evaluable.*)
Abort.
Lemma merge_all_evaluable :
forall G (ctx: @ctx G) ps,
pred_forest_evaluable ctx ps ->
forall f args,
all_evaluable ctx ps (merge (list_translation args f)).
Proof.
intros. eapply predicated_evaluable_all. eauto.
Qed.
Lemma forest_evaluable_regset :
forall A f (ctx: @ctx A) n x,
forest_evaluable ctx f ->
forest_evaluable ctx f #r x <- n.
Proof.
unfold forest_evaluable, pred_forest_evaluable; intros.
eapply H. eauto.
Qed.
Lemma evaluable_impl :
forall A (ctx: @ctx A) a b,
p_evaluable ctx a ->
p_evaluable ctx b ->
p_evaluable ctx (a → b).
Proof.
unfold evaluable.
inversion_clear 1 as [b1 SEM1].
inversion_clear 1 as [b2 SEM2].
unfold Pimplies.
econstructor. apply sem_pexpr_Por;
eauto using sem_pexpr_negate.
Qed.
Lemma parts_evaluable :
forall A (ctx: @ctx A) b p0,
evaluable sem_pred ctx p0 ->
evaluable sem_pexpr ctx (Plit (b, p0)).
Proof.
intros. unfold evaluable in *. inv H.
destruct b. do 2 econstructor. eauto.
exists (negb x). constructor. rewrite negb_involutive. auto.
Qed.
Lemma p_evaluable_Pand :
forall A (ctx: @ctx A) a b,
p_evaluable ctx a ->
p_evaluable ctx b ->
p_evaluable ctx (a ∧ b).
Proof.
intros. inv H. inv H0.
econstructor. apply sem_pexpr_Pand; eauto.
Qed.
Lemma from_predicated_evaluable :
forall A (ctx: @ctx A) f b a,
pred_forest_evaluable ctx f ->
all_evaluable2 ctx sem_pred a ->
p_evaluable ctx (from_predicated b f a).
Proof.
induction a.
cbn. destruct_match; intros.
eapply evaluable_impl.
eauto using predicated_evaluable.
unfold all_evaluable2 in H0. unfold p_evaluable.
eapply parts_evaluable. eapply H0. econstructor.
intros. cbn. destruct_match.
eapply p_evaluable_Pand.
eapply all_evaluable2_cons2 in H0.
eapply evaluable_impl.
eauto using predicated_evaluable.
unfold all_evaluable2 in H0. unfold p_evaluable.
eapply parts_evaluable. eapply H0.
eapply all_evaluable2_cons in H0. eauto.
Qed.
Lemma p_evaluable_imp :
forall A (ctx: @ctx A) a b,
sem_pexpr ctx a false ->
p_evaluable ctx (a → b).
Proof.
intros. unfold "→".
unfold p_evaluable, evaluable. exists true.
constructor. replace true with (negb false) by trivial. left.
now apply sem_pexpr_negate.
Qed.
|
