fundamental.v 2.77 KB
Newer Older
Amin Timany's avatar
Amin Timany committed
1
From iris_examples.logrel.stlc Require Export logrel.
Amin Timany's avatar
Amin Timany committed
2
From iris.proofmode Require Import tactics.
Amin Timany's avatar
Amin Timany committed
3
From iris_examples.logrel.stlc Require Import rules.
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
From iris.base_logic Require Export big_op.
From iris.program_logic Require Import lifting.

Section typed_interp.
  Context `{irisG stlc_lang Σ}.

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

  Theorem fundamental Γ vs e τ :
    Γ  e : τ   Γ * vs   τ ⟧ₑ e.[env_subst vs].
  Proof.
    intros Htyped; revert vs.
    induction Htyped; iIntros (vs) "#Hctx /=".
    - (* var *)
      iDestruct (interp_env_Some_l with "[]") as (v) "[#H1 #H2]"; eauto;
        iDestruct "H1" as %Heq; rewrite /env_subst Heq /=.
      by iApply wp_value.
    - (* unit *) by iApply wp_value.
    - (* pair *)
      smart_wp_bind (PairLCtx e2.[env_subst vs]) v "# Hv" IHHtyped1.
      smart_wp_bind (PairRCtx v) v' "# Hv'" IHHtyped2.
      iApply wp_value; eauto 10.
    - (* fst *)
      smart_wp_bind (FstCtx) v "# Hv" IHHtyped; 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" IHHtyped; 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" IHHtyped. by iApply wp_value; eauto.
    - (* injr *)
      smart_wp_bind (InjRCtx) v "# Hv" IHHtyped. by iApply wp_value; eauto.
    - (* case *)
      iDestruct (interp_env_length with "[]") as %Hlen; auto.
      smart_wp_bind (CaseCtx _ _) v "# Hv" IHHtyped1; cbn.
      iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as (w) "[% Hw]"; subst.
      + simpl. iApply wp_pure_step_later; auto. asimpl.
        specialize (IHHtyped2 (w::vs)).
        erewrite <- ?typed_subst_head_simpl in *; eauto; simpl in *; auto.
        iNext. iApply (IHHtyped2). iApply interp_env_cons; by iSplit.
      + simpl. iApply wp_pure_step_later; auto. asimpl.
        specialize (IHHtyped3 (w::vs)).
        erewrite <- ?typed_subst_head_simpl in *; eauto; simpl in *; auto.
        iNext. iApply (IHHtyped3). iApply interp_env_cons; by iSplit.
    - (* lam *)
      iDestruct (interp_env_length with "[]") as %Hlen; auto.
      iApply wp_value. simpl. iAlways; iIntros (w) "#Hw".
      iApply wp_pure_step_later; auto.
      asimpl; erewrite typed_subst_head_simpl; [|eauto|cbn]; eauto.
      iNext; iApply (IHHtyped (w :: vs)). iApply interp_env_cons; by iSplit.
    - (* app *)
      smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1.
      smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
      iApply "Hv"; auto.
  Qed.
End typed_interp.