fundamental_binary.v 21.7 KB
Newer Older
1
2
From iris_logrel.logrel Require Export logrel_binary.
From iris_logrel.logrel.proofmode Require Export tactics_rel tactics_threadpool.
3

4
Section fundamental.
5
Context `{logrelG Σ}.
6
7
8
9
10
11
12
Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types e : expr.
Implicit Types Δ : listC D.
Hint Resolve to_of_val.

Section masked.
  Variable (E : coPset).
13

14
  Local Ltac value_case :=
15
    iApply (related_ret );
16
17
    iApply interp_ret; [solve_to_val..|];
    simpl; eauto.
18

19
20
21
22
23
24
25
26
27
  Local Ltac value_case' := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|]; repeat iModIntro.

  Local Tactic Notation "rel_bind_ap" uconstr(e1) uconstr(e2) constr(IH) ident(v) ident(w) constr(Hv):=
    rel_bind_l e1;
    rel_bind_r e2;
    iApply (related_bind with IH);
    iIntros ([v w]) Hv; simpl.

  (* Old tactic *)
28
  Local Tactic Notation "smart_bind" ident(j) uconstr(e) uconstr(e') constr(IH) ident(v) ident(w) constr(Hv):=
29
    try (iModIntro);
30
31
    wp_bind e;
    tp_bind j e';
32
    iSpecialize (IH with "Hs [HΓ] Hj"); eauto;
33
34
    iApply fupd_wp; iApply (fupd_mask_mono _); auto;
    iMod IH as IH; iModIntro;
35
    iApply (wp_wand with IH);
36
37
38
39
    iIntros (v);
    let vh := iFresh in
    iIntros vh;
    try (iMod vh);
Dan Frumin's avatar
Dan Frumin committed
40
    iDestruct vh as (w) (String.append "[Hj " (String.append Hv " ]")); simpl.
41

42
  Lemma bin_log_related_var Δ Γ x τ :
43
    Γ !! x = Some τ 
44
    {E,E;Δ;Γ}  Var x log Var x : τ.
45
  Proof.
46
    rewrite bin_log_related_eq.
47
    iIntros (? vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
48
49
50
51
52
53
54
    iDestruct (interp_env_Some_l with "HΓ") as ([v v']) "[Hvv' ?]"; first done.
    iDestruct "Hvv'" as %Hvv'.
    cbn-[env_subst].
    rewrite (env_subst_lookup (snd <$> vvs) x v'); last first.
    { rewrite lookup_fmap. by rewrite Hvv'. } 
    rewrite (env_subst_lookup _ x v); last first.
    { rewrite lookup_fmap. by rewrite Hvv'. } 
55
    iModIntro. value_case'; eauto.
56
57
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
58
  Lemma bin_log_related_unit Δ Γ : {E,E;Δ;Γ}  #() log #() : TUnit.
59
  Proof.
60
    value_case.
61
62
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
63
  Lemma bin_log_related_nat Δ Γ (n : nat) : {E,E;Δ;Γ}  # n log # n : TNat.
64
  Proof.
65
    value_case.
66
67
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
68
  Lemma bin_log_related_bool Δ Γ (b : bool) : {E,E;Δ;Γ}  # b log # b : TBool.
69
  Proof.
70
    value_case.
71
  Qed.
72

73
  Lemma bin_log_related_pair Δ Γ e1 e2 e1' e2' τ1 τ2 :
74
75
76
    {E,E;Δ;Γ}  e1 log e1' : τ1 -
    {E,E;Δ;Γ}  e2 log e2' : τ2 -
    {E,E;Δ;Γ}  Pair e1 e2 log Pair e1' e2' : TProd τ1 τ2.
77
  Proof.
78
79
80
    iIntros "IH1 IH2".
    rel_bind_ap e1 e1' "IH1" v1 v1' "Hvv1".
    rel_bind_ap e2 e2' "IH2" v2 v2' "Hvv2".
81
    value_case.
82
83
    iExists _, _; eauto.
    iSplit; simpl; eauto.  auto. 
84
85
  Qed.

86
  Lemma bin_log_related_fst Δ Γ e e' τ1 τ2 :
87
     logrelN  E 
88
89
    {E,E;Δ;Γ}  e log e' : TProd τ1 τ2 -
    {E,E;Δ;Γ}  Fst e log Fst e' : τ1.
90
  Proof.
91
    iIntros (?) "IH".
92
93
    rel_bind_ap e e' "IH" v w "IH".
    iDestruct "IH" as ([v1 v2] [w1 w2]) "[% [IHw IHw']]". simplify_eq/=.
94
95
96
    rel_proj_l.
    rel_proj_r.
    value_case.
97
98
  Qed.

99
  Lemma bin_log_related_snd Δ Γ e e' τ1 τ2 :
100
     logrelN  E 
101
102
    {E,E;Δ;Γ}  e log e' : TProd τ1 τ2 -
    {E,E;Δ;Γ}  Snd e log Snd e' : τ2.
103
  Proof.
104
    iIntros (?) "IH".
105
106
    rel_bind_ap e e' "IH" v w "IH".
    iDestruct "IH" as ([v1 v2] [w1 w2]) "[% [IHw IHw']]". simplify_eq/=.
107
108
109
    rel_proj_l.
    rel_proj_r.
    value_case.
110
111
  Qed.

112
113
114
115
  Lemma bin_log_related_app Δ Γ e1 e2 e1' e2' τ1 τ2 :
    {E,E;Δ;Γ}  e1 log e1' : TArrow τ1 τ2 -
    {E,E;Δ;Γ}  e2 log e2' : τ1 -
    {E,E;Δ;Γ}  App e1 e2 log App e1' e2' :  τ2.
116
117
  Proof.
    iIntros "IH1 IH2".
118
119
    rel_bind_ap e1 e1' "IH1" f f' "Hff".
    rel_bind_ap e2 e2' "IH2" v v' "Hvv".
120
121
    iSpecialize ("Hff" with "Hvv"). simpl.
    by iApply related_ret.
122
  Qed.
123

124
  Lemma bin_log_related_rec Δ (Γ : stringmap type) (f x : binder) (e e' : expr) τ1 τ2 :
125
126
    Closed (x :b: f :b: dom _ Γ) e 
    Closed (x :b: f :b: dom _ Γ) e' 
127
128
     ({E,E;Δ;<[x:=τ1]>(<[f:=TArrow τ1 τ2]>Γ)}  e log e' : τ2) -
    {E,E;Δ;Γ}  Rec f x e log Rec f x e' : TArrow τ1 τ2.
129
  Proof.
130
    rewrite bin_log_related_eq.
131
    iIntros (??) "#Ht".
132
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=". cbn.
133
    iDestruct (interp_env_dom with "HΓ") as %Hdom.
134
135
    (* TODO: how to get rid of/ simplify those proofs? *)
    assert (Closed (x :b: f :b: )
136
              (subst_p (delete f (delete x (fst <$> vvs))) e)).
137
138
139
140
141
142
    { eapply subst_p_closes; eauto.
      rewrite ?dom_delete_binder Hdom.
      rewrite dom_fmap.
      destruct x as [|x], f as [|f]; cbn-[union difference].
      + set_solver.
      + rewrite difference_empty.
143
        rewrite assoc. rewrite difference_union.
144
145
        set_solver.
      + rewrite difference_empty.
146
        rewrite assoc. rewrite difference_union.
147
148
149
        set_solver.
      + rewrite ?(right_id  union).
        rewrite (comm union {[x]} {[f]}) !assoc.
150
        rewrite difference_union.
151
        rewrite -!assoc (comm union {[f]} {[x]}) !assoc.
152
        rewrite difference_union.
153
        set_solver. }
154
    assert (Closed (x :b: f :b: )
155
              (subst_p (delete f (delete x (snd <$> vvs))) e')).
156
157
158
159
160
161
    { eapply subst_p_closes; eauto.
      rewrite ?dom_delete_binder Hdom.
      rewrite dom_fmap.
      destruct x as [|x], f as [|f]; cbn-[union difference].
      + set_solver.
      + rewrite difference_empty.
162
        rewrite assoc. rewrite difference_union.
163
164
        set_solver.
      + rewrite difference_empty.
165
        rewrite assoc. rewrite difference_union.
166
167
168
        set_solver.
      + rewrite ?(right_id  union).
        rewrite (comm union {[x]} {[f]}) !assoc.
169
        rewrite difference_union.
170
        rewrite -!assoc (comm union {[f]} {[x]}) !assoc.
171
        rewrite difference_union.
172
        set_solver.
173
    }
174
    iModIntro. value_case'; eauto.
175
    { rewrite decide_left; eauto. }
176
177
178
179
180
    iExists (RecV f x (subst_p (delete f (delete x (snd <$> vvs))) e')). iIntros "{$Hj} !#".
    iLöb as "IH". iIntros ([v v']) "#Hiv". simpl. iIntros (j' K') "Hj".
    iModIntro. simpl.
    iApply (wp_rec _ f x (subst_p _ e)); eauto 2 using to_of_val. iNext.
    iApply fupd_wp.
181
    tp_rec j'.
182
183
184
185
186
187
188
189
190
191
192
193
194
    pose (vvs':=(<[x:=(v,v')]>(<[f:=(RecV f x (subst_p (delete f (delete x (fst <$> vvs))) e), RecV f x (subst_p (delete f (delete x (snd <$> vvs))) e'))]>vvs))).
    iAssert (interp_env (<[x:=τ1]> (<[f:=TArrow τ1 τ2]> Γ))   Δ vvs') as "#HΓ'".
    { unfold vvs'. destruct f as [|f], x as [|x]; cbn; eauto;
      rewrite -?interp_env_cons -?Hdom; eauto. }
    iSpecialize ("Ht" with "Hs [HΓ']"); eauto.
    iSpecialize ("Ht" $! j' K').
    rewrite {2}/vvs' /env_subst.
    rewrite !fmap_insert' /=.
    rewrite subst_p_insert.
    rewrite !subst_p_insert /=.
    unfold env_subst in *.
    erewrite !subst_p_delete; auto. (* TODO: [auto] solve the [Closed] goal, but [solve_closed] does not *)
    rewrite !(delete_commute_binder _ x f).
195
    iApply (fupd_mask_mono E); auto.
196
    iApply ("Ht" with "Hj").
197
198
  Qed.

199
  Lemma bin_log_related_injl Δ Γ e e' τ1 τ2 :
200
     logrelN  E 
201
202
    {E,E;Δ;Γ}  e log e' : τ1 -
    {E,E;Δ;Γ}  InjL e log InjL e' : (TSum τ1 τ2).
203
  Proof.
204
    iIntros (?) "IH".
205
    rel_bind_ap e e' "IH" v v' "Hvv".
206
    value_case.
207
    iLeft. iExists (_,_); eauto.
208
  Qed.
209

210
  Lemma bin_log_related_injr Δ Γ e e' τ1 τ2 :
211
     logrelN  E 
212
213
    {E,E;Δ;Γ}  e log e' : τ2 -
    {E,E;Δ;Γ}  InjR e log InjR e' : TSum τ1 τ2.
214
  Proof.
215
    iIntros (?) "IH".
216
    rel_bind_ap e e' "IH" v v' "Hvv".
217
    value_case.
218
    iRight. iExists (_,_); eauto.
219
220
  Qed.

221
  Lemma bin_log_related_case Δ Γ e0 e1 e2 e0' e1' e2' τ1 τ2 τ3 :
222
     logrelN  E 
223
224
    {E,E;Δ;Γ}  e0 log e0' : TSum τ1 τ2 -
    {E,E;Δ;Γ}  e1 log e1' : TArrow τ1 τ3 -
225
    {E,E;Δ;Γ}  e2 log e2' : TArrow τ2 τ3 -
226
    {E,E;Δ;Γ}  Case e0 e1 e2 log Case e0' e1' e2' : τ3.
227
  Proof.
228
    iIntros (?) "IH1 IH2 IH3".
229
    rel_bind_ap e0 e0' "IH1" v0 v0' "IH1".
230
    iDestruct "IH1" as "[Hiv|Hiv]";
231
    iDestruct "Hiv" as ([w w']) "[% #Hw]"; simplify_eq/=;
232
233
234
235
236
      rel_case_l; rel_case_r.
    - iApply (bin_log_related_app with "IH2").
      value_case.
    - iApply (bin_log_related_app with "IH3").
      value_case.
237
238
  Qed.

239
  Lemma bin_log_related_if Δ Γ e0 e1 e2 e0' e1' e2' τ :
240
     logrelN  E 
241
242
    {E,E;Δ;Γ}  e0 log e0' : TBool -
    {E,E;Δ;Γ}  e1 log e1' : τ -
243
    {E,E;Δ;Γ}  e2 log e2' : τ -
244
    {E,E;Δ;Γ}  If e0 e1 e2 log If e0' e1' e2' : τ.
245
  Proof.
246
    iIntros (?) "IH1 IH2 IH3".
247
    rel_bind_ap e0 e0' "IH1" v0 v0' "IH1".
248
    iDestruct "IH1" as ([]) "[% %]"; simplify_eq/=;
249
      rel_if_l; rel_if_r; iAssumption.
250
251
  Qed.

Dan Frumin's avatar
Dan Frumin committed
252
  Lemma bin_log_related_nat_binop Δ Γ op e1 e2 e1' e2' τ :
253
     logrelN  E 
Dan Frumin's avatar
Dan Frumin committed
254
    binop_nat_res_type op = Some τ 
255
256
    {E,E;Δ;Γ}  e1 log e1' : TNat -
    {E,E;Δ;Γ}  e2 log e2' : TNat -
Dan Frumin's avatar
Dan Frumin committed
257
    {E,E;Δ;Γ}  BinOp op e1 e2 log BinOp op e1' e2' : τ.
258
  Proof.
Dan Frumin's avatar
Dan Frumin committed
259
    iIntros (? Hopτ) "IH1 IH2".
260
261
    rel_bind_ap e1 e1' "IH1" v1 v1' "IH1".
    rel_bind_ap e2 e2' "IH2" v2 v2' "IH2".
262
263
    iDestruct "IH1" as (n) "[% %]"; simplify_eq/=.
    iDestruct "IH2" as (n') "[% %]"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
264
    destruct (binop_nat_typed_safe op n n' _ Hopτ) as [v' Hopv'].
265
266
267
    rel_op_l; eauto.
    rel_op_r; eauto.
    value_case.
Dan Frumin's avatar
Dan Frumin committed
268
269
270
271
272
    destruct op; simpl in Hopv'; simplify_eq/=; try destruct eq_nat_dec; try destruct le_dec;
      try destruct lt_dec; eauto.
  Qed.

  Lemma bin_log_related_bool_binop Δ Γ op e1 e2 e1' e2' τ :
273
     logrelN  E 
Dan Frumin's avatar
Dan Frumin committed
274
275
276
277
278
279
    binop_bool_res_type op = Some τ 
    {E,E;Δ;Γ}  e1 log e1' : TBool -
    {E,E;Δ;Γ}  e2 log e2' : TBool -
    {E,E;Δ;Γ}  BinOp op e1 e2 log BinOp op e1' e2' : τ.
  Proof.
    iIntros (? Hopτ) "IH1 IH2".
280
281
    rel_bind_ap e1 e1' "IH1" v1 v1' "IH1".
    rel_bind_ap e2 e2' "IH2" v2 v2' "IH2".
Dan Frumin's avatar
Dan Frumin committed
282
283
284
    iDestruct "IH1" as (n) "[% %]"; simplify_eq/=.
    iDestruct "IH2" as (n') "[% %]"; simplify_eq/=.
    destruct (binop_bool_typed_safe op n n' _ Hopτ) as [v' Hopv'].
285
286
287
    rel_op_l; eauto.
    rel_op_r; eauto.
    value_case.
288
    destruct op; simpl in Hopv'; simplify_eq/=; eauto.
289
  Qed.
290

291
  Lemma bin_log_related_tlam Δ Γ e e' τ :
292
293
    Closed (dom _ Γ) e 
    Closed (dom _ Γ) e' 
294
     logrelN  E 
295
296
    ( (τi : D), ⌜∀ ww, PersistentP (τi ww)   ({E,E;(τi::Δ);Autosubst_Classes.subst (ren (+1)) <$> Γ}  e log e' : τ)) -
    {E,E;Δ;Γ}  TLam e log TLam e' : TForall τ.
297
  Proof.
298
    rewrite bin_log_related_eq.
299
    iIntros (???) "#IH".
300
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
301
302
303
304
305
    iDestruct (interp_env_dom with "HΓ") as %Hdom.
    assert (Closed  (env_subst (fst <$> vvs) e)).
    { eapply subst_p_closes; eauto. rewrite dom_fmap Hdom. rewrite right_id. reflexivity. }
    assert (Closed  (env_subst (snd <$> vvs) e')).
    { eapply subst_p_closes; eauto. rewrite dom_fmap Hdom. rewrite right_id. reflexivity. }
306
    value_case'. rewrite decide_left; eauto.
307
308
309
310
311
    iExists (TLamV (env_subst (snd <$> vvs) e')). cbn.
    iFrame "Hj". iAlways.
    iIntros (τi ? j' K') "Hv /=".
    iApply wp_tlam; eauto. iModIntro; iNext; iApply fupd_wp.
    tp_tlam j'; eauto.
312
313
    iSpecialize ("IH" $! τi with "[] Hs [HΓ]"); auto.
    { by rewrite interp_env_ren. }
314
315
    iSpecialize ("IH" with "Hv").
    iApply (fupd_mask_mono E); eauto.
316
  Qed.
317

318
319
320
  Lemma bin_log_related_tapp' Δ Γ e e' τ τ' :
    {E,E;Δ;Γ}  e log e' : TForall τ -
    {E,E;Δ;Γ}  TApp e log TApp e' : τ.[τ'/].
321
  Proof.
322
    iIntros "IH".
323
    rel_bind_ap e e' "IH" v v' "IH".
324
    iSpecialize ("IH" $! (interp   τ' Δ) with "[#]"); [iPureIntro; apply _|].
325
326
    iApply (related_ret ).
    iApply (interp_expr_subst Δ τ τ' (TApp v, TApp v')  with "IH").
327
328
  Qed.

329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
  Lemma bin_log_related_tapp (τi : D) Δ Γ e e' τ :
    ( ww, PersistentP (τi ww)) 
    {E,E;Δ;Γ}  e log e' : TForall τ -
    {E,E;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$> Γ}  TApp e log TApp e' : τ.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (?) "IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    wp_bind (env_subst _ e).
    tp_bind j (env_subst _ e').
    iSpecialize ("IH" with "Hs [HΓ] Hj").
    { by rewrite interp_env_ren. }
    iMod "IH" as "IH /=". iModIntro.
    iApply (wp_wand with "IH").
    iIntros (v). iDestruct 1 as (v') "[Hj #IH]".
    iSpecialize ("IH" $! τi with "[]"); auto.
    unfold interp_expr.
    iMod ("IH" with "Hj") as "IH /=".
    done.
  Qed.

  Lemma bin_log_related_fold Δ Γ e e' τ :
    {E,E;Δ;Γ}  e log e' : τ.[(TRec τ)/] -
    {E,E;Δ;Γ}  Fold e log Fold e' : TRec τ.
353
  Proof.
354
    iIntros "IH".
355
356
    rel_bind_ap e e' "IH" v v' "IH".
    value_case.
357
    rewrite fixpoint_unfold /= -interp_subst.
358
    iExists (_, _); eauto.
359
360
  Qed.

361
  Lemma bin_log_related_unfold Δ Γ e e' τ :
362
     logrelN  E 
363
364
    {E,E;Δ;Γ}  e log e' : TRec τ -
    {E,E;Δ;Γ}  Unfold e log Unfold e' : τ.[(TRec τ)/].
365
  Proof.
366
    iIntros (?) "IH".
367
    rel_bind_ap e e' "IH" v v' "IH".
368
    rewrite /= fixpoint_unfold /=.
369
    change (fixpoint _) with (interp   (TRec τ) Δ).
370
    iDestruct "IH" as ([w w']) "#[% Hiz]"; simplify_eq/=.
371
372
373
    rel_unfold_l.
    rel_unfold_r.
    value_case. by rewrite -interp_subst.
374
375
  Qed.

376
377
378
  Lemma bin_log_related_pack' Δ Γ e e' τ τ' :
    {E,E;Δ;Γ}  e log e' : τ.[τ'/] -
    {E,E;Δ;Γ}  Pack e log Pack e' : TExists τ.
379
  Proof.
380
    iIntros "IH".
381
382
    rel_bind_ap e e' "IH" v v' "#IH".
    value_case.
383
    iExists (v, v'). simpl; iSplit; eauto.
Dan Frumin's avatar
Dan Frumin committed
384
    iExists ( τ'  Δ).
385
    iSplit; eauto. iPureIntro. apply _.
386
    by rewrite interp_subst.
387
388
  Qed.

389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
  Lemma bin_log_related_pack (τi : D) Δ Γ e e' τ :
    ( ww, PersistentP (τi ww)) 
    {E,E;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$> Γ}  e log e' : τ -
    {E,E;Δ;Γ}  Pack e log Pack e' : TExists τ.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (?) "IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    wp_bind (env_subst _ e).
    tp_bind j (env_subst _ e').
    iSpecialize ("IH" with "Hs [HΓ] Hj").
    { by rewrite interp_env_ren. }
    iMod "IH" as "IH /=". iModIntro.
    iApply (wp_wand with "IH").
    iIntros (v). iDestruct 1 as (v') "[Hj #IH]".
404
    value_case'.
405
406
407
408
409
    iExists (PackV v'). simpl. iFrame.
    iExists (v, v'). simpl; iSplit; eauto.
  Qed.

  Lemma bin_log_related_unpack Δ Γ e1 e1' e2 e2' τ τ2
410
    (Hmasked :  logrelN  E) :
411
    {E,E;Δ;Γ}  e1 log e1' : TExists τ -
Robbert Krebbers's avatar
Robbert Krebbers committed
412
413
414
    ( τi : D, ⌜∀ ww, PersistentP (τi ww) 
      {E,E;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$> Γ} 
        e2 log e2' : TArrow τ (Autosubst_Classes.subst (ren (+1)) τ2)) -
415
    {E,E;Δ;Γ}  Unpack e1 e2 log Unpack e1' e2' : τ2.
416
  Proof.
417
    rewrite bin_log_related_eq.
418
    iIntros "IH1 IH2".
419
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
420
    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
421
    iDestruct "IH1" as ([w w']) "[% #Hτi]"; simplify_eq/=.
422
    iDestruct "Hτi" as (τi) "[% #Hτi]"; simplify_eq/=.
423
    iApply wp_pack; eauto. iNext.
424
    iApply fupd_wp.
425
    tp_pack j; eauto. iModIntro.
426
427
    iSpecialize ("IH2" $! τi with "[] Hs [HΓ]"); auto.
    { by rewrite interp_env_ren. }
428
429
430
431
432
433
434
    tp_bind j (env_subst (snd <$> vvs) e2').
    iApply fupd_wp. iApply (fupd_mask_mono E); eauto.
    iMod ("IH2" with "Hj") as "IH2". simpl.
    wp_bind (env_subst (fst <$> vvs) e2).
    iApply (wp_wand with "IH2"). iModIntro.
    iIntros (v). iDestruct 1 as (v') "[Hj #Hvv']".
    iSpecialize ("Hvv'" $! (w,w') with "Hτi Hj"). simpl.
435
    iMod "Hvv'".
436
    iApply (wp_wand with "Hvv'"). clear v v'.
437
    iIntros (v). iDestruct 1 as (v') "[Hj #Hvv']".
438
    rewrite (interp_weaken [] [τi] Δ _ _ τ2) /=.
439
    eauto.
440
  Qed.
441

442
  Lemma bin_log_related_fork Δ Γ e e' :
443
     logrelN  E 
444
445
    {E,E;Δ;Γ}  e log e' : TUnit -
    {E,E;Δ;Γ}  Fork e log Fork e' : TUnit.
446
  Proof.
447
    rewrite bin_log_related_eq.
448
    iIntros (?) "IH".
449
    iIntros (vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
450
451
    tp_fork j as i "Hi". fold subst_p.  iModIntro.
    iApply wp_fork. fold subst_p. iNext. iSplitL "Hj".
Robbert Krebbers's avatar
Robbert Krebbers committed
452
    - iExists #(); eauto.
453
    - iSpecialize ("IH" with "Hs HΓ").
454
      iSpecialize ("IH" $! i []). simpl.
455
456
      iSpecialize ("IH" with "Hi").
      iApply fupd_wp. iApply (fupd_mask_mono E); eauto.
457
      iMod "IH". iApply (wp_wand with "IH"). eauto.
458
459
  Qed.

460
  Lemma bin_log_related_alloc Δ Γ e e' τ :
461
     logrelN  E 
462
463
    {E,E;Δ;Γ}  e log e' : τ -
    {E,E;Δ;Γ}  Alloc e log Alloc e' : Tref τ.
464
  Proof.
465
    iIntros (?) "IH".
466
    rel_bind_ap e e' "IH" v v' "IH".
467
468
    rel_alloc_l as l "Hl".
    rel_alloc_r as k "Hk".
469
    iMod (inv_alloc (logN .@ (l,k)) _ ( w : val * val,
470
      l ↦ᵢ w.1  k ↦ₛ w.2  interp _ _ τ Δ w)%I with "[Hl Hk IH]") as "HN"; eauto.
471
    { iNext. iExists (v, v'); simpl; iFrame. }
472
473
    rel_vals.
    iExists (l, k). eauto.
474
475
  Qed.

476
  Lemma bin_log_related_load Δ Γ e e' τ :
477
    logrelN   E 
478
479
    {E,E;Δ;Γ}  e log e' : (Tref τ) -
    {E,E;Δ;Γ}  Load e log Load e' : τ.
480
  Proof.
481
    iIntros (?) "IH".
482
483
    rel_bind_ap e e' "IH" v v' "IH".
    iDestruct "IH" as ([l l']) "[% Hinv]"; simplify_eq/=.
484
    rel_load_l_atomic.
Dan Frumin's avatar
Dan Frumin committed
485
    iInv (logN .@ (l,l')) as ([w w']) "[Hw1 [>Hw2 #Hw]]" "Hclose"; simpl.
486
    iModIntro. iExists _; iFrame "Hw1".
Dan Frumin's avatar
Dan Frumin committed
487
    iNext. iIntros "Hw1".
488
    rel_load_r.
Dan Frumin's avatar
Dan Frumin committed
489
    iMod ("Hclose" with "[Hw1 Hw2]").
Robbert Krebbers's avatar
Robbert Krebbers committed
490
    { iNext. iExists (w,w'); by iFrame. }
491
    rel_vals; eauto.
492
493
  Qed.

494
  Lemma bin_log_related_store Δ Γ e1 e2 e1' e2' τ :
495
    logrelN   E 
496
497
498
    {E,E;Δ;Γ}  e1 log e1' : (Tref τ) -
    {E,E;Δ;Γ}  e2 log e2' : τ -
    {E,E;Δ;Γ}  Store e1 e2 log Store e1' e2' : TUnit.
499
  Proof.
500
    iIntros (?) "IH1 IH2".
501
502
503
    rel_bind_ap e1 e1' "IH1" v v' "IH1".
    iDestruct "IH1" as ([l l']) "[% Hinv]"; simplify_eq/=.
    rel_bind_ap e2 e2' "IH2" w w' "IH2".
504
    rel_store_l_atomic.
Dan Frumin's avatar
Dan Frumin committed
505
    iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
506
507
508
509
    iModIntro. iExists _; iFrame "Hv1".
    iNext. iIntros "Hw1".
    rel_store_r.
    iMod ("Hclose" with "[Hw1 Hv2 IH2]").
510
    { iNext; iExists (_, _); simpl; iFrame. }
511
    by rel_vals.
512
513
  Qed.

514
  Lemma bin_log_related_CAS Δ Γ e1 e2 e3 e1' e2' e3' τ
515
    (HEqτ : EqType τ) :
516
    logrelN   E 
517
518
519
520
    {E,E;Δ;Γ}  e1 log e1' : Tref τ -
    {E,E;Δ;Γ}  e2 log e2' : τ -
    {E,E;Δ;Γ}  e3 log e3' : τ -
    {E,E;Δ;Γ}  CAS e1 e2 e3 log CAS e1' e2' e3' : TBool.
521
  Proof.
522
    iIntros (?) "IH1 IH2 IH3".
523
524
525
    rel_bind_ap e1 e1' "IH1" v1 v1' "#IH1".
    rel_bind_ap e2 e2' "IH2" v2 v2' "#IH2".
    rel_bind_ap e3 e3' "IH3" v3 v3' "#IH3".
526
    iDestruct "IH1" as ([l l']) "[% Hinv]"; simplify_eq/=.
527
    rel_cas_l_atomic.
Dan Frumin's avatar
Dan Frumin committed
528
    iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
529
    iPoseProof ("Hv") as "Hv' /=".
530
    rewrite {2}[interp _ _ τ Δ (v, v')]interp_EqType_agree; trivial.
531
    iMod "Hv'" as %Hv'; subst.
532
533
534
535
536
537
538
539
540
541
    iModIntro. iExists _; iFrame. simpl.
    destruct (decide (v' = v2)) as [|Hneq]; subst.
    - iSplitR; first by (iIntros (?); contradiction).
      iIntros (?). iNext. iIntros "Hv1".
      iApply fupd_logrel'.
      iAssert ( v2 = v2'⌝)%I with "[IH2]" as ">%".
      { rewrite ?interp_EqType_agree; trivial. }
      iModIntro.
      rel_cas_suc_r.
      iMod ("Hclose" with "[-]").
Robbert Krebbers's avatar
Robbert Krebbers committed
542
      { iNext; iExists (_, _); by iFrame. }
543
544
545
546
547
      rel_vals; eauto.
    - iSplitL; last by (iIntros (?); congruence).
      iIntros (?). iNext. iIntros "Hv1".
      iApply fupd_logrel'.
      iAssert ( v'  v2'⌝)%I as ">%".
Dan Frumin's avatar
Dan Frumin committed
548
      { rewrite ?interp_EqType_agree; trivial. iSimplifyEq. auto. }
549
550
551
      iModIntro.
      rel_cas_fail_r.
      iMod ("Hclose" with "[-]").
Robbert Krebbers's avatar
Robbert Krebbers committed
552
      { iNext; iExists (_, _); by iFrame. }
553
      rel_vals; eauto.
554
555
  Qed.

556
  Theorem binary_fundamental_masked Δ Γ e τ :
557
    logrelN  E 
558
    Γ ⊢ₜ e : τ  ({E,E;Δ;Γ}  e log e : τ)%I.
559
  Proof.
560
    intros HlogN Ht. iInduction Ht as [] "IH" forall (Δ).
561
562
563
564
565
    - by iApply bin_log_related_var.
    - iApply bin_log_related_unit.
    - by iApply bin_log_related_nat.
    - by iApply bin_log_related_bool.
    - by iApply (bin_log_related_nat_binop with "[]").
Dan Frumin's avatar
Dan Frumin committed
566
    - by iApply (bin_log_related_bool_binop with "[]").
567
568
569
570
571
    - by iApply (bin_log_related_pair with "[]").
    - by iApply bin_log_related_fst.
    - by iApply bin_log_related_snd.
    - by iApply bin_log_related_injl.
    - by iApply bin_log_related_injr.
572
    - by iApply (bin_log_related_case with "[] []").
573
    - by iApply (bin_log_related_if with "[] []").
574
575
576
    - assert (Closed (x :b: f :b: dom (gset string) Γ) e).
      { apply typed_X_closed in Ht.
        rewrite !dom_insert_binder in Ht.
577
        revert Ht. destruct x,f; cbn-[union];
578
579
580
581
        (* TODO: why is simple rewriting is not sufficient here? *)
        erewrite ?(left_id ); eauto.
        all: apply _. }
      iApply (bin_log_related_rec with "[]"); eauto.
582
    - by iApply (bin_log_related_app with "[] []").
583
    - assert (Closed (dom _ Γ) e).
584
585
      { apply typed_X_closed in Ht.
        pose (K:=(dom_fmap (Autosubst_Classes.subst (ren (+1))) Γ)).
586
587
        fold_leibniz. by rewrite -K. }
      iApply bin_log_related_tlam; eauto.
588
    - by iApply bin_log_related_tapp'.
589
590
    - by iApply bin_log_related_fold.
    - by iApply bin_log_related_unfold.
591
592
    - by iApply bin_log_related_pack'.
    - iApply (bin_log_related_unpack with "[]"); eauto.
593
594
595
596
597
    - by iApply bin_log_related_fork.
    - by iApply bin_log_related_alloc.
    - by iApply bin_log_related_load.
    - by iApply (bin_log_related_store with "[]").
    - by iApply (bin_log_related_CAS with "[] []").
598
  Qed.
599
600
End masked.

Dan Frumin's avatar
Dan Frumin committed
601
602
Theorem binary_fundamental Δ Γ e τ :
  Γ ⊢ₜ e : τ  ({,;Δ;Γ}  e log e : τ)%I.
603
604
Proof. by eapply binary_fundamental_masked. Qed.

605
End fundamental.