fundamental.v 4.57 KB
Newer Older
Amin Timany's avatar
Amin Timany committed
1
From iris_examples.logrel.F_mu_ref Require Export logrel.
Amin Timany's avatar
Amin Timany committed
2 3
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import lifting.
Amin Timany's avatar
Amin Timany committed
4
From iris_examples.logrel.F_mu_ref Require Import rules.
Amin Timany's avatar
Amin Timany committed
5 6 7 8 9 10 11 12

Definition log_typed `{heapG Σ} (Γ : list type) (e : expr) (τ : type) :=  Δ vs,
  env_Persistent Δ 
   Γ * Δ vs   τ ⟧ₑ Δ e.[env_subst vs].
Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next level).

Section fundamental.
  Context `{heapG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
13
  Notation D := (valO -n> iProp Σ).
Amin Timany's avatar
Amin Timany committed
14 15 16 17 18 19 20 21 22 23 24

  Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
    iApply (wp_bind (fill [ctx]));
    iApply (wp_wand with "[-]"); [iApply Hp; trivial|]; cbn;
    iIntros (v) Hv; cbn.

  Theorem fundamental Γ e τ : Γ  e : τ  Γ  e : τ.
  Proof.
    induction 1; iIntros (Δ vs HΔ) "#HΓ /=".
    - (* var *)
      iDestruct (interp_env_Some_l with "HΓ") as (v) "[% ?]"; first done.
Amin Timany's avatar
Amin Timany committed
25
      erewrite env_subst_lookup; eauto. by iApply wp_value.
Amin Timany's avatar
Amin Timany committed
26 27 28 29
    - (* unit *) by iApply wp_value.
    - (* pair *)
      smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHtyped1.
      smart_wp_bind (PairRCtx v) v' "# Hv'" IHtyped2.
Ralf Jung's avatar
Ralf Jung committed
30
      iApply wp_value. eauto 10.
Amin Timany's avatar
Amin Timany committed
31 32 33
   - (* fst *)
      smart_wp_bind (FstCtx) v "# Hv" IHtyped; cbn.
      iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
Ralf Jung's avatar
Ralf Jung committed
34
      iApply wp_pure_step_later; auto. by iApply wp_value.
Amin Timany's avatar
Amin Timany committed
35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
    - (* snd *)
      smart_wp_bind (SndCtx) v "# Hv" IHtyped; cbn.
      iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
      iApply wp_pure_step_later; auto; by iApply wp_value.
    - (* injl *)
      smart_wp_bind (InjLCtx) v "# Hv" IHtyped; cbn.
      iApply wp_value; eauto.
    - (* injr *)
      smart_wp_bind (InjRCtx) v "# Hv" IHtyped; cbn.
      iApply wp_value; eauto.
    - (* case *)
      smart_wp_bind (CaseCtx _ _) v "#Hv" IHtyped1; cbn.
      iDestruct (interp_env_length with "HΓ") as %?.
      iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as (w) "[% Hw]"; simplify_eq/=.
      + iApply wp_pure_step_later; auto 1 using to_of_val; asimpl. iNext.
        iApply (IHtyped2 Δ (w :: vs)). iApply interp_env_cons; auto.
      + iApply wp_pure_step_later; auto 1 using to_of_val; asimpl. iNext.
        iApply (IHtyped3 Δ (w :: vs)). iApply interp_env_cons; auto.
    - (* lam *)
      iApply wp_value. simpl. iAlways. iIntros (w) "#Hw".
      iDestruct (interp_env_length with "HΓ") as %?.
      iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
Amin Timany's avatar
Amin Timany committed
57
      asimpl.
Amin Timany's avatar
Amin Timany committed
58 59 60 61 62 63 64 65 66 67 68 69 70 71 72
      iApply (IHtyped Δ (w :: vs)). iApply interp_env_cons; auto.
    - (* app *)
      smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHtyped1.
      smart_wp_bind (AppRCtx v) w "#Hw" IHtyped2.
      iApply wp_mono; [|iApply "Hv"]; auto.
    - (* TLam *)
      iApply wp_value.
      iAlways; iIntros (τi) "%". iApply wp_pure_step_later; auto; iNext.
      iApply IHtyped. by iApply interp_env_ren.
    - (* TApp *)
      smart_wp_bind TAppCtx v "#Hv" IHtyped; cbn.
      iApply wp_wand_r; iSplitL; [iApply ("Hv" $! (interp  τ' Δ)); iPureIntro; apply _|].
      iIntros (w) "?". by rewrite interp_subst.
    - (* Fold *)
      smart_wp_bind FoldCtx v "#Hv" IHtyped; cbn.
Ralf Jung's avatar
Ralf Jung committed
73
      iApply wp_value. rewrite /= -interp_subst fixpoint_interp_rec1_eq /=.
Amin Timany's avatar
Amin Timany committed
74 75 76 77
      iAlways; eauto.
    - (* Unfold *)
      iApply (wp_bind (fill [UnfoldCtx]));
        iApply wp_wand_l; iSplitL; [|iApply IHtyped; auto].
Ralf Jung's avatar
Ralf Jung committed
78
      iIntros (v) "#Hv". rewrite /= fixpoint_interp_rec1_eq.
Amin Timany's avatar
Amin Timany committed
79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
      change (fixpoint _) with (interp  (TRec τ) Δ); simpl.
      iDestruct "Hv" as (w) "#[% Hw]"; subst.
      iApply wp_pure_step_later; cbn; auto using to_of_val.
      iNext. iApply wp_value. by rewrite -interp_subst.
    - (* Alloc *)
      smart_wp_bind AllocCtx v "#Hv" IHtyped; cbn. iClear "HΓ". iApply wp_fupd.
      iApply wp_alloc; auto 1 using to_of_val.
      iNext; iIntros (l) "Hl".
      iMod (inv_alloc _ with "[Hl]") as "HN";
        [| iModIntro; iExists _; iSplit; trivial]; eauto.
    - (* Load *)
      smart_wp_bind LoadCtx v "#Hv" IHtyped; cbn. iClear "HΓ".
      iDestruct "Hv" as (l) "[% #Hv]"; subst.
      iInv (logN .@ l) as (w) "[Hw1 #Hw2]" "Hclose".
      iApply (wp_load with "Hw1 [Hclose]").
      iNext.
      iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
    - (* Store *)
      smart_wp_bind (StoreLCtx _) v "#Hv" IHtyped1; cbn.
      smart_wp_bind (StoreRCtx _) w "#Hw" IHtyped2; cbn. iClear "HΓ".
      iDestruct "Hv" as (l) "[% #Hv]"; subst.
      iInv (logN .@ l) as (z) "[Hz1 #Hz2]" "Hclose".
      iApply (wp_store with "Hz1 [Hclose]"); eauto using to_of_val. iNext.
      iIntros "Hz1". iMod ("Hclose" with "[Hz1 Hz2]"); eauto.
  Qed.
End fundamental.