fundamental.v 11.7 KB
Newer Older
1 2 3 4 5 6 7 8
Require Import iris.program_logic.hoare.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import F_mu_ref.lang F_mu_ref.typing F_mu_ref.rules F_mu_ref.logrel.
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.
Amin Timany's avatar
Amin Timany committed
9
Require Import prelude.Vlist.
10 11 12 13 14 15 16 17 18 19 20
Import uPred.

Section typed_interp.
  Context
    {Σ : gFunctors}
    `{i : heapG Σ}
    `{L : namespace}.
  
  Implicit Types P Q R : iPropG lang Σ.
  Notation "# v" := (of_val v) (at level 20).

21
  (*
22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
  Local Ltac ipropsimpl :=
    repeat
      match goal with
      | [|- (_  (_  _))%I] => eapply and_intro
      | [|- ( _   _)%I] => apply later_mono
      | [|- (_   _, _)%I] => rewrite -exist_intro
      | [|- (( _, _)  _)%I] => let v := fresh "v" in rewrite exist_elim; [|intros v]
      end.

  Local Hint Extern 1 => progress ipropsimpl.

  Local Tactic Notation "smart_wp_bind" uconstr(ctx) uconstr(t) ident(v) :=
    rewrite -(@wp_bind _ _ _ [ctx]) /= -wp_impl_l; apply and_intro; [
    apply (@always_intro _ _ _ t), forall_intro=> v /=; apply impl_intro_l| eauto with itauto].

  Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) :=
    rewrite -(@wp_bind _ _ _ [ctx]) /= -wp_mono; eauto; intros v; cbn.

  Create HintDb itauto.

  Local Hint Extern 3 ((_  _)  _)%I => rewrite and_elim_r : itauto.
  Local Hint Extern 3 ((_  _)  _)%I => rewrite and_elim_l : itauto.
  Local Hint Extern 3 (_  (_  _))%I => rewrite -or_intro_l : itauto.
  Local Hint Extern 3 (_  (_  _))%I => rewrite -or_intro_r : itauto.
  Local Hint Extern 2 (_   _)%I => etransitivity; [|rewrite -later_intro] : itauto.
  
  Local Ltac value_case := rewrite -wp_value/= ?to_of_val //; auto 2.
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86
*)

  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.

  Local Hint Extern 1 =>
  match goal with
    |-
    (_
       --------------------------------------
       (_  _)) => iSplit
  end : itauto.
  
  
  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.
              
  Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.

  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.
87 88 89 90 91 92 93

  Lemma typed_interp N k Δ Γ vs e τ
        (HNLdisj :  l : loc, N  L .@ l)
        (Htyped : typed k Γ e τ)
        (Hctx : closed_ctx k Γ)
        (HC : closed_type k τ)
        (HΔ : VlistAlwaysStable Δ)
94
    : List.length Γ = List.length vs 
95 96 97 98
      (heap_ctx N  Π∧ zip_with (λ τ v, (@interp Σ i L) k (` τ) (proj2_sig τ) Δ v) (closed_ctx_list _ Γ Hctx) vs)%I 
                  WP (e.[env_subst vs]) @  {{ λ v, (@interp Σ i L) k τ HC Δ v }}.
  Proof.
    revert Hctx HC HΔ vs.
99
    induction Htyped; intros Hctx HC HΔ vs Hlen; iIntros "#[Hheap HΓ]"; cbn.
100 101 102
    - (* var *)
      destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
      { by rewrite -Hlen; apply lookup_lt_Some with τ. }
103
      rewrite /env_subst Hv; value_case.
104
      edestruct (zipwith_Forall_lookup _ Hctx) as [Hτ' Hτ'eq]; eauto.
105 106 107
      iApply interp_closed_irrel_turnstile.
      iApply big_and_elem_of "HΓ"; eauto.
      apply elem_of_list_lookup_2 with x.
108 109 110
      rewrite lookup_zip_with; simplify_option_eq; trivial.
    - (* unit *) value_case.
    - (* pair *)
111 112
      smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHHtyped1.
      smart_wp_bind (PairRCtx v) v' "# Hv'" IHHtyped2.
113 114
      value_case; eauto 10 with itauto.
    - (* fst *)
115 116 117 118 119
      smart_wp_bind (FstCtx) v "# Hv" IHHtyped; cbn.
      iApply double_exists; [|trivial].
      intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H; cbn.
      iApply wp_fst; eauto using to_of_val; cbn.
      iNext; iApply interp_closed_irrel_turnstile; trivial.
120
    - (* snd *)
121 122 123 124 125 126 127 128 129 130 131
      smart_wp_bind (SndCtx) v "# Hv" IHHtyped; cbn.
      iApply double_exists; [|trivial].
      intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H; cbn.
      iApply wp_snd; eauto using to_of_val; cbn.
      iNext; iApply interp_closed_irrel_turnstile; trivial.
    - (* 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.
132
    - (* case *)
133 134 135 136 137 138 139 140 141 142 143 144 145
      smart_wp_bind (CaseCtx _ _) v "#Hv" IHHtyped1; cbn.
      iDestruct "Hv" as "[Hv|Hv]"; eauto; iRevert "HΓ"; iRevert "Hheap";
        iApply exist_elim; eauto; cbn;
          iIntros {w} "#[% Hw2] #HΓ #Hheap"; rewrite H; cbn;
            [iApply wp_case_inl|iApply wp_case_inr];
            auto 1 using to_of_val;
            asimpl;
            [specialize (IHHtyped2 Δ (typed_closed_ctx _ _ _ _ Htyped2) HC HΔ (w::vs)) |
             specialize (IHHtyped3 Δ (typed_closed_ctx _ _ _ _ Htyped3) HC HΔ (w::vs))];
              erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto); iNext;
                [iApply IHHtyped2 | iApply IHHtyped3]; cbn; auto;
                  (iSplit; [trivial|iSplit]; [iApply interp_closed_irrel_turnstile|
                            iApply type_context_closed_irrel_turnstile]; trivial).
146
    - (* lam *)
147 148 149 150 151 152 153
      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.
      iNext; iApply (IHHtyped Δ (typed_closed_ctx _ _ _ _ Htyped) (closed_type_arrow_2 HC)
                              HΔ (w :: vs)); cbn; auto.
      (iSplit; [trivial|iSplit]; [iApply interp_closed_irrel_turnstile|
                iApply type_context_closed_irrel_turnstile]; trivial).
154
    - (* app *)
155 156 157 158
      smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1.
      smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
      iApply wp_mono; [|iApply "Hv"; auto with itauto].
      intros; apply interp_closed_irrel_turnstile.
159
    - (* TLam *)
160 161 162 163 164 165 166 167 168
      value_case; iApply exist_intro; iSplit; trivial.
      iIntros {τi}; destruct τi as [τi τiPr].
      iRevert "Hheap".
      iPoseProof always_intro "HΓ" as "HP"; try typeclasses eauto;
        try (iApply always_impl; iExact "HP").
      iIntros "#HΓ #Hheap"; iNext.
      iApply IHHtyped; [rewrite map_length|]; trivial.
      iSplit; trivial.
      iRevert "HΓ". rewrite zip_with_closed_ctx_list_subst. iIntros "#HΓ"; trivial.
169
    - (* TApp *)
170 171 172 173 174 175 176 177 178
      smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
      iApply exist_elim; [|iExact "Hv"]; cbn.
      iIntros {e'} "[% #He']"; rewrite H0.
      iApply wp_TLam.
      iSpecialize "He'" {((interp k τ' H Δ)  _)}; cbn.
      iApply always_elim. iApply always_mono; [|trivial].
      iIntros "He'"; iNext.
      iApply wp_mono; [|trivial].
      intros w; cbn; rewrite -interp_subst; trivial.
179 180
    - (* Fold *)
      rewrite map_length in IHHtyped.
181 182 183 184 185 186 187 188 189 190 191 192 193 194
      iApply (@wp_bind _ _ _ [FoldCtx]);
        iApply wp_impl_l;
        iSplit; [eapply (@always_intro _ _ _ _)|
                 iApply (IHHtyped _ _ (closed_type_rec HC)); trivial]; cbn.
      + iIntros {v} "#Hv".
        value_case. rewrite /interp_rec fixpoint_unfold. unfold interp_rec_pre at 1; cbn.
        eapply (@always_intro _ _ _ _).
        iApply exist_intro; iSplit; trivial.
        iNext.
        change (fixpoint (interp_rec_pre
                            (Vlist_cons_apply Δ (interp (S k) τ (closed_type_rec HC)))))
        with ((@interp _ _ L k (TRec τ) HC) Δ); trivial.
      + iRevert "HΓ"; rewrite zip_with_closed_ctx_list_subst; iIntros "#HΓ";
          iSplit; trivial.
195
    - (* Unfold *)
196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217
      iApply (@wp_bind _ _ _ [UnfoldCtx]);
        iApply wp_impl_l;
        iSplit; [eapply (@always_intro _ _ _ _)|
                 iApply (IHHtyped _ _ (typed_closed_type _ _ _ _ Htyped)); trivial];
        [|iSplit; trivial]; cbn.
      iIntros {v}.
      rewrite /interp_rec fixpoint_unfold. unfold interp_rec_pre at 1; cbn.
      iIntros "#Hv".
      iApply exist_elim; [|iAssumption].
      iIntros {w}; cbn.
      change (fixpoint (interp_rec_pre
                          (Vlist_cons_apply
                             Δ
                             (interp
                                (S k) τ
                                (closed_type_rec
                                   (typed_closed_type k Γ e (TRec τ) Htyped))))))
      with ((@interp _ _ L k (TRec τ) (typed_closed_type k Γ e (TRec τ) Htyped)) Δ);
        trivial.
      iIntros "[% #Hw]"; rewrite H.
      iApply wp_Fold; cbn; auto using to_of_val.
      iRevert "Hw". rewrite -interp_subst. iIntros "#Hw". trivial.
218
    - (* Alloc *)
219 220 221 222 223 224 225 226 227 228 229 230
      smart_wp_bind AllocCtx v "#Hv" IHHtyped; cbn. iClear "HΓ".
      iApply wp_atomic; cbn; trivial; [rewrite to_of_val; auto|].
      iApply pvs_intro.
      iApply wp_alloc; [| | | |iSplit;[iExact "Hheap"|iExact "Hv"]];
        [|iIntros "#[Hheap Hv]"| |]; auto using to_of_val.
      iIntros "#[Hheap Hv]". iNext.
      iIntros {l} "Hl".
      iApply exist_intro.
      iApply and_intro; [| trivial |]; auto.
      iApply inv_alloc; trivial. iNext.
      iApply exist_intro.
      iSplit; trivial.
231
    - (* Load *)
232 233 234 235 236 237 238 239 240 241 242 243 244 245
      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.
      iApply wp_inv; [auto using to_of_val| trivial
                      | apply and_elim_r | apply and_elim_l | ].
      iApply pvs_intro. iSplit; trivial.
      iIntros "Hl".
      iPoseProof later_exist_turnstile "Hl" as "Hl'"; [typeclasses eauto|].
      iRevert "Hheap".
      iApply exist_elim; [|iExact "Hl'"].
      iIntros {w} "[Hl1 #Hl2] #Hheap".
      iApply (wp_load _ _ _ 1);
        [apply and_elim_r| trivial | apply and_elim_l | iSplit; trivial].
246
      specialize (HNLdisj l); set_solver_ndisj.
247 248 249 250 251 252
      iNext.
      iSplitL; trivial.
      iIntros "Hl".
      iSplitL.
      + iNext. iApply exist_intro; iSplitL; trivial.
      + iApply pvs_intro; iApply interp_closed_irrel_turnstile; trivial.
253
    - (* Store *)
254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269
      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 |].
      iApply wp_inv; [cbn; rewrite ?to_of_val; auto| trivial
                      | apply and_elim_r | apply and_elim_l | ].
      iApply pvs_intro. iSplit; trivial.
      iClear "Hl". iIntros "Hl".
      iPoseProof later_exist_turnstile "Hl" as "Hl'"; [typeclasses eauto|].
      iRevert "Hheap Hw".
      iApply exist_elim; [|iExact "Hl'"].
      iIntros {u} "[Hl1 #Hl2] #Hheap #Hw".
      iApply wp_store;
        [rewrite to_of_val; trivial | apply and_elim_r
         | | apply and_elim_l | iSplit; trivial]. 
270
      specialize (HNLdisj l); set_solver_ndisj.
271 272 273 274 275
      iSplitL; trivial.
      iNext. iIntros "Hl".
      iSplitL; [|iApply pvs_intro; trivial].
      iNext. iApply exist_intro; iSplitL; trivial.
      iApply interp_closed_irrel_turnstile; trivial.
276 277
      (* unshelving *)
      Unshelve.
278 279
      all: cbn; solve [eauto 2 using closed_ctx_map_S_back,
                       typed_closed_type | try typeclasses eauto].
280 281 282
  Qed.
  
End typed_interp.