compatibility.v 9.91 KB
Newer Older
1
From solutions Require Export sem_typed sem_operators.
2

3
(** * Compatibility lemmas *)
Robbert Krebbers's avatar
Robbert Krebbers committed
4
5
6
(** We prove that the logical relations, i.e., the semantic typing judgment,
that we have defined is compatible with typing rules. That is, the logical
relations is a congruence with respect to the typing rules.
Amin Timany's avatar
Amin Timany committed
7

Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
10
These compatibility lemmas are what one gets when the syntactic typing judgment
is replaced semantic typing judgment in syntactic typing rules. For instance
([sem_typed_pair]):
Amin Timany's avatar
Amin Timany committed
11
12

<<
Robbert Krebbers's avatar
Robbert Krebbers committed
13
14
15
   Γ ⊢ e1 : τ1        Γ ⊢ e2 : τ2
  --------------------------------
       Γ ⊢ (e1, e2) : τ1 × τ2
Amin Timany's avatar
Amin Timany committed
16
>>
Robbert Krebbers's avatar
Robbert Krebbers committed
17
18

becomes:
Amin Timany's avatar
Amin Timany committed
19
20

<<
Robbert Krebbers's avatar
Robbert Krebbers committed
21
  (Γ ⊨ e1 : A1) -∗ (Γ ⊨ e2 : A2) -∗ Γ ⊢ (e1, e2) : A1 * A2
Amin Timany's avatar
Amin Timany committed
22
>>
Robbert Krebbers's avatar
Robbert Krebbers committed
23
*)
Amin Timany's avatar
Amin Timany committed
24

25
Section compatibility.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
  Context `{!heapG Σ}.
27
28
29
  Implicit Types A B : sem_ty Σ.
  Implicit Types C : sem_ty Σ  sem_ty Σ.

30
31
  (** * Compatibility rules for expression typing *)
  (** * Variables *)
Robbert Krebbers's avatar
Robbert Krebbers committed
32
  Lemma Var_sem_typed Γ (x : string) A : Γ !! x = Some A  (Γ  x : A)%I.
33
34
35
36
37
38
  Proof.
    iIntros (HΓx vs) "!# #HΓ /=".
    iDestruct (env_sem_typed_lookup with "HΓ") as (v ->) "HA"; first done.
    by iApply wp_value.
  Qed.

39
  Lemma Val_sem_typed Γ v A :  v : A - Γ  v : A.
40
41
42
43
  Proof.
    iIntros "#Hv" (vs) "!# #HΓ /=".
    iApply wp_value. iApply "Hv".
  Qed.
44

45
  (** * Products and sums *)
46
  Lemma Pair_sem_typed Γ e1 e2 A1 A2 :
47
    Γ  e1 : A1 - Γ  e2 : A2 - Γ  (e1,e2) : A1 * A2.
48
49
50
51
52
53
  Proof.
    iIntros "#H1 #H2" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H2 [//])"); iIntros (w2) "#HA2".
    wp_apply (wp_wand with "(H1 [//])"); iIntros (w1) "#HA1".
    wp_pures. iExists w1, w2. auto.
  Qed.
54
  Lemma Fst_sem_typed Γ e A1 A2 : Γ  e : A1 * A2 - Γ  Fst e : A1.
55
56
57
58
59
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H [//])"); iIntros (w).
    iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures.
  Qed.
60
  (* REMOVE *) Lemma Snd_sem_typed Γ e A1 A2 : Γ  e : A1 * A2 - Γ  Snd e : A2.
61
62
63
64
65
66
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H [//])"); iIntros (w).
    iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures.
  Qed.

67
  Lemma InjL_sem_typed Γ e A1 A2 : Γ  e : A1 - Γ  InjL e : A1 + A2.
68
  (* REMOVE *) Proof.
69
70
71
72
    iIntros "#H" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HA".
    wp_pures. iLeft. iExists w. auto.
  Qed.
73
  (* REMOVE *) Lemma InjR_sem_typed Γ e A1 A2 : Γ  e : A2 - Γ  InjR e : A1 + A2.
74
75
76
77
78
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HA".
    wp_pures. iRight. iExists w. auto.
  Qed.
79
  Lemma Case_sem_typed Γ e e1 e2 A1 A2 B :
80
    Γ  e : A1 + A2 - Γ  e1 : (A1  B) - Γ  e2 : (A2  B) -
81
    Γ  Case e e1 e2 : B.
82
  (* REMOVE *) Proof.
83
84
85
86
87
88
89
90
    iIntros "#H #H1 #H2" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H [//])"); iIntros (w) "#[HA|HA]".
    - iDestruct "HA" as (w1 ->) "HA". wp_pures.
      wp_apply (wp_wand with "(H1 [//])"); iIntros (v) "#HAB". by iApply "HAB".
    - iDestruct "HA" as (w2 ->) "HA". wp_pures.
      wp_apply (wp_wand with "(H2 [//])"); iIntros (v) "#HAB". by iApply "HAB".
  Qed.

91
  (** * Functions *)
92
  Lemma Rec_sem_typed Γ f x e A1 A2 :
93
94
    binder_insert f (A1  A2)%sem_ty (binder_insert x A1 Γ)  e : A2 -
    Γ  (rec: f x := e) : (A1  A2).
95
96
97
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=". wp_pures. iLöb as "IH".
    iIntros "!#" (v) "#HA1". wp_pures. set (r := RecV f x _).
Robbert Krebbers's avatar
Robbert Krebbers committed
98
99
    rewrite -subst_map_binder_insert_2. iApply "H".
    iApply (env_sem_typed_insert with "IH"). by iApply env_sem_typed_insert.
100
101
  Qed.

102
  Lemma App_sem_typed Γ e1 e2 A1 A2 :
103
    Γ  e1 : (A1  A2) - Γ  e2 : A1 - Γ  e1 e2 : A2.
104
105
106
107
108
109
  Proof.
    iIntros "#H1 #H2" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H2 [//])"); iIntros (w) "#HA1".
    wp_apply (wp_wand with "(H1 [//])"); iIntros (v) "#HA". by iApply "HA".
  Qed.

110
  (** * Polymorphic functions and existentials *)
111
  Lemma TLam_sem_typed Γ e C : ( A, Γ  e : C A) - Γ  (Λ: e) :  A, C A.
112
113
114
115
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=". wp_pures.
    iIntros "!#" (A) "/=". wp_pures. by iApply ("H" $! A).
  Qed.
116
  Lemma TApp_sem_typed Γ e C A : (Γ  e :  A, C A) - Γ  e <_> : C A.
117
118
119
120
121
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB". by iApply ("HB" $! A).
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
122
  Lemma Pack_sem_typed Γ e C A : Γ  e : C A - Γ  (pack: e) :  A, C A.
123
  (* REMOVE *) Proof.
124
    iIntros "#H" (vs) "!# #HΓ /=".
Robbert Krebbers's avatar
Robbert Krebbers committed
125
126
    wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB".
    wp_lam. by iExists A.
127
  Qed.
128
  Lemma Unpack_sem_typed Γ x e1 e2 C B :
129
130
    (Γ  e1 :  A, C A) - ( A, binder_insert x (C A) Γ  e2 : B) -
    Γ  (unpack: x := e1 in e2) : B.
131
  (* REMOVE *) Proof.
132
133
134
135
136
137
138
139
    iIntros "#H1 #H2" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H1 [//])"); iIntros (v); iDestruct 1 as (A) "#HC".
    rewrite /exist_unpack; wp_pures. rewrite -subst_map_binder_insert.
    wp_apply (wp_wand with "(H2 [])").
    { by iApply env_sem_typed_insert. }
    auto.
  Qed.

140
  (** ** Heap operations *)
141
  Lemma Alloc_sem_typed Γ e A : Γ  e : A - Γ  ref e : ref A.
142
143
144
145
146
147
148
149
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=".
    wp_bind (subst_map _ e). iApply (wp_wand with "(H [//])"); iIntros (w) "HA".
    iApply wp_fupd. wp_alloc l as "Hl".
    iMod (inv_alloc (tyN .@ l) _ ( v, l  v  A v)%I with "[Hl HA]") as "#?".
    { iExists w. iFrame. }
    iModIntro. iExists l; auto.
  Qed.
150
  Lemma Load_sem_typed Γ e A : Γ  e : ref A - Γ  ! e : A.
151
152
153
154
155
156
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=".
    wp_bind (subst_map _ e). iApply (wp_wand with "(H [//])"); iIntros (w).
    iDestruct 1 as (l ->) "#?".
    iInv (tyN.@l) as (v) "[>Hl HA]". wp_load. eauto 10.
  Qed.
157
  Lemma Store_sem_typed Γ e1 e2 A :
158
    Γ  e1 : ref A - Γ  e2 : A - Γ  (e1 <- e2) : ().
159
  (* REMOVE *) Proof.
160
161
162
163
164
    iIntros "#H1 #H2" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H2 [//])"); iIntros (w2) "#HA".
    wp_apply (wp_wand with "(H1 [//])"); iIntros (w1); iDestruct 1 as (l ->) "#?".
    iInv (tyN.@l) as (v) "[>Hl _]". wp_store. eauto 10.
  Qed.
165
  Lemma FAA_sem_typed Γ e1 e2 :
166
    Γ  e1 : ref sem_ty_int - Γ  e2 : sem_ty_int - Γ  FAA e1 e2 : sem_ty_int.
167
  (* REMOVE *) Proof.
168
169
170
171
172
173
    iIntros "#H1 #H2" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H2 [//])"); iIntros (w2); iDestruct 1 as (n) "->".
    wp_apply (wp_wand with "(H1 [//])"); iIntros (w1); iDestruct 1 as (l ->) "#?".
    iInv (tyN.@l) as (v) "[>Hl Hv]"; iDestruct "Hv" as (n') "> ->".
    wp_faa. iModIntro. eauto 10.
  Qed.
174
  Lemma CmpXchg_sem_typed Γ A e1 e2 e3 :
175
    SemTyUnboxed A 
176
177
    Γ  e1 : ref A - Γ  e2 : A - Γ  e3 : A -
    Γ  CmpXchg e1 e2 e3 : A * sem_ty_bool.
178
  (* REMOVE *) Proof.
179
180
181
182
183
184
185
186
187
    intros. iIntros "#H1 #H2 #H3" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H3 [//])"); iIntros (w3) "HA3".
    wp_apply (wp_wand with "(H2 [//])"); iIntros (w2) "HA2".
    iDestruct (sem_ty_unboxed with "HA2") as %?.
    wp_apply (wp_wand with "(H1 [//])"); iIntros (w1); iDestruct 1 as (l ->) "#?".
    iInv (tyN.@l) as (v) "[>Hl #Hv]". wp_cmpxchg as ?|?; iModIntro;
      (iSplitL; [by eauto 12 with iFrame | iExists _, _; eauto]).
  Qed.

188
  (** ** Operators *)
189
  Lemma UnOp_sem_typed Γ e op A B :
190
    SemTyUnOp op A B  Γ  e : A - Γ  UnOp op e : B.
191
192
193
194
195
  Proof.
    intros ?. iIntros "#H" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H [//])"); iIntros (v) "#HA".
    iDestruct (sem_ty_un_op with "HA") as (w ?) "#HB". by wp_unop.
  Qed.
196
  Lemma BinOp_sem_typed Γ e1 e2 op A1 A2 B :
197
    SemTyBinOp op A1 A2 B  Γ  e1 : A1 - Γ  e2 : A2 - Γ  BinOp op e1 e2 : B.
198
  (* REMOVE *) Proof.
199
200
201
202
203
204
    intros. iIntros "#H1 #H2" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H2 [//])"); iIntros (v2) "#HA2".
    wp_apply (wp_wand with "(H1 [//])"); iIntros (v1) "#HA1".
    iDestruct (sem_ty_bin_op with "HA1 HA2") as (w ?) "#HB". by wp_binop.
  Qed.

205
  Lemma If_sem_typed Γ e e1 e2 B :
206
    Γ  e : sem_ty_bool - Γ  e1 : B - Γ  e2 : B -
207
    Γ  (if: e then e1 else e2) : B.
208
  (* REMOVE *) Proof.
209
210
211
212
213
    iIntros "#H #H1 #H2" (vs) "!# #HΓ /=".
    iSpecialize ("H1" with "HΓ"). iSpecialize ("H2" with "HΓ").
    wp_apply (wp_wand with "(H [//])"); iIntros (w). iDestruct 1 as ([]) "->"; by wp_if.
  Qed.

214
  (** ** Fork *)
215
  Lemma Fork_sem_typed Γ e : Γ  e : () - Γ  Fork e : ().
216
  (* REMOVE *) Proof.
217
218
219
    iIntros "#H" (vs) "!# #HΓ /=".
    wp_apply wp_fork; last done. by iApply (wp_wand with "(H [//])").
  Qed.
220

221
222
  (** * Compatibility rules for value typing *)
  (** ** Base types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
223
  Lemma UnitV_sem_typed : ( #() : ())%I.
224
  Proof. by iPureIntro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
  Lemma BoolV_sem_typed (b : bool) : ( #b : sem_ty_bool)%I.
226
  Proof. by iExists b. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
227
  Lemma IntV_sem_typed (n : Z) : ( #n : sem_ty_int)%I.
228
  (* REMOVE *) Proof. by iExists n. Qed.
229

230
  (** ** Products and sums *)
231
  Lemma PairV_sem_typed v1 v2 τ1 τ2 :
232
     v1 : τ1 -  v2 : τ2 -
233
234
235
     PairV v1 v2 : (τ1 * τ2).
  Proof. iIntros "#H1 #H2". iExists v1, v2. auto. Qed.
  Lemma InjLV_sem_typed v τ1 τ2 :
236
     v : τ1 -
237
238
239
     InjLV v : (τ1 + τ2).
  Proof. iIntros "H". iLeft. auto. Qed.
  Lemma InjRV_sem_typed v τ1 τ2 :
240
     v : τ2 -
241
242
243
     InjRV v : (τ1 + τ2).
  Proof. iIntros "H". iRight. auto. Qed.

244
  (** ** Functions *)
245
  Lemma RecV_sem_typed f x e A B :
246
    binder_insert f (A  B)%sem_ty (binder_insert x A )  e : B -
247
248
249
250
251
252
253
254
     RecV f x e : (A  B).
  Proof.
    iIntros "#H". iLöb as "IH".
    iIntros "!#" (v) "#HA1". wp_pures. set (r := RecV f x _).
    rewrite -subst_map_binder_insert_2_empty. iApply "H".
    iApply (env_sem_typed_insert with "IH").
    iApply (env_sem_typed_insert with "[$]"). iApply env_sem_typed_empty.
  Qed.
255
256
257
258
259
260
261

  Lemma TLamV_sem_typed e C : ( A,   e : C A) -  (Λ: e) :  A, C A.
  Proof.
    iIntros "#H !#" (A) "/=". wp_pures.
    rewrite -{2}(subst_map_empty e). iApply ("H" $! A).
    by iApply env_sem_typed_empty.
  Qed.
262
End compatibility.