fundamental.v 8.06 KB
Newer Older
1 2 3
Require Import iris.program_logic.hoare.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
4 5
Require Import iris_logrel.F_mu_ref.lang iris_logrel.F_mu_ref.typing
        iris_logrel.F_mu_ref.rules iris_logrel.F_mu_ref.logrel.
6 7 8 9
From iris.program_logic Require Export lifting.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth.
10
Require Import iris.proofmode.tactics iris.proofmode.invariants.
11 12 13
Import uPred.

Section typed_interp.
14 15
  Context {Σ : gFunctors} `{i : heapG Σ} `{L : namespace}.

16 17 18
  Implicit Types P Q R : iPropG lang Σ.
  Notation "# v" := (of_val v) (at level 20).

19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
  Local Hint Extern 1 =>
  match goal with
    |-
    (_
       --------------------------------------
        _ : ?A, _) => let W := fresh "W" in evar (W : A); iExists W; unfold W; clear W
  end : itauto.

  Local Hint Extern 1 =>
  match goal with
    |-
    (_
       --------------------------------------
        _) => iNext
  end : itauto.

35 36 37 38 39 40 41 42
  Local Hint Extern 1 =>
  match goal with
    |-
    (_
       --------------------------------------
        _) => eapply (@always_intro _ _ _ _)
  end : itauto.

43 44 45 46 47 48 49
  Local Hint Extern 1 =>
  match goal with
    |-
    (_
       --------------------------------------
       (_  _)) => iSplit
  end : itauto.
50

51 52 53 54 55
  Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
    iApply (@wp_bind _ _ _ [ctx]);
    iApply wp_impl_l;
    iSplit; [| iApply Hp; trivial];
    [apply (always_intro _ _); iIntros {v} Hv|iSplit; trivial]; cbn.
56 57

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

  Lemma later_exist_turnstile (M : cmraT) (A : Type) :
    Inhabited A   Φ : A  uPred M, ( ( a : A, Φ a))%I  ( a : A,  Φ a)%I.
  Proof. intros H Φ. rewrite later_exist; trivial. Qed.
62

63
  Lemma typed_interp N Δ Γ vs e τ
64
        (HNLdisj :  l : loc, N  L .@ l)
65 66
        (Htyped : typed Γ e τ)
        (HΔ : context_interp_Persistent Δ)
67
    : List.length Γ = List.length vs 
68 69
      (heap_ctx N  Π∧ zip_with (λ τ v, (@interp Σ i L) τ Δ v) Γ vs)%I 
                  WP (e.[env_subst vs]) @  {{ λ v, (@interp Σ i L) τ Δ v }}.
70
  Proof.
71 72
    revert Δ HΔ vs.
    induction Htyped; intros Δ HΔ vs Hlen; iIntros "#[Hheap HΓ]"; cbn.
73 74 75
    - (* var *)
      destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
      { by rewrite -Hlen; apply lookup_lt_Some with τ. }
76
      rewrite /env_subst Hv; value_case.
77
      iApply (big_and_elem_of with "HΓ").
78
      apply elem_of_list_lookup_2 with x.
79
      rewrite lookup_zip_with; simplify_option_eq; trivial.
80
    - (* unit *) value_case; trivial.
81
    - (* pair *)
82 83
      smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHHtyped1.
      smart_wp_bind (PairRCtx v) v' "# Hv'" IHHtyped2.
84 85
      value_case; eauto 10 with itauto.
    - (* fst *)
86 87 88
      smart_wp_bind (FstCtx) v "# Hv" IHHtyped; cbn.
      iApply double_exists; [|trivial].
      intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H; cbn.
89
      iApply wp_fst; try iNext; eauto using to_of_val; cbn.
90
    - (* snd *)
91 92 93
      smart_wp_bind (SndCtx) v "# Hv" IHHtyped; cbn.
      iApply double_exists; [|trivial].
      intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H; cbn.
94
      iApply wp_snd; try iNext; eauto using to_of_val; cbn.
95 96 97 98 99 100
    - (* injl *)
      smart_wp_bind (InjLCtx) v "# Hv" IHHtyped; cbn.
      value_case; iLeft; auto with itauto.
    - (* injr *)
      smart_wp_bind (InjRCtx) v "# Hv" IHHtyped; cbn.
      value_case; iRight; auto with itauto.
101
    - (* case *)
102
      smart_wp_bind (CaseCtx _ _) v "#Hv" IHHtyped1; cbn.
103 104 105 106 107 108 109 110 111
      iDestruct "Hv" as "[Hv|Hv]";
      iDestruct "Hv" as {w} "[% Hw]"; rewrite H;
        [iApply wp_case_inl|iApply wp_case_inr];
        auto 1 using to_of_val;
        asimpl;
        [specialize (IHHtyped2 Δ HΔ (w::vs)) |
         specialize (IHHtyped3 Δ HΔ (w::vs))];
        erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto); iNext;
          [iApply IHHtyped2 | iApply IHHtyped3]; cbn; auto with itauto.
112
    - (* lam *)
113 114 115
      value_case; apply (always_intro _ _); iIntros {w} "#Hw".
      iApply wp_lam; auto 1 using to_of_val.
      asimpl; erewrite typed_subst_head_simpl; [|eauto|cbn]; eauto.
116
      iNext; iApply (IHHtyped Δ HΔ (w :: vs)); cbn; auto with itauto.
117
    - (* app *)
118 119
      smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1.
      smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
120
      iApply wp_mono; [|iApply "Hv"]; auto with itauto.
121
    - (* TLam *)
122 123 124
      value_case; iApply exist_intro; iSplit; trivial.
      iIntros {τi}; destruct τi as [τi τiPr].
      iRevert "Hheap".
125
      iPoseProof (always_intro with "HΓ") as "HP"; try typeclasses eauto;
126
        try (iApply always_impl; iExact "HP").
127
      iIntros "#HΓ #Hheap".
128 129
      iApply IHHtyped; [rewrite map_length|]; trivial.
      iSplit; trivial.
130 131
      iRevert "Hheap HΓ". rewrite zip_with_context_interp_subst.
      iIntros "#Hheap #HΓ"; trivial.
132
    - (* TApp *)
133
      smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
134
      iDestruct "Hv" as {e'} "[% He']"; rewrite H.
135
      iApply wp_TLam.
136
      iSpecialize ("He'" $! ((interp τ' Δ)  _)); cbn.
137 138 139
      iApply always_elim. iApply always_mono; [|trivial].
      iIntros "He'"; iNext.
      iApply wp_mono; [|trivial].
140
      iIntros {w} "#H". rewrite -interp_subst; trivial.
141 142
    - (* Fold *)
      rewrite map_length in IHHtyped.
143 144
      iApply (@wp_bind _ _ _ [FoldCtx]).
        iApply wp_impl_l.
145
        iSplit; [eapply (@always_intro _ _ _ _)|
146 147
                 iApply (IHHtyped (extend_context_interp ((interp (TRec τ)) Δ) Δ));
                 trivial].
148
      + iIntros {v} "#Hv".
149 150 151 152 153
        value_case.
        rewrite fixpoint_unfold; cbn.
        auto with itauto.
      + iRevert "Hheap HΓ"; rewrite zip_with_context_interp_subst;
          iIntros "#Hheap #HΓ"; auto with itauto.
154
    - (* Unfold *)
155 156 157
      iApply (@wp_bind _ _ _ [UnfoldCtx]);
        iApply wp_impl_l;
        iSplit; [eapply (@always_intro _ _ _ _)|
158 159
                 iApply IHHtyped;
                 auto with itauto].
160
      iIntros {v}.
161 162 163 164 165
      cbn [interp interp_rec cofe_mor_car].
      rewrite fixpoint_unfold.
      iIntros "#Hv"; cbn.
      change (fixpoint _) with (@interp _ _ L (TRec τ) Δ).
      iDestruct "Hv" as {w} "[% #Hw]"; rewrite H.
166
      iApply wp_Fold; cbn; auto using to_of_val.
167
      rewrite -interp_subst; auto with itauto.
168
    - (* Alloc *)
169 170
      smart_wp_bind AllocCtx v "#Hv" IHHtyped; cbn. iClear "HΓ".
      iApply wp_atomic; cbn; trivial; [rewrite to_of_val; auto|].
171 172 173
      iPvsIntro.
      iApply wp_alloc; auto 1 using to_of_val.
      iFrame "Hheap". iNext.
174
      iIntros {l} "Hl".
175 176 177 178
      iPvs (inv_alloc _ with "[Hl]") as "HN";
        [| | iPvsIntro; iExists _; iSplit; trivial].
      trivial.
      iNext; iExists _; iFrame "Hl"; trivial.
179
    - (* Load *)
180 181 182 183
      smart_wp_bind LoadCtx v "#Hv" IHHtyped; cbn. iClear "HΓ".
      iRevert "Hheap". iApply exist_elim; [|iExact "Hv"].
      iIntros {l} "[% #Hv] #Hheap"; rewrite H.
      iApply wp_atomic; cbn; eauto using to_of_val.
184 185 186
      iPvsIntro.
      iInv (L .@ l) as {w} "[Hw1 #Hw2]".
      iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial.
187
      specialize (HNLdisj l); set_solver_ndisj.
188 189 190
      iFrame "Hw1". iNext.
      iIntros "Hw1". iSplitL; trivial.
      iNext; iExists _. iFrame "Hw1"; trivial.
191
    - (* Store *)
192 193 194 195 196
      smart_wp_bind (StoreLCtx _) v "#Hv" IHHtyped1; cbn.
      smart_wp_bind (StoreRCtx _) w "#Hw" IHHtyped2; cbn. iClear "HΓ".
      iRevert "Hheap Hw". iApply exist_elim; [|iExact "Hv"].
      iIntros {l} "#[% Hl] #Hheap #Hw"; rewrite H.
      iApply wp_atomic; cbn; [trivial| rewrite ?to_of_val; auto |].
197 198 199 200
      iPvsIntro.
      iInv (L .@ l) as {z} "[Hz1 #Hz2]".
      eapply bool_decide_spec; eauto using to_of_val.
      iApply (wp_store N); auto using to_of_val.
201
      specialize (HNLdisj l); set_solver_ndisj.
202 203 204 205 206
      iFrame "Hheap Hz1".
      iNext.
      iIntros "Hz1".
      iSplitL; [|iPvsIntro; trivial].
      iNext; iExists _. iFrame "Hz1"; trivial.
207 208
      (* unshelving *)
      Unshelve.
209
      cbn; typeclasses eauto.
210
  Qed.
211

212
End typed_interp.