Release exercise 2.7

_CoqProject

@@ -18,6 +18,13 @@ theories/type_systems/stlc/notation.v
 theories/type_systems/stlc/untyped.v
 theories/type_systems/stlc/types.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/bigstep.v
+theories/type_systems/stlc_extended/ctxstep.v
+
 # By removing the # below, you can add the exercise sheets to make
 #theories/type_systems/warmup/warmup.v
 #theories/type_systems/warmup/warmup_sol.v

theories/type_systems/stlc_extended/bigstep.v

@@ -0,0 +1,49 @@
+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.ts.stlc_extended Require Import lang notation types.
+
+(** * Big-step semantics *)
+
+Implicit Types
+  (Γ : typing_context)
+  (v : val)
+  (e : expr)
+  (A : type).
+
+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
+
+(* TODO : extend the big-step semantics *)
+    .
+#[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.
+
+(* TODO : this should be fixed once you have added the right semantics *)
+Admitted.
+
+
+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

@@ -0,0 +1,180 @@
+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)
+  (* TODO: extend the definition *)
+.
+
+#[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)
+  (* TODO: extend the definition *)
+.
+
+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)
+  (* TODO: extend the definition *)
+  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')
+  (* TODO: extend the definition *)
+  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.
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma contextual_step_pair_r e1 e2 e2':
+  contextual_step e2 e2' →
+  contextual_step (Pair e1 e2) (Pair e1 e2').
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma contextual_step_fst e e':
+  contextual_step e e' →
+  contextual_step (Fst e) (Fst e').
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma contextual_step_snd e e':
+  contextual_step e e' →
+  contextual_step (Snd e) (Snd e').
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma contextual_step_injl e e':
+  contextual_step e e' →
+  contextual_step (InjL e) (InjL e').
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma contextual_step_injr e e':
+  contextual_step e e' →
+  contextual_step (InjR e) (InjR e').
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+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.
+
+
+#[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/lang.v

@@ -0,0 +1,175 @@
+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.
+
+Inductive expr :=
+  (* Base lambda calculus *)
+  | Var (x : string)
+  | Lam (x : binder) (e : expr)
+  | App (e1 e2 : expr)
+  (* Base types and their operations *)
+  | LitInt (n: Z)
+  | Plus (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 :=
+  | LitIntV (n: Z)
+  | LamV (x : binder) (e : expr)
+  | 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
+  | LitIntV n => LitInt n
+  | LamV x e => Lam x e
+  | 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
+  | LitInt n => Some $ LitIntV n
+  | Lam x e => Some (LamV x e)
+  | 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
+  | LitInt l => True
+  | Lam x e => True
+  | 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 | | 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 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.
+
+(** Substitution *)
+Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
+  match e with
+  | LitInt _ => 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)
+  | Plus e1 e2 => Plus (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.
+
+(** Closed terms **)
+
+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
+  | LitInt _ => true
+  | Fst e | Snd e | InjL e | InjR e => is_closed X e
+  | App e1 e2 | Plus e1 e2 | Pair e1 e2 => is_closed X e1 && is_closed X 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.

theories/type_systems/stlc_extended/notation.v

@@ -0,0 +1,56 @@
+From semantics.ts.stlc_extended Require Export lang.
+Set Default Proof Using "Type".
+
+
+(** Coercions to make programs easier to type. *)
+Coercion of_val : val >-> expr.
+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" := (LitIntV l%Z%V%stdpp) (at level 8, format "# l").
+Notation "# l" := (LitInt 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 "e1 + e2" := (Plus e1%E e2%E) : expr_scope.
+
+(*Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : 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.

theories/type_systems/stlc_extended/types.v

@@ -0,0 +1,255 @@
+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.
+
+(** ** 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
+  (* TODO: provide the new typing rules *)
+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.
+
+(* TODO: add inversion lemmas for the new typing rules.
+  They will be very useful for the proofs below!
+*)
+
+
+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.
+  - (* TODO *) admit.
+  - (* TODO *) admit.
+  - (* TODO *) admit.
+  - (* TODO *) admit.
+  - (* TODO *) admit.
+  - (* TODO *) admit.
+Admitted.
+
+(** 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.
+
+(* TODO: add canonical forms lemmas for the new types *)
+
+(** 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].
+  - 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.
+
+(* FIXME: prove the new cases *)
+Admitted.
+
+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.
+
+(* TODO: extend this for the new cases *)
+Admitted.
+
+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.