fundamental_binary.v 25 KB
Newer Older
1
From iris_logrel.F_mu_ref_conc Require Export logrel_binary.
2
From iris.proofmode Require Import tactics.
3
From iris_logrel.F_mu_ref_conc Require Import lang rules_binary tactics.
4
From iris.base_logic Require Export big_op.
5
From iris.program_logic Require Import ectx_lifting.
6

7
Section fundamental.
8
Context `{logrelG Σ}.
9 10 11 12 13 14 15
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).
16

17
  Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|]; repeat iModIntro.
18

19
  Local Tactic Notation "smart_bind" ident(j) uconstr(e) uconstr(e') constr(IH) ident(v) ident(w) constr(Hv):=
20
    try (iModIntro);
21 22
    wp_bind e;
    tp_bind j e';
23
    iSpecialize (IH with "Hs [HΓ] Hj"); eauto;
24 25
    iApply fupd_wp; iApply (fupd_mask_mono _); auto;
    iMod IH as IH; iModIntro;
26
    iApply (wp_wand with IH);
27 28 29 30
    iIntros (v);
    let vh := iFresh in
    iIntros vh;
    try (iMod vh);
Dan Frumin's avatar
Dan Frumin committed
31
    iDestruct vh as (w) (String.append "[Hj " (String.append Hv " ]")); simpl.
32

33
  Lemma bin_log_related_var Δ Γ x τ :
34
    Γ !! x = Some τ 
35
    {E,E;Δ;Γ}  Var x log Var x : τ.
36
  Proof.
37
    rewrite bin_log_related_eq.
38
    iIntros (? vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
39 40 41 42 43 44 45
    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'. } 
46
    iModIntro. value_case; eauto.
47 48
  Qed.

49
  Lemma bin_log_related_unit Δ Γ : {E,E;Δ;Γ}  Unit log Unit : TUnit.
50
  Proof.
51
    rewrite bin_log_related_eq.
52
    iIntros (vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
53 54
    value_case. 
    iExists UnitV; eauto.
55 56
  Qed.

57
  Lemma bin_log_related_nat Δ Γ n : {E,E;Δ;Γ}  #n n log #n n : TNat.
58
  Proof.
59
    rewrite bin_log_related_eq.
60
    iIntros (vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
61 62
    value_case.
    iExists (#nv _); eauto.
63 64
  Qed.

65
  Lemma bin_log_related_bool Δ Γ b : {E,E;Δ;Γ}  # b log # b : TBool.
66
  Proof.
67
    rewrite bin_log_related_eq.
68
    iIntros (vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
69 70
    value_case.
    iExists (#v _); eauto.
71
  Qed.
72

73 74 75 76
  Lemma bin_log_related_pair Δ Γ e1 e2 e1' e2' τ1 τ2 :
      {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
    rewrite bin_log_related_eq.
79
    iIntros "IH1 IH2". iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
80 81 82 83
    cbn.
    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v1 w1 "IH1".
    smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" v2 w2 "IH2".
    value_case.
84 85 86
    iExists (PairV w1 w2); iFrame. 
    iExists _, _; eauto.
    iSplit; simpl; eauto.  auto. 
87 88
  Qed.

89
  Lemma bin_log_related_fst Δ Γ e e' τ1 τ2 :
90
     specN  E 
91 92
    {E,E;Δ;Γ}  e log e' : TProd τ1 τ2 -
    {E,E;Δ;Γ}  Fst e log Fst e' : τ1.
93
  Proof.
94
    rewrite bin_log_related_eq.
95
    iIntros (?) "IH".
96
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
97 98
    cbn.
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v w "IH".    
99
    iDestruct "IH" as ([v1 v2] [w1 w2]) "[% [IHw IHw']]".
100
    simplify_eq/=.
101 102
    iApply wp_fst; eauto. iNext.
    iExists v2.
103
    tp_fst j; eauto. 
104 105
  Qed.

106
  Lemma bin_log_related_snd Δ Γ e e' τ1 τ2 :
107
     specN  E 
108 109
    {E,E;Δ;Γ}  e log e' : TProd τ1 τ2 -
    {E,E;Δ;Γ}  Snd e log Snd e' : τ2.
110
  Proof.
111
    rewrite bin_log_related_eq.
112
    iIntros (?) "IH".
113
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
114 115
    cbn.
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v w "IH".
116
    iDestruct "IH" as ([v1 v2] [w1 w2]) "[% [IHw IHw']]".
117
    simplify_eq.
118
    iApply wp_snd; eauto. iNext. 
119
    iExists w2.
120 121 122
    tp_snd j; eauto. 
  Qed.

123 124 125 126
  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.
127
  Proof.
128
    rewrite bin_log_related_eq.
129
    iIntros "IH1 IH2".
130
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
131 132 133 134 135
    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" f f' "#IH1".
    smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" v v' "IH2".
    iSpecialize ("IH1" with "IH2 Hj").    
    by iMod "IH1". 
  Qed.
Dan Frumin's avatar
Dan Frumin committed
136
    
137
  Lemma bin_log_related_rec Δ (Γ : stringmap type) (f x : binder) (e e' : expr) τ1 τ2 :
138 139
    Closed (x :b: f :b: dom _ Γ) e 
    Closed (x :b: f :b: dom _ Γ) e' 
140 141
     ({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.
142
  Proof.
143
    rewrite bin_log_related_eq.
144
    iIntros (??) "#Ht".
145
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=". cbn.
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
    iDestruct (interp_env_dom with "HΓ") as %Hdom.    
    (* TODO: how to get rid of/ simplify those proofs? *)
    assert (Closed (x :b: f :b: )
              (env_subst (delete f (delete x (fst <$> vvs))) e)).
    { 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.
        rewrite assoc. rewrite difference_union_id. 
        set_solver.
      + rewrite difference_empty.
        rewrite assoc. rewrite difference_union_id. 
        set_solver.
      + rewrite ?(right_id  union).
        rewrite (comm union {[x]} {[f]}) !assoc.
        rewrite difference_union_id. 
        rewrite -!assoc (comm union {[f]} {[x]}) !assoc.
        rewrite difference_union_id. 
        set_solver.
    } 
    assert (Closed (x :b: f :b: )
              (env_subst (delete f (delete x (snd <$> vvs))) e')).
    { 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.
        rewrite assoc. rewrite difference_union_id. 
        set_solver.
      + rewrite difference_empty.
        rewrite assoc. rewrite difference_union_id. 
        set_solver.
      + rewrite ?(right_id  union).
        rewrite (comm union {[x]} {[f]}) !assoc.
        rewrite difference_union_id. 
        rewrite -!assoc (comm union {[f]} {[x]}) !assoc.
        rewrite difference_union_id. 
        set_solver.
187 188
    }
    iModIntro. value_case; eauto. rewrite decide_left; eauto.
189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207
    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.
    tp_rec j'; auto.
    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).
208
    iApply (fupd_mask_mono E); auto.
209
    iApply ("Ht" with "Hj").
210 211
  Qed.

212
  Lemma bin_log_related_injl Δ Γ e e' τ1 τ2 :
213
     specN  E 
214 215
    {E,E;Δ;Γ}  e log e' : τ1 -
    {E,E;Δ;Γ}  InjL e log InjL e' : (TSum τ1 τ2).
216
  Proof.
217
    rewrite bin_log_related_eq.
218
    iIntros (?) "IH".
219
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
220 221
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v w "IH".
    value_case.
222 223
    iExists (InjLV w); iFrame.
    iLeft. iExists (_,_); eauto 10.
224
  Qed.
225
    
226
  Lemma bin_log_related_injr Δ Γ e e' τ1 τ2 :
227
     specN  E 
228 229
    {E,E;Δ;Γ}  e log e' : τ2 -
    {E,E;Δ;Γ}  InjR e log InjR e' : TSum τ1 τ2.
230
  Proof.
231
    rewrite bin_log_related_eq.
232
    iIntros (?) "IH".
233
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
234
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v w "IH".
235
    value_case.
236 237
    iExists (InjRV w); iFrame.
    iRight. iExists (_,_); eauto 10.
238 239
  Qed.

240
  Lemma bin_log_related_case Δ Γ e0 e1 e2 e0' e1' e2' τ1 τ2 τ3 :
241
     specN  E 
242 243 244 245
    {E,E;Δ;Γ}  e0 log e0' : TSum τ1 τ2 -
    {E,E;Δ;Γ}  e1 log e1' : TArrow τ1 τ3 -
    {E,E;Δ;Γ}  e2 log e2' : TArrow τ2 τ3 - 
    {E,E;Δ;Γ}  Case e0 e1 e2 log Case e0' e1' e2' : τ3.
246
  Proof.
247
    rewrite bin_log_related_eq.
248
    iIntros (?) "IH1 IH2 IH3".
249
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
250
    smart_bind j (env_subst _ e0) (env_subst _ e0') "IH1" v v' "IH1".
251
    iDestruct "IH1" as "[Hiv|Hiv]";
252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273
    iDestruct "Hiv" as ([w w']) "[% #Hw]"; simplify_eq; iApply fupd_wp.
    - tp_case_inl j; eauto. 
      iApply wp_case_inl; eauto using to_of_val. fold of_val. 
      iSpecialize ("IH2" with "Hs [HΓ]"); auto.
      tp_bind j (env_subst (snd <$> vvs) e1').
      iApply (fupd_mask_mono _); eauto.
      iMod ("IH2" with "Hj") as "IH2". iModIntro. iNext. simpl.
      wp_bind (env_subst (fst <$> vvs) e1).
      iApply (wp_wand with "IH2").
      iIntros (v). iDestruct 1 as (v') "[Hj #Ht]".
      iSpecialize ("Ht" $! (w, w') with "Hw Hj"). cbn.
      by iApply fupd_wp. 
    - tp_case_inr j; eauto. 
      iApply wp_case_inr; eauto using to_of_val. fold of_val. 
      iSpecialize ("IH3" with "Hs [HΓ]"); auto.
      tp_bind j (env_subst (snd <$> vvs) e2').
      iApply (fupd_mask_mono _); eauto.
      iMod ("IH3" with "Hj") as "IH3". iModIntro. iNext. simpl.
      wp_bind (env_subst (fst <$> vvs) e2).
      iApply (wp_wand with "IH3").
      iIntros (v). iDestruct 1 as (v') "[Hj #Ht]".
      iSpecialize ("Ht" $! (w, w') with "Hw Hj"). cbn.
274
      by iApply fupd_wp.
275 276
  Qed.

277
  Lemma bin_log_related_if Δ Γ e0 e1 e2 e0' e1' e2' τ :
278
    specN  E 
279 280 281 282
    {E,E;Δ;Γ}  e0 log e0' : TBool -
    {E,E;Δ;Γ}  e1 log e1' : τ -
    {E,E;Δ;Γ}  e2 log e2' : τ - 
    {E,E;Δ;Γ}  If e0 e1 e2 log If e0' e1' e2' : τ.
283
  Proof.
284
    rewrite bin_log_related_eq.
285
    iIntros (?) "IH1 IH2 IH3".
286
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
287
    smart_bind j (env_subst _ e0) (env_subst _ e0') "IH1" v v' "IH1".
288
    iDestruct "IH1" as ([]) "[% %]"; simplify_eq/=; iApply fupd_wp.
289 290 291 292 293 294
    - tp_if_true j; eauto. iModIntro.
      iApply wp_if_true. iNext. iApply fupd_wp.
      smart_bind j (env_subst _ e1) (env_subst _ e1') "IH2" v v' "?".
    - tp_if_false j; eauto. iModIntro.
      iApply wp_if_false. iNext. iApply fupd_wp.
      smart_bind j (env_subst _ e2) (env_subst _ e2') "IH3" v v' "?".
295 296
  Qed.

297
  Lemma bin_log_related_nat_binop Δ Γ op e1 e2 e1' e2' :
298
    specN  E 
299 300 301
    {E,E;Δ;Γ}  e1 log e1' : TNat -
    {E,E;Δ;Γ}  e2 log e2' : TNat -
    {E,E;Δ;Γ}  BinOp op e1 e2 log BinOp op e1' e2' : binop_res_type op.
302
  Proof.
303
    rewrite bin_log_related_eq.
304
    iIntros (?) "IH1 IH2".
305
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
306 307
    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
    smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" w w' "IH2".
308 309
    iDestruct "IH1" as (n) "[% %]"; simplify_eq/=.
    iDestruct "IH2" as (n') "[% %]"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
310
    iApply fupd_wp.
311
    tp_nat_binop j; eauto; tp_normalise j.
312
    iApply wp_nat_binop. iModIntro. iExists _; iSplitL; eauto.
313
    repeat iModIntro.
314
    destruct op; simpl; try destruct eq_nat_dec; try destruct le_dec;
315
      try destruct lt_dec; eauto.
316
  Qed.
317

318
  Lemma bin_log_related_tlam Δ Γ e e' τ :
319 320
    Closed (dom _ Γ) e 
    Closed (dom _ Γ) e' 
321 322 323
     specN  E 
    ( (τ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 τ.
324
  Proof.
325
    rewrite bin_log_related_eq.
326
    iIntros (???) "#IH".
327
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
328 329 330 331 332 333 334 335 336 337 338
    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. }
    value_case. rewrite decide_left; eauto. 
    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.
339 340
    iSpecialize ("IH" $! τi with "[] Hs [HΓ]"); auto.
    { by rewrite interp_env_ren. }
341 342
    iSpecialize ("IH" with "Hv").
    iApply (fupd_mask_mono E); eauto.
343
  Qed.
344

345 346 347
  Lemma bin_log_related_tapp' Δ Γ e e' τ τ' :
    {E,E;Δ;Γ}  e log e' : TForall τ -
    {E,E;Δ;Γ}  TApp e log TApp e' : τ.[τ'/].
348
  Proof.
349
    rewrite bin_log_related_eq.
350
    iIntros "IH".
351
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
352
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
353
    iSpecialize ("IH" $! (interp   τ' Δ) with "[#]"); [iPureIntro; apply _|].
354
    iApply wp_wand_r; iSplitL.
355
    iSpecialize ("IH" with "Hj").
356
    iApply fupd_wp. iApply "IH". 
357
    iIntros (w).
358
    iDestruct 1 as (w') "[Hw Hiw]".
359
    iExists _; rewrite -interp_subst; eauto. 
360 361
  Qed.

362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385
  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 τ.
386
  Proof.
387
    rewrite bin_log_related_eq.
388
    iIntros "IH".
389
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
390
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
391
    value_case. 
392
    iExists (FoldV v'); iFrame "Hj".
393
    rewrite fixpoint_unfold /= -interp_subst.
394
    iExists (_, _); eauto.
395 396
  Qed.

397
  Lemma bin_log_related_unfold Δ Γ e e' τ :
398
    specN  E 
399 400
    {E,E;Δ;Γ}  e log e' : TRec τ -
    {E,E;Δ;Γ}  Unfold e log Unfold e' : τ.[(TRec τ)/].
401
  Proof.
402
    rewrite bin_log_related_eq.
403
    iIntros (?) "IH".
404
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
405
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
406
    rewrite /= fixpoint_unfold /=.
407
    change (fixpoint _) with (interp   (TRec τ) Δ).
408
    iDestruct "IH" as ([w w']) "#[% Hiz]"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
409
    iApply fupd_wp.
410 411 412
    tp_fold j; eauto.
    iApply wp_fold; cbn; auto.
    iModIntro; iNext. iExists _; iFrame. by rewrite -interp_subst. 
413 414
  Qed.

415 416 417
  Lemma bin_log_related_pack' Δ Γ e e' τ τ' :
    {E,E;Δ;Γ}  e log e' : τ.[τ'/] -
    {E,E;Δ;Γ}  Pack e log Pack e' : TExists τ.
418
  Proof.
419
    rewrite bin_log_related_eq.
420
    iIntros "IH".
421
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
422
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
423
    value_case. 
424 425
    iExists (PackV v'). simpl. iFrame.
    iExists (v, v'). simpl; iSplit; eauto.
426
    iAlways. rewrite -interp_subst. iExists (interp _ _ τ' Δ).
427 428 429
    iSplit; eauto. iPureIntro. apply _.
  Qed.

430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450
  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]".
    value_case.
    iExists (PackV v'). simpl. iFrame.
    iExists (v, v'). simpl; iSplit; eauto.
  Qed.

  Lemma bin_log_related_unpack Δ Γ e1 e1' e2 e2' τ τ2
451
    (Hmasked : specN  E) :
452 453 454
    {E,E;Δ;Γ}  e1 log e1' : TExists τ -
    ( (τi : D), ⌜∀ ww, PersistentP (τi ww)  {E,E;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$> Γ}  e2 log e2' : TArrow τ (Autosubst_Classes.subst (ren (+1)) τ2)) -
    {E,E;Δ;Γ}  Unpack e1 e2 log Unpack e1' e2' : τ2.
455
  Proof.
456
    rewrite bin_log_related_eq.
457
    iIntros "IH1 IH2".
458
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
459
    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
460
    iDestruct "IH1" as ([w w']) "[% #Hτi]"; simplify_eq/=.
461
    iDestruct "Hτi" as (τi) "[% #Hτi]"; simplify_eq/=.
462
    iApply wp_pack; eauto. iNext.
463
    iApply fupd_wp. 
464
    tp_pack j; eauto. iModIntro.
465 466
    iSpecialize ("IH2" $! τi with "[] Hs [HΓ]"); auto.
    { by rewrite interp_env_ren. }
467 468 469 470 471 472 473 474 475 476
    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.
    iMod "Hvv'". 
    iApply (wp_wand with "Hvv'"). clear v v'.
    iIntros (v). iDestruct 1 as (v') "[Hj #Hvv']".    
477
    rewrite (interp_weaken [] [τi] Δ _ _ τ2) /=.
478
    eauto.
479 480
  Qed.
  
481
  Lemma bin_log_related_fork Δ Γ e e' :
482
    specN  E 
483 484
    {E,E;Δ;Γ}  e log e' : TUnit -
    {E,E;Δ;Γ}  Fork e log Fork e' : TUnit.
485
  Proof.
486
    rewrite bin_log_related_eq.
487
    iIntros (?) "IH".
488
    iIntros (vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
489 490
    tp_fork j as i "Hi". fold subst_p.  iModIntro.
    iApply wp_fork. fold subst_p. iNext. iSplitL "Hj".
491
    - iExists UnitV; eauto.
492 493 494 495
    - iSpecialize ("IH" with "Hs HΓ"). 
      iSpecialize ("IH" $! i []). simpl.
      iSpecialize ("IH" with "Hi"). 
      iApply fupd_wp. iApply (fupd_mask_mono E); eauto.      
496
      iMod "IH". iApply (wp_wand with "IH"). eauto.
497 498
  Qed.

499
  Lemma bin_log_related_alloc Δ Γ e e' τ :
500
    specN  E 
501 502
    {E,E;Δ;Γ}  e log e' : τ -
    {E,E;Δ;Γ}  Alloc e log Alloc e' : Tref τ.
503
  Proof.
504
    rewrite bin_log_related_eq.
505
    iIntros (?) "IH".
506
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
507
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "IH".
Dan Frumin's avatar
Dan Frumin committed
508
    iApply fupd_wp.
509
    tp_alloc j as k "Hk"; eauto.  iModIntro.
Dan Frumin's avatar
Dan Frumin committed
510
    iApply wp_atomic; eauto.
511
    iApply wp_alloc; eauto. iModIntro. iNext.
512 513
    iIntros (l) "Hl". 
    iMod (inv_alloc (logN .@ (l,k)) _ ( w : val * val,
514
      l ↦ᵢ w.1  k ↦ₛ w.2  interp _ _ τ Δ w)%I with "[Hl Hk IH]") as "HN"; eauto.
515 516
    { iNext. iExists (v, v'); simpl; iFrame. }
    iModIntro; iExists (LocV k).
517
    iFrame "Hj". iExists (l, k); eauto.
518 519
  Qed.

520
  Lemma bin_log_related_load Δ Γ e e' τ :
521 522
    specN  E 
    logN   E 
523 524
    {E,E;Δ;Γ}  e log e' : (Tref τ) -
    {E,E;Δ;Γ}  Load e log Load e' : τ.
525
  Proof.
526
    rewrite bin_log_related_eq.
527
    iIntros (??) "IH".
528
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
529
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "IH".
530
    iDestruct "IH" as ([l l']) "[% Hinv]"; simplify_eq/=. 
Dan Frumin's avatar
Dan Frumin committed
531 532 533 534 535
    iApply wp_atomic; eauto.
    iInv (logN .@ (l,l')) as ([w w']) "[Hw1 [>Hw2 #Hw]]" "Hclose"; simpl.
    iModIntro.
    iApply (wp_load with "Hw1").
    iNext. iIntros "Hw1".
536
    tp_load j.
Dan Frumin's avatar
Dan Frumin committed
537
    iMod ("Hclose" with "[Hw1 Hw2]").
Robbert Krebbers's avatar
Robbert Krebbers committed
538
    { iNext. iExists (w,w'); by iFrame. }
539
    iModIntro. iExists w'; by iFrame.
540 541
  Qed.

542
  Lemma bin_log_related_store Δ Γ e1 e2 e1' e2' τ :
543 544
    specN  E 
    logN   E     
545 546 547
    {E,E;Δ;Γ}  e1 log e1' : (Tref τ) -
    {E,E;Δ;Γ}  e2 log e2' : τ -
    {E,E;Δ;Γ}  Store e1 e2 log Store e1' e2' : TUnit.
548
  Proof.
549
    rewrite bin_log_related_eq.
550
    iIntros (??) "IH1 IH2".
551
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
552 553
    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
    smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" w w' "#IH2".
554
    iDestruct "IH1" as ([l l']) "[% Hinv]"; simplify_eq/=. 
Dan Frumin's avatar
Dan Frumin committed
555 556 557 558
    iApply wp_atomic; eauto.
    iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
    iModIntro.
    iApply (wp_store with "Hv1"); auto using to_of_val. 
Dan Frumin's avatar
Dan Frumin committed
559 560
    iNext. iIntros "Hw2".
    tp_store j.
Dan Frumin's avatar
Dan Frumin committed
561
    iMod ("Hclose" with "[Hw2 Hv2]").
562
    { iNext; iExists (_, _); simpl; iFrame. iFrame "IH2". }
Robbert Krebbers's avatar
Robbert Krebbers committed
563
    iExists UnitV; iFrame; auto.
564 565
  Qed.

566
  Lemma bin_log_related_CAS Δ Γ e1 e2 e3 e1' e2' e3' τ
567 568 569
    (HEqτ : EqType τ) :
    specN  E     
    logN   E     
570 571 572 573
    {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.
574
  Proof.
575
    rewrite bin_log_related_eq.
576
    iIntros (??) "IH1 IH2 IH3".
577
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
578 579 580
    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
    smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" w w' "#IH2".
    smart_bind j (env_subst _ e3) (env_subst _ e3') "IH3" u u' "#IH3".
581
    iDestruct "IH1" as ([l l']) "[% Hinv]"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
582 583 584
    iApply wp_atomic; eauto.
    iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
    iModIntro.
585
    iPoseProof ("Hv") as "Hv'".
586
    rewrite {2}[interp _ _ τ Δ (v, v')]interp_EqType_agree; trivial.
587 588
    iMod "Hv'" as %Hv'; subst.
    destruct (decide (v' = w)) as [|Hneq]; subst.
Dan Frumin's avatar
Dan Frumin committed
589
    - iAssert ( w' = w)%I as ">%".
590
      { rewrite ?interp_EqType_agree; trivial. by iSimplifyEq. }
Dan Frumin's avatar
Dan Frumin committed
591 592
      simpl. iApply (wp_cas_suc with "Hv1"); eauto using to_of_val.
      iNext. iIntros "Hv1".
593
      tp_cas_suc j; subst; eauto using to_of_val. 
Dan Frumin's avatar
Dan Frumin committed
594
      iMod ("Hclose" with "[Hv1 Hv2]").
Robbert Krebbers's avatar
Robbert Krebbers committed
595
      { iNext; iExists (_, _); by iFrame. }
596
      iExists (#v true). iModIntro. eauto. 
Dan Frumin's avatar
Dan Frumin committed
597 598 599 600
    - iAssert ( v'  w'⌝)%I as ">%".
      { rewrite ?interp_EqType_agree; trivial. iSimplifyEq. auto. }
      simpl. iApply (wp_cas_fail with "Hv1"); eauto.
      iNext. iIntros "Hv1". 
601
      tp_cas_fail j; eauto.
Dan Frumin's avatar
Dan Frumin committed
602
      iMod ("Hclose" with "[Hv1 Hv2]").
Robbert Krebbers's avatar
Robbert Krebbers committed
603
      { iNext; iExists (_, _); by iFrame. }
604
      iExists (#v false); repeat iModIntro; eauto.
605 606
  Qed.

607
  Theorem binary_fundamental_masked Δ Γ e τ :
608 609
    specN  E 
    logN  E 
610
    Γ ⊢ₜ e : τ  ({E,E;Δ;Γ}  e log e : τ)%I.
611
  Proof.
612
    intros HspecN HlogN Ht. iInduction Ht as [] "IH" forall (Δ).
613 614 615 616 617 618 619 620 621 622
    - 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 "[]").
    - 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.
623
    - by iApply (bin_log_related_case with "[] []").
624
    - by iApply (bin_log_related_if with "[] []").
625 626 627 628 629 630 631 632
    - assert (Closed (x :b: f :b: dom (gset string) Γ) e).
      { apply typed_X_closed in Ht.
        rewrite !dom_insert_binder in Ht.
        revert Ht. destruct x,f; cbn-[union]; 
        (* TODO: why is simple rewriting is not sufficient here? *)
        erewrite ?(left_id ); eauto.
        all: apply _. }
      iApply (bin_log_related_rec with "[]"); eauto.
633
    - by iApply (bin_log_related_app with "[] []").
634 635 636 637 638
    - assert (Closed (dom _ Γ) e).
      { apply typed_X_closed in Ht.        
        pose (K:=(dom_fmap (Autosubst_Classes.subst (ren (+1))) Γ)). 
        fold_leibniz. by rewrite -K. }
      iApply bin_log_related_tlam; eauto.
639
    - by iApply bin_log_related_tapp'.
640 641
    - by iApply bin_log_related_fold.
    - by iApply bin_log_related_unfold.
642 643
    - by iApply bin_log_related_pack'.
    - iApply (bin_log_related_unpack with "[]"); eauto.
644 645 646 647 648
    - 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 "[] []").
649
  Qed.
650 651 652 653 654 655
End masked.

Theorem binary_fundamental Γ e τ :
  Γ ⊢ₜ e : τ  (Γ  e log e : τ)%I.
Proof. by eapply binary_fundamental_masked. Qed.

656
End fundamental.