(** * Normalization of simply typed lambda calculus (TAPL Chapter 12)

We now formalize the version of Tait's normalization proof for simply
typed lambda calculus that is described in TAPL Chapter 12. The language
we study contains only functions and a single base type. The same proof
technique could easily be extended to a language with e.g. booleans and
numbers, but for simplicity, we here stick to a minimal language.

The developments below differ somewhat from those in TAPL, and the main
technical reason for this is the fact that we have no convention that
forces all variables to be distinct. This simplifies definitions, but
forces us to occasionally check whether two variables are the same or
not.

It is customary to present a proof from the bottom up, building complex
proofs from simpler ones, and in Coq this is even a technical necessity.
However, the actual practice of proving is often different: a number of
the auxiliary lemmas below were proven only after noticing, in the
middle of another proof, that the proof depends on a non-trivial
property, which is better to prove separately.

Note that before the section "Substitution" most of the
definitions and proofs are familiar from earlier chapters. They are
only included because we are now dealing with a different language
(one with just functions and a single base type [A]), so we have to
prove the results again, even though the proof scripts are sometimes
word-for-word identical. *)

Require Import notations.

Require Export tapl_ch8.
Require Export tapl_ch9.

Module typed_base_fun.

Require Export typed_base_fun_lang.

Hint Constructors term val eval type typing and or ex bound fvs : base_fun.

Hint Constructors RSC : base_fun.

Hint Unfold not : base_fun.

Notation "t1 -->* t2" := 
  (RSC eval t1 t2) (at level 80, no associativity) : type_scope.

Definition closed t := forall x, ~(fvs t x).

Definition normal_form t := ~exists t', t --> t'.

Hint Unfold normal_form : base_fun.

Definition well_typed (t : term) : Prop :=
  exists T, |- t : T.

Definition halts (t : term) : Prop :=
  exists t', t -->* t' /\ normal_form t'.

Hint Unfold halts.

Inductive fv : term -> Prop :=
  fv_abs x T t : fv (\x:T,t)%tm.

Hint Constructors fv : base_fun.

Lemma fv_is_val t : fv t -> val t.
Proof.
  intros t fv_t.
  destruct fv_t.
  apply Val_Abs.
Qed.


(** ** Canonical forms *)

Lemma canonical_forms_fun : forall v T1 T2, val v -> |- v : (T1 -> T2) -> fv v.
Proof.
  intros v T1 T2 val_v v_F.
  induction val_v; inversion v_F; subst; 
    try inversion H; eauto with base_fun.
Qed.

Hint Resolve canonical_forms_fun : base_fun.


(** ** Progress *)

Theorem progress t : well_typed t -> val t \/ exists t', t --> t'.
Proof with eauto with base_fun.
  intros t [T t_T].
  remember {}%ctx as G.
  induction t_T; subst G...
    Case "T_Var {} x T H".
    (* Impossible to have a bound variable in an empty context. *)
    inversion H.

    Case "T_App {} t1 t2 T12 T11 t_T1 t_T2".
    destruct IHt_T1 as [val_t1 | [t1' t1Et1']]...
      SCase "val t1".
      destruct IHt_T2 as [val_t2 | [t2' t2Et2']]...
        SSCase "val t2".
        elimtype (fv t1)...
Qed.



Corollary normal_is_value t : well_typed t -> normal_form t -> val t.
Proof.
  intros t wf_t nf_t.
  destruct (progress t wf_t).
    trivial.
  
    contradiction H.
Qed.


Lemma val_is_normal : forall t, val t -> normal_form t.
Proof with eauto with base_fun.
  intros t vt.
  destruct vt.
  intros [t' tEt'].
  inversion tEt'.
Qed.

Hint Resolve val_is_normal : base_fun.


(** *** Evaluation is deterministic *)

Lemma eval_deterministic : forall t t' t'', t --> t' -> t --> t'' -> t' = t''.
Proof with eauto with base_fun.
  intros t t' t'' tEt' tEt''.
  induction tEt' in t'', tEt'' |- *; inversion tEt''; subst...
    rewrite -> (IHtEt' t1'0)...

    contradiction (val_is_normal t1)...

    inversion tEt'.

    contradiction (val_is_normal t1)...

    rewrite -> (IHtEt' t2'0)...

    contradiction (val_is_normal t2)...

    inversion H3.

    contradiction (val_is_normal t2)...
Qed.


(** *** Only the types of the free variables of a term affect its typing *)

Lemma context_invariance : 
  forall G G' t T,
  (forall x T', fvs t x -> bound x T' G -> bound x T' G')  ->
  G |- t : T  ->
  G' |- t : T.
Proof with eauto 20 with base_fun.
  intros G G' t T H G_t_T.
  induction G_t_T in G', H |- *...
    Case "T_Abs".
    apply T_Abs.
    apply IHG_t_T.
    intros x' T' x'_f_t2 B.
    inversion B...
Qed.


(** A well-typed term has its type in any context *)

Lemma empty_weakening : forall G t T, |- t : T -> G |- t : T.
Proof with eauto with base_fun.
  intros G t T t_T.
  apply (context_invariance {})...
    intros x T' x_f_t x_B_E.
    inversion x_B_E.
Qed.


(** *** Substitution preserves typing *)

Theorem subst_preservation : forall G x S s t T,
  {G, x : S} |- t : T   -> 
  {} |- s : S           -> 
  G |- [x |-> s]t : T.
Proof with eauto with base_fun.
  intros G x S s t T t_T s_S.
  induction t in G, T, t_T |- *; simpl; inversion t_T; subst...

    Case "T_Var".
    assert (Q := beq_decides_eq_nat x v).
    destruct (beq_nat x v); simpl in Q.
      SCase "x = v".
      subst v.
      inversion H1; subst.
        SSCase "B_Here".
        apply empty_weakening.
        apply s_S.

        SSCase "B_Next".
        contradiction H4.
        reflexivity.

      SCase "x <> v".
      apply T_Var.
      inversion H1; subst.
        SSCase "B_Here".
        contradiction Q.
        reflexivity.

        SSCase "B_Next".
        assumption.
 
    Case "T_Abs".        
    assert (Q := beq_decides_eq_nat x v).
    destruct (beq_nat x v); simpl in Q.
      SCase "x = v".
      subst v.
      apply T_Abs.
      apply (context_invariance {{G, x : S}, x : t}%ctx)...
      intros x' T' x'_f_t2 x'_B_G1.
      destruct (nat_eq_dec x x') as [xQx' | nxQx'].
        SSCase "x = x'".
        subst x'.
        inversion x'_B_G1; subst...
          contradiction H3...
          
        SSCase "x <> x'".
        inversion x'_B_G1; subst...
        inversion H6; subst...
          contradiction H3...

      SCase "x <> v".
      apply T_Abs.
      apply IHt.
      apply (context_invariance {{G, x : S}, v : t}%ctx)...
      intros x' T' x'_f_t2 x'_B_G1.
      inversion x'_B_G1; subst.
        SSCase "B_Here".
        apply B_Next...

        SSCase "B_Next".
        inversion H6; subst...
Qed.


(** *** Evaluation preserves typing *)

Theorem preservation : forall t t' T, 
  |- t : T    ->  
  t --> t'    ->  
  |- t' : T.
Proof.
(** Exercise **)
Admitted.

(** *** Multi-step evaluation preserves typing *)

Theorem meval_preservation : forall t t' T, 
  |- t : T    ->  
  t -->* t'   ->  
  |- t' : T.
Proof.
  intros t t' T tT tMt'.
  induction tMt'; eauto using preservation.
Qed.
    



(** ** A free variable of a typable term must be bound in the context *)

Lemma free_in_context : forall G t T x, 
  (G |- t : T) -> fvs t x -> exists T', bound x T' G.
Proof.
  intros G t T x G_t_T x_f_t.
  induction G_t_T; inversion x_f_t; subst; auto.
    Case "T_Var".
      SCase "FVS_Var".
      exists T.
      apply H.
    
    Case "T_Abs".
      SCase "FVS_Abs".
      destruct (IHG_t_T H4) as [T' B].
      exists T'.
      inversion B; subst.
        SSCase "B_Here".
        contradiction H3.
        reflexivity.

        SSCase "B_Next".
        assumption.
Qed.


Hint Unfold well_typed : base_fun.

(** ** A well-typed term is closed *)

Corollary well_typed_is_closed : forall t, well_typed t -> closed t.
Proof.
  intros t [T t_T].
  red.
  red.
  intros x x_f_t.
  destruct (free_in_context {} t T x t_T x_f_t) as [T' B].
  inversion B.
Qed.

Hint Resolve well_typed_is_closed : base_fun.


(** ** Substitution

The proof of the normalization of the simply-typed lambda calculus
depends heavily on various basic properties of the substitution
operation [[x |-> t']t] which replaces every free occurrence of [x] in
[t] with [t']. In informal proofs, most of these properties are often
considered so self-evident that they are not even worth mentioning.
However, when we formalize our reasoning, we often find that various
supposedly self-evident facts require a substantial amount of proving.
Thankfully, the proofs are usually reasonably simple.

We next prove some basic lemmas about substitution. Almost all the
proofs proceed by induction on the term in which we substitute. In the
[TmVar] and [TmAbs] cases we have to take into account the equality or
inequality of variables which is checked by the substitution function.
The [beq_nat_eq_dec] lemma allows us to easily check the two possible
cases.


*** Substituting for a non-free variable has no effect

The substitution function has been designed so that it substitutes only
in the _free_ occurrences of [x] in [t]. If there are no free
occurrences of [x] in [t], the result of the substitution is the
original term unchanged. This fact is proven below. *)

Lemma closed_subst_nop t x t' : ~(fvs t x) -> ([x |-> t']t)%tm = t.
Proof with eauto with base_fun.
  intros t x t' nx_f_t.
  induction t as [y | y T t'' IHt'' | t1 IHt1 t2 IHt2]; simpl.
    Case "t = 'y".
    destruct (beq_nat_eq_dec x y) as [[H Q] | [H Q]]...
(** If [x = y], it contradicts our assumption that [x] does not appear
           free in [t]. *)
      SCase "x = y".
      contradiction nx_f_t.
      rewrite -> Q...

(** If [x <> y], the substitution produces the original term 
         directly. *)
      SCase "x <> y".
      rewrite -> H...


    Case "t = \y:T, t''".
    destruct (beq_nat_eq_dec x y) as [[H Q] | [H Q]]...
(** If [x = y] then substitution produces the original term 
         directly. *)
      SCase "x = y".
      rewrite -> H...
      

(** If [x <> y] then we apply the inductive hypothesis. Even
         though [y] may appear free in [t''], we know that [x <> y] so
         [~(fvs x t'')] is proved easily by automation. *)
      SCase "x <> y".
      rewrite -> H.
      rewrite -> IHt''...

(** The [TmApp] case is proved directly with the inductive
       hypotheses. *)
    Case "t = t1 $ t2".
    rewrite -> IHt1...
    rewrite -> IHt2...
Qed.

      
(** *** Repeated substitution of the same variable has no additional effect

If we substitute [[x |-> s]t], and [s] is closed, then the result of this
substitution cannot contain any free occurrences of [x]. Hence if we
then do another substitution of [x], it will have no further effect.

*)

Lemma subst_idem {t x s s'} : closed s ->
  ([x |-> s']([x |-> s]t))%tm = ([x |-> s]t)%tm.
Proof.
  intros t x s s' clo_s.
  induction t; simpl.
    Case "TmVar".
    destruct (beq_nat_eq_dec x v) as [[Q H] | [Q H]].
      SCase "x = v".
      rewrite -> Q.
      auto using closed_subst_nop.

(** Here we see a reason why we could not simply do [destruct
      (beq_nat x v)]: the same equality test is done _twice_ by each
      of the substitutions. If we did [destruct] for both cases, we
      would end up considering cases where [beq_nat x v] returned [true]
      at one time, and [false] at another. So instead, we have checked
      the result once and for all and stored it in an equality, and then
      use it to rewrite uniformly all instances of [beq_nat x v] that we
      meet. *)
      SCase "x <> v".
      rewrite -> Q.
      simpl.
      rewrite -> Q.
      reflexivity.

    Case "TmAbs".
    destruct (beq_nat_eq_dec x v) as [[Q H] | [Q H]].
      SCase "x = v".
      rewrite -> Q.
      simpl.
      rewrite -> Q.
      reflexivity.

      SCase "x <> v".
      rewrite -> Q.
      simpl.
      rewrite -> Q.
      rewrite -> IHt.
      reflexivity.

    Case "TmApp".
    rewrite -> IHt1.
    rewrite -> IHt2.
    reflexivity.
Qed.


(** *** Substitution of distinct variables commutes

Suppose we substitute [[x |-> s][x' |-> s']t], when [x <> x'] and [s]
and [s'] are both closed. Then both of these substitutions are
independent of each other: one replaces the free occurrences of [x], and
the other replaces the free occurrences of [x']. Because [s] and [s']
are both closed, they don't contain free occurrences of [x'] or [x], so
one substitution cannot produce any subterms which would be affected by
the other substitution. *)

Lemma beq_nat_refl_false x x' : x <> x' -> beq_nat x x' = false.
Proof.
  intros x x' xNQx'.
  assert (Q' := beq_decides_eq_nat x x').
  destruct (beq_nat x x'); simpl in Q'...
      contradiction xNQx'.
      reflexivity.
Qed.
    
Lemma subst_exchange x s x' s' t :
  x <> x' -> closed s -> closed s' ->
  ([x |-> s]([x' |-> s'] t))%tm = ([x' |-> s']([x |-> s] t))%tm.
Proof with auto.
  intros x s x' s' t xNQx' clo_s clo_s'.
  assert (beq_nat x' x = false) as H1.
    auto using beq_nat_refl_false with base_fun.
  assert (beq_nat x x' = false) as H2.
    auto using beq_nat_refl_false.
  induction t; simpl.
    Case "TmVar".
    assert (Q := beq_decides_eq_nat x v).
    remember (beq_nat x v) as E.
    destruct E; simpl in Q |- *.
      subst v.
      rewrite -> H1.
      simpl.
      rewrite <- HeqE.
      rewrite -> closed_subst_nop...

      assert (Q' := beq_decides_eq_nat x' v).
      remember (beq_nat x' v) as E'.
      destruct E'; simpl in Q |- *.
        rewrite -> closed_subst_nop...

        rewrite <- HeqE...

    Case "TmAbs".
    assert (Q := beq_decides_eq_nat x' v).
    remember (beq_nat x' v) as E.
    destruct E; simpl in Q |- *.
      subst v.
      rewrite -> H2.
      simpl.
      rewrite <- HeqE.
      reflexivity.

      assert (Q' := beq_decides_eq_nat x v).
      remember (beq_nat x v) as E'.
      destruct E'; simpl in Q |- *.
        rewrite <- HeqE.
        reflexivity.

        rewrite <- HeqE.
        rewrite -> IHt.
        reflexivity.

    Case "TmApp".
    rewrite -> IHt1.
    rewrite -> IHt2.
    reflexivity.
Qed.


(** ** Evaluation

Next, two basic facts about evaluation and halting.


*** Evaluation preserves halting *)

Lemma eval_preserves_halts : forall t t', t --> t' -> halts t -> halts t'.
Proof with eauto with base_fun.
(** Exercise **)
Admitted.

(** *)


(** *** Evaluation reflects halting *)

Lemma eval_reflects_halts : forall t t', t --> t' -> halts t' -> halts t.
Proof with eauto with base_fun.
  intros t t' tEt' [t'' [t'Et'' nft'']]...
Qed.



(** *** Multi-step evaluation is congruent in the argument position

We are going to need this particular congruence result later on.

*)

Lemma meval_app2_congr : forall t1 t2 t2',
    val t1 ->
    t2 -->* t2'  -> (t1 $ t2)%tm -->* (t1 $ t2')%tm.
Proof.
  intros val_t1 t1 t2 t2' t2Mt2'.
  induction t2Mt2'; eauto with base_fun.
Qed.



(** ** Recursive halting (TAPL 12.1.2)

After the above preliminary work, we are finally ready to begin the
actual normalization proof. The first stage is defining the recursive
halting predicate, [R_T(t)] in TAPL. This formally no different from our
previous recursive definitions, except that this time the our recursive
function produces a _proposition_ instead of a value.

Notice that in TAPL the predicate [R_T] is defined on "closed terms of
type T". We could include these constraints in the propositions produced
by the definition below, or even in the domain of the function, but this
would complicate the formalization a little. Instead, we simply add
additional constraints for closedness or well-typedness wherever they
are needed. This accounts for some of the slight differences between the
formalization below and the definition in TAPL.

*)

Fixpoint rhalts (T : type) (t : term) : Prop :=
  match T with
    | A%ty => halts t
    | (T1 -> T2)%ty => 
      halts t /\ forall s, |- s : T1 -> rhalts T1 s -> rhalts T2 (t $ s)
  end.

Hint Unfold rhalts.


(** *** Recursively halting terms are halting (TAPL 12.1.3) *)

Lemma rhalts_then_halts T t : rhalts T t -> halts t.
Proof.
 intros T t rTt.
 destruct T.
   exact rTt.

   destruct rTt as [ht _].
   exact ht.
Qed.


(** *** Evaluation preserves and reflects recursive halting (TAPL 12.1.4)

These basic facts are straightforward to prove. Note that it is usually
more practical to prove and use each direction of an equivalence as a
separate implication lemma. (Sometimes, however, we need a bidirectional
equivalence as a inductive hypothesis, so both directions have to be
proven simultaneously. That is not the case here, though.)

*)

Lemma eval_preserves_rhalts T t t' :
  t --> t' -> rhalts T t -> rhalts T t'.
Proof with eauto 10 with base_fun.
  intros T t t' tEt'.
  induction T in t, t', tEt' |- *; simpl.
    apply eval_preserves_halts...

    intros [ht rt].
    split.
      eapply eval_preserves_halts...
        
      intros s sT1 rT1s.
      eapply IHT2...
Qed.

Corollary meval_preserves_rhalts T t t' :
  t -->* t' -> rhalts T t -> rhalts T t'.
Proof.
  intros T t t' tMt'.
  induction tMt'; eauto using eval_preserves_rhalts.
Qed.

Lemma eval_reflects_rhalts T t t' :
  t --> t' -> rhalts T t' -> rhalts T t.
Proof with eauto 10 with base_fun.
  intros T t t' tEt'.
  induction T in t, t', tEt' |- *; simpl.
    apply eval_reflects_halts...

    intros [ht' rt'].
    split.
      eapply eval_reflects_halts...

      intros s sT1 rT1s.
      eapply IHT2...
Qed.

Corollary meval_reflects_rhalts T t t' :
  t -->* t' -> rhalts T t' -> rhalts T t.
Proof.
  intros T t t' tMt'.
  induction tMt'; eauto using eval_reflects_rhalts.
Qed.


(** ** Substitution environments

We now get to the most complicated part of our proof developments. In
principle, we would like to show that [|- t : T] implies [rhalts T t].
However, this only makes sense for closed terms. If we try to prove this
by induction on the typing derivation (or on the structure of [t]), then
we eventually encounter the open terms that are the bodies of lambda
abstractions. The question is: what properties do we want open terms to
have in order to prove that closed terms halt?

A direct consequence of our evaluation rules is that if we begin
evaluating a closed term [t], then at it remains closed during every
step of the evaluation, i.e. every [t'] is closed when [t -->* t']. In
particular, every open subterm (and those are always within the bodies
of lambda abstractions) has all its free variables replaced by closed
terms before it is evaluated.

So the relevant question about the evaluation of open terms is what
happens to the result of substituting the free variables of a term with
closed terms.

More precisely, if [G] is a context [x1:T1, x2:T2...], and we have [G |-
t : T], the question is what happens to [[x1 |-> v1][x2 |-> v2]...t],
where the values [vn] are closed and have [|- vn : Tn]. Moreover, since
we want to prove recursive halting by induction, we can as an inductive
hypothesis assume that we have [rhalts Tn vn].

Our first step is to formalize this sequence [v1, v2...], which should
have the above properties relative to a context [G]. We firstly define
an _environment_ as simply a list of terms: *)

Inductive env :=
| env_empty
| env_extend : env -> term -> env
.

Delimit Scope env_scope with env.
Bind Scope env_scope with env.


(** *** Typing of an environment with respect to a typing context

We then need to define when exactly an environment [E] has the desired
properties relative to a context [G]. That is, [E] should have the same
length as [G] and its elements should be closed recursively halting
values that have the type of the corresponding variable in [G]. We
define this correspondence inductively: *)

Inductive env_typing : env -> ctx -> Prop :=
| ET_empty : env_typing env_empty {}
| ET_extend E G x T v :
  |- v : T -> val v -> rhalts T v -> env_typing E G -> 
  env_typing (env_extend E v) {G, x : T}
.
(** With a slight abuse of notation, we write [|= E : G] to mean that
the terms in [E] ar halting values that have the types of the
corresponding variables in [G]. *)

Notation "|=  E : G" := (env_typing E G) 
  (at level 70, E at next level, no associativity).

(** *** Substitution of an environment in a term

Finally, we need to define what it means to substitute the variables of
a context [G] with the values in an environment [E]. We proceed
recursively, traversing both the environment and the context, and
substituting the variables from right to left.

We have to define the result for the case where the environment and the
context have different lenghts, but since we will only deal with
environments that are well-typed relative to the context, this erroneous
situation will never occur. *)

Fixpoint env_subst G E t :=
  match E, G with
    | env_empty, {}%ctx => t
    | env_extend E' v, {G', x:T}%ctx => env_subst G' E' ([x |-> v]t)%tm
    | _, _ => t (* impossible when [|= E : G] *)
  end.

(** Again, we abuse notation and write [[G |=> E]t] for the result of
substituting every variable of [G] in [t] with the corresponding value
in [E]. *)

Notation "[ G |=> E ] t" := (env_subst G E t) 
  (at level 7, left associativity) : term_scope.


(** *** E-Substitution in a closed term has no effect

We then define some basic properties of environment substitution. These
are mostly direct corollaries of the similar properties of plain single
substitution. *)

Lemma closed_env_subst_nop : forall E G t, 
  closed t  ->  |= E : G  ->  ([G |=> E]t)%tm = t.
Proof with eauto with base_fun.
  intros E G t clo_t E_G.
  induction E_G; simpl...
    rewrite -> closed_subst_nop...
Qed.


(** *** E-substitution distributes over application *)

Lemma env_subst_distr_app : forall E G t t', 
  |= E : G  ->
  ([G |=> E](t $ t'))%tm = ([G |=> E]t $ [G |=> E]t')%tm.
Proof.
  intros E G t t' E_G.
  induction E_G in t, t' |- *; simpl.
    reflexivity.
    
    apply IHE_G.
Qed.

(** *** E-substitution in an abstraction produces an abstraction *)

Lemma fv_env_subst_fv : forall E G t, 
  |= E : G  ->  fv t  ->  fv ([G |=> E]t).
Proof with eauto with base_fun.
  intros E G t E_G fvt.
  destruct fvt as [x T t'].
  induction E_G in t' |- *; simpl...
    destruct (beq_nat x0 x)...
Qed.



(** *** E-substitution preserves typing *)

Lemma env_subst_preservation : forall E G t T, 
  |= E : G           ->
  G |- t : T         ->  
  |- [G |=> E]t : T.
Proof with eauto with base_fun.
  intros E G t T E_G G_t_T.
  induction E_G in t, T, G_t_T |- *; simpl.
    apply G_t_T.

    apply IHE_G.
    eapply subst_preservation.
    apply G_t_T.
    apply H.
Qed.


(** *** Beta reduction extends substitution environment

This result is somewhat specific to our needs, but it is simpler to
prove than prettier, more general-purpose lemmas.

What we want to show here is that when we are evaluating an application
of a lambda abstraction [\x:T, t] to a value [v], and the lambda
abstraction has closed by an [E]-substitution, then the result of the
application is the body [t] of the abstraction, but closed by an
_extended_ substitution, where we add [v] to the environment and
[x:T] to the context.

Intuitively this makes directly sense, because [(\x:T, t) v --> [x |->
v]t]. In practice things are complicated a little by the fact that we
must check if [x] is already in the context or not. *)

Lemma beta_ext_env_subst : forall E G x T t v,
  |= E : G   -> 
  |- v : T   -> 
  val v      ->
  ([G |=> E](\x : T, t)) $ v --> [{G, x : T} |=> env_extend E v]t.
Proof with eauto with base_fun.
  intros E G x T t v E_G v_T val_v.
  induction E_G as [| E' G' x' T' v' v'_T' val_v' rT'v' E'_G' IHE'_G'] 
        in t |- *; simpl.
    Case "E = env_empty, G = {}".
    auto using E_AppAbs.  

    Case "E = env_extend E' v', G = {G', x' : T'}".
    simpl in IHE'_G'.
    assert (Q := beq_decides_eq_nat x' x).
    destruct (beq_nat x' x); simpl in Q.
      SCase "x' = x".
      subst x'.
      rewrite -> subst_idem.
        apply IHE'_G'.

        apply well_typed_is_closed...
 
      SCase "x' <> x".
      rewrite -> subst_exchange.
        apply IHE'_G'.

        apply Q.

        apply well_typed_is_closed...

        apply well_typed_is_closed...
Qed.


(** ** E-Substitution preserves halting (TAPL 12.1.5)

We now get to the main theorem: _every_ term [t] that has the type
[T] in some context [G], will recursively halt when its free variables
are substituted with recursively halting values that respect the types
of [G].

We consider the case where [t] is a variable first, since it does not
require any inductive hypotheses. The variable case is described as
"immediate" in TAPL, but because we do not require all variables to be
distinct (as is done in TAPL), we have to consider a number of cases and
eliminate the impossible ones.

Intuitively, however, the proof is simple: if [x:T] is bound in [G], and
[E] respects the typees of [G], then at some point during the
E-substitution we must replace [x] by some recursively halting value [v]
of type [T]. Since [v] is well-typed, it is closed, and therefore none
of the remaining substitutions in [E] can affect it. *)

Lemma env_subst_var_rhalts : forall E G x T,
  |= E : G       ->
  bound x T G    ->
  rhalts T [G |=> E]'x.
Proof with eauto with base_fun.
  intros E G x T E_G x_T_G.
  induction E_G as [| E' G' x' T' v' v'_T' val_v' rT'v' E'_G' IHE'_G']; simpl.
    Case "E = env_empty, G = {}".
    inversion x_T_G. (* Impossible *)

    Case "E = env_extend E' v', G = {G', x' : T'}".
    assert (Q := beq_decides_eq_nat x' x).
    destruct (beq_nat x' x); simpl in Q.
      SCase "x' = x".
      subst x'.
      inversion x_T_G; subst.
        SSCase "B_Here, T = T', x = x".
        rewrite -> closed_env_subst_nop...

        SSCase "B_Next, x <> x, bound x T G'".
        contradiction H3... 

      SCase "x' <> x".
      apply IHE'_G'.
      inversion x_T_G; subst.
        SSCase "B_Here, T = T', x = x'".
        contradiction Q...

        SSCase "B_Next, x <> x', bound x T G'".
        apply H5.
Qed.
    
(** We then move to the main theorem. The interesting case is [T_Abs],
which requires an innovative use of the induction hypothesis. *)

Lemma env_subst_rhalts : forall E G t T,
  |= E : G              ->
  G |- t : T            ->
  rhalts T [G |=> E]t.
Proof with eauto.
  intros E G t T E_G G_t_T.
  induction G_t_T in E, E_G |- *; simpl.
    Case "T_Var, t = 'x".
    apply env_subst_var_rhalts...

    Case "T_Abs, T = T1 -> T2, t = \x:T1, t2".
    split.
(** We first prove that the result of the substitution halts. We
      use the auxiliary result that the result of the substitution is an
      abstraction, so it is immediately a value and thus a normal form.
      *)
      SSCase "halts ([G |=> E]t)".
      exists ([G |=> E](\x:T1, t2))%tm.
      split.
        SSSCase "t -->* t".
        apply rsc_refl.

        SSSCase "normal_form ([G |=> E]t)".
        apply val_is_normal.
        apply fv_is_val.
        apply fv_env_subst_fv...
        apply fv_abs.
        
(** Here begins the most interesting part of the proof. We have to
    show that given a recursively halting term [s] of type [T1], then
    [[G |=> E]t $ s] is also recursively halting.

    Because the following proof uses practically all of the lemmas we
    have defined previously, and is perhaps hard to decipher, we write
    it unusually in the forward reasoning style, writing out explicitly
    the intermediate results by which the final goal is proven. This is
    more verbose than the standard backward reasoning style of Coq, and
    hopefully easier to follow.

    Notice that we are not using any hint databases: when a tactic ends
    with ellipses ([apply foo...]), it means that the required arguments
    to [foo] can be found from our current assumptions. *)

    intros s sT1 rT1s.
    assert (halts s) as [v [sMv nfv]].
      eapply rhalts_then_halts...
    assert (|- v : T1).
      eapply meval_preservation...
    assert (rhalts T1 v).
      eapply meval_preserves_rhalts...
    assert (val v).
      eapply normal_is_value...
      exists T1...
    pose (G' := {G, x : T1}%ctx).
    pose (E' := env_extend E v).
    assert (|= E' : G').
      apply ET_extend...
    assert (rhalts T2 [G' |=> E']t2).
      apply IHG_t_T...
    assert (([G |=> E](\x : T1, t2) $ s)%tm -->* ([G' |=> E']t2)%tm).
      eapply rsc_trans.
        apply meval_app2_congr.
          apply fv_is_val.
          apply fv_env_subst_fv...
          apply fv_abs.
        apply sMv.
      eapply rsc_step.
        apply beta_ext_env_subst...
      apply rsc_refl.
    assert (rhalts T2 ([G |=> E](\x:T1, t2) $ s)).
      eapply meval_reflects_rhalts...
    assumption.

(** Compared to abstractions, the application case is relatively
       straightforward. *)
    Case "T_App, T = T11 -> T12, t = t1 $ t2".
    rewrite -> env_subst_distr_app...
    assert (rhalts (T11 -> T12) [G |=> E]t1) as [h1 fr1].
      apply IHG_t_T1...
    fold rhalts in fr1. (* just to make the context prettier *)
    apply fr1.
      apply env_subst_preservation...
    apply IHG_t_T2...
Qed.

(** ** Normalization (TAPL 12.1.6) *)

Corollary normalization t T : |- t : T -> halts t.
Proof.
  intros t T t_T.
  eapply rhalts_then_halts.
  apply (env_subst_rhalts env_empty {} t T).
    apply ET_empty.
  assumption.
Qed.



End typed_base_fun.

(** **)