-
Notifications
You must be signed in to change notification settings - Fork 0
/
Ext.v
211 lines (176 loc) · 7.11 KB
/
Ext.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
From Coq Require Import Lia.
From Elo Require Import Util.
From Elo Require Import Array.
From Elo Require Import Map.
From Elo Require Import Sem.
(* ------------------------------------------------------------------------- *)
(* step tactics *)
(* ------------------------------------------------------------------------- *)
Ltac inv_tstep := match goal with H : _ --[_]--> _ |- _ => inv H end.
Ltac inv_mstep := match goal with H : _ / _ ==[_]==> _ / _ |- _ => inv H end.
Ltac inv_cstep := match goal with H : _ / _ ~~[_, _]~~> _ / _ |- _ => inv H end.
Ltac inv_mulst := match goal with H : _ / _ ~~[_]~~>* _ / _ |- _ => inv H end.
Ltac invc_mstep :=
match goal with H : _ / _ ==[_]==> _ / _ |- _ => invc H end.
Ltac invc_cstep :=
match goal with H : _ / _ ~~[_, _]~~> _ / _ |- _ => invc H end.
Ltac invc_mulst :=
match goal with H : _ / _ ~~[_]~~>* _ / _ |- _ => invc H end.
Ltac induction_tstep :=
match goal with H : _ --[?e]--> _ |- _ =>
remember e eqn:Heq; induction H; inv Heq
end.
Ltac induction_mulst :=
match goal with
| H : _ / _ ~~[_]~~>* _ / _ |- _ =>
induction H as [| ? ? ? ? ? ? ? ? ? Hmulst ? Hcstep]
end.
(* ------------------------------------------------------------------------- *)
(* type tactics *)
(* ------------------------------------------------------------------------- *)
Ltac inv_type :=
match goal with
| H : _ |-- <{ unit }> is _ |- _ => inv H
| H : _ |-- <{ N _ }> is _ |- _ => inv H
| H : _ |-- <{ & _ :: _ }> is _ |- _ => inv H
| H : _ |-- <{ new _ _ }> is _ |- _ => inv H
| H : _ |-- <{ * _ }> is _ |- _ => inv H
| H : _ |-- <{ _ = _ }> is _ |- _ => inv H
| H : _ |-- <{ var _ }> is _ |- _ => inv H
| H : _ |-- <{ fn _ _ _ }> is _ |- _ => inv H
| H : _ |-- <{ call _ _ }> is _ |- _ => inv H
| H : _ |-- <{ _ ; _ }> is _ |- _ => inv H
| H : _ |-- <{ spawn _ }> is _ |- _ => inv H
end.
Ltac invc_type :=
match goal with
| H : _ |-- <{ unit }> is _ |- _ => invc H
| H : _ |-- <{ N _ }> is _ |- _ => invc H
| H : _ |-- <{ & _ :: _ }> is _ |- _ => invc H
| H : _ |-- <{ new _ _ }> is _ |- _ => invc H
| H : _ |-- <{ * _ }> is _ |- _ => invc H
| H : _ |-- <{ _ = _ }> is _ |- _ => invc H
| H : _ |-- <{ var _ }> is _ |- _ => invc H
| H : _ |-- <{ fn _ _ _ }> is _ |- _ => invc H
| H : _ |-- <{ call _ _ }> is _ |- _ => invc H
| H : _ |-- <{ _ ; _ }> is _ |- _ => invc H
| H : _ |-- <{ spawn _ }> is _ |- _ => invc H
end.
Ltac induction_type :=
match goal with
| H : _ |-- _ is _ |- _ => induction H
end.
(* ------------------------------------------------------------------------- *)
(* dec *)
(* ------------------------------------------------------------------------- *)
Lemma value_dec : forall t,
value t \/ ~ value t.
Proof.
intros. induction t; eauto using value; right; intros F; inv F.
Qed.
Lemma ityp_eq_dec : forall (T1 T2 : ityp),
{T1 = T2} + {T1 <> T2}.
Proof. intros. decide equality; eauto. Qed.
Lemma typ_eq_dec : forall (T1 T2 : typ),
{T1 = T2} + {T1 <> T2}.
Proof. intros. decide equality; eauto using ityp_eq_dec. Qed.
Lemma tm_eq_dec : forall (t1 t2 : tm),
{t1 = t2} + {t1 <> t2}.
Proof.
intros. decide equality; eauto using nat_eq_dec, string_eq_dec, typ_eq_dec.
Qed.
Lemma eff_eq_dec : forall (e1 e2 : eff),
{e1 = e2} + {e1 <> e2}.
Proof.
intros. decide equality; eauto using nat_eq_dec, typ_eq_dec, tm_eq_dec.
Qed.
(* ------------------------------------------------------------------------- *)
(* forall properties *)
(* ------------------------------------------------------------------------- *)
Definition forall_memory (m : mem) (P : tm -> _) : Prop :=
forall_array memory_default (fun tT => P (fst tT)) m.
Definition forall_threads (ths : threads) (P : tm -> _) : Prop :=
forall_array thread_default P ths.
Definition forall_program (m : mem) (ths : threads) (P : tm -> _) : Prop :=
(forall_memory m P) /\ (forall_threads ths P).
#[export] Hint Unfold forall_program : core.
(* ------------------------------------------------------------------------- *)
(* determinism *)
(* ------------------------------------------------------------------------- *)
Lemma deterministic_typing : forall Gamma t T1 T2,
Gamma |-- t is T1 ->
Gamma |-- t is T2 ->
T1 = T2.
Proof.
intros * Htype1. generalize dependent T2.
induction Htype1; intros ? Htype2; inv Htype2; eauto;
repeat match goal with
| IH : forall _, _ |-- ?t is _ -> _, H : _ |-- ?t is _ |- _ =>
eapply IH in H; subst
end;
congruence.
Qed.
Ltac apply_deterministic_typing :=
match goal with
| H1 : _ |-- ?t is ?T1
, H2 : _ |-- ?t is ?T2
|- _ =>
assert (Heq : T1 = T2) by eauto using deterministic_typing; subst;
try (invc Heq)
end.
(* ------------------------------------------------------------------------- *)
(* auxiliary lemmas *)
(* ------------------------------------------------------------------------- *)
Lemma tstep_length_tid : forall t ths tid e,
ths[tid] --[e]--> t ->
tid < #ths.
Proof.
intros. decompose sum (lt_eq_lt_dec tid (#ths)); subst; trivial;
simpl_array; try lia; inv_tstep.
Qed.
Lemma mstep_length_tid : forall m m' t' ths tid e,
m / ths[tid] ==[e]==> m' / t' ->
tid < #ths.
Proof.
intros. inv_mstep; eauto using tstep_length_tid.
Qed.
Lemma cstep_length_tid : forall m m' ths ths' tid e,
m / ths ~~[tid, e]~~> m' / ths' ->
tid < #ths.
Proof.
intros. inv_cstep; trivial.
Qed.
(* ------------------------------------------------------------------------- *)
(* hints *)
(* ------------------------------------------------------------------------- *)
#[export] Hint Unfold forall_array : fall.
#[export] Hint Unfold forall_memory : fall.
#[export] Hint Unfold forall_threads : fall.
#[export] Hint Extern 4 => unfold forall_array : fall.
#[export] Hint Extern 4 => unfold forall_memory : fall.
#[export] Hint Extern 4 => unfold forall_threads : fall.
(* ------------------------------------------------------------------------- *)
(* context equivalences *)
(* ------------------------------------------------------------------------- *)
Lemma ctx_eqv_safe : forall Gamma1 Gamma2,
Gamma1 === Gamma2 ->
safe Gamma1 === safe Gamma2.
Proof.
unfold map_equivalence, safe. intros * Heq k.
specialize (Heq k). rewrite Heq. trivial.
Qed.
Lemma ctx_eqv_typing : forall Gamma1 Gamma2 t T,
Gamma1 === Gamma2 ->
Gamma1 |-- t is T ->
Gamma2 |-- t is T.
Proof.
intros. generalize dependent Gamma2. induction_type; intros;
eauto using type_of, ctx_eqv_safe,
MapEquivalence.lookup, MapEquivalence.update_equivalence.
Qed.
Lemma ctx_eqv_safe_lookup : forall Gamma x,
Gamma x = None ->
(safe Gamma) x = None.
Proof.
unfold safe. intros * H. rewrite H. reflexivity.
Qed.