Proof of syntactic type safety for call-by-value STLC extended with natural number constants.

stlc+nat.v

Set Implicit Arguments.
Require Import List Program FunctionalExtensionality.

(** Proof of syntactic type safety for call-by-value STLC extended with ℕ. *)

(** Names/Variables will be identified with a natural number. 
    λx.λy.y x is represented as λλ0 1 *)
Definition var : Type := nat.

(** There is a need for partial maps, e.g., to keep track of what variable 
    corresponds to what type. The following definitions/properties are mostly
    taken almost verbatim from the Software Foundations book series, Volume 2. *)
Definition total_map (B:Type) := var -> B.
Definition t_empty {B:Type} (v : B) : total_map B :=
  (fun _ => v)
.
Definition t_update {B:Type} (m : total_map B)
                    (x : var) (v : B) :=
  fun x' => if PeanoNat.Nat.eqb x x' then v else m x'.

Lemma t_apply_empty: forall B x v, @t_empty B v x = v.
Proof. easy. Qed.
Lemma t_update_eq : forall B (m: total_map B) x v,
  (t_update m x v) x = v.
Proof.
  intros; unfold t_update; now rewrite PeanoNat.Nat.eqb_refl.
Qed.
Theorem t_update_neq : forall (B:Type) v x1 x2 (m : total_map B),
  x1 <> x2 ->
  (t_update m x1 v) x2 = m x2.
Proof.
  intros B v x1 x2 m H; unfold t_update; now apply PeanoNat.Nat.eqb_neq in H as ->.
Qed.
Lemma t_update_shadow : forall B (m: total_map B) v1 v2 x,
    t_update (t_update m x v1) x v2 = t_update m x v2.
Proof.
  intros; unfold t_update; extensionality y; now destruct (PeanoNat.Nat.eqb x y).
Qed.
Theorem t_update_same : forall B x (m : total_map B), t_update m x (m x) = m.
Proof.
  intros; unfold t_update; extensionality y.
  destruct (PeanoNat.Nat.eq_dec x y) as [H0|H0]; subst.
  - now rewrite PeanoNat.Nat.eqb_refl.
  - now apply PeanoNat.Nat.eqb_neq in H0 as ->.
Qed.
Theorem t_update_permute : forall (B:Type) v1 v2 x1 x2 (m : total_map B),
  x2 <> x1 ->
  (t_update (t_update m x2 v2) x1 v1) = (t_update (t_update m x1 v1) x2 v2).
Proof.
  intros; unfold t_update; extensionality y.
  destruct (PeanoNat.Nat.eq_dec x1 y) as [H0|H0]; subst.
  - rewrite PeanoNat.Nat.eqb_refl; now apply PeanoNat.Nat.eqb_neq in H as ->.
  - apply PeanoNat.Nat.eqb_neq in H0 as ->; now destruct (PeanoNat.Nat.eqb x2 y).
Qed.
Definition partial_map (B:Type) := total_map (option B).
Definition empty {B:Type} : partial_map B := t_empty None.
Definition update {B:Type} (m : partial_map B) (x : var) (v : B) :=
  t_update m x (Some v)
.
Lemma apply_empty : forall B x, @empty B x = None.
Proof.
  intros; unfold empty; now rewrite t_apply_empty.
Qed.
Lemma update_eq : forall B (m: partial_map B) x v,
  (update m x v) x = Some v.
Proof.
  intros; unfold update; now rewrite t_update_eq.
Qed.
Theorem update_neq : forall (B:Type) v x1 x2 (m : partial_map B),
  x2 <> x1 ->
  (update m x2 v) x1 = m x1.
Proof.
  intros; unfold update; now rewrite t_update_neq.
Qed.
Lemma update_shadow : forall B (m: partial_map B) v1 v2 x,
  update (update m x v1) x v2 = update m x v2.
Proof.
  intros; unfold update; now rewrite t_update_shadow.
Qed.
Theorem update_same : forall B v x (m : partial_map B),
  m x = Some v ->
  update m x v = m.
Proof.
  intros B v x m H0; unfold update; rewrite <- H0; apply t_update_same.
Qed.
Theorem update_permute : forall (B:Type) v1 v2 x1 x2 (m : partial_map B),
  x2 <> x1 ->
  (update (update m x2 v2) x1 v1) = (update (update m x1 v1) x2 v2).
Proof.
  intros; unfold update; now apply t_update_permute.
Qed.
Definition includedin {B} (m1 m2 : partial_map B) :=
  forall a b, m1 a = Some b -> m2 a = Some b
.
Lemma includedin_update B (m1 m2 : partial_map B) (a : var) (b : B) :
  includedin m1 m2  ->
  includedin (update m1 a b) (update m2 a b).
Proof.
  unfold includedin; intros;
  match goal with
  | [ |- (update _ ?a _) ?x = Some _ ] => destruct (PeanoNat.Nat.eq_dec a x)
  end; subst; (rewrite update_eq in * + rewrite update_neq in *); auto.
Qed.
Lemma includedin_empty B (m : partial_map B) : includedin empty m.
Proof.
  unfold includedin; intros;
  match goal with
  | [H: empty _ = Some _ |- _] => cbv in H; inversion H
  end.
Qed.
Lemma includedin_cons_propagate B (m1 m2 : partial_map B) (a : var) (b : B) :
  includedin (update m1 a b) m2 ->
  includedin (update m1 a b) (update m2 a b).
Proof.
  unfold includedin; intros H0 a0 b0 H1.
  destruct (PeanoNat.Nat.eq_dec a a0) as [H2|H2].
  - subst; rewrite update_eq in H1; inversion H1; subst; now rewrite update_eq.
  - rewrite update_neq in H1; trivial. rewrite update_neq; trivial.
    eapply H0; rewrite update_neq; trivial.
Qed.
#[global]
Notation "∅" := (empty).
#[global]
Notation "a '↦' b '◘' M" := (update M a b) (at level 80, b at next level).

(** Next, there needs to be a way to get fresh variables with respect to a
    given list of known variables. One way to do this is to get the maximum
    from the given list (since identifiers are numbers) and add One. *)
Definition fresh (xs:list var) : var := 1 + List.list_max xs.
Lemma fresh_above_any (x : var) (xs : list var) :
  List.In x xs -> x < fresh xs
.
Proof.
  intros; induction xs; cbn; try now inversion H.
  destruct H; apply PeanoNat.Nat.lt_succ_r.
  - subst; apply PeanoNat.Nat.le_max_l.
  - specialize (IHxs H); unfold fresh in *.
    apply PeanoNat.Nat.le_succ_l, le_S_n in IHxs.
    transitivity (List.list_max xs); eauto using PeanoNat.Nat.le_max_r.
Qed.
Lemma above_fresh_not_in (y : var) (xs : list var) : 
  fresh xs <= y -> ~ List.In y xs
.
Proof. 
  intros H0 H1%fresh_above_any%PeanoNat.Nat.lt_nge; contradiction.
Qed.
(** Having established basic properties on names, the following corollary
    establishes that (fresh xs) is actually fresh. *)
Corollary fresh_not_in (xs : list var) :
  ~ List.In (fresh xs) xs
.
Proof.
  eauto using above_fresh_not_in.
Qed.
(** Sometimes, I want to get a fresh identifier with respect to more
    than one list. While one could just (fresh (xs ++ ys)), I have chosen
    to just special-case it instead. *)
Definition fresh2 (xs ys : list var) := 
  max (fresh xs) (fresh ys)
.
Lemma above_fresh2_not_in (x : var) (xs ys : list var) :
  fresh2 xs ys <= x ->
  ~List.In x xs /\ ~List.In x ys
.
Proof.
  repeat split; eapply above_fresh_not_in; unfold fresh2 in *; trivial;
  transitivity (Nat.max (fresh xs) (fresh ys)); trivial;
  (apply PeanoNat.Nat.le_max_l + apply PeanoNat.Nat.le_max_r).
Qed.
Lemma fresh2_not_in (xs ys : list var) x :
  x = (fresh2 xs ys) ->
  ~List.In x xs /\ ~List.In x ys
.
Proof.
  intros ->; eapply above_fresh2_not_in; trivial.
Qed.

(** ** STLC+ℕ *)

Inductive ty : Type :=
  | Int : ty
  | Arrow : ty -> ty -> ty
.
Inductive expr : Type := 
  | econst : nat -> expr        (* constants 0,1,2,3,... *)
  | ebvar : var -> expr         (* bound variables *)
  | efvar : var -> expr         (* "free" variables, bound by a context *)
  | eapp : expr -> expr -> expr (* function application f a *)
  | elam : expr -> expr         (* lambda functions λ.e *)
.
Inductive value : expr -> Prop :=
  | vconst : forall n, value (econst n)
  | vlam : forall b, value (elam b)
.
Hint Constructors value : core.

(** Grabbing all free variables. *)
Fixpoint fv (e : expr) : list var := 
  match e with
  | econst n => nil
  | ebvar x => nil
  | efvar x => cons x nil
  | eapp a b => List.app (fv a) (fv b)
  | elam a => fv a
  end
.
(** An expression e is locally closed at k if all bound variables in e 
    are strictly less than k. *)
Fixpoint lc_at (k : var) (e : expr) : Prop :=
  match e with
  | econst _ => True
  | ebvar x => x < k
  | efvar _ => True
  | eapp a b => lc_at k a /\ lc_at k b
  | elam a => lc_at (S k) a
  end
.
Lemma lc_at_le k x e :
  k < x ->
  lc_at k e ->
  lc_at x e
.
Proof.
  revert k x; induction e; cbn; intros; trivial.
  - etransitivity; eauto.
  - split; (eapply IHe1 + eapply IHe2); destruct H0; eauto.
  - eapply IHe; try exact H0; now apply le_n_S.
Qed.
Lemma lc_at_Sx x e :
  lc_at x e ->
  lc_at (S x) e
.
Proof.
  apply lc_at_le; constructor.
Qed.

(** An expression can be "opened" by swapping a bound variable k 
    for a free variable y, thus "opening" up e. *)
Fixpoint open_at (k y : var) (e : expr) : expr :=
  match e with
  | econst n => econst n 
  | ebvar x => if Nat.eqb x k then efvar y else ebvar x
  | efvar x => efvar x
  | eapp a b => eapp (open_at k y a) (open_at k y b)
  | elam b => elam (open_at (S k) y b)
  end
.
(** The usual case for "opening" an expression is for the next best lambda. *)
Definition unbind (x : var) (e : expr) : expr := open_at O x e.

(** Substitution functions for both free and bound variables. *)
Fixpoint substFV (ewhat : var) (efor ein : expr) : expr :=
  match ein with
  | econst n => econst n
  | ebvar x => ebvar x
  | efvar x => if Nat.eqb x ewhat then efor else efvar x 
  | eapp a b => eapp (substFV ewhat efor a) (substFV ewhat efor b)
  | elam b => elam (substFV ewhat efor b)
  end
.
Fixpoint substBV (ewhat : var) (efor ein : expr) : expr :=
  match ein with
  | econst n => econst n
  | ebvar x => if Nat.eqb x ewhat then efor else ebvar x 
  | efvar x => efvar x
  | eapp a b => eapp (substBV ewhat efor a) (substBV ewhat efor b)
  | elam b => elam (substBV (S ewhat) efor b)
  end
.
(** Various properties related to lc, opening, and substitutions. *)
Lemma fv_open_at_subsets j x e :
  (forall y, List.In y (fv e) -> List.In y (fv (open_at j x e)))
.
Proof.
  revert j x; induction e; cbn; trivial; intros; try contradiction.
  apply List.in_app_or in H as [H|H]; apply List.in_or_app;
  (now (left + right); eauto).
  now eapply IHe.
Qed.
Lemma fv_unbind_subsets x e :
  (forall y, List.In y (fv e) -> List.In y (fv (unbind x e)))
.
Proof. 
  intros; eauto using fv_open_at_subsets.
Qed.
Lemma open_at_substBV k y e :
  open_at k y e = substBV k (efvar y) e
.
Proof.
  revert k; induction e; intros; cbn; eauto.
  now rewrite IHe1, IHe2.
  now rewrite IHe.
Qed.
Lemma lc_at_open_at k y e :
  lc_at k (open_at k y e) -> 
  lc_at (S k) e 
.
Proof.
  revert k y; induction e; cbn; intros k y H; eauto.
  - destruct (PeanoNat.Nat.eq_dec v k) as [->|H'];
    try eapply PeanoNat.Nat.lt_succ_diag_r;
    eapply PeanoNat.Nat.eqb_neq in H'; rewrite H' in H; cbn in H;
    transitivity k; eauto.
  - destruct H; eauto.
Qed.
Lemma lc_at_unbind y e :
  lc_at 0 (unbind y e) -> 
  lc_at 1 e 
.
Proof.
  apply lc_at_open_at.
Qed.
Lemma unbind_substBV y e :
  unbind y e = substBV O (efvar y) e
.
Proof.
  eapply open_at_substBV.
Qed.
Lemma substBV_substFV_unbind k i v e :
  ~ List.In k (fv e) ->
  substBV i v e = substFV k v (open_at i k e)
.
Proof.
  revert i; induction e; intros; cbn; eauto.
  - destruct (Nat.eqb v0 i); cbn; try rewrite PeanoNat.Nat.eqb_refl; try easy.
  - destruct (PeanoNat.Nat.eq_dec v0 k); subst.
    + exfalso; apply H; now left.
    + now apply PeanoNat.Nat.eqb_neq in n as ->.
  - rewrite IHe1, IHe2; try easy.
    all:intros H'; apply H; cbn; apply List.in_or_app; now (right + left).
  - now rewrite IHe.
Qed.
Lemma substFV_unbind k v e :
  ~ List.In k (fv e) ->
  substBV O v e = substFV k v (unbind k e)
.
Proof. apply substBV_substFV_unbind. Qed.
Lemma substBV_lc k x v e :
  k <= x ->
  lc_at k e ->
  substBV x v e = e
.
Proof.
  revert k x v; induction e; intros; cbn; try easy.
  - destruct (PeanoNat.Nat.eq_dec v x) as [->|H1].
    + eapply (PeanoNat.Nat.lt_le_trans x k x) in H0; eauto;
      exfalso; now eapply (PeanoNat.Nat.lt_irrefl x).
    + now apply PeanoNat.Nat.eqb_neq in H1 as ->.
  - erewrite IHe1, IHe2; eauto; now cbn in H0.
  - f_equal; revert H0; eapply IHe; eauto;
    now rewrite PeanoNat.Nat.add_le_mono_l with (p:=1) in H.
Qed.
Lemma commute_substFV_substBV x y v w e :
  lc_at x w ->
  substFV y w (substBV x v e) = substBV x (substFV y w v) (substFV y w e)
.
Proof.
  revert x y v w; induction e; intros; cbn; try easy; try (f_equal; eauto).
  - now destruct (PeanoNat.Nat.eqb v x).
  - destruct (PeanoNat.Nat.eqb v y); trivial;
    erewrite substBV_lc; eauto.
  - rewrite IHe; eauto using lc_at_Sx.
Qed.
Lemma substFV_unbind_comm x y v e :
  x <> y -> lc_at 0 v ->
  substFV x v (unbind y e) = unbind y (substFV x v e)
.
Proof.
  intros; repeat rewrite unbind_substBV.
  apply PeanoNat.Nat.eqb_neq in H.
  assert (substFV x v (efvar y) = efvar y) as H1 by (cbn; now rewrite PeanoNat.Nat.eqb_sym, H).
  rewrite commute_substFV_substBV; trivial.
  now rewrite H1.
Qed.

(** Dynamic semantics of STLC+ℕ are encoded as evaluation-context based. 
    To this end, I define a primitive step relation that simply
    "evaluates" function calls. *)
Inductive pstep : expr -> expr -> Prop :=
  | papp : forall a b, value b -> pstep (eapp (elam a) b) (substBV 0 b a)
.
(** Evaluation contexts are a neat way to factor structural rules in 
    small-step semantics that just reduce arguments of some construct.
    Remove the EappL constructor to get call-by-name instead of call-by-value.
*)
Inductive Ectx :=
  | Ehole 
  | EappL : Ectx -> expr -> Ectx
  | EappR : expr -> Ectx -> Ectx
.
(** Filling the hole of an evaluation context with a given expression. *)
Fixpoint fill_hole (K : Ectx) (e : expr) : expr :=
  match K with
  | Ehole => e
  | EappL K e' => eapp (fill_hole K e) e' 
  | EappR e' K => eapp e' (fill_hole K e)
  end
.
(** Evaluation-context based step reduction says that subexpressions (=redexes)
    that fill a hole of some evaluation context reduce. *)
Inductive estep : expr -> expr -> Prop :=
  | estepc : forall e e' e0 e0' E,
      e = fill_hole E e0 ->
      e' = fill_hole E e0' ->
      pstep e0 e0' ->
      estep e e'
.
(** Reflexive transitive closure of estep constitutes the final piece in 
    the dynamic semantics to describe a whole execution of a program. *)
Inductive star_step : expr -> expr -> Prop :=
  | star_refl : forall e, star_step e e
  | star_trans : forall e0 e1 e2, estep e0 e1 ->
      star_step e1 e2 ->
      star_step e0 e2
.

(** Typing uses a trick for lambdas to prevent name clashes.
    Given whatever set of pre-determined names, it is possible to extend 
    the typing context with any variable not part of that list. 
    This assumption is useful for the later proofs to prevent name captures. *)
Definition Gamma : Type := partial_map ty.
Inductive check : Gamma -> expr -> ty -> Prop :=
  | check_const : forall G n, check G (econst n) Int 
  | check_var : forall G x t,
      G x = Some t ->
      check G (efvar x) t
  | check_app : forall G a b ta tb,
      check G a (Arrow ta tb) ->
      check G b ta ->
      check G (eapp a b) tb
  | check_lam : forall G a ta tb nms,
      (forall y, ~List.In y nms -> check (y ↦ ta ◘ G) (unbind y a) tb) ->
      check G (elam a) (Arrow ta tb)
.
Hint Constructors check : core.

(** Weakening property is an easy induction. *)
Lemma weakening G G' e t :
  check G e t ->
  includedin G G' ->
  check G' e t
.
Proof.
  intros Ht; revert G'; induction Ht; intros; eauto;
  eapply check_lam; intros; eapply H0; eauto using includedin_update.
Qed.
(** Canonical forms lemmata. *)
Lemma cf_int e :
  check ∅ e Int ->
  value e ->
  exists n, e = econst n
.
Proof.
  intros H0 H1; dependent induction H0; eauto; inversion H1.
Qed.
Lemma cf_lam e t0 t1 :
  check ∅ e (Arrow t0 t1) ->
  value e ->
  exists bdy, e = elam bdy 
.
Proof.
  intros H0 H1; dependent induction H0; eauto; try now destruct H.
  inversion H1.
Qed.
(** Inversion lemma for lambdas. *)
Lemma invert_lam G a ta tb :
  check G (elam a) (Arrow ta tb) ->
  (exists nms, forall y, ~List.In y nms ->
    check (y ↦ ta ◘ G) (unbind y a) tb 
  )
.
Proof.
  intros Ht; dependent induction Ht; eauto.
Qed.

(** Expressions that typecheck under an empty context are locally closed at 0. *)
Lemma check_empty_lc v t :
  check ∅ v t ->
  lc_at 0 v
.
Proof.
  induction 1; cbn; eauto. eapply lc_at_unbind, H0, fresh_not_in.
Qed.
(** Any free variables in e should occur in G *)
Lemma lem_fv_subset G e t :
  check G e t ->
  (forall x, List.In x (fv e) -> G x <> None)
.
Proof.
  induction 1; cbn; try easy; unfold includedin; intros.
  - destruct H0 as [-> | []]; intros ?; congruence.
  - apply List.in_app_or in H1 as [H1|H1]; eauto.
  - specialize (@fresh2_not_in nms (fv a) _ eq_refl); intros [H2a H2b] H3.
    enough (x <> fresh2 nms (fv a)) as Hne.
    eapply H0; eauto using fv_unbind_subsets.
    rewrite update_neq; eauto.
    intros ->; contradiction.
Qed.
(** Likewise, anything that does not occur in G is not a free variable of e. *)
Lemma lem_fv_not_in G e t x :
  check G e t -> 
  G x = None ->
  ~ List.In x (fv e)
.
Proof.
  intros Ha Hb Hc; eapply lem_fv_subset; eauto.
Qed.

(** Substitution lemma *)
Lemma substitution G e t tv v x :
  G x = None ->
  check (x ↦ tv ◘ G) e t ->
  check ∅ v tv ->
  check G (substFV x v e) t
.
Proof.
  intros Hdom Ht Hv; remember (x ↦ tv ◘ G) as G';
  generalize dependent G; dependent induction Ht; intros; cbn; eauto.
  - destruct (PeanoNat.Nat.eq_dec x0 x) as [->|Hn].
    + subst; rewrite PeanoNat.Nat.eqb_refl. 
      rewrite update_eq in H; inversion H; subst; clear H.
      eapply weakening; eauto using includedin_empty.
    + assert (Hn':=Hn); apply PeanoNat.Nat.eqb_neq in Hn as ->; constructor; subst.
      rewrite update_neq in H; eauto.
  - eapply check_lam; intros; subst. instantiate (1:=cons x nms) in H1.
    assert (~In y nms) by (intros ?; apply H1; now right).
    specialize (H0 y H2 Hv (y ↦ ta ◘ G0)).
    assert (x <> y) as Hne by (intros ->; apply H1; now left).
    assert ((y ↦ ta ◘ G0) x = None) as Hno by (rewrite update_neq; eauto).
    assert ((y ↦ ta ◘ (x ↦ tv ◘ G0)) = (x ↦ tv ◘ (y ↦ ta ◘ G0))) as Heq by now rewrite update_permute.
    specialize (H0 Hno Heq).
    rewrite <- substFV_unbind_comm; eauto using check_empty_lc.
Qed.

(** Typing of evaluation contexts *)
Definition check_Ectx (G : Gamma) (E : Ectx) (t0 t1 : ty) : Prop :=
  forall e, check G e t0 -> check G (fill_hole E e) t1
.
Lemma Ehole_typing G t :
  check_Ectx G Ehole t t
.
Proof.
  unfold check_Ectx; intros; now cbn.
Qed.
Hint Resolve Ehole_typing : core.

(** De- and recomposition lemmata for evaluation context typing. *)
Lemma decomposition G E e t1 :
  check G (fill_hole E e) t1 ->
  exists t0, check_Ectx G E t0 t1 /\ check G e t0
.
Proof.
  revert t1; induction E; cbn; intros; eauto.
  - inversion H; subst. specialize (IHE _ H3); destruct IHE as [x [IHE1 IHE2]].
    exists x; split; trivial. unfold check_Ectx; intros; cbn.
    eapply check_app; eauto.
  - inversion H; subst. specialize (IHE _ H5); destruct IHE as [x [IHE1 IHE2]].
    exists x; split; trivial. unfold check_Ectx; intros; cbn.
    eapply check_app; eauto.
Qed.
Lemma recomposition G E e t0 t1 :
  check_Ectx G E t0 t1 ->
  check G e t0 ->
  check G (fill_hole E e) t1
.
Proof. auto. Qed.

(** Preservation is now proven in three steps, one for each reduction relation. *)
(** First up, primitive preservation. *)
Lemma ppreservation e e' t :
  check ∅ e t -> 
  pstep e e' ->
  check ∅ e' t
.
Proof.
  intros H; remember ∅ as G; revert e' HeqG; induction H; intros; match goal with [H: pstep _ _ |- _] => inversion H; subst end.
  assert (H':=H); eapply invert_lam in H as [nms H].
  pose proof (fresh_not_in nms); specialize (H (fresh nms) H2).
  erewrite substFV_unbind; try instantiate (1:=fresh nms). 
  eapply substitution; eauto.
  eapply lem_fv_not_in with (x:=fresh nms) in H'; easy.
Qed.
(** Evaluation-context based preservation is a simple consequence from 
    primitive preservation as well as the decomposition lemma for 
    evaluation context typing. *)
Corollary epreservation e e' t :
  estep e e' -> 
  check ∅ e t -> 
  check ∅ e' t
.
Proof.
  revert t; induction 1; intros; subst.
  eapply decomposition in H2 as [t' [H2a H2b]].
  eapply ppreservation in H1; eauto.
Qed.
(** Finally, preservation follows from star induction. *)
Corollary preservation e e' t :
  star_step e e' ->
  check ∅ e t ->
  check ∅ e' t
.
Proof.
  intros H; revert t; induction H; intros; trivial;
  eapply epreservation in H; eauto.
Qed.

(** Progressive expressions are either values or they have a redex *)
Definition progressive (e : expr) : Prop :=
  value e \/ exists e', estep e e'
.
(** Progress can then be proven in a straightforward fashion *)
Lemma progress e t :
  check ∅ e t ->
  progressive e
.
Proof.
  remember ∅ as G; induction 1; cbn; (try now left); right; subst; try easy.
  - destruct (IHcheck1 eq_refl).
    + inversion H; inversion H1; subst; try discriminate. inversion H7; subst.
      destruct (IHcheck2 eq_refl).
      * exists (substBV O b a0). econstructor. instantiate (2:=Ehole); now cbn.
        now cbn. now constructor.
      * destruct H2 as [b' H2]. inversion H2; subst.
        exists (eapp (elam a0) (fill_hole E e0')).
        econstructor. instantiate (2:=EappR (elam a0) E); now cbn.
        now cbn. trivial.
    + destruct H1 as [a' H1]. inversion H1; subst.
      exists (eapp (fill_hole E e0') b). econstructor.
      instantiate (2:=EappL E b); now cbn. now cbn. trivial.
Qed.

(** Lastly, establish syntactic type saftey as a consequence from 
    progress and preservation lemmata. *)
Theorem type_safety e e' t :
  check ∅ e t ->
  star_step e e' ->
  progressive e'
.
Proof.
  eintros H Hs; eapply preservation in Hs as Hs'; eauto.
  eapply progress; eauto.
Qed.