fundamental_unary.v 7.12 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4
From iris_logrel.F_mu_ref_par Require Export logrel_unary.
From iris_logrel.F_mu_ref_par Require Import rules.
From iris.algebra Require Export upred_big_op.
From iris.proofmode Require Import tactics pviewshifts invariants.
5 6

Section typed_interp.
7
  Context {Σ : gFunctors} `{i : heapIG Σ} {L : namespace}.
8 9 10 11
  Implicit Types P Q R : iPropG lang Σ.

  Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
    iApply (@wp_bind _ _ _ [ctx]);
12 13
    iApply wp_wand_l;
    iSplitL; [| iApply Hp; trivial]; [iIntros {v} Hv|iSplit; trivial]; cbn.
14 15 16

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

Robbert Krebbers's avatar
Robbert Krebbers committed
17
  Lemma typed_interp N (Δ : varC -n> valC -n> iPropG lang Σ) Γ vs e τ
Robbert Krebbers's avatar
Robbert Krebbers committed
18
      (HNLdisj : N  L) (HΔ :  x v, PersistentP (Δ x v)) :
19
    Γ ⊢ₜ e : τ 
Robbert Krebbers's avatar
Robbert Krebbers committed
20
    length Γ = length vs 
21 22
    heapI_ctx N  [] zip_with (λ τ, interp L τ Δ) Γ vs
     WP e.[env_subst vs] {{ interp L τ Δ }}.
23
  Proof.
24 25
    intros Htyped; revert Δ HΔ vs.
    induction Htyped; iIntros {Δ HΔ vs Hlen} "#[Hheap HΓ] /=".
26 27 28 29 30 31 32 33
    - (* var *)
      destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
      { by rewrite -Hlen; apply lookup_lt_Some with τ. }
      rewrite /env_subst Hv; value_case.
      iApply (big_and_elem_of with "HΓ").
      apply elem_of_list_lookup_2 with x.
      rewrite lookup_zip_with; simplify_option_eq; trivial.
    - (* unit *) value_case; trivial.
34 35 36
    - (* nat *) value_case; iExists _ ; trivial.
    - (* bool *) value_case; iExists _ ; trivial.
    - (* nat bin op *)
37 38
      smart_wp_bind (BinOpLCtx _ e2.[env_subst vs]) v "#Hv" IHHtyped1.
      smart_wp_bind (BinOpRCtx _ v) v' "# Hv'" IHHtyped2.
39
      iDestruct "Hv" as {n} "%"; iDestruct "Hv'" as {n'} "%"; subst. simpl.
40
      iApply wp_nat_bin_op. iNext; iPvsIntro; destruct op; simpl;
41
      try destruct eq_nat_dec; try destruct le_dec; try destruct lt_dec;
42
        eauto 10.
43 44 45
    - (* pair *)
      smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHHtyped1.
      smart_wp_bind (PairRCtx v) v' "# Hv'" IHHtyped2.
46 47
      value_case; eauto.
   - (* fst *)
48
      smart_wp_bind (FstCtx) v "# Hv" IHHtyped; cbn.
49 50
      iDestruct "Hv" as {w1 w2} "#[% [H2 H3]]"; subst.
      iApply wp_fst; eauto using to_of_val.
51 52
    - (* snd *)
      smart_wp_bind (SndCtx) v "# Hv" IHHtyped; cbn.
53 54
      iDestruct "Hv" as {w1 w2} "#[% [H2 H3]]"; subst.
      iApply wp_snd; eauto using to_of_val.
55 56
    - (* injl *)
      smart_wp_bind (InjLCtx) v "# Hv" IHHtyped; cbn.
57
      value_case; eauto.
58 59
    - (* injr *)
      smart_wp_bind (InjRCtx) v "# Hv" IHHtyped; cbn.
60
      value_case; eauto.
61 62
    - (* case *)
      smart_wp_bind (CaseCtx _ _) v "#Hv" IHHtyped1; cbn.
63 64 65 66 67 68 69 70 71
      iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as {w} "[% Hw]"; subst.
      + iApply wp_case_inl; auto 1 using to_of_val; asimpl.
        specialize (IHHtyped2 Δ HΔ (w::vs)).
        erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto).
        iNext; iApply IHHtyped2; cbn; auto.
      + iApply wp_case_inr; auto 1 using to_of_val; asimpl.
        specialize (IHHtyped3 Δ HΔ (w::vs)).
        erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto).
        iNext; iApply IHHtyped3; cbn; auto.
72 73
    - (* If *)
      smart_wp_bind (IfCtx _ _) v "#Hv" IHHtyped1; cbn.
74
      iDestruct "Hv" as { [] } "%"; subst; simpl;
75
        [iApply wp_if_true| iApply wp_if_false]; iNext;
76
      [iApply IHHtyped2| iApply IHHtyped3]; auto.
77
    - (* lam *)
78
      value_case; iAlways; iLöb as "Hlat"; iIntros {w} "#Hw".
79
      iApply wp_lam; auto 1 using to_of_val.
80 81 82
      asimpl. change (Lam _) with (# (LamV e.[upn 2 (env_subst vs)])).
      erewrite typed_subst_head_simpl_2; [|eauto|cbn]; eauto.
      iNext; iApply (IHHtyped Δ HΔ (_ :: w :: vs)); cbn; auto.
83 84 85
    - (* app *)
      smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1.
      smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
86
      iApply wp_mono; [|iApply "Hv"]; auto.
87
    - (* TLam *)
88
      value_case. iIntros {τi} "! /= %". iApply wp_TLam; iNext.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
      iApply (IHHtyped (extend_context_interp_fun1 τi Δ)); [rewrite map_length|]; trivial.
90
      iSplit; trivial.
91
      rewrite zip_with_context_interp_subst; trivial.
92 93
    - (* TApp *)
      smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
94 95
      iApply wp_wand_r; iSplitL; [iApply ("Hv" $! (interp L τ' Δ)); iPureIntro; apply _|]; cbn.
      iIntros {w} "?". by rewrite -interp_subst; simpl.
96
    - (* Fold *)
97
      specialize (IHHtyped Δ HΔ vs Hlen).
98
      iApply (@wp_bind _ _ _ [FoldCtx]).
99 100 101 102
        iApply wp_wand_l.
        iSplitL; [|iApply IHHtyped; auto].
      iIntros {v} "#Hv".
      value_case.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
      rewrite -interp_subst.
104 105
      rewrite fixpoint_unfold; cbn.
      iAlways; eauto.
106 107
    - (* Unfold *)
      iApply (@wp_bind _ _ _ [UnfoldCtx]);
108
        iApply wp_wand_l; iSplitL; [|iApply IHHtyped; auto].
109 110 111 112
      iIntros {v}.
      cbn [interp interp_rec cofe_mor_car].
      rewrite fixpoint_unfold.
      iIntros "#Hv"; cbn.
113
      change (fixpoint _) with (interp L (TRec τ) Δ).
114 115
      iDestruct "Hv" as {w} "[% #Hw]"; rewrite H.
      iApply wp_Fold; cbn; auto using to_of_val.
116
      rewrite -interp_subst; auto.
117 118 119
    - (* Fork *)
      iApply wp_fork.
      iNext; iSplitL; trivial.
120 121
      iApply wp_wand_l.
      iSplitL; [|iApply IHHtyped; auto]; auto.
122 123 124 125 126 127
    - (* Alloc *)
      smart_wp_bind AllocCtx v "#Hv" IHHtyped; cbn. iClear "HΓ".
      iApply wp_atomic; cbn; trivial; [rewrite to_of_val; auto|].
      iPvsIntro.
      iApply wp_alloc; auto 1 using to_of_val.
      iFrame "Hheap". iNext.
128
      iIntros {l} "Hl". iPvsIntro.
129
      iPvs (inv_alloc _ with "[Hl]") as "HN";
130
        [| | iPvsIntro; iExists _; iSplit; trivial]; eauto.
131 132
    - (* Load *)
      smart_wp_bind LoadCtx v "#Hv" IHHtyped; cbn. iClear "HΓ".
133
      iDestruct "Hv" as {l} "[% #Hv]"; subst.
134 135 136
      iApply wp_atomic; cbn; eauto using to_of_val.
      iPvsIntro.
      iInv (L .@ l) as {w} "[Hw1 #Hw2]".
Robbert Krebbers's avatar
Robbert Krebbers committed
137 138
      iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial. solve_ndisj.
      iIntros "{$Hw1} > Hw1". iPvsIntro; iSplitL; eauto.
139 140 141
    - (* Store *)
      smart_wp_bind (StoreLCtx _) v "#Hv" IHHtyped1; cbn.
      smart_wp_bind (StoreRCtx _) w "#Hw" IHHtyped2; cbn. iClear "HΓ".
142
      iDestruct "Hv" as {l} "[% #Hv]"; subst.
143 144 145 146
      iApply wp_atomic; cbn; [trivial| rewrite ?to_of_val; auto |].
      iPvsIntro.
      iInv (L .@ l) as {z} "[Hz1 #Hz2]".
      eapply bool_decide_spec; eauto using to_of_val.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
      iApply (wp_store N); auto using to_of_val. solve_ndisj.
148
      iIntros "{$Hheap $Hz1} > Hz1". iPvsIntro. iSplitL; eauto 10.
149 150 151 152 153 154 155 156 157
    - (* CAS *)
      smart_wp_bind (CasLCtx _ _) v1 "#Hv1" IHHtyped1; cbn.
      smart_wp_bind (CasMCtx _ _) v2 "#Hv2" IHHtyped2; cbn.
      smart_wp_bind (CasRCtx _ _) v3 "#Hv3" IHHtyped3; cbn. iClear "HΓ".
      iDestruct "Hv1" as {l} "[% Hinv]"; subst.
      iApply wp_atomic; cbn; eauto 10 using to_of_val.
      iPvsIntro.
      iInv (L .@ l) as {w} "[Hw1 #Hw2]"; [cbn; eauto 10 using to_of_val|].
      destruct (val_dec_eq v2 w) as [|Hneq]; subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
      + iApply (wp_cas_suc N); eauto using to_of_val. solve_ndisj.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
        iIntros "{$Hheap $Hw1} > Hw1"; iPvsIntro.
160
        iSplitL; [|iPvsIntro]; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
      + iApply (wp_cas_fail N); eauto using to_of_val. solve_ndisj.
162
        iIntros "{$Hheap $Hw1} > Hw1". iPvsIntro. iSplitL; eauto.
163
  Qed.
164
End typed_interp.