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 6 7 8 9
  Context `{logrelG Σ}.
  Notation D := (prodC valC valC -n> iProp Σ).
  Implicit Types e : expr.
  Implicit Types Δ : listC D.
  Hint Resolve to_of_val.
10

11
  Local Ltac value_case :=
12
    iApply (related_ret );
13 14
    iApply interp_ret; [solve_to_val..|];
    simpl; eauto.
15

16
  Local Ltac value_case' := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|]; repeat iModIntro; try solve_to_val.
17 18 19 20 21 22 23 24

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

39
  Lemma bin_log_related_var Δ Γ x τ :
40
    Γ !! x = Some τ 
41
    {Δ;Γ}  Var x log Var x : τ.
42
  Proof.
43
    rewrite bin_log_related_eq.
44
    iIntros (? vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
45 46 47 48
    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.
49
    { rewrite lookup_fmap. by rewrite Hvv'. }
50
    rewrite (env_subst_lookup _ x v); last first.
51 52
    { rewrite lookup_fmap. by rewrite Hvv'. }
    iModIntro.
53
    iApply wp_value. eauto.
54 55
  Qed.

56
  Lemma bin_log_related_unit Δ Γ : {Δ;Γ}  #() log #() : Unit.
57
  Proof.
58
    value_case.
59 60
  Qed.

61
  Lemma bin_log_related_nat Δ Γ (n : nat) : {Δ;Γ}  #n log #n : TNat.
62
  Proof.
63
    value_case.
64 65
  Qed.

66
  Lemma bin_log_related_bool Δ Γ (b : bool) : {Δ;Γ}  #b log #b : Bool.
67
  Proof.
68
    value_case.
69
  Qed.
70

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

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

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

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

120
  Lemma bin_log_related_rec Δ (Γ : stringmap type) (f x : binder) (e e' : expr) τ1 τ2 :
121 122
    Closed (x :b: f :b: dom _ Γ) e 
    Closed (x :b: f :b: dom _ Γ) e' 
123 124
     ({Δ;<[x:=τ1]>(<[f:=TArrow τ1 τ2]>Γ)}  e log e' : τ2) -
    {Δ;Γ}  Rec f x e log Rec f x e' : TArrow τ1 τ2.
125
  Proof.
126
    rewrite bin_log_related_eq.
127
    iIntros (??) "#Ht".
128
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=". cbn.
129
    iDestruct (interp_env_dom with "HΓ") as %Hdom.
130 131
    (* TODO: how to get rid of/ simplify those proofs? *)
    assert (Closed (x :b: f :b: )
132
              (subst_p (delete f (delete x (fst <$> vvs))) e)).
133 134 135 136 137 138
    { 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.
139
        rewrite assoc. rewrite difference_union.
140 141
        set_solver.
      + rewrite difference_empty.
142
        rewrite assoc. rewrite difference_union.
143 144 145
        set_solver.
      + rewrite ?(right_id  union).
        rewrite (comm union {[x]} {[f]}) !assoc.
146
        rewrite difference_union.
147
        rewrite -!assoc (comm union {[f]} {[x]}) !assoc.
148
        rewrite difference_union.
149
        set_solver. }
150
    assert (Closed (x :b: f :b: )
151
              (subst_p (delete f (delete x (snd <$> vvs))) e')).
152 153 154 155 156 157
    { 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.
158
        rewrite assoc. rewrite difference_union.
159 160
        set_solver.
      + rewrite difference_empty.
161
        rewrite assoc. rewrite difference_union.
162 163 164
        set_solver.
      + rewrite ?(right_id  union).
        rewrite (comm union {[x]} {[f]}) !assoc.
165
        rewrite difference_union.
166
        rewrite -!assoc (comm union {[f]} {[x]}) !assoc.
167
        rewrite difference_union.
168
        set_solver.
169
    }
170
    iModIntro. value_case'; eauto.
171
    { rewrite /IntoVal. simpl. rewrite decide_left; eauto. }
172 173 174
    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.
Dan Frumin's avatar
Dan Frumin committed
175
    wp_rec.
176
    iApply fupd_wp.
177
    tp_rec j'.
178
    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))).
179
    iAssert (interp_env (<[x:=τ1]> (<[f:=TArrow τ1 τ2]> Γ))  Δ vvs') as "#HΓ'".
180 181 182 183 184 185 186 187 188 189 190 191
    { 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).
    iApply ("Ht" with "Hj").
192 193
  Qed.

Dan Frumin's avatar
Dan Frumin committed
194
  Lemma bin_log_related_seq R Δ Γ e1 e2 e1' e2' τ1 τ2 `{Closed  e2} `{Closed  e2'} :
195 196 197
    {(R::Δ);⤉Γ}  e1 log e1' : τ1 -
    {Δ;Γ}  e2 log e2' : τ2 -
    {Δ;Γ}  (e1;; e2) log (e1';; e2') : τ2.
198
  Proof.
199
    iIntros "He1 He2".
200 201
    rel_bind_l e1.
    rel_bind_r e1'.
Dan Frumin's avatar
Dan Frumin committed
202
    iApply (related_bind_up _ _ R with "He1 [He2]").
203 204 205 206 207 208
    iIntros (?) "? /=".
    rel_rec_l.
    rel_rec_r.
    done.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
209
  Lemma bin_log_related_seq' Δ Γ e1 e2 e1' e2' τ1 τ2 `{Closed  e2} `{Closed  e2'} :
210 211 212
    {Δ;Γ}  e1 log e1' : τ1 -
    {Δ;Γ}  e2 log e2' : τ2 -
    {Δ;Γ}  (e1;; e2) log (e1';; e2') : τ2.
Dan Frumin's avatar
Dan Frumin committed
213
  Proof.
214
    iIntros "He1 He2".
Dan Frumin's avatar
Dan Frumin committed
215 216 217 218
    iApply (bin_log_related_seq (λne _, True%I) _ _ _ _ _ _ τ1.[ren (+1)] with "[He1]"); auto.
    by iApply bin_log_related_weaken_2.
  Qed.

219
  Lemma bin_log_related_injl Δ Γ e e' τ1 τ2 :
220 221
    {Δ;Γ}  e log e' : τ1 -
    {Δ;Γ}  InjL e log InjL e' : (TSum τ1 τ2).
222
  Proof.
223
    iIntros "IH".
224
    rel_bind_ap e e' "IH" v v' "Hvv".
225
    value_case.
226
    iLeft. iExists (_,_); eauto.
227
  Qed.
228

229
  Lemma bin_log_related_injr Δ Γ e e' τ1 τ2 :
230 231
    {Δ;Γ}  e log e' : τ2 -
    {Δ;Γ}  InjR e log InjR e' : TSum τ1 τ2.
232
  Proof.
233
    iIntros "IH".
234
    rel_bind_ap e e' "IH" v v' "Hvv".
235
    value_case.
236
    iRight. iExists (_,_); eauto.
237 238
  Qed.

239
  Lemma bin_log_related_case Δ Γ e0 e1 e2 e0' e1' e2' τ1 τ2 τ3 :
240 241 242 243
    {Δ;Γ}  e0 log e0' : TSum τ1 τ2 -
    {Δ;Γ}  e1 log e1' : TArrow τ1 τ3 -
    {Δ;Γ}  e2 log e2' : TArrow τ2 τ3 -
    {Δ;Γ}  Case e0 e1 e2 log Case e0' e1' e2' : τ3.
244
  Proof.
245
    iIntros "IH1 IH2 IH3".
246
    rel_bind_ap e0 e0' "IH1" v0 v0' "IH1".
247
    iDestruct "IH1" as "[Hiv|Hiv]";
248
    iDestruct "Hiv" as ([w w']) "[% #Hw]"; simplify_eq/=;
249 250 251 252 253
      rel_case_l; rel_case_r.
    - iApply (bin_log_related_app with "IH2").
      value_case.
    - iApply (bin_log_related_app with "IH3").
      value_case.
254 255
  Qed.

256
  Lemma bin_log_related_if Δ Γ e0 e1 e2 e0' e1' e2' τ :
257 258 259 260
    {Δ;Γ}  e0 log e0' : TBool -
    {Δ;Γ}  e1 log e1' : τ -
    {Δ;Γ}  e2 log e2' : τ -
    {Δ;Γ}  If e0 e1 e2 log If e0' e1' e2' : τ.
261
  Proof.
262
    iIntros "IH1 IH2 IH3".
263
    rel_bind_ap e0 e0' "IH1" v0 v0' "IH1".
264
    iDestruct "IH1" as ([]) "[% %]"; simplify_eq/=;
265
      rel_if_l; rel_if_r; iAssumption.
266 267
  Qed.

Dan Frumin's avatar
Dan Frumin committed
268 269
  Lemma bin_log_related_nat_binop Δ Γ op e1 e2 e1' e2' τ :
    binop_nat_res_type op = Some τ 
270 271 272
    {Δ;Γ}  e1 log e1' : TNat -
    {Δ;Γ}  e2 log e2' : TNat -
    {Δ;Γ}  BinOp op e1 e2 log BinOp op e1' e2' : τ.
273
  Proof.
274
    iIntros (Hopτ) "IH1 IH2".
275 276
    rel_bind_ap e1 e1' "IH1" v1 v1' "IH1".
    rel_bind_ap e2 e2' "IH2" v2 v2' "IH2".
277 278
    iDestruct "IH1" as (n) "[% %]"; simplify_eq/=.
    iDestruct "IH2" as (n') "[% %]"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
279
    destruct (binop_nat_typed_safe op n n' _ Hopτ) as [v' Hopv'].
280 281 282
    rel_op_l; eauto.
    rel_op_r; eauto.
    value_case.
283
    destruct op; simpl in Hopv'; simplify_eq/=; try case_match; eauto.
Dan Frumin's avatar
Dan Frumin committed
284 285 286 287
  Qed.

  Lemma bin_log_related_bool_binop Δ Γ op e1 e2 e1' e2' τ :
    binop_bool_res_type op = Some τ 
288 289 290
    {Δ;Γ}  e1 log e1' : TBool -
    {Δ;Γ}  e2 log e2' : TBool -
    {Δ;Γ}  BinOp op e1 e2 log BinOp op e1' e2' : τ.
Dan Frumin's avatar
Dan Frumin committed
291
  Proof.
292
    iIntros (Hopτ) "IH1 IH2".
293 294
    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
295 296 297
    iDestruct "IH1" as (n) "[% %]"; simplify_eq/=.
    iDestruct "IH2" as (n') "[% %]"; simplify_eq/=.
    destruct (binop_bool_typed_safe op n n' _ Hopτ) as [v' Hopv'].
298 299 300
    rel_op_l; eauto.
    rel_op_r; eauto.
    value_case.
301
    destruct op; simpl in Hopv'; simplify_eq/=; eauto.
302
  Qed.
303

304
  Lemma bin_log_related_ref_binop Δ Γ e1 e2 e1' e2' τ :
305 306 307
    {Δ;Γ}  e1 log e1' : Tref τ -
    {Δ;Γ}  e2 log e2' : Tref τ -
    {Δ;Γ}  BinOp Eq e1 e2 log BinOp Eq e1' e2' : TBool.
308
  Proof.
309
    iIntros "IH1 IH2".
310 311 312 313 314 315 316
    rel_bind_ap e1 e1' "IH1" v1 v1' "#IH1".
    rel_bind_ap e2 e2' "IH2" v2 v2' "#IH2".
    iDestruct "IH1" as ([l1 l2]) "[% #Hl]"; simplify_eq/=.
    iDestruct "IH2" as ([l1' l2']) "[% #Hl']"; simplify_eq/=.
    rel_op_l.
    rel_op_r.
    destruct (decide (l1 = l1')) as [->|?].
317
    - iMod (interp_ref_funct _ _ _ l1' l2 l2' with "[Hl Hl']") as %->.
318 319 320 321 322
      { solve_ndisj. }
      { iSplit; iExists (_,_); eauto. }
      rewrite decide_left.
      value_case.
    - destruct (decide (l2 = l2')) as [->|?].
323
      + iMod (interp_ref_inj _ _ _ l2' l1 l1' with "[Hl Hl']") as %->.
324 325 326 327 328 329
        { solve_ndisj. }
        { iSplit; iExists (_,_); eauto. }
        congruence.
      + value_case.
  Qed.

330
  Lemma bin_log_related_tlam Δ Γ e e' τ :
331 332
    Closed (dom _ Γ) e 
    Closed (dom _ Γ) e' 
333 334
    ( (τi : D),
       ({(τi::Δ);⤉Γ}  e log e' : τ)) -
335
    {Δ;Γ}  TLam e log TLam e' : TForall τ.
336
  Proof.
337
    rewrite bin_log_related_eq.
338
    iIntros (? ?) "#IH".
339
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
340 341 342 343 344
    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. }
345
    iModIntro. iApply wp_value.
346 347
    iExists (TLamV (env_subst (snd <$> vvs) e')). cbn.
    iFrame "Hj". iAlways.
348 349
    iIntros (τi). iIntros (j' K') "Hv /=".
    (* iIntros (τi ? j' K') "Hv /=". *)
Dan Frumin's avatar
Dan Frumin committed
350 351
    iModIntro. wp_tlam.
    iApply fupd_wp.
352
    tp_tlam j'; eauto.
353
    iSpecialize ("IH" $! τi with "Hs [HΓ]"); auto.
354
    { by rewrite interp_env_ren. }
355
    iApply ("IH" with "Hv").
356
  Qed.
357

358
  Lemma bin_log_related_tapp' Δ Γ e e' τ τ' :
359 360
    {Δ;Γ}  e log e' : TForall τ -
    {Δ;Γ}  TApp e log TApp e' : τ.[τ'/].
361
  Proof.
362
    iIntros "IH".
363
    rel_bind_ap e e' "IH" v v' "IH".
364
    iSpecialize ("IH" $! (interp  τ' Δ)).
365 366
    iApply (related_ret ).
    iApply (interp_expr_subst Δ τ τ' (TApp v, TApp v')  with "IH").
367 368
  Qed.

369
  Lemma bin_log_related_tapp (τi : D) Δ Γ e e' τ :
370 371
    {Δ;Γ}  e log e' : TForall τ -
    {τi::Δ;⤉Γ}  TApp e log TApp e' : τ.
372 373
  Proof.
    rewrite bin_log_related_eq.
374
    iIntros "IH".
375 376 377 378 379 380 381 382
    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]".
383
    iMod ("IH" $! τi with "Hj"); auto.
384 385 386
  Qed.

  Lemma bin_log_related_fold Δ Γ e e' τ :
387 388
    {Δ;Γ}  e log e' : τ.[(TRec τ)/] -
    {Δ;Γ}  Fold e log Fold e' : TRec τ.
389
  Proof.
390
    iIntros "IH".
391 392
    rel_bind_ap e e' "IH" v v' "IH".
    value_case.
393
    rewrite fixpoint_unfold /= -interp_subst.
394
    iExists (_, _); eauto.
395 396
  Qed.

397
  Lemma bin_log_related_unfold Δ Γ e e' τ :
398 399
    {Δ;Γ}  e log e' : TRec τ -
    {Δ;Γ}  Unfold e log Unfold e' : τ.[(TRec τ)/].
400
  Proof.
401
    iIntros "IH".
402
    rel_bind_ap e e' "IH" v v' "IH".
403
    rewrite /= fixpoint_unfold /=.
404
    change (fixpoint _) with (interp  (TRec τ) Δ).
405
    iDestruct "IH" as ([w w']) "#[% Hiz]"; simplify_eq/=.
406 407 408
    rel_unfold_l.
    rel_unfold_r.
    value_case. by rewrite -interp_subst.
409 410
  Qed.

411
  Lemma bin_log_related_pack' Δ Γ e e' τ τ' :
412 413
    {Δ;Γ}  e log e' : τ.[τ'/] -
    {Δ;Γ}  Pack e log Pack e' : TExists τ.
414
  Proof.
415
    iIntros "IH".
416 417
    rel_bind_ap e e' "IH" v v' "#IH".
    value_case.
418
    iExists (v, v'). iModIntro. simpl; iSplit; eauto.
419
    iExists ( τ'  Δ).    
420
    by rewrite interp_subst.
421 422
  Qed.

423
  Lemma bin_log_related_pack (τi : D) Δ Γ e e' τ :
424 425
    {τi::Δ;⤉Γ}  e log e' : τ -
    {Δ;Γ}  Pack e log Pack e' : TExists τ.
426 427
  Proof.
    rewrite bin_log_related_eq.
428
    iIntros "IH".
429 430 431 432 433 434 435 436
    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]".
437
    iApply wp_value.
438 439 440 441
    iExists (PackV v'). simpl. iFrame.
    iExists (v, v'). simpl; iSplit; eauto.
  Qed.

442 443
  Lemma bin_log_related_unpack Δ Γ e1 e1' e2 e2' τ τ2 :
    {Δ;Γ}  e1 log e1' : TExists τ -
444
    ( τi : D,
445
      {τi::Δ;⤉Γ} 
446
        e2 log e2' : TArrow τ (asubst (ren (+1)) τ2)) -
447
    {Δ;Γ}  Unpack e1 e2 log Unpack e1' e2' : τ2.
448
  Proof.
449
    rewrite bin_log_related_eq.
450
    iIntros "IH1 IH2".
451
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
452
    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
453
    iDestruct "IH1" as ([w w']) "[% #Hτi]"; simplify_eq/=.
454
    iDestruct "Hτi" as (τi) "#Hτi"; simplify_eq/=.
455
    wp_unpack.
456
    iApply fupd_wp.
457
    tp_pack j; eauto. iModIntro.
458
    iSpecialize ("IH2" $! τi with "Hs [HΓ]"); auto.
459
    { by rewrite interp_env_ren. }
460 461 462
    tp_bind j (env_subst (snd <$> vvs) e2').
    iMod ("IH2" with "Hj") as "IH2". simpl.
    wp_bind (env_subst (fst <$> vvs) e2).
463
    iApply (wp_wand with "IH2").
464 465
    iIntros (v). iDestruct 1 as (v') "[Hj #Hvv']".
    iSpecialize ("Hvv'" $! (w,w') with "Hτi Hj"). simpl.
466
    iMod "Hvv'".
467
    iApply (wp_wand with "Hvv'"). clear v v'.
468
    iIntros (v). iDestruct 1 as (v') "[Hj #Hvv']".
469
    rewrite (interp_weaken [] [τi] Δ _ τ2) /=.
470
    eauto.
471
  Qed.
472

473
  Lemma bin_log_related_fork Δ Γ e e' :
474 475
    {Δ;Γ}  e log e' : TUnit -
    {Δ;Γ}  Fork e log Fork e' : TUnit.
476
  Proof.
477
    rewrite bin_log_related_eq.
478
    iIntros "IH".
479
    iIntros (vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
480 481
    tp_fork j as i "Hi". fold subst_p.  iModIntro.
    iApply wp_fork. fold subst_p. iNext. iSplitL "Hj".
482
    - iExists #(); eauto.
483
    - iSpecialize ("IH" with "Hs HΓ").
484
      iSpecialize ("IH" $! i []). simpl.
485
      iSpecialize ("IH" with "Hi").
486
      iMod "IH". iApply (wp_wand with "IH"). eauto.
487 488
  Qed.

489
  Lemma bin_log_related_alloc Δ Γ e e' τ :
490 491
    {Δ;Γ}  e log e' : τ -
    {Δ;Γ}  Alloc e log Alloc e' : Tref τ.
492
  Proof.
493
    iIntros "IH".
494
    rel_bind_ap e e' "IH" v v' "IH".
495 496
    rel_alloc_l as l "Hl".
    rel_alloc_r as k "Hk".
497
    iMod (inv_alloc (logN .@ (l,k)) _ ( w : val * val,
498
      l ↦ᵢ w.1  k ↦ₛ w.2  interp _ τ Δ w)%I with "[Hl Hk IH]") as "HN"; eauto.
499
    { iNext. iExists (v, v'); simpl; iFrame. }
500 501
    rel_vals.
    iExists (l, k). eauto.
502 503
  Qed.

504
  Lemma bin_log_related_load Δ Γ e e' τ :
505 506
    {Δ;Γ}  e log e' : (Tref τ) -
    {Δ;Γ}  Load e log Load e' : τ.
507
  Proof.
508
    iIntros "IH".
509 510
    rel_bind_ap e e' "IH" v v' "IH".
    iDestruct "IH" as ([l l']) "[% Hinv]"; simplify_eq/=.
511
    rel_load_l_atomic.
512
    iInv (logN .@ (l,l')) as ([w w']) "[Hw1 [>Hw2 #Hw]]" "Hclose"; simpl.
513
    iModIntro. iExists _; iFrame "Hw1".
514
    iNext. iIntros "Hw1".
515
    rel_load_r.
516
    iMod ("Hclose" with "[Hw1 Hw2]").
517
    { iNext. iExists (w,w'); by iFrame. }
518
    rel_vals; eauto.
519 520
  Qed.

521
  Lemma bin_log_related_store Δ Γ e1 e2 e1' e2' τ :
522 523 524
    {Δ;Γ}  e1 log e1' : (Tref τ) -
    {Δ;Γ}  e2 log e2' : τ -
    {Δ;Γ}  Store e1 e2 log Store e1' e2' : TUnit.
525
  Proof.
526
    iIntros "IH1 IH2".
527 528 529
    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".
530
    rel_store_l_atomic.
531
    iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
532 533 534 535
    iModIntro. iExists _; iFrame "Hv1".
    iNext. iIntros "Hw1".
    rel_store_r.
    iMod ("Hclose" with "[Hw1 Hv2 IH2]").
536
    { iNext; iExists (_, _); simpl; iFrame. }
537
    by rel_vals.
538 539
  Qed.

540
  Lemma bin_log_related_CAS Δ Γ e1 e2 e3 e1' e2' e3' τ
541
    (HEqτ : EqType τ) :
542 543 544 545
    {Δ;Γ}  e1 log e1' : Tref τ -
    {Δ;Γ}  e2 log e2' : τ -
    {Δ;Γ}  e3 log e3' : τ -
    {Δ;Γ}  CAS e1 e2 e3 log CAS e1' e2' e3' : TBool.
546
  Proof.
547
    iIntros "IH1 IH2 IH3".
548 549 550
    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".
551
    iDestruct "IH1" as ([l l']) "[% Hinv]"; simplify_eq/=.
552
    rel_cas_l_atomic.
553
    iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
554
    iPoseProof ("Hv") as "Hv' /=".
555
    rewrite {2}[interp _ τ Δ (v, v')]interp_EqType_agree; trivial.
556
    iMod "Hv'" as %Hv'; subst.
557 558 559 560
    iModIntro. iExists _; iFrame. simpl.
    destruct (decide (v' = v2)) as [|Hneq]; subst.
    - iSplitR; first by (iIntros (?); contradiction).
      iIntros (?). iNext. iIntros "Hv1".
561
      iAssert (v2 = v2'⌝)%I with "[IH2]" as %->.
562 563 564
      { rewrite ?interp_EqType_agree; trivial. }
      rel_cas_suc_r.
      iMod ("Hclose" with "[-]").
565
      { iNext; iExists (_, _); by iFrame. }
566 567 568
      rel_vals; eauto.
    - iSplitL; last by (iIntros (?); congruence).
      iIntros (?). iNext. iIntros "Hv1".
569
      iAssert (v'  v2'⌝)%I as "%".
570
      { rewrite ?interp_EqType_agree; trivial. iSimplifyEq. auto. }
571 572
      rel_cas_fail_r.
      iMod ("Hclose" with "[-]").
573
      { iNext; iExists (_, _); by iFrame. }
574
      rel_vals; eauto.
575 576
  Qed.

577 578
  Theorem binary_fundamental Δ Γ e τ :
    Γ ⊢ₜ e : τ  ({Δ;Γ}  e log e : τ)%I.
579
  Proof.
580
    intros Ht. iInduction Ht as [] "IH" forall (Δ).
581 582 583 584 585
    - 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
586
    - by iApply (bin_log_related_bool_binop with "[]").
587
    - by iApply bin_log_related_ref_binop.
588 589 590 591 592
    - 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.
593
    - by iApply (bin_log_related_case with "[] []").
594
    - by iApply (bin_log_related_if with "[] []").
595 596 597
    - assert (Closed (x :b: f :b: dom (gset string) Γ) e).
      { apply typed_X_closed in Ht.
        rewrite !dom_insert_binder in Ht.
598
        revert Ht. destruct x,f; cbn-[union];
599 600 601 602
        (* TODO: why is simple rewriting is not sufficient here? *)
        erewrite ?(left_id ); eauto.
        all: apply _. }
      iApply (bin_log_related_rec with "[]"); eauto.
603
    - by iApply (bin_log_related_app with "[] []").
604
    - assert (Closed (dom _ Γ) e).
605
      { apply typed_X_closed in Ht.
606
        pose (K:=(dom_fmap (asubst (ren (+1))) Γ (D:=stringset))).
607 608
        fold_leibniz. by rewrite -K. }
      iApply bin_log_related_tlam; eauto.
609
    - by iApply bin_log_related_tapp'.
610 611
    - by iApply bin_log_related_fold.
    - by iApply bin_log_related_unfold.
612 613
    - by iApply bin_log_related_pack'.
    - iApply (bin_log_related_unpack with "[]"); eauto.
614 615 616 617 618
    - 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 "[] []").
619
  Qed.
620

621
End fundamental.