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 1/2] 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.

From 70e61abdcb51e7937dc9818dffcd85f36ed9e334 Mon Sep 17 00:00:00 2001
From: Benjamin Peters <bpeters@mpi-sws.org>
Date: Thu, 16 Nov 2023 17:07:19 +0100
Subject: [PATCH 2/2] Release exercise 04

---
 _CoqProject                                   |   3 +
 theories/type_systems/systemf/exercises04.v   | 279 +++++++
 theories/type_systems/systemf/free_theorems.v |  55 ++
 theories/type_systems/systemf/logrel.v        | 753 ++++++++++++++++++
 4 files changed, 1090 insertions(+)
 create mode 100644 theories/type_systems/systemf/exercises04.v
 create mode 100644 theories/type_systems/systemf/free_theorems.v
 create mode 100644 theories/type_systems/systemf/logrel.v

diff --git a/_CoqProject b/_CoqProject
index 1f133c0..78b6690 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -42,6 +42,8 @@ theories/type_systems/systemf/types.v
 theories/type_systems/systemf/tactics.v
 theories/type_systems/systemf/bigstep.v
 theories/type_systems/systemf/parallel_subst.v
+theories/type_systems/systemf/logrel.v
+theories/type_systems/systemf/free_theorems.v
 
 # By removing the # below, you can add the exercise sheets to make
 #theories/type_systems/warmup/warmup.v
@@ -54,3 +56,4 @@ theories/type_systems/systemf/parallel_subst.v
 #theories/type_systems/stlc/cbn_logrel_sol.v
 #theories/type_systems/systemf/exercises03.v
 #theories/type_systems/systemf/exercises03_sol.v
+#theories/type_systems/systemf/exercises04.v
diff --git a/theories/type_systems/systemf/exercises04.v b/theories/type_systems/systemf/exercises04.v
new file mode 100644
index 0000000..df39922
--- /dev/null
+++ b/theories/type_systems/systemf/exercises04.v
@@ -0,0 +1,279 @@
+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.ts.systemf Require Import lang notation parallel_subst types logrel tactics.
+
+(** Exercise 1 (LN Exercise 19): De Bruijn Terms *)
+Module dbterm.
+  (** Your type of expressions only needs to encompass the operations of our base lambda calculus. *)
+  Inductive expr :=
+    | Lit (l : base_lit)
+    | Var (n : nat)
+    | Lam (e : expr)
+    | Plus (e1 e2 : expr)
+    | App (e1 e2 : expr)
+  .
+
+  (** Formalize substitutions and renamings as functions. *)
+  Definition subt := nat → expr.
+  Definition rent := nat → nat.
+
+  Implicit Types
+    (σ : subt)
+    (δ : rent)
+    (n x : nat)
+    (e : expr).
+
+  Fixpoint subst σ e :=
+    (* FIXME *) e.
+
+  
+
+  Goal (subst
+    (λ n, match n with
+          | 0 => Lit (LitInt 42)
+          | 1 => Var 0
+          | _ => Var n
+          end)
+    (Lam (Plus (Plus (Var 2) (Var 1)) (Var 0)))) = 
+    Lam (Plus (Plus (Var 1) (Lit 42%Z)) (Var 0)).
+  Proof.
+    cbn. 
+    (* Should be by reflexivity. *)
+    (* TODO: exercise *)
+  Admitted.
+
+
+End dbterm.
+
+Section church_encodings.
+  (** Exercise 2 (LN Exercise 24): Church encoding, sum types *)
+  (* a) Define your encoding *)
+  Definition sum_type (A B : type) : type := #0 (* FIXME *).
+    
+
+  (* b) Implement inj1, inj2, case *)
+  Definition injl_val (v : val) : val := #0 (* FIXME *).
+  Definition injl_expr (e : expr) : expr := #0 (* FIXME *).
+  Definition injr_val (v : val) : val := #0 (* FIXME *).
+  Definition injr_expr (e : expr) : expr := #0 (* FIXME *).
+
+  (* You may want to use the variables x1, x2 for the match arms to fit the typing statements below. *)
+  Definition match_expr (e : expr) (e1 e2 : expr) : expr := #0. (* FIXME *)
+    
+
+  (* c) Reduction behavior *)
+  (* Some lemmas about substitutions might be useful. Look near the end of the lang.v file! *)
+  Lemma match_expr_red_injl e e1 e2 (vl v' : val) :
+    is_closed [] vl →
+    is_closed ["x1"] e1 →
+    big_step e (injl_val vl) →
+    big_step (subst' "x1" vl e1) v' →
+    big_step (match_expr e e1 e2) v'.
+  Proof.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  Lemma match_expr_red_injr e e1 e2 (vl v' : val) :
+    is_closed [] vl →
+    big_step e (injr_val vl) →
+    big_step (subst' "x2" vl e2) v' →
+    big_step (match_expr e e1 e2) v'.
+  Proof.
+    intros. bs_step_det.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  Lemma injr_expr_red e v :
+    big_step e v →
+    big_step (injr_expr e) (injr_val v).
+  Proof.
+    intros. bs_step_det.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  Lemma injl_expr_red e v :
+    big_step e v →
+    big_step (injl_expr e) (injl_val v).
+  Proof.
+    intros. bs_step_det.
+    (* TODO: exercise *)
+  Admitted.
+
+
+
+  (* d) Typing rules *)
+  Lemma sum_injl_typed n Γ (e : expr) A B :
+    type_wf n B →
+    type_wf n A →
+    TY n; Γ ⊢ e : A →
+    TY n; Γ ⊢ injl_expr e : sum_type A B.
+  Proof.
+    intros. solve_typing.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  Lemma sum_injr_typed n Γ e A B :
+    type_wf n B →
+    type_wf n A →
+    TY n; Γ ⊢ e : B →
+    TY n; Γ ⊢ injr_expr e : sum_type A B.
+  Proof.
+    intros. solve_typing.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  Lemma sum_match_typed n Γ A B C e e1 e2 :
+    type_wf n A →
+    type_wf n B →
+    type_wf n C →
+    TY n; Γ ⊢ e : sum_type A B →
+    TY n; <["x1" := A]> Γ ⊢ e1 : C →
+    TY n; <["x2" := B]> Γ ⊢ e2 : C →
+    TY n; Γ ⊢ match_expr e e1 e2 : C.
+  Proof.
+    intros. solve_typing.
+    (* TODO: exercise *)
+  Admitted.
+
+
+
+  (** Exercise 3 (LN Exercise 25): church encoding, list types *)
+
+  (* a) translate the type of lists into De Bruijn. *)
+  Definition list_type (A : type) : type := #0 (* FIXME *).
+    
+
+  (* b) Implement nil and cons. *)
+  Definition nil_val : val := #0 (* FIXME *).
+  Definition cons_val (v1 v2 : val) : val := #0 (* FIXME *).
+  Definition cons_expr (e1 e2 : expr) : expr := #0 (* FIXME *).
+
+  (* c) Define typing rules and prove them *)
+  Lemma nil_typed n Γ A :
+    type_wf n A →
+    TY n; Γ ⊢ nil_val : list_type A.
+  Proof.
+    intros. solve_typing.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  Lemma cons_typed n Γ (e1 e2 : expr) A :
+    type_wf n A →
+    TY n; Γ ⊢ e2 : list_type A →
+    TY n; Γ ⊢ e1 : A →
+    TY n; Γ ⊢ cons_expr e1 e2 : list_type A.
+  Proof.
+    intros. repeat solve_typing.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  (* d) Define a function head of type list A → A + 1 *)
+  Definition head : val := #0 (* FIXME *).
+    
+
+  Lemma head_typed n Γ A :
+    type_wf n A →
+    TY n; Γ ⊢ head: (list_type A → (A + Unit)).
+  Proof.
+    intros. solve_typing.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  (* e) Define a function [tail] of type list A → list A *)
+  
+  Definition tail : val := #0 (* FIXME *).
+    
+
+  Lemma tail_typed n Γ A :
+    type_wf n A →
+    TY n; Γ ⊢ tail: (list_type A → list_type A).
+  Proof.
+    intros. repeat solve_typing.
+    (* TODO: exercise *)
+  Admitted.
+
+
+End church_encodings.
+
+Section free_theorems.
+
+  (** Exercise 4 (LN Exercise 27): Free Theorems I *)
+  (* a) State a free theorem for the type ∀ α, β. α → β → α × β *)
+  Lemma free_thm_1 :
+    ∀ f : val,
+    TY 0; ∅ ⊢ f : (∀: ∀: #1 → #0 → #1 × #0) →
+    True (* FIXME state your theorem *).
+  Proof.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  (* b) State a free theorem for the type ∀ α, β. α × β → α *)
+  Lemma free_thm_2 :
+    ∀ f : val,
+    TY 0; ∅ ⊢ f : (∀: ∀: #1 × #0 → #1) →
+    True (* FIXME state your theorem *).
+  Proof.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  (* c) State a free theorem for the type ∀ α, β. α → β *)
+  Lemma free_thm_3 :
+    ∀ f : val,
+    TY 0; ∅ ⊢ f : (∀: ∀: #1 → #0) →
+    True (* FIXME state your theorem *).
+  Proof.
+    (* TODO: exercise *)
+  Admitted.
+
+
+
+  (** Exercise 5 (LN Exercise 28): Free Theorems II *)
+  Lemma free_theorem_either :
+    ∀ f : val,
+    TY 0; ∅ ⊢ f : (∀: #0 → #0 → #0) →
+    ∀ (v1 v2 : val), is_closed [] v1 → is_closed [] v2 →
+      big_step (f <> v1 v2) v1 ∨ big_step (f <> v1 v2) v2.
+  Proof.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  (** Exercise 6 (LN Exercise 29): Free Theorems III *)
+  (* Hint: you might want to use the fact that our reduction is deterministic. *)
+  Lemma big_step_det e v1 v2 :
+    big_step e v1 → big_step e v2 → v1 = v2.
+  Proof.
+    induction 1 in v2 |-*; inversion 1; subst; eauto 2.
+    all: naive_solver.
+  Qed.
+
+  Lemma free_theorems_magic :
+    ∀ (A A1 A2 : type) (f g : val),
+    type_wf 0 A → type_wf 0 A1 → type_wf 0 A2 →
+    is_closed [] f → is_closed [] g →
+    TY 0; ∅ ⊢ f : (∀: (A1 → A2 → #0) → #0) →
+    TY 0; ∅ ⊢ g : (A1 → A2 → A) →
+    ∀ v, big_step (f <> g) v →
+    ∃ (v1 v2 : val), big_step (g v1 v2) v.
+  Proof.
+    (* Hint: you may find the following lemmas useful:
+        - [sem_val_rel_cons]
+        - [type_wf_closed]
+        - [val_rel_is_closed]
+        - [big_step_preserve_closed]
+    *)
+    (* TODO: exercise *)
+  Admitted.
+
+
+End free_theorems.
diff --git a/theories/type_systems/systemf/free_theorems.v b/theories/type_systems/systemf/free_theorems.v
new file mode 100644
index 0000000..a649148
--- /dev/null
+++ b/theories/type_systems/systemf/free_theorems.v
@@ -0,0 +1,55 @@
+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.lib Require Export debruijn.
+From semantics.ts.systemf Require Import lang notation parallel_subst types bigstep tactics logrel.
+From Equations Require Import Equations.
+
+(** * Free Theorems *)
+Implicit Types
+  (Δ : nat)
+  (Γ : typing_context)
+  (v : val)
+  (α : var)
+  (e : expr)
+  (A : type).
+
+Lemma not_every_type_inhabited : ¬ ∃ e, TY 0; ∅ ⊢ e : (∀: #0).
+Proof.
+  intros (e & [Htycl Hty]%sem_soundness).
+  specialize (Hty ∅ δ_any). simp type_interp in Hty.
+  destruct Hty as (v & Hb & Hv).
+  { constructor. }
+  simp type_interp in Hv. destruct Hv as (e' & -> & Hcl & Ha).
+  (* [specialize_sem_type] defines a semantic type, spawning a subgoal for the closedness sidecondition *)
+  specialize_sem_type Ha with (λ _, False) as τ; first done.
+  simp type_interp in Ha. destruct Ha as (v' & He' & Hv').
+  simp type_interp in Hv'. simpl in Hv'.
+  done.
+Qed.
+
+Lemma all_identity :
+  ∀ e,
+  TY 0; ∅ ⊢ e : (∀: #0 → #0) →
+  ∀ v, is_closed [] v → big_step (e <> (of_val v)) v.
+Proof.
+  intros e [Htycl Hty]%sem_soundness v0 Hcl_v0.
+  specialize (Hty ∅ δ_any). simp type_interp in Hty.
+  destruct Hty as (v & Hb & Hv).
+  { constructor. }
+
+  simp type_interp in Hv. destruct Hv as (e' & -> & Hcl & Hv).
+  specialize_sem_type Hv with (λ v, v = v0) as τ.
+  { intros v ->; done. }
+  simp type_interp in Hv.
+
+  destruct Hv as (v & He & Hv).
+  simp type_interp in Hv.
+  destruct Hv as (x & e'' & -> & Hcl' & Hv).
+  specialize (Hv v0 ltac:(done)).
+
+  simp type_interp in Hv. destruct Hv as (v & Hb' & Hv).
+  simp type_interp in Hv; simpl in Hv. subst v.
+
+  rewrite subst_map_empty in Hb.
+  eauto using big_step_of_val.
+Qed.
diff --git a/theories/type_systems/systemf/logrel.v b/theories/type_systems/systemf/logrel.v
new file mode 100644
index 0000000..a8757cf
--- /dev/null
+++ b/theories/type_systems/systemf/logrel.v
@@ -0,0 +1,753 @@
+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.lib Require Export facts.
+From semantics.ts.systemf Require Import lang notation parallel_subst types bigstep.
+From Equations Require Export Equations.
+
+
+(** * Logical relation for SystemF *)
+
+Implicit Types
+  (Δ : nat)
+  (Γ : typing_context)
+  (v : val)
+  (α : var)
+  (e : expr)
+  (A : type).
+
+(* *** Definition of the logical relation. *)
+(* In Coq, we need to make argument why the logical relation is well-defined
+   precise: 
+   In particular, we need to show that the mutual recursion between the value
+   relation and the expression relation, which are defined in terms of each
+   other, terminates. We therefore define a termination measure [mut_measure]
+   that makes sure that for each recursive call, we either decrease the size of
+   the type or switch from the expression case to the value case.
+
+   We use the Equations package to define the logical relation, as it's tedious
+   to make the termination argument work with Coq's built-in support for
+   recursive functions---but under the hood, Equations also just encodes it as
+   a Coq Fixpoint.
+ *)
+Inductive val_or_expr : Type :=
+| inj_val : val → val_or_expr
+| inj_expr : expr → val_or_expr.
+
+(* The [type_size] function essentially computes the size of the "type tree". *)
+(* Note that we have added some additional primitives to make our (still
+   simple) language more expressive. *)
+Equations type_size (A : type) : nat :=
+  type_size Int := 1;
+  type_size Bool := 1;
+  type_size Unit := 1;
+  type_size (A → B) := type_size A + type_size B + 1;
+  type_size (#α) := 1;
+  type_size (∀: A) := type_size A + 2;
+  type_size (∃: A) := type_size A + 2;
+  type_size (A × B) := type_size A + type_size B + 1;
+  type_size (A + B) := max (type_size A) (type_size B) + 1.
+(* The definition of the expression relation uses the value relation -- therefore, it needs to be larger, and we add [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.
+
+(** A semantic type consists of a value-predicate and a proof of closedness *)
+Record sem_type := mk_ST {
+  sem_type_car :> val → Prop;
+  sem_type_closed_val v : sem_type_car v → is_closed [] (of_val v);
+  }.
+(** Two tactics we will use later on.
+  [pose_sem_type P as N] defines a semantic type at name [N] with the value predicate [P].
+  [specialize_sem_type S with P as N] specializes a universal quantifier over sem types in [S] with
+    a semantic type with predicate [P], giving it the name [N].
+ *)
+(* slightly complicated formulation to make the proof term [p] opaque and prevent it from polluting the context *)
+Tactic Notation "pose_sem_type" uconstr(P) "as" ident(N) :=
+  let p := fresh "__p" in
+  unshelve refine ((λ p, let N := (mk_ST P p) in _) _); first (simpl in p); cycle 1.
+Tactic Notation "specialize_sem_type" constr(S) "with" uconstr(P) "as" ident(N) :=
+  pose_sem_type P as N; last specialize (S N).
+
+(** We represent type variable assignments [δ] as lists of semantic types.
+  The variable #n (in De Bruijn representation) is mapped to the [n]-th element of the list.
+ *)
+Definition tyvar_interp := nat → sem_type.
+Implicit Types
+  (δ : tyvar_interp)
+  (τ : sem_type).
+
+(** The logical relation *)
+Equations type_interp (c : val_or_expr) (t : type) δ : Prop by wf (mut_measure c t) := {
+  type_interp (inj_val v) Int δ =>
+    ∃ z : Z, v = #z ;
+  type_interp (inj_val v) Bool δ =>
+    ∃ b : bool, v = #b ;
+  type_interp (inj_val v) Unit δ =>
+    v = #LitUnit ;
+  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 ∧ is_closed (x :b: nil) e ∧
+      ∀ v',
+        type_interp (inj_val v') A δ →
+        type_interp (inj_expr (subst' x (of_val v') e)) B δ;
+  (** Type variable case *)
+  type_interp (inj_val v) (#α) δ =>
+    (δ α).(sem_type_car) v;
+  (** ∀ case *)
+  type_interp (inj_val v) (∀: A) δ =>
+    ∃ e, v = TLamV e ∧ is_closed [] e ∧
+      ∀ τ, type_interp (inj_expr e) A (τ .: δ);
+  (** ∃ case *)
+  type_interp (inj_val v) (∃: A) δ =>
+    ∃ v', v = PackV v' ∧
+      ∃ τ : sem_type, type_interp (inj_val v') A (τ .: δ);
+
+  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. repeat simp mut_measure; simp type_size; lia. Qed.
+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.
+
+(** Value relation and expression relation *)
+Notation sem_val_rel A δ v := (type_interp (inj_val v) A δ).
+Notation sem_expr_rel A δ e := (type_interp (inj_expr e) A δ).
+
+Notation 𝒱 A δ v := (sem_val_rel A δ v).
+Notation ℰ A δ v := (sem_expr_rel A δ v).
+
+
+(* *** Semantic typing of contexts *)
+Implicit Types
+  (θ : gmap string expr).
+Inductive sem_context_rel (δ : tyvar_interp) : 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.
+
+
+
+(* Semantic typing judgement *)
+Definition sem_typed Δ Γ e A :=
+  is_closed (elements (dom Γ)) e ∧
+  ∀ θ δ, 𝒢 δ Γ θ → ℰ A δ (subst_map θ e).
+Notation "'TY' Δ ; Γ ⊨ e : A" := (sem_typed Δ Γ e A) (at level 74, e, A at next level).
+
+
+Lemma val_rel_closed v δ A:
+  𝒱 A δ v → is_closed [] (of_val v).
+Proof.
+  induction A as [ | | | | | A IHA | | A IH1 B IH2 | A IH1 B IH2] in v, δ |-*; simp type_interp.
+  - eapply sem_type_closed_val.
+  - intros [z ->]. done.
+  - intros [b ->]. done.
+  - intros ->. done.
+  - intros (e & -> & ? & _). done.
+  - intros (v' & -> & (τ & Hinterp)). simpl. by eapply IHA.
+  - intros (x & e & -> & ? & _). done.
+  - intros (v1 & v2 & -> & ? & ?). simpl. apply andb_True. eauto.
+  - intros [(v' & -> & ?) | (v' & -> & ?)]; simpl; eauto.
+Qed.
+
+(** Interpret a syntactic type *)
+Program Definition interp_type A δ : sem_type := {|
+  sem_type_car := fun v => 𝒱 A δ v;
+|}.
+Next Obligation. by eapply val_rel_closed. Qed.
+
+
+(* We start by proving a couple of helper lemmas that will be useful later. *)
+
+Lemma sem_expr_rel_of_val A δ v :
+  ℰ A δ (of_val 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 sem_context_rel_closed δ Γ θ:
+  𝒢 δ Γ θ → subst_is_closed [] θ.
+Proof.
+  induction 1.
+  - done.
+  - 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.
+
+
+Section boring_lemmas.
+  (** The lemmas in this section are all quite boring and expected statements,
+    but are quite technical to prove due to De Bruijn binders.
+    We encourage you to skip over the proofs of these lemmas.
+  *)
+
+  Lemma sem_val_rel_ext B δ δ' v :
+    (∀ n v, δ n v ↔ δ' n v) →
+    𝒱 B δ v ↔ 𝒱 B δ' v.
+  Proof.
+    induction B in δ, δ', v |-*; simpl; simp type_interp; eauto; intros Hiff.
+    - f_equiv; intros e. f_equiv. f_equiv.
+      eapply forall_proper; intros τ.
+      simp type_interp. f_equiv. intros w.
+      f_equiv. etransitivity; last apply IHB; first done.
+      intros [|m] ?; simpl; eauto.
+    - f_equiv; intros w. f_equiv. f_equiv. intros τ.
+      etransitivity; last apply IHB; first done.
+      intros [|m] ?; simpl; eauto.
+    - f_equiv. intros ?. f_equiv. intros ?.
+      f_equiv. f_equiv. eapply forall_proper. intros x.
+      eapply if_iff; first eauto.
+      simp type_interp. f_equiv. intros ?. f_equiv.
+      eauto.
+    - f_equiv. intros ?. f_equiv. intros ?.
+      f_equiv. f_equiv; eauto.
+    - f_equiv; f_equiv; intros ?; f_equiv; eauto.
+  Qed.
+
+
+  Lemma sem_val_rel_move_ren B δ σ v :
+     𝒱 B (λ n, δ (σ n)) v ↔ 𝒱 (rename σ B) δ v.
+  Proof.
+    induction B in σ, δ, v |-*; simpl; simp type_interp; eauto.
+    - f_equiv; intros e. f_equiv. f_equiv.
+      eapply forall_proper; intros τ.
+      simp type_interp. f_equiv. intros w.
+      f_equiv. etransitivity; last apply IHB.
+      eapply sem_val_rel_ext; intros [|n] u; asimpl; done.
+    - f_equiv; intros w. f_equiv. f_equiv. intros τ.
+      etransitivity; last apply IHB.
+      eapply sem_val_rel_ext; intros [|n] u.
+      +  simp type_interp. done.
+      + simpl. rewrite /up. simpl. done.
+    - f_equiv. intros ?. f_equiv. intros ?.
+      f_equiv. f_equiv. eapply forall_proper. intros x.
+      eapply if_iff; first done.
+      simp type_interp. f_equiv. intros ?. f_equiv.
+      done.
+    - f_equiv. intros ?. f_equiv. intros ?.
+      f_equiv. f_equiv; done.
+    - f_equiv; f_equiv; intros ?; f_equiv; done.
+  Qed.
+
+
+  Lemma sem_val_rel_move_subst B δ σ v :
+    𝒱 B (λ n, interp_type (σ n) δ) v ↔ 𝒱 (B.[σ]) δ v.
+  Proof.
+    induction B in σ, δ, v |-*; simpl; simp type_interp; eauto.
+    - f_equiv; intros e. f_equiv. f_equiv.
+      eapply forall_proper; intros τ.
+      simp type_interp. f_equiv. intros w.
+      f_equiv. etransitivity; last apply IHB.
+      eapply sem_val_rel_ext; intros [|n] u.
+      +  simp type_interp. done.
+      + simpl. rewrite /up. simpl.
+        etransitivity; last eapply sem_val_rel_move_ren.
+        simpl. done.
+    - f_equiv; intros w. f_equiv. f_equiv. intros τ.
+      etransitivity; last apply IHB.
+      eapply sem_val_rel_ext; intros [|n] u.
+      +  simp type_interp. done.
+      + simpl. rewrite /up. simpl.
+        etransitivity; last eapply sem_val_rel_move_ren.
+        simpl. done.
+    - f_equiv. intros ?. f_equiv. intros ?.
+      f_equiv. f_equiv. eapply forall_proper. intros x.
+      eapply if_iff; first done.
+      simp type_interp. f_equiv. intros ?. f_equiv.
+      done.
+    - f_equiv. intros ?. f_equiv. intros ?.
+      f_equiv. f_equiv; done.
+    - f_equiv; f_equiv; intros ?; f_equiv; done.
+  Qed.
+
+  Lemma sem_val_rel_move_single_subst A B δ v :
+    𝒱 B (interp_type A δ .: δ) v ↔ 𝒱 (B.[A/]) δ v.
+  Proof.
+    rewrite -sem_val_rel_move_subst. eapply sem_val_rel_ext.
+    intros [| n] w; simpl; done.
+  Qed.
+
+  Lemma sem_val_rel_cons A δ v τ :
+    𝒱 A δ v ↔ 𝒱  A.[ren (+1)] (τ .: δ) v.
+  Proof.
+    rewrite -sem_val_rel_move_subst; simpl.
+    eapply sem_val_rel_ext; done.
+  Qed.
+
+  Lemma sem_context_rel_cons Γ δ θ τ :
+    𝒢 δ Γ θ →
+    𝒢 (τ .: δ) (⤉ Γ) θ.
+  Proof.
+    induction 1 as [ | Γ θ v x A Hv Hctx IH]; simpl.
+    - rewrite fmap_empty. constructor.
+    - rewrite fmap_insert. constructor; last done.
+      rewrite -sem_val_rel_cons. done.
+  Qed.
+End boring_lemmas.
+
+(** ** Compatibility lemmas *)
+
+Lemma compat_int Δ Γ z : TY Δ; Γ ⊨ (Lit $ LitInt z) : Int.
+Proof.
+  split; first done. 
+  intros θ δ _. simp type_interp.
+  exists #z. split. { simpl. constructor. }
+  simp type_interp. eauto.
+Qed.
+
+Lemma compat_bool Δ Γ b : TY Δ; Γ ⊨ (Lit $ LitBool b) : Bool.
+Proof.
+  split; first done. 
+  intros θ δ _. simp type_interp.
+  exists #b. split. { simpl. constructor. }
+  simp type_interp. eauto.
+Qed.
+
+Lemma compat_unit Δ Γ : TY Δ; Γ ⊨ (Lit $ LitUnit) : Unit.
+Proof.
+  split; first done. 
+  intros θ δ _. simp type_interp.
+  exists #LitUnit. split. { simpl. constructor. }
+  simp type_interp. eauto.
+Qed.
+
+Lemma compat_var Δ Γ x A :
+  Γ !! x = Some A →
+  TY Δ; Γ ⊨ (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 :
+  TY Δ; Γ ⊨ e1 : (A → B) →
+  TY Δ; Γ ⊨ e2 : A →
+  TY Δ; Γ ⊨ (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 & Hv1).
+  simp type_interp in Hv1. destruct Hv1 as (x & e & -> & 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.
+  - eapply is_closed_weaken; first done.
+    rewrite dom_delete dom_insert (sem_context_rel_dom δ Γ θ) //.
+    intros y. destruct (decide (x = y)); set_solver.
+  - intros x' e' Hx.
+    eapply (is_closed_weaken []); last set_solver.
+    eapply sem_context_rel_closed; first eassumption.
+    eapply map_subseteq_spec; last done.
+    apply map_delete_subseteq.
+Qed.
+Lemma compat_lam Δ Γ x e A B :
+  TY Δ; (<[ x := A ]> Γ) ⊨ e : B →
+  TY Δ; Γ ⊨ (Lam (BNamed x) e) : (A → B).
+Proof.
+  intros [Hbodycl Hbody]. split.
+  { simpl. eapply is_closed_weaken; first eassumption. set_solver. }
+  intros θ Hctxt. simpl. simp type_interp.
+  eexists.
+  split; first by eauto.
+  simp type_interp.
+  eexists _, _. 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 :
+  TY Δ; Γ ⊨ e : B →
+  TY Δ; Γ ⊨ (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; simpl.
+    - by erewrite <-sem_context_rel_dom.
+    - by eapply sem_context_rel_closed. }
+  naive_solver.
+Qed.
+
+Lemma compat_int_binop Δ Γ op e1 e2 :
+  bin_op_typed op Int Int Int →
+  TY Δ; Γ ⊨ e1 : Int →
+  TY Δ; Γ ⊨ e2 : Int →
+  TY Δ; Γ ⊨ (BinOp op e1 e2) : Int.
+Proof.
+  intros Hop [He1cl He1] [He2cl He2].
+  split; first naive_solver.
+
+  intros θ δ Hctx. simpl.
+  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 & ->).
+
+  inversion Hop; subst op.
+  + exists #(z1 + z2)%Z. split.
+    - econstructor; done.
+    - exists (z1 + z2)%Z. done.
+  + exists #(z1 - z2)%Z. split.
+    - econstructor; done.
+    - exists (z1 - z2)%Z. done.
+  + exists #(z1 * z2)%Z. split.
+    - econstructor; done.
+    - exists (z1 * z2)%Z. done.
+Qed.
+
+Lemma compat_int_bool_binop Δ Γ op e1 e2 :
+  bin_op_typed op Int Int Bool →
+  TY Δ; Γ ⊨ e1 : Int →
+  TY Δ; Γ ⊨ e2 : Int →
+  TY Δ; Γ ⊨ (BinOp op e1 e2) : Bool.
+Proof.
+  intros Hop [He1cl He1] [He2cl He2].
+  split; first naive_solver.
+
+  intros θ δ Hctx. simpl.
+  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 & ->).
+
+  inversion Hop; subst op.
+  + exists #(bool_decide (z1 < z2))%Z. split.
+    - econstructor; done.
+    - by eexists _.
+  + exists #(bool_decide (z1 ≤ z2))%Z. split.
+    - econstructor; done.
+    - by eexists _.
+  + exists #(bool_decide (z1 = z2))%Z. split.
+    - econstructor; done.
+    - eexists _. done.
+Qed.
+
+Lemma compat_unop Δ Γ op A B e :
+  un_op_typed op A B →
+  TY Δ; Γ ⊨ e : A →
+  TY Δ; Γ ⊨ (UnOp op e) : B.
+Proof.
+  intros Hop [Hecl 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).
+  inversion Hop; subst; simp type_interp in Hv.
+  - destruct Hv as (b & ->).
+    exists #(negb b). split.
+    + econstructor; done.
+    + by eexists _.
+  - destruct Hv as (z & ->).
+    exists #(-z)%Z. split.
+    + econstructor; done.
+    + by eexists _.
+Qed.
+
+Lemma compat_tlam Δ Γ e A :
+  TY S Δ; (⤉ Γ) ⊨ e : A →
+  TY Δ; Γ ⊨ (Λ, e) : (∀: A).
+Proof.
+  intros [Hecl He]. split.
+  { simpl. by erewrite <-dom_fmap. }
+  intros θ δ Hctx. simpl.
+  simp type_interp.
+  exists (Λ, subst_map θ e)%V.
+  split; first constructor.
+
+  simp type_interp.
+  eexists _. split_and!; first done.
+  { simpl. eapply subst_map_closed; simpl.
+    - erewrite <-sem_context_rel_dom; last eassumption. 
+      by erewrite <-dom_fmap.
+    - by eapply sem_context_rel_closed. }
+  intros τ. eapply He.
+  by eapply sem_context_rel_cons.
+Qed.
+
+Lemma compat_tapp Δ Γ e A B :
+  type_wf Δ B →
+  TY Δ; Γ ⊨ e : (∀: A) →
+  TY Δ; Γ ⊨ (e <>) : (A.[B/]).
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma compat_pack Δ Γ e n A B :
+  type_wf n B →
+  type_wf (S n) A →
+  TY n; Γ ⊨ e : A.[B/] →
+  TY n; Γ ⊨ (pack e) : (∃: A).
+Proof.
+  (* This will be an exercise for you next week :) *)
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma compat_unpack n Γ A B e e' x :
+  type_wf n B →
+  TY n; Γ ⊨ e : (∃: A) →
+  TY S n; <[x:=A]> (⤉Γ) ⊨ e' : B.[ren (+1)] →
+  TY n; Γ ⊨ (unpack e as BNamed x in e') : B.
+Proof.
+  (* This will be an exercise for you next week :) *)
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma compat_if n Γ e0 e1 e2 A :
+  TY n; Γ ⊨ e0 : Bool →
+  TY n; Γ ⊨ e1 : A →
+  TY n; Γ ⊨ e2 : A →
+  TY n; Γ ⊨ (if: e0 then e1 else e2) : A.
+Proof.
+  intros [He0cl He0] [He1cl He1] [He2cl He2].
+  split; first naive_solver.
+  intros θ δ Hctx. simpl.
+  simp type_interp.
+  specialize (He0 _ _ Hctx). simp type_interp in He0.
+  specialize (He1 _ _ Hctx). simp type_interp in He1.
+  specialize (He2 _ _ Hctx). simp type_interp in He2.
+
+  destruct He0 as (v0 & Hb0 & Hv0). simp type_interp in Hv0. destruct Hv0 as (b & ->).
+  destruct He1 as (v1 & Hb1 & Hv1).
+  destruct He2 as (v2 & Hb2 & Hv2).
+
+  destruct b.
+  - exists v1. split; first by repeat econstructor. done.
+  - exists v2. split; first by repeat econstructor. done.
+Qed.
+
+Lemma compat_pair Δ Γ e1 e2 A B :
+  TY Δ; Γ ⊨ e1 : A →
+  TY Δ; Γ ⊨ e2 : B →
+  TY Δ; Γ ⊨ (e1, e2) : A × B.
+Proof.
+  intros [He1cl He1] [He2cl He2].
+  split; first 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 :
+  TY Δ; Γ ⊨ e : A × B →
+  TY Δ; Γ ⊨ Fst e : A.
+Proof.
+  intros [Hecl 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 :
+  TY Δ; Γ ⊨ e : A × B →
+  TY Δ; Γ ⊨ Snd e : B.
+Proof.
+  intros [Hecl 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 :
+  TY Δ; Γ ⊨ e : A →
+  TY Δ; Γ ⊨ InjL e : A + B.
+Proof.
+  intros [Hecl 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 :
+  TY Δ; Γ ⊨ e : B →
+  TY Δ; Γ ⊨ InjR e : A + B.
+Proof.
+  intros [Hecl 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 :
+  TY Δ; Γ ⊨ e : B + C →
+  TY Δ; Γ ⊨ e1 : (B → A) →
+  TY Δ; Γ ⊨ e2 : (C → A) →
+  TY Δ; Γ ⊨ Case e e1 e2 : A.
+Proof.
+  intros [Hecl He] [He1cl He1] [He2cl He2].
+  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 [(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 :
+  TY Δ; Γ ⊢ e : A →
+  TY Δ; Γ ⊨ e : A.
+Proof.
+  induction 1 as [ | | | | | | | |  | | | | n Γ e1 e2 op A B C Hop ? ? ? ? | | | | | | | ].
+  - by apply compat_var.
+  - by apply compat_lam.
+  - by apply compat_lam_anon.
+  - by apply compat_tlam.
+  - apply compat_tapp; done.
+  - eapply compat_pack; done.
+  - eapply compat_unpack; done.
+  - apply compat_int.
+  - by eapply compat_bool.
+  - by eapply compat_unit.
+  - by eapply compat_if.
+  - by eapply compat_app.
+  - inversion Hop; subst.
+    1-3: by apply compat_int_binop.
+    1-3: by apply compat_int_bool_binop.
+  - by eapply compat_unop.
+  - 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.
+
+(* dummy delta which we can use if we don't care *)
+Program Definition any_type : sem_type := {| sem_type_car := λ v, is_closed [] v |}.
+Definition δ_any : var → sem_type := λ _, any_type.
+
+Lemma termination e A :
+  (TY 0; ∅ ⊢ e : A)%ty →
+  ∃ v, big_step e v.
+Proof.
+  intros [Hsemcl Hsem]%sem_soundness.
+  specialize (Hsem ∅ δ_any).
+  simp type_interp in Hsem.
+  rewrite subst_map_empty in Hsem.
+  destruct Hsem as (v & Hbs & _); last eauto.
+  constructor.
+Qed.