(** * Normalization for cbv System T *)
(* Version of 11/27/2009, based on Pierce TAPL, Chapter 12 *)

(** In this document we consider System T with call-by-value reduction,
 and prove that every (well-typed) term in this system reduces to a value. 
 The proof largely follows the normalization proof given in Chapter 12 of 
 Pierce's "Types and Programming Languages" book, which is recommended 
 reading.

We begin by importing some definitions and facts from the standard library,
 and define a variant of the inversion tactic (that we seen previously). *)

Require Import Arith  Relations.
Ltac sinv h := (inversion h; clear h; subst).  (* a useful tactic *)

(** ** Syntax *)

(** *** Identifiers *)
(** Identifiers are represented by natural numbers, using the wrapper [Id]. 
 Two identifiers are equal if and only if they are represented by the same natural number. *)

Inductive id : Type := 
  Id : nat -> id.
Definition beq_id id1 id2  := 
  match (id1, id2) with (Id n1, Id n2) => beq_nat n1 n2 end.
Hint Unfold beq_id. 

Theorem beq_id_refl : forall i,
  true = beq_id i i.
Proof. 
intros. destruct i. unfold beq_id. apply beq_nat_refl. 
Qed.

Theorem not_eq_false_beq_id : forall i1 i2,
  i1 <> i2 -> false = beq_id i1 i2.
Proof.
intro. destruct i1 as [n1]. 
induction n1; destruct i2 as [n2]; destruct n2; unfold beq_id; intuition.
simpl. rewrite (IHn1 (Id n2)). trivial. intuition. inversion H0. intuition. 
Qed. 

(** *** Types and terms *)
(** The syntax of types and terms are defined as inductive types; 
 values are described by an inductively defined predicate: *)

Inductive ty : Type := 
  | ty_nat : ty 
  | ty_arrow : ty -> ty -> ty.

Inductive tm : Type :=
  | tm_var : id -> tm
  | tm_app : tm -> tm -> tm
  | tm_abs : id -> ty -> tm -> tm
  | tm_zero : tm 
  | tm_succ : tm -> tm
  | tm_pr : tm -> tm -> tm -> tm.

Inductive value : tm -> Prop :=
  | v_abs : forall x T t,  value (tm_abs x T t)
  | v_zero : value(tm_zero)
  | v_succ : forall t, value t -> value (tm_succ t).

Hint Constructors value.


(** ** Environments *)
(** We use a polymorphic type for environments: 
 [env X] is the type of partial functions from identifiers to [X]. 
This has the advantage that we can use [env] to implement both typing contexts 
(as [env ty]) as well as parallel substitutions (as [env tm], see below). *)

Definition env (X:Type) := id -> (option X).

Definition empty (X:Type) : env X := (fun _ => None).

Definition update (X:Type) (Gamma : env X) (n:id) (x:option X) : env X :=
  fun n' => if beq_id n n' then x else Gamma n'.

Implicit Arguments update [X].
Hint Unfold update.

(** The following operation [pointwise] "lifts" a relation [R] between [X] and [Y] 
 to a relation [Pointwise X Y R] between [env X] and [env Y]: two environments 
 are related if they have the same domain and for each argument the respective 
 images are related by [R]. *)

Definition pointwise (X Y :Type) (R :X->Y->Prop) (Gamma :env X) (Delta :env Y) :Prop :=
  forall n, (Gamma n = None -> Delta n = None) 
         /\ (forall x, Gamma n = Some x -> exists y, Delta n = Some y /\ R x y). 

Implicit Arguments pointwise [X Y].
Hint Unfold pointwise. 

(** ** Parallel Substitution *)
(** To state and prove the propositions that lead to the normalization proof for System T 
 it is convenient to phrase the operational semantics in terms of a parallel substitution 
 operation. This operation generalizes our earlier substitution [[x:=s]t] so that we can 
 substitute multiple terms simultaneously, [[x1:=s1 ... xn:=sn]t]. 

 We follow our earlier approach and just state the properties of parallel substitution that
 we need as assumptions, rather than implementing a particular parallel substitution operation. 
 However, to formulate these assumptions in a meaningful way, we restrict substitutions so 
 that [s1,...,sn] in [[x1:=s1 ... xn:=sn]t] are closed terms. (Otherwise, we would need to be much more  
 careful to avoid the possible capture of free variables of the terms [si] by the binders within [t].) *)

(** *** Free variables and closed terms *)
(** The proposition [appears_free_in x t] characterizes those variables [x] that appear free in [t]: *)

Inductive appears_free_in : id -> tm -> Prop :=
  | afi_var : forall x,
      appears_free_in x (tm_var x)
  | afi_app1 : forall x t1 t2,
      appears_free_in x t1 -> appears_free_in x (tm_app t1 t2)
  | afi_app2 : forall x t1 t2,
      appears_free_in x t2 -> appears_free_in x (tm_app t1 t2)
  | afi_abs : forall x y T11 t12,
        y <> x 
     -> appears_free_in x t12
     -> appears_free_in x (tm_abs y T11 t12)
  | afi_succ : forall x t, appears_free_in x t -> appears_free_in x (tm_succ t)
  | afi_pr1 : forall x t1 t2 t3, 
      appears_free_in x t1 -> appears_free_in x (tm_pr t1 t2 t3)
  | afi_pr2 : forall x t1 t2 t3,
      appears_free_in x t2 -> appears_free_in x (tm_pr t1 t2 t3)
  | afi_pr3 : forall x t1 t2 t3,
      appears_free_in x t3 -> appears_free_in x (tm_pr t1 t2 t3). 

(** It is now easy to define when a term [t] is closed, and when a substitution [gamma] 
 substitutes only closed terms which we call (somewhat inaccurately) [closing]: *)

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

Definition closing  (gamma:env tm) := 
  forall x s, gamma x = Some s -> closed s.  

Hint Constructors appears_free_in.
Hint Unfold closed closing. 

(** *** Assumptions about parallel (simultaneous) substitution *)
(** We assume the existence of a parallel (simultaneous) substitution operation [simsubst]: *)
Hypothesis simsubst : env tm -> tm -> tm.

(** and axiomatize its behaviour on terms: *)
Hypothesis subst_var : forall gamma x t, gamma x = Some t -> simsubst gamma (tm_var x) = t. 

Hypothesis subst_var2 : forall gamma x, gamma x = None -> simsubst gamma (tm_var x) = tm_var x. 

Hypothesis subst_abs : forall gamma x T t, closing gamma ->
    simsubst gamma (tm_abs x T t) = tm_abs x T (simsubst (update gamma x None) t). 

Hypothesis subst_app : forall gamma t1 t2, 
    simsubst gamma (tm_app t1 t2) = tm_app (simsubst gamma t1) (simsubst gamma t2).
 
Hypothesis subst_zero : forall gamma, simsubst gamma tm_zero = tm_zero. 

Hypothesis subst_succ : forall gamma t, simsubst gamma (tm_succ t) = tm_succ (simsubst gamma t). 

Hypothesis subst_pr : forall gamma t t1 t2,
    simsubst gamma (tm_pr t t1 t2) = tm_pr (simsubst gamma t) (simsubst gamma t1) (simsubst gamma t2).
 
(** Ordinary substitution is defined as a special case of simultaneous substitution: *)
Definition subst :=fun (x:id) (s:tm) => simsubst (update (empty tm) x (Some s)).  

(** We also assume that successive substitutions can be merged, expressed by the following hypothesis: *)
Hypothesis subst_simsubst : forall (gamma:env tm) x s t, closing gamma ->
      subst x s (simsubst (update gamma x None) t) = simsubst (update gamma x (Some s)) t. 

Hint Resolve subst_var subst_var2 subst_abs subst_app subst_zero subst_succ subst_pr. 
Hint Resolve subst_simsubst. 

(** As a first sanity check for our definitions and the assumptions we made so far, we prove that 
 applying the empty substitution to a term [t] does not change [t]. *)

Proposition subst_id : forall t, simsubst (empty tm) t = t.
Proof with eauto. 
assert (forall t gamma, (forall x, gamma x = None) -> simsubst gamma t = t)...
induction t; intros...
(* Case tm_app *) rewrite subst_app. rewrite IHt1. rewrite IHt2... trivial. 
(* Case tm_abs *) rewrite subst_abs. rewrite IHt... 
  intro x. unfold update. destruct (beq_id i x)...  
  intros x t1 H1. rewrite H in H1. inversion H1...
(* Case tm_succ *) rewrite subst_succ. rewrite IHt...
(* Case tm_pr *) rewrite subst_pr. rewrite IHt1... rewrite IHt2... rewrite IHt3... 
Qed. 
Hint Resolve subst_id.   

(** ** Reduction Relation *)

(** The reduction relation is the one we have seen previously: *)
Inductive step : tm -> tm -> Prop :=
  | ST_AppAbs : forall x T t12 v2,
         value v2
      -> step (tm_app (tm_abs x T t12) v2) (subst x v2 t12)
  | ST_App1 : forall t1 t1' t2,
         step t1 t1'
      -> step (tm_app t1 t2) (tm_app t1' t2)
  | ST_App2 : forall v1 t2 t2',
         value v1
      -> step t2 t2'
      -> step (tm_app v1 t2) (tm_app v1 t2')
  | ST_Succ : forall t t',
         step t t'
      -> step (tm_succ t) (tm_succ t')
  | ST_Pr : forall t t' t1 t2,
         step t t'
      -> step (tm_pr t t1 t2) (tm_pr t' t1 t2)
  | ST_PrZero : forall t1 t2,
         step (tm_pr tm_zero t1 t2) t1
  | ST_PrSucc : forall v t1 t2,
         value v
      -> step (tm_pr (tm_succ v) t1 t2) (tm_app (tm_app t2 v) (tm_pr v t1 t2)). 

(** We can introduce some nice notation for the single step relation and its reflexive transitive
 closure. To define the latter, we use the operation [clos_refl_trans] that is defined in the Coq library. *)

Notation "t1 '~~>' t2" := (step t1 t2) (at level 40).
Notation stepmany := (clos_refl_trans tm step).
Notation "t1 '~~>*' t2" := (stepmany t1 t2) (at level 40).
Hint Constructors step.

Lemma step_in_stepmany: forall t1 t2, t1~~>t2 -> t1~~>*t2.
Proof. intros. apply rt_step. trivial. Qed. 

Hint Resolve step_in_stepmany. 

(** A useful observation is that values are irreducible (have no successor). *)
Definition irred (t:tm) := forall t', t ~~> t' -> False. 
Hint Unfold irred. 

Lemma value_irred : forall v, value v -> irred v. 
Proof with eauto. intros. induction H... 
(* Case tm_abs *) intros t' H. sinv H.
(* Case tm_zero *) intros t' H. sinv H.  
(* Case tm_succ *) intros t' H1. sinv H1. apply IHvalue in H2. sinv H2.     
Qed.     

(** *** Reductions in (some particular) reduction contexts *)
(** In the normalization proof we sometimes need to construct new reduction sequences
 from given ones. Usually these new reductions will simulate the given ones in a reduction context. 
 To realize these constructions without too much repetition of proofs, it is useful to abstract 
 slightly and consider a notion of compatible relation. (In fact, we have seen this already in
 the coincidence proof for PCF when we showed the agreement between the small-step reduction 
 semantics and the evaluation relation.) *) 

Definition compat (A:Type) (R:relation A) f := forall t t', R t t' -> R (f t) (f t').
Hint Unfold compat. 

Lemma compatLifting: forall A R f,
  compat A R f -> compat A (clos_refl_trans A R) f.
Proof with eauto. 
unfold compat. intros. induction H0.  
apply rt_step. apply H... 
apply rt_refl.  
eapply rt_trans... 
Qed.

(** We then instantiate this definition to three particular cases: reductions of function arguments, 
 reductions below [S], and reductions of the first argument of primitive recursions. *)

Lemma compat_App2: forall v, value v -> compat tm stepmany (tm_app v). 
Proof with eauto. intros. apply compatLifting... Qed. 

Lemma compat_Succ: compat tm stepmany tm_succ. 
Proof with eauto. intros. apply compatLifting... Qed.

Lemma compat_Pr1: forall t1 t2, compat tm stepmany (fun t => tm_pr t t1 t2). 
Proof with eauto. intros. apply compatLifting... Qed. 

Hint Resolve compat_App2 compat_Succ compat_Pr1. 

  
(**  ** Typing *)
(** The inductive definition of the typing relation is straightforward: *)
Inductive has_type : env ty -> tm -> ty -> Prop :=
  | T_Var : forall Gamma x T,
      Gamma x = Some T ->
      has_type Gamma (tm_var x) T
  | T_Abs : forall Gamma x T11 T12 t12,
      has_type (update Gamma x (Some T11)) t12 T12 -> 
      has_type Gamma (tm_abs x T11 t12) (ty_arrow T11 T12)
  | T_App : forall T1 T2 Gamma t1 t2,
      has_type Gamma t1 (ty_arrow T1 T2) -> 
      has_type Gamma t2 T1 -> 
      has_type Gamma (tm_app t1 t2) T2
  | T_Zero : forall Gamma, has_type Gamma tm_zero ty_nat
  | T_Succ : forall Gamma t, 
      has_type Gamma t ty_nat -> 
      has_type Gamma (tm_succ t) ty_nat
  | T_PR : forall Gamma t t1 t2 T,
      has_type Gamma t ty_nat ->
      has_type Gamma t1 T -> 
      has_type Gamma t2 (ty_arrow ty_nat (ty_arrow T T)) -> 
      has_type Gamma (tm_pr t t1 t2) T.

Hint Constructors has_type.

(** A simple observation that relates the typing relation and the notion of free variables 
 of a term is given next.  *)
Lemma free_in_context : forall x t T Gamma,
   appears_free_in x t ->
   has_type Gamma t T ->
   exists T', Gamma x = Some T'.
Proof with eauto.
intros. generalize dependent Gamma. generalize dependent T.
induction H; intros; try solve [sinv H0; eauto]. 
(* Case afi_abs *) 
sinv H1. apply IHappears_free_in in H7. 
unfold update in H7. apply not_eq_false_beq_id in H. rewrite <- H in H7...
Qed. 

(** *** Type preservation *)
(** We assume a substitution lemma. This lemma takes a more general form than the one
 we have seen earlier for PCF - the reason is that we need to adapt it to the parallel
 substitutions that we are using now. *)

Hypothesis substitution_lemma : forall Gamma t T gamma Gamma', 
  has_type Gamma t T ->  
  pointwise (fun T t => has_type Gamma' t T) Gamma gamma -> 
  has_type Gamma' (simsubst gamma t) T.

(** With the help of this substitution lemma, it is not too difficult to prove the type 
 preservation theorem for System T: *)

Theorem preservation: forall t t' T, 
  has_type (empty ty) t T -> t ~~> t' -> has_type (empty ty) t' T. 
Proof with eauto.
assert (forall Gamma t t' T, (forall x, Gamma x = None) ->  
  has_type Gamma t T -> t ~~> t' -> has_type Gamma t' T). 
intros Gamma t t' T H0 H. generalize t'; clear t'...
induction H; intros t' HR; sinv HR...
(* Case ST_AppAbs *) apply substitution_lemma with (Gamma:=update Gamma x (Some T1)). 
  sinv H...
  intro n. unfold update. remember (beq_id x n) as b. destruct b. intuition.
  sinv H4. sinv H4. exists t2. split... sinv H...
  intuition. rewrite H0 in H3. sinv H3. 
(* Case ST_PrSucc *) eapply T_App... eapply T_App... sinv H... 
  eapply T_PR... sinv H...
intros. eapply H...  
Qed. 

Corollary preservation_stepmany: forall t t' T,
  has_type (empty ty) t T -> t ~~>* t' -> has_type (empty ty) t' T. 
Proof with eauto.
intros. induction H0... eapply preservation... 
Qed. 
  
Hint Resolve preservation preservation_stepmany.


(** ** The Logical  Relation [R] *)
(** The property that we are interested in eventually is that every typable term 
 reduces to a value: *)

Definition halts t := exists v, t ~~>* v /\ value v.

Hint Unfold halts.

(** However, this property turns out to be "too weak" to be established directly by an 
 inductive proof. To get a sufficiently strong induction hypothesis, we consider the following 
 type-indexed family of predicates, the "logical" relation [R]: *) 

Fixpoint R (T:ty) (t:tm) {struct T} : Prop := has_type (empty ty) t T /\
  match T with 
  | ty_nat  => halts t
  | ty_arrow T1 T2 => halts t /\ (forall s, R T1 s -> R T2 (tm_app t s))
  end.

(** This family is defined recursively on the type [T]: 
 - [R ty_nat] is simply [halts], i.e., the property we're interested in, and 
 - [R (ty_arrow T1 T2)] additionally expresses that application preserves the property of being 
in the relation. Accordingly [R (ty_arrow T1 T2)] it is defined in terms of [R T1] and [R T2]. 

The relation can be extended to substitutions straightforwardly, using the [pointwise] operation, as 
[pointwise R Gamma]. 

Note that it is not possible to define [R] using [Inductive]: the reason is that in the right hand 
side of the case [R (ty_arrow T1 T2)] the relation [R] appears in a "negative" position (to the left of 
an implication), which conflicts with the "monotonicity" requirement that Coq enforces for inductive
definitions. 

From the definition it is clear that [R T] consists of closed terms of type [T]: *) 
  
Lemma R_typed : forall T t,
  R T t -> has_type (empty ty) t T. 
Proof. 
intros. destruct T; simpl R in H; intuition.
Qed.   

Lemma ptR_typed : forall Gamma gamma, 
  pointwise R Gamma gamma -> 
  pointwise (fun T t => has_type (empty ty) t T) Gamma gamma.
Proof with eauto. 
unfold pointwise. intros. destruct (H n). destruct (Gamma n).
intuition. sinv H2. destruct (H1 x) as [y]... eexists. intuition... eapply R_typed...   
intuition. inversion H0. 
Qed. 

(** It is also immediate from the definition that [R] implies normalization: *)

Lemma (* 12.1.3 *) R_halts : forall T t, 
  R T t -> halts t. 
Proof.    
intros. destruct T; simpl R in H; intuition.
Qed.


(** *** Closure properties of [R] *)
(** For the normalization proof we need two closure properties of the logical relation:
       - closure under reduction
       - closure under expansion

      To establish these, we must in particular prove that the predicate [halts] is closed 
      under both reduction and expansion. In turn, to prove the former, we first show that 
      the reduction relation is deterministic: *)
 
Lemma determinacy : forall t t1 t2, 
  t ~~> t1 -> t ~~> t2 -> t1=t2. 
Proof with eauto.
intros t t1 t2 H1. generalize t2; clear t2. 
induction H1; intros t3 H2; sinv H2; try solve [f_equal; eauto]... 
sinv H4.
apply value_irred in H5... sinv H5. 
sinv H1. 
apply value_irred in H1... sinv H1. 
apply value_irred in H1... sinv H1.     
apply value_irred in H5... sinv H5. 
sinv H1.  
apply value_irred in H1... sinv H1. 
sinv H4.
apply value_irred in H5... sinv H5. 
Qed.

Lemma halts_step_closed : forall t t',  
  halts t -> t ~~> t' -> halts t'. 
Proof with eauto. 
intros t t' H Htt'. destruct H as [v].
exists v. intuition. apply trans_rt1n in H0. sinv H0. 
eapply value_irred in Htt'... inversion Htt'.
eapply determinacy in Htt'... subst.  apply rt1n_trans... 
Qed. 

Lemma halts_exp_closed : forall t t', 
  halts t' -> t ~~> t' -> halts t. 
Proof with eauto. 
intros. destruct H as [v]. exists v. intuition. eapply rt_trans... 
Qed.  

(** We prove that each [R T] is closed under reduction by induction on [T]. *)   

Lemma (* 12.1.4a *) R_step_closed : forall T t t', 
  t ~~> t' -> R T t -> R T t'. 
Proof with eauto. 
intros T. induction T; intros t t' H1 H2; simpl in *|-*; intuition... 
eapply halts_step_closed...
eapply halts_step_closed...
Qed.

Lemma (* 12.1.4b *) R_stepmany_closed : forall T t t', 
  t ~~>* t' -> R T t -> R T t'. 
Proof with eauto. 
intros. induction H... 
eapply R_step_closed...
Qed.

(** Similarly, we prove that each [R T] is closed under expansion by induction on [T]. 
 Since this requires that both terms are of type [T], we must add an additional assumption (why?). *)   

Lemma (* 12.1.4c *) R_exp_closed : forall T t t', has_type (empty ty) t T -> 
  t ~~> t' -> R T t' -> R T t. 
Proof with eauto. 
intros T. induction T; intros t t' H H1 H2; simpl in *|-*; intuition... 
eapply halts_exp_closed...
eapply halts_exp_closed... 
eapply IHT2... apply R_typed in H3...
Qed.

Lemma (* 12.1.4d *) R_expmany_closed: forall T t t', has_type (empty ty) t T -> 
  t ~~>* t' -> R T t' -> R T t. 
Proof with eauto.
intros. induction H0... 
eapply R_exp_closed...
Qed.   

(** ** Preservation properties for  [R] *)
(** We can now prove that [R] is preserved by all the typing rules of System T. 
 We begin with the case of abstraction: *)
Lemma BL_Abs : forall x T t T', has_type (empty ty) (tm_abs x T t) (ty_arrow T T') -> 
  (forall s, R T s -> R T' (subst x s t)) -> R (ty_arrow T T') (tm_abs x T t). 
Proof with eauto. 
intros. simpl. intuition... 
eexists; intuition. 
assert (A: R T s)... eapply R_halts in A... destruct A as [v [H2 H3]].
assert (B: R T v). eapply R_stepmany_closed...
eapply R_expmany_closed with (t':= tm_app (tm_abs x T t) v)...
eapply T_App... eapply R_typed...
eapply  compat_App2...
eapply R_exp_closed... eapply T_App... eapply R_typed...
Qed. 
   
(** This was the most difficult case, because the function body [t] will in general have an 
 [x] as an additional free variable. The cases of the remaining preservation lemmas reflect the
 respective typing rules even more directly. They are also easier to prove, essentially
 because the free variables of the direct subterms are the same as those of the term itself: *)

Lemma BL_App : forall t1 t2 T T', 
  R (ty_arrow T T')  t1 -> R T t2 -> R T' (tm_app t1 t2).
Proof with eauto. 
intros. simpl in H. intuition. 
Qed.

Lemma BL_Zero : R ty_nat tm_zero.
Proof with eauto.  
Admitted.

Lemma BL_Succ : forall t, 
  R ty_nat t -> R ty_nat (tm_succ t). 
Proof with eauto. 
Admitted. 

Lemma BL_PR : forall t t1 t2 T, 
  R ty_nat t -> R T t1 -> R (ty_arrow ty_nat (ty_arrow T T)) t2 -> R T (tm_pr t t1 t2). 
Proof with eauto.
intros t t1 t2 T H.  
assert(A: has_type (empty ty) t ty_nat). eapply R_typed...
intros. destruct H as [H2 [v [H3]]]. 
eapply preservation_stepmany in A...
eapply R_expmany_closed with (t':=tm_pr v t1 t2)...
eapply T_PR... eapply R_typed... eapply R_typed... eapply compat_Pr1...
clear H2 H3 t.   
induction H; intros. sinv A. 
(* Case tm_zero *) 
eapply R_exp_closed... apply T_PR... eapply R_typed... eapply R_typed...
(* Case tm_succ *)
assert(B: R ty_nat t). split... sinv A... exists t. intuition.  
eapply R_exp_closed... 
apply T_PR... eapply R_typed... eapply R_typed...
eapply BL_App... eapply BL_App... apply IHvalue. eapply R_typed... 
Qed.

(** ** Basic lemma for the logical relation *)
(** We prove that typable terms of type [T] are in the relation [R T]. For the induction to
 go through this needs to be generalized to open terms (in context [Gamma]) and 
 substitutions (that are in  [pointwise R Gamma]). We also need to know that we can modify 
 substitutions, by updating with terms that are in [R]: *)

Lemma R_preserving_context_update: forall Gamma gamma T x t,
  pointwise R Gamma gamma -> 
   R T t -> 
  pointwise R (update Gamma x (Some T)) (update gamma x (Some t)). 
Proof with eauto.
  unfold pointwise. unfold update. intros Gamma gamma T x t H0 H1 n. 
  set (b := beq_id x n). destruct b...
  intuition. inversion H. exists t. sinv H... 
Qed.

(* ** Recall that the axiomatization of the parallel substitution depends on the substitution being
 "closing", i.e., to substitute only closed terms. To ensure that the equations are applicable, we prove 
 that all [gamma] such that [pointwise R Gamma gamma] are closing. *)

Lemma ptR_implies_closing: forall gamma Gamma,
  pointwise R Gamma gamma -> closing gamma.
Proof with eauto.
unfold closing. unfold closed. intros. intro C. 
unfold pointwise in H. destruct (H x)... destruct (Gamma x).
destruct (H2 t)... destruct H3. rewrite H3 in H0. sinv H0. 
eapply R_typed in H4. eapply free_in_context in H4... 
destruct H4. unfold empty in H0. sinv H0. 
intuition. rewrite H0 in H3. sinv H3. 
Qed. 

(** Now we can prove the so-called "basic lemma" for the relation [R]. 
 Its proof is pretty straightforward - 
 all the hard work has been done in the above preservation lemmas. More precisely, in each 
 of the inductive cases we apply the appropriate preservation lemma. There are only two 
 exceptional cases: First, 
 the case of a variable follows from  the assumptions on the substitution gamma. Second, the 
 case of an abstraction which requires some preliminary work before the preservation lemma 
 can be applied. 

 Since the relation [R T] is restricted to well-typed terms of type T, this property must be 
 established when proving the basic lemma. To this end  the following 
 consequence of the assumed substitution lemma is used. *)

Lemma Gamma_closing : forall Gamma t T gamma, 
  has_type Gamma t T -> pointwise R Gamma gamma -> has_type (empty ty) (simsubst gamma t) T.
Proof with eauto. 
  intros. apply ptR_typed in H0. eapply substitution_lemma...
Qed. 

Lemma (* 12.1.5 *) Basic_lemma : forall Gamma t T gamma, 
  has_type Gamma t T -> pointwise R Gamma gamma -> R T (simsubst gamma t). 
Proof with eauto. 
intros Gamma t T gamma H. generalize gamma; clear gamma. induction H; intros. 
(* Case T_Var *)
apply H0 in H. destruct H. destruct H. erewrite subst_var...
(* Case T_Abs *)
assert (A: closing gamma). eapply ptR_implies_closing...
assert (B: has_type (empty ty) (tm_abs x T11 (simsubst (update gamma x None) t12)) (ty_arrow T11 T12)).
  apply T_Abs in H. rewrite <-subst_abs... eapply Gamma_closing...
assert (C: forall s, R T11 s -> R T12 (subst x s (simsubst (update gamma x None) t12))).
  intros. rewrite subst_simsubst... eapply IHhas_type. eapply R_preserving_context_update...  
rewrite subst_abs... eapply BL_Abs... 
(* Case T_App *)
rewrite subst_app. eapply BL_App...
(* Case T_Zero *) 
rewrite subst_zero. eapply BL_Zero...
(* Case T_Succ *) 
rewrite subst_succ. eapply BL_Succ...
(* Case T_Pr *) 
rewrite subst_pr. eapply BL_PR...        
Qed.  

(** ** Normalization *)
(** Finally it is a fairly simple matter of connecting all the pieces and conclude normalization. 
 This is left as an exercise. (Hint: Use [R_halts] and [Basic_lemma]. The lemma 
 [subst_id] may also be useful.) *)

Theorem (* 12.1.6 *) normalization: forall t T, 
  has_type (empty ty) t T -> halts t.
Proof with eauto. 
Admitted.