fundamental.v 4.83 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From exercises Require Export typed compatibility interp.
2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19

(** * 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 Σ).

Robbert Krebbers's avatar
Robbert Krebbers committed
20 21 22
  (** First we need to prove soundness of operator typing. We declare these
  lemmas as instances so they will be used automatically in the proof of the
  fundamental theorem. *)
23 24 25 26 27 28 29 30 31
  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.

Robbert Krebbers's avatar
Robbert Krebbers committed
32 33 34 35 36 37
  (** The fundamental theorem. Since the syntactic typing judgment is defined
  in a mutual inductive fashion, we need to prove the fundamental theorem for
  expressions mutually with the fundamental theorem for values. Note that for
  such mutually inductive proofs, we need to make sure ourselves that the
  induction hypotheses is only used on smaller derivations. *)
  Theorem fundamental Γ e τ ρ
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 99 100 101 102 103 104 105 106
    (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.