From f53e90782af7c113da18c7ed630726194a47f312 Mon Sep 17 00:00:00 2001
From: Benjamin Peters <bpeters@mpi-sws.org>
Date: Wed, 15 Nov 2023 15:21:28 +0100
Subject: [PATCH] Solution for exercises02

---
 _CoqProject                                   |   3 +
 theories/type_systems/stlc/cbn_logrel_sol.v   | 305 +++++++++++++
 .../type_systems/stlc_extended/logrel_sol.v   | 402 ++++++++++++++++++
 .../type_systems/systemf/exercises03_sol.v    | 108 +++++
 theories/type_systems/systemf/notation.v      |   3 +-
 .../type_systems/systemf/parallel_subst.v     |  48 +++
 6 files changed, 867 insertions(+), 2 deletions(-)
 create mode 100644 theories/type_systems/stlc/cbn_logrel_sol.v
 create mode 100644 theories/type_systems/stlc_extended/logrel_sol.v
 create mode 100644 theories/type_systems/systemf/exercises03_sol.v

diff --git a/_CoqProject b/_CoqProject
index 45fcbf7..1f133c0 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -33,6 +33,7 @@ theories/type_systems/stlc_extended/ctxstep.v
 theories/type_systems/stlc_extended/ctxstep_sol.v
 theories/type_systems/stlc_extended/parallel_subst.v
 theories/type_systems/stlc_extended/logrel.v
+theories/type_systems/stlc_extended/logrel_sol.v
 
 # System F
 theories/type_systems/systemf/lang.v
@@ -50,4 +51,6 @@ theories/type_systems/systemf/parallel_subst.v
 #theories/type_systems/stlc/exercises02.v
 #theories/type_systems/stlc/exercises02_sol.v
 #theories/type_systems/stlc/cbn_logrel.v
+#theories/type_systems/stlc/cbn_logrel_sol.v
 #theories/type_systems/systemf/exercises03.v
+#theories/type_systems/systemf/exercises03_sol.v
diff --git a/theories/type_systems/stlc/cbn_logrel_sol.v b/theories/type_systems/stlc/cbn_logrel_sol.v
new file mode 100644
index 0000000..f882261
--- /dev/null
+++ b/theories/type_systems/stlc/cbn_logrel_sol.v
@@ -0,0 +1,305 @@
+From stdpp Require Import base relations.
+From iris Require Import prelude.
+From semantics.lib Require Import sets maps.
+From semantics.ts.stlc Require Import lang notation types parallel_subst.
+From Equations Require Import Equations.
+
+Implicit Types
+  (Γ : typing_context)
+  (v : val)
+  (e : expr)
+  (A : type).
+
+(** *** Big-Step Semantics for cbn *)
+Inductive big_step : expr → val → Prop :=
+  | bs_lit (n : Z) :
+      big_step (LitInt n) (LitIntV n)
+  | bs_lam (x : binder) (e : expr) :
+      big_step (Lam x e) (LamV x e)
+  | bs_add e1 e2 (z1 z2 : Z) :
+      big_step e1 (LitIntV z1) →
+      big_step e2 (LitIntV z2) →
+      big_step (Plus e1 e2) (LitIntV (z1 + z2))%Z
+  | bs_app e1 e2 x e v2 v :
+      big_step e1 (@LamV x e) →
+      big_step (subst' x e2 e) v →
+      big_step (App e1 e2) v
+    .
+#[export] Hint Constructors big_step : core.
+
+
+Lemma big_step_vals (v: val): big_step (of_val v) v.
+Proof.
+  induction v; econstructor.
+Qed.
+
+Lemma big_step_inv_vals (v w: val): big_step (of_val v) w → v = w.
+Proof.
+  destruct v; inversion 1; eauto.
+Qed.
+
+
+
+(* *** Definition of the logical relation. *)
+(* We reuse most of these definitions. *)
+Inductive val_or_expr : Type :=
+| inj_val : val → val_or_expr
+| inj_expr : expr → val_or_expr.
+
+(* Note that we're using a slightly modified termination argument here. *)
+Equations type_size (t : type) : nat :=
+  type_size Int := 1;
+  type_size (Fun A B) := type_size A + type_size B + 2.
+Equations mut_measure (ve : val_or_expr) (t : type) : nat :=
+  mut_measure (inj_val _) t := type_size t;
+  mut_measure (inj_expr _) t := 1 + type_size t.
+
+Equations type_interp (ve : val_or_expr) (t : type) : Prop by wf (mut_measure ve t) := {
+  type_interp (inj_val v) Int =>
+    ∃ z : Z, v = z ;
+  type_interp (inj_val v) (A → B) =>
+    ∃ x e, v = @LamV x e ∧ closed (x :b: nil) e ∧
+      ∀ e',
+        type_interp (inj_expr e') A →
+        type_interp (inj_expr (subst' x e' e)) B;
+
+  type_interp (inj_expr e) t =>
+    (* we now need to explicitly require that expressions here are closed so
+       that we can apply them to lambdas directly. *)
+    ∃ v, big_step e v ∧ closed [] e ∧ type_interp (inj_val v) t
+}.
+Next Obligation.
+  repeat simp mut_measure; simp type_size; lia.
+Qed.
+Next Obligation.
+  simp mut_measure. simp type_size.
+  destruct A; repeat simp mut_measure; repeat simp type_size; lia.
+Qed.
+
+(* We derive the expression/value relation. *)
+Notation sem_val_rel t v := (type_interp (inj_val v) t).
+Notation sem_expr_rel t e := (type_interp (inj_expr e) t).
+
+Notation 𝒱 t v := (sem_val_rel t v).
+Notation ℰ t v := (sem_expr_rel t v).
+
+
+(* *** Semantic typing of contexts *)
+Implicit Types
+  (θ : gmap string expr).
+
+Inductive sem_context_rel : typing_context → (gmap string expr) → Prop :=
+  | sem_context_rel_empty : sem_context_rel ∅ ∅
+  (* contexts may now contain arbitrary (semantically well-typed) expressions
+     as opposed to just values. *)
+  | sem_context_rel_insert Γ θ e x A :
+    ℰ A e →
+    sem_context_rel Γ θ →
+    sem_context_rel (<[x := A]> Γ) (<[x := e]> θ).
+
+Notation 𝒢 := sem_context_rel.
+
+(* The semantic typing judgement. Note that we require e to be closed under Γ. *)
+Definition sem_typed Γ e A :=
+  closed (elements (dom Γ)) e ∧
+  ∀ θ, 𝒢 Γ θ → ℰ A (subst_map θ e).
+Notation "Γ ⊨ e : A" := (sem_typed Γ e A) (at level 74, e, A at next level).
+
+
+(* We start by proving a couple of helper lemmas that will be useful later. *)
+
+Lemma sem_expr_rel_of_val A v:
+  ℰ A v → 𝒱 A v.
+Proof.
+  simp type_interp.
+  intros (v' & ->%big_step_inv_vals & Hv').
+  apply Hv'.
+Qed.
+
+
+
+Lemma val_rel_closed v A:
+  𝒱 A v → closed [] v.
+Proof.
+  induction A; simp type_interp.
+  - intros [z ->]. done.
+  - intros (x & e & -> & Hcl & _). done.
+Qed.
+Lemma val_inclusion A v:
+  𝒱 A v → ℰ A v.
+Proof.
+  intros H. simp type_interp. eauto using big_step_vals, val_rel_closed.
+Qed.
+Lemma expr_rel_closed e A :
+  ℰ A e → closed [] e.
+Proof.
+  simp type_interp. intros (v & ? & ? & ?). done.
+Qed.
+Lemma sem_context_rel_closed Γ θ:
+  𝒢 Γ θ → subst_closed [] θ.
+Proof.
+  induction 1; rewrite /subst_closed.
+  - naive_solver.
+  - intros y e'. rewrite lookup_insert_Some.
+    intros [[-> <-]|[Hne Hlook]].
+    + by eapply expr_rel_closed.
+    + eapply IHsem_context_rel; last done.
+Qed.
+
+
+(* This is essentially an inversion lemma for 𝒢 *)
+Lemma sem_context_rel_exprs Γ θ x A :
+  sem_context_rel Γ θ →
+  Γ !! x = Some A →
+  ∃ e, θ !! x = Some e ∧ ℰ A e.
+Proof.
+  induction 1 as [|Γ θ e y B Hvals Hctx IH].
+  - naive_solver.
+  - rewrite lookup_insert_Some. intros [[-> ->]|[Hne Hlook]].
+    + eexists; first by rewrite lookup_insert.
+    + eapply IH in Hlook as (e' & Hlook & He).
+      eexists; split; first by rewrite lookup_insert_ne.
+      done.
+Qed.
+
+Lemma sem_context_rel_dom Γ θ :
+  𝒢 Γ θ → dom Γ = dom θ.
+Proof.
+  induction 1.
+  - by rewrite !dom_empty.
+  - rewrite !dom_insert. congruence.
+Qed.
+
+
+(* *** Compatibility lemmas *)
+Lemma compat_int Γ z : Γ ⊨ (LitInt z) : Int.
+Proof.
+  split; first done.
+  intros θ _. simp type_interp.
+  exists z. split; simpl.
+  - constructor.
+  - simp type_interp. eauto.
+Qed.
+
+Lemma compat_var Γ x A :
+  Γ !! x = Some A →
+  Γ ⊨ (Var x) : A.
+Proof.
+  intros Hx. split.
+  { eapply bool_decide_pack, elem_of_elements, elem_of_dom_2, Hx. }
+  intros θ Hctx; simpl.
+  eapply sem_context_rel_exprs in Hx as (e & Heq & He); last done.
+  rewrite Heq. done.
+Qed.
+
+Lemma compat_app Γ e1 e2 A B :
+  Γ ⊨ e1 : (A → B) →
+  Γ ⊨ e2 : A →
+  Γ ⊨ (e1 e2) : B.
+Proof.
+  intros [Hfuncl Hfun] [Hargcl Harg]. split.
+  { simpl. eauto. }
+  intros θ Hctx; simpl.
+  specialize (Hfun _ Hctx). simp type_interp in Hfun. destruct Hfun as (v1 & Hbs1 & Hcl1 & Hv1).
+  simp type_interp in Hv1. destruct Hv1 as (x & e & -> & Hcl & Hv1).
+  specialize (Harg _ Hctx). 
+  (* compare this to the cbv logical relation: in that case we now extract a
+     value from Harg. We don't need to do this here, since we don't need to
+     evaluate [subst_map θ e2] before applying it to [λ: x, e]. However, we do
+     need a closedness statement for e2, which we obtain from the definition of
+     ℰ. *)
+  specialize (expr_rel_closed _ _ Harg) as He2cl.
+
+  apply Hv1 in Harg.
+  simp type_interp in Harg. destruct Harg as (v & Hbsv & Hcl' & Hv).
+
+  simp type_interp.
+  exists v. repeat split.
+  - eauto.
+  - cbn. by apply andb_True. 
+  - eauto.
+Qed.
+
+
+Lemma lam_closed Γ θ (x : string) A e :
+  closed (elements (dom (<[x:=A]> Γ))) e → 
+  𝒢 Γ θ → 
+  closed [] (Lam x (subst_map (delete x θ) e)).
+Proof.
+  intros Hcl Hctxt.
+  eapply subst_map_closed'_2.
+  - eapply closed_weaken; first done.
+    rewrite dom_delete dom_insert (sem_context_rel_dom Γ θ) //.
+    intros y. destruct (decide (x = y)); set_solver.
+  - eapply subst_closed_weaken, sem_context_rel_closed; last done.
+    + set_solver.
+    + apply map_delete_subseteq.
+Qed.
+Lemma compat_lam Γ x e A B :
+  (<[ x := A ]> Γ) ⊨ e : B →
+  Γ ⊨ (Lam (BNamed x) e) : (A → B).
+Proof.
+  intros [Hbodycl Hbody]. split.
+  { simpl. eapply closed_weaken; first eassumption. set_solver. }
+  intros θ Hctxt. simpl. simp type_interp.
+  eexists.
+  split; first by eauto.
+  split; first by eapply lam_closed.
+  simp type_interp.
+  eexists _, _. split; first reflexivity.
+  split; first by eapply lam_closed.
+  intros e' He'.
+  specialize (Hbody (<[ x := e']> θ)).
+  simpl. rewrite subst_subst_map; last by eapply sem_context_rel_closed.
+  apply Hbody.
+  apply sem_context_rel_insert; done.
+Qed.
+
+Lemma compat_add Γ e1 e2 :
+  Γ ⊨ e1 : Int →
+  Γ ⊨ e2 : Int →
+  Γ ⊨ (e1 + e2) : Int.
+Proof.
+  intros [Hcl1 He1] [Hcl2 He2]. split.
+  { simpl. eauto. }
+  intros θ Hctx.
+  simp type_interp.
+  specialize (He1 _ Hctx). specialize (He2 _ Hctx).
+  simp type_interp in He1. simp type_interp in He2.
+
+  destruct He1 as (v1 & Hb1 & Hv1).
+  destruct He2 as (v2 & Hb2 & Hv2).
+  simp type_interp in Hv1, Hv2.
+  destruct Hv1 as (Hcl1' & z1 & ->). destruct Hv2 as (Hcl2' & z2 & ->).
+
+  exists (z1 + z2)%Z. repeat split.
+  - constructor; done.
+  - simpl. by apply andb_True.
+  - exists (z1 + z2)%Z. done.
+Qed.
+
+Lemma sem_soundness Γ e A :
+  (Γ ⊢ e : A)%ty →
+  Γ ⊨ e : A.
+Proof.
+  induction 1 as [ | Γ x e A B Hsyn IH | | | ].
+  - by apply compat_var.
+  - by apply compat_lam.
+  - apply compat_int.
+  - by eapply compat_app.
+  - by apply compat_add.
+Qed.
+
+Lemma termination e A :
+  (∅ ⊢ e : A)%ty →
+  ∃ v, big_step e v.
+Proof.
+  (* You may want to add suitable intermediate lemmas, like we did for the cbv
+     logical relation as seen in the lecture. *)
+  intros [Hsemcl Hsem]%sem_soundness.
+  specialize (Hsem ∅).
+  simp type_interp in Hsem.
+  rewrite subst_map_empty in Hsem.
+  destruct Hsem as (v & Hbs & _); last eauto.
+  constructor.
+Qed.
diff --git a/theories/type_systems/stlc_extended/logrel_sol.v b/theories/type_systems/stlc_extended/logrel_sol.v
new file mode 100644
index 0000000..29a9132
--- /dev/null
+++ b/theories/type_systems/stlc_extended/logrel_sol.v
@@ -0,0 +1,402 @@
+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.ts.stlc_extended Require Import lang notation parallel_subst types bigstep.
+From semantics.ts.stlc_extended Require Import lang notation parallel_subst types_sol bigstep_sol.
+From Equations Require Export Equations.
+
+
+
+(** * Logical relation for the extended STLC *)
+
+Implicit Types
+  (Γ : typing_context)
+  (v : val)
+  (e : expr)
+  (A : type).
+
+
+(* *** Definition of the logical relation. *)
+
+Inductive val_or_expr : Type :=
+| inj_val : val → val_or_expr
+| inj_expr : expr → val_or_expr.
+
+Equations type_size (A : type) : nat :=
+  type_size Int := 1;
+  type_size (A → B) := type_size A + type_size B + 1;
+  type_size (A × B) := type_size A + type_size B + 1;
+  type_size (A + B) := max (type_size A) (type_size B) + 1.
+Equations mut_measure (ve : val_or_expr) (t : type) : nat :=
+  mut_measure (inj_val _) t := type_size t;
+  mut_measure (inj_expr _) t := 1 + type_size t.
+
+
+Equations type_interp (ve : val_or_expr) (t : type) : Prop by wf (mut_measure ve t) := {
+  type_interp (inj_val v) Int =>
+    ∃ z : Z, v = #z ;
+  type_interp (inj_val v) (A × B) =>
+    ∃ v1 v2 : val, v = (v1, v2)%V ∧ type_interp (inj_val v1) A ∧ type_interp (inj_val v2) B;
+  type_interp (inj_val v) (A + B) =>
+    (∃ v' : val, v = InjLV v' ∧ type_interp (inj_val v') A) ∨
+    (∃ v' : val, v = InjRV v' ∧ type_interp (inj_val v') B);
+  type_interp (inj_val v) (A → B) =>
+    ∃ x e, v = @LamV x e ∧ closed (x :b: nil) e ∧
+      ∀ v',
+        type_interp (inj_val v') A →
+        type_interp (inj_expr (subst' x v' e)) B;
+
+  type_interp (inj_expr e) t =>
+    ∃ v, big_step e v ∧ type_interp (inj_val v) t
+}.
+Next Obligation.
+  repeat simp mut_measure; simp type_size; lia.
+Qed.
+Next Obligation.
+  simp mut_measure. simp type_size.
+  destruct A; repeat simp mut_measure; repeat simp type_size; lia.
+Qed.
+Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed.
+Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed.
+Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed.
+Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed.
+
+
+Notation sem_val_rel t v := (type_interp (inj_val v) t).
+Notation sem_expr_rel t e := (type_interp (inj_expr e) t).
+
+Notation 𝒱 t v := (sem_val_rel t v).
+Notation ℰ t v := (sem_expr_rel t v).
+
+
+(* *** Semantic typing of contexts *)
+Implicit Types
+  (θ : gmap string expr).
+
+Inductive sem_context_rel : typing_context → (gmap string expr) → Prop :=
+  | sem_context_rel_empty : sem_context_rel ∅ ∅
+  | sem_context_rel_insert Γ θ v x A :
+    𝒱 A v →
+    sem_context_rel Γ θ →
+    sem_context_rel (<[x := A]> Γ) (<[x := of_val v]> θ).
+
+Notation 𝒢 := sem_context_rel.
+
+Definition sem_typed Γ e A :=
+  closed (elements (dom Γ)) e ∧
+  ∀ θ, 𝒢 Γ θ → ℰ A (subst_map θ e).
+Notation "Γ ⊨ e : A" := (sem_typed Γ e A) (at level 74, e, A at next level).
+
+
+(* We start by proving a couple of helper lemmas that will be useful later. *)
+
+Lemma sem_expr_rel_of_val A v:
+  ℰ A v → 𝒱 A v.
+Proof.
+  simp type_interp.
+  intros (v' & ->%big_step_val & Hv').
+  apply Hv'.
+Qed.
+Lemma val_inclusion A v:
+  𝒱 A v → ℰ A v.
+Proof.
+  intros H. simp type_interp. eauto using big_step_of_val.
+Qed.
+
+
+
+Lemma val_rel_closed v A:
+  𝒱 A v → closed [] v.
+Proof.
+  induction A in v |-*; simp type_interp.
+  - intros [z ->]. done.
+  - intros (x & e & -> & Hcl & _). done.
+  - intros (v1 & v2 & -> & H1 & H2). unfold closed. simpl. naive_solver.
+  - intros [(v' & -> & Hv) | (v' & -> & Hv)]; naive_solver.
+Qed.
+Lemma sem_context_rel_closed Γ θ:
+  𝒢 Γ θ → subst_closed [] θ.
+Proof.
+  induction 1; rewrite /subst_closed.
+  - naive_solver.
+  - intros y e. rewrite lookup_insert_Some.
+    intros [[-> <-]|[Hne Hlook]].
+    + by eapply val_rel_closed.
+    + eapply IHsem_context_rel; last done.
+Qed.
+
+
+(* This is essentially an inversion lemma for 𝒢 *)
+Lemma sem_context_rel_vals Γ θ x A :
+  𝒢 Γ θ →
+  Γ !! x = Some A →
+  ∃ e v, θ !! x = Some e ∧ to_val e = Some v ∧ 𝒱 A v.
+Proof.
+  induction 1 as [|Γ θ v y B Hvals Hctx IH].
+  - naive_solver.
+  - rewrite lookup_insert_Some. intros [[-> ->]|[Hne Hlook]].
+    + do 2 eexists. split; first by rewrite lookup_insert.
+      split; first by eapply to_of_val. done.
+    + eapply IH in Hlook as (e & w & Hlook & He & Hval).
+      do 2 eexists; split; first by rewrite lookup_insert_ne.
+      split; first done. done.
+Qed.
+
+Lemma sem_context_rel_dom Γ θ :
+  𝒢 Γ θ → dom Γ = dom θ.
+Proof.
+  induction 1.
+  - by rewrite !dom_empty.
+  - rewrite !dom_insert. congruence.
+Qed.
+
+
+(* *** Compatibility lemmas *)
+Lemma compat_int Γ z : Γ ⊨ (LitInt z) : Int.
+Proof.
+  split; first done.
+  intros θ _. simp type_interp.
+  exists #z. split; simpl.
+  - constructor.
+  - simp type_interp. eauto.
+Qed.
+
+Lemma compat_var Γ x A :
+  Γ !! x = Some A →
+  Γ ⊨ (Var x) : A.
+Proof.
+  intros Hx. split.
+  { eapply bool_decide_pack, elem_of_elements, elem_of_dom_2, Hx. }
+  intros θ Hctx; simpl.
+  eapply sem_context_rel_vals in Hx as (e & v & He & Heq & Hv); last done.
+  rewrite He. simp type_interp. exists v. split; last done.
+  rewrite -(of_to_val _ _ Heq).
+  by apply big_step_of_val.
+Qed.
+
+Lemma compat_app Γ e1 e2 A B :
+  Γ ⊨ e1 : (A → B) →
+  Γ ⊨ e2 : A →
+  Γ ⊨ (e1 e2) : B.
+Proof.
+  intros [Hfuncl Hfun] [Hargcl Harg]. split.
+  { unfold closed. simpl. eauto. }
+  intros θ Hctx; simpl.
+  specialize (Hfun _ Hctx). simp type_interp in Hfun. destruct Hfun as (v1 & Hbs1 & Hv1).
+  simp type_interp in Hv1. destruct Hv1 as (x & e & -> & Hcl & Hv1).
+  specialize (Harg _ Hctx). simp type_interp in Harg.
+  destruct Harg as (v2 & Hbs2 & Hv2).
+
+  apply Hv1 in Hv2.
+  simp type_interp in Hv2. destruct Hv2 as (v & Hbsv & Hv).
+
+  simp type_interp.
+  exists v. split; last done.
+  eauto.
+Qed.
+
+
+(* Compatibility for [lam] unfortunately needs a very technical helper lemma. *)
+Lemma lam_closed Γ θ (x : string) A e :
+  closed (elements (dom (<[x:=A]> Γ))) e → 
+  𝒢 Γ θ → 
+  closed [] (Lam x (subst_map (delete x θ) e)).
+Proof.
+  intros Hcl Hctxt.
+  eapply subst_map_closed'_2.
+  - eapply is_closed_weaken; first done.
+    rewrite dom_delete dom_insert (sem_context_rel_dom Γ θ) //.
+    intros y. destruct (decide (x = y)); set_solver.
+  - eapply subst_closed_weaken, sem_context_rel_closed; last done.
+    + set_solver.
+    + apply map_delete_subseteq.
+Qed.
+Lemma compat_lam Γ x e A B :
+  (<[ x := A ]> Γ) ⊨ e : B →
+  Γ ⊨ (Lam (BNamed x) e) : (A → B).
+Proof.
+  intros [Hbodycl Hbody]. split.
+  { unfold closed in *. cbn in *. eapply is_closed_weaken; first eassumption.
+    set_solver. }
+  intros θ Hctxt. simpl. simp type_interp.
+  eexists.
+  split; first by eauto.
+  simp type_interp.
+  eexists x, _. split; first reflexivity.
+  split; first by eapply lam_closed.
+  intros v' Hv'.
+  specialize (Hbody (<[ x := of_val v']> θ)).
+  simpl. rewrite subst_subst_map; last by eapply sem_context_rel_closed.
+  apply Hbody.
+  apply sem_context_rel_insert; done.
+Qed.
+Lemma compat_lam_anon Γ e A B :
+  Γ ⊨ e : B →
+  Γ ⊨ (Lam BAnon e) : (A → B).
+Proof.
+  intros [Hbodycl Hbody]. split; first done.
+  intros θ Hctxt. simpl. simp type_interp.
+  eexists.
+  split; first by eauto.
+  simp type_interp.
+  eexists _, _. split; first reflexivity.
+  split.
+  { simpl. eapply subst_map_closed'_2; simpl.
+    - by erewrite <-sem_context_rel_dom.
+    - by eapply sem_context_rel_closed. }
+  naive_solver.
+Qed.
+
+Lemma compat_add Γ e1 e2 :
+  Γ ⊨ e1 : Int →
+  Γ ⊨ e2 : Int →
+  Γ ⊨ (e1 + e2) : Int.
+Proof.
+  intros [Hcl1 He1] [Hcl2 He2]. split.
+  { unfold closed in *. naive_solver. }
+  intros θ Hctx.
+  simp type_interp.
+  specialize (He1 _ Hctx). specialize (He2 _ Hctx).
+  simp type_interp in He1. simp type_interp in He2.
+
+  destruct He1 as (v1 & Hb1 & Hv1).
+  destruct He2 as (v2 & Hb2 & Hv2).
+  simp type_interp in Hv1, Hv2.
+  destruct Hv1 as (z1 & ->). destruct Hv2 as (z2 & ->).
+
+  exists #(z1 + z2). split.
+  - constructor; done.
+  - exists (z1 + z2)%Z. done.
+
+Qed.
+
+
+Lemma compat_pair Γ e1 e2 A B :
+  Γ ⊨ e1 : A →
+  Γ ⊨ e2 : B →
+  Γ ⊨ (e1, e2) : A × B.
+Proof.
+  intros [Hcl1 He1] [Hcl2 He2]. split.
+  { unfold closed. naive_solver. }
+  intros θ Hctx. simpl.
+  simp type_interp.
+  specialize (He1 _ Hctx). simp type_interp in He1.
+  destruct He1 as (v1 & Hb1 & Hv1).
+  specialize (He2 _ Hctx). simp type_interp in He2.
+  destruct He2 as (v2 & Hb2 & Hv2).
+  exists (v1, v2)%V. split; first eauto.
+  simp type_interp. exists v1, v2. done.
+Qed.
+
+Lemma compat_fst Γ e A B :
+  Γ ⊨ e : A × B →
+  Γ ⊨ Fst e : A.
+Proof.
+  intros [Hcl He]. split; first naive_solver.
+  intros θ Hctx. simpl.
+  simp type_interp.
+  specialize (He _ Hctx). simp type_interp in He.
+  destruct He as (v & Hb & Hv).
+  simp type_interp in Hv. destruct Hv as (v1 & v2 & -> & Hv1 & Hv2).
+  exists v1. split; first eauto. done.
+Qed.
+
+Lemma compat_snd Γ e A B :
+  Γ ⊨ e : A × B →
+  Γ ⊨ Snd e : B.
+Proof.
+  intros [Hcl He]. split; first naive_solver.
+  intros θ Hctx. simpl.
+  simp type_interp.
+  specialize (He _ Hctx). simp type_interp in He.
+  destruct He as (v & Hb & Hv).
+  simp type_interp in Hv. destruct Hv as (v1 & v2 & -> & Hv1 & Hv2).
+  exists v2. split; first eauto. done.
+Qed.
+
+Lemma compat_injl Γ e A B :
+  Γ ⊨ e : A →
+  Γ ⊨ InjL e : A + B.
+Proof.
+  intros [Hcl He]. split; first naive_solver.
+  intros θ Hctx. simpl.
+  simp type_interp.
+  specialize (He _ Hctx). simp type_interp in He.
+  destruct He as (v & Hb & Hv).
+  exists (InjLV v). split; first eauto.
+  simp type_interp. eauto.
+Qed.
+
+Lemma compat_injr Γ e A B :
+  Γ ⊨ e : B →
+  Γ ⊨ InjR e : A + B.
+Proof.
+  intros [Hcl He]. split; first naive_solver.
+  intros θ Hctx. simpl.
+  simp type_interp.
+  specialize (He _ Hctx). simp type_interp in He.
+  destruct He as (v & Hb & Hv).
+  exists (InjRV v). split; first eauto.
+  simp type_interp. eauto.
+Qed.
+
+Lemma compat_case Γ e e1 e2 A B C :
+  Γ ⊨ e : B + C →
+  Γ ⊨ e1 : (B → A) →
+  Γ ⊨ e2 : (C → A) →
+  Γ ⊨ Case e e1 e2 : A.
+Proof.
+  intros [Hcl He] [Hcl1 He1] [Hcl2 He2]. split.
+  { unfold closed. naive_solver. }
+  intros θ Hctx. simpl.
+  simp type_interp.
+  specialize (He _ Hctx). simp type_interp in He.
+  destruct He as (v & Hb & Hv).
+  simp type_interp in Hv. destruct Hv as [(v' & -> & Hv') | (v' & -> & Hv')].
+  - specialize (He1 _ Hctx). simp type_interp in He1.
+    destruct He1 as (v & Hb' & Hv).
+    simp type_interp in Hv. destruct Hv as (x & e' & -> & Cl & Hv).
+    apply Hv in Hv'. simp type_interp in Hv'. destruct Hv' as (v & Hb'' & Hv'').
+    exists v. split; last done.
+    econstructor; first done.
+    econstructor; [done | apply big_step_of_val; done | done].
+  - specialize (He2 _ Hctx). simp type_interp in He2.
+    destruct He2 as (v & Hb' & Hv).
+    simp type_interp in Hv. destruct Hv as (x & e' & -> & Cl & Hv).
+    apply Hv in Hv'. simp type_interp in Hv'. destruct Hv' as (v & Hb'' & Hv'').
+    exists v. split; last done.
+    econstructor; first done.
+    econstructor; [done | apply big_step_of_val; done | done].
+Qed.
+
+Lemma sem_soundness Γ e A :
+  (Γ ⊢ e : A)%ty →
+  Γ ⊨ e : A.
+Proof.
+  induction 1.
+  - by apply compat_var.
+  - by apply compat_lam.
+  - by apply compat_lam_anon.
+  - apply compat_int.
+  - by eapply compat_app.
+  - by apply compat_add.
+  (* add compatibility lemmas for the new rules here. *)
+  - by apply compat_pair.
+  - by eapply compat_fst.
+  - by eapply compat_snd.
+  - by eapply compat_injl.
+  - by eapply compat_injr.
+  - by eapply compat_case.
+Qed.
+
+Lemma termination e A :
+  (∅ ⊢ e : A)%ty →
+  ∃ v, big_step e v.
+Proof.
+  intros [Hsemcl Hsem]%sem_soundness.
+  specialize (Hsem ∅).
+  simp type_interp in Hsem.
+  rewrite subst_map_empty in Hsem.
+  destruct Hsem as (v & Hbs & _); last eauto.
+  constructor.
+Qed.
+
diff --git a/theories/type_systems/systemf/exercises03_sol.v b/theories/type_systems/systemf/exercises03_sol.v
new file mode 100644
index 0000000..15480a2
--- /dev/null
+++ b/theories/type_systems/systemf/exercises03_sol.v
@@ -0,0 +1,108 @@
+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.ts.systemf Require Import lang notation types tactics.
+
+(** Exercise 3 (LN Exercise 22): Universal Fun *)
+
+Definition fun_comp : val :=
+  Λ, Λ, Λ, λ: "f" "g" "x", "g" ("f" "x").
+Definition fun_comp_type : type :=
+  ∀: ∀: ∀: (#2 → #1) → (#1 → #0) → #2 → #0.
+Lemma fun_comp_typed :
+  TY 0; ∅ ⊢ fun_comp : fun_comp_type.
+Proof. 
+  (* should be solved by solve_typing. *)
+  solve_typing. 
+Qed.
+
+Definition swap_args : val :=
+  Λ, Λ, Λ, λ: "f" "x" "y", "f" "y" "x".
+Definition swap_args_type : type :=
+  ∀: ∀: ∀: (#2 → #1 → #0) → #1 → #2 → #0.
+Lemma swap_args_typed :
+  TY 0; ∅ ⊢ swap_args : swap_args_type.
+Proof. 
+  (* should be solved by solve_typing. *)
+  solve_typing. 
+Qed.
+
+Definition lift_prod : val :=
+  Λ, Λ, Λ, Λ, λ: "f" "g" "p", ("f" (Fst "p"), "g" (Snd "p")).
+Definition lift_prod_type : type :=
+  (∀: ∀: ∀: ∀: (#3 → #1) → (#2 → #0) → #3 × #2 → #1 × #0).
+Lemma lift_prod_typed :
+  TY 0; ∅ ⊢ lift_prod : lift_prod_type.
+Proof. 
+  (* should be solved by solve_typing. *)
+  solve_typing. 
+Qed.
+
+Definition lift_sum : val :=
+  Λ, Λ, Λ, Λ, λ: "f" "g" "s",
+    match: "s" with
+      InjL "x" => InjL ("f" "x")
+    | InjR "x" => InjR ("g" "x")
+    end.
+Definition lift_sum_type : type :=
+  (∀: ∀: ∀: ∀: (#3 → #1) → (#2 → #0) → #3 + #2 → #1 + #0).
+Lemma lift_sum_typed :
+  TY 0; ∅ ⊢ lift_sum : lift_sum_type.
+Proof. 
+  (* should be solved by solve_typing. *)
+  solve_typing. 
+Qed.
+
+(** Exercise 5 (LN Exercise 18): Named to De Bruijn *)
+Inductive ptype : Type :=
+  | PTVar : string → ptype
+  | PInt
+  | PBool
+  | PTForall : string → ptype → ptype
+  | PTExists : string → ptype → ptype
+  | PFun (A B : ptype).
+
+Declare Scope PType_scope.
+Delimit Scope PType_scope with pty.
+Bind Scope PType_scope with ptype.
+Coercion PTVar: string >-> ptype.
+Infix "→" := PFun : PType_scope.
+Notation "∀:  x , τ" :=
+    (PTForall x τ%pty)
+    (at level 100, τ at level 200) : PType_scope.
+Notation "∃:  x , τ" :=
+    (PTExists x τ%pty)
+    (at level 100, τ at level 200) : PType_scope.
+
+Fixpoint debruijn (m: gmap string nat) (A: ptype) : option type :=
+   match A with
+  | PTVar x => match m !! x with None => None | Some n => Some (TVar n) end
+  | PInt => Some Int
+  | PBool => Some Bool
+  | PFun A B => match debruijn m A, debruijn m B with Some A, Some B => Some (A → B)%ty | _, _ => None end
+  | PTForall x A =>
+    let m' := <[x := 0]> (S <$> m) in
+    match debruijn m' A with None => None | Some A => Some (TForall A) end
+  | PTExists x A =>
+    let m' := <[x := 0]> (S <$> m) in
+    match debruijn m' A with None => None | Some A => Some (TExists A) end
+  end.
+
+(* Example *)
+Goal debruijn ∅ (∀: "x", ∀: "y", "x" → "y")%pty = Some (∀: ∀: #1 → #0)%ty.
+Proof.
+  (* Should be solved by reflexivity. *)
+  reflexivity.
+Qed.
+
+Goal debruijn ∅ (∀: "x", "x" → ∀: "y", "y")%pty = Some (∀: #0 → ∀: #0)%ty.
+Proof.
+  (* Should be solved by reflexivity. *)
+  reflexivity.
+Qed.
+
+Goal debruijn ∅ (∀: "x", "x" → ∀: "y", "x")%pty = Some (∀: #0 → ∀: #1)%ty.
+Proof.
+  (* Should be solved by reflexivity. *)
+  reflexivity.
+Qed.
+
diff --git a/theories/type_systems/systemf/notation.v b/theories/type_systems/systemf/notation.v
index 563b111..83c2230 100644
--- a/theories/type_systems/systemf/notation.v
+++ b/theories/type_systems/systemf/notation.v
@@ -61,8 +61,7 @@ Notation "λ: x y .. z , e" := (LamV x%binder (Lam y%binder .. (Lam z%binder e%E
    format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.
 
 Notation "'let:' x := e1 'in' e2" := (Lam x%binder e2%E e1%E)
-  (at level 200, x at level 1, e1, e2 at level 200,
-   format "'[' 'let:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : expr_scope.
+  (only parsing, at level 200, x at level 1, e1, e2 at level 200) : expr_scope.
 Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
   (at level 100, e2 at level 200,
    format "'[' '[hv' '[' e1 ']' ;;  ']' '/' e2 ']'") : expr_scope.
diff --git a/theories/type_systems/systemf/parallel_subst.v b/theories/type_systems/systemf/parallel_subst.v
index 8f8987b..29ad195 100644
--- a/theories/type_systems/systemf/parallel_subst.v
+++ b/theories/type_systems/systemf/parallel_subst.v
@@ -178,3 +178,51 @@ Proof.
               end.
   all: naive_solver.
 Qed.
+
+Lemma subst_map_closed' X Y Θ e:
+  is_closed Y e →
+  (∀ x, x ∈ Y → if Θ !! x is (Some e') then closed X e' else x ∈ X) →
+  is_closed X (subst_map Θ e).
+Proof.
+  induction e in X, Θ, Y |-*; simpl.
+  2: { 
+    intros Hel%bool_decide_unpack Hcl.
+    eapply Hcl in Hel.
+    destruct (Θ !! x); first done.
+    simpl. by eapply bool_decide_pack. }
+  2: { 
+    intros Hcl Hcl'. destruct x as [|x]; simpl; first naive_solver. 
+    eapply IHe; first done.
+    intros y [|]%elem_of_cons.
+    + subst. rewrite lookup_delete. set_solver.
+    + destruct (decide (x = y)); first by subst; rewrite lookup_delete; set_solver.
+      rewrite lookup_delete_ne //=. eapply Hcl' in H.
+      destruct lookup; last set_solver.
+      eapply is_closed_weaken; eauto with set_solver. }
+  9: {
+    intros [Hcl1 Hcl2]%andb_True H.
+    apply andb_True. split; first eauto.
+    destruct x as [|x]; simpl; first naive_solver.
+    eapply IHe2; first done.
+    intros y [|H0]%elem_of_cons.
+    + subst. rewrite lookup_delete. set_solver.
+    + destruct (decide (x = y)); first by subst; rewrite lookup_delete; set_solver.
+      rewrite lookup_delete_ne //=. eapply H in H0.
+      destruct lookup; last set_solver.
+      eapply is_closed_weaken; eauto with set_solver.
+  }
+  all: try naive_solver.
+Qed.
+
+Lemma subst_map_closed X θ e:
+  is_closed (X ++ (elements (dom θ))) e ->
+  subst_is_closed X θ ->
+  is_closed X (subst_map θ e).
+Proof.
+  intros Hcl Hsubst.
+  eapply subst_map_closed'; first eassumption.
+  intros x Hx.
+  destruct (θ !! x) as [e'|] eqn:Heq.
+  - eauto.
+  - by eapply elem_of_app in Hx as [H|H%elem_of_elements%not_elem_of_dom].
+Qed.