fundamental.v 4.29 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From solutions Require Export typed compatibility interp.
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

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