Merge remote-tracking branch 'origin/main' into amethyst

.gitignore

@@ -18,3 +18,5 @@ _opam
 tags
 _build
 public
+# I have no idea how this guy keeps sneaking in
+target

_CoqProject

@@ -11,19 +11,36 @@
 # library stuff
 theories/lib/maps.v
 theories/lib/sets.v
+theories/lib/debruijn.v
+theories/lib/facts.v
 
 # STLC
 theories/type_systems/stlc/lang.v
 theories/type_systems/stlc/notation.v
 theories/type_systems/stlc/untyped.v
 theories/type_systems/stlc/types.v
+theories/type_systems/stlc/logrel.v
+theories/type_systems/stlc/parallel_subst.v
 
 # Extended STLC
 theories/type_systems/stlc_extended/lang.v
 theories/type_systems/stlc_extended/notation.v
 theories/type_systems/stlc_extended/types.v
+theories/type_systems/stlc_extended/types_sol.v
 theories/type_systems/stlc_extended/bigstep.v
+theories/type_systems/stlc_extended/bigstep_sol.v
 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
+
+# System F
+theories/type_systems/systemf/lang.v
+theories/type_systems/systemf/notation.v
+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
 
 # By removing the # below, you can add the exercise sheets to make
 theories/type_systems/warmup/warmup.v
@@ -31,3 +48,6 @@ theories/type_systems/warmup/warmup.v
 theories/type_systems/stlc/exercises01.v
 #theories/type_systems/stlc/exercises01_sol.v
 theories/type_systems/stlc/exercises02.v
+#theories/type_systems/stlc/exercises02_sol.v
+#theories/type_systems/stlc/cbn_logrel.v
+#theories/type_systems/systemf/exercises03.v

theories/lib/debruijn.v

@@ -0,0 +1,47 @@
+From iris.prelude Require Import prelude options.
+From Autosubst Require Export Autosubst.
+
+
+(* [idss n sigma] alters the substitution [sigma] by
+  "prepending" binders [0..n), so that [#i] is substituted for binder [i].
+  After that, the binders from [sigma] follow.
+ *)
+Definition idss `{Ids X} (n : nat) (sigma : var → X) (x : var) :=
+  if decide (x < n) then ids x else sigma (x - n).
+Lemma idss_0 `{Ids X} (sigma : var → X) :
+  idss 0 sigma = sigma.
+Proof.
+  f_ext. intros x; unfold idss. simpl.
+  replace (x - 0) with x by lia. done.
+Qed.
+Lemma up_idss `{Ids X} `{Rename X} (sigma : var → X) n :
+  (* this precondition holds for the instances we are interested in,
+    but is not a general law assumed by autosubst *)
+  (∀ x : var, rename (+1) (ids x) = ids (S x)) →
+  up (idss n sigma) = idss (S n) (sigma >>> rename (+1) ).
+Proof.
+  intros Hren_law.
+  f_ext. intros x. destruct x as [ | x]; unfold idss; simpl; first done.
+  unfold up. simpl.
+  destruct (decide (x < n)).
+  - rewrite decide_True; last lia. apply Hren_law.
+  - rewrite decide_False; last lia. done.
+Qed.
+
+(* We will also need something like [idss] to shift variable renamings [var → var].
+  Instead of doing a separate definition like
+  [ Definition idsc (n : nat) (sigma : var → var) (x : var) := if decide (x < n) then x else sigma (x - n). ]
+  we declare suitable instances to use [idss] for variable renamings.
+*)
+#[global] Instance Ids_var : Ids var. exact id. Defined.
+#[global] Instance Rename_var : Rename var. exact id. Defined.
+
+(* a lemma for the nat instance *)
+Lemma upren_idss sigma n :
+  upren (idss n sigma) = idss (S n) (sigma >>> S).
+Proof.
+  f_ext. intros x. destruct x as [ | x]; unfold idss; simpl; first done.
+  destruct (decide (x < n)).
+  - rewrite decide_True; [done | lia ].
+  - rewrite decide_False; lia.
+Qed.

theories/lib/facts.v

@@ -0,0 +1,53 @@
+From stdpp Require Export relations.
+From stdpp Require Import binders gmap.
+
+Lemma if_iff P Q R S:
+  (P ↔ Q) →
+  (R ↔ S) →
+  ((P → R) ↔ (Q → S)).
+Proof.
+  naive_solver.
+Qed.
+
+Lemma if_iff' P R S :
+  (P → R ↔ S) → (P → R) ↔ (P → S).
+Proof. tauto. Qed.
+Lemma and_iff' (P R S : Prop) :
+  (P → R ↔ S) → (P ∧ R) ↔ (P ∧ S).
+Proof. tauto. Qed.
+Lemma and_iff (P Q R S : Prop) :
+  (P ↔ Q) → ((P ∨ Q) → R ↔ S) → (P ∧ R) ↔ (Q ∧ S).
+Proof. tauto. Qed.
+
+Lemma list_subseteq_cons {X} (A B : list X) x : A ⊆ B → x :: A ⊆ x :: B.
+Proof. intros Hincl. intros y. rewrite !elem_of_cons. naive_solver. Qed.
+Lemma list_subseteq_cons_binder A B x : A ⊆ B → x :b: A ⊆ x :b: B.
+Proof. destruct x; [done|]. apply list_subseteq_cons. Qed.
+Lemma list_subseteq_cons_l {X} (A B : list X) x : A ⊆ x :: B → x :: A ⊆ x :: B.
+Proof. 
+  intros Hincl. intros y. rewrite elem_of_cons. intros [-> | ?]. 
+  - left.
+  - apply Hincl. naive_solver. 
+Qed.
+
+Lemma list_subseteq_cons_elem {X} (A B : list X) x :
+  x ∈ B → A ⊆ B → (x :: A) ⊆ B.
+Proof.
+  intros Hel Hincl.
+  intros a [-> | ?]%elem_of_cons; [done|].
+  by apply Hincl.
+Qed.
+
+Lemma elements_subseteq `{EqDecision A} `{Countable A} (X Y : gset A):
+  X ⊆ Y → elements X ⊆ elements Y.
+Proof.
+  rewrite elem_of_subseteq.
+  intros Ha a. rewrite !elem_of_elements.
+  apply Ha.
+Qed.
+Lemma list_subseteq_cons_r {X} (A B : list X) x :
+  A ⊆ B → A ⊆ (x :: B).
+Proof.
+  intros Hincl. trans B; [done|].
+  intros b Hel. apply elem_of_cons; by right.
+Qed.

theories/type_systems/stlc/auto_step.v

@@ -0,0 +1,177 @@
+From stdpp Require Import base relations tactics.
+From iris Require Import prelude.
+From semantics.lib Require Import sets maps.
+From semantics.ts.stlc Require Import lang notation.
+
+Fixpoint eval_step (e: expr): option expr :=
+  match e with
+    | Var _ => None
+    | Lam x body => None
+    | LitInt n => None
+    | App lhs rhs => match to_val rhs, to_val lhs with
+      | None, _ => fmap (λ (rhs': expr), App lhs rhs') (eval_step rhs)
+      | Some _, None => fmap (λ (lhs': expr), App lhs' rhs) (eval_step lhs)
+      | Some rhs', Some (LamV name body) => Some (subst' name rhs' body)
+      | _, _ => None
+      end
+    | Plus lhs rhs => match to_val rhs, to_val lhs with
+      | None, _ => fmap (λ (rhs': expr), Plus lhs rhs') (eval_step rhs)
+      | Some _, None => fmap (λ (lhs': expr), Plus lhs' rhs) (eval_step lhs)
+      | Some (LitIntV rhs'), Some (LitIntV lhs') => Some (LitInt (lhs' + rhs'))
+      | _, _ => None
+      end
+  end.
+
+Theorem step_eval_step (e e': expr): step e e' → eval_step e = Some e'.
+Proof.
+  intro H_step.
+  induction H_step; unfold eval_step; fold eval_step.
+  - unfold to_val.
+    destruct e'; try (unfold is_val in H; exfalso; exact H).
+    reflexivity.
+    reflexivity.
+  - destruct e1; try (unfold eval_step in IHH_step; discriminate IHH_step).
+    + unfold to_val.
+      destruct e2; try (unfold is_val in H; exfalso; exact H).
+      all: rewrite IHH_step; reflexivity.
+    + unfold to_val.
+      destruct e2; try (unfold is_val in H; exfalso; exact H).
+      all: rewrite IHH_step; reflexivity.
+  - destruct (to_val e2) eqn:H_to_val.
+    {
+      apply of_to_val in H_to_val.
+      assert (is_val (of_val v)); try exact (is_val_of_val v).
+      apply val_no_step in H_step.
+      exfalso; exact H_step.
+      rewrite <-H_to_val.
+      assumption.
+    }
+    rewrite IHH_step.
+    reflexivity.
+  - unfold to_val.
+    rewrite H.
+    reflexivity.
+  - destruct e2; try (unfold is_val in H; exfalso; exact H).
+    unfold to_val.
+
+    destruct H_step; try (rewrite IHH_step; reflexivity).
+    unfold to_val.
+    rewrite IHH_step; simpl.
+    destruct e1.
+    + inversion H_step.
+    + val_no_step.
+    + reflexivity.
+    + val_no_step.
+    + reflexivity.
+  - destruct (to_val e2) eqn:H_to_val.
+    {
+      apply of_to_val in H_to_val.
+      assert (is_val (of_val v)); try exact (is_val_of_val v).
+      apply val_no_step in H_step.
+      exfalso; exact H_step.
+      rewrite <-H_to_val.
+      assumption.
+    }
+    rewrite IHH_step.
+    reflexivity.
+Qed.
+
+Theorem eval_step_step (e e': expr): eval_step e = Some e' → step e e'.
+Proof.
+  revert e'.
+  induction e; intros e' H_eq.
+  all: try (unfold eval_step in H_eq; discriminate H_eq).
+  - unfold eval_step in H_eq; fold eval_step in H_eq.
+
+    induction (eval_step e2).
+    + remember (IHe2 a (eq_refl _)) as H_appr.
+      unfold eval_step in H_eq; fold eval_step in H_eq.
+      destruct (to_val e2) eqn:H_to_val.
+      clear HeqH_appr.
+      {
+        apply of_to_val in H_to_val.
+        assert (is_val (of_val v)); try exact (is_val_of_val v).
+        apply val_no_step in H_appr.
+        exfalso; exact H_appr.
+        rewrite <-H_to_val.
+        assumption.
+      }
+      simpl in H_eq.
+      injection H_eq; intro H_eq'.
+      rewrite <-H_eq'.
+      apply StepAppR.
+      assumption.
+    + destruct (to_val e2) eqn:H_e2_to_val.
+      all: destruct (to_val e1) eqn:H_e1_to_val.
+      all: try (simpl in H_eq; discriminate H_eq).
+      all: try remember (of_to_val _ _ H_e1_to_val) as H_e1_val.
+      all: try remember (of_to_val _ _ H_e2_to_val) as H_e2_val.
+      {
+        subst.
+        induction v0.
+        discriminate H_eq.
+        injection H_eq; intro H_eq'; subst.
+        apply StepBeta.
+        eauto.
+      }
+      induction (eval_step e1).
+      {
+        simpl in H_eq.
+        injection H_eq; intro H_eq'.
+        rewrite <-H_eq'.
+        eapply StepAppL.
+        rewrite <-H_e2_val.
+        apply is_val_of_val.
+        apply (IHe1 a (eq_refl _)).
+      }
+      simpl in H_eq; discriminate H_eq.
+  - unfold eval_step in H_eq; fold eval_step in H_eq.
+    destruct (to_val e2) eqn:H_e2_to_val.
+    all: destruct (to_val e1) eqn:H_e1_to_val.
+    all: try remember (of_to_val _ _ H_e1_to_val) as H_e1_val.
+    all: try remember (of_to_val _ _ H_e2_to_val) as H_e2_val.
+    + induction v; induction v0; try discriminate H_eq.
+      rewrite <-H_e2_val.
+      rewrite <-H_e1_val.
+      unfold of_val.
+      injection H_eq; intro H_eq'.
+      rewrite <-H_eq'.
+      eauto.
+    + induction v; try discriminate H_eq.
+      all: (
+        unfold of_val in H_e2_val;
+        rewrite <-H_e2_val;
+        induction (eval_step e1); try (simpl in H_eq; discriminate H_eq);
+        simpl in H_eq;
+        injection H_eq; intro H_eq';
+        subst;
+        eapply StepPlusL;
+        unfold is_val; intuition;
+        exact (IHe1 a (eq_refl _))
+      ).
+    + induction (eval_step e2); try (simpl in H_eq; discriminate H_eq).
+      simpl in H_eq; injection H_eq; intro H_eq'.
+      subst.
+      eapply StepPlusR.
+      exact (IHe2 a (eq_refl _)).
+    + induction (eval_step e2); try (simpl in H_eq; discriminate H_eq).
+      simpl in H_eq; injection H_eq; intro H_eq'.
+      subst.
+      eapply StepPlusR.
+      exact (IHe2 a (eq_refl _)).
+Qed.
+
+
+Ltac auto_subst :=
+  (rewrite subst_closed_nil; last assumption) ||
+  (unfold subst'; unfold subst; simpl; fold subst).
+
+Ltac auto_step := (simpl;
+  repeat (eapply rtc_l;
+    first apply eval_step_step;
+    first simpl;
+    first reflexivity;
+    try (reflexivity; done)
+  );
+  reflexivity
+).

theories/type_systems/stlc/cbn_logrel.v

@@ -0,0 +1,184 @@
+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.
+
+
+
+
+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. *)
+  (* TODO: exercise *)
+Admitted.
+

theories/type_systems/stlc/exercises02_sol.v

@@ -0,0 +1,378 @@
+From stdpp Require Import gmap base relations tactics.
+From iris Require Import prelude.
+From semantics.ts.stlc Require Import lang notation.
+From semantics.ts.stlc Require untyped types.
+
+
+(** README: Please also download the assigment sheet as a *.pdf from here:
+            https://cms.sic.saarland/semantics_ws2324/materials/
+            It contains additional explanation and excercises. **)
+
+(** ** Exercise 1: Prove that the structural and contextual semantics are equivalent. *)
+(** You will find it very helpful to separately derive the structural rules of the
+  structural semantics for the contextual semantics. *)
+
+Lemma contextual_step_beta x e e':
+  is_val e' → contextual_step ((λ: x, e) e') (subst' x e' e).
+Proof.
+  intros Hval. eapply base_contextual_step, BetaS; done.
+Qed.
+
+Lemma contextual_step_app_r (e1 e2 e2': expr) :
+  contextual_step e2 e2' →
+  contextual_step (e1 e2) (e1 e2').
+Proof.
+  intros Hval. by eapply fill_contextual_step with (K := AppRCtx e1 HoleCtx).
+Qed.
+
+Lemma contextual_step_app_l (e1 e1' e2: expr) :
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (e1 e2) (e1' e2).
+Proof.
+  intros Hval. eapply is_val_spec in Hval as [v Hval].
+  eapply of_to_val in Hval as <-.
+  eapply fill_contextual_step with (K := (AppLCtx HoleCtx v)).
+Qed.
+
+Lemma contextual_step_plus_red (n1 n2 n3: Z) :
+  (n1 + n2)%Z = n3 →
+  contextual_step (n1 + n2)%E n3.
+Proof.
+  intros Hval. eapply base_contextual_step, PlusS; done.
+Qed.
+
+Lemma contextual_step_plus_r e1 e2 e2' :
+  contextual_step e2 e2' →
+  contextual_step (Plus e1 e2) (Plus e1 e2').
+Proof.
+  intros Hval. by eapply fill_contextual_step with (K := (PlusRCtx e1 HoleCtx)).
+Qed.
+
+Lemma contextual_step_plus_l e1 e1' e2 :
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (Plus e1 e2) (Plus e1' e2).
+Proof.
+  intros Hval. eapply is_val_spec in Hval as [v Hval].
+  eapply of_to_val in Hval as <-.
+  eapply fill_contextual_step with (K := (PlusLCtx HoleCtx v)).
+Qed.
+
+(** We register these lemmas as hints for [eauto]. *)
+#[global]
+Hint Resolve contextual_step_beta contextual_step_app_l contextual_step_app_r contextual_step_plus_red contextual_step_plus_l contextual_step_plus_r : core.
+
+Lemma step_contextual_step e1 e2: step e1 e2 → contextual_step e1 e2.
+Proof.
+  (* The hints above make sure eauto uses the right lemmas. *)
+  induction 1; eauto.
+Qed.
+
+(** Now the other direction. *)
+(* You may find it helpful to introduce intermediate lemmas. *)
+
+Lemma base_step_step e1 e2:
+  base_step e1 e2 → step e1 e2.
+Proof.
+  destruct 1; subst.
+  - eauto.
+  - by econstructor.
+Qed.
+
+Lemma fill_step K e1 e2:
+  step e1 e2 → step (fill K e1) (fill K e2).
+Proof.
+  induction K; simpl; eauto.
+Qed.
+Lemma contextual_step_step e1 e2:
+  contextual_step e1 e2 → step e1 e2.
+Proof.
+  destruct 1 as [K h1 h2 -> -> Hstep].
+  eapply fill_step, base_step_step, Hstep.
+Qed.
+
+
+(** ** Exercise 2: Scott encodings *)
+Section scott.
+  (* take a look at untyped.v for usefull lemmas and definitions *)
+  Import semantics.ts.stlc.untyped.
+
+  (** Scott encoding of Booleans *)
+  Definition true_scott : val := λ: "t" "f", "t".
+  Definition false_scott : val := λ: "t" "f", "f".
+
+  Lemma true_red (v1 v2 : val) :
+    closed [] v1 →
+    closed [] v2 →
+    rtc step (true_scott v1 v2) v1.
+  Proof.
+    intros Hcl1 Hcl2.
+    eapply rtc_l.
+    { econstructor; first auto.
+      econstructor. auto.
+    }
+    simpl.
+    eapply rtc_l.
+    { econstructor; auto. }
+    simpl.
+    rewrite subst_closed_nil; done.
+  Qed.
+
+  Lemma false_red (v1 v2 : val) :
+    closed [] v1 →
+    closed [] v2 →
+    rtc step (false_scott v1 v2) v2.
+  Proof.
+    intros Hcl1 Hcl2.
+    eapply rtc_l.
+    { econstructor; first auto.
+      econstructor. auto.
+    }
+    simpl.
+    eapply rtc_l.
+    { econstructor; auto. }
+    simpl. done.
+  Qed.
+
+  (** Scott encoding of Pairs *)
+  Definition pair_scott : val := λ: "v1" "v2", λ: "d", "d" "v1" "v2".
+
+  Definition fst_scott : val := λ: "p", "p" (λ: "a" "b", "a").
+  Definition snd_scott : val := λ: "p", "p" (λ: "a" "b", "b").
+
+  Lemma fst_red (v1 v2 : val) :
+    is_closed [] v1 →
+    is_closed [] v2 →
+    rtc step (fst_scott (pair_scott v1 v2)) v1.
+  Proof.
+    intros Hcl1 Hcl2.
+    eapply rtc_l.
+    { econstructor 3. econstructor; first auto.
+      econstructor. auto.
+    }
+    simpl. eapply rtc_l.
+    { econstructor 3. econstructor; first auto. }
+    simpl. eapply rtc_l.
+    { econstructor. done. }
+    simpl. eapply rtc_l.
+    { econstructor. done. }
+    simpl.
+    rewrite !(subst_closed_nil v1); [ | done..].
+    rewrite subst_closed_nil; last done.
+    eapply rtc_l.
+    { econstructor; first auto.
+      econstructor. auto.
+    }
+    simpl. eapply rtc_l.
+    { econstructor; first auto. }
+    simpl. rewrite subst_closed_nil; done.
+  Qed.
+
+  Lemma snd_red (v1 v2 : val) :
+    is_closed [] v1 →
+    is_closed [] v2 →
+    rtc step (snd_scott (pair_scott v1 v2)) v2.
+  Proof.
+    intros Hcl1 Hcl2.
+    eapply rtc_l.
+    { econstructor 3. econstructor; first auto.
+      econstructor. auto.
+    }
+    simpl. eapply rtc_l.
+    { econstructor 3. econstructor; first auto. }
+    simpl. eapply rtc_l.
+    { econstructor. done. }
+    simpl. eapply rtc_l.
+    { econstructor. done. }
+    simpl.
+    rewrite !(subst_closed_nil v2); [ | done..].
+    rewrite !(subst_closed_nil v1); [ | done..].
+    eapply rtc_l.
+    { econstructor; first auto.
+      econstructor. auto.
+    }
+    simpl. eapply rtc_l.
+    { econstructor; first auto. }
+    simpl. done.
+  Qed.
+
+End scott.
+
+Import semantics.ts.stlc.types.
+
+(** ** Exercise 3: type erasure *)
+(** Source terms *)
+Inductive src_expr :=
+| ELitInt (n: Z)
+(* Base lambda calculus *)
+| EVar (x : string)
+| ELam (x : binder) (A: type) (e : src_expr)
+| EApp (e1 e2 : src_expr)
+(* Base types and their operations *)
+| EPlus (e1 e2 : src_expr).
+
+(** The erasure function *)
+Fixpoint erase (E: src_expr) : expr :=
+match E with
+| ELitInt n => LitInt n
+| EVar x => Var x
+| ELam x A E => Lam x (erase E)
+| EApp E1 E2 => App (erase E1) (erase E2)
+| EPlus E1 E2 => Plus (erase E1) (erase E2)
+end.
+
+Reserved Notation "Γ '⊢S' e : A" (at level 74, e, A at next level).
+Inductive src_typed : typing_context → src_expr → type → Prop :=
+| src_typed_var Γ x A :
+    Γ !! x = Some A →
+    Γ ⊢S (EVar x) : A
+| src_typed_lam Γ x E A B :
+    (<[ x := A]> Γ) ⊢S E : B →
+    Γ ⊢S (ELam (BNamed x) A E) : (A → B)
+| src_typed_int Γ z :
+    Γ ⊢S (ELitInt z) : Int
+| src_typed_app Γ E1 E2 A B :
+    Γ ⊢S E1 : (A → B) →
+    Γ ⊢S E2 : A →
+    Γ ⊢S EApp E1 E2 : B
+| src_typed_add Γ E1 E2 :
+    Γ ⊢S E1 : Int →
+    Γ ⊢S E2 : Int →
+    Γ ⊢S EPlus E1 E2 : Int
+where "Γ '⊢S' E : A" := (src_typed Γ E%E A%ty) : FType_scope.
+#[export] Hint Constructors src_typed : core.
+
+Lemma type_erasure_correctness Γ E A:
+  (Γ ⊢S E : A)%ty → (Γ ⊢ erase E : A)%ty.
+Proof.
+  induction 1; simpl; eauto.
+Qed.
+
+(** ** Exercise 4: Unique Typing *)
+Lemma src_typing_unique Γ E A B:
+  (Γ ⊢S E : A)%ty → (Γ ⊢S E : B)%ty → A = B.
+Proof.
+  induction 1 as [ | ????? H1 IH1 | | ????? H1 IH1 H2 IH2 | ??? H1 IH1 H2 IH2] in B |-*; inversion 1; subst; try congruence.
+  - f_equal. eauto.
+  - rename select (_ ⊢S _ : (_ → _))%ty into Ha.
+    eapply IH1 in Ha. by injection Ha.
+Qed.
+
+(** TODO: Is runtime typing (Curry-style) also unique? Prove it or give a counterexample. *)
+(** Runtime typing is not unique! *)
+Lemma id_int: (∅ ⊢ (λ: "x", "x") : (Int → Int))%ty.
+Proof. eauto. Qed.
+
+Lemma id_int_to_int: (∅ ⊢ (λ: "x", "x") : ((Int → Int) → (Int → Int)))%ty.
+Proof. eauto. Qed.
+
+(** ** Exercise 5: Type Inference *)
+
+Fixpoint type_eq A B :=
+  match A, B with
+  | Int, Int => true
+  | Fun A B, Fun A' B' => type_eq A A' && type_eq B B'
+  | _, _ => false
+  end.
+
+Lemma type_eq_iff A B: type_eq A B ↔ A = B.
+Proof.
+  induction A in B |-*; destruct B; simpl; naive_solver.
+Qed.
+
+Notation ctx := (gmap string type).
+Fixpoint infer_type (Γ: ctx) E :=
+  match E with
+  | EVar x => Γ !! x
+  | ELam (BNamed x) A E =>
+    match infer_type (<[x := A]> Γ) E with
+    | Some B => Some (Fun A B)
+    | None => None
+    end
+  | ELitInt l => Some Int
+  | EApp E1 E2 =>
+    match infer_type Γ E1, infer_type Γ E2 with
+    | Some (Fun A B), Some C => if type_eq A C then Some B else None
+    | _, _ => None
+    end
+  | EPlus E1 E2 =>
+    match infer_type Γ E1, infer_type Γ E2 with
+    | Some Int, Some Int => Some Int
+    | _, _ => None
+    end
+  | ELam BAnon A E => None
+  end.
+
+(** Prove both directions of the correctness theorem. *)
+Lemma infer_type_typing Γ E A:
+  infer_type Γ E = Some A → (Γ ⊢S E : A)%ty.
+Proof.
+  induction E as [l|x|x B E IH|E1 IH1 E2 IH2|E1 IH1 E2 IH2] in Γ, A |-*; simpl.
+  - destruct l; naive_solver.
+  - eauto.
+  - destruct x as [|x]; first naive_solver.
+    destruct infer_type eqn: Heq; last naive_solver.
+    eapply IH in Heq. injection 1 as <-. eauto.
+  - destruct infer_type as [B|] eqn: Heq1; last naive_solver.
+    destruct B as [|B1 B2]; try naive_solver.
+    destruct (infer_type Γ E2) as [C|] eqn: Heq2; last naive_solver.
+    destruct type_eq eqn: Heq3; last naive_solver.
+    injection 1 as <-. eapply Is_true_eq_left in Heq3.
+    eapply type_eq_iff in Heq3 as ->.
+    eauto.
+  - destruct infer_type as [B|] eqn: Heq1; last naive_solver.
+    destruct B; try naive_solver.
+    destruct (infer_type Γ E2) as [C|] eqn: Heq2; last naive_solver.
+    destruct C; naive_solver.
+Qed.
+
+Lemma typing_infer_type Γ E A:
+  (Γ ⊢S E : A)%ty → infer_type Γ E = Some A.
+Proof.
+  induction 1; simpl; eauto.
+  - by rewrite IHsrc_typed.
+  - rewrite IHsrc_typed1 IHsrc_typed2.
+    rewrite (Is_true_eq_true (type_eq A A)) //=.
+    by eapply type_eq_iff.
+  - by rewrite IHsrc_typed1 IHsrc_typed2.
+Qed.
+
+
+(** ** Exercise 6: untypable, safe term *)
+
+(* The exercise asks you to:
+  "Give one example if there is such an expression, otherwise prove their non-existence."
+  So either finish one section or the other.
+*)
+
+Section give_example.
+  Definition ust : expr := (λ: "f", 5) (λ: "x", 0 0)%E.
+
+  Lemma ust_safe e':
+    rtc step ust e' → is_val e' ∨ reducible e'.
+  Proof.
+    inversion 1 as [ | x y z H1 H2]; subst.
+    - right. eexists. eapply StepBeta. done.
+    - inversion H1 as [??? Ha | ??? Ha Hb | ??? Ha | | ??? Ha Hb | ??? Ha ]; subst.
+      + simpl in H2. inversion H2 as [ | ??? [] _]; subst; eauto.
+      + inversion Hb.
+      + inversion Ha.
+  Qed.
+
+  Lemma ust_no_type Γ A:
+    ¬ (Γ ⊢ ust : A)%ty.
+  Proof.
+    intros H. inversion H; subst.
+    inversion H5; subst. inversion H6; subst.
+    inversion H4.
+  Qed.
+End give_example.
+
+Section prove_non_existence.
+  Lemma no_ust :
+  ∀ e, (∀ e', rtc step e e' → is_val e' ∨ reducible e') → ∃ A, (∅ ⊢ e : A)%ty.
+  Proof.
+    (* This is not possible as shown above *)
+  Abort.
+End prove_non_existence.

theories/type_systems/stlc/lang.v

@@ -336,4 +336,4 @@ Ltac val_no_step :=
   match goal with
   | [H: step ?e1 ?e2 |- _] =>
     solve [exfalso; eapply (val_no_step _ _ H); done]
-  end.
+  end.

theories/type_systems/stlc/logrel.v

@@ -0,0 +1,296 @@
+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).
+
+
+(* *** 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". *)
+Equations type_size (t : type) : nat :=
+  type_size Int := 1;
+  type_size (Fun A B) := 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.
+
+
+(* The main definition of the logical relation.
+   To handle the mutual recursion, both the expression and value relation are
+   handled by one definition, with [val_or_expr] determining the case.
+
+   The [by wf ..] part tells Equations to use [mut_measure] for the
+   well-formedness argument.
+ *)
+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 ∧
+      ∀ 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.
+  (* [simp] is a tactic provided by [Equations]. It rewrites with the defining equations of the definition.
+    [simpl]/[cbn] will NOT unfold definitions made with Equations.
+   *)
+  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. 
+   Note that these are [Notation], not [Definition]: we are not introducing new
+   terms here that have to be unfolded, we are merely introducing a notational
+   short-hand. This means tactics like [simp] can still "see" the underlying
+   [type_interp], which makes proofs a lot more pleasant. *)
+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 *)
+(* Substitutions map to expressions (as opposed to values)) -- this is so that
+   we can more easily reuse notions like closedness *)
+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.
+
+(* The semantic typing judgement. Note that we require e to be closed under Γ.
+   This is not strictly required for the semantic soundness proof, but does
+   make it more elegant. *)
+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_inclusion A v:
+  𝒱 A v → ℰ A v.
+Proof.
+  intros H. simp type_interp. eauto using big_step_vals.
+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 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_vals.
+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 & 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 closed_weaken; first done.
+    rewrite dom_delete dom_insert (sem_context_rel_dom Γ θ) //.
+    (* The [set_solver] tactic is great for solving goals involving set
+    inclusion and union. However, when set difference is involved, it can't
+    always solve the goal -- we need to help it by doing a case distinction on
+    whether the element we are considering is [x] or not. *)
+    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.
+  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_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 (z1 & ->). destruct Hv2 as (z2 & ->).
+
+  exists (z1 + z2)%Z. split.
+  - constructor; done.
+  - 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.
+  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.

theories/type_systems/stlc/parallel_subst.v

@@ -0,0 +1,189 @@
+From semantics.ts.stlc Require Import lang.
+From stdpp Require Import prelude.
+From iris Require Import prelude.
+From semantics.lib Require Export maps .
+
+(** * Parallel substitution *)
+
+(** This is the parallel substitution operation. We represent a substitution map as a finite map [xs]. *)
+Fixpoint subst_map (xs : gmap string expr) (e : expr) : expr :=
+  match e with
+  | LitInt n => LitInt n
+  | Var y => match xs !! y with Some es => es | _ =>  Var y end
+  | App e1 e2 => App (subst_map xs e1) (subst_map xs e2)
+  | Lam x e => Lam x (subst_map (binder_delete x xs) e)
+  | Plus e1 e2 => Plus (subst_map xs e1) (subst_map xs e2)
+  end.
+
+Lemma subst_map_empty e :
+  subst_map ∅ e = e.
+Proof.
+  induction e; simpl; f_equal; eauto.
+  destruct x; simpl; [done | by rewrite !delete_empty..].
+Qed.
+
+
+
+Lemma subst_map_closed X e xs :
+  closed X e →
+  (∀ x : string, x ∈ dom xs → x ∉ X) →
+  subst_map xs e = e.
+Proof.
+  intros Hclosed Hd.
+  induction e in xs, X, Hd, Hclosed |-*; simpl in *;try done.
+  { (* Var *)
+    apply bool_decide_spec in Hclosed.
+    assert (xs !! x = None) as ->; last done.
+    destruct (xs !! x) as [s | ] eqn:Helem; last done.
+    exfalso; eapply Hd; last apply Hclosed.
+    apply elem_of_dom; eauto.
+  }
+  { (* lambdas *)
+    erewrite IHe; [done | done |].
+    intros y. destruct x as [ | x]; first apply Hd.
+    simpl.
+    rewrite dom_delete elem_of_difference not_elem_of_singleton.
+    intros [Hnx%Hd Hneq]. rewrite elem_of_cons. intros [? | ?]; done.
+  }
+  (* all other cases *)
+  all: repeat match goal with
+  | H : Is_true (_ && _)  |- _ => apply andb_True in H as [ ? ? ]
+           end.
+  all: repeat match goal with
+       | H : ∀ _ _, _ → _ → subst_map _ _ = _ |- _ => erewrite H; clear H
+       end; done.
+Qed.
+
+Lemma subst_map_subst map x (e e': expr) :
+  closed [] e' →
+  subst_map map (subst x e' e) = subst_map (<[x:=e']>map) e.
+Proof.
+  intros He'; induction e as [y|y e IH | | |]in map|-*; simpl; try (f_equal; eauto).
+  - case_decide.
+    + simplify_eq/=. rewrite lookup_insert.
+      rewrite (subst_map_closed []); [done | apply He' | ].
+      intros ? ?. apply not_elem_of_nil.
+    + rewrite lookup_insert_ne; done.
+  - destruct y; simpl; first done.
+    + case_decide.
+      * simplify_eq/=. by rewrite delete_insert_delete.
+      * rewrite delete_insert_ne; last by congruence. done.
+Qed.
+
+(** We lift the notion of closedness [closed] to substitution maps. *)
+Definition subst_closed (X : list string) (map : gmap string expr) :=
+  ∀ x e, map !! x = Some e → closed X e.
+Lemma subst_closed_subseteq X map1 map2 :
+  map1 ⊆ map2 → subst_closed X map2 → subst_closed X map1.
+Proof.
+  intros Hsub Hclosed2 x e Hl. eapply Hclosed2, map_subseteq_spec; done.
+Qed.
+
+Lemma subst_closed_weaken X Y map1 map2 :
+  Y ⊆ X → map1 ⊆ map2 → subst_closed Y map2 → subst_closed X map1.
+Proof.
+  intros Hsub1 Hsub2 Hclosed2 x e Hl.
+  eapply closed_weaken. 1:eapply Hclosed2, map_subseteq_spec; done. done.
+Qed.
+
+(** Lemma about the interaction with "normal" substitution. *)
+Lemma subst_subst_map x es map e :
+  subst_closed [] map →
+  subst x es (subst_map (delete x map) e) =
+  subst_map (<[x:=es]> map) e.
+Proof.
+  revert map es x; induction e; intros map v0 xx Hclosed; simpl;
+  try (f_equal; eauto).
+  - destruct (decide (xx=x)) as [->|Hne].
+    + rewrite lookup_delete // lookup_insert //. simpl.
+      rewrite decide_True //.
+    + rewrite lookup_delete_ne // lookup_insert_ne //.
+      destruct (_ !! x) as [rr|] eqn:Helem.
+      * apply Hclosed in Helem.
+        by apply subst_closed_nil.
+      * simpl. rewrite decide_False //.
+  - destruct x; simpl; first by auto.
+    case_decide.
+    + simplify_eq. rewrite delete_idemp delete_insert_delete. done.
+    + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. apply IHe.
+      eapply subst_closed_subseteq; last done.
+      apply map_delete_subseteq.
+Qed.
+
+Lemma subst'_subst_map b (es : expr) map e :
+  subst_closed [] map →
+  subst' b es (subst_map (binder_delete b map) e) =
+  subst_map (binder_insert b es map) e.
+Proof.
+  destruct b; first done.
+  apply subst_subst_map.
+Qed.
+
+Lemma closed_subst_weaken e map X Y :
+  subst_closed [] map →
+  (∀ x, x ∈ X → x ∉ dom map → x ∈ Y) →
+  closed X e →
+  closed Y (subst_map map e).
+Proof.
+  induction e in X, Y, map |-*; simpl; intros Hmclosed Hsub Hcl.
+  { (* vars *)
+    destruct (map !! x) as [es | ] eqn:Heq.
+    + apply closed_weaken_nil. by eapply Hmclosed.
+    + apply bool_decide_pack. apply Hsub; first by eapply bool_decide_unpack.
+      by apply not_elem_of_dom.
+  }
+  { (* lambdas *)
+    eapply IHe; last done.
+    + eapply subst_closed_subseteq; last done.
+      destruct x; first done. apply map_delete_subseteq.
+    + intros y. destruct x as [ | x]; first by apply Hsub.
+      rewrite !elem_of_cons. intros [-> | Hy] Hn; first by left.
+      destruct (decide (y = x)) as [ -> | Hneq]; first by left.
+      right. eapply Hsub; first done. set_solver.
+  }
+  (* all other cases *)
+  all: repeat match goal with
+         | H : Is_true (_ && _)  |- _ => apply andb_True in H as [ ? ? ]
+              end.
+  all: repeat match goal with
+         | |- Is_true (_ && _) => apply andb_True; split
+              end.
+  all: naive_solver.
+Qed.
+
+
+Lemma subst_map_closed' X Y Θ e:
+  closed Y e →
+  (∀ x, x ∈ Y → if Θ !! x is (Some e') then closed X e' else x ∈ X) →
+  closed X (subst_map Θ e).
+Proof.
+  induction e in X, Θ, Y |-*; simpl.
+  - intros Hel%bool_decide_unpack Hcl.
+    eapply Hcl in Hel.
+    destruct (Θ !! x); first done.
+    simpl. by eapply bool_decide_pack.
+  - 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 closed_weaken; eauto with set_solver.
+  - rewrite !andb_True. intros [H1 H2] Hcl. split; eauto.
+  - auto.
+  - rewrite !andb_True. intros [H1 H2] Hcl. split; eauto.
+Qed.
+
+Lemma subst_map_closed'_2 X Θ e:
+  closed (X ++ (elements (dom Θ))) e ->
+  subst_closed X Θ ->
+  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.

theories/type_systems/stlc_extended/bigstep.v

@@ -10,21 +10,45 @@ Implicit Types
 
 Inductive big_step : expr → val → Prop :=
   | bs_lit (n : Z) :
-      big_step (LitInt n) (LitIntV n)
+    big_step (LitInt n) (LitIntV n)
   | bs_lam (x : binder) (e : expr) :
-      big_step (λ: x, e)%E (λ: x, e)%V
+    big_step (λ: x, e)%E (λ: x, e)%V
   | 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
+    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 e2 v2 →
-      big_step (subst' x (of_val v2) e) v →
-      big_step (App e1 e2) v
-
-(* TODO : extend the big-step semantics *)
-    .
+    big_step e1 (LamV x e) →
+    big_step e2 v2 →
+    big_step (subst' x (of_val v2) e) v →
+    big_step (App e1 e2) v
+  (* Pairs and fst, snd *)
+  | bs_pair (e1 e2 : expr) (v1 v2 : val) :
+    big_step e1 v1 →
+    big_step e2 v2 →
+    big_step (Pair e1 e2) (PairV v1 v2)
+  | bs_fst (e : expr) (v1 v2: val):
+    big_step e (PairV v1 v2) →
+    big_step (Fst e) v1
+  | bs_snd (e : expr) (v1 v2: val):
+    big_step e (PairV v1 v2) →
+    big_step (Fst e) v1
+  (* Inj *)
+  | bs_inj_l e v :
+    big_step e v →
+    big_step (InjL e) (InjLV v)
+  | bs_inj_r e v :
+    big_step e v →
+    big_step (InjR e) (InjRV v)
+  | bs_case_l (e_inj e_l e_r: expr) (v_inj v: val):
+    big_step e_inj (InjLV v_inj) →
+    big_step (e_l (of_val v_inj)) v →
+    big_step (Case e_inj e_l e_r) v
+  | bs_case_r (e_inj e_l e_r: expr) (v_inj v: val):
+    big_step e_inj (InjRV v_inj) →
+    big_step (e_r (of_val v_inj)) v →
+    big_step (Case e_inj e_l e_r) v
+.
 #[export] Hint Constructors big_step : core.
 
 Lemma big_step_of_val e v :
@@ -33,9 +57,7 @@ Lemma big_step_of_val e v :
 Proof.
   intros ->.
   induction v; simpl; eauto.
-
-(* TODO : this should be fixed once you have added the right semantics *)
-Admitted.
+Qed.
 
 
 Lemma big_step_val v v' :

theories/type_systems/stlc_extended/bigstep_sol.v

@@ -0,0 +1,69 @@
+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.ts.stlc_extended Require Import lang notation.
+
+(** * Big-step semantics *)
+
+Implicit Types
+  (v : val)
+  (e : expr).
+
+Inductive big_step : expr → val → Prop :=
+  | bs_lit (n : Z) :
+      big_step (LitInt n) (LitIntV n)
+  | bs_lam (x : binder) (e : expr) :
+      big_step (λ: x, e)%E (λ: x, e)%V
+  | 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 e2 v2 →
+      big_step (subst' x (of_val v2) e) v →
+      big_step (App e1 e2) v
+| bs_pair e1 e2 v1 v2 :
+      big_step e1 v1 →
+      big_step e2 v2 →
+      big_step (e1, e2) (v1, v2)
+  | bs_fst e v1 v2 :
+      big_step e (v1, v2) →
+      big_step (Fst e) v1
+  | bs_snd e v1 v2 :
+      big_step e (v1, v2) →
+      big_step (Snd e) v2
+  | bs_injl e v :
+      big_step e v →
+      big_step (InjL e) (InjLV v)
+  | bs_injr e v :
+      big_step e v →
+      big_step (InjR e) (InjRV v)
+  | bs_casel e e1 e2 v v' :
+      big_step e (InjLV v) →
+      big_step (e1 (of_val v)) v' →
+      big_step (Case e e1 e2) v'
+  | bs_caser e e1 e2 v v' :
+      big_step e (InjRV v) →
+      big_step (e2 (of_val v)) v' →
+      big_step (Case e e1 e2) v'
+
+    .
+#[export] Hint Constructors big_step : core.
+
+Lemma big_step_of_val e v :
+  e = of_val v →
+  big_step e v.
+Proof.
+  intros ->.
+  induction v; simpl; eauto.
+Qed.
+
+
+
+Lemma big_step_val v v' :
+  big_step (of_val v) v' → v' = v.
+Proof.
+  enough (∀ e, big_step e v' → e = of_val v → v' = v) by naive_solver.
+  intros e Hb.
+  induction Hb in v |-*; intros Heq; subst; destruct v; inversion Heq; subst; naive_solver.
+Qed.

theories/type_systems/stlc_extended/ctxstep.v

@@ -12,7 +12,24 @@ Inductive base_step : expr → expr → Prop :=
      e2 = (LitInt n2) →
      (n1 + n2)%Z = n3 →
      base_step (Plus e1 e2) (LitInt n3)
-  (* TODO: extend the definition *)
+  | FstS e v1 v2:
+    is_val v1 →
+    is_val v2 →
+    e = (Pair v1 v2) →
+    base_step (Fst e) v1
+  | SndS e v1 v2:
+    is_val v1 →
+    is_val v2 →
+    e = (Pair v1 v2) →
+    base_step (Snd e) v2
+  | CaseLS v_inj v e1 e2:
+    is_val v_inj →
+    v_inj = (InjL v) →
+    base_step (Case v_inj e1 e2) (App e1 v)
+  | CaseRS v_inj v e1 e2:
+    is_val v_inj →
+    v_inj = (InjR v) →
+    base_step (Case v_inj e1 e2) (App e2 v)
 .
 
 #[export] Hint Constructors base_step : core.
@@ -24,7 +41,13 @@ Inductive ectx :=
   | AppRCtx (e1 : expr) (K: ectx)
   | PlusLCtx (K: ectx) (v2 : val)
   | PlusRCtx (e1 : expr) (K: ectx)
-  (* TODO: extend the definition *)
+  | PairLCtx (K: ectx) (v2: val)
+  | PairRCtx (e1: expr) (K: ectx)
+  | FstCtx (K: ectx)
+  | SndCtx (K: ectx)
+  | InjLCtx (K: ectx)
+  | InjRCtx (K: ectx)
+  | CaseCtx (K: ectx) (e1: expr) (e2: expr)
 .
 
 Fixpoint fill (K : ectx) (e : expr) : expr :=
@@ -34,7 +57,13 @@ Fixpoint fill (K : ectx) (e : expr) : expr :=
   | AppRCtx e1 K => App e1 (fill K e)
   | PlusLCtx K v2 => Plus (fill K e) (of_val v2)
   | PlusRCtx e1 K => Plus e1 (fill K e)
-  (* TODO: extend the definition *)
+  | PairLCtx K v2 => Pair (fill K e) (of_val v2)
+  | PairRCtx e1 K => Pair e1 (fill K e)
+  | FstCtx K => Fst (fill K e)
+  | SndCtx K => Snd (fill K e)
+  | InjLCtx K => InjL (fill K e)
+  | InjRCtx K => InjR (fill K e)
+  | CaseCtx K e1 e2 => Case (fill K e) e1 e2
   end.
 
 Fixpoint comp_ectx (K: ectx) (K' : ectx) : ectx :=
@@ -44,7 +73,13 @@ Fixpoint comp_ectx (K: ectx) (K' : ectx) : ectx :=
   | AppRCtx e1 K => AppRCtx e1 (comp_ectx K K')
   | PlusLCtx K v2 => PlusLCtx (comp_ectx K K') v2
   | PlusRCtx e1 K => PlusRCtx e1 (comp_ectx K K')
-  (* TODO: extend the definition *)
+  | PairLCtx K v2 => PairLCtx (comp_ectx K K') v2
+  | PairRCtx e1 K => PairRCtx e1 (comp_ectx K K')
+  | FstCtx K => FstCtx (comp_ectx K K')
+  | SndCtx K => SndCtx (comp_ectx K K')
+  | InjLCtx K => InjLCtx (comp_ectx K K')
+  | InjRCtx K => InjRCtx (comp_ectx K K')
+  | CaseCtx K e1 e2 => CaseCtx (comp_ectx K K') e1 e2
   end.
 
 (** Contextual steps *)
@@ -116,61 +151,79 @@ Proof.
   by eapply (fill_contextual_step (PlusRCtx e1 HoleCtx)).
 Qed.
 
+Ltac is_val_to_val v H :=
+  rewrite (is_val_spec _) in H; destruct H as [v H]; apply of_to_val in H; symmetry in H.
+
 Lemma contextual_step_pair_l e1 e1' e2:
   is_val e2 →
   contextual_step e1 e1' →
   contextual_step (Pair e1 e2) (Pair e1' e2).
 Proof.
-  (* TODO: exercise *)
-Admitted.
-
+  intros H_val H_ctx.
+  is_val_to_val v2 H_val.
+  rewrite H_val.
+  eapply (fill_contextual_step (PairLCtx HoleCtx v2)).
+  assumption.
+Qed.
 
 Lemma contextual_step_pair_r e1 e2 e2':
   contextual_step e2 e2' →
   contextual_step (Pair e1 e2) (Pair e1 e2').
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_ctx.
+  eapply (fill_contextual_step (PairRCtx e1 HoleCtx)).
+  assumption.
+Qed.
 
 
 Lemma contextual_step_fst e e':
   contextual_step e e' →
   contextual_step (Fst e) (Fst e').
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_ctx.
+  eapply (fill_contextual_step (FstCtx HoleCtx)).
+  assumption.
+Qed.
 
 
 Lemma contextual_step_snd e e':
   contextual_step e e' →
   contextual_step (Snd e) (Snd e').
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_ctx.
+  eapply (fill_contextual_step (SndCtx HoleCtx)).
+  assumption.
+Qed.
 
 
 Lemma contextual_step_injl e e':
   contextual_step e e' →
   contextual_step (InjL e) (InjL e').
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_ctx.
+  eapply (fill_contextual_step (InjLCtx HoleCtx)).
+  assumption.
+Qed.
 
 
 Lemma contextual_step_injr e e':
   contextual_step e e' →
   contextual_step (InjR e) (InjR e').
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_ctx.
+  eapply (fill_contextual_step (InjRCtx HoleCtx)).
+  assumption.
+Qed.
 
 
 Lemma contextual_step_case e e' e1 e2:
   contextual_step e e' →
   contextual_step (Case e e1 e2) (Case e' e1 e2).
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_ctx.
+  eapply (fill_contextual_step (CaseCtx HoleCtx e1 e2)).
+  assumption.
+Qed.
 
 
 #[global]

theories/type_systems/stlc_extended/ctxstep_sol.v

@@ -0,0 +1,211 @@
+From semantics.ts.stlc_extended Require Export lang.
+
+(** The stepping relation *)
+
+Inductive base_step : expr → expr → Prop :=
+  | BetaS x e1 e2 e' :
+     is_val e2 →
+     e' = subst' x e2 e1 →
+     base_step (App (Lam x e1) e2) e'
+  | PlusS e1 e2 (n1 n2 n3 : Z):
+     e1 = (LitInt n1) →
+     e2 = (LitInt n2) →
+     (n1 + n2)%Z = n3 →
+     base_step (Plus e1 e2) (LitInt n3)
+  | FstS e1 e2 :
+    is_val e1 →
+    is_val e2 →
+    base_step (Fst (Pair e1 e2)) e1
+  | SndS e1 e2 :
+    is_val e1 →
+    is_val e2 →
+    base_step (Snd (Pair e1 e2)) e2
+  | CaseLS e e1 e2 :
+    is_val e →
+    base_step (Case (InjL e) e1 e2) (App e1 e)
+  | CaseRS e e1 e2 :
+    is_val e →
+    base_step (Case (InjR e) e1 e2) (App e2 e)
+.
+
+#[export] Hint Constructors base_step : core.
+
+(** We define evaluation contexts *)
+Inductive ectx :=
+  | HoleCtx
+  | AppLCtx (K: ectx) (v2 : val)
+  | AppRCtx (e1 : expr) (K: ectx)
+  | PlusLCtx (K: ectx) (v2 : val)
+  | PlusRCtx (e1 : expr) (K: ectx)
+  | PairLCtx (K: ectx) (v2 : val)
+  | PairRCtx (e1 : expr) (K: ectx)
+  | FstCtx (K: ectx)
+  | SndCtx (K: ectx)
+  | InjLCtx (K: ectx)
+  | InjRCtx (K: ectx)
+  | CaseCtx (K: ectx) (e1 : expr) (e2 : expr)
+.
+
+Fixpoint fill (K : ectx) (e : expr) : expr :=
+  match K with
+  | HoleCtx => e
+  | AppLCtx K v2 => App (fill K e) (of_val v2)
+  | AppRCtx e1 K => App e1 (fill K e)
+  | PlusLCtx K v2 => Plus (fill K e) (of_val v2)
+  | PlusRCtx e1 K => Plus e1 (fill K e)
+  | PairLCtx K v2 => Pair (fill K e) (of_val v2)
+  | PairRCtx e1 K => Pair e1 (fill K e)
+  | FstCtx K => Fst (fill K e)
+  | SndCtx K => Snd (fill K e)
+  | InjLCtx K => InjL (fill K e)
+  | InjRCtx K => InjR (fill K e)
+  | CaseCtx K e1 e2 => Case (fill K e) e1 e2
+  end.
+
+Fixpoint comp_ectx (K: ectx) (K' : ectx) : ectx :=
+  match K with
+  | HoleCtx => K'
+  | AppLCtx K v2 => AppLCtx (comp_ectx K K') v2
+  | AppRCtx e1 K => AppRCtx e1 (comp_ectx K K')
+  | PlusLCtx K v2 => PlusLCtx (comp_ectx K K') v2
+  | PlusRCtx e1 K => PlusRCtx e1 (comp_ectx K K')
+  | PairLCtx K v2 => PairLCtx (comp_ectx K K') v2
+  | PairRCtx e1 K => PairRCtx e1 (comp_ectx K K')
+  | FstCtx K => FstCtx (comp_ectx K K')
+  | SndCtx K => SndCtx (comp_ectx K K')
+  | InjLCtx K => InjLCtx (comp_ectx K K')
+  | InjRCtx K => InjRCtx (comp_ectx K K')
+  | CaseCtx K e1 e2 => CaseCtx (comp_ectx K K') e1 e2
+  end.
+
+(** Contextual steps *)
+Inductive contextual_step (e1 : expr) (e2 : expr) : Prop :=
+  Ectx_step K e1' e2' :
+    e1 = fill K e1' → e2 = fill K e2' →
+    base_step e1' e2' → contextual_step e1 e2.
+
+#[export] Hint Constructors contextual_step : core.
+
+Definition reducible (e : expr) :=
+  ∃ e', contextual_step e e'.
+
+Definition empty_ectx := HoleCtx.
+
+(** Basic properties about the language *)
+Lemma fill_empty e : fill empty_ectx e = e.
+Proof. done. Qed.
+
+Lemma fill_comp (K1 K2 : ectx) e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e.
+Proof. induction K1; simpl; congruence. Qed.
+
+Lemma base_contextual_step e1 e2 :
+  base_step e1 e2 → contextual_step e1 e2.
+Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
+
+Lemma fill_contextual_step K e1 e2 :
+  contextual_step e1 e2 → contextual_step (fill K e1) (fill K e2).
+Proof.
+  destruct 1 as [K' e1' e2' -> ->].
+  rewrite !fill_comp. by econstructor.
+Qed.
+
+(** We derive a few lemmas about contextual steps:
+  these essentially provide rules for structural lifting
+   akin to the structural semantics.
+ *)
+Lemma contextual_step_app_l e1 e1' e2:
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (App e1 e2) (App e1' e2).
+Proof.
+  intros [v <-%of_to_val]%is_val_spec Hcontextual.
+  by eapply (fill_contextual_step (AppLCtx HoleCtx v)).
+Qed.
+
+Lemma contextual_step_app_r e1 e2 e2':
+  contextual_step e2 e2' →
+  contextual_step (App e1 e2) (App e1 e2').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (AppRCtx e1 HoleCtx)).
+Qed.
+
+Lemma contextual_step_plus_l e1 e1' e2:
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (Plus e1 e2) (Plus e1' e2).
+Proof.
+  intros [v <-%of_to_val]%is_val_spec Hcontextual.
+  by eapply (fill_contextual_step (PlusLCtx HoleCtx v)).
+Qed.
+
+Lemma contextual_step_plus_r e1 e2 e2':
+  contextual_step e2 e2' →
+  contextual_step (Plus e1 e2) (Plus e1 e2').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (PlusRCtx e1 HoleCtx)).
+Qed.
+
+Lemma contextual_step_pair_l e1 e1' e2:
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (Pair e1 e2) (Pair e1' e2).
+Proof.
+  intros [v <-%of_to_val]%is_val_spec Hcontextual.
+  by eapply (fill_contextual_step (PairLCtx HoleCtx v)).
+Qed.
+
+Lemma contextual_step_pair_r e1 e2 e2':
+  contextual_step e2 e2' →
+  contextual_step (Pair e1 e2) (Pair e1 e2').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (PairRCtx e1 HoleCtx)).
+Qed.
+
+Lemma contextual_step_fst e e':
+  contextual_step e e' →
+  contextual_step (Fst e) (Fst e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (FstCtx HoleCtx)).
+Qed.
+
+Lemma contextual_step_snd e e':
+  contextual_step e e' →
+  contextual_step (Snd e) (Snd e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (SndCtx HoleCtx)).
+Qed.
+
+Lemma contextual_step_injl e e':
+  contextual_step e e' →
+  contextual_step (InjL e) (InjL e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (InjLCtx HoleCtx)).
+Qed.
+
+Lemma contextual_step_injr e e':
+  contextual_step e e' →
+  contextual_step (InjR e) (InjR e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (InjRCtx HoleCtx)).
+Qed.
+
+Lemma contextual_step_case e e' e1 e2:
+  contextual_step e e' →
+  contextual_step (Case e e1 e2) (Case e' e1 e2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (CaseCtx HoleCtx e1 e2)).
+Qed.
+
+#[global]
+Hint Resolve
+  contextual_step_app_l contextual_step_app_r contextual_step_plus_l contextual_step_plus_r
+  contextual_step_case contextual_step_fst contextual_step_injl contextual_step_injr
+  contextual_step_pair_l contextual_step_pair_r contextual_step_snd : core.

theories/type_systems/stlc_extended/logrel.v

@@ -0,0 +1,307 @@
+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 bigstep.
+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) =>
+    (* TODO: add type interpretation *) 
+    False;
+  type_interp (inj_val v) (A + B) =>
+    (* TODO: add type interpretation *)
+    False;
+  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.
+(* Uncomment the following once you have amended the type interpretation to
+   solve the new obligations: *)
+(*
+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.
+  (* TODO: exercise *)
+Admitted.
+
+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 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. *)
+  (* TODO: exercise *)
+Admitted.
+
+
+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.
+

theories/type_systems/stlc_extended/parallel_subst.v

@@ -0,0 +1,193 @@
+From stdpp Require Import prelude.
+From iris Require Import prelude.
+From semantics.ts.stlc_extended Require Import lang.
+From semantics.lib Require Import maps.
+
+Fixpoint subst_map (xs : gmap string expr) (e : expr) : expr :=
+  match e with
+  | LitInt n => LitInt n
+  | Var y => match xs !! y with Some es => es | _ =>  Var y end
+  | App e1 e2 => App (subst_map xs e1) (subst_map xs e2)
+  | Lam x e => Lam x (subst_map (binder_delete x xs) e)
+  | Plus e1 e2 => Plus (subst_map xs e1) (subst_map xs e2)
+  | Pair e1 e2 => Pair (subst_map xs e1) (subst_map xs e2)
+  | Fst e => Fst (subst_map xs e)
+  | Snd e => Snd (subst_map xs e)
+  | InjL e => InjL (subst_map xs e)
+  | InjR e => InjR (subst_map xs e)
+  | Case e e1 e2 => Case (subst_map xs e) (subst_map xs e1) (subst_map xs e2)
+  end.
+
+
+Lemma subst_map_empty e :
+  subst_map ∅ e = e.
+Proof.
+  induction e; simpl; f_equal; eauto.
+  destruct x; simpl; [done | by rewrite !delete_empty..].
+Qed.
+
+
+
+Lemma subst_map_closed X e xs :
+  closed X e →
+  (∀ x : string, x ∈ dom xs → x ∉ X) →
+  subst_map xs e = e.
+Proof.
+  intros Hclosed Hd.
+  induction e in xs, X, Hd, Hclosed |-*; simpl in *;try done.
+  { (* Var *)
+    apply bool_decide_spec in Hclosed.
+    assert (xs !! x = None) as ->; last done.
+    destruct (xs !! x) as [s | ] eqn:Helem; last done.
+    exfalso; eapply Hd; last apply Hclosed.
+    apply elem_of_dom; eauto.
+  }
+  { (* lambdas *)
+    erewrite IHe; [done | done |].
+    intros y. destruct x as [ | x]; first apply Hd.
+    simpl.
+    rewrite dom_delete elem_of_difference not_elem_of_singleton.
+    intros [Hnx%Hd Hneq]. rewrite elem_of_cons. intros [? | ?]; done.
+  }
+  (* all other cases *)
+  all: unfold closed in *; simpl in *.
+  all: repeat match goal with
+  | H : Is_true (_ && _)  |- _ => apply andb_True in H as [ ? ? ]
+              end.
+  all: repeat match goal with
+       | H : ∀ _ _, _ → _ → subst_map _ _ = _ |- _ => erewrite H; clear H
+       end; try done.
+Qed.
+
+Lemma subst_map_subst map x (e e': expr) :
+  closed [] e' →
+  subst_map map (subst x e' e) = subst_map (<[x:=e']>map) e.
+Proof.
+  intros He'; induction e as [y|y e IH | | | | | | | | | ]in map|-*; simpl; try (f_equal; eauto).
+  - case_decide.
+    + simplify_eq/=. rewrite lookup_insert.
+      rewrite (subst_map_closed []); [done | apply He' | ].
+      intros ? ?. apply not_elem_of_nil.
+    + rewrite lookup_insert_ne; done.
+  - destruct y; simpl; first done.
+    + case_decide.
+      * simplify_eq/=. by rewrite delete_insert_delete.
+      * rewrite delete_insert_ne; last by congruence. done.
+Qed.
+
+(** We lift the notion of closedness [closed] to substitution maps. *)
+Definition subst_closed (X : list string) (map : gmap string expr) :=
+  ∀ x e, map !! x = Some e → closed X e.
+Lemma subst_closed_subseteq X map1 map2 :
+  map1 ⊆ map2 → subst_closed X map2 → subst_closed X map1.
+Proof.
+  intros Hsub Hclosed2 x e Hl. eapply Hclosed2, map_subseteq_spec; done.
+Qed.
+
+Lemma subst_closed_weaken X Y map1 map2 :
+  Y ⊆ X → map1 ⊆ map2 → subst_closed Y map2 → subst_closed X map1.
+Proof.
+  intros Hsub1 Hsub2 Hclosed2 x e Hl.
+  eapply is_closed_weaken. 1:eapply Hclosed2, map_subseteq_spec; done. done.
+Qed.
+
+(** Lemma about the interaction with "normal" substitution. *)
+Lemma subst_subst_map x es map e :
+  subst_closed [] map →
+  subst x es (subst_map (delete x map) e) =
+  subst_map (<[x:=es]> map) e.
+Proof.
+  revert map es x; induction e; intros map v0 xx Hclosed; simpl;
+  try (f_equal; eauto).
+  - destruct (decide (xx=x)) as [->|Hne].
+    + rewrite lookup_delete // lookup_insert //. simpl.
+      rewrite decide_True //.
+    + rewrite lookup_delete_ne // lookup_insert_ne //.
+      destruct (_ !! x) as [rr|] eqn:Helem.
+      * apply Hclosed in Helem.
+        by apply subst_is_closed_nil.
+      * simpl. rewrite decide_False //.
+  - destruct x; simpl; first by auto.
+    case_decide.
+    + simplify_eq. rewrite delete_idemp delete_insert_delete. done.
+    + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. apply IHe.
+      eapply subst_closed_subseteq; last done.
+      apply map_delete_subseteq.
+Qed.
+
+Lemma subst'_subst_map b (es : expr) map e :
+  subst_closed [] map →
+  subst' b es (subst_map (binder_delete b map) e) =
+  subst_map (binder_insert b es map) e.
+Proof.
+  destruct b; first done.
+  apply subst_subst_map.
+Qed.
+
+Lemma closed_subst_weaken e map X Y :
+  subst_closed [] map →
+  (∀ x, x ∈ X → x ∉ dom map → x ∈ Y) →
+  closed X e →
+  closed Y (subst_map map e).
+Proof.
+  induction e in X, Y, map |-*; simpl; intros Hmclosed Hsub Hcl.
+  { (* vars *)
+    destruct (map !! x) as [es | ] eqn:Heq.
+    + apply is_closed_weaken_nil. by eapply Hmclosed.
+    + apply bool_decide_pack. apply Hsub; first by eapply bool_decide_unpack.
+      by apply not_elem_of_dom.
+  }
+  { (* lambdas *)
+    eapply IHe; last done.
+    + eapply subst_closed_subseteq; last done.
+      destruct x; first done. apply map_delete_subseteq.
+    + intros y. destruct x as [ | x]; first by apply Hsub.
+      rewrite !elem_of_cons. intros [-> | Hy] Hn; first by left.
+      destruct (decide (y = x)) as [ -> | Hneq]; first by left.
+      right. eapply Hsub; first done. set_solver.
+  }
+  (* all other cases *)
+  all: unfold closed in *; simpl in *.
+  all: repeat match goal with
+         | H : Is_true (_ && _)  |- _ => apply andb_True in H as [ ? ? ]
+              end.
+  all: repeat match goal with
+         | |- Is_true (_ && _) => apply andb_True; split
+              end.
+  all: try naive_solver.
+Qed.
+
+
+Lemma subst_map_closed' X Y Θ e:
+  closed Y e →
+  (∀ x, x ∈ Y → if Θ !! x is (Some e') then closed X e' else x ∈ X) →
+  closed X (subst_map Θ e).
+Proof.
+  induction e in X, Θ, Y |-*; simpl.
+  { intros Hel%bool_decide_unpack Hcl.
+    eapply Hcl in Hel.
+    destruct (Θ !! x); first done.
+    simpl. by eapply bool_decide_pack. }
+  { 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. }
+  all: unfold closed; simpl; naive_solver.
+Qed.
+
+Lemma subst_map_closed'_2 X Θ e:
+  closed (X ++ (elements (dom Θ))) e ->
+  subst_closed X Θ ->
+  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.

theories/type_systems/stlc_extended/types_sol.v

@@ -0,0 +1,350 @@
+From stdpp Require Import base relations.
+From iris Require Import prelude.
+From semantics.lib Require Import maps.
+From semantics.ts.stlc_extended Require Import lang notation ctxstep_sol.
+
+(** ** Syntactic typing *)
+Inductive type : Type :=
+  | Int
+  | Fun (A B : type)
+  | Prod (A B : type)
+  | Sum (A B : type).
+
+Definition typing_context := gmap string type.
+Implicit Types
+  (Γ : typing_context)
+  (v : val)
+  (e : expr).
+
+Declare Scope FType_scope.
+Delimit Scope FType_scope with ty.
+Bind Scope FType_scope with type.
+Infix "→" := Fun : FType_scope.
+Notation "(→)" := Fun (only parsing) : FType_scope.
+Infix "×" := Prod (at level 70) : FType_scope.
+Notation "(×)" := Prod (only parsing) : FType_scope.
+Infix "+" := Sum : FType_scope.
+Notation "(+)" := Sum (only parsing) : FType_scope.
+
+Reserved Notation "Γ ⊢ e : A" (at level 74, e, A at next level).
+
+Inductive syn_typed : typing_context → expr → type → Prop :=
+  | typed_var Γ x A :
+      Γ !! x = Some A →
+      Γ ⊢ (Var x) : A
+  | typed_lam Γ x e A B :
+      (<[ x := A]> Γ) ⊢ e : B →
+      Γ ⊢ (Lam (BNamed x) e) : (A → B)
+  | typed_lam_anon Γ e A B :
+      Γ ⊢ e : B →
+      Γ ⊢ (Lam BAnon e) : (A → B)
+  | typed_int Γ z : Γ ⊢ (LitInt z) : Int
+  | typed_app Γ e1 e2 A B :
+      Γ ⊢ e1 : (A → B) →
+      Γ ⊢ e2 : A →
+      Γ ⊢ (e1 e2)%E : B
+  | typed_add Γ e1 e2 :
+      Γ ⊢ e1 : Int →
+      Γ ⊢ e2 : Int →
+      Γ ⊢ e1 + e2 : Int
+  | typed_pair Γ e1 e2 A B :
+      Γ ⊢ e1 : A →
+      Γ ⊢ e2 : B →
+      Γ ⊢ (e1, e2) : A × B
+  | typed_fst Γ e A B :
+      Γ ⊢ e : A × B →
+      Γ ⊢ Fst e : A
+  | typed_snd Γ e A B :
+      Γ ⊢ e : A × B →
+      Γ ⊢ Snd e : B
+  | typed_injl Γ e A B :
+      Γ ⊢ e : A →
+      Γ ⊢ InjL e : A + B
+  | typed_injr Γ e A B :
+      Γ ⊢ e : B →
+      Γ ⊢ InjR e : A + B
+  | typed_case Γ e e1 e2 A B C :
+      Γ ⊢ e : B + C →
+      Γ ⊢ e1 : (B → A) →
+      Γ ⊢ e2 : (C → A) →
+      Γ ⊢ Case e e1 e2 : A
+where "Γ ⊢ e : A" := (syn_typed Γ e%E A%ty).
+#[export] Hint Constructors syn_typed : core.
+
+(** Examples *)
+Goal ∅ ⊢ (λ: "x", "x")%E : (Int → Int).
+Proof. eauto. Qed.
+
+Lemma syn_typed_closed Γ e A X :
+  Γ ⊢ e : A →
+  (∀ x, x ∈ dom Γ → x ∈ X) →
+  is_closed X e.
+Proof.
+  (* TODO: you will need to add the new cases, i.e. "|"'s to the intro pattern. The proof then should go through *)
+  induction 1 as [ | ?????? IH | | | | | | | | | | ] in X |-*; simpl; intros Hx; try done.
+  { (* var *) apply bool_decide_pack, Hx. apply elem_of_dom; eauto. }
+  { (* lam *) apply IH.
+    intros y. rewrite elem_of_dom lookup_insert_is_Some.
+    intros [<- | [? Hy]]; first by apply elem_of_cons; eauto.
+    apply elem_of_cons. right. eapply Hx. by apply elem_of_dom.
+  }
+  { (* anon lam *) naive_solver. }
+  (* everything else *)
+  all: repeat match goal with
+              | |- Is_true (_ && _)  => apply andb_True; split
+              end.
+  all: try naive_solver.
+Qed.
+
+Lemma typed_weakening Γ Δ e A:
+  Γ ⊢ e : A →
+  Γ ⊆ Δ →
+  Δ ⊢ e : A.
+Proof.
+  (* TODO: here you will need to add the new cases to the intro pattern as well. The proof then should go through *)
+  induction 1 as [| Γ x e A B Htyp IH | | | | | | | | | |] in Δ |-*; intros Hsub; eauto.
+  - (* var *) econstructor. by eapply lookup_weaken.
+  - (* lam *) econstructor. eapply IH; eauto. by eapply insert_mono.
+Qed.
+
+(** Typing inversion lemmas *)
+Lemma var_inversion Γ (x: string) A: Γ ⊢ x : A → Γ !! x = Some A.
+Proof. inversion 1; subst; auto. Qed.
+
+Lemma lam_inversion Γ (x: string) e C:
+  Γ ⊢ (λ: x, e) : C →
+  ∃ A B, C = (A → B)%ty ∧ <[x:=A]> Γ ⊢ e : B.
+Proof. inversion 1; subst; eauto 10. Qed.
+
+Lemma lam_anon_inversion Γ e C:
+  Γ ⊢ (λ: <>, e) : C →
+  ∃ A B, C = (A → B)%ty ∧ Γ ⊢ e : B.
+Proof. inversion 1; subst; eauto 10. Qed.
+
+Lemma app_inversion Γ e1 e2 B:
+  Γ ⊢ e1 e2 : B →
+  ∃ A, Γ ⊢ e1 : (A → B) ∧ Γ ⊢ e2 : A.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma plus_inversion Γ e1 e2 B:
+  Γ ⊢ e1 + e2 : B →
+  B = Int ∧ Γ ⊢ e1 : Int ∧ Γ ⊢ e2 : Int.
+Proof. inversion 1; subst; eauto. Qed.
+
+
+(* There are the inversion lemmas for the new typing rules *)
+Lemma pair_inversion Γ e1 e2 C :
+  Γ ⊢ (e1, e2) : C →
+  ∃ A B, C = (A × B)%ty ∧ Γ ⊢ e1 : A ∧ Γ ⊢ e2 : B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma fst_inversion Γ e A :
+  Γ ⊢ Fst e : A →
+  ∃ B, Γ ⊢ e : A × B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma snd_inversion Γ e B :
+  Γ ⊢ Snd e : B →
+  ∃ A, Γ ⊢ e : A × B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma injl_inversion Γ e C :
+  Γ ⊢ InjL e : C →
+  ∃ A B, C = (A + B)%ty ∧ Γ ⊢ e : A.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma injr_inversion Γ e C :
+  Γ ⊢ InjR e : C →
+  ∃ A B, C = (A + B)%ty ∧ Γ ⊢ e : B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma case_inversion Γ e e1 e2 A :
+  Γ ⊢ Case e e1 e2 : A →
+  ∃ B C, Γ ⊢ e : B + C ∧ Γ ⊢ e1 : (B → A) ∧ Γ ⊢ e2 : (C → A).
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma typed_substitutivity e e' Γ (x: string) A B :
+  ∅ ⊢ e' : A →
+  (<[x := A]> Γ) ⊢ e : B →
+  Γ ⊢ lang.subst x e' e : B.
+Proof.
+  intros He'. revert B Γ; induction e as [y | y | | | | | | |  | | ]; intros B Γ; simpl.
+  - intros Hp % var_inversion.
+    destruct (decide (x = y)).
+    + subst. rewrite lookup_insert in Hp. injection Hp as ->.
+      eapply typed_weakening; [done| ]. apply map_empty_subseteq.
+    + rewrite lookup_insert_ne in Hp; last done. auto.
+  - destruct y as [ | y].
+    { intros (A' & C & -> & Hty) % lam_anon_inversion.
+      econstructor. destruct decide as [Heq|].
+      + congruence.
+      + eauto.
+    }
+    intros (A' & C & -> & Hty) % lam_inversion.
+    econstructor. destruct decide as [Heq|].
+    + injection Heq as [= ->]. by rewrite insert_insert in Hty.
+    + rewrite insert_commute in Hty; last naive_solver. eauto.
+  - intros (C & Hty1 & Hty2) % app_inversion. eauto.
+  - inversion 1; subst; auto.
+  - intros (-> & Hty1 & Hty2)%plus_inversion; eauto.
+  - intros (? & ? & -> & ? & ?) % pair_inversion. eauto.
+  - intros (? & ?)%fst_inversion. eauto.
+  - intros (? & ?)%snd_inversion. eauto.
+  - intros (? & ? & -> & ?)%injl_inversion. eauto.
+  - intros (? & ? & -> & ?)%injr_inversion. eauto.
+  - intros (? & ? & ? & ? & ?)%case_inversion. eauto.
+Qed.
+
+(** Canonical values *)
+Lemma canonical_values_arr Γ e A B:
+  Γ ⊢ e : (A → B) →
+  is_val e →
+  ∃ x e', e = (λ: x, e')%E.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_int Γ e:
+  Γ ⊢ e : Int →
+  is_val e →
+  ∃ n: Z, e = (#n)%E.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+(* canonical forms lemmas for the new types *)
+Lemma canonical_values_prod Γ e A B :
+  Γ ⊢ e : A × B →
+  is_val e →
+  ∃ e1 e2, e = (e1, e2)%E ∧ is_val e1 ∧ is_val e2.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_sum Γ e A B :
+  Γ ⊢ e : A + B →
+  is_val e →
+  (∃ e', e = InjL e' ∧ is_val e') ∨ (∃ e', e = InjR e' ∧ is_val e').
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+(** Progress *)
+Lemma typed_progress e A:
+  ∅ ⊢ e : A → is_val e ∨ reducible e.
+Proof.
+  remember ∅ as Γ.
+  (* TODO: you will need to extend the intro pattern *)
+  induction 1 as [| | | | Γ e1 e2 A B Hty IH1 _ IH2 | Γ e1 e2 Hty1 IH1 Hty2 IH2 | Γ e1 e2 A B Hty1 IH1 Hty2 IH2 | Γ e A B Hty IH | Γ e A B Hty IH | Γ e A B Hty IH | Γ e A B Hty IH| Γ e e1 e2 A B C Htye IHe Htye1 IHe1 Htye2 IHe2].
+  - subst. naive_solver.
+  - left. done.
+  - left. done.
+  - (* int *)left. done.
+  - (* app *)
+    destruct (IH2 HeqΓ) as [H2|H2]; [destruct (IH1 HeqΓ) as [H1|H1]|].
+    + eapply canonical_values_arr in Hty as (x & e & ->); last done.
+      right. eexists.
+      eapply base_contextual_step, BetaS; eauto.
+    + right. destruct H1 as [e1' Hstep].
+      eexists. eauto.
+    + right. destruct H2 as [e2' H2].
+      eexists. eauto.
+  - (* plus *)
+    destruct (IH2 HeqΓ) as [H2|H2]; [destruct (IH1 HeqΓ) as [H1|H1]|].
+    + right. eapply canonical_values_int in Hty1 as [n1 ->]; last done.
+      eapply canonical_values_int in Hty2 as [n2 ->]; last done.
+      subst. eexists; eapply base_contextual_step. eauto.
+    + right. destruct H1 as [e1' Hstep]. eexists. eauto.
+    + right. destruct H2 as [e2' H2]. eexists. eauto.
+- (* pair *)
+    destruct (IH2 HeqΓ) as [H2|H2]; [destruct (IH1 HeqΓ) as [H1|H1]|].
+    + left. done.
+    + right. destruct H1 as [e1' Hstep]. eexists. eauto.
+    + right. destruct H2 as [e2' H2]. eexists. eauto.
+  - (* fst *)
+    destruct (IH HeqΓ) as [H | H].
+    + eapply canonical_values_prod in Hty as (e1 & e2 & -> & ? & ?); last done.
+      right. eexists. eapply base_contextual_step. econstructor; done.
+    + right. destruct H as [e' H]. eexists. eauto.
+  - (* snd *)
+    destruct (IH HeqΓ) as [H | H].
+    + eapply canonical_values_prod in Hty as (e1 & e2 & -> & ? & ?); last done.
+      right. eexists. eapply base_contextual_step. econstructor; done.
+    + right. destruct H as [e' H]. eexists. eauto.
+  - (* injl *)
+    destruct (IH HeqΓ) as [H | H].
+    + left. done.
+    + right. destruct H as [e' H]. eexists. eauto.
+  - (* injr *)
+    destruct (IH HeqΓ) as [H | H].
+    + left. done.
+    + right. destruct H as [e' H]. eexists. eauto.
+  - (* case *)
+    right. destruct (IHe HeqΓ) as [H1|H1].
+    + eapply canonical_values_sum in Htye as [(e' & -> & ?) | (e' & -> & ?)]; last done.
+      * eexists. eapply base_contextual_step. econstructor. done.
+      * eexists. eapply base_contextual_step. econstructor. done.
+    + destruct H1 as [e' H1]. eexists. eauto.
+  Qed.
+
+
+Definition ectx_typing (K: ectx) (A B: type) :=
+  ∀ e, ∅ ⊢ e : A → ∅ ⊢ (fill K e) : B.
+
+Lemma fill_typing_decompose K e A:
+  ∅ ⊢ fill K e : A →
+  ∃ B, ∅ ⊢ e : B ∧ ectx_typing K B A.
+Proof.
+  unfold ectx_typing; induction K in e,A |-*; simpl; eauto.
+  all: inversion 1; subst; edestruct IHK as [? [Hit Hty]]; eauto.
+Qed.
+
+Lemma fill_typing_compose K e A B:
+  ∅ ⊢ e : B →
+  ectx_typing K B A →
+  ∅ ⊢ fill K e : A.
+Proof.
+  intros H1 H2; by eapply H2.
+Qed.
+
+Lemma typed_preservation_base_step e e' A:
+  ∅ ⊢ e : A →
+  base_step e e' →
+  ∅ ⊢ e' : A.
+Proof.
+  intros Hty Hstep.
+  destruct Hstep as [  ]; subst.
+  - eapply app_inversion in Hty as (B & H1 & H2).
+    destruct x as [|x].
+    { eapply lam_anon_inversion in H1 as (C & D & [= -> ->] & Hty). done. }
+    eapply lam_inversion in H1 as (C & D & Heq & Hty).
+    injection Heq as -> ->.
+    eapply typed_substitutivity; eauto.
+  - eapply plus_inversion in Hty as (-> & Hty1 & Hty2). constructor.
+- by eapply fst_inversion in Hty as (B & (? & ? & [= <- <-] & ? & ?)%pair_inversion).
+  - by eapply snd_inversion in Hty as (B & (? & ? & [= <- <-] & ? & ?)%pair_inversion).
+  - eapply case_inversion in Hty as (B & C & (? & ? & [= <- <-] & Hty)%injl_inversion & ? & ?).
+    eauto.
+  - eapply case_inversion in Hty as (B & C & (? & ? & [= <- <-] & Hty )%injr_inversion & ? & ?).
+    eauto.
+Qed.
+
+
+Lemma typed_preservation e e' A:
+  ∅ ⊢ e : A →
+  contextual_step e e' →
+  ∅ ⊢ e' : A.
+Proof.
+  intros Hty Hstep. destruct Hstep as [K e1 e2 -> -> Hstep].
+  eapply fill_typing_decompose in Hty as [B [H1 H2]].
+  eapply fill_typing_compose; last done.
+  by eapply typed_preservation_base_step.
+Qed.
+
+Lemma type_safety e1 e2 A:
+  ∅ ⊢ e1 : A →
+  rtc contextual_step e1 e2 →
+  is_val e2 ∨ reducible e2.
+Proof.
+  induction 2; eauto using typed_progress, typed_preservation.
+Qed.

theories/type_systems/systemf/bigstep.v

@@ -0,0 +1,223 @@
+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 types.
+From Equations Require Import Equations.
+
+(** * Big-step semantics *)
+
+Implicit Types
+  (Δ : nat)
+  (Γ : typing_context)
+  (v : val)
+  (α : var)
+  (e : expr)
+  (A : type).
+
+Inductive big_step : expr → val → Prop :=
+  | bs_lit (l : base_lit) :
+      big_step (Lit l) (LitV l)
+  | bs_lam (x : binder) (e : expr) :
+      big_step (λ: x, e)%E (λ: x, e)%V
+  | bs_binop e1 e2 v1 v2 v' op :
+      big_step e1 v1 →
+      big_step e2 v2 →
+      bin_op_eval op v1 v2 = Some v' →
+      big_step (BinOp op e1 e2) v'
+  | bs_unop e v v' op :
+      big_step e v →
+      un_op_eval op v = Some v' →
+      big_step (UnOp op e) v'
+  | bs_app e1 e2 x e v2 v :
+      big_step e1 (LamV x e) →
+      big_step e2 v2 →
+      big_step (subst' x (of_val v2) e) v →
+      big_step (App e1 e2) v
+  | bs_tapp e1 e2 v :
+      big_step e1 (TLamV e2) →
+      big_step e2 v →
+      big_step (e1 <>) v
+  | bs_tlam e :
+      big_step (Λ, e)%E (Λ, e)%V
+  | bs_pack e v :
+      big_step e v →
+      big_step (pack e)%E (pack v)%V
+  | bs_unpack e1 e2 v1 v2 x :
+      big_step e1 (pack v1)%V →
+      big_step (subst' x (of_val v1) e2) v2 →
+      big_step (unpack e1 as x in e2) v2
+  | bs_if_true e0 e1 e2 v :
+      big_step e0 #true →
+      big_step e1 v →
+     big_step (if: e0 then e1 else e2) v
+  | bs_if_false e0 e1 e2 v :
+      big_step e0 #false →
+      big_step e2 v →
+     big_step (if: e0 then e1 else e2) v
+  | bs_pair e1 e2 v1 v2 :
+      big_step e1 v1 →
+      big_step e2 v2 →
+      big_step (e1, e2) (v1, v2)
+  | bs_fst e v1 v2 :
+      big_step e (v1, v2) →
+      big_step (Fst e) v1
+  | bs_snd e v1 v2 :
+      big_step e (v1, v2) →
+      big_step (Snd e) v2
+  | bs_injl e v :
+      big_step e v →
+      big_step (InjL e) (InjLV v)
+  | bs_injr e v :
+      big_step e v →
+      big_step (InjR e) (InjRV v)
+  | bs_casel e e1 e2 v v' :
+      big_step e (InjLV v) →
+      big_step (e1 (of_val v)) v' →
+      big_step (Case e e1 e2) v'
+  | bs_caser e e1 e2 v v' :
+      big_step e (InjRV v) →
+      big_step (e2 (of_val v)) v' →
+      big_step (Case e e1 e2) v'
+    .
+#[export] Hint Constructors big_step : core.
+#[export] Hint Constructors base_step : core.
+#[export] Hint Constructors contextual_step : core.
+
+Lemma fill_rtc_contextual_step {e1 e2} K :
+  rtc contextual_step e1 e2 →
+  rtc contextual_step (fill K e1) (fill K e2).
+Proof.
+  induction 1 as [ | x y z H1 H2 IH]; first done.
+  etrans; last apply IH.
+  econstructor 2; last constructor 1.
+  by apply fill_contextual_step.
+Qed.
+
+Lemma big_step_contextual e v :
+  big_step e v → rtc contextual_step e (of_val v).
+Proof.
+  induction 1 as [ | | e1 e2 v1 v2 v' op H1 IH1 H2 IH2 Hop | e v v' op H1 IH1 Hop | e1 e2 x e v2 v H1 IH1 H2 IH2 H3 IH3 | e1 e2 v1 H1 IH1 H2 IH2 | | | e1 e2 v1 v2 x H1 IH1 H2 IH2 | e0 e1 e2 v H1 IH1 H2 IH2 | e0 e1 e2 v H1 IH1 H2 IH2| e1 e2 v1 v2 H1 IH1 H2 IH2 | e v1 v2 H IH | e v1 v2 H IH | e v H IH | e v H IH | e e1 e2 v v' H1 IH1 H2 IH2 | e e1 e2 v v' H1 IH1 H2 IH2 ].
+  - constructor.
+  - constructor.
+  - (* binop *)
+    etrans.
+    { eapply (fill_rtc_contextual_step (BinOpRCtx _ _ HoleCtx)). apply IH2. }
+    etrans.
+    { eapply (fill_rtc_contextual_step (BinOpLCtx _ HoleCtx _)). apply IH1. }
+    simpl.
+    etrans.
+    { econstructor 2; last econstructor 1.
+      apply base_contextual_step. econstructor; last done.
+      all: apply to_of_val.
+    }
+    constructor.
+  - (* unop *)
+    etrans.
+    { eapply (fill_rtc_contextual_step (UnOpCtx _ HoleCtx)). apply IH1. }
+    simpl. etrans.
+    { econstructor 2; last econstructor 1.
+      apply base_contextual_step. econstructor; last done.
+      all: apply to_of_val.
+    }
+    constructor.
+  - etrans.
+    { eapply (fill_rtc_contextual_step (AppRCtx _ HoleCtx)). apply IH2. }
+    etrans.
+    { eapply (fill_rtc_contextual_step (AppLCtx HoleCtx _)). apply IH1. }
+    simpl. etrans.
+    { econstructor 2; last econstructor 1.
+      apply base_contextual_step. constructor; [| reflexivity]. apply is_val_of_val.
+    }
+    apply IH3.
+  - etrans.
+    { eapply (fill_rtc_contextual_step (TAppCtx HoleCtx)). apply IH1. }
+    etrans. { econstructor 2; last constructor. apply base_contextual_step. by constructor. }
+    done.
+  - constructor.
+  - etrans.
+    { eapply (fill_rtc_contextual_step (PackCtx HoleCtx)). done. }
+    done.
+  - etrans.
+    { eapply (fill_rtc_contextual_step (UnpackCtx x HoleCtx e2)). done. }
+    etrans.
+    { econstructor 2; last constructor. apply base_contextual_step. simpl. constructor; last reflexivity.
+      apply is_val_spec. rewrite to_of_val. eauto.
+    }
+    done.
+  - etrans.
+    { eapply (fill_rtc_contextual_step (IfCtx HoleCtx _ _)). done. }
+    etrans.
+    { econstructor; last constructor. eapply base_contextual_step. econstructor. }
+    done.
+  - etrans.
+    { eapply (fill_rtc_contextual_step (IfCtx HoleCtx _ _)). done. }
+    etrans.
+    { econstructor; last constructor. eapply base_contextual_step. econstructor. }
+    done.
+  - etrans.
+    { eapply (fill_rtc_contextual_step (PairRCtx e1 HoleCtx)). done. }
+    etrans.
+    {  eapply (fill_rtc_contextual_step (PairLCtx HoleCtx v2)). done. }
+    econstructor.
+  - etrans.
+    { eapply (fill_rtc_contextual_step (FstCtx HoleCtx)). done. }
+    econstructor.
+    { eapply base_contextual_step. simpl. constructor; apply is_val_of_val. }
+    econstructor.
+  - etrans.
+    { eapply (fill_rtc_contextual_step (SndCtx HoleCtx)). done. }
+    econstructor.
+    { eapply base_contextual_step. simpl. constructor; apply is_val_of_val. }
+    econstructor.
+  - etrans.
+    { eapply (fill_rtc_contextual_step (InjLCtx HoleCtx)). done. }
+    econstructor.
+  - etrans.
+    { eapply (fill_rtc_contextual_step (InjRCtx HoleCtx)). done. }
+    econstructor.
+  - etrans.
+    { eapply (fill_rtc_contextual_step (CaseCtx HoleCtx e1 e2)). done. }
+    simpl. econstructor.
+    { eapply base_contextual_step. constructor. apply is_val_of_val. }
+    done.
+  - etrans.
+    { eapply (fill_rtc_contextual_step (CaseCtx HoleCtx e1 e2)). done. }
+    simpl. econstructor.
+    { eapply base_contextual_step. constructor. apply is_val_of_val. }
+    done.
+Qed.
+
+Lemma big_step_of_val e v :
+  e = of_val v →
+  big_step e v.
+Proof.
+  intros ->.
+  induction v; simpl; eauto.
+Qed.
+
+Lemma big_step_val v v' :
+  big_step (of_val v) v' → v' = v.
+Proof.
+  enough (∀ e, big_step e v' → e = of_val v → v' = v) by naive_solver.
+  intros e Hb.
+  induction Hb in v |-*; intros Heq; subst; destruct v; inversion Heq; subst; naive_solver.
+Qed.
+
+Lemma big_step_preserve_closed e v :
+  is_closed [] e → big_step e v → is_closed [] v.
+Proof.
+  intros Hcl. induction 1; try done.
+  all: simpl in Hcl;
+    repeat match goal with
+           | H : Is_true (_ && _)  |- _ => apply andb_True in H; destruct H
+           end; try naive_solver.
+  - (* binOP *)
+    destruct v1 as [[] | | | | | |], v2 as [[] | | | | | |]; simpl in H1; try congruence.
+    destruct op; simpl in H1; inversion H1; done.
+  - (* unop *)
+    destruct v as [[] | | | | | |]; destruct op; simpl in H0; inversion H0; done.
+  - (* app *)
+    apply IHbig_step3. apply is_closed_do_subst'; naive_solver.
+  - (* unpack *)
+    apply IHbig_step2. apply is_closed_do_subst'; naive_solver.
+Qed.

theories/type_systems/systemf/exercises03.v

@@ -0,0 +1,100 @@
+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 :=
+  #0 (* TODO *).
+Definition fun_comp_type : type :=
+  #0 (* TODO *).
+Lemma fun_comp_typed :
+  TY 0; ∅ ⊢ fun_comp : fun_comp_type.
+Proof. 
+  (* should be solved by solve_typing. *)
+  (* TODO: exercise *)
+Admitted.
+
+
+Definition swap_args : val :=
+  #0 (* TODO *).
+Definition swap_args_type : type :=
+  #0 (* TODO *).
+Lemma swap_args_typed :
+  TY 0; ∅ ⊢ swap_args : swap_args_type.
+Proof. 
+  (* should be solved by solve_typing. *)
+  (* TODO: exercise *)
+Admitted.
+
+
+Definition lift_prod : val :=
+  #0 (* TODO *).
+Definition lift_prod_type : type :=
+  #0 (* TODO *).
+Lemma lift_prod_typed :
+  TY 0; ∅ ⊢ lift_prod : lift_prod_type.
+Proof. 
+  (* should be solved by solve_typing. *)
+  (* TODO: exercise *)
+Admitted.
+
+
+Definition lift_sum : val :=
+  #0 (* TODO *).
+Definition lift_sum_type : type :=
+  #0 (* TODO *).
+Lemma lift_sum_typed :
+  TY 0; ∅ ⊢ lift_sum : lift_sum_type.
+Proof. 
+  (* should be solved by solve_typing. *)
+  (* TODO: exercise *)
+Admitted.
+
+
+(** 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 :=
+  None (* FIXME *). 
+
+(* Example *)
+Goal debruijn ∅ (∀: "x", ∀: "y", "x" → "y")%pty = Some (∀: ∀: #1 → #0)%ty.
+Proof.
+  (* Should be solved by reflexivity. *)
+  (* TODO: exercise *)
+Admitted.
+
+
+Goal debruijn ∅ (∀: "x", "x" → ∀: "y", "y")%pty = Some (∀: #0 → ∀: #0)%ty.
+Proof.
+  (* Should be solved by reflexivity. *)
+  (* TODO: exercise *)
+Admitted.
+
+
+Goal debruijn ∅ (∀: "x", "x" → ∀: "y", "x")%pty = Some (∀: #0 → ∀: #1)%ty.
+Proof.
+  (* Should be solved by reflexivity. *)
+  (* TODO: exercise *)
+Admitted.
+
+

theories/type_systems/systemf/lang.v

@@ -0,0 +1,516 @@
+From stdpp Require Export binders strings.
+From iris.prelude Require Import options.
+From semantics.lib Require Export maps.
+
+Declare Scope expr_scope.
+Declare Scope val_scope.
+Delimit Scope expr_scope with E.
+Delimit Scope val_scope with V.
+
+(** Expressions and vals. *)
+Inductive base_lit : Set :=
+  | LitInt (n : Z) | LitBool (b : bool) | LitUnit.
+Inductive un_op : Set :=
+  | NegOp | MinusUnOp.
+Inductive bin_op : Set :=
+  | PlusOp | MinusOp | MultOp (* Arithmetic *)
+  | LtOp | LeOp | EqOp. (* Comparison *)
+
+
+Inductive expr :=
+  | Lit (l : base_lit)
+  (* Base lambda calculus *)
+  | Var (x : string)
+  | Lam (x : binder) (e : expr)
+  | App (e1 e2 : expr)
+  (* Base types and their operations *)
+  | UnOp (op : un_op) (e : expr)
+  | BinOp (op : bin_op) (e1 e2 : expr)
+  | If (e0 e1 e2 : expr)
+  (* Polymorphism *)
+  | TApp (e : expr)
+  | TLam (e : expr)
+  | Pack (e : expr)
+  | Unpack (x : binder) (e1 e2 : expr)
+  (* Products *)
+  | Pair (e1 e2 : expr)
+  | Fst (e : expr)
+  | Snd (e : expr)
+  (* Sums *)
+  | InjL (e : expr)
+  | InjR (e : expr)
+  | Case (e0 : expr) (e1 : expr) (e2 : expr).
+
+Bind Scope expr_scope with expr.
+
+Inductive val :=
+  | LitV (l : base_lit)
+  | LamV (x : binder) (e : expr)
+  | TLamV (e : expr)
+  | PackV (v : val)
+  | PairV (v1 v2 : val)
+  | InjLV (v : val)
+  | InjRV (v : val)
+.
+
+Bind Scope val_scope with val.
+
+Fixpoint of_val (v : val) : expr :=
+  match v with
+  | LitV l => Lit l
+  | LamV x e => Lam x e
+  | TLamV e => TLam e
+  | PackV v => Pack (of_val v)
+  | PairV v1 v2 => Pair (of_val v1) (of_val v2)
+  | InjLV v => InjL (of_val v)
+  | InjRV v => InjR (of_val v)
+  end.
+
+Fixpoint to_val (e : expr) : option val :=
+  match e with
+  | Lit l => Some $ LitV l
+  | Lam x e => Some (LamV x e)
+  | TLam e => Some (TLamV e)
+  | Pack e =>
+     to_val e ≫= (λ v, Some $ PackV v)
+  | Pair e1 e2 =>
+    to_val e1 ≫= (λ v1, to_val e2 ≫= (λ v2, Some $ PairV v1 v2))
+  | InjL e => to_val e ≫= (λ v, Some $ InjLV v)
+  | InjR e => to_val e ≫= (λ v, Some $ InjRV v)
+  | _ => None
+  end.
+
+(** Equality and other typeclass stuff *)
+Lemma to_of_val v : to_val (of_val v) = Some v.
+Proof.
+  by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
+Qed.
+
+Lemma of_to_val e v : to_val e = Some v → of_val v = e.
+Proof.
+  revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
+Qed.
+
+#[export] Instance of_val_inj : Inj (=) (=) of_val.
+Proof. by intros ?? Hv; apply (inj Some); rewrite <-!to_of_val, Hv. Qed.
+
+(** structural computational version *)
+Fixpoint is_val (e : expr) : Prop :=
+  match e with
+  | Lit l => True
+  | Lam x e => True
+  | TLam e => True
+  | Pack e => is_val e
+  | Pair e1 e2 => is_val e1 ∧ is_val e2
+  | InjL e => is_val e
+  | InjR e => is_val e
+  | _ => False
+  end.
+Lemma is_val_spec e : is_val e ↔ ∃ v, to_val e = Some v.
+Proof.
+  induction e as [ | | ? e IH | e1 IH1 e2 IH2 | e IH | ? e1 IH1 e2 IH2 | e1 IH1 e2 IH2 e3 IH3 | e IH | e IH | e IH | ? e1 IH1 e2 IH2 | e1 IH1 e2 IH2 | e IH | e IH | e IH | e IH | e1 IH1 e2 IH2 e3 IH3 ];
+    simpl; (split; [ | intros (v & Heq)]); simplify_option_eq; try done; eauto.
+  - rewrite IH. intros (v & ->). eauto.
+  - apply IH. eauto.
+  - rewrite IH1, IH2. intros [(v1 & ->) (v2 & ->)]. eauto.
+  - rewrite IH1, IH2. eauto.
+  - rewrite IH. intros (v & ->). eauto.
+  - apply IH. eauto.
+  - rewrite IH. intros (v & ->); eauto.
+  - apply IH. eauto.
+Qed.
+
+Ltac simplify_val :=
+  repeat match goal with
+  | H: to_val (of_val ?v) = ?o |- _ => rewrite to_of_val in H
+  | H: is_val ?e |- _ => destruct (proj1 (is_val_spec e) H) as (? & ?); clear H
+  end.
+
+(* Misc *)
+Lemma is_val_of_val v : is_val (of_val v).
+Proof. apply is_val_spec. rewrite to_of_val. eauto. Qed.
+
+(* literals and our operators have decidable equality. *)
+Global Instance base_lit_eq_dec : EqDecision base_lit.
+Proof. solve_decision. Defined.
+Global Instance un_op_eq_dec : EqDecision un_op.
+Proof. solve_decision. Defined.
+Global Instance bin_op_eq_dec : EqDecision bin_op.
+Proof. solve_decision. Defined.
+
+
+(** Substitution *)
+Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
+  match e with
+  | Lit _ => e
+  | Var y => if decide (x = y) then es else Var y
+  | Lam y e =>
+      Lam y $ if decide (BNamed x = y) then e else subst x es e
+  | App e1 e2 => App (subst x es e1) (subst x es e2)
+  | TApp e => TApp (subst x es e)
+  | TLam e => TLam (subst x es e)
+  | Pack e => Pack (subst x es e)
+  | Unpack y e1 e2 => Unpack y (subst x es e1) (if decide (BNamed x = y) then e2 else subst x es e2)
+  | UnOp op e => UnOp op (subst x es e)
+  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
+  | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
+  | Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
+  | Fst e => Fst (subst x es e)
+  | Snd e => Snd (subst x es e)
+  | InjL e => InjL (subst x es e)
+  | InjR e => InjR (subst x es e)
+  | Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
+  end.
+
+Definition subst' (mx : binder) (es : expr) : expr → expr :=
+  match mx with BNamed x => subst x es | BAnon => id end.
+
+(** The stepping relation *)
+Definition un_op_eval (op : un_op) (v : val) : option val :=
+  match op, v with
+  | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
+  | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
+  | _, _ => None
+  end.
+
+Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : option base_lit :=
+  match op with
+  | PlusOp => Some $ LitInt (n1 + n2)
+  | MinusOp => Some $ LitInt (n1 - n2)
+  | MultOp => Some $ LitInt (n1 * n2)
+  | LtOp => Some $ LitBool (bool_decide (n1 < n2))
+  | LeOp => Some $ LitBool (bool_decide (n1 ≤ n2))
+  | EqOp => Some $ LitBool (bool_decide (n1 = n2))
+  end%Z.
+
+Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
+  match v1, v2 with
+  | LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
+  | _, _ => None
+  end.
+
+Inductive base_step : expr → expr → Prop :=
+  | BetaS x e1 e2 e' :
+     is_val e2 →
+     e' = subst' x e2 e1 →
+     base_step (App (Lam x e1) e2) e'
+  | TBetaS e1 :
+      base_step (TApp (TLam e1)) e1
+  | UnpackS e1 e2 e' x :
+      is_val e1 →
+      e' = subst' x e1 e2 →
+      base_step (Unpack x (Pack e1) e2) e'
+  | UnOpS op e v v' :
+     to_val e = Some v →
+     un_op_eval op v = Some v' →
+     base_step (UnOp op e) (of_val v')
+  | BinOpS op e1 v1 e2 v2 v' :
+     to_val e1 = Some v1 →
+     to_val e2 = Some v2 →
+     bin_op_eval op v1 v2 = Some v' →
+     base_step (BinOp op e1 e2) (of_val v')
+  | IfTrueS e1 e2 :
+     base_step (If (Lit $ LitBool true) e1 e2) e1
+  | IfFalseS e1 e2 :
+     base_step (If (Lit $ LitBool false) e1 e2) e2
+  | FstS e1 e2 :
+     is_val e1 →
+     is_val e2 →
+     base_step (Fst (Pair e1 e2)) e1
+  | SndS e1 e2 :
+     is_val e1 →
+     is_val e2 →
+     base_step (Snd (Pair e1 e2)) e2
+  | CaseLS e e1 e2 :
+     is_val e →
+     base_step (Case (InjL e) e1 e2) (App e1 e)
+  | CaseRS e e1 e2 :
+     is_val e →
+     base_step (Case (InjR e) e1 e2) (App e2 e)
+.
+
+(** We define evaluation contexts *)
+Inductive ectx :=
+  | HoleCtx
+  | AppLCtx (K: ectx) (v2 : val)
+  | AppRCtx (e1 : expr) (K: ectx)
+  | TAppCtx (K: ectx)
+  | PackCtx (K: ectx)
+  | UnpackCtx (x : binder)(K: ectx)  (e2 : expr)
+  | UnOpCtx (op : un_op) (K: ectx)
+  | BinOpLCtx (op : bin_op) (K: ectx) (v2 : val)
+  | BinOpRCtx (op : bin_op) (e1 : expr) (K: ectx)
+  | IfCtx (K: ectx) (e1 e2 : expr)
+  | PairLCtx (K: ectx) (v2 : val)
+  | PairRCtx (e1 : expr) (K: ectx)
+  | FstCtx (K: ectx)
+  | SndCtx (K: ectx)
+  | InjLCtx (K: ectx)
+  | InjRCtx (K: ectx)
+  | CaseCtx (K: ectx) (e1 : expr) (e2 : expr) .
+
+Fixpoint fill (K : ectx) (e : expr) : expr :=
+  match K with
+  | HoleCtx => e
+  | AppLCtx K v2 => App (fill K e) (of_val v2)
+  | AppRCtx e1 K => App e1 (fill K e)
+  | TAppCtx K => TApp (fill K e)
+  | PackCtx K => Pack (fill K e)
+  | UnpackCtx x K e2 => Unpack x (fill K e) e2
+  | UnOpCtx op K => UnOp op (fill K e)
+  | BinOpLCtx op K v2 => BinOp op (fill K e) (of_val v2)
+  | BinOpRCtx op e1 K => BinOp op e1 (fill K e)
+  | IfCtx K e1 e2 => If (fill K e) e1 e2
+  | PairLCtx K v2 => Pair (fill K e) (of_val v2)
+  | PairRCtx e1 K => Pair e1 (fill K e)
+  | FstCtx K => Fst (fill K e)
+  | SndCtx K => Snd (fill K e)
+  | InjLCtx K => InjL (fill K e)
+  | InjRCtx K => InjR (fill K e)
+  | CaseCtx K e1 e2 => Case (fill K e) e1 e2
+  end.
+
+Fixpoint comp_ectx (K: ectx) (K' : ectx) : ectx :=
+  match K with
+  | HoleCtx => K'
+  | AppLCtx K v2 => AppLCtx (comp_ectx K K') v2
+  | AppRCtx e1 K => AppRCtx e1 (comp_ectx K K')
+  | TAppCtx K => TAppCtx (comp_ectx K K')
+  | PackCtx K => PackCtx (comp_ectx K K')
+  | UnpackCtx x K e2 => UnpackCtx x (comp_ectx K K') e2
+  | UnOpCtx op K => UnOpCtx op (comp_ectx K K')
+  | BinOpLCtx op K v2 => BinOpLCtx op (comp_ectx K K') v2
+  | BinOpRCtx op e1 K => BinOpRCtx op e1 (comp_ectx K K')
+  | IfCtx K e1 e2 => IfCtx (comp_ectx K K') e1 e2
+  | PairLCtx K v2 => PairLCtx (comp_ectx K K') v2
+  | PairRCtx e1 K => PairRCtx e1 (comp_ectx K K')
+  | FstCtx K => FstCtx (comp_ectx K K')
+  | SndCtx K => SndCtx (comp_ectx K K')
+  | InjLCtx K => InjLCtx (comp_ectx K K')
+  | InjRCtx K => InjRCtx (comp_ectx K K')
+  | CaseCtx K e1 e2 => CaseCtx (comp_ectx K K') e1 e2
+  end.
+
+(** Contextual steps *)
+Inductive contextual_step (e1 : expr) (e2 : expr) : Prop :=
+  Ectx_step K e1' e2' :
+    e1 = fill K e1' → e2 = fill K e2' →
+    base_step e1' e2' → contextual_step e1 e2.
+
+Definition reducible (e : expr) :=
+  ∃ e', contextual_step e e'.
+
+
+Definition empty_ectx := HoleCtx.
+
+(** Basic properties about the language *)
+Lemma fill_empty e : fill empty_ectx e = e.
+Proof. done. Qed.
+
+Lemma fill_comp (K1 K2 : ectx) e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e.
+Proof. induction K1; simpl; congruence. Qed.
+
+
+
+Lemma base_contextual_step e1 e2 :
+  base_step e1 e2 → contextual_step e1 e2.
+Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
+
+Lemma fill_contextual_step K e1 e2 :
+  contextual_step e1 e2 → contextual_step (fill K e1) (fill K e2).
+Proof.
+  destruct 1 as [K' e1' e2' -> ->].
+  rewrite !fill_comp. by econstructor.
+Qed.
+
+Fixpoint is_closed (X : list string) (e : expr) : bool :=
+  match e with
+  | Var x => bool_decide (x ∈ X)
+  | Lam x e => is_closed (x :b: X) e
+  | Unpack x e1 e2 => is_closed X e1 && is_closed (x :b: X) e2
+  | Lit _ => true
+  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | TApp e | TLam e | Pack e => is_closed X e
+  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 => is_closed X e1 && is_closed X e2
+  |  If e0 e1 e2 | Case e0 e1 e2 =>
+   is_closed X e0 && is_closed X e1 && is_closed X e2
+  end.
+
+(** [closed] states closedness as a Coq proposition, through the [Is_true] transformer. *)
+Definition closed (X : list string) (e : expr) : Prop := Is_true (is_closed X e).
+#[export] Instance closed_proof_irrel X e : ProofIrrel (closed X e).
+Proof. unfold closed. apply _. Qed.
+#[export] Instance closed_dec X e : Decision (closed X e).
+Proof. unfold closed. apply _. Defined.
+
+(** closed expressions *)
+Lemma is_closed_weaken X Y e : is_closed X e → X ⊆ Y → is_closed Y e.
+Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
+
+Lemma is_closed_weaken_nil X e : is_closed [] e → is_closed X e.
+Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
+
+Lemma is_closed_subst X e x es :
+  is_closed [] es → is_closed (x :: X) e → is_closed X (subst x es e).
+Proof.
+  intros ?.
+  induction e in X |-*; simpl; intros ?; destruct_and?; split_and?; simplify_option_eq;
+    try match goal with
+    | H : ¬(_ ∧ _) |- _ => apply not_and_l in H as [?%dec_stable|?%dec_stable]
+    end; eauto using is_closed_weaken with set_solver.
+Qed.
+Lemma is_closed_do_subst' X e x es :
+  is_closed [] es → is_closed (x :b: X) e → is_closed X (subst' x es e).
+Proof. destruct x; eauto using is_closed_subst. Qed.
+
+(** Substitution lemmas *)
+Lemma subst_is_closed X e x es : is_closed X e → x ∉ X → subst x es e = e.
+Proof.
+  induction e in X |-*; simpl; rewrite ?bool_decide_spec, ?andb_True; intros ??;
+    repeat case_decide; simplify_eq; simpl; f_equal; intuition eauto with set_solver.
+Qed.
+
+Lemma subst_is_closed_nil e x es : is_closed [] e → subst x es e = e.
+Proof. intros. apply subst_is_closed with []; set_solver. Qed.
+Lemma subst'_is_closed_nil e x es : is_closed [] e → subst' x es e = e.
+Proof. intros. destruct x as [ | x]. { done. } by apply subst_is_closed_nil. Qed.
+
+
+(* we derive a few lemmas about contextual steps *)
+Lemma contextual_step_app_l e1 e1' e2:
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (App e1 e2) (App e1' e2).
+Proof.
+  intros [v <-%of_to_val]%is_val_spec Hcontextual.
+  by eapply (fill_contextual_step (AppLCtx HoleCtx v)).
+Qed.
+
+Lemma contextual_step_app_r e1 e2 e2':
+  contextual_step e2 e2' →
+  contextual_step (App e1 e2) (App e1 e2').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (AppRCtx e1 HoleCtx)).
+Qed.
+
+Lemma contextual_step_tapp e e':
+  contextual_step e e' →
+  contextual_step (TApp e) (TApp e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (TAppCtx HoleCtx)).
+Qed.
+
+Lemma contextual_step_pack e e':
+  contextual_step e e' →
+  contextual_step (Pack e) (Pack e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (PackCtx HoleCtx)).
+Qed.
+
+Lemma contextual_step_unpack x e e' e2:
+  contextual_step e e' →
+  contextual_step (Unpack x e e2) (Unpack x e' e2).
+  Proof.
+    intros Hcontextual.
+    by eapply (fill_contextual_step (UnpackCtx x HoleCtx e2)).
+  Qed.
+
+Lemma contextual_step_unop op e e':
+  contextual_step e e' →
+  contextual_step (UnOp op e) (UnOp op e').
+  Proof.
+    intros Hcontextual.
+    by eapply (fill_contextual_step (UnOpCtx op HoleCtx)).
+  Qed.
+
+Lemma contextual_step_binop_l op e1 e1' e2:
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (BinOp op e1 e2) (BinOp op e1' e2).
+Proof.
+  intros [v <-%of_to_val]%is_val_spec Hcontextual.
+  by eapply (fill_contextual_step (BinOpLCtx op HoleCtx v)).
+Qed.
+
+Lemma contextual_step_binop_r op e1 e2 e2':
+  contextual_step e2 e2' →
+  contextual_step (BinOp op e1 e2) (BinOp op e1 e2').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (BinOpRCtx op e1 HoleCtx)).
+Qed.
+
+Lemma contextual_step_if e e' e1 e2:
+  contextual_step e e' →
+  contextual_step (If e e1 e2) (If e' e1 e2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (IfCtx HoleCtx e1 e2)).
+Qed.
+
+Lemma contextual_step_pair_l e1 e1' e2:
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (Pair e1 e2) (Pair e1' e2).
+Proof.
+  intros [v <-%of_to_val]%is_val_spec Hcontextual.
+  by eapply (fill_contextual_step (PairLCtx HoleCtx v)).
+Qed.
+
+Lemma contextual_step_pair_r e1 e2 e2':
+  contextual_step e2 e2' →
+  contextual_step (Pair e1 e2) (Pair e1 e2').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (PairRCtx e1 HoleCtx)).
+Qed.
+
+
+Lemma contextual_step_fst e e':
+  contextual_step e e' →
+  contextual_step (Fst e) (Fst e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (FstCtx HoleCtx)).
+Qed.
+
+Lemma contextual_step_snd e e':
+  contextual_step e e' →
+  contextual_step (Snd e) (Snd e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (SndCtx HoleCtx)).
+Qed.
+
+Lemma contextual_step_injl e e':
+  contextual_step e e' →
+  contextual_step (InjL e) (InjL e').
+  Proof.
+    intros Hcontextual.
+    by eapply (fill_contextual_step (InjLCtx HoleCtx)).
+  Qed.
+
+Lemma contextual_step_injr e e':
+  contextual_step e e' →
+  contextual_step (InjR e) (InjR e').
+  Proof.
+    intros Hcontextual.
+    by eapply (fill_contextual_step (InjRCtx HoleCtx)).
+  Qed.
+
+Lemma contextual_step_case e e' e1 e2:
+  contextual_step e e' →
+  contextual_step (Case e e1 e2) (Case e' e1 e2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (CaseCtx HoleCtx e1 e2)).
+Qed.
+
+#[export]
+Hint Resolve
+  contextual_step_app_l contextual_step_app_r contextual_step_binop_l contextual_step_binop_r
+  contextual_step_case contextual_step_fst contextual_step_if contextual_step_injl contextual_step_injr
+  contextual_step_pack contextual_step_pair_l contextual_step_pair_r contextual_step_snd contextual_step_tapp
+  contextual_step_tapp contextual_step_unop contextual_step_unpack : core.

theories/type_systems/systemf/notation.v

@@ -0,0 +1,90 @@
+From semantics.ts.systemf Require Export lang.
+Set Default Proof Using "Type".
+
+
+(** Coercions to make programs easier to type. *)
+Coercion of_val : val >-> expr.
+Coercion LitInt : Z >-> base_lit.
+Coercion LitBool : bool >-> base_lit.
+Coercion App : expr >-> Funclass.
+Coercion Var : string >-> expr.
+
+(** Define some derived forms. *)
+Notation Let x e1 e2 := (App (Lam x e2) e1) (only parsing).
+Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing).
+Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).
+
+(* No scope for the values, does not conflict and scope is often not inferred
+properly. *)
+Notation "# l" := (LitV l%Z%V%stdpp) (at level 8, format "# l").
+Notation "# l" := (Lit l%Z%E%stdpp) (at level 8, format "# l") : expr_scope.
+
+(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
+    first. *)
+Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope.
+Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope.
+
+Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
+  (Match e0 x1%binder e1 x2%binder e2)
+  (e0, x1, e1, x2, e2 at level 200,
+   format "'[hv' 'match:'  e0  'with'  '/  ' '[' 'InjL'  x1  =>  '/  ' e1 ']'  '/' '[' |  'InjR'  x2  =>  '/  ' e2 ']'  '/' 'end' ']'") : expr_scope.
+Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
+  (Match e0 x2%binder e2 x1%binder e1)
+  (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope.
+
+Notation "()" := LitUnit : val_scope.
+
+Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E) : expr_scope.
+Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E) : expr_scope.
+Notation "e1 * e2" := (BinOp MultOp e1%E e2%E) : expr_scope.
+Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E) : expr_scope.
+Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) : expr_scope.
+Notation "e1 < e2" := (BinOp LtOp e1%E e2%E) : expr_scope.
+
+(*Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.*)
+
+Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
+  (at level 200, e1, e2, e3 at level 200) : expr_scope.
+
+Notation "λ: x , e" := (Lam x%binder e%E)
+  (at level 200, x at level 1, e at level 200,
+   format "'[' 'λ:'  x ,  '/  ' e ']'") : expr_scope.
+Notation "λ: x y .. z , e" := (Lam x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
+  (at level 200, x, y, z at level 1, e at level 200,
+   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : expr_scope.
+
+Notation "λ: x , e" := (LamV x%binder e%E)
+  (at level 200, x at level 1, e at level 200,
+   format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
+Notation "λ: x y .. z , e" := (LamV x%binder (Lam y%binder .. (Lam z%binder e%E) .. ))
+  (at level 200, x, y, z at level 1, e at level 200,
+   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.
+Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
+  (at level 100, e2 at level 200,
+   format "'[' '[hv' '[' e1 ']' ;;  ']' '/' e2 ']'") : expr_scope.
+
+
+Notation "'Λ' , e" := (TLam e%E)
+  (at level 200, e at level 200,
+    format "'[' 'Λ' , '/  ' e ']'") : expr_scope.
+Notation "'Λ' , e" := (TLamV e%E)
+  (at level 200, e at level 200,
+    format "'[' 'Λ' , '/  ' e ']'") : val_scope.
+
+(* the [e] always needs to be paranthesized, due to the level
+   (chosen to make this cooperate with the [App] coercion) *)
+Notation "e '<>'" := (TApp e%E)
+  (at level 10) : expr_scope.
+(*Check ((Λ, #4) <>)%E.*)
+(*Check (((λ: "x", "x") #5) <>)%E.*)
+
+Notation "'pack' e" := (Pack e%E)
+  (at level 200, e at level 200) : expr_scope.
+Notation "'pack' v" := (PackV v%V)
+  (at level 200, v at level 200) : val_scope.
+Notation "'unpack'  e1  'as'  x  'in'  e2" := (Unpack x%binder e1%E e2%E)
+  (at level 200, e1, e2 at level 200, x at level 1) : expr_scope.

theories/type_systems/systemf/parallel_subst.v

@@ -0,0 +1,180 @@
+From stdpp Require Import prelude.
+From iris Require Import prelude.
+From semantics.ts.systemf Require Import lang.
+From semantics.lib Require Import maps.
+
+Fixpoint subst_map (xs : gmap string expr) (e : expr) : expr :=
+  match e with
+  | Lit l => Lit l
+  | Var y => match xs !! y with Some es => es | _ =>  Var y end
+  | App e1 e2 => App (subst_map xs e1) (subst_map xs e2)
+  | Lam x e => Lam x (subst_map (binder_delete x xs) e)
+  | UnOp op e => UnOp op (subst_map xs e)
+  | BinOp op e1 e2 => BinOp op (subst_map xs e1) (subst_map xs e2)
+  | If e0 e1 e2 => If (subst_map xs e0) (subst_map xs e1) (subst_map xs e2)
+  | TApp e => TApp (subst_map xs e)
+  | TLam e => TLam (subst_map xs e)
+  | Pack e => Pack (subst_map xs e)
+  | Unpack x e1 e2 => Unpack x (subst_map xs e1) (subst_map (binder_delete x xs) e2)
+  | Pair e1 e2 => Pair (subst_map xs e1) (subst_map xs e2)
+  | Fst e => Fst (subst_map xs e)
+  | Snd e => Snd (subst_map xs e)
+  | InjL e => InjL (subst_map xs e)
+  | InjR e => InjR (subst_map xs e)
+  | Case e e1 e2 => Case (subst_map xs e) (subst_map xs e1) (subst_map xs e2)
+  end.
+
+Lemma subst_map_empty e :
+  subst_map ∅ e = e.
+Proof.
+  induction e; simpl; f_equal; eauto.
+  all: destruct x; simpl; [done | by rewrite !delete_empty..].
+Qed.
+
+Lemma subst_map_is_closed X e xs :
+  is_closed X e →
+  (∀ x : string, x ∈ dom xs → x ∉ X) →
+  subst_map xs e = e.
+Proof.
+  intros Hclosed Hd.
+  induction e in xs, X, Hd, Hclosed |-*; simpl in *;try done.
+  all: repeat match goal with
+  | H : Is_true (_ && _)  |- _ => apply andb_True in H as [ ? ? ]
+              end.
+  { (* Var *)
+    apply bool_decide_spec in Hclosed.
+    assert (xs !! x = None) as ->; last done.
+    destruct (xs !! x) as [s | ] eqn:Helem; last done.
+    exfalso; eapply Hd; last apply Hclosed.
+    apply elem_of_dom; eauto.
+  }
+  { (* lambdas *)
+    erewrite IHe; [done | done |].
+    intros y. destruct x as [ | x]; first apply Hd.
+    simpl.
+    rewrite dom_delete elem_of_difference not_elem_of_singleton.
+    intros [Hnx%Hd Hneq]. rewrite elem_of_cons. intros [? | ?]; done.
+  }
+  8: { (* Unpack *)
+    erewrite IHe1; [ | done | done].
+    erewrite IHe2; [ done | done | ].
+    intros y. destruct x as [ | x]; first apply Hd.
+    simpl.
+    rewrite dom_delete elem_of_difference not_elem_of_singleton.
+    intros [Hnx%Hd Hneq]. rewrite elem_of_cons. intros [? | ?]; done.
+  }
+  (* all other cases *)
+  all: repeat match goal with
+       | H : ∀ _ _, _ → _ → subst_map _ _ = _ |- _ => erewrite H; clear H
+       end; done.
+Qed.
+
+Lemma subst_map_subst map x (e e' : expr) :
+  is_closed [] e' →
+  subst_map map (subst x e' e) = subst_map (<[x:=e']>map) e.
+Proof.
+  intros He'.
+  revert x map; induction e; intros xx map; simpl;
+  try (f_equal; eauto).
+  - case_decide.
+    + simplify_eq/=. rewrite lookup_insert.
+      rewrite (subst_map_is_closed []); [done | apply He' | ].
+      intros ? ?. apply not_elem_of_nil.
+    + rewrite lookup_insert_ne; done.
+  - destruct x; simpl; first done.
+    + case_decide.
+      * simplify_eq/=. by rewrite delete_insert_delete.
+      * rewrite delete_insert_ne; last by congruence. done.
+  - destruct x; simpl; first done.
+    + case_decide.
+      * simplify_eq/=. by rewrite delete_insert_delete.
+      * rewrite delete_insert_ne; last by congruence. done.
+Qed.
+
+Definition subst_is_closed (X : list string) (map : gmap string expr) :=
+  ∀ x e, map !! x = Some e → closed X e.
+Lemma subst_is_closed_subseteq X map1 map2 :
+  map1 ⊆ map2 → subst_is_closed X map2 → subst_is_closed X map1.
+Proof.
+  intros Hsub Hclosed2 x e Hl. eapply Hclosed2, map_subseteq_spec; done.
+Qed.
+
+Lemma subst_subst_map x es map e :
+  subst_is_closed [] map →
+  subst x es (subst_map (delete x map) e) =
+  subst_map (<[x:=es]>map) e.
+Proof.
+  revert map es x; induction e; intros map v0 xx Hclosed; simpl;
+  try (f_equal; eauto).
+  - destruct (decide (xx=x)) as [->|Hne].
+    + rewrite lookup_delete // lookup_insert //. simpl.
+      rewrite decide_True //.
+    + rewrite lookup_delete_ne // lookup_insert_ne //.
+      destruct (_ !! x) as [rr|] eqn:Helem.
+      * apply Hclosed in Helem.
+        by apply subst_is_closed_nil.
+      * simpl. rewrite decide_False //.
+  - destruct x; simpl; first by auto.
+    case_decide.
+    + simplify_eq. rewrite delete_idemp delete_insert_delete. done.
+    + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. apply IHe.
+      eapply subst_is_closed_subseteq; last done.
+      apply map_delete_subseteq.
+  - destruct x; simpl; first by auto.
+    case_decide.
+    + simplify_eq. rewrite delete_idemp delete_insert_delete. done.
+    + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. apply IHe2.
+      eapply subst_is_closed_subseteq; last done.
+      apply map_delete_subseteq.
+Qed.
+
+Lemma subst'_subst_map b (es : expr) map e :
+  subst_is_closed [] map →
+  subst' b es (subst_map (binder_delete b map) e) =
+  subst_map (binder_insert b es map) e.
+Proof.
+  destruct b; first done.
+  apply subst_subst_map.
+Qed.
+
+Lemma closed_subst_weaken e map X Y :
+  subst_is_closed [] map →
+  (∀ x, x ∈ X → x ∉ dom map → x ∈ Y) →
+  closed X e →
+  closed Y (subst_map map e).
+Proof.
+  induction e in X, Y, map |-*; rewrite /closed; simpl; intros Hmclosed Hsub Hcl; first done.
+  all: repeat match goal with
+  | H : Is_true (_ && _)  |- _ => apply andb_True in H as [ ? ? ]
+              end.
+  { (* vars *)
+    destruct (map !! x) as [es | ] eqn:Heq.
+    + apply is_closed_weaken_nil. by eapply Hmclosed.
+    + apply bool_decide_pack. apply Hsub; first by eapply bool_decide_unpack.
+      by apply not_elem_of_dom.
+  }
+  { (* lambdas *)
+    eapply IHe; last done.
+    + eapply subst_is_closed_subseteq; last done.
+      destruct x; first done. apply map_delete_subseteq.
+    + intros y. destruct x as [ | x]; first by apply Hsub.
+      rewrite !elem_of_cons. intros [-> | Hy] Hn; first by left.
+      destruct (decide (y = x)) as [ -> | Hneq]; first by left.
+      right. eapply Hsub; first done. set_solver.
+  }
+  8: { (* unpack *)
+    apply andb_True; split; first naive_solver.
+    eapply IHe2; last done.
+    + eapply subst_is_closed_subseteq; last done.
+      destruct x; first done. apply map_delete_subseteq.
+    + intros y. destruct x as [ | x]; first by apply Hsub.
+      rewrite !elem_of_cons. intros [-> | Hy] Hn; first by left.
+      destruct (decide (y = x)) as [ -> | Hneq]; first by left.
+      right. eapply Hsub; first done. set_solver.
+  }
+  (* all other cases *)
+  all: repeat match goal with
+         | |- Is_true (_ && _) => apply andb_True; split
+              end.
+  all: naive_solver.
+Qed.

theories/type_systems/systemf/tactics.v

@@ -0,0 +1,113 @@
+From stdpp Require Import base relations.
+From iris Require Import prelude.
+From semantics.lib Require Import facts.
+From semantics.ts.systemf Require Export lang notation parallel_subst types bigstep.
+
+Lemma list_subseteq_cons {X} (A B : list X) x : A ⊆ B → x :: A ⊆ x :: B.
+Proof. intros Hincl. intros y. rewrite !elem_of_cons. naive_solver. Qed.
+Lemma list_subseteq_cons_binder A B x : A ⊆ B → x :b: A ⊆ x :b: B.
+Proof. destruct x; first done. apply list_subseteq_cons. Qed.
+
+Ltac simplify_list_elem :=
+  simpl;
+  repeat match goal with
+         | |- ?x ∈ ?y :: ?l => apply elem_of_cons; first [left; reflexivity | right]
+         | |- _ ∉ [] => apply not_elem_of_nil
+         | |- _ ∉ _ :: _ => apply not_elem_of_cons; split
+  end; try fast_done.
+Ltac simplify_list_subseteq :=
+  simpl;
+  repeat match goal with
+         | |- ?x :: _ ⊆ ?x :: _ => apply list_subseteq_cons_l
+         | |- ?x :: _ ⊆ _ => apply list_subseteq_cons_elem; first solve [simplify_list_elem]
+         | |- elements _ ⊆ elements _ => apply elements_subseteq; set_solver
+         | |- [] ⊆ _ => apply list_subseteq_nil
+         | |- ?x :b: _ ⊆ ?x :b: _ => apply list_subseteq_cons_binder
+         end;
+  try fast_done.
+
+(* Try to solve [is_closed] goals using a number of heuristics (that shouldn't make the goal unprovable) *)
+Ltac simplify_closed :=
+  simpl; intros;
+  repeat match goal with
+  | |- closed _ _ => unfold closed; simpl
+  | |- Is_true (is_closed [] _) => first [assumption | done]
+  | |- Is_true (is_closed _ (lang.subst _ _ _)) => rewrite subst_is_closed_nil; last solve[simplify_closed]
+  | |- Is_true (is_closed ?X ?v) => assert_fails (is_evar X); eapply is_closed_weaken
+  | |- Is_true (is_closed _ _) => eassumption
+  | |- Is_true (_ && true) => rewrite andb_true_r
+  | |- Is_true (true && _) => rewrite andb_true_l
+  | |- Is_true (?a && ?a) => rewrite andb_diag
+  | |- Is_true (_ && _)  => simpl; rewrite !andb_True; split_and!
+  | |- _ ⊆ ?A => match type of A with | list _ => simplify_list_subseteq end
+  | |- _ ∈ ?A => match type of A with | list _ => simplify_list_elem end
+  | |- _ ∉ ?A => match type of A with | list _ => simplify_list_elem end
+  | |- _ ≠ _ => congruence
+  | H : closed _ _ |- _ => unfold closed in H; simpl in H
+  | H: Is_true (_ && _) |- _ => simpl in H; apply andb_True in H
+  | H : _ ∧ _ |- _ => destruct H
+  | |- Is_true (bool_decide (_ ∈ _)) => apply bool_decide_pack; set_solver
+  end; try fast_done.
+
+
+Ltac bs_step_det :=
+  repeat match goal with
+  | |- big_step ?e _ =>
+      simpl;
+      match e with
+      (* case analysis, don't backtrack but pose the goal to the user *)
+      | Case _ _ _ => idtac
+      | If _ _ _ => idtac
+      (* use the value lemma *)
+      | of_val _ => apply big_step_of_val; done
+      (* try to solve substitutions by using disjointness assumptions *)
+      | context[decide (?p = ?p)] => rewrite decide_True; [ | done]
+      | context[decide (_ = _)] => rewrite decide_True; [ | congruence]
+      | context[decide (_ = _)] => rewrite decide_False; [ | congruence]
+      | context[decide (_ ≠ _)] => rewrite decide_True; [ | congruence]
+      | context[decide (_ ≠ _)] => rewrite decide_False; [ | congruence]
+      (* if we have a substitution that didn't simplify, try to show that it's closed *)
+      (* we don't make any attempt to solve it if it isn't closed under [] *)
+      | context[lang.subst _ _ ?e] => is_var e; rewrite subst_is_closed_nil; last solve[simplify_closed]
+      | context[lang.subst _ _ (of_val ?v)] => is_var v; rewrite subst_is_closed_nil; last solve[simplify_closed]
+      (* try to use a [big_step] assumption, or else apply a constructor *)
+      | _ => first [eassumption | econstructor]
+      end
+  | |- bin_op_eval _ _ _ = _ =>
+      simpl; reflexivity
+  end; simplify_closed.
+Ltac bs_steps_det := repeat bs_step_det.
+
+Ltac map_solver :=
+  repeat match goal with
+         | |-  (⤉ _) !! _ = Some _ =>
+             rewrite fmap_insert
+         | |- <[ ?p := _ ]> _ !! ?p = Some _ =>
+             apply lookup_insert
+         | |- <[ _ := _ ]> _ !! _ = Some _ =>
+             rewrite lookup_insert_ne; [ | congruence]
+         end.
+Ltac solve_typing :=
+  repeat match goal with
+  | |- TY _ ; _ ⊢ ?e : ?A => first [eassumption | econstructor]
+  (* heuristic to solve tapp goals where we need to pick the right type for the substitution *)
+  | |- TY _ ; _ ⊢ ?e <> : ?A => eapply typed_tapp'; [solve_typing | | asimpl; reflexivity]
+  | |- bin_op_typed _ _ _ _ => econstructor
+  | |- type_wf _ ?e => assert_fails (is_evar e); eassumption
+  | |- type_wf _ ?e => assert_fails (is_evar e); econstructor
+  | |- type_wf _ (subst _ ?A) => eapply type_wf_subst; [ | intros; simpl]
+  | |- type_wf _ ?e => assert_fails (is_evar e); eapply type_wf_mono; [eassumption | lia]
+  (* conditions spawned by the tyvar case of [type_wf] *)
+  | |- _ < _ => lia
+  (* conditions spawned by the variable case *)
+  | |- _ !! _ = Some _ => map_solver
+  end.
+
+Tactic Notation "unify_type" uconstr(A) :=
+  match goal with
+  | |- TY ?n; ?Γ ⊢ ?e : ?B => unify A B
+  end.
+Tactic Notation "replace_type" uconstr(A) :=
+  match goal with
+  | |- TY ?n; ?Γ ⊢ ?e : ?B => replace B%ty with A%ty; cycle -1; first try by asimpl
+  end.

theories/type_systems/systemf/types.v

@@ -0,0 +1,866 @@
+From stdpp Require Import base relations.
+From iris Require Import prelude.
+From semantics.lib Require Import maps.
+From semantics.ts.systemf Require Import lang notation.
+From Autosubst Require Export Autosubst.
+
+(** ** Syntactic typing *)
+(** We use De Bruijn indices with the help of the Autosubst library. *)
+Inductive type : Type :=
+  (** [var] is the type of variables of Autosubst -- it unfolds to [nat] *)
+  | TVar : var → type
+  | Int
+  | Bool
+  | Unit
+  (** The [{bind 1 of type}] tells Autosubst to put a De Bruijn binder here *)
+  | TForall : {bind 1 of type} → type
+  | TExists : {bind 1 of type} → type
+  | Fun (A B : type)
+  | Prod (A B : type)
+  | Sum (A B : type).
+
+(** Autosubst instances.
+  This lets Autosubst do its magic and derive all the substitution functions, etc.
+ *)
+#[export] Instance Ids_type : Ids type. derive. Defined.
+#[export] Instance Rename_type : Rename type. derive. Defined.
+#[export] Instance Subst_type : Subst type. derive. Defined.
+#[export] Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
+
+Definition typing_context := gmap string type.
+Implicit Types
+  (Γ : typing_context)
+  (v : val)
+  (e : expr).
+
+Declare Scope FType_scope.
+Delimit Scope FType_scope with ty.
+Bind Scope FType_scope with type.
+Notation "# x" := (TVar x) : FType_scope.
+Infix "→" := Fun : FType_scope.
+Notation "(→)" := Fun (only parsing) : FType_scope.
+Notation "∀: τ" :=
+  (TForall τ%ty)
+  (at level 100, τ at level 200) : FType_scope.
+Notation "∃: τ" :=
+  (TExists τ%ty)
+  (at level 100, τ at level 200) : FType_scope.
+Infix "×" := Prod (at level 70) : FType_scope.
+Notation "(×)" := Prod (only parsing) : FType_scope.
+Infix "+" := Sum : FType_scope.
+Notation "(+)" := Sum (only parsing) : FType_scope.
+
+
+(** Shift all the indices in the context by one,
+   used when inserting a new type interpretation in Δ. *)
+(* [<$>] is notation for the [fmap] operation that maps the substitution over the whole map. *)
+(* [ren] is Autosubst's renaming operation -- it renames all type variables according to the given function,
+  in this case [(+1)] to shift the variables up by 1. *)
+Notation "⤉ Γ" := (Autosubst_Classes.subst (ren (+1)) <$> Γ) (at level 10, format "⤉ Γ").
+
+Reserved Notation "'TY' n ; Γ ⊢ e : A" (at level 74, e, A at next level).
+
+(** [type_wf n A] states that a type [A] has only free variables up to < [n].
+ (in other words, all variables occurring free are strictly bounded by [n]). *)
+Inductive type_wf : nat → type → Prop :=
+  | type_wf_TVar m n:
+      m < n →
+      type_wf n (TVar m)
+  | type_wf_Int n: type_wf n Int
+  | type_wf_Bool n : type_wf n Bool
+  | type_wf_Unit n : type_wf n Unit
+  | type_wf_TForall n A :
+      type_wf (S n) A →
+      type_wf n (TForall A)
+  | type_wf_TExists n A :
+      type_wf (S n) A →
+      type_wf n (TExists A)
+  | type_wf_Fun n A B:
+      type_wf n A →
+      type_wf n B →
+      type_wf n (Fun A B)
+  | type_wf_Prod n A B :
+      type_wf n A →
+      type_wf n B →
+      type_wf n (Prod A B)
+  | type_wf_Sum n A B :
+      type_wf n A →
+      type_wf n B →
+      type_wf n (Sum A B)
+.
+#[export] Hint Constructors type_wf : core.
+
+Inductive bin_op_typed : bin_op → type → type → type → Prop :=
+  | plus_op_typed : bin_op_typed PlusOp Int Int Int
+  | minus_op_typed : bin_op_typed MinusOp Int Int Int
+  | mul_op_typed : bin_op_typed MultOp Int Int Int
+  | lt_op_typed : bin_op_typed LtOp Int Int Bool
+  | le_op_typed : bin_op_typed LeOp Int Int Bool
+  | eq_op_typed : bin_op_typed EqOp Int Int Bool.
+#[export] Hint Constructors bin_op_typed : core.
+
+Inductive un_op_typed : un_op → type → type → Prop :=
+  | neg_op_typed : un_op_typed NegOp Bool Bool
+  | minus_un_op_typed : un_op_typed MinusUnOp Int Int.
+
+Inductive syn_typed : nat → typing_context → expr → type → Prop :=
+  | typed_var n Γ x A :
+      Γ !! x = Some A →
+      TY n; Γ ⊢ (Var x) : A
+  | typed_lam n Γ x e A B :
+      TY n ; (<[ x := A]> Γ) ⊢ e : B →
+      type_wf n A →
+      TY n; Γ ⊢ (Lam (BNamed x) e) : (A → B)
+  | typed_lam_anon n Γ e A B :
+      TY n ; Γ ⊢ e : B →
+      type_wf n A →
+      TY n; Γ ⊢ (Lam BAnon e) : (A → B)
+  | typed_tlam n Γ e A :
+      (* we need to shift the context up as we descend under a binder *)
+      TY S n; (⤉ Γ) ⊢ e : A →
+      TY n; Γ ⊢ (Λ, e) : (∀: A)
+  | typed_tapp n Γ A B e :
+      TY n; Γ ⊢ e : (∀: A) →
+      type_wf n B →
+      (* A.[B/] is the notation for Autosubst's substitution operation that
+        replaces variable 0 by [B] *)
+      TY n; Γ ⊢ (e <>) : (A.[B/])
+  | typed_pack n Γ A B e :
+      type_wf n B →
+      type_wf (S n) A →
+      TY n; Γ ⊢ e : (A.[B/]) →
+      TY n; Γ ⊢ (pack e) : (∃: A)
+  | typed_unpack n Γ A B e e' x :
+      type_wf n B → (* we should not leak the existential! *)
+      TY n; Γ ⊢ e : (∃: A) →
+      (* As we descend under a type variable binder for the typing of [e'],
+          we need to shift the indices in [Γ] and [B] up by one.
+        On the other hand, [A] is already defined under this binder, so we need not shift it.
+      *)
+      TY (S n); (<[x := A]>(⤉Γ)) ⊢ e' : (B.[ren (+1)]) →
+      TY n; Γ ⊢ (unpack e as BNamed x in e') : B
+  | typed_int n Γ z : TY n; Γ ⊢ (Lit $ LitInt z) : Int
+  | typed_bool n Γ b : TY n; Γ ⊢ (Lit $ LitBool b) : Bool
+  | typed_unit n Γ : TY n; Γ ⊢ (Lit $ LitUnit) : Unit
+  | typed_if n Γ e0 e1 e2 A :
+      TY n; Γ ⊢ e0 : Bool →
+      TY n; Γ ⊢ e1 : A →
+      TY n; Γ ⊢ e2 : A →
+      TY n; Γ ⊢ If e0 e1 e2 : A
+  | typed_app n Γ e1 e2 A B :
+      TY n; Γ ⊢ e1 : (A → B) →
+      TY n; Γ ⊢ e2 : A →
+      TY n; Γ ⊢ (e1 e2)%E : B
+  | typed_binop n Γ e1 e2 op A B C :
+      bin_op_typed op A B C →
+      TY n; Γ ⊢ e1 : A →
+      TY n; Γ ⊢ e2 : B →
+      TY n; Γ ⊢ BinOp op e1 e2 : C
+  | typed_unop n Γ e op A B :
+      un_op_typed op A B →
+      TY n; Γ ⊢ e : A →
+      TY n; Γ ⊢ UnOp op e : B
+  | typed_pair n Γ e1 e2 A B :
+      TY n; Γ ⊢ e1 : A →
+      TY n; Γ ⊢ e2 : B →
+      TY n; Γ ⊢ (e1, e2) : A × B
+  | typed_fst n Γ e A B :
+      TY n; Γ ⊢ e : A × B →
+      TY n; Γ ⊢ Fst e : A
+  | typed_snd n Γ e A B :
+      TY n; Γ ⊢ e : A × B →
+      TY n; Γ ⊢ Snd e : B
+  | typed_injl n Γ e A B :
+      type_wf n B →
+      TY n; Γ ⊢ e : A →
+      TY n; Γ ⊢ InjL e : A + B
+  | typed_injr n Γ e A B :
+      type_wf n A →
+      TY n; Γ ⊢ e : B →
+      TY n; Γ ⊢ InjR e : A + B
+  | typed_case n Γ e e1 e2 A B C :
+      TY n; Γ ⊢ e : B + C →
+      TY n; Γ ⊢ e1 : (B → A) →
+      TY n; Γ ⊢ e2 : (C → A) →
+      TY n; Γ ⊢ Case e e1 e2 : A
+where "'TY' n ; Γ ⊢ e : A" := (syn_typed n Γ e%E A%ty).
+#[export] Hint Constructors syn_typed : core.
+
+(** Examples *)
+Goal TY 0; ∅ ⊢ (λ: "x", #1 + "x")%E : (Int → Int).
+Proof. eauto. Qed.
+(** [∀: #0 → #0] corresponds to [∀ α. α → α] with named binders. *)
+Goal TY 0; ∅ ⊢ (Λ, λ: "x", "x")%E : (∀: #0 → #0).
+Proof. repeat econstructor. Qed.
+Goal TY 0; ∅ ⊢ (pack ((λ: "x", "x"), #42)) : ∃: (#0 → #0) × #0.
+Proof.
+  apply (typed_pack _ _ _ Int).
+  - eauto.
+  - repeat econstructor.
+  - (* [asimpl] is Autosubst's tactic for simplifying goals involving type substitutions. *)
+    asimpl. eauto.
+Qed.
+Goal TY 0; ∅ ⊢ (unpack (pack ((λ: "x", "x"), #42)) as "y" in (λ: "x", #1337) ((Fst "y") (Snd "y"))) : Int.
+Proof.
+  (* if we want to typecheck stuff with existentials, we need a bit more explicit proofs.
+    Letting eauto try to instantiate the evars becomes too expensive. *)
+  apply (typed_unpack _ _ ((#0 → #0) × #0)%ty).
+  - done.
+  - apply (typed_pack _ _ _ Int); asimpl; eauto.
+    repeat econstructor.
+  - eapply (typed_app _ _ _ _ (#0)%ty); eauto 10.
+Qed.
+
+(** fails: we are not allowed to leak the existential *)
+Goal TY 0; ∅ ⊢ (unpack (pack ((λ: "x", "x"), #42)) as "y" in (Fst "y") (Snd "y")) : #0.
+Proof.
+  apply (typed_unpack _ _ ((#0 → #0) × #0)%ty).
+Abort.
+
+(* derived typing rule for match *)
+Lemma typed_match n Γ e e1 e2 x1 x2 A B C :
+  type_wf n B →
+  type_wf n C →
+  TY n; Γ ⊢ e : B + C →
+  TY n; <[x1 := B]> Γ ⊢ e1 : A →
+  TY n; <[x2 := C]> Γ ⊢ e2 : A →
+  TY n; Γ ⊢ match: e with InjL (BNamed x1) => e1 | InjR (BNamed x2) => e2 end : A.
+Proof. eauto. Qed.
+
+Lemma syn_typed_closed n Γ e A X :
+  TY n ; Γ ⊢ e : A →
+  (∀ x, x ∈ dom Γ → x ∈ X) →
+  is_closed X e.
+Proof.
+  induction 1 as [ | ??????? IH | | n Γ e A H IH | | | n Γ A B e e' x Hwf H1 IH1 H2 IH2 | | | | | | | | | | | | | ] in X |-*; simpl; intros Hx; try done.
+
+  { (* var *) apply bool_decide_pack, Hx. apply elem_of_dom; eauto. }
+  { (* lam *) apply IH.
+    intros y. rewrite elem_of_dom lookup_insert_is_Some.
+    intros [<- | [? Hy]]; first by apply elem_of_cons; eauto.
+    apply elem_of_cons. right. eapply Hx. by apply elem_of_dom.
+  }
+  { (* anon lam *) naive_solver. }
+  { (* tlam *)
+    eapply IH. intros x Hel. apply Hx.
+    by rewrite dom_fmap in Hel.
+  }
+  3: { (* unpack *)
+    apply andb_True; split.
+    - apply IH1. apply Hx.
+    - apply IH2. intros y. rewrite elem_of_dom lookup_insert_is_Some.
+    intros [<- | [? Hy]]; first by apply elem_of_cons; eauto.
+    apply elem_of_cons. right. eapply Hx.
+    apply elem_of_dom. revert Hy. rewrite lookup_fmap fmap_is_Some. done.
+  }
+  (* everything else *)
+  all: repeat match goal with
+              | |- Is_true (_ && _)  => apply andb_True; split
+              end.
+  all: try naive_solver.
+Qed.
+
+(** *** Lemmas about [type_wf] *)
+Lemma type_wf_mono n m A:
+  type_wf n A → n ≤ m → type_wf m A.
+Proof.
+  induction 1 in m |-*; eauto with lia.
+Qed.
+
+Lemma type_wf_rename n A δ:
+  type_wf n A →
+  (∀ i j, i < j → δ i < δ j) →
+  type_wf (δ n) (rename δ A).
+Proof.
+  induction 1 in δ |-*; intros Hmon; simpl; eauto.
+  all: econstructor; eapply type_wf_mono; first eapply IHtype_wf; last done.
+  all: intros i j Hlt; destruct i, j; simpl; try lia.
+  all: rewrite -Nat.succ_lt_mono; eapply Hmon; lia.
+Qed.
+
+(** [A.[σ]], i.e. [A] with the substitution [σ] applied to it, is well-formed under [m] if
+   [A] is well-formed under [n] and all the things we substitute up to [n] are well-formed under [m].
+ *)
+Lemma type_wf_subst n m A σ:
+  type_wf n A →
+  (∀ x, x < n → type_wf m (σ x)) →
+  type_wf m A.[σ].
+Proof.
+  induction 1 in m, σ |-*; intros Hsub; simpl; eauto.
+  + econstructor; eapply IHtype_wf.
+    intros [|x]; rewrite /up //=.
+    - econstructor. lia.
+    - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
+      intros i j Hlt'; simpl; lia.
+  + econstructor; eapply IHtype_wf.
+    intros [|x]; rewrite /up //=.
+    - econstructor. lia.
+    - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto.
+      intros i j Hlt'; simpl; lia.
+Qed.
+
+Lemma type_wf_single_subst n A B: type_wf n B → type_wf (S n) A → type_wf n A.[B/].
+Proof.
+  intros HB HA. eapply type_wf_subst; first done.
+  intros [|x]; simpl; eauto.
+  intros ?; econstructor. lia.
+Qed.
+
+(** We lift [type_wf] to well-formedness of contexts *)
+Definition ctx_wf n Γ := (∀ x A, Γ !! x = Some A → type_wf n A).
+
+Lemma ctx_wf_empty n : ctx_wf n ∅.
+Proof. rewrite /ctx_wf. set_solver. Qed.
+
+Lemma ctx_wf_insert n x Γ A: ctx_wf n Γ → type_wf n A → ctx_wf n (<[x := A]> Γ).
+Proof. intros H1 H2 y B. rewrite lookup_insert_Some. naive_solver. Qed.
+
+Lemma ctx_wf_up n Γ:
+  ctx_wf n Γ → ctx_wf (S n) (⤉Γ).
+Proof.
+  intros Hwf x A; rewrite lookup_fmap.
+  intros (B & Hlook & ->) % fmap_Some.
+  asimpl. eapply type_wf_subst; first eauto.
+  intros y Hlt. simpl. econstructor. lia.
+Qed.
+
+#[global]
+Hint Resolve ctx_wf_empty ctx_wf_insert ctx_wf_up : core.
+
+(** Well-typed terms at [A] under a well-formed context have well-formed types [A].*)
+Lemma syn_typed_wf n Γ e A:
+  ctx_wf n Γ →
+  TY n; Γ ⊢ e : A →
+  type_wf n A.
+Proof.
+  intros Hwf; induction 1 as [ | n Γ x e A B Hty IH Hwfty | | n Γ e A Hty IH | n Γ A B e Hty IH Hwfty | n Γ A B e Hwfty Hty IH| | |  | | | n Γ e1 e2 A B HtyA IHA HtyB IHB | n Γ e1 e2 op A B C Hop HtyA IHA HtyB IHB | n Γ e op A B Hop H IH | n Γ e1 e2 A B HtyA IHA HtyB IHB | n Γ e A B Hty IH | n Γ e A B Hty IH | n Γ e A B Hwfty Hty IH | n Γ e A B Hwfty Hty IH| n Γ e e1 e2 A B C Htye IHe Htye1 IHe1 Htye2 IHe2 ]; eauto.
+  - eapply type_wf_single_subst; first done.
+    specialize (IH Hwf) as Hwf'.
+    by inversion Hwf'.
+  - specialize (IHA Hwf) as Hwf'.
+    by inversion Hwf'; subst.
+  - inversion Hop; subst; eauto.
+  - inversion Hop; subst; eauto.
+  - specialize (IH Hwf) as Hwf'. by inversion Hwf'; subst.
+  - specialize (IH Hwf) as Hwf'. by inversion Hwf'; subst.
+  - specialize (IHe1 Hwf) as Hwf''. by inversion Hwf''; subst.
+Qed.
+
+Lemma renaming_inclusion Γ Δ : Γ ⊆ Δ → ⤉Γ ⊆ ⤉Δ.
+Proof.
+  eapply map_fmap_mono.
+Qed.
+
+Lemma typed_weakening n m Γ Δ e A:
+  TY n; Γ ⊢ e : A →
+  Γ ⊆ Δ →
+  n ≤ m →
+  TY m; Δ ⊢ e : A.
+Proof.
+  induction 1 as [| n Γ x e A B Htyp IH | | n Γ e A Htyp IH | | |n Γ A B e e' x Hwf H1 IH1 H2 IH2 | | | | | | | | |  | | | | ] in Δ, m |-*; intros Hsub Hle; eauto using type_wf_mono.
+  - (* var *) econstructor. by eapply lookup_weaken.
+  - (* lam *) econstructor; last by eapply type_wf_mono. eapply IH; eauto. by eapply insert_mono.
+  - (* tlam *) econstructor. eapply IH; last by lia. by eapply renaming_inclusion.
+  - (* pack *)
+    econstructor; last naive_solver. all: (eapply type_wf_mono; [ done | lia]).
+  - (* unpack *) econstructor.
+    + eapply type_wf_mono; done.
+    + eapply IH1; done.
+    + eapply IH2; last lia. apply insert_mono. by apply renaming_inclusion.
+Qed.
+
+Lemma type_wf_subst_dom σ τ n A:
+  type_wf n A →
+  (∀ m, m < n → σ m = τ m) →
+  A.[σ] = A.[τ].
+Proof.
+  induction 1 in σ, τ |-*; simpl; eauto.
+  - (* tforall *)
+    intros Heq; asimpl. f_equal.
+    eapply IHtype_wf; intros [|m]; rewrite /up; simpl; first done.
+    intros Hlt. f_equal. eapply Heq. lia.
+  - (* texists *)
+    intros Heq; asimpl. f_equal.
+    eapply IHtype_wf. intros [ | m]; rewrite /up; simpl; first done.
+    intros Hlt. f_equal. apply Heq. lia.
+  - (* fun *) intros ?. f_equal; eauto.
+  - (* prod *) intros ?. f_equal; eauto.
+  - (* sum *) intros ?. f_equal; eauto.
+Qed.
+
+Lemma type_wf_closed A σ:
+  type_wf 0 A →
+  A.[σ] = A.
+Proof.
+  intros Hwf; erewrite (type_wf_subst_dom _ (ids) 0).
+  - by asimpl.
+  - done.
+  - intros ??; lia.
+Qed.
+
+(** Typing inversion lemmas *)
+Lemma var_inversion Γ n (x: string) A: TY n; Γ ⊢ x : A → Γ !! x = Some A.
+Proof. inversion 1; subst; auto. Qed.
+
+Lemma lam_inversion n Γ (x: string) e C:
+  TY n; Γ ⊢ (λ: x, e) : C →
+  ∃ A B, C = (A → B)%ty ∧ type_wf n A ∧ TY n; <[x:=A]> Γ ⊢ e : B.
+Proof. inversion 1; subst; eauto 10. Qed.
+
+Lemma lam_anon_inversion n Γ e C:
+  TY n; Γ ⊢ (λ: <>, e) : C →
+  ∃ A B, C = (A → B)%ty ∧ type_wf n A ∧ TY n; Γ ⊢ e : B.
+Proof. inversion 1; subst; eauto 10. Qed.
+
+Lemma app_inversion n Γ e1 e2 B:
+  TY n; Γ ⊢ e1 e2 : B →
+  ∃ A, TY n; Γ ⊢ e1 : (A → B) ∧ TY n; Γ ⊢ e2 : A.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma if_inversion n Γ e0 e1 e2 B:
+  TY n; Γ ⊢ If e0 e1 e2 : B →
+  TY n; Γ ⊢ e0 : Bool ∧ TY n; Γ ⊢ e1 : B ∧ TY n; Γ ⊢ e2 : B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma binop_inversion n Γ op e1 e2 B:
+  TY n; Γ ⊢ BinOp op e1 e2 : B →
+  ∃ A1 A2, bin_op_typed op A1 A2 B ∧ TY n; Γ ⊢ e1 : A1 ∧ TY n; Γ ⊢ e2 : A2.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma unop_inversion n Γ op e B:
+  TY n; Γ ⊢ UnOp op e : B →
+  ∃ A, un_op_typed op A B ∧ TY n; Γ ⊢ e : A.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma type_app_inversion n Γ e B:
+  TY n; Γ ⊢ e <> : B →
+  ∃ A C, B = A.[C/] ∧ type_wf n C ∧ TY n; Γ ⊢ e : (∀: A).
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma type_lam_inversion n Γ e B:
+  TY n; Γ ⊢ (Λ,e) : B →
+  ∃ A, B = (∀: A)%ty ∧ TY (S n); ⤉Γ ⊢ e : A.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma type_pack_inversion n Γ e B :
+  TY n; Γ ⊢ (pack e) : B →
+  ∃ A C, B = (∃: A)%ty ∧ TY n; Γ ⊢ e : (A.[C/])%ty ∧ type_wf n C ∧ type_wf (S n) A.
+Proof. inversion 1; subst; eauto 10. Qed.
+
+Lemma type_unpack_inversion n Γ e e' x B :
+  TY n; Γ ⊢ (unpack e as x in e') : B →
+  ∃ A x', x = BNamed x' ∧ type_wf n B ∧ TY n; Γ ⊢ e : (∃: A) ∧ TY S n; <[x' := A]> (⤉Γ) ⊢ e' : (B.[ren (+1)]).
+Proof. inversion 1; subst; eauto 10. Qed.
+
+Lemma pair_inversion n Γ e1 e2 C :
+  TY n; Γ ⊢ (e1, e2) : C →
+  ∃ A B, C = (A × B)%ty ∧ TY n; Γ ⊢ e1 : A ∧ TY n; Γ ⊢ e2 : B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma fst_inversion n Γ e A :
+  TY n; Γ ⊢ Fst e : A →
+  ∃ B, TY n; Γ ⊢ e : A × B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma snd_inversion n Γ e B :
+  TY n; Γ ⊢ Snd e : B →
+  ∃ A, TY n; Γ ⊢ e : A × B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma injl_inversion n Γ e C :
+  TY n; Γ ⊢ InjL e : C →
+  ∃ A B, C = (A + B)%ty ∧ TY n; Γ ⊢ e : A ∧ type_wf n B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma injr_inversion n Γ e C :
+  TY n; Γ ⊢ InjR e : C →
+  ∃ A B, C = (A + B)%ty ∧ TY n; Γ ⊢ e : B ∧ type_wf n A.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma case_inversion n Γ e e1 e2 A :
+  TY n; Γ ⊢ Case e e1 e2 : A →
+  ∃ B C, TY n; Γ ⊢ e : B + C ∧ TY n; Γ ⊢ e1 : (B → A) ∧ TY n; Γ ⊢ e2 : (C → A).
+Proof. inversion 1; subst; eauto. Qed.
+
+
+Lemma typed_substitutivity n e e' Γ (x: string) A B :
+  TY 0; ∅ ⊢ e' : A →
+  TY n; (<[x := A]> Γ) ⊢ e : B →
+  TY n; Γ ⊢ lang.subst x e' e : B.
+Proof.
+  intros He'. revert n B Γ; induction e as [| y | y | | | | | | | | | | | | | | ]; intros n B Γ; simpl.
+  - inversion 1; subst; auto.
+  - intros Hp % var_inversion.
+    destruct (decide (x = y)).
+    + subst. rewrite lookup_insert in Hp. injection Hp as ->.
+      eapply typed_weakening; [done| |lia]. apply map_empty_subseteq.
+    + rewrite lookup_insert_ne in Hp; last done. auto.
+  - destruct y as [ | y].
+    { intros (A' & C & -> & Hwf & Hty) % lam_anon_inversion.
+      econstructor; last done. destruct decide as [Heq|].
+      + congruence.
+      + eauto.
+    }
+    intros (A' & C & -> & Hwf & Hty) % lam_inversion.
+    econstructor; last done. destruct decide as [Heq|].
+    + injection Heq as [= ->]. by rewrite insert_insert in Hty.
+    + rewrite insert_commute in Hty; last naive_solver. eauto.
+  - intros (C & Hty1 & Hty2) % app_inversion. eauto.
+  - intros (? & Hop & H1) % unop_inversion.
+    destruct op; inversion Hop; subst; eauto.
+  - intros (? & ? & Hop & H1 & H2) % binop_inversion.
+    destruct op; inversion Hop; subst; eauto.
+  - intros (H1 & H2 & H3)%if_inversion. naive_solver.
+  - intros (C & D & -> & Hwf & Hty) % type_app_inversion. eauto.
+  - intros (C & -> & Hty)%type_lam_inversion. econstructor.
+    eapply IHe. revert Hty. rewrite fmap_insert.
+    eapply syn_typed_wf in He'; last by naive_solver.
+    rewrite type_wf_closed; eauto.
+  - intros (C & D & -> & Hty & Hwf1 & Hwf2)%type_pack_inversion.
+    econstructor; [done..|]. apply IHe. done.
+  - intros (C & x' & -> & Hwf & Hty1 & Hty2)%type_unpack_inversion.
+    econstructor; first done.
+    + eapply IHe1. done.
+    + destruct decide as [Heq | ].
+      * injection Heq as [= ->]. by rewrite fmap_insert insert_insert in Hty2.
+      * rewrite fmap_insert in Hty2. rewrite insert_commute in Hty2; last naive_solver.
+        eapply IHe2. rewrite type_wf_closed in Hty2; first done.
+        eapply syn_typed_wf; last apply He'. done.
+  - intros (? & ? & -> & ? & ?) % pair_inversion. eauto.
+  - intros (? & ?)%fst_inversion. eauto.
+  - intros (? & ?)%snd_inversion. eauto.
+  - intros (? & ? & -> & ? & ?)%injl_inversion. eauto.
+  - intros (? & ? & -> & ? & ?)%injr_inversion. eauto.
+  - intros (? & ? & ? & ? & ?)%case_inversion. eauto.
+Qed.
+
+(** Canonical values *)
+Lemma canonical_values_arr n Γ e A B:
+  TY n; Γ ⊢ e : (A → B) →
+  is_val e →
+  ∃ x e', e = (λ: x, e')%E.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_forall n Γ e A:
+  TY n; Γ ⊢ e : (∀: A)%ty →
+  is_val e →
+  ∃ e', e = (Λ, e')%E.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_exists n Γ e A :
+  TY n; Γ ⊢ e : (∃: A) →
+  is_val e →
+  ∃ e', e = (pack e')%E.
+Proof. inversion 1; simpl; naive_solver. Qed.
+
+Lemma canonical_values_int n Γ e:
+  TY n; Γ ⊢ e : Int →
+  is_val e →
+  ∃ n: Z, e = (#n)%E.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_bool n Γ e:
+  TY n; Γ ⊢ e : Bool →
+  is_val e →
+  ∃ b: bool, e = (#b)%E.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_unit n Γ e:
+  TY n; Γ ⊢ e : Unit →
+  is_val e →
+  e = (#LitUnit)%E.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_prod n Γ e A B :
+  TY n; Γ ⊢ e : A × B →
+  is_val e →
+  ∃ e1 e2, e = (e1, e2)%E ∧ is_val e1 ∧ is_val e2.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_sum n Γ e A B :
+  TY n; Γ ⊢ e : A + B →
+  is_val e →
+  (∃ e', e = InjL e' ∧ is_val e') ∨ (∃ e', e = InjR e' ∧ is_val e').
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+(** Progress *)
+Lemma typed_progress e A:
+  TY 0; ∅ ⊢ e : A → is_val e ∨ reducible e.
+Proof.
+  remember ∅ as Γ. remember 0 as n.
+  induction 1 as [| | | | n Γ A B e Hty IH | n Γ A B e Hwf Hwf' Hty IH | n Γ A B e e' x Hwf Hty1 IH1 Hty2 IH2 | | | | n Γ e0 e1 e2 A Hty1 IH1 Hty2 IH2 Hty3 IH3 | n Γ e1 e2 A B Hty IH1 _ IH2 | n Γ e1 e2 op A B C Hop Hty1 IH1 Hty2 IH2 | n Γ e op A B Hop Hty IH | n Γ e1 e2 A B Hty1 IH1 Hty2 IH2 | n Γ e A B Hty IH | n Γ e A B Hty IH | n Γ e A B Hwf Hty IH | n Γ e A B Hwf Hty IH| n Γ e e1 e2 A B C Htye IHe Htye1 IHe1 Htye2 IHe2].
+  - subst. naive_solver.
+  - left. done.
+  - left. done.
+  - (* big lambda *) left; done.
+  - (* type app *)
+    right. destruct (IH HeqΓ Heqn) as [H1|H1].
+    + eapply canonical_values_forall in Hty as [e' ->]; last done.
+      eexists. eapply base_contextual_step. eapply TBetaS.
+    + destruct H1 as [e' H1]. eexists. eauto.
+  - (* pack *)
+    (* FIXME this will be an exercise for you soon :) *)
+    admit.
+  - (* unpack *)
+    (* FIXME this will be an exercise for you soon :) *)
+    admit.
+  - (* int *)left. done.
+  - (* bool*) left. done.
+  - (* unit *) left. done.
+  - (* if *)
+    destruct (IH1 HeqΓ Heqn) as [H1 | H1].
+    + eapply canonical_values_bool in Hty1 as (b & ->); last done.
+      right. destruct b; eexists; eapply base_contextual_step; constructor.
+    + right. destruct H1 as [e0' Hstep].
+      eexists. eauto.
+  - (* app *)
+    destruct (IH2 HeqΓ Heqn) as [H2|H2]; [destruct (IH1 HeqΓ Heqn) as [H1|H1]|].
+    + eapply canonical_values_arr in Hty as (x & e & ->); last done.
+      right. eexists.
+      eapply base_contextual_step, BetaS; eauto.
+    + right. destruct H1 as [e1' Hstep].
+      eexists. eauto.
+    + right. destruct H2 as [e2' H2].
+      eexists. eauto.
+  - (* binop *)
+    assert (A = Int ∧ B = Int) as [-> ->].
+    { inversion Hop; subst A B C; done. }
+    destruct (IH2 HeqΓ Heqn) as [H2|H2]; [destruct (IH1 HeqΓ Heqn) as [H1|H1]|].
+    + right. eapply canonical_values_int in Hty1 as [n1 ->]; last done.
+      eapply canonical_values_int in Hty2 as [n2 ->]; last done.
+      inversion Hop; subst; simpl.
+      all: eexists; eapply base_contextual_step; eapply BinOpS; eauto.
+    + right. destruct H1 as [e1' Hstep]. eexists. eauto.
+    + right. destruct H2 as [e2' H2]. eexists. eauto.
+  - (* unop *)
+    inversion Hop; subst A B op.
+    + right. destruct (IH HeqΓ Heqn) as [H2 | H2].
+      * eapply canonical_values_bool in Hty as [b ->]; last done.
+        eexists; eapply base_contextual_step; eapply UnOpS; eauto.
+      * destruct H2 as [e' H2]. eexists. eauto.
+    + right. destruct (IH HeqΓ Heqn) as [H2 | H2].
+      * eapply canonical_values_int in Hty as [z ->]; last done.
+        eexists; eapply base_contextual_step; eapply UnOpS; eauto.
+      * destruct H2 as [e' H2]. eexists. eauto.
+  - (* pair *)
+    destruct (IH2 HeqΓ Heqn) as [H2|H2]; [destruct (IH1 HeqΓ Heqn) as [H1|H1]|].
+    + left. done.
+    + right. destruct H1 as [e1' Hstep]. eexists. eauto.
+    + right. destruct H2 as [e2' H2]. eexists. eauto.
+  - (* fst *)
+    destruct (IH HeqΓ Heqn) as [H | H].
+    + eapply canonical_values_prod in Hty as (e1 & e2 & -> & ? & ?); last done.
+      right. eexists. eapply base_contextual_step. econstructor; done.
+    + right. destruct H as [e' H]. eexists. eauto.
+  - (* snd *)
+    destruct (IH HeqΓ Heqn) as [H | H].
+    + eapply canonical_values_prod in Hty as (e1 & e2 & -> & ? & ?); last done.
+      right. eexists. eapply base_contextual_step. econstructor; done.
+    + right. destruct H as [e' H]. eexists. eauto.
+  - (* injl *)
+    destruct (IH HeqΓ Heqn) as [H | H].
+    + left. done.
+    + right. destruct H as [e' H]. eexists. eauto.
+  - (* injr *)
+    destruct (IH HeqΓ Heqn) as [H | H].
+    + left. done.
+    + right. destruct H as [e' H]. eexists. eauto.
+  - (* case *)
+    right. destruct (IHe HeqΓ Heqn) as [H1|H1].
+    + eapply canonical_values_sum in Htye as [(e' & -> & ?) | (e' & -> & ?)]; last done.
+      * eexists. eapply base_contextual_step. econstructor. done.
+      * eexists. eapply base_contextual_step. econstructor. done.
+    + destruct H1 as [e' H1]. eexists. eauto.
+(*Qed.*)
+Admitted.
+
+
+
+
+Definition ectx_typing (K: ectx) (A B: type) :=
+  ∀ e, TY 0; ∅ ⊢ e : A → TY 0; ∅ ⊢ (fill K e) : B.
+
+
+Lemma fill_typing_decompose K e A:
+  TY 0; ∅ ⊢ fill K e : A →
+  ∃ B, TY 0; ∅ ⊢ e : B ∧ ectx_typing K B A.
+Proof.
+  unfold ectx_typing; induction K in A |-*; simpl; inversion 1; subst; eauto.
+  all: edestruct IHK as (? & ? & ?); eauto.
+Qed.
+
+Lemma fill_typing_compose K e A B:
+  TY 0; ∅ ⊢ e : B →
+  ectx_typing K B A →
+  TY 0; ∅ ⊢ fill K e : A.
+Proof.
+  intros H1 H2; by eapply H2.
+Qed.
+
+Lemma fmap_up_subst σ Γ: ⤉(subst σ <$> Γ) = subst (up σ) <$> ⤉Γ.
+Proof.
+  rewrite -!map_fmap_compose.
+  eapply map_fmap_ext. intros x A _. by asimpl.
+Qed.
+
+Lemma typed_subst_type n m Γ e A σ:
+  TY n; Γ ⊢ e : A → (∀ k, k < n → type_wf m (σ k)) → TY m; (subst σ) <$> Γ ⊢ e : A.[σ].
+Proof.
+  induction 1 as [ n Γ x A Heq | | | n Γ e A Hty IH | |n Γ A B e Hwf Hwf' Hty IH | n Γ A B e e' x Hwf Hty1 IH1 Hty2 IH2 | | | | | |? ? ? ? ? ? ? ? Hop | ? ? ? ? ? ? Hop | | | | | | ] in σ, m |-*; simpl; intros Hlt; eauto.
+  - econstructor. rewrite lookup_fmap Heq //=.
+  - econstructor; last by eapply type_wf_subst.
+    rewrite -fmap_insert. eauto.
+  - econstructor; last by eapply type_wf_subst. eauto.
+  - econstructor. rewrite fmap_up_subst. eapply IH.
+    intros [| x] Hlt'; rewrite /up //=.
+    + econstructor. lia.
+    + eapply type_wf_rename; last by (intros ???; simpl; lia).
+      eapply Hlt. lia.
+  - replace (A.[B/].[σ]) with (A.[up σ].[B.[σ]/]) by by asimpl.
+    eauto using type_wf_subst.
+  - (* pack *)
+    eapply (typed_pack _ _ _ (subst σ B)).
+    + eapply type_wf_subst; done.
+    + eapply type_wf_subst; first done.
+      intros [ | k] Hk; first ( asimpl;constructor; lia).
+      rewrite /up //=. eapply type_wf_rename; last by (intros ???; simpl; lia).
+      eapply Hlt. lia.
+    + replace (A.[up σ].[B.[σ]/]) with (A.[B/].[σ])  by by asimpl.
+      eauto using type_wf_subst.
+  - (* unpack *)
+    eapply (typed_unpack _ _ A.[up σ]).
+    + eapply type_wf_subst; done.
+    + replace (∃: A.[up σ])%ty with ((∃: A).[σ])%ty by by asimpl.
+      eapply IH1. done.
+    + rewrite fmap_up_subst. rewrite -fmap_insert.
+      replace (B.[σ].[ren (+1)]) with (B.[ren(+1)].[up σ]) by by asimpl.
+      eapply IH2.
+      intros [ | k] Hk; asimpl; first (constructor; lia).
+      eapply type_wf_subst; first (eapply Hlt; lia).
+      intros k' Hk'. asimpl. constructor. lia.
+  - (* binop *)
+    inversion Hop; subst.
+    all: econstructor; naive_solver.
+  - (* unop *)
+    inversion Hop; subst.
+    all: econstructor; naive_solver.
+  - econstructor; last naive_solver. by eapply type_wf_subst.
+  - econstructor; last naive_solver. by eapply type_wf_subst.
+Qed.
+
+Lemma typed_subst_type_closed C e A:
+  type_wf 0 C → TY 1; ⤉∅ ⊢ e : A → TY 0; ∅ ⊢ e : A.[C/].
+Proof.
+  intros Hwf Hty. eapply typed_subst_type with (σ := C .: ids) (m := 0) in Hty; last first.
+  { intros [|k] Hlt; last lia. done. }
+  revert Hty. by rewrite !fmap_empty.
+Qed.
+
+Lemma typed_subst_type_closed' x C B e A:
+  type_wf 0 A →
+  type_wf 1 C →
+  type_wf 0 B →
+  TY 1; <[x := C]> ∅ ⊢ e : A →
+  TY 0; <[x := C.[B/]]> ∅ ⊢ e : A.
+Proof.
+  intros ??? Hty.
+  set (s := (subst (B.:ids))).
+  rewrite -(fmap_empty s) -(fmap_insert s).
+  replace A with (A.[B/]).
+  2: { replace A with (A.[ids]) at 2 by by asimpl.
+      eapply type_wf_subst_dom; first done. lia.
+  }
+  eapply typed_subst_type; first done.
+  intros [ | k] Hk; last lia. done.
+Qed.
+
+Lemma typed_preservation_base_step e e' A:
+  TY 0; ∅ ⊢ e : A →
+  base_step e e' →
+  TY 0; ∅ ⊢ e' : A.
+Proof.
+  intros Hty Hstep. destruct Hstep as [ | | | op e v v' Heq Heval | op e1 v1 e2 v2 v3 Heq1 Heq2 Heval | | | | | | ]; subst.
+  - eapply app_inversion in Hty as (B & H1 & H2).
+    destruct x as [|x].
+    { eapply lam_anon_inversion in H1 as (C & D & [= -> ->] & Hwf & Hty). done. }
+    eapply lam_inversion in H1 as (C & D & Heq & Hwf & Hty).
+    injection Heq as -> ->.
+    eapply typed_substitutivity; eauto.
+  - eapply type_app_inversion in Hty as (B & C & -> & Hwf & Hty).
+    eapply type_lam_inversion in Hty as (A & Heq & Hty).
+    injection Heq as ->. by eapply typed_subst_type_closed.
+  - (* unpack *)
+    (* FIXME: this will be an exercise for you soon :) *)
+    admit.
+  - (* unop *)
+    eapply unop_inversion in Hty as (A1 & Hop & Hty).
+    assert ((A1 = Int ∧ A = Int) ∨ (A1 = Bool ∧ A = Bool)) as [(-> & ->) | (-> & ->)].
+    { inversion Hop; subst; eauto. }
+    + eapply canonical_values_int in Hty as [n ->]; last by eapply is_val_spec; eauto.
+      simpl in Heq. injection Heq as <-.
+      inversion Hop; subst; simpl in *; injection Heval as <-; constructor.
+    + eapply canonical_values_bool in Hty as [b ->]; last by eapply is_val_spec; eauto.
+      simpl in Heq. injection Heq as <-.
+      inversion Hop; subst; simpl in *; injection Heval as <-; constructor.
+  - (* binop *)
+    eapply binop_inversion in Hty as (A1 & A2 & Hop & Hty1 & Hty2).
+    assert (A1 = Int ∧ A2 = Int ∧ (A = Int ∨ A = Bool)) as (-> & -> & HC).
+    { inversion Hop; subst; eauto. }
+    eapply canonical_values_int in Hty1 as [n ->]; last by eapply is_val_spec; eauto.
+    eapply canonical_values_int in Hty2 as [m ->]; last by eapply is_val_spec; eauto.
+    simpl in Heq1, Heq2. injection Heq1 as <-. injection Heq2 as <-.
+    simpl in Heval.
+    inversion Hop; subst; simpl in *; injection Heval as <-; constructor.
+  - by eapply if_inversion in Hty as (H1 & H2 & H3).
+  - by eapply if_inversion in Hty as (H1 & H2 & H3).
+  - by eapply fst_inversion in Hty as (B & (? & ? & [= <- <-] & ? & ?)%pair_inversion).
+  - by eapply snd_inversion in Hty as (B & (? & ? & [= <- <-] & ? & ?)%pair_inversion).
+  - eapply case_inversion in Hty as (B & C & (? & ? & [= <- <-] & Hty & ?)%injl_inversion & ? & ?).
+    eauto.
+  - eapply case_inversion in Hty as (B & C & (? & ? & [= <- <-] & Hty & ?)%injr_inversion & ? & ?).
+    eauto.
+(*Qed.*)
+Admitted.
+
+Lemma typed_preservation e e' A:
+  TY 0; ∅ ⊢ e : A →
+  contextual_step e e' →
+  TY 0; ∅ ⊢ e' : A.
+Proof.
+  intros Hty Hstep. destruct Hstep as [K e1 e2 -> -> Hstep].
+  eapply fill_typing_decompose in Hty as [B [H1 H2]].
+  eapply fill_typing_compose; last done.
+  by eapply typed_preservation_base_step.
+Qed.
+
+Lemma typed_safety e1 e2 A:
+  TY 0; ∅ ⊢ e1 : A →
+  rtc contextual_step e1 e2 →
+  is_val e2 ∨ reducible e2.
+Proof.
+  induction 2; eauto using typed_progress, typed_preservation.
+Qed.
+
+(** derived typing rules *)
+Lemma typed_tapp' n Γ A B C e :
+  TY n; Γ ⊢ e : (∀: A) →
+  type_wf n B →
+  C = A.[B/] →
+  TY n; Γ ⊢ e <> : C.
+Proof.
+ intros; subst C; by eapply typed_tapp.
+Qed.