fundamental.v 4.83 KB
 Ralf Jung committed Jan 20, 2020 1 ``````From exercises 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 `````` (** * 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 committed Jan 20, 2020 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. *) `````` Ralf Jung committed Jan 20, 2020 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 committed Jan 20, 2020 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 τ ρ `````` Ralf Jung committed Jan 20, 2020 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.``````