-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathNoInit.v
349 lines (296 loc) · 12.6 KB
/
NoInit.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
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
From Elo Require Import Core.
(* ------------------------------------------------------------------------- *)
(* no-init *)
(* ------------------------------------------------------------------------- *)
Inductive no_init (ad : addr) : tm -> Prop :=
| noinit_unit : no_init ad <{unit }>
| noinit_nat : forall n, no_init ad <{nat n }>
| noinit_plus : forall t1 t2, no_init ad t1 ->
no_init ad t2 ->
no_init ad <{t1 + t2 }>
| noinit_monus : forall t1 t2, no_init ad t1 ->
no_init ad t2 ->
no_init ad <{t1 - t2 }>
| noinit_seq : forall t1 t2, no_init ad t1 ->
no_init ad t2 ->
no_init ad <{t1; t2 }>
| noinit_if : forall t1 t2 t3, no_init ad t1 ->
no_init ad t2 ->
no_init ad t3 ->
no_init ad <{if t1 then t2 else t3 end}>
| noinit_while : forall t1 t2, no_init ad t1 ->
no_init ad t2 ->
no_init ad <{while t1 do t2 end }>
| noinit_var : forall x, no_init ad <{var x }>
| noinit_fun : forall x Tx t, no_init ad t ->
no_init ad <{fn x Tx t }>
| noinit_call : forall t1 t2, no_init ad t1 ->
no_init ad t2 ->
no_init ad <{call t1 t2 }>
| noinit_ref : forall ad' T, no_init ad <{&ad' : T }>
| noinit_new : forall T t, no_init ad t ->
no_init ad <{new t : T }>
| noinit_init : forall ad' T t, ad <> ad' ->
no_init ad t ->
no_init ad <{init ad' t : T }>
| noinit_load : forall t, no_init ad t ->
no_init ad <{*t }>
| noinit_asg : forall t1 t2, no_init ad t1 ->
no_init ad t2 ->
no_init ad <{t1 := t2 }>
| noinit_acq : forall t1 x t2, no_init ad t1 ->
no_init ad t2 ->
no_init ad <{acq t1 x t2 }>
| noinit_cr : forall ad' t, no_init ad t ->
no_init ad <{cr ad' t }>
| noinit_wait : forall t, no_init ad t ->
no_init ad <{wait t }>
| noinit_reacq : forall ad', no_init ad <{reacq ad' }>
| noinit_spawn : forall t, no_init ad t ->
no_init ad <{spawn t }>
.
(* inversion --------------------------------------------------------------- *)
Local Ltac _noinit tt :=
match goal with
| H : no_init _ <{unit }> |- _ => clear H
| H : no_init _ <{nat _ }> |- _ => clear H
| H : no_init _ <{_ + _ }> |- _ => tt H
| H : no_init _ <{_ - _ }> |- _ => tt H
| H : no_init _ <{_; _ }> |- _ => tt H
| H : no_init _ <{if _ then _ else _ end}> |- _ => tt H
| H : no_init _ <{while _ do _ end }> |- _ => tt H
| H : no_init _ <{var _ }> |- _ => clear H
| H : no_init _ <{fn _ _ _ }> |- _ => tt H
| H : no_init _ <{call _ _ }> |- _ => tt H
| H : no_init _ <{&_ : _ }> |- _ => clear H
| H : no_init _ <{new _ : _ }> |- _ => tt H
| H : no_init ?ad <{init ?ad _ : _ }> |- _ => invc H; auto
| H : no_init _ <{init _ _ : _ }> |- _ => tt H
| H : no_init _ <{* _ }> |- _ => tt H
| H : no_init _ <{_ := _ }> |- _ => tt H
| H : no_init _ <{acq _ _ _ }> |- _ => tt H
| H : no_init _ <{cr _ _ }> |- _ => tt H
| H : no_init _ <{wait _ }> |- _ => tt H
| H : no_init _ <{reacq _ }> |- _ => clear H
| H : no_init _ <{spawn _ }> |- _ => tt H
end.
Ltac inv_noinit := _noinit inv.
Ltac invc_noinit := _noinit invc.
(* decidability ------------------------------------------------------------ *)
Lemma noinit_dec : forall ad t,
Decidable.decidable (no_init ad t).
Proof.
unfold Decidable.decidable. unfold not. intros.
induction t; auto using no_init;
(destruct IHt1, IHt2, IHt3 || destruct IHt1, IHt2 || destruct IHt);
auto using no_init;
try solve [right; intros; invc_noinit; auto].
match goal with ad1 : addr, ad2 : addr |- _ => nat_eq_dec ad1 ad2 end;
auto using no_init.
right. intros. invc_noinit.
Qed.
(* lemmas ------------------------------------------------------------------ *)
Lemma noinit_init_term : forall ad t1 t2 ad' t',
no_init ad t1 ->
t1 --[e_init ad' t']--> t2 ->
no_init ad t'.
Proof.
intros. ind_tstep; invc_noinit; auto using no_init.
Qed.
Lemma noinit_write_term : forall ad t1 t2 ad' t',
no_init ad t1 ->
t1 --[e_write ad' t']--> t2 ->
no_init ad t'.
Proof.
intros. ind_tstep; invc_noinit; auto using no_init.
Qed.
Lemma noinit_init_contradiction : forall t1 t2 ad t,
no_init ad t1 ->
t1 --[e_init ad t]--> t2 ->
False.
Proof.
intros. ind_tstep; invc_noinit; auto.
Qed.
(* preservation lemmas ----------------------------------------------------- *)
Lemma noinit_subst : forall ad x tx t,
no_init ad t ->
no_init ad tx ->
no_init ad <{[x := tx] t}>.
Proof.
intros. induction t; invc_noinit;
simpl in *; repeat destruct _str_eq_dec; auto using no_init.
Qed.
(* preservation ------------------------------------------------------------ *)
Local Ltac solve_noinit_preservation :=
intros; ind_tstep; repeat invc_noinit; auto using noinit_subst, no_init.
Lemma noinit_preservation_none : forall ad t1 t2,
no_init ad t1 ->
t1 --[e_none]--> t2 ->
no_init ad t2.
Proof. solve_noinit_preservation. Qed.
Lemma noinit_preservation_alloc : forall ad t1 t2 ad' T',
ad <> ad' ->
no_init ad t1 ->
t1 --[e_alloc ad' T']--> t2 ->
no_init ad t2.
Proof. solve_noinit_preservation. Qed.
Lemma noinit_preservation_init : forall ad t1 t2 ad' t',
no_init ad t1 ->
t1 --[e_init ad' t']--> t2 ->
no_init ad t2.
Proof. solve_noinit_preservation. Qed.
Lemma noinit_preservation_read : forall ad t1 t2 ad' t',
no_init ad t' ->
(* --- *)
no_init ad t1 ->
t1 --[e_read ad' t']--> t2 ->
no_init ad t2.
Proof. solve_noinit_preservation. Qed.
Lemma noinit_preservation_write : forall ad t1 t2 ad' t',
no_init ad t1 ->
t1 --[e_write ad' t']--> t2 ->
no_init ad t2.
Proof. solve_noinit_preservation. Qed.
Lemma noinit_preservation_acq : forall ad t1 t2 ad' t',
no_init ad t' ->
(* --- *)
no_init ad t1 ->
t1 --[e_acq ad' t']--> t2 ->
no_init ad t2.
Proof. solve_noinit_preservation. Qed.
Lemma noinit_preservation_rel : forall ad t1 t2 ad',
no_init ad t1 ->
t1 --[e_rel ad']--> t2 ->
no_init ad t2.
Proof. solve_noinit_preservation. Qed.
Lemma noinit_preservation_wacq : forall ad t1 t2 ad',
no_init ad t1 ->
t1 --[e_wacq ad']--> t2 ->
no_init ad t2.
Proof. solve_noinit_preservation. Qed.
Lemma noinit_preservation_wrel : forall ad t1 t2 ad',
no_init ad t1 ->
t1 --[e_wrel ad']--> t2 ->
no_init ad t2.
Proof. solve_noinit_preservation. Qed.
Lemma noinit_preservation_spawn : forall ad t1 t2 t',
no_init ad t1 ->
t1 --[e_spawn t']--> t2 ->
no_init ad t2.
Proof. solve_noinit_preservation. Qed.
Lemma noinit_preservation_spawned : forall ad t1 t2 t',
no_init ad t1 ->
t1 --[e_spawn t']--> t2 ->
no_init ad t'.
Proof. solve_noinit_preservation. Qed.
(* ------------------------------------------------------------------------- *)
(* no-inits *)
(* ------------------------------------------------------------------------- *)
(*
(!!!) no-inits is an initial condition.
*)
Definition no_inits (t : tm) := forall ad, no_init ad t.
(* inversion --------------------------------------------------------------- *)
Local Ltac solve_inv_noinits :=
unfold no_inits; intros; repeat split; intros; spec; invc_noinit; auto.
Local Lemma inv_noinits_plus : forall t1 t2,
no_inits <{t1 + t2}> -> no_inits t1 /\ no_inits t2.
Proof. solve_inv_noinits. Qed.
Local Lemma inv_noinits_monus : forall t1 t2,
no_inits <{t1 - t2}> -> no_inits t1 /\ no_inits t2.
Proof. solve_inv_noinits. Qed.
Local Lemma inv_noinits_seq : forall t1 t2,
no_inits <{t1; t2}> -> no_inits t1 /\ no_inits t2.
Proof. solve_inv_noinits. Qed.
Local Lemma inv_noinits_if : forall t1 t2 t3,
no_inits (tm_if t1 t2 t3) -> no_inits t1 /\ no_inits t2 /\ no_inits t3.
Proof. solve_inv_noinits. Qed.
Local Lemma inv_noinits_while : forall t1 t2,
no_inits <{while t1 do t2 end}> -> no_inits t1 /\ no_inits t2.
Proof. solve_inv_noinits. Qed.
Local Lemma inv_noinits_fun : forall x Tx t,
no_inits <{fn x Tx t}> -> no_inits t.
Proof. solve_inv_noinits. Qed.
Local Lemma inv_noinits_call : forall t1 t2,
no_inits <{call t1 t2}> -> no_inits t1 /\ no_inits t2.
Proof. solve_inv_noinits. Qed.
Local Lemma inv_noinits_new : forall t T,
no_inits <{new t : T}> -> no_inits t.
Proof. solve_inv_noinits. Qed.
Local Lemma inv_noinits_init : forall ad t T,
no_inits <{init ad t : T}> -> False.
Proof. solve_inv_noinits. Qed.
Local Lemma inv_noinits_load : forall t,
no_inits <{*t}> -> no_inits t.
Proof. solve_inv_noinits. Qed.
Local Lemma inv_noinits_asg : forall t1 t2,
no_inits <{t1 := t2}> -> no_inits t1 /\ no_inits t2.
Proof. solve_inv_noinits. Qed.
Local Lemma inv_noinits_acq : forall t1 x t2,
no_inits <{acq t1 x t2}> -> no_inits t1 /\ no_inits t2.
Proof. solve_inv_noinits. Qed.
Local Lemma inv_noinits_cr : forall ad t,
no_inits <{cr ad t}> -> no_inits t.
Proof. solve_inv_noinits. Qed.
Local Lemma inv_noinits_wait : forall t,
no_inits <{wait t}> -> no_inits t.
Proof. solve_inv_noinits. Qed.
Local Lemma inv_noinits_spawn : forall t,
no_inits <{spawn t}> -> no_inits t.
Proof. solve_inv_noinits. Qed.
Ltac invc_noinits :=
match goal with
| H : no_inits <{unit }> |- _ => clear H
| H : no_inits <{nat _ }> |- _ => clear H
| H : no_inits <{_ + _ }> |- _ => eapply inv_noinits_plus in H
| H : no_inits <{_ - _ }> |- _ => eapply inv_noinits_monus in H
| H : no_inits <{_; _ }> |- _ => eapply inv_noinits_seq in H
| H : no_inits (tm_if _ _ _ ) |- _ => eapply inv_noinits_if in H
| H : no_inits (tm_while _ _ ) |- _ => eapply inv_noinits_while in H
| H : no_inits <{var _ }> |- _ => clear H
| H : no_inits <{fn _ _ _ }> |- _ => eapply inv_noinits_fun in H
| H : no_inits <{call _ _ }> |- _ => eapply inv_noinits_call in H
| H : no_inits <{& _ : _ }> |- _ => clear H
| H : no_inits <{new _ : _ }> |- _ => eapply inv_noinits_new in H
| H : no_inits <{init _ _ : _}> |- _ => eapply inv_noinits_init in H; auto
| H : no_inits <{* _ }> |- _ => eapply inv_noinits_load in H
| H : no_inits <{_ := _ }> |- _ => eapply inv_noinits_asg in H
| H : no_inits <{acq _ _ _ }> |- _ => eapply inv_noinits_acq in H
| H : no_inits <{cr _ _ }> |- _ => eapply inv_noinits_cr in H
| H : no_inits <{wait _ }> |- _ => eapply inv_noinits_wait in H
| H : no_inits <{reacq _ }> |- _ => clear H
| H : no_inits <{spawn _ }> |- _ => eapply inv_noinits_spawn in H
end;
repeat match goal with
| H : no_inits _ /\ no_inits _ |- _ => destruct H
| H : no_inits _ /\ no_inits _ /\ no_inits _ |- _ => destruct H as [? [? ?]]
end.
(* lemmas ------------------------------------------------------------------ *)
Corollary noinit_from_noinits : forall ad t,
no_inits t ->
no_init ad t.
Proof.
unfold no_inits. auto.
Qed.
Corollary noinits_init_term : forall t1 t2 ad' t',
no_inits t1 ->
t1 --[e_init ad' t']--> t2 ->
no_inits t'.
Proof.
unfold no_inits. eauto using noinit_init_term.
Qed.
Corollary noinits_write_term : forall t1 t2 ad' t',
no_inits t1 ->
t1 --[e_write ad' t']--> t2 ->
no_inits t'.
Proof.
unfold no_inits. eauto using noinit_write_term.
Qed.
(* preservation lemmas ----------------------------------------------------- *)
Corollary noinits_subst : forall x tx t,
no_inits t ->
no_inits tx ->
no_inits <{[x := tx] t}>.
Proof.
intros ** ?. auto using noinit_subst.
Qed.