fundamental_binary.v 22.6 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 9 10 11 12 13 14 15
Context `{heapIG Σ, cfgSG Σ}.
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 38 39 40 41 42 43 44
    iIntros (? Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
    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'. } 
45
    iModIntro. value_case; eauto.
46 47
  Qed.

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

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

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

69
  Lemma bin_log_related_pair Γ e1 e2 e1' e2' τ1 τ2 :
70 71 72
      {E,E;Γ}  e1 log e1' : τ1 -
      {E,E;Γ}  e2 log e2' : τ2 -
      {E,E;Γ}  Pair e1 e2 log Pair e1' e2' : TProd τ1 τ2.
73
  Proof.
74
    iIntros "IH1 IH2". iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
75 76 77 78
    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.
79 80 81
    iExists (PairV w1 w2); iFrame. 
    iExists _, _; eauto.
    iSplit; simpl; eauto.  auto. 
82 83
  Qed.

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

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

  Lemma bin_log_related_app Γ e1 e2 e1' e2' τ1 τ2 :
117 118 119
    {E,E;Γ}  e1 log e1' : TArrow τ1 τ2 -
    {E,E;Γ}  e2 log e2' : τ1 -
    {E,E;Γ}  App e1 e2 log App e1' e2' :  τ2.
120 121 122 123 124 125 126 127
  Proof.
    iIntros "IH1 IH2".
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    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
128
    
129 130 131
  Lemma bin_log_related_rec (Γ : stringmap type) (f x : binder) (e e' : expr) τ1 τ2 :
    Closed (x :b: f :b: dom _ Γ) e 
    Closed (x :b: f :b: dom _ Γ) e' 
132 133
     ({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.
134 135 136 137 138 139 140 141 142 143 144 145 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
  Proof.
    iIntros (??) "#Ht".
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=". cbn.
    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.
178 179
    }
    iModIntro. value_case; eauto. rewrite decide_left; eauto.
180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198
    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).
199
    iApply (fupd_mask_mono E); auto.
200
    iApply ("Ht" with "Hj").
201 202
  Qed.

203
  Lemma bin_log_related_injl Γ e e' τ1 τ2 :
204 205 206
     specN  E 
    {E,E;Γ}  e log e' : τ1 -
    {E,E;Γ}  InjL e log InjL e' : (TSum τ1 τ2).
207
  Proof.
208
    iIntros (?) "IH".
209
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
210 211
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v w "IH".
    value_case.
212 213
    iExists (InjLV w); iFrame.
    iLeft. iExists (_,_); eauto 10.
214
  Qed.
215
    
216
  Lemma bin_log_related_injr Γ e e' τ1 τ2 :
217 218 219
     specN  E 
    {E,E;Γ}  e log e' : τ2 -
    {E,E;Γ}  InjR e log InjR e' : TSum τ1 τ2.
220
  Proof.
221
    iIntros (?) "IH".
222
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
223
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v w "IH".
224
    value_case.
225 226
    iExists (InjRV w); iFrame.
    iRight. iExists (_,_); eauto 10.
227 228
  Qed.

229 230 231 232 233
  Lemma bin_log_related_case Γ e0 e1 e2 e0' e1' e2' τ1 τ2 τ3 :
     specN  E 
    {E,E;Γ}  e0 log e0' : TSum τ1 τ2 -
    {E,E;Γ}  e1 log e1' : TArrow τ1 τ3 -
    {E,E;Γ}  e2 log e2' : TArrow τ2 τ3 - 
234
    {E,E;Γ}  Case e0 e1 e2 log Case e0' e1' e2' : τ3.
235
  Proof.
236
    iIntros (?) "IH1 IH2 IH3".
237
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
238
    smart_bind j (env_subst _ e0) (env_subst _ e0') "IH1" v v' "IH1".
239
    iDestruct "IH1" as "[Hiv|Hiv]";
240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262
    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.
      by iApply fupd_wp. 
263 264
  Qed.

265 266
  Lemma bin_log_related_if Γ e0 e1 e2 e0' e1' e2' τ :
    specN  E 
267 268 269 270
    {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' : τ.
271
  Proof.
272
    iIntros (?) "IH1 IH2 IH3".
273
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
274
    smart_bind j (env_subst _ e0) (env_subst _ e0') "IH1" v v' "IH1".
275
    iDestruct "IH1" as ([]) "[% %]"; simplify_eq/=; iApply fupd_wp.
276 277 278 279 280 281
    - 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' "?".
282 283
  Qed.

284 285
  Lemma bin_log_related_nat_binop Γ op e1 e2 e1' e2' :
    specN  E 
286 287 288
    {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.
289
  Proof.
290
    iIntros (?) "IH1 IH2".
291
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
292 293
    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".
294 295
    iDestruct "IH1" as (n) "[% %]"; simplify_eq/=.
    iDestruct "IH2" as (n') "[% %]"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
296
    iApply fupd_wp.
297
    tp_nat_binop j; eauto; tp_normalise j.
298
    iApply wp_nat_binop. iModIntro. iExists _; iSplitL; eauto.
299
    repeat iModIntro.
300
    destruct op; simpl; try destruct eq_nat_dec; try destruct le_dec;
301
      try destruct lt_dec; eauto.
302
  Qed.
303

304
  Lemma bin_log_related_tlam Γ e e' τ :
305 306
    Closed (dom _ Γ) e 
    Closed (dom _ Γ) e' 
307
    ( specN  E) 
308 309
     ({E,E;(Autosubst_Classes.subst (ren (+1)) <$> Γ)}  e log e' : τ) -
    {E,E;Γ}  TLam e log TLam e' : TForall τ.
310
  Proof.
311
    iIntros (???) "#IH".
312
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
313 314 315 316 317 318 319 320 321 322 323 324
    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.
    iSpecialize ("IH" with "Hs [HΓ]"); auto.
325
    { iAlways. by iApply interp_env_ren. }
326 327
    iSpecialize ("IH" with "Hv").
    iApply (fupd_mask_mono E); eauto.
328
  Qed.
329

330
  Lemma bin_log_related_tapp Γ e e' τ τ' :
331 332
    {E,E;Γ}  e log e' : TForall τ -
    {E,E;Γ}  TApp e log TApp e' : τ.[τ'/].
333
  Proof.
334 335
    iIntros "IH".
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
336
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
337
    iSpecialize ("IH" $! (interp   τ' Δ) with "[#]"); [iPureIntro; apply _|].
338
    iApply wp_wand_r; iSplitL.
339
    iSpecialize ("IH" with "Hj").
340
    iApply fupd_wp. iApply "IH". 
341
    iIntros (w).
342
    iDestruct 1 as (w') "[Hw Hiw]".
343
    iExists _; rewrite -interp_subst; eauto. 
344 345
  Qed.

346
  Lemma bin_log_related_fold Γ e e' τ :
347 348
    {E,E;Γ}  e log e' : τ.[(TRec τ)/] -
    {E,E;Γ}  Fold e log Fold e' : TRec τ.
349
  Proof.
350 351
    iIntros "IH".
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
352
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
353
    value_case. 
354
    iExists (FoldV v'); iFrame "Hj".
355
    rewrite fixpoint_unfold /= -interp_subst.
356
    iExists (_, _); eauto.
357 358
  Qed.

359 360
  Lemma bin_log_related_unfold Γ e e' τ :
    specN  E 
361 362
    {E,E;Γ}  e log e' : TRec τ -
    {E,E;Γ}  Unfold e log Unfold e' : τ.[(TRec τ)/].
363
  Proof.
364
    iIntros (?) "IH".
365
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
366
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
367
    rewrite /= fixpoint_unfold /=.
368
    change (fixpoint _) with (interp   (TRec τ) Δ).
369
    iDestruct "IH" as ([w w']) "#[% Hiz]"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
370
    iApply fupd_wp.
371 372 373
    tp_fold j; eauto.
    iApply wp_fold; cbn; auto.
    iModIntro; iNext. iExists _; iFrame. by rewrite -interp_subst. 
374 375
  Qed.

376
  Lemma bin_log_related_pack Γ e e' τ τ' :
377 378
    {E,E;Γ}  e log e' : τ.[τ'/] -
    {E,E;Γ}  Pack e log Pack e' : TExists τ.
379
  Proof.
380 381
    iIntros "IH".
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
382
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
383
    value_case. 
384 385
    iExists (PackV v'). simpl. iFrame.
    iExists (v, v'). simpl; iSplit; eauto.
386
    iAlways. rewrite -interp_subst. iExists (interp _ _ τ' Δ).
387 388 389
    iSplit; eauto. iPureIntro. apply _.
  Qed.

390 391
  Lemma bin_log_related_unpack Γ e1 e1' e2 e2' τ τ2
    (Hmasked : specN  E) :
392 393 394
    {E,E;Γ}  e1 log e1' : TExists τ -
    {E,E;(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.
395
  Proof.
396 397
    iIntros "IH1 IH2".
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
398
    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
399
    iDestruct "IH1" as ([w w']) "[% #Hτi]"; simplify_eq/=.
400
    iDestruct "Hτi" as (τi) "[% #Hτi]"; simplify_eq/=. 
401
    iApply wp_pack; eauto. iNext.
402
    iApply fupd_wp. 
403 404 405 406 407 408 409 410 411 412 413 414 415 416
    tp_pack j; eauto. iModIntro.
    iSpecialize ("IH2" with "Hs [HΓ]"); auto.
    { iAlways. by iApply interp_env_ren. }
    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']".    
    rewrite (interp_weaken [] [τi] Δ _ _ τ2). simpl.
417
    eauto.
418 419
  Qed.
  
420 421
  Lemma bin_log_related_fork Γ e e' :
    specN  E 
422 423
    {E,E;Γ}  e log e' : TUnit -
    {E,E;Γ}  Fork e log Fork e' : TUnit.
424
  Proof.
425
    iIntros (?) "IH".
426
    iIntros (Δ vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
427 428
    tp_fork j as i "Hi". fold subst_p.  iModIntro.
    iApply wp_fork. fold subst_p. iNext. iSplitL "Hj".
429
    - iExists UnitV; eauto.
430 431 432 433
    - iSpecialize ("IH" with "Hs HΓ"). 
      iSpecialize ("IH" $! i []). simpl.
      iSpecialize ("IH" with "Hi"). 
      iApply fupd_wp. iApply (fupd_mask_mono E); eauto.      
434
      iMod "IH". iApply (wp_wand with "IH"). eauto.
435 436
  Qed.

437 438
  Lemma bin_log_related_alloc Γ e e' τ :
    specN  E 
439 440
    {E,E;Γ}  e log e' : τ -
    {E,E;Γ}  Alloc e log Alloc e' : Tref τ.
441
  Proof.
442
    iIntros (?) "IH".
443
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
444
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "IH".
Dan Frumin's avatar
Dan Frumin committed
445
    iApply fupd_wp.
446
    tp_alloc j as k "Hk"; eauto.  iModIntro.
Dan Frumin's avatar
Dan Frumin committed
447
    iApply wp_atomic; eauto.
448
    iApply wp_alloc; eauto. iModIntro. iNext.
449 450
    iIntros (l) "Hl". 
    iMod (inv_alloc (logN .@ (l,k)) _ ( w : val * val,
451
      l ↦ᵢ w.1  k ↦ₛ w.2  interp _ _ τ Δ w)%I with "[Hl Hk IH]") as "HN"; eauto.
452 453
    { iNext. iExists (v, v'); simpl; iFrame. }
    iModIntro; iExists (LocV k).
454
    iFrame "Hj". iExists (l, k); eauto.
455 456
  Qed.

457 458 459
  Lemma bin_log_related_load Γ e e' τ :
    specN  E 
    logN   E 
460 461
    {E,E;Γ}  e log e' : (Tref τ) -
    {E,E;Γ}  Load e log Load e' : τ.
462
  Proof.
463
    iIntros (??) "IH".
464
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
465
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "IH".
466
    iDestruct "IH" as ([l l']) "[% Hinv]"; simplify_eq/=. 
Dan Frumin's avatar
Dan Frumin committed
467 468 469 470 471
    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".
472
    tp_load j.
Dan Frumin's avatar
Dan Frumin committed
473
    iMod ("Hclose" with "[Hw1 Hw2]").
Robbert Krebbers's avatar
Robbert Krebbers committed
474
    { iNext. iExists (w,w'); by iFrame. }
475
    iModIntro. iExists w'; by iFrame.
476 477
  Qed.

478 479 480
  Lemma bin_log_related_store Γ e1 e2 e1' e2' τ :
    specN  E 
    logN   E     
481 482 483
    {E,E;Γ}  e1 log e1' : (Tref τ) -
    {E,E;Γ}  e2 log e2' : τ -
    {E,E;Γ}  Store e1 e2 log Store e1' e2' : TUnit.
484
  Proof.
485
    iIntros (??) "IH1 IH2".
486
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
487 488
    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".
489
    iDestruct "IH1" as ([l l']) "[% Hinv]"; simplify_eq/=. 
Dan Frumin's avatar
Dan Frumin committed
490 491 492 493 494
    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. 
    iNext. iIntros "Hw2". 
495
    tp_store j; eauto; tp_normalise j.
Dan Frumin's avatar
Dan Frumin committed
496
    iMod ("Hclose" with "[Hw2 Hv2]").
497
    { iNext; iExists (_, _); simpl; iFrame. iFrame "IH2". }
Robbert Krebbers's avatar
Robbert Krebbers committed
498
    iExists UnitV; iFrame; auto.
499 500
  Qed.

501 502 503 504
  Lemma bin_log_related_CAS Γ e1 e2 e3 e1' e2' e3' τ 
    (HEqτ : EqType τ) :
    specN  E     
    logN   E     
505 506 507 508
    {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.
509
  Proof.
510
    iIntros (??) "IH1 IH2 IH3".
511
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
512 513 514
    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".
515
    iDestruct "IH1" as ([l l']) "[% Hinv]"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
516 517 518
    iApply wp_atomic; eauto.
    iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
    iModIntro.
519
    iPoseProof ("Hv") as "Hv'".
520
    rewrite {2}[interp _ _ τ Δ (v, v')]interp_EqType_agree; trivial.
521 522
    iMod "Hv'" as %Hv'; subst.
    destruct (decide (v' = w)) as [|Hneq]; subst.
Dan Frumin's avatar
Dan Frumin committed
523
    - iAssert ( w' = w)%I as ">%".
524
      { rewrite ?interp_EqType_agree; trivial. by iSimplifyEq. }
Dan Frumin's avatar
Dan Frumin committed
525 526
      simpl. iApply (wp_cas_suc with "Hv1"); eauto using to_of_val.
      iNext. iIntros "Hv1".
527
      tp_cas_suc j; subst; eauto using to_of_val. 
Dan Frumin's avatar
Dan Frumin committed
528
      iMod ("Hclose" with "[Hv1 Hv2]").
Robbert Krebbers's avatar
Robbert Krebbers committed
529
      { iNext; iExists (_, _); by iFrame. }
530
      iExists (#v true). iModIntro. eauto. 
Dan Frumin's avatar
Dan Frumin committed
531 532 533 534
    - iAssert ( v'  w'⌝)%I as ">%".
      { rewrite ?interp_EqType_agree; trivial. iSimplifyEq. auto. }
      simpl. iApply (wp_cas_fail with "Hv1"); eauto.
      iNext. iIntros "Hv1". 
535
      tp_cas_fail j; eauto.
Dan Frumin's avatar
Dan Frumin committed
536
      iMod ("Hclose" with "[Hv1 Hv2]").
Robbert Krebbers's avatar
Robbert Krebbers committed
537
      { iNext; iExists (_, _); by iFrame. }
538
      iExists (#v false); repeat iModIntro; eauto.
539 540
  Qed.

541
  Opaque bin_log_related.
542 543 544 545 546

  Theorem binary_fundamental_masked Γ e τ :
    specN  E 
    logN  E 
    Γ ⊢ₜ e : τ  ({E,E;Γ}  e log e : τ)%I.
547
  Proof.
548
    intros HspecN HlogN Ht. iInduction Ht as [] "IH".
549 550 551 552 553 554 555 556 557 558
    - 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.
559
    - by iApply (bin_log_related_case with "[] []").
560
    - by iApply (bin_log_related_if with "[] []").
561 562 563 564 565 566 567 568
    - 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.
569
    - by iApply (bin_log_related_app with "[] []").
570 571 572 573 574
    - 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.
575 576 577 578 579 580 581 582 583 584
    - by iApply bin_log_related_tapp.
    - by iApply bin_log_related_fold.
    - by iApply bin_log_related_unfold.
    - by iApply bin_log_related_pack.
    - by iApply (bin_log_related_unpack with "[]").
    - 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 "[] []").
585
  Qed.
586 587 588 589 590 591
End masked.

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

592
End fundamental.