compatibility.v 7.44 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From exercises Require Export sem_typed sem_operators.
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

(** * Compatibility lemmas *)
(** 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 : τ1        Γ ⊢ e2 : τ2
  --------------------------------
       Γ ⊢ (e1, e2) : τ1 × τ2
>>

becomes:

<<
  (Γ ⊨ e1 : A1) -∗ (Γ ⊨ e2 : A2) -∗ Γ ⊢ (e1, e2) : A1 * A2
>>
*)

Section compatibility.
  Context `{!heapG Σ}.
  Implicit Types A B : sem_ty Σ.
  Implicit Types C : sem_ty Σ  sem_ty Σ.

  (** * Compatibility rules for expression typing *)
  (** * Variables *)
32
  Lemma Var_sem_typed Γ (x : string) A : Γ !! x = Some A   Γ  x : A.
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
  Proof.
    iIntros (HΓx vs) "!# #HΓ /=".
    iDestruct (env_sem_typed_lookup with "HΓ") as (v ->) "HA"; first done.
    by iApply wp_value.
  Qed.

  Lemma Val_sem_typed Γ v A :  v : A - Γ  v : A.
  Proof.
    iIntros "#Hv" (vs) "!# #HΓ /=".
    iApply wp_value. iApply "Hv".
  Qed.

  (** * Products and sums *)
  Lemma Pair_sem_typed Γ e1 e2 A1 A2 :
    Γ  e1 : A1 - Γ  e2 : A2 - Γ  (e1,e2) : A1 * A2.
  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.
  Lemma Fst_sem_typed Γ e A1 A2 : Γ  e : A1 * A2 - Γ  Fst e : A1.
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H [//])"); iIntros (w).
    iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures.
  Qed.
  Lemma Snd_sem_typed Γ e A1 A2 : Γ  e : A1 * A2 - Γ  Snd e : A2.
Robbert Krebbers's avatar
Robbert Krebbers committed
61
  Proof. (* FILL IN YOUR PROOF *) Admitted.
62
63

  Lemma InjL_sem_typed Γ e A1 A2 : Γ  e : A1 - Γ  InjL e : A1 + A2.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
66
  Proof. (* FILL IN YOUR PROOF *) Admitted.
  Lemma InjR_sem_typed Γ e A1 A2 : Γ  e : A2 - Γ  InjR e : A1 + A2.
  Proof. (* FILL IN YOUR PROOF *) Admitted.
67
68
69
  Lemma Case_sem_typed Γ e e1 e2 A1 A2 B :
    Γ  e : A1 + A2 - Γ  e1 : (A1  B) - Γ  e2 : (A2  B) -
    Γ  Case e e1 e2 : B.
Robbert Krebbers's avatar
Robbert Krebbers committed
70
  Proof. (* FILL IN YOUR PROOF *) Admitted.
71
72
73
74

  (** * Functions *)
  Lemma Rec_sem_typed Γ f x e A1 A2 :
    binder_insert f (A1  A2)%sem_ty (binder_insert x A1 Γ)  e : A2 -
Robbert Krebbers's avatar
Robbert Krebbers committed
75
    Γ  (rec: f x := e) : (A1  A2).
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
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=". wp_pures. iLöb as "IH".
    iIntros "!#" (v) "#HA1". wp_pures. set (r := RecV f x _).
    rewrite -subst_map_binder_insert_2. iApply "H".
    iApply (env_sem_typed_insert with "IH"). by iApply env_sem_typed_insert.
  Qed.

  Lemma App_sem_typed Γ e1 e2 A1 A2 :
    Γ  e1 : (A1  A2) - Γ  e2 : A1 - Γ  e1 e2 : A2.
  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.

  (** * Polymorphic functions and existentials *)
  Lemma TLam_sem_typed Γ e C : ( A, Γ  e : C A) - Γ  (Λ: e) :  A, C A.
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=". wp_pures.
    iIntros "!#" (A) "/=". wp_pures. by iApply ("H" $! A).
  Qed.
  Lemma TApp_sem_typed Γ e C A : (Γ  e :  A, C A) - Γ  e <_> : C A.
  Proof.
    iIntros "#H" (vs) "!# #HΓ /=".
    wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB". by iApply ("HB" $! A).
  Qed.

  Lemma Pack_sem_typed Γ e C A : Γ  e : C A - Γ  (pack: e) :  A, C A.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
  Proof. (* FILL IN YOUR PROOF *) Admitted.
105
106
107
  Lemma Unpack_sem_typed Γ x e1 e2 C B :
    (Γ  e1 :  A, C A) - ( A, binder_insert x (C A) Γ  e2 : B) -
    Γ  (unpack: x := e1 in e2) : B.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
  Proof. (* FILL IN YOUR PROOF *) Admitted.
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128

  (** ** Heap operations *)
  Lemma Alloc_sem_typed Γ e A : Γ  e : A - Γ  ref e : ref A.
  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.
  Lemma Load_sem_typed Γ e A : Γ  e : ref A - Γ  ! e : A.
  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.
  Lemma Store_sem_typed Γ e1 e2 A :
    Γ  e1 : ref A - Γ  e2 : A - Γ  (e1 <- e2) : ().
Robbert Krebbers's avatar
Robbert Krebbers committed
129
  Proof. (* FILL IN YOUR PROOF *) Admitted.
130
131
  Lemma FAA_sem_typed Γ e1 e2 :
    Γ  e1 : ref sem_ty_int - Γ  e2 : sem_ty_int - Γ  FAA e1 e2 : sem_ty_int.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
  Proof. (* FILL IN YOUR PROOF *) Admitted.
133
134
135
136
  Lemma CmpXchg_sem_typed Γ A e1 e2 e3 :
    SemTyUnboxed A 
    Γ  e1 : ref A - Γ  e2 : A - Γ  e3 : A -
    Γ  CmpXchg e1 e2 e3 : A * sem_ty_bool.
Robbert Krebbers's avatar
Robbert Krebbers committed
137
  Proof. (* FILL IN YOUR PROOF *) Admitted.
138
139
140
141
142
143
144
145
146
147
148

  (** ** Operators *)
  Lemma UnOp_sem_typed Γ e op A B :
    SemTyUnOp op A B  Γ  e : A - Γ  UnOp op e : B.
  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.
  Lemma BinOp_sem_typed Γ e1 e2 op A1 A2 B :
    SemTyBinOp op A1 A2 B  Γ  e1 : A1 - Γ  e2 : A2 - Γ  BinOp op e1 e2 : B.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
  Proof. (* FILL IN YOUR PROOF *) Admitted.
150
151
152
153

  Lemma If_sem_typed Γ e e1 e2 B :
    Γ  e : sem_ty_bool - Γ  e1 : B - Γ  e2 : B -
    Γ  (if: e then e1 else e2) : B.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
  Proof. (* FILL IN YOUR PROOF *) Admitted.
155
156
157

  (** ** Fork *)
  Lemma Fork_sem_typed Γ e : Γ  e : () - Γ  Fork e : ().
Robbert Krebbers's avatar
Robbert Krebbers committed
158
  Proof. (* FILL IN YOUR PROOF *) Admitted.
159
160
161

  (** * Compatibility rules for value typing *)
  (** ** Base types *)
162
  Lemma UnitV_sem_typed :   #() : ().
163
  Proof. by iPureIntro. Qed.
164
  Lemma BoolV_sem_typed (b : bool) :   #b : sem_ty_bool.
165
  Proof. by iExists b. Qed.
166
  Lemma IntV_sem_typed (n : Z) :   #n : sem_ty_int.
Robbert Krebbers's avatar
Robbert Krebbers committed
167
  Proof. (* FILL IN YOUR PROOF *) Admitted.
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

  (** ** Products and sums *)
  Lemma PairV_sem_typed v1 v2 τ1 τ2 :
     v1 : τ1 -  v2 : τ2 -
     PairV v1 v2 : (τ1 * τ2).
  Proof. iIntros "#H1 #H2". iExists v1, v2. auto. Qed.
  Lemma InjLV_sem_typed v τ1 τ2 :
     v : τ1 -
     InjLV v : (τ1 + τ2).
  Proof. iIntros "H". iLeft. auto. Qed.
  Lemma InjRV_sem_typed v τ1 τ2 :
     v : τ2 -
     InjRV v : (τ1 + τ2).
  Proof. iIntros "H". iRight. auto. Qed.

  (** ** Functions *)
  Lemma RecV_sem_typed f x e A B :
    binder_insert f (A  B)%sem_ty (binder_insert x A )  e : B -
     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.

  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.
End compatibility.