fundamental_unary.v 7.39 KB
Newer Older
Amin Timany's avatar
Amin Timany committed
1 2
From iris_examples.logrel.F_mu_ref_conc Require Export logrel_unary.
From iris_examples.logrel.F_mu_ref_conc Require Import rules.
Ralf Jung's avatar
Ralf Jung committed
3
From iris.base_logic Require Export invariants.
Amin Timany's avatar
Amin Timany committed
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 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 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
From iris.program_logic Require Export lifting.
From iris.proofmode Require Import tactics.

Definition log_typed `{heapIG Σ} (Γ : 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 typed_interp.
  Context `{heapIG Σ}.
  Notation D := (valC -n> iProp Σ).

  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.

  Theorem fundamental Γ e τ : Γ  e : τ  Γ  e : τ.
  Proof.
    induction 1; iIntros (Δ vs HΔ) "#HΓ /=".
    - (* var *)
      iDestruct (interp_env_Some_l with "HΓ") as (v) "[% ?]"; first done.
      rewrite /env_subst. simplify_option_eq. by iApply wp_value.
    - (* unit *) iApply wp_value; trivial.
    - (* nat *) iApply wp_value; simpl; eauto.
    - (* bool *) iApply wp_value; simpl; eauto.
    - (* nat bin op *)
      smart_wp_bind (BinOpLCtx _ e2.[env_subst vs]) v "#Hv" IHtyped1.
      smart_wp_bind (BinOpRCtx _ v) v' "# Hv'" IHtyped2.
      iDestruct "Hv" as (n) "%"; iDestruct "Hv'" as (n') "%"; simplify_eq/=.
      iApply wp_pure_step_later; auto. iNext. iApply wp_value.
      destruct op; simpl; try destruct eq_nat_dec;
        try destruct le_dec; try destruct lt_dec; eauto 10.
    - (* pair *)
      smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHtyped1.
      smart_wp_bind (PairRCtx v) v' "# Hv'" IHtyped2.
      iApply wp_value; eauto.
    - (* fst *)
      smart_wp_bind (FstCtx) v "# Hv" IHtyped; cbn.
      iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
      iApply wp_pure_step_later; auto. by iApply wp_value.
    - (* 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.
        erewrite typed_subst_head_simpl by naive_solver.
        iApply (IHtyped2 Δ (w :: vs)). iApply interp_env_cons; auto.
      + iApply wp_pure_step_later; auto 1 using to_of_val; asimpl. iNext.
        erewrite typed_subst_head_simpl by naive_solver.
        iApply (IHtyped3 Δ (w :: vs)). iApply interp_env_cons; auto.
    - (* If *)
      smart_wp_bind (IfCtx _ _) v "#Hv" IHtyped1; cbn.
      iDestruct "Hv" as ([]) "%"; subst; simpl;
        [iApply wp_pure_step_later .. ]; auto; iNext;
      [iApply IHtyped2| iApply IHtyped3]; auto.
    - (* Rec *)
      iApply wp_value. simpl. iAlways. iLöb as "IH". iIntros (w) "#Hw".
      iDestruct (interp_env_length with "HΓ") as %?.
      iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
      asimpl. change (Rec _) with (of_val (RecV e.[upn 2 (env_subst vs)])) at 2.
      erewrite typed_subst_head_simpl_2 by naive_solver.
      iApply (IHtyped Δ (_ :: w :: vs)).
      iApply interp_env_cons; iSplit; [|iApply interp_env_cons]; auto.
78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
    - (* 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.
      asimpl.
      erewrite typed_subst_head_simpl by naive_solver.
      iApply (IHtyped Δ (w :: vs)); auto.
      iApply interp_env_cons; iSplit; auto.
    - (* LetIn *)
      smart_wp_bind (LetInCtx _) v "#Hv" IHtyped1; cbn.
      iDestruct (interp_env_length with "HΓ") as %?.
      iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
      asimpl. erewrite typed_subst_head_simpl by naive_solver.
      iApply (IHtyped2 Δ (v :: vs)).
      iApply interp_env_cons; iSplit; eauto.
    - (* Seq *)
      smart_wp_bind (SeqCtx _) v "#Hv" IHtyped1; cbn.
      iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
      by iApply IHtyped2.
Amin Timany's avatar
Amin Timany committed
97 98 99
    - (* app *)
      smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHtyped1.
      smart_wp_bind (AppRCtx v) w "#Hw" IHtyped2.
Ralf Jung's avatar
Ralf Jung committed
100
      by iApply "Hv".
Amin Timany's avatar
Amin Timany committed
101 102 103 104 105 106 107 108 109 110 111 112
    - (* 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" $! ( τ'  Δ)); iPureIntro; apply _|]; cbn.
      iIntros (w) "?". by iApply interp_subst.
    - (* Fold *)
      iApply (wp_bind (fill [FoldCtx]));
        iApply wp_wand_l; iSplitL; [|iApply (IHtyped Δ vs); auto].
      iIntros (v) "#Hv". iApply wp_value.
Ralf Jung's avatar
Ralf Jung committed
113
      rewrite /= -interp_subst fixpoint_interp_rec1_eq /=.
Amin Timany's avatar
Amin Timany committed
114 115 116 117
      iAlways; eauto.
    - (* Unfold *)
      iApply (wp_bind (fill [UnfoldCtx]));
        iApply wp_wand_l; iSplitL; [|iApply IHtyped; auto].
Ralf Jung's avatar
Ralf Jung committed
118
      iIntros (v) "#Hv". rewrite /= fixpoint_interp_rec1_eq.
Amin Timany's avatar
Amin Timany committed
119 120 121 122 123
      change (fixpoint _) with ( TRec τ  Δ); simpl.
      iDestruct "Hv" as (w) "#[% Hw]"; subst.
      iApply wp_pure_step_later; cbn; auto using to_of_val.
      iNext. iApply wp_value. by iApply interp_subst.
    - (* Fork *)
Ralf Jung's avatar
Ralf Jung committed
124
      iApply wp_fork. rewrite -bi.later_sep. iNext; iSplitL; trivial.
Amin Timany's avatar
Amin Timany committed
125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145
      iApply wp_wand_l. iSplitL; [|iApply IHtyped; auto]; auto.
    - (* 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.
      iApply wp_atomic.
      iInv (logN .@ l) as (w) "[Hw1 #Hw2]" "Hclose".
      iApply (wp_load with "Hw1").
      iModIntro. 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.
      iApply wp_atomic.
      iInv (logN .@ l) as (z) "[Hz1 #Hz2]" "Hclose".
146
      iApply (wp_store with "Hz1"); auto using to_of_val.
Amin Timany's avatar
Amin Timany committed
147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164
      iModIntro. iNext.
      iIntros "Hz1". iMod ("Hclose" with "[Hz1 Hz2]"); eauto.
    - (* CAS *)
      smart_wp_bind (CasLCtx _ _) v1 "#Hv1" IHtyped1; cbn.
      smart_wp_bind (CasMCtx _ _) v2 "#Hv2" IHtyped2; cbn.
      smart_wp_bind (CasRCtx _ _) v3 "#Hv3" IHtyped3; cbn. iClear "HΓ".
      iDestruct "Hv1" as (l) "[% Hv1]"; subst.
      iApply wp_atomic.
      iInv (logN .@ l) as (w) "[Hw1 #Hw2]" "Hclose".
      destruct (decide (v2 = w)) as [|Hneq]; subst.
      + iApply (wp_cas_suc with "Hw1"); auto using to_of_val.
        iModIntro. iNext.
        iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
      + iApply (wp_cas_fail with "Hw1"); auto using to_of_val.
        iModIntro. iNext.
        iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
  Qed.
End typed_interp.