compatibility.v 9.23 KB
Newer Older
1
From tutorial_popl20 Require Export sem_typed sem_operators.
2

Amin Timany's avatar
Amin Timany committed
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
(** * Compatibility of logical relations with typing rules.

    Here 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.

    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]):

<<
       Γ ⊢ e1 : T1        Γ ⊢ e2 : T2
      --------------------------------
           Γ ⊢ (e1, e2) : T1 × T2
>>
    becomes

<<
      (Γ ⊨ e1 : T1) -∗ (Γ ⊨ e2 : T2) -∗ Γ ⊢ (e1, e2) : T1 × T2
>>
 *)

26
27
28
29
30
Section compatibility.
  Context `{heapG Σ}.
  Implicit Types A B : sem_ty Σ.
  Implicit Types C : sem_ty Σ  sem_ty Σ.

31
  Lemma Var_sem_typed Γ (x : string) A : Γ !! x = Some A  Γ  x : A.
32
33
34
35
36
37
  Proof.
    iIntros (HΓx vs) "!# #HΓ /=".
    iDestruct (env_sem_typed_lookup with "HΓ") as (v ->) "HA"; first done.
    by iApply wp_value.
  Qed.

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

44
  Lemma Pair_sem_typed Γ e1 e2 A1 A2 :
45
    Γ  e1 : A1 - Γ  e2 : A2 - Γ  (e1,e2) : A1 * A2.
46
47
48
49
50
51
  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.
52
  Lemma Fst_sem_typed Γ e A1 A2 : Γ  e : A1 * A2 - Γ  Fst e : A1.
53
54
55
56
57
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H [//])"); iIntros (w).
    iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures.
  Qed.
58
  Lemma Snd_sem_typed Γ e A1 A2 : Γ  e : A1 * A2 - Γ  Snd e : A2.
59
60
61
62
63
64
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H [//])"); iIntros (w).
    iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures.
  Qed.

65
  Lemma InjL_sem_typed Γ e A1 A2 : Γ  e : A1 - Γ  InjL e : A1 + A2.
66
67
68
69
70
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HA".
    wp_pures. iLeft. iExists w. auto.
  Qed.
71
  Lemma InjR_sem_typed Γ e A1 A2 : Γ  e : A2 - Γ  InjR e : A1 + A2.
72
73
74
75
76
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HA".
    wp_pures. iRight. iExists w. auto.
  Qed.
77
  Lemma Case_sem_typed Γ e e1 e2 A1 A2 B :
78
    Γ  e : A1 + A2 - Γ  e1 : (A1  B) - Γ  e2 : (A2  B) -
79
80
81
82
83
84
85
86
87
88
    Γ  Case e e1 e2 : B.
  Proof.
    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.

89
  Lemma Rec_sem_typed Γ f x e A1 A2 :
90
91
    binder_insert f (A1  A2)%sem_ty (binder_insert x A1 Γ)  e : A2 -
    Γ  (rec: f x := e) : (A1  A2).
92
93
94
  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
95
96
    rewrite -subst_map_binder_insert_2. iApply "H".
    iApply (env_sem_typed_insert with "IH"). by iApply env_sem_typed_insert.
97
98
  Qed.

99
  Lemma App_sem_typed Γ e1 e2 A1 A2 :
100
    Γ  e1 : (A1  A2) - Γ  e2 : A1 - Γ  e1 e2 : A2.
101
102
103
104
105
106
  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.

107
  Lemma TLam_sem_typed Γ e C : ( A, Γ  e : C A) - Γ  (Λ: e) :  A, C A.
108
109
110
111
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=". wp_pures.
    iIntros "!#" (A) "/=". wp_pures. by iApply ("H" $! A).
  Qed.
112
  Lemma TApp_sem_typed Γ e C A : (Γ  e :  A, C A) - Γ  e <_> : C A.
113
114
115
116
117
  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
118
  Lemma Pack_sem_typed Γ e C A : Γ  e : C A - Γ  (pack: e) :  A, C A.
119
120
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=".
Robbert Krebbers's avatar
Robbert Krebbers committed
121
122
    wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB".
    wp_lam. by iExists A.
123
  Qed.
124
  Lemma Unpack_sem_typed Γ x e1 e2 C B :
125
126
127
128
129
130
131
132
133
134
135
    (Γ  e1 :  A, C A) - ( A, binder_insert x (C A) Γ  e2 : B) -
    Γ  (unpack: x := e1 in e2) : B.
  Proof.
    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.

136
  Lemma Alloc_sem_typed Γ e A : Γ  e : A - Γ  ref e : ref A.
137
138
139
140
141
142
143
144
  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.
145
  Lemma Load_sem_typed Γ e A : Γ  e : ref A - Γ  ! e : A.
146
147
148
149
150
151
  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.
152
  Lemma Store_sem_typed Γ e1 e2 A :
153
    Γ  e1 : ref A - Γ  e2 : A - Γ  (e1 <- e2) : ().
154
155
156
157
158
159
  Proof.
    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.
160
  Lemma FAA_sem_typed Γ e1 e2 :
161
    Γ  e1 : ref sem_ty_int - Γ  e2 : sem_ty_int - Γ  FAA e1 e2 : sem_ty_int.
162
163
164
165
166
167
168
  Proof.
    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.
169
  Lemma CmpXchg_sem_typed Γ A e1 e2 e3 :
170
    SemTyUnboxed A 
171
172
    Γ  e1 : ref A - Γ  e2 : A - Γ  e3 : A -
    Γ  CmpXchg e1 e2 e3 : A * sem_ty_bool.
173
174
175
176
177
178
179
180
181
182
  Proof.
    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.

183
  Lemma UnOp_sem_typed Γ e op A B :
184
    SemTyUnOp op A B  Γ  e : A - Γ  UnOp op e : B.
185
186
187
188
189
  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.
190
  Lemma BinOp_sem_typed Γ e1 e2 op A1 A2 B :
191
    SemTyBinOp op A1 A2 B  Γ  e1 : A1 - Γ  e2 : A2 - Γ  BinOp op e1 e2 : B.
192
193
194
195
196
197
198
  Proof.
    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.

199
  Lemma If_sem_typed Γ e e1 e2 B :
200
    Γ  e : sem_ty_bool - Γ  e1 : B - Γ  e2 : B -
201
202
203
204
205
206
207
    Γ  (if: e then e1 else e2) : B.
  Proof.
    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.

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

  Lemma UnitV_sem_typed :  #() : ().
  Proof. by iPureIntro. Qed.
  Lemma BoolV_sem_typed (b : bool) :  #b : sem_ty_bool.
  Proof. by iExists b. Qed.
  Lemma IntV_sem_typed (n : Z) :  #n : sem_ty_int.
  Proof. by iExists n. Qed.

  Lemma PairV_sem_typed v1 v2 τ1 τ2 :
222
     v1 : τ1 -  v2 : τ2 -
223
224
225
     PairV v1 v2 : (τ1 * τ2).
  Proof. iIntros "#H1 #H2". iExists v1, v2. auto. Qed.
  Lemma InjLV_sem_typed v τ1 τ2 :
226
     v : τ1 -
227
228
229
     InjLV v : (τ1 + τ2).
  Proof. iIntros "H". iLeft. auto. Qed.
  Lemma InjRV_sem_typed v τ1 τ2 :
230
     v : τ2 -
231
232
233
234
     InjRV v : (τ1 + τ2).
  Proof. iIntros "H". iRight. auto. Qed.

  Lemma RecV_sem_typed f x e A B :
235
    binder_insert f (A  B)%sem_ty (binder_insert x A )  e : B -
236
237
238
239
240
241
242
243
     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.
244
End compatibility.