Strong Normalization for STLC

TypeSystem.v

Require Import Coq.Unicode.Utf8 Arith FunctionalExtensionality String Coq.Program.Equality.

Set Implicit Arguments.

Ltac invert H := inversion H; clear H; subst.
Ltac invert1 H := invert H; [].

Inductive star A (R : A -> A -> Prop) : A -> A -> Prop :=
| StarRefl : forall x,
  star R x x
| StarStep : forall x1 x2 x3,
  R x1 x2
  -> star R x2 x3
  -> star R x1 x3.

Theorem star_trans : forall A (R : A -> A -> Prop) x1 x2 x3,
  star R x1 x2
  -> star R x2 x3
  -> star R x1 x3.
Proof.
  induction 1; intros.

  assumption.

  econstructor.
  eassumption.
  apply IHstar.
  assumption.
Qed.

Lemma star_incl : forall A (R : A -> A -> Prop) x1 x2,
  R x1 x2
  -> star R x1 x2.
Proof.
  intros.
  econstructor 2.
  eassumption.
  constructor.
Qed.

Inductive exp : Set :=
| Var : string -> exp
| Const : bool -> exp
| Abs : string -> exp -> exp
| App : exp -> exp -> exp
| IfThenElse : exp -> exp -> exp -> exp.

Inductive value : exp -> Prop :=
| VConst : forall b, value (Const b) 
| VAbs : forall x e1, value (Abs x e1).

(* assume e' is closed *)
Fixpoint subst (x : string) (e' : exp) (e : exp) : exp :=
  match e with
    | Var y => if string_dec y x then e' else Var y
    | Const b => Const b
    | Abs y e1 => Abs y (if string_dec y x then e1 else subst x e' e1)
    | App e1 e2 => App (subst x e' e1) (subst x e' e2)
    | IfThenElse e1 e2 e3 => IfThenElse (subst x e' e1) (subst x e' e2) (subst x e' e3)
  end.

Inductive context : Set :=
| Hole : context
| App1 : context -> exp -> context
| App2 : exp -> context -> context
| IfCond : context -> exp -> exp -> context.

Inductive plug : context -> exp -> exp -> Prop :=
| PlugHole : forall e, plug Hole e e
| PlugApp1 : forall e e' C e2,
  plug C e e'
  -> plug (App1 C e2) e (App e' e2)
| PlugApp2 : forall e e' v1 C,
  value v1
  -> plug C e e'
  -> plug (App2 v1 C) e (App v1 e')
| PlugIfCond : forall e e' C e2 e3,
  plug C e e'
  -> plug (IfCond C e2 e3) e (IfThenElse e' e2 e3).

Inductive step0 : exp -> exp -> Prop :=
| Beta : forall x e v,
  value v
  -> step0 (App (Abs x e) v) (subst x v e)
| IfTrue : forall e1 e2,
  step0 (IfThenElse (Const true) e1 e2) e1
| IfFalse : forall e1 e2,
  step0 (IfThenElse (Const false) e1 e2) e2.

Inductive step : exp -> exp -> Prop :=
| Step : forall C e1 e2 e1' e2',
  plug C e1 e1'
  -> plug C e2 e2'
  -> step0 e1 e2
  -> step e1' e2'.

Inductive type : Set :=
| Bool : type
| Fun : type -> type -> type.

Definition tyenv := string -> option type.

Notation empty := (fun _ => None).

Definition extend (x : string) (t : type) (G : tyenv) : tyenv :=
  fun y => if string_dec y x then Some t else G y.

Inductive hasty : tyenv -> exp -> type -> Prop :=
| HtVar : forall G x t,
  G x = Some t
  -> hasty G (Var x) t
| HtConst : forall G b,
  hasty G (Const b) Bool
| HtAbs : forall G x e1 t1 t2,
  hasty (extend x t1 G) e1 t2
  -> hasty G (Abs x e1) (Fun t1 t2)
| HtApp : forall G e1 e2 t1 t2,
  hasty G e1 (Fun t1 t2)
  -> hasty G e2 t1
  -> hasty G (App e1 e2) t2
| HtIfThenElse : forall G e e1 e2 t,
  hasty G e Bool
  -> hasty G e1 t
  -> hasty G e2 t
  -> hasty G (IfThenElse e e1 e2) t.

Hint Constructors star value plug step0 step hasty.

(* Type Safety *)

Ltac t1' := match goal with
            | [ |- context[step (IfThenElse (Const ?x) _ _) _] ] => is_var x; destruct x
            | [ H : ex _ |- _ ] => destruct H
            | [ H : hasty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H
            | [ H : step _ _ |- _ ] => invert H
            | [ H : hasty _ _ _ |- _ ] => invert1 H
            | [ H : plug _ _ _ |- _ ] => invert1 H
            end.

Ltac t1 := simpl; intuition subst; repeat t1'; try congruence; eauto 6.

Lemma progress : forall e t,
  hasty empty e t
  -> value e
  \/ (exists e' : exp, step e e').
Proof.
  intros.
  (* dependent induction H; simpl; t1. *)
  dependent induction H; simpl.

  left; constructor.
  left; constructor.

  right.
  intuition.
  
    inversion H2; subst.
    inversion H; subst.
    inversion H3; subst.

    econstructor.
    econstructor.
    apply PlugHole.
    apply PlugHole.
    constructor.
    assumption.

    econstructor.
    econstructor.
    apply PlugHole.
    apply PlugHole.
    constructor.
    assumption.

    destruct H3.
    inversion H1; subst.
    econstructor.
    econstructor.
    apply PlugApp2.
    assumption.
    eassumption.
    apply PlugApp2.
    assumption.
    eassumption.
    assumption.

    destruct H2.
    inversion H1; subst.
    econstructor.
    econstructor.
    eapply PlugApp1.
    eassumption.
    eapply PlugApp1.
    eassumption.
    assumption.

    destruct H2.
    inversion H1; subst.
    econstructor.
    econstructor.
    eapply PlugApp1.
    eassumption.
    eapply PlugApp1.
    eassumption.
    assumption.

  right.
  intuition.

    inversion H3; subst.
    inversion H; subst.
    destruct b.

      econstructor.
      econstructor.
      eapply PlugHole.
      eapply PlugHole.
      eapply IfTrue.

      econstructor.
      econstructor.
      eapply PlugHole.
      eapply PlugHole.
      eapply IfFalse.

    inversion H.

    inversion H3; subst.
    inversion H; subst.
    destruct H5.
    destruct b.
      
      econstructor.
      econstructor.
      eapply PlugHole.
      eapply PlugHole.
      eapply IfTrue.
      
      econstructor.
      econstructor.
      eapply PlugHole.
      eapply PlugHole.
      eapply IfFalse.

    inversion H.
  
    inversion H3; subst.
    inversion H; subst.
    destruct H4.
    destruct b.
      
      econstructor.
      econstructor.
      eapply PlugHole.
      eapply PlugHole.
      eapply IfTrue.
      
      econstructor.
      econstructor.
      eapply PlugHole.
      eapply PlugHole.
      eapply IfFalse.

    inversion H.

    inversion H3; subst.
    inversion H; subst.
    destruct H4.
    destruct b.
      
      econstructor.
      econstructor.
      eapply PlugHole.
      eapply PlugHole.
      eapply IfTrue.
      
      econstructor.
      econstructor.
      eapply PlugHole.
      eapply PlugHole.
      eapply IfFalse.

    inversion H.

    destruct H3.
    inversion H2; subst.
    econstructor.
    econstructor.
    eapply PlugIfCond.
    eassumption.
    eapply PlugIfCond.
    eassumption.
    assumption.

    destruct H3.
    inversion H2; subst.
    econstructor.
    econstructor.
    eapply PlugIfCond.
    eassumption.
    eapply PlugIfCond.
    eassumption.
    assumption.

    destruct H3.
    inversion H2; subst.
    econstructor.
    econstructor.
    eapply PlugIfCond.
    eassumption.
    eapply PlugIfCond.
    eassumption.
    assumption.

    destruct H3.
    inversion H2; subst.
    econstructor.
    econstructor.
    eapply PlugIfCond.
    eassumption.
    eapply PlugIfCond.
    eassumption.
    assumption.
Qed.

Hint Resolve progress.

Lemma extend_eq : forall G t x t',
  extend x t' G x = Some t
  -> t = t'.
Proof.
  unfold extend.
  intros.
  destruct (string_dec x x); congruence. 
Qed.

Lemma extend_neq : forall G t x y t',
  extend x t' G y = Some t
  -> x <> y
  -> G y = Some t.
Proof.
  unfold extend.
  intros.
  destruct (string_dec y x); congruence. 
Qed.

Lemma extend_weakening : forall G G' x t,
  (forall x' t', G x' = Some t' -> G' x' = Some t')
  -> (forall x' t', extend x t G x' = Some t'
                    -> extend x t G' x' = Some t').
Proof.
  unfold extend.
  intros.
  destruct (string_dec x' x). 

    assumption.
    
    apply H.
    assumption.
Qed.

Lemma weakening : forall G e t,
  hasty G e t
  -> forall G', (forall x t, G x = Some t -> G' x = Some t)
    -> hasty G' e t.
Proof.
  induction 1; intros.

  econstructor.
  eapply H0.
  assumption.

  econstructor.

  econstructor.
  apply IHhasty.
  apply extend_weakening.
  assumption.

  econstructor.
  apply IHhasty1; assumption.
  apply IHhasty2; assumption.

  intuition.
Qed.

Lemma hasty_change : forall G e t,
  hasty G e t
  -> forall G', G' = G
    -> hasty G' e t.
Proof.
  congruence.
Qed.

Lemma substitution : forall G x t' e t e',
  hasty (extend x t' G) e t
  -> hasty empty e' t'
  -> hasty G (subst x e' e) t.
Proof.
  intros.
  dependent induction H; simpl.

  destruct (string_dec x0 x).

    subst.
    apply extend_eq in H.
    subst.
    eapply weakening.
    eassumption.
    congruence.

    apply extend_neq in H.
    econstructor.
    eassumption.
    congruence.

  econstructor.

  econstructor.
  destruct (string_dec x0 x).

    subst.
    eapply hasty_change.
    eassumption.
    extensionality y.
    unfold extend.
    destruct (string_dec y x); subst; congruence.

    eapply IHhasty with (t'0 := t').
    extensionality y.
    unfold extend.
    destruct (string_dec y x0); subst;
    destruct (string_dec x0 x); subst;
    congruence.

  assumption.
  
  intuition.
  econstructor; eassumption.

  intuition.
Qed.

Lemma preservation0 : forall e1 e2,
  step0 e1 e2
  -> forall t, hasty empty e1 t
    -> hasty empty e2 t.
Proof.
  intros.
  invert H; invert H0.

  invert H4.
  eapply substitution; eassumption.

  assumption.
  assumption.
Qed.

Lemma generalize_plug : forall C e1 e1',
  plug C e1 e1'
  -> forall e2 e2', plug C e2 e2'
    -> (forall t, hasty empty e1 t -> hasty empty e2 t)
    -> (forall t, hasty empty e1' t -> hasty empty e2' t).
Proof.
  (* induction 1; t1. *)

  induction 1; intros. 

  invert H.
  apply H0.
  assumption.

  invert H0.
  invert H2.
  econstructor.
  eapply IHplug.
  eassumption.
  eassumption.
  eassumption.
  assumption.

  invert H1.
  invert H3.
  econstructor.
  eassumption.
  eapply IHplug.
  eassumption.
  assumption.
  assumption.

  invert H0.
  invert H2.
  econstructor.
  eapply IHplug.
  eassumption.
  assumption.
  assumption.
  assumption.
  assumption.
Qed.

Lemma preservation : forall e1 e2,
  step e1 e2
  -> forall t, hasty empty e1 t
    -> hasty empty e2 t.
Proof.
  intros.
  invert H.
  apply (generalize_plug H1 H2).
  eapply preservation0.
  assumption.
  assumption.
Qed.

Theorem safety : forall e1 e2, star step e1 e2
  -> forall t, hasty empty e1 t
  -> value e2
     \/ (exists e3, step e2 e3).
Proof.
  intros.
  induction H.

  eapply progress.
  eassumption.

  apply IHstar.
  eapply preservation.
  eassumption.
  assumption.
Qed.

(* Determinism *)

(* We exploit flat small step to show the determinism *)
Inductive fstep : exp -> exp -> Prop :=
| FBeta : forall x e1 v,
  value v
  -> fstep (App (Abs x e1) v) (subst x v e1)
| FApp1 : forall e1 e1' e2,
  fstep e1 e1'
  -> fstep (App e1 e2) (App e1' e2)
| FApp2 : forall e1 e2 e2',
  value e1
  -> fstep e2 e2'
  -> fstep (App e1 e2) (App e1 e2')
| FIfCond : forall e e' e1 e2,
  fstep e e'
  -> fstep (IfThenElse e e1 e2) (IfThenElse e' e1 e2)
| FIfTrue : forall e1 e2,
  fstep (IfThenElse (Const true) e1 e2) e1
| FIfFalse : forall e1 e2,
  fstep (IfThenElse (Const false) e1 e2) e2.

Hint Constructors fstep.

Lemma value_not_fstep : forall v,
  value v
  -> forall e, not (fstep v e).
Proof.
  destruct 2; invert H.
Qed.

Ltac t2' := match goal with
            | [ H : fstep ?e _ |- _ ] => first [ is_var e; fail 1 | invert H] 
            | [ H : fstep ?e _, H' : value ?e |- _ ] => exfalso; eapply (value_not_fstep H' H)
            | [ H : step _ _ |- _ ] => invert H
            | [ H : plug _ _ _ |- _ ] => invert1 H
            | [ |- App _ _ = App _ _ ] => f_equal 
            | [ |- IfThenElse _ _ _ = IfThenElse _ _ _ ] => f_equal 
            end.

Ltac t2 := simpl; intuition subst; repeat t2'; try congruence; eauto 6.

Lemma fstep_step : forall e1 e2,
  fstep e1 e2
  -> step e1 e2.
Proof.
  induction 1; t2.
Qed.

Lemma plug_fstep : forall c e1 e1', 
  plug c e1 e1'
  -> forall e2 e2', plug c e2 e2'
                    -> fstep e1 e2
                    -> fstep e1' e2'.
Proof.
  induction 1; t2.
Qed.

Lemma step_fstep : forall e1 e2, 
  step e1 e2
  -> fstep e1 e2.
Proof.
  destruct 1; destruct H1; eapply plug_fstep; eauto.
Qed.

Lemma determinism' : forall e e1,
  fstep e e1
  -> forall e2, fstep e e2
                -> e1 = e2.
Proof.
  induction 1; intros; t2.
Qed.

Lemma determinism : forall e e1,
  step e e1
  -> forall e2, step e e2
                -> e1 = e2.
Proof.
  intros.
  eapply determinism'; eapply step_fstep; eassumption.
Qed.

Inductive hasval : exp -> Prop :=
| Hv : forall e v,
  value v
  -> star step e v
  -> hasval e.

Hint Constructors hasval.

Lemma value_hasval : forall v, value v -> hasval v.
Proof.
  eauto.
Qed.

Lemma value_not_step : forall v,
  value v
  -> forall e, not (step v e).
Proof.
  destruct 2; destruct H; invert H0; invert H2.
Qed.

Lemma hasval_preservation : forall e1 e2,
  step e1 e2
  -> hasval e1
  -> hasval e2.
Proof.
  destruct 2.
  destruct H1.
  exfalso.
  eapply value_not_step; eassumption.
  econstructor.
  eassumption.
  replace e2 with x2.
  assumption.
  eapply determinism; eassumption. 
Qed.

Lemma hasval_backward_preservation : forall e1 e2,
  step e1 e2
  -> hasval e2
  -> hasval e1.
Proof.
  destruct 2.
  eauto.
Qed.

(* Strong Normalization *)

Open Scope list_scope.

Definition expass := list (string * exp).
Definition tyass := list (string * type).

Fixpoint msubst (s : expass) (e : exp) : exp :=
  match s with
    | nil => e
    | ((x, e') :: s') => msubst s' (subst x e' e)
  end.

Fixpoint mextend (S : tyass) (G : tyenv) : tyenv :=
  match S with
    | nil => G
    | ((x, t) :: S') => extend x t (mextend S' G) 
  end.

Inductive fit0 : expass -> tyass -> Prop :=
| FitEmpty0 : fit0 nil nil
| FitExtend0 : forall s S x e t,
  fit0 s S
  -> hasty empty e t
  -> fit0 ((x, e) :: s) ((x, t) :: S).

Lemma multisubstitution : forall s S,
  fit0 s S
  -> forall G e t, hasty G e t
                   -> G = mextend S empty
                   -> hasty empty (msubst s e) t.
Proof.
  induction 1; intros.

  simpl in *.
  rewrite H0 in H.
  assumption.

  simpl.
  eapply IHfit0.
  eapply substitution.
  simpl in H2.
  rewrite H2 in H1.
  eassumption.
  assumption.
  reflexivity.
Qed.

Fixpoint not_freein (x : string) (e : exp) : Prop :=
  match e with
  | Var y => y <> x
  | Const _ => True
  | Abs y e1 => y = x \/ not_freein x e1
  | App e1 e2 => not_freein x e1 /\ not_freein x e2
  | IfThenElse e e1 e2 => not_freein x e /\ not_freein x e1 /\ not_freein x e2
  end.

Lemma not_freein_substitution : forall x e, 
  not_freein x e
  -> forall e', subst x e' e = e.
Proof.
  intros.
  induction e; simpl.

  destruct (string_dec s x).
  destruct H.
  assumption.
  reflexivity.

  reflexivity.

  destruct (string_dec s x).
  reflexivity.
  destruct H.
  congruence. 
  rewrite IHe; [ reflexivity | assumption ].

  destruct H.
  rewrite IHe1, IHe2; [ reflexivity | assumption .. ].

  destruct H.
  destruct H0.
  rewrite IHe1, IHe2, IHe3; [ reflexivity | assumption .. ].
Qed.

Definition closed (e : exp) : Prop := forall x, not_freein x e.

Fixpoint closed_expass (s : expass) : Prop :=
  match s with
  | nil => True
  | (x, e) :: s' => closed e /\ closed_expass s'
  end.

Lemma closed_substitution : forall e,
  closed e
  -> (forall x e', subst x e' e = e).
Proof.
  intros.
  apply not_freein_substitution.
  apply H.
Qed.

Lemma closed_multisubstitution : forall e,
  closed e
  -> (forall s, msubst s e = e).
Proof.
  intros.
  induction s; simpl.

  reflexivity.

  destruct a.
  replace (subst s0 e0 e) with e.
  assumption.
  symmetry.
  apply closed_substitution.
  assumption.
Qed.

Fixpoint lookup (A : Set) (x : string) (ls : list (string * A)) : option A :=
  match ls with
  | nil => None
  | (y, a) :: ls' => if string_dec y x then Some a else lookup x ls'
  end.

Fixpoint remove (A : Set) (x : string) (ls : list (string * A)) : list (string * A) :=
  match ls with
  | nil => nil
  | (y, a) :: ls' => if string_dec y x then remove x ls' else (y, a) :: remove x ls'
  end.

Lemma extend_idem : forall x t t' G,
  extend x t (extend x t' G) = extend x t G. 
Proof.
  intros.
  extensionality y.
  unfold extend.
  destruct (string_dec y x); reflexivity.
Qed.

Lemma extend_comm : forall x x' t t' G,
  x <> x'
  -> extend x t (extend x' t' G) = extend x' t' (extend x t G). 
Proof.
  intros.
  extensionality y.
  unfold extend.
  destruct (string_dec y x); destruct (string_dec y x'); congruence || reflexivity.
Qed.

Lemma mextend_remove : forall x t S G,
  mextend ((x, t) :: remove x S) G = mextend ((x, t) :: S) G.
Proof.
  intros.
  induction S; simpl in *.

  reflexivity.

  destruct a.
  destruct (string_dec s x).

    subst.
    rewrite extend_idem.
    apply IHS.

    simpl.
    rewrite extend_comm.
    rewrite IHS.
    rewrite extend_comm.
    reflexivity.
    assumption.
    simplify_eq; intuition.
Qed.

Lemma subst_comm : forall e e1 e2 x1 x2,
  closed e1
  -> closed e2
  -> x1 <> x2
  -> subst x1 e1 (subst x2 e2 e) = subst x2 e2 (subst x1 e1 e).
Proof.
  intros.
  induction e; simpl.

  destruct (string_dec s x1); destruct (string_dec s x2); simpl. 
  congruence.
  destruct (string_dec s x1).
  rewrite closed_substitution.
  reflexivity.
  assumption.
  congruence.
  destruct (string_dec s x2).
  rewrite closed_substitution.
  reflexivity.
  assumption.
  congruence.
  destruct (string_dec s x1); destruct (string_dec s x2); simpl. 
  congruence.
  congruence.
  congruence.
  reflexivity.

  reflexivity.

  destruct (string_dec s x1); destruct (string_dec s x2); simpl. 
  reflexivity.
  reflexivity.
  reflexivity.
  rewrite IHe.
  reflexivity.
 
  rewrite IHe1, IHe2.
  reflexivity.

  rewrite IHe1, IHe2, IHe3.
  reflexivity.
Qed.

Lemma subst_msubst_comm : forall x e s,
  closed e
  -> closed_expass s
  -> forall e', subst x e (msubst (remove x s) e') = msubst ((x, e) :: remove x s) e'. 
Proof.
  intros.
  dependent induction s; simpl.

  reflexivity.

  destruct a.
  simpl in H0.
  destruct H0.
  destruct (string_dec s0 x).
    
    apply IHs.
    assumption.
    assumption.

    simpl.
    rewrite subst_comm; try assumption. 
    apply IHs; assumption.
Qed.


Lemma msubst_var : forall s x,
  closed_expass s
  -> msubst s (Var x) =
       match lookup x s with
       | Some e => e
       | None => (Var x)
       end.
Proof.
  intros.
  dependent induction s; simpl.

  reflexivity.

  destruct a.  
  destruct H.
  destruct (string_dec x s0); subst.

    destruct (string_dec s0 s0).
    apply closed_multisubstitution.
    assumption.
    congruence.

    destruct (string_dec s0 x).
    rewrite e0 in n.
    congruence.
    apply IHs.
    assumption.
Qed.

Lemma msubst_abs : forall s x e,
  closed_expass s
  -> msubst s (Abs x e) = Abs x (msubst (remove x s) e).
Proof.
  intros.
  dependent induction s; simpl.

  reflexivity.

  destruct a.
  destruct H.
  destruct (string_dec x s0); subst.

    destruct (string_dec s0 s0).
    apply IHs.
    assumption.
    congruence.
    
    destruct (string_dec s0 x).
    subst; congruence.
    simpl.
    apply IHs.
    assumption.
Qed.

Lemma msubst_app : forall s e1 e2,
  msubst s (App e1 e2) = App (msubst s e1) (msubst s e2).
Proof.
  intros.
  dependent induction s; simpl.

  reflexivity.

  destruct a.
  apply IHs.
Qed.

Lemma msubst_if : forall s e e1 e2,
  msubst s (IfThenElse e e1 e2) = IfThenElse (msubst s e) (msubst s e1) (msubst s e2).
Proof.
  intros.
  dependent induction s; simpl.

  reflexivity.

  destruct a.
  apply IHs.
Qed.

Lemma hasty_not_freein : forall G e t,
  hasty G e t
  -> forall x, G x = None
               -> not_freein x e.
Proof.
  intros.
  dependent induction H; simpl.

  congruence.
  constructor.
  
  destruct (string_dec x0 x).
  left; subst; reflexivity.
  right.
  apply IHhasty.
  unfold extend.
  destruct (string_dec x0 x).
  congruence.
  assumption.

  split; [apply IHhasty1 | apply IHhasty2]; assumption.

  split; [apply IHhasty1 | split; [ apply IHhasty2 | apply IHhasty3 ] ]; assumption.
Qed.

Lemma hasty_closed : forall e t,
  hasty empty e t
  -> closed e.
Proof.
  unfold closed.
  intros.
  eapply hasty_not_freein.
  eassumption.
  simpl.
  reflexivity.
Qed.

(* Coq rejects this because of a negative occurrence of sn
Inductive sn : type -> exp -> Prop :=
| SNBool : forall e,
  hasty empty e Bool
  -> hasval e
  -> sn Bool e
| SNFun : forall e t1 t2,
  hasty empty e (Fun t1 t2)
  -> hasval e
  -> (forall e', sn t1 e' -> sn t2 (App e e'))
  -> sn (Fun t1 t2) e.
*)

Fixpoint sn (t : type) (e : exp) {struct t} : Prop :=
  hasty empty e t /\ hasval e /\
  (match t with
   | Bool => True
   | Fun t1 t2 => forall e', sn t1 e' -> sn t2 (App e e')
   end).

Lemma sn_hasty : forall t e, sn t e -> hasty empty e t.
Proof.
  unfold sn.
  destruct t; intuition.
Qed.

Lemma sn_hasval : forall t e, sn t e -> hasval e.
Proof.
  unfold sn.
  destruct t; intuition.
Qed.

Lemma sn_preservation : forall t e1 e2, 
  step e1 e2
  -> sn t e1
  -> sn t e2.
Proof.
  intros.
  dependent induction t; destruct H0; destruct H1. 

  split.
  eapply preservation; eassumption.
  split.
  eapply hasval_preservation; eassumption.
  intuition.

  split.  
  eapply preservation; eassumption.
  split.
  eapply hasval_preservation; eassumption.
  intros.
  assert (step (App e1 e') (App e2 e')).
  inversion H.
  econstructor.
  eapply PlugApp1.
  eassumption.
  eapply PlugApp1.
  eassumption.
  assumption.
  eapply IHt2.
  eassumption.
  apply H2.
  assumption.
Qed.

Lemma sn_preservation_star : forall t e1 e2, 
  star step e1 e2
  -> sn t e1
  -> sn t e2.
Proof.
  intros.
  induction H.

  assumption.

  apply IHstar.
  eapply sn_preservation; eassumption.
Qed.

Lemma sn_backward_preservation : forall t e1 e2, 
  hasty empty e1 t
  -> step e1 e2
  -> sn t e2
  -> sn t e1.
Proof.
  intros.
  dependent induction t; destruct H1; destruct H2. 

  split.
  assumption.
  split.
  eapply hasval_backward_preservation; eassumption.
  intuition.

  split.
  assumption.
  split.
  eapply hasval_backward_preservation; eassumption.
  intros.
  assert (step (App e1 e') (App e2 e')).
  invert H0.
  econstructor.
  eapply PlugApp1.
  eassumption.
  eapply PlugApp1.
  eassumption.
  assumption.
  eapply IHt2.
  econstructor.
  eassumption.
  apply sn_hasty; assumption.
  eassumption.
  apply H3.
  assumption.
Qed.

Lemma sn_backward_preservation_star : forall t e1 e2, 
  hasty empty e1 t
  -> star step e1 e2
  -> sn t e2
  -> sn t e1.
Proof.
  intros.
  induction H0.

  assumption.

  eapply sn_backward_preservation.
  assumption.
  eassumption.
  apply IHstar.
  eapply preservation.
  eassumption.
  assumption.
  assumption.
Qed.

Inductive fit : expass -> tyass -> Prop :=
| FitEmpty : fit nil nil
| FitExtend : forall s S x e t,
  fit s S
  -> sn t e
  -> fit ((x, e) :: s) ((x, t) :: S).


Lemma fit_fit0 : forall s S, fit s S -> fit0 s S.
Proof.
  induction 1.

  constructor.

  econstructor.
  assumption.
  apply sn_hasty.
  assumption.
Qed.

Lemma fit_closed : forall s S, fit s S -> closed_expass s.
Proof.
  induction 1; simpl.

  constructor.

  invert H.
  split.
  eapply hasty_closed.
  eapply sn_hasty.
  eassumption.
  assumption.
  split.
  eapply hasty_closed.
  eapply sn_hasty.
  eassumption.
  assumption.
Qed.

Lemma fit_remove : forall s S,
  fit s S
  -> forall x, fit (remove x s) (remove x S).
Proof.
  intros.
  dependent induction H; simpl.

  constructor. 

  destruct (string_dec x x0).
  apply IHfit.
  constructor.
  apply IHfit.
  assumption.
Qed.

Lemma star_step_app2 : forall v e e',
  value v
  -> star step e e'
  -> star step (App v e) (App v e'). 
Proof.
  induction 2.

  constructor 1.

  destruct H0.
  econstructor.
  econstructor.
  eapply PlugApp2.
  eassumption.
  eassumption.
  eapply PlugApp2.
  eassumption.
  eassumption.
  assumption.
  assumption.
Qed.

Lemma star_step_if : forall e e' e1 e2,
  star step e e'
  -> star step (IfThenElse e e1 e2) (IfThenElse e' e1 e2). 
Proof.
  induction 1.

  constructor 1.

  destruct H.
  econstructor.
  econstructor.
  eapply PlugIfCond.
  eassumption.
  eapply PlugIfCond.
  eassumption.
  assumption.
  assumption.
Qed.

Lemma preservation_star : forall e1 e2,
  star step e1 e2
  -> forall t, hasty empty e1 t
    -> hasty empty e2 t.
Proof.
  induction 1; intros.

  assumption.

  eapply IHstar.  
  eapply preservation; eassumption.
Qed.

Lemma fundamental_property : forall G e t,
  hasty G e t
  -> forall s S, fit s S
                 -> G = mextend S empty
                 -> sn t (msubst s e).
Proof.
  intros.
  dependent induction H; subst.

  induction H0; simpl in *.
  congruence.
  destruct (string_dec x x0); subst.

    replace t0 with t in *; [ | eapply extend_eq; eassumption ]. 
    replace (msubst s e) with e.
    assumption.
    symmetry.
    eapply closed_multisubstitution.
    eapply hasty_closed.
    eapply sn_hasty.
    eassumption.

    eapply IHfit.
    eapply extend_neq.
    eassumption.
    simplify_eq.
    subst.
    assumption.

  replace (msubst s (Const b)) with (Const b). 
  split.
  constructor.
  split.
  eapply value_hasval.
  econstructor.
  constructor.
  symmetry.
  eapply closed_multisubstitution.
  constructor.

  assert (hasty empty (msubst s (Abs x e1)) (Fun t1 t2)).
  eapply multisubstitution.
  eapply fit_fit0.
  eassumption.
  econstructor.
  eassumption.
  reflexivity.
  rewrite msubst_abs in *; [ | eapply fit_closed; eassumption .. ].
  split.
  assumption.
  split.
  eapply value_hasval.
  constructor.

  intros.
  assert (hasval e').
  eapply sn_hasval; eassumption.
  destruct H3.
  assert (sn t1 v).
  eapply sn_preservation_star; eassumption.
  eapply sn_backward_preservation_star.
  econstructor.
  eassumption.
  eapply sn_hasty.
  assumption.
  eapply star_trans.
  eapply star_step_app2.
  constructor.
  eassumption.
  eapply star_incl.
  eapply Step with (C := Hole).
  eapply PlugHole.
  eapply PlugHole.
  eapply Beta.
  assumption.
  rewrite subst_msubst_comm.
  eapply IHhasty with (S0 := (x, t1) :: remove x S).
  econstructor.
  apply fit_remove; assumption.
  assumption.
  rewrite mextend_remove.
  simpl.
  reflexivity.
  eapply hasty_closed. 
  eapply sn_hasty.
  eassumption.
  eapply fit_closed.
  eassumption.

  rewrite msubst_app.
  eapply IHhasty1.
  eassumption.
  reflexivity.
  eapply IHhasty2.
  eassumption.
  reflexivity.

  rewrite msubst_if.
  assert (sn Bool (msubst s e)).
  eapply IHhasty1; eassumption || reflexivity.
  destruct H3.
  destruct H4.
  destruct H4.
  assert (hasty empty v Bool).
  eapply preservation_star; eassumption.
  invert H4; invert H7.
  destruct b.

    eapply sn_backward_preservation_star.
    econstructor.
    assumption.
    eapply sn_hasty; eapply IHhasty2; eassumption || reflexivity.
    eapply sn_hasty; eapply IHhasty3; eassumption || reflexivity.
    eapply star_trans.
    eapply star_step_if.
    eassumption.
    eapply star_incl.
    econstructor.
    eapply PlugHole.
    eapply PlugHole.
    eapply IfTrue.
    eapply IHhasty2; eassumption || reflexivity.

    eapply sn_backward_preservation_star.
    econstructor.
    assumption.
    eapply sn_hasty; eapply IHhasty2; eassumption || reflexivity.
    eapply sn_hasty; eapply IHhasty3; eassumption || reflexivity.
    eapply star_trans.
    eapply star_step_if.
    eassumption.
    eapply star_incl.
    econstructor.
    eapply PlugHole.
    eapply PlugHole.
    eapply IfFalse.
    eapply IHhasty3; eassumption || reflexivity.
Qed.

Lemma strong_normalization : forall e t,
  hasty empty e t -> hasval e.
Proof.
  intros.
  eapply sn_hasval.
  replace e with (msubst nil e).
  eapply fundamental_property.
  eassumption.
  constructor.
  simpl; reflexivity.
  simpl; reflexivity.
Qed.