### script to generate exercises, and generate them

parent c7362b6b
 From tutorial_popl20 Require Export sem_typed sem_operators. (** * Compatibility lemmas *) (** We prove that the logical relations, i.e., the semantic typing judgment, that we have defined is compatible with typing rules. That is, the logical relations is a congruence with respect to the typing rules. These compatibility lemmas are what one gets when the syntactic typing judgment is replaced semantic typing judgment in syntactic typing rules. For instance ([sem_typed_pair]): << Γ ⊢ e1 : τ1 Γ ⊢ e2 : τ2 -------------------------------- Γ ⊢ (e1, e2) : τ1 × τ2 >> becomes: << (Γ ⊨ e1 : A1) -∗ (Γ ⊨ e2 : A2) -∗ Γ ⊢ (e1, e2) : A1 * A2 >> *) Section compatibility. Context `{!heapG Σ}. Implicit Types A B : sem_ty Σ. Implicit Types C : sem_ty Σ → sem_ty Σ. (** * Compatibility rules for expression typing *) (** * Variables *) Lemma Var_sem_typed Γ (x : string) A : Γ !! x = Some A → (Γ ⊨ x : A)%I. Proof. iIntros (HΓx vs) "!# #HΓ /=". iDestruct (env_sem_typed_lookup with "HΓ") as (v ->) "HA"; first done. by iApply wp_value. Qed. Lemma Val_sem_typed Γ v A : ⊨ᵥ v : A -∗ Γ ⊨ v : A. Proof. iIntros "#Hv" (vs) "!# #HΓ /=". iApply wp_value. iApply "Hv". Qed. (** * Products and sums *) Lemma Pair_sem_typed Γ e1 e2 A1 A2 : Γ ⊨ e1 : A1 -∗ Γ ⊨ e2 : A2 -∗ Γ ⊨ (e1,e2) : A1 * A2. Proof. iIntros "#H1 #H2" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H2 [//])"); iIntros (w2) "#HA2". wp_apply (wp_wand with "(H1 [//])"); iIntros (w1) "#HA1". wp_pures. iExists w1, w2. auto. Qed. Lemma Fst_sem_typed Γ e A1 A2 : Γ ⊨ e : A1 * A2 -∗ Γ ⊨ Fst e : A1. Proof. iIntros "#H" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H [//])"); iIntros (w). iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures. Qed. Lemma Snd_sem_typed Γ e A1 A2 : Γ ⊨ e : A1 * A2 -∗ Γ ⊨ Snd e : A2. Proof. iIntros "#H" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H [//])"); iIntros (w). iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures. Qed. Lemma InjL_sem_typed Γ e A1 A2 : Γ ⊨ e : A1 -∗ Γ ⊨ InjL e : A1 + A2. Proof. (* FILL IN YOUR PROOF *) Qed. (* REMOVE *) Lemma InjR_sem_typed Γ e A1 A2 : Γ ⊨ e : A2 -∗ Γ ⊨ InjR e : A1 + A2. Proof. iIntros "#H" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HA". wp_pures. iRight. iExists w. auto. Qed. Lemma Case_sem_typed Γ e e1 e2 A1 A2 B : Γ ⊨ e : A1 + A2 -∗ Γ ⊨ e1 : (A1 → B) -∗ Γ ⊨ e2 : (A2 → B) -∗ Γ ⊨ Case e e1 e2 : B. Proof. (* FILL IN YOUR PROOF *) Qed. (** * Functions *) Lemma Rec_sem_typed Γ f x e A1 A2 : binder_insert f (A1 → A2)%sem_ty (binder_insert x A1 Γ) ⊨ e : A2 -∗ Γ ⊨ (rec: f x. (* FILL IN HERE *) Admitted. Proof. iIntros "#H" (vs) "!# #HΓ /=". wp_pures. iLöb as "IH". iIntros "!#" (v) "#HA1". wp_pures. set (r := RecV f x _). rewrite -subst_map_binder_insert_2. iApply "H". iApply (env_sem_typed_insert with "IH"). by iApply env_sem_typed_insert. Qed. Lemma App_sem_typed Γ e1 e2 A1 A2 : Γ ⊨ e1 : (A1 → A2) -∗ Γ ⊨ e2 : A1 -∗ Γ ⊨ e1 e2 : A2. Proof. iIntros "#H1 #H2" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H2 [//])"); iIntros (w) "#HA1". wp_apply (wp_wand with "(H1 [//])"); iIntros (v) "#HA". by iApply "HA". Qed. (** * Polymorphic functions and existentials *) Lemma TLam_sem_typed Γ e C : (∀ A, Γ ⊨ e : C A) -∗ Γ ⊨ (Λ: e) : ∀ A, C A. Proof. iIntros "#H" (vs) "!# #HΓ /=". wp_pures. iIntros "!#" (A) "/=". wp_pures. by iApply ("H" \$! A). Qed. Lemma TApp_sem_typed Γ e C A : (Γ ⊨ e : ∀ A, C A) -∗ Γ ⊨ e <_> : C A. Proof. iIntros "#H" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB". by iApply ("HB" \$! A). Qed. Lemma Pack_sem_typed Γ e C A : Γ ⊨ e : C A -∗ Γ ⊨ (pack: e) : ∃ A, C A. Proof. (* FILL IN YOUR PROOF *) Qed. Lemma Unpack_sem_typed Γ x e1 e2 C B : (Γ ⊨ e1 : ∃ A, C A) -∗ (∀ A, binder_insert x (C A) Γ ⊨ e2 : B) -∗ Γ ⊨ (unpack: x := e1 in e2) : B. Proof. (* FILL IN YOUR PROOF *) Qed. (** ** Heap operations *) Lemma Alloc_sem_typed Γ e A : Γ ⊨ e : A -∗ Γ ⊨ ref e : ref A. Proof. iIntros "#H" (vs) "!# #HΓ /=". wp_bind (subst_map _ e). iApply (wp_wand with "(H [//])"); iIntros (w) "HA". iApply wp_fupd. wp_alloc l as "Hl". iMod (inv_alloc (tyN .@ l) _ (∃ v, l ↦ v ∗ A v)%I with "[Hl HA]") as "#?". { iExists w. iFrame. } iModIntro. iExists l; auto. Qed. Lemma Load_sem_typed Γ e A : Γ ⊨ e : ref A -∗ Γ ⊨ ! e : A. Proof. iIntros "#H" (vs) "!# #HΓ /=". wp_bind (subst_map _ e). iApply (wp_wand with "(H [//])"); iIntros (w). iDestruct 1 as (l ->) "#?". iInv (tyN.@l) as (v) "[>Hl HA]". wp_load. eauto 10. Qed. Lemma Store_sem_typed Γ e1 e2 A : Γ ⊨ e1 : ref A -∗ Γ ⊨ e2 : A -∗ Γ ⊨ (e1 <- e2) : (). Proof. (* FILL IN YOUR PROOF *) Qed. Lemma FAA_sem_typed Γ e1 e2 : Γ ⊨ e1 : ref sem_ty_int -∗ Γ ⊨ e2 : sem_ty_int -∗ Γ ⊨ FAA e1 e2 : sem_ty_int. Proof. (* FILL IN YOUR PROOF *) Qed. Lemma CmpXchg_sem_typed Γ A e1 e2 e3 : SemTyUnboxed A → Γ ⊨ e1 : ref A -∗ Γ ⊨ e2 : A -∗ Γ ⊨ e3 : A -∗ Γ ⊨ CmpXchg e1 e2 e3 : A * sem_ty_bool. Proof. (* FILL IN YOUR PROOF *) Qed. (** ** Operators *) Lemma UnOp_sem_typed Γ e op A B : SemTyUnOp op A B → Γ ⊨ e : A -∗ Γ ⊨ UnOp op e : B. Proof. intros ?. iIntros "#H" (vs) "!# #HΓ /=". wp_apply (wp_wand with "(H [//])"); iIntros (v) "#HA". iDestruct (sem_ty_un_op with "HA") as (w ?) "#HB". by wp_unop. Qed. Lemma BinOp_sem_typed Γ e1 e2 op A1 A2 B : SemTyBinOp op A1 A2 B → Γ ⊨ e1 : A1 -∗ Γ ⊨ e2 : A2 -∗ Γ ⊨ BinOp op e1 e2 : B. Proof. (* FILL IN YOUR PROOF *) Qed. Lemma If_sem_typed Γ e e1 e2 B : Γ ⊨ e : sem_ty_bool -∗ Γ ⊨ e1 : B -∗ Γ ⊨ e2 : B -∗ Γ ⊨ (if: e then e1 else e2) : B. Proof. (* FILL IN YOUR PROOF *) Qed. (** ** Fork *) Lemma Fork_sem_typed Γ e : Γ ⊨ e : () -∗ Γ ⊨ Fork e : (). Proof. (* FILL IN YOUR PROOF *) Qed. (** * Compatibility rules for value typing *) (** ** Base types *) Lemma UnitV_sem_typed : (⊨ᵥ #() : ())%I. Proof. by iPureIntro. Qed. Lemma BoolV_sem_typed (b : bool) : (⊨ᵥ #b : sem_ty_bool)%I. Proof. by iExists b. Qed. Lemma IntV_sem_typed (n : Z) : (⊨ᵥ #n : sem_ty_int)%I. Proof. (* FILL IN YOUR PROOF *) Qed. (** ** Products and sums *) Lemma PairV_sem_typed v1 v2 τ1 τ2 : ⊨ᵥ v1 : τ1 -∗ ⊨ᵥ v2 : τ2 -∗ ⊨ᵥ PairV v1 v2 : (τ1 * τ2). Proof. iIntros "#H1 #H2". iExists v1, v2. auto. Qed. Lemma InjLV_sem_typed v τ1 τ2 : ⊨ᵥ v : τ1 -∗ ⊨ᵥ InjLV v : (τ1 + τ2). Proof. iIntros "H". iLeft. auto. Qed. Lemma InjRV_sem_typed v τ1 τ2 : ⊨ᵥ v : τ2 -∗ ⊨ᵥ InjRV v : (τ1 + τ2). Proof. iIntros "H". iRight. auto. Qed. (** ** Functions *) Lemma RecV_sem_typed f x e A B : binder_insert f (A → B)%sem_ty (binder_insert x A ∅) ⊨ e : B -∗ ⊨ᵥ RecV f x e : (A → B). Proof. iIntros "#H". iLöb as "IH". iIntros "!#" (v) "#HA1". wp_pures. set (r := RecV f x _). rewrite -subst_map_binder_insert_2_empty. iApply "H". iApply (env_sem_typed_insert with "IH"). iApply (env_sem_typed_insert with "[\$]"). iApply env_sem_typed_empty. Qed. Lemma TLamV_sem_typed e C : (∀ A, ∅ ⊨ e : C A) -∗ ⊨ᵥ (Λ: e) : ∀ A, C A. Proof. iIntros "#H !#" (A) "/=". wp_pures. rewrite -{2}(subst_map_empty e). iApply ("H" \$! A). by iApply env_sem_typed_empty. Qed. End compatibility.
exercises/demo.v 0 → 100644
 From tutorial_popl20 Require Import language. From iris.base_logic.lib Require Import invariants. From iris.heap_lang Require Import adequacy. (** This file contains a simplified version of the development that we used throughout the lectures. This simplified version contains a subset of the features in the full version. Notably, it does not support unary and binary operators, sums, polymorphic functions, and existential types. Moreover, in this version, we define the interpretation of types [interp] in a direct style, instead of using semantic type formers as combinators on [sem_ty]. Overview of the lecture: 1. HeapLang is a untyped language. We first define a syntactic types and a syntactic typing judgment. Γ ⊢ₜ e : τ 2. Following Dreyer's talk, we define semantic typing in Iris: Γ ⊨ e : τ 3. We then prove the fundamental theorem: Γ ⊢ₜ e : τ → Γ ⊨ e : τ Every term that is syntactically typed, is also semantically typed 4. We prove safety of semantic typing: ∅ ⊨ e : τ → e is safe, i.e. cannot crash 5. We prove that we get more by showing that certain "unsafe" programs are also semantically typed *) Inductive ty := | TUnit : ty | TBool : ty | TInt : ty | TProd : ty → ty → ty | TArr : ty → ty → ty | TRef : ty → ty. Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level). Inductive typed : gmap string ty → expr → ty → Prop := (** Variables *) | Var_typed Γ x τ : Γ !! x = Some τ → Γ ⊢ₜ Var x : τ (** Base values *) | UnitV_typed Γ : Γ ⊢ₜ #() : TUnit | BoolV_typed Γ (b : bool) : Γ ⊢ₜ #b : TBool | IntV_val_typed Γ (i : Z) : Γ ⊢ₜ #i : TInt (** Products *) | Pair_typed Γ e1 e2 τ1 τ2 : Γ ⊢ₜ e1 : τ1 → Γ ⊢ₜ e2 : τ2 → Γ ⊢ₜ Pair e1 e2 : TProd τ1 τ2 | Fst_typed Γ e τ1 τ2 : Γ ⊢ₜ e : TProd τ1 τ2 → Γ ⊢ₜ Fst e : τ1 | Snd_typed Γ e τ1 τ2 : Γ ⊢ₜ e : TProd τ1 τ2 → Γ ⊢ₜ Snd e : τ2 (** Functions *) | Rec_typed Γ f x e τ1 τ2 : binder_insert f (TArr τ1 τ2) (binder_insert x τ1 Γ) ⊢ₜ e : τ2 → Γ ⊢ₜ Rec f x e : TArr τ1 τ2 | App_typed Γ e1 e2 τ1 τ2 : Γ ⊢ₜ e1 : TArr τ1 τ2 → Γ ⊢ₜ e2 : τ1 → Γ ⊢ₜ App e1 e2 : τ2 (** Heap operations *) | Alloc_typed Γ e τ : Γ ⊢ₜ e : τ → Γ ⊢ₜ Alloc e : TRef τ | Load_typed Γ e τ : Γ ⊢ₜ e : TRef τ → Γ ⊢ₜ Load e : τ | Store_typed Γ e1 e2 τ : Γ ⊢ₜ e1 : TRef τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ Store e1 e2 : TUnit (** If *) | If_typed Γ e0 e1 e2 τ : Γ ⊢ₜ e0 : TBool → Γ ⊢ₜ e1 : τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ If e0 e1 e2 : τ where "Γ ⊢ₜ e : τ" := (typed Γ e τ). Section semtyp. Context `{!heapG Σ}. Record sem_ty := SemTy { sem_ty_car :> val → iProp Σ; sem_ty_persistent v : Persistent (sem_ty_car v) }. Arguments SemTy _%I {_}. Existing Instance sem_ty_persistent. Fixpoint interp (τ : ty) : sem_ty := match τ with | TUnit => SemTy (λ w, ⌜w = #()⌝) | TBool => SemTy (λ w, ⌜w = #true⌝ ∨ ⌜w = #false⌝) | TInt => SemTy (λ w, ∃ n : Z, ⌜w = #n⌝ ) | TProd τ1 τ2 => SemTy (λ w, ∃ v1 v2, ⌜w = (v1, v2)%V⌝ ∗ interp τ1 v1 ∗ interp τ2 v2) | TArr τ1 τ2 => SemTy (λ w, □ ∀ v, interp τ1 v -∗ WP w v {{ u, interp τ2 u}}) | TRef τ => SemTy (λ w, ∃ l : loc, ⌜ w = #l ⌝ ∗ inv (nroot .@ "ref" .@ l) (∃ v, l ↦ v ∗ interp τ v)) end%I. Definition interp_env (Γ : gmap string ty) (vs : gmap string val) : iProp Σ := [∗ map] τ;v ∈ Γ;vs, interp τ v. Definition sem_typed (Γ : gmap string ty) (e : expr) (τ : ty) : iProp Σ := □ ∀ vs, interp_env Γ vs -∗ WP subst_map vs e {{ w, interp τ w }}. Notation "Γ ⊨ e : A" := (sem_typed Γ e A) (at level 74, e, A at next level). Lemma Pair_sem_typed Γ e1 e2 τ1 τ2 : Γ ⊨ e1 : τ1 -∗ Γ ⊨ e2 : τ2 -∗ Γ ⊨ Pair e1 e2 : TProd τ1 τ2. Proof. iIntros "#He1 #He2". rewrite /sem_typed. iIntros "!#". iIntros (vs) "#Hvs". simpl. wp_bind (subst_map vs e2). iApply wp_wand. { by iApply "He2". } iIntros (w2) "Hw2". wp_bind (subst_map vs e1). iApply wp_wand. { by iApply "He1". } iIntros (w1) "Hw1". wp_pures. iExists w1, w2. iFrame. auto. Restart. iIntros "#He1 #He2 !#" (vs) "#Hvs /=". wp_apply (wp_wand with "(He2 [\$])"). iIntros (w2) "Hw2". wp_apply (wp_wand with "(He1 [\$])"). iIntros (w1) "Hw1". wp_pures; eauto. Qed. Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ → Γ ⊨ e : τ. Proof. intros Htyped. iInduction Htyped as [] "IH". 5:{ iApply Pair_sem_typed; auto. } (** Other cases left as an exercise to the reader *) Admitted. Lemma sem_typed_unsafe_pure : ∅ ⊨ (if: #true then #13 else #13 #37) : TInt. Proof. iIntros "!#" (vs) "Hvs /=". wp_pures. auto. Qed. End semtyp. Notation "Γ ⊨ e : A" := (sem_typed Γ e A) (at level 74, e, A at next level). Definition safe (e : expr) := ∀ σ es' e' σ', rtc erased_step ([e], σ) (es', σ') → e' ∈ es' → is_Some (to_val e') ∨ reducible e' σ'. Lemma sem_type_safety `{!heapPreG Σ} e τ : (∀ `{!heapG Σ}, ∅ ⊨ e : τ) → safe e. Proof. intros Hty σ es' e' σ'. apply (heap_adequacy Σ NotStuck e σ (λ _, True))=> // ?. iDestruct (Hty \$! ∅) as "#He". rewrite subst_map_empty. iApply (wp_wand with "(He [])"). { rewrite /interp_env. auto. } auto. Qed. Lemma type_safety e τ : ∅ ⊢ₜ e : τ → safe e. Proof. intros Hty. eapply (sem_type_safety (Σ:=heapΣ))=> ?. by apply fundamental. Qed.
 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.
 From tutorial_popl20 Require Export sem_typed sem_type_formers types. (** * Interpretation of syntactic types *) (** We use semantic type formers to define the interpretation [⟦ τ ⟧ : sem_ty] of syntactic types [τ : ty]. The interpretation is defined recursively on the structure of syntactic types. *) Reserved Notation "⟦ τ ⟧". Fixpoint interp `{!heapG Σ} (τ : ty) (ρ : list (sem_ty Σ)) : sem_ty Σ := match τ return _ with | TVar x => default () (ρ !! x) (* dummy in case [x ∉ ρ] *) | TUnit => () | TBool => sem_ty_bool | TInt => sem_ty_int | TProd τ1 τ2 => ⟦ τ1 ⟧ ρ * ⟦ τ2 ⟧ ρ | TSum τ1 τ2 => ⟦ τ1 ⟧ ρ + ⟦ τ2 ⟧ ρ | TArr τ1 τ2 => ⟦ τ1 ⟧ ρ → ⟦ τ2 ⟧ ρ | TForall τ => ∀ X, ⟦ τ ⟧ (X :: ρ) | TExist τ => ∃ X, ⟦ τ ⟧ (X :: ρ) | TRef τ => ref (⟦ τ ⟧ ρ) end%sem_ty where "⟦ τ ⟧" := (interp τ). Instance: Params (@interp) 2 := {}. (** Given a syntactic typing context [Γ : gmap string ty] (a mapping from variables [string] to syntactic types [ty]) together with a mapping [ρ : list (sem_ty Σ)] from type variables (that appear freely in [Γ]) to their corresponding semantic types (represented as a list, since de use De Bruijn indices for type variables), we define a semantic typing context [interp_env Γ ρ : gmap string (sem_ty Σ)], i.e., a mapping from variables (strings) to semantic types. *) Definition interp_env `{!heapG Σ} (Γ : gmap string ty) (ρ : list (sem_ty Σ)) : gmap string (sem_ty Σ) := flip interp ρ <\$> Γ. Instance: Params (@interp_env) 3 := {}. (** Below we prove several useful lemmas about [interp] and [interp_env], including important lemmas about the effect that lifting (de Bruijn indices) and substitution in type level variables have on the interpretation of syntactic types and typing contexts. *) Section interp_properties. Context `{!heapG Σ}. Implicit Types Γ : gmap string ty. Implicit Types τ : ty. Implicit Types ρ : list (sem_ty Σ). Implicit Types i n j : nat. Global Instance interp_ne τ : NonExpansive ⟦ τ ⟧. Proof. induction τ; solve_proper. Qed.