fundamental.v 4.29 KB
Newer Older
1 2 3 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 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98
From tutorial_popl20 Require Export typed compatibility interp.

(** * The fundamental theorem of logical relations *)
(** The fundamental theorem of logical relations says that any syntactically
typed term is also semantically typed:

  if [Γ ⊢ e : τ] then [interp Γ ρ ⊨ e : 〚τ〛 ρ]

Here, [ρ] is any mapping free type variables in [Γ] and [τ] to semantic types.

This theorem essentially follows from the compatibility lemmas and an induction
on the typing derivation. *)

Section fundamental.
  Context `{!heapG Σ}.
  Implicit Types Γ : gmap string ty.
  Implicit Types τ : ty.
  Implicit Types ρ : list (sem_ty Σ).

  Instance ty_unboxed_sound τ ρ : ty_unboxed τ  SemTyUnboxed ( τ  ρ).
  Proof. destruct 1; simpl; apply _. Qed.
  Instance ty_un_op_sound op τ σ ρ :
    ty_un_op op τ σ  SemTyUnOp op ( τ  ρ) ( σ  ρ).
  Proof. destruct 1; simpl; apply _. Qed.
  Instance ty_bin_op_sound op τ1 τ2 σ ρ :
    ty_bin_op op τ1 τ2 σ  SemTyBinOp op ( τ1  ρ) ( τ2  ρ) ( σ  ρ).
  Proof. destruct 1; simpl; apply _. Qed.

  Lemma fundamental Γ e τ ρ
    (Hty : Γ  e : τ) : (interp_env Γ ρ  e :  τ  ρ)%I
  with fundamental_val v τ ρ
    (Hty :  v : τ) : ( v :  τ  ρ)%I.
  Proof.
    - destruct Hty; simpl.
      + iApply Var_sem_typed. by apply lookup_interp_env.
      + iApply Val_sem_typed; by iApply fundamental_val.
      + iApply Pair_sem_typed; by iApply fundamental.
      + iApply Fst_sem_typed; by iApply (fundamental _ _ (_ * _)%ty).
      + iApply Snd_sem_typed; by iApply (fundamental _ _ (_ * _)%ty).
      + iApply InjL_sem_typed; by iApply fundamental.
      + iApply InjR_sem_typed; by iApply fundamental.
      + iApply Case_sem_typed.
        * by iApply (fundamental _ _ (_ + _)%ty).
        * by iApply (fundamental _ _ (_  _)%ty).
        * by iApply (fundamental _ _ (_  _)%ty).
      + iApply Rec_sem_typed.
        change ( ?τ1  _   ?τ2  _)%sem_ty with ( τ1  τ2  ρ).
        rewrite -!interp_env_binder_insert. by iApply fundamental.
      + iApply App_sem_typed.
        * by iApply (fundamental _ _ (_  _)%ty).
        * by iApply fundamental.
      + iApply TLam_sem_typed; iIntros (A).
        rewrite -interp_env_ty_lift_0. by iApply fundamental.
      + rewrite interp_ty_subst_0.
        iApply (TApp_sem_typed _ _ (λ A,  _  (A :: _))).
        by iApply (fundamental _ _ (∀: _)%ty).
      + iApply (Pack_sem_typed _ _ _ ( _  ρ)).
        rewrite -interp_ty_subst_0. by iApply fundamental.
      + iApply (Unpack_sem_typed _ _ _ _ (λ A,  _  (A :: _))).
        * by iApply (fundamental _ _ (∃: _)%ty).
        * iIntros (A).
          rewrite -(interp_ty_lift_0 _ A ρ) -(interp_env_ty_lift_0 _ A ρ).
          rewrite -interp_env_binder_insert.
          by iApply fundamental.
      + iApply Alloc_sem_typed. by iApply fundamental.
      + iApply Load_sem_typed. by iApply (fundamental _ _ (ref _)%ty).
      + iApply Store_sem_typed.
        * by iApply (fundamental _ _ (ref _)%ty).
        * by iApply fundamental.
      + iApply FAA_sem_typed.
        * by iApply (fundamental _ _ (ref TInt)%ty).
        * by iApply (fundamental _ _ TInt).
      + iApply CmpXchg_sem_typed.
        * by iApply (fundamental _ _ (ref _)%ty).
        * by iApply fundamental.
        * by iApply fundamental.
      + iApply UnOp_sem_typed. by iApply fundamental.
      + iApply BinOp_sem_typed; by iApply fundamental.
      + iApply If_sem_typed.
        * by iApply (fundamental _ _ TBool).
        * by iApply fundamental.
        * by iApply fundamental.
      + iApply Fork_sem_typed. by iApply (fundamental _ _ TUnit).
    - destruct Hty; simpl.
      + iApply UnitV_sem_typed.
      + iApply BoolV_sem_typed.
      + iApply IntV_sem_typed.
      + iApply PairV_sem_typed; by iApply fundamental_val.
      + iApply InjLV_sem_typed; by iApply fundamental_val.
      + iApply InjRV_sem_typed; by iApply fundamental_val.
      + iApply RecV_sem_typed.
        change ( ?τ1  _   ?τ2  _)%sem_ty with ( τ1  τ2  ρ).
        rewrite -(interp_env_empty ρ) -!interp_env_binder_insert.
        by iApply fundamental.
      + iApply TLamV_sem_typed; iIntros (A).
        rewrite -(interp_env_empty (A :: ρ)). by iApply fundamental.
   Qed.
End fundamental.