fundamental.v 4.29 KB
 Ralf Jung committed Jan 20, 2020 1 ``````From solutions Require Export typed compatibility interp. `````` Ralf Jung committed Jan 20, 2020 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.``````