fundamental.v 3.57 KB
Newer Older
1
Require Import iris.proofmode.tactics.
Amin Timany's avatar
Amin Timany committed
2 3 4
Require Import iris.program_logic.hoare.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
5 6
Require Import iris_logrel.stlc.lang iris_logrel.stlc.typing
        iris_logrel.stlc.rules iris_logrel.stlc.logrel.
Amin Timany's avatar
Amin Timany committed
7 8 9 10 11
Import uPred.

Section typed_interp.
  Context {Σ : iFunctor}.

12 13 14 15 16 17 18
  Local Hint Extern 1 =>
  match goal with
    |-
    (_
       --------------------------------------
        _ : ?A, _) => let W := fresh "W" in evar (W : A); iExists W; unfold W; clear W
  end : itauto.
Amin Timany's avatar
Amin Timany committed
19

20 21 22 23 24 25 26
  Local Hint Extern 1 =>
  match goal with
    |-
    (_
       --------------------------------------
        _) => iNext
  end : itauto.
Amin Timany's avatar
Amin Timany committed
27

28 29 30 31 32 33 34
  Local Hint Extern 1 =>
  match goal with
    |-
    (_
       --------------------------------------
       (_  _)) => iSplit
  end : itauto.
Amin Timany's avatar
Amin Timany committed
35

36 37 38 39 40 41
  Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) constr(Hp) :=
    iApply (@wp_bind _ _ _ [ctx]);
    iApply wp_impl_l;
    iSplit; [| iApply Hp; trivial]; cbn;
    eapply (@always_intro _ _ _ _);
    iIntros {v} Hv.
Amin Timany's avatar
Amin Timany committed
42

43
  Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.
Amin Timany's avatar
Amin Timany committed
44 45 46 47 48 49

  Lemma typed_interp Γ vs e τ :
    typed Γ e τ  length Γ = length vs 
    Π∧ zip_with (@interp Σ) Γ vs  wp  (e.[env_subst vs]) (interp τ).
  Proof.
    intros Htyped; revert vs.
50
    induction Htyped; intros vs Hlen; iIntros "#Hctx"; cbn.
Amin Timany's avatar
Amin Timany committed
51 52 53
    - (* var *)
      destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
      { by rewrite -Hlen; apply lookup_lt_Some with τ. }
54 55 56 57
      rewrite /env_subst Hv. value_case.
      iApply big_and_elem_of; eauto.
      apply elem_of_list_lookup_2 with x.
      rewrite lookup_zip_with; simplify_option_eq; trivial.
Amin Timany's avatar
Amin Timany committed
58 59
    - (* unit *) value_case.
    - (* pair *)
60 61
      smart_wp_bind (PairLCtx e2.[env_subst vs]) v "# Hv" IHHtyped1.
      smart_wp_bind (PairRCtx v) v' "# Hv'" IHHtyped2.
Amin Timany's avatar
Amin Timany committed
62 63
      value_case; eauto 10 with itauto.
    - (* fst *)
64 65 66
      smart_wp_bind (FstCtx) v "# Hv" IHHtyped; cbn.
      iApply double_exists; [|trivial].
      intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H.
67
      iApply wp_fst; try iNext; eauto using to_of_val.
Amin Timany's avatar
Amin Timany committed
68
    - (* snd *)
69 70 71
      smart_wp_bind (SndCtx) v "# Hv" IHHtyped; cbn.
      iApply double_exists; [|trivial].
      intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H.
72
      iApply wp_snd; try iNext; eauto using to_of_val.
73 74 75 76 77 78
    - (* injl *)
      smart_wp_bind (InjLCtx) v "# Hv" IHHtyped; value_case.
      iLeft; iExists v; auto with itauto.
    - (* injr *)
      smart_wp_bind (InjRCtx) v "# Hv" IHHtyped; value_case.
      iRight; iExists v; auto with itauto.
Amin Timany's avatar
Amin Timany committed
79
    - (* case *)
80 81 82 83 84 85 86 87 88
      smart_wp_bind (CaseCtx _ _) v "#Hv" IHHtyped1; cbn.
      iDestruct "Hv" as "[Hv|Hv]"; eauto; iRevert "Hctx";
        iApply exist_elim; eauto; cbn;
          iIntros {w} "#[% Hw2] #Hctx"; rewrite H; cbn;
            [iApply wp_case_inl|iApply wp_case_inr];
            auto 1 using to_of_val;
            asimpl; [specialize (IHHtyped2 (w::vs)) | specialize (IHHtyped3 (w::vs))];
              erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto); iNext;
                [iApply IHHtyped2 | iApply IHHtyped3]; cbn; auto with itauto.
Amin Timany's avatar
Amin Timany committed
89
    - (* lam *)
90 91 92 93
      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 (w :: vs)); cbn; auto with itauto.
Amin Timany's avatar
Amin Timany committed
94
    - (* app *)
95 96 97
      smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1.
      smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
      iApply "Hv"; auto with itauto.
Amin Timany's avatar
Amin Timany committed
98 99
  Qed.

Amin Timany's avatar
Amin Timany committed
100
End typed_interp.