(* -*- coq-prog-args: ("-emacs-U" "-impredicative-set" "-debug"); compile-command: ". ../env.sh && ./make.sh" -*- *)
(** printing --> $\rightarrow$ *)(** printing G $\Gamma$ *)(** printing G' $\Gamma'$ *)(** printing G'' $\Gamma''$ *)(** printing D $\Delta$ *)(** printing D' $\Delta'$ *)(** printing L $\Lambda$ *)(** printing tau $\tau$ *)(** printing tau' $\tau'$ *)
(** printing empty $[~\!]$ *)(** printing ++ $\mathbin{+\!\!\!+}$ *)(** printing :, $,$ *)
(* begin hide *)
Require Import Coq.Program.Program.
Require Import Omega.
(* end hide *)

(** 
   We will develop a complete formalization of simply-typed lambda-calculus with constants in Coq, 
   using the Program extension to write dependently-typed programs on inductive families.
   The development uses a pure de Bruijn encoding and dependently-typed abstract syntax.
   It includes the theory of lifting and substitution, a denotational semantics given by interpreting
   terms directly into Coq, and finally a proof of weak normalization for the call-by name strategy.

   This paper describes all the technical parts of the development. It is a literate coqdoc script, 
   missing only the proof scripts.

   First we define a set of tactics that will be used later. *)

(** Rewrite using uniqueness of indentity proofs [H = refl_equal X]. *)

Ltac simpl_uip :=
  match goal with
    [ H : ?X = ?X |- _ ] => rewrite (UIP_refl _ _ H) in *; clear H
  end.

(* begin hide *)

Ltac simpl_eq := simpl ; repeat (elim_eq_rect ; simpl) ; repeat (simpl_uip ; simpl).
(* end hide *)

(** Try to abstract a proof of equality, if no proof of the same equality is present in the context. *)

Ltac abstract_eq_hyp H' p := 
  match type of p with
    ?X = ?Y => 
    match goal with 
      | [ H : X = Y |- _ ] => fail 1
      | _ => set (H':=p) ; try (change p with H') ; clearbody H'
    end
  end.

(** Apply the tactic tac to proofs of equality appearing as coercion arguments. *)

Ltac on_coerce_proof tac :=
  match goal with
    [ |- ?T ] =>
    match T with
      | context [ eq_rect _ _ _ _ ?p ] => tac p
    end
  end.

(** Abstract proofs of equalities of coercions. *)

Ltac abstract_eq_proof := on_coerce_proof ltac:(fun p => let H := fresh "eqH" in abstract_eq_hyp H p).
  
(** Factorize proofs, by using proof irrelevance so that two proofs of the same equality 
   in the goal become convertible. *)

Ltac pi_eq_proof_hyp p :=
  match type of p with
    ?X = ?Y => 
    match goal with 
      | [ H : X = Y |- _ ] => 
        match p with
          | H => fail 2
          | _ => rewrite (proof_irrelevance (X = Y) p H)
        end
      | _ => fail " No hypothesis with same type "
    end
  end.

(** Factorize proofs of equality appearing as coercion arguments. *)

Ltac pi_eq_proof := on_coerce_proof pi_eq_proof_hyp.

(** Clear unused reflexivity proofs. *)

Ltac clear_refl_eq := 
  match goal with [ H : ?X = ?X |- _ ] => clear H end.
Ltac clear_refl_eqs := repeat clear_refl_eq.

(** Clear unused equality proofs. *)

Ltac clear_eq := 
  match goal with [ H : _ = _ |- _ ] => clear H end.
Ltac clear_eqs := repeat clear_eq.

(** Everything is done in implicit arguments mode. *)

Set Implicit Arguments.

(** * Constants

   The development is parameterized by module implementing the constants and their typing. *)

Module Type Constants.

  (** The set of constant types. *)

  Parameter constant_types : Set.

  (** The constants themselves. *)

  Parameter constants : Set.

  (** A typing function for constants. *) 

  Parameter type_constant : constants -> constant_types.

End Constants.

(** * The implementation.

   The functor [L] implements typing, denotational semantics and normalization of simply-typed
   lambda-calculus plus constants [C]. *)

Module L (C : Constants).
  Import C.
  
  (** ** Abstract syntax *)

  (** The types are just atoms or the arrow. *)

  Inductive type : Set :=
  | type_cst : constant_types -> type
  | type_arrow : type -> type -> type.

  Coercion type_cst : constant_types >-> type.
  Infix " --> " := type_arrow (at level 20).

  (** A context is either empty or a context and a variable. 
     Contexts are effectively snoc-lists, hence the new inductive. *)

  Inductive ctx : Set := 
  | empty : ctx 
  | comma : ctx -> type -> ctx.
  
  Infix ":," := comma (at level 40, left associativity).

  (** Appending one context to another, by induction on the second one. *)

  Fixpoint append (G D : ctx) { struct D } : ctx :=
    match D with 
      | empty => G
      | D' :, x => (append G D') :, x
    end.
  
  Hint Unfold append.

  Infix ";" := append (right associativity, at level 60).
    
  (** Due to the way append is defined, these two are not convertible. *)

  Lemma app_empty : forall G, (empty ; G) = G.
  Proof.
    induction G ; simpl ; auto.
    rewrite IHG.
    reflexivity.
  Defined.
  
  (** Associativity of context appending. *)

  Lemma app_assoc : forall G D L, G ; D ; L = (G ; D) ; L.
  Proof.
    induction L ; simpl ; auto.
    rewrite IHL.
    reflexivity.
  Defined.

  Hint Rewrite app_empty app_assoc : app.
  Opaque app_assoc.
  
  (** Simplification tactic using the previous lemmas. *)

  Ltac my_simpl := program_simpl ; try simpl_JMeq ; autorewrite with app ; program_simpl.

  (** Variables are encoded as typed de Bruijn indices. *)

  Inductive var : ctx -> type -> Set :=
  | first : forall G T, var (G :, T) T
  | next : forall G T, var G T -> forall U, var (G :, U) T.

  (** The AST of well-typed terms. 
     Constants get their type from the [type_constant] function.
     A [rel] just embeds a variable. The abstraction constructor
     [lam] contains a body typed in an extended environment.
     Application applies only functions to objects having their domain type.
     *)

  Inductive term (G : ctx) : type -> Set :=
  | cst : forall c : constants, term G (type_constant c)
  | rel : forall T, var G T -> term G T
  | lam : forall (T T' : type), 
    term (G :, T) T' -> term G (T --> T')
  | app : forall T T' : type,
    term G (T --> T') -> term G T -> term G T'.
  
  (** The really dependent scheme for term. Not used in the development but may be useful. *)

  Scheme term_dep := Induction for term Sort Prop.
  
  (** Tactic to automatically invert contradictory hypotheses. *)

  Ltac try_inversion := 
    match goal with 
      | H : _ = _ |- _ => inversion H ; auto
      | H : var empty _ |- _ => inversion H
    end.

  (** Use these for solving obligations from now on. *)

  Obligations Tactic := my_simpl ; try try_inversion ; try omega.

  (** ** Dealing with coercions and equality. *)

  (** The next two functions reindex variables and terms in [G] to a new context [G']
     with respect to an equality between [G] and [G']. These are dynamic coercions in the sense
     that they can be reduced when applied to a constructed term, contrary to the 
     substitution principle [eq_rect]. *)

  Program Fixpoint coerce_var_context G T (v : var G T) G' (H : G = G')
    { struct v } : var G' T :=
    match G' with
      | empty => !
      | G'' :, V' =>
        match v with
          | first vG vT => first G'' V'
          | next v'G v'T v' V => 
            @next G'' v'T (coerce_var_context v' _) V'
        end
    end.
  
  Program Fixpoint coerce_term_context G T (t : term G T) G' (H : G = G') 
    { struct t } : term G' T :=
    match t with
      | cst c => cst G' c
      | rel T v => rel (coerce_var_context v H)
      | lam tau tau' b => @lam G' _ _ (@coerce_term_context (G :, tau) tau' b (G' :, tau) _)
      | app tau tau' f e => @app G' tau tau' (coerce_term_context f H)
        (coerce_term_context e H)
    end.

  (** Like [eq_rect], coerce reduces to the identity when [G] and [G'] are convertible. *)

  Lemma coerce_var_context_id : forall (G : ctx) T (v : var G T), 
    coerce_var_context v (refl_equal G) = v.
  Proof.
    intros.
    induction v ; simpl ; try elim_eq_rect ; simpl ; auto.
    
    elim_eq_rect ; simpl ; auto.
    
    elim_eq_rect ; simpl ; auto.
    f_equal.
    
    rewrite <- IHv.
    f_equal ; auto.
    apply proof_irrelevance.
  Qed.
  
  Lemma coerce_term_context_id : forall (G : ctx) T (t : term G T), 
    coerce_term_context t (refl_equal G) = t.
  Proof.
    intros.
    induction t ; simpl ; try elim_eq_rect ; simpl ; auto.
    
    f_equal ; apply coerce_var_context_id.
    
    f_equal.
    pattern t at 5.
    rewrite <- IHt.
    f_equal ; apply proof_irrelevance.
    
    f_equal ; eauto.
  Qed.
  
  (** We now define some tactics that help to deal with coercions. They work in multiple
     passes. First, we abstract any equality proof appearing in the goal as an argument of
     a coercion, so as not to polute it with irrelevant proof terms. Then we factorize the proofs 
     and normalize the term using proof irrelevance so that two references to the same equality proof
     are the same. Next we try to simplify the equations using Streicher's axiom K
     (a proof [p] of [x = x] can be substituted by [refl_equal x]). Finally we try to rewrite the term
     using the previous lemmas about [coerce] and [refl_equal]. This procedure is very effective, 
     most of the coercions can be eliminated this way. We get stuck only when an induction is needed. *)

  (** Abstract a proof of equality, if none is already present in the context. *)

  Ltac on_coerce_proof tac :=
    match goal with
      [ |- ?T ] =>
      match T with
        | context [ coerce_var_context _ ?p ] => 
          tac p
        | context [ coerce_term_context _ ?p ] => 
          tac p
        | context [ eq_rect _ _ _ _ ?p ] => 
          tac p
      end
    end.

  Ltac abstract_coerce_proof := on_coerce_proof 
    ltac:(fun p =>
      let H := fresh "coerceH" in
        abstract_eq_hyp H p).

  Ltac abstract_coerce_proofs := repeat abstract_coerce_proof.

  (** Use proof-irrelevance to eliminate remaining non-abstracted proofs. *)

  Ltac pi_coerce_proof := on_coerce_proof ltac:(pi_eq_proof_hyp).

  Ltac pi_coerce_proofs := repeat pi_coerce_proof.

  (** The two preceding tactics in sequence. *)
  Ltac clear_coerce_proofs :=
    abstract_coerce_proofs ; pi_coerce_proofs.

  (** Rewrite [coerce_* t (refl_equal _)] to [t]. *)

  Hint Rewrite coerce_term_context_id coerce_var_context_id : coerce_id.

  Ltac rewrite_coerce_id := autorewrite with coerce_id.
  
  (** Clear the context and term of equality proofs. *)

  Ltac clear_coerce_ctx :=
    rewrite_coerce_id ; clear_coerce_proofs.
  
  (** Reapeated elimination of [eq_rect] applications. 
     Abstracting equalities makes it run much faster than an naive implementation. *)

  Ltac simpl_eqs := 
    repeat (elim_eq_rect ; simpl ; clear_coerce_ctx).

  (** Combine all the tactics to simplify goals containing coercions. *)

  Ltac simpl_term := 
    simpl ; simpl_eqs ; clear_coerce_ctx ; clear_refl_eqs ;  
      try subst ; simpl ; repeat simpl_uip ; rewrite_coerce_id.

  (** In fact [eq_rect] and [coerce] are always equal, so we can switch between 
     frozen and dynamic coercions at will. *)

  Lemma eq_rect_coerce : forall G T (t : term G T) G' (Heq: G = G'), 
    eq_rect _ (fun G' => term G' T) t _ Heq = coerce_term_context t Heq.
  Proof.
    induction t ; simpl ; intros ; simpl_term ; reflexivity.
  Qed.
  
  Lemma eq_rect_coerce_var : forall G T (t : var G T) G' (Heq: G = G'), 
    eq_rect _ (fun G' => var G' T) t _ Heq = coerce_var_context t Heq.
  Proof.
    induction t ; simpl ; intros ; simpl_term ; reflexivity.
  Qed.

  (** Tactic to change [eq_rect] applications to coercions. 
     Allows to reduce coercions sometimes. *)
  
  Hint Rewrite eq_rect_coerce eq_rect_coerce_var : eq_rect_coerce.

  Ltac rew_eq_coerce := autorewrite with eq_rect_coerce.

  (** * Lifting and substitution.

     We now define lifting and substitution of terms. The specifications of the functions are exactly
     the lemmas you would expect. *)

  Section Substitution.
    
    (** Lifting a variable [t] in context [G ; D] by [U] to get a variable in [G :, U ; D]. 
       The context [D] represents the bindings we must avoid to capture.
       *)

    Program Fixpoint lift_var (G D : ctx) (T : type) (t : var (G ; D) T) 
      (U : type) {struct t} : var (G :, U ; D) T :=
      match D with
        | empty => next t U
        | D' :, _ => 
          match t with
            | first G' _ => first (G :, U ; D') T
            | next G' T' v V' => next (lift_var G D' v U) V'
          end
      end.

    (** We prove the defining equations as lemmas. *)

    Lemma lift_var_empty : forall G T U (v : var G T), lift_var G empty v U = next v U.
    Proof.
      intros ; simpl_eq.
      destruct v ; simpl_eq ; reflexivity.
    Qed.

    (** Lifting a term by a type [U] is just a fold. *)

    Program Fixpoint lift_rec G D T (t : term (G ; D) T) U
      {struct t}: term (G :, U ; D) T :=
      match t with
        | cst c => cst _ c
        | rel T v => rel (lift_var G D v U)
        | lam tau tau' b => lam (lift_rec G (D :, tau) b U)
        | app tau tau' f e => app (lift_rec G D f U) (lift_rec G D e U)
      end.

    (** The non recursive version, a.k.a. weakening. *)

    Program Definition lift (G : ctx) T (t : term G T) U : term (G :, U) T := 
      lift_rec G empty t U.
    
    (** The defining equations for the variable case. *)

    Lemma lift_rec_empty : forall G T U (v : var G T),
      lift_rec G empty (rel v) U = rel (next v U).
    Proof.
      intros ; simpl_eq.
      f_equal.
      destruct v ; simpl_eq ; reflexivity.
    Qed.

    Lemma lift_rec_comma_first : forall G T U D,
      lift_rec G (D :, T) (rel (first (G ; D) T)) U = rel (first (G :, U ; D) T).
    Proof.
      intros ; simpl_eq ; reflexivity.
    Qed.

    Lemma lift_rec_comma_next : forall G T U D T' (v : var (G ; D) T'),
      lift_rec G (D :, T) (rel (next v T)) U = rel (next (lift_var _ _ v U) T).
    Proof.
      intros ; simpl_eq ; reflexivity.
    Qed.

    (** Lifting by a context is lifting by each variable in turn. *)

    Program Fixpoint lift_ctx (G D : ctx) T (t : term G T)
      { struct D } : term (G ; D) T := 
      match D with
        | empty => t
        | D' :, U => let t' := lift_ctx D' t in 
          lift t' U
      end.

    (** Substitution of a variable by a term in context [G], under a context [D]. *)

    Program Fixpoint subst_var_rec G D T U (t : var (G :, T ; D) U)
      (s : term G T) { struct D } : term (G ; D) U :=
      match D with
        | empty => 
          match t with
            | first tG tT => s (** substitution takes place *)
            | next tG' tT' tv _ => 
              rel tv (** unlift the var to account for subtitution *)
          end
        | D' :, V => 
          match t with 
            | first tG tT => rel (first (G ; D') V) (** do nothing *)
            | next tG' tT' tv V => (** substitute inside, then lift by one *)
              lift (@subst_var_rec G D' T U tv s) V 
          end
      end.

    (** The defining equations. *)

    Lemma subst_var_rec_empty_first : forall G T (s : term G T), 
      subst_var_rec empty (first G T) s = s.
    Proof.
      intros ; simpl_term ; auto.
    Qed.

    Lemma subst_var_rec_empty_next : forall G T (v : var G T) T' (s : term G T'), 
      subst_var_rec empty (next v T') s = rel v.
    Proof.
      intros ; simpl_term ; auto.
    Qed.
    
    Lemma subst_var_rec_comma_first : forall G T T' (t : term G T') D, 
      subst_var_rec (D :, T) (first (G :, T' ; D) T) t = rel (first (G ; D) T).
    Proof.
      intros ; simpl_eq ; reflexivity.
    Qed.

    Lemma subst_var_rec_comma_next : forall G T T' (t : term G T') D
      T'' (v : var (G :, T' ; D) T), 
      subst_var_rec (D :, T'') (next v T'') t = lift (subst_var_rec D v t) T''.
    Proof.
      intros ; simpl_eq ; reflexivity.
    Qed.

    (** Non-recursive wrapper to substitute the first variable in the context. *)

    Program Definition subst_var G T U (t : var (G :, T) U) (s : term G T) : 
      term G U := subst_var_rec empty t s.

    (** Substitution in a term. *)

    Program Fixpoint subst_rec G D T U (t : term (G :, T ; D) U)
      (s : term G T) { struct t } : term (G ; D) U :=
      match t with
        | cst c => cst (G ; D) c
        | rel _ v => @subst_var_rec G D T U v s
        | lam tau tau' b => 
          lam (subst_rec (D :, tau) b s)
        | app tau tau' f e => app (subst_rec D f s) (subst_rec D e s)
      end.
    
    (** Wrapped again. *)
    
    Program Definition subst (G : ctx) (T U : type) (t : term (G :, T) U) 
      (s : term G T) : term G U := subst_rec empty t s.
      
    (** The defining equations. *)

    Lemma subst_rec_empty_first : forall G T (t : term G T), 
      subst_rec empty (rel (first G T)) t = t.
    Proof.
      intros ; simpl_eq ; reflexivity.
    Qed.

    Lemma subst_rec_empty_next : forall G T T' (t : term G T) (v : var G T'), 
      subst_rec empty (rel (next v T)) t = rel v.
    Proof.
      intros ; simpl_eq ; reflexivity.
    Qed.
    
    Lemma subst_rec_comma_first : forall G T T' (t : term G T') D, 
      subst_rec (D :, T) (rel (first (G :, T' ; D) T)) t = rel (first (G ; D) T).
    Proof.
      intros ; simpl_eq ; reflexivity.
    Qed.

    Lemma subst_rec_comma_next : forall G T T' (t : term G T') D
      T'' (v : var (G :, T' ; D) T), 
      subst_rec (D :, T'') (rel (next v T'')) t = lift (subst_rec D (rel v) t) T''.
    Proof.
      intros ; simpl_eq ; reflexivity.
    Qed.
    
    (** ** Commutation lemmas.

       We now relate lifting and substitution to ultimately prove the substitution lemma. *)

    (** Substituting for a variable just lifted is a no-op.

       We first typecheck the statement, which will insert coercions around [t] to get the 
       right indices. The obligations are automatically resolved using the [Heq] hypothesis.
       Note that we separate the equality so that induction can proceed on [t] of type [term G' T] 
       while still retaining the equation between [G'] and [G ; D]. *)

    Program Definition subst_lift_rec_stmt :=
      forall G' T (t : term G' T) G D T' (u : term G T') (Heq : G' = (G ; D)), 
        subst_rec D (lift_rec G D t T') u = t.

    (** Now we prove it, by induction on [t]. We first rewrite [eq_rect] to coercions, then simplify
       the term using [simpl_term]. This takes care of almost all the plumbing. *)

    Lemma subst_lift_rec : subst_lift_rec_stmt.
    (* begin hide *)
    Proof.
      red ; induction t ; simpl ; intros ; rew_eq_coerce ; simpl_term ; auto.

      generalize dependent G0.
      generalize dependent G.
      generalize dependent T'.
      generalize dependent T.
      induction D ; intros.
      
      simpl in * |-.
      
      rewrite lift_var_empty.
      simpl_eq ; auto.
      
      induction v.
      inversion Heq.
      subst.
      simpl_term ; reflexivity.

      inversion Heq ; subst.
      simpl_term.

      clear IHv.
      pose (IHD T T' (G0 ; D) v G0 u (refl_equal (G0 ; D))).
      revert e.
      simpl in *.
      simpl_term.
      intros ; rewrite e.
      unfold lift ; simpl_term.
      rewrite lift_var_empty ; reflexivity.

      f_equal.
      pose (@IHt G0 (D :, T) T'0 u (refl_equal ((G0;D):, T))).
      revert e ; simpl_term ; auto.

      pose (IHt1 _ _ _ u Heq).
      pose (IHt2 _ _ _ u Heq).
      revert e ; revert e0 ; rew_eq_coerce ; simpl_term.
      intros.
      rewrite e0 ; rewrite e.
      reflexivity.
    Qed.
    (* end hide *)

    Opaque coerce_var_context.

    Lemma subst_lift_var : forall G D T (v : var (G ; D) T) T' (u : term G T'),
      subst_var_rec D (lift_var G D v T') u = rel v.
    Proof.
      intros G D.
      generalize dependent G.

      induction D ; intros.
      
      simpl in * |-.
      
      rewrite lift_var_empty.
      simpl_eq ; auto.
      
      revert T' u.
      dependent induction v generalizing G t.
      inversion H.
      subst.
      simpl_term ; reflexivity.

      inversion H ; subst.
      simpl_term.

      clear IHv.
      rewrite (IHD G0 T v).
      unfold lift ; simpl_term.
      rewrite lift_var_empty ; reflexivity.
    Qed.

    Lemma subst_lift : forall G D T (t : term (G ; D) T) T' (u : term G T'),
      subst_rec D (lift_rec G D t T') u = t.
    Proof.
      intros until t.
      dependent induction t generalizing G D ; intros ; subst* ; simpl ; 
        try discriminate ; rew_eq_coerce ; simpl_term ; auto.

      apply subst_lift_var.

      f_equal.
      pose (@IHt G0 (D :, T) (refl_equal ((G0;D):, T))).
      revert e ; simpl_term ; auto.

      pose (IHt1 _ _ H _ u).
      pose (IHt2 _ _ H _ u).
      revert e ; revert e0 ; rew_eq_coerce ; simpl_term.
      intros.
      rewrite e0 ; rewrite e.
      reflexivity.
    Qed.

    (** The real lemma is then just an instance of the previous one. *)

    Lemma subst_lift : forall G D T (t : term (G ; D) T) T' (u : term G T'),
      subst_rec D (lift_rec G D t T') u = t.
    Proof.
      intros.
      pose (subst_lift_rec t _ u (refl_equal (G ; D))).
      revert e ; simpl_term ; auto.
    Qed.

    (** We now prove that equality coercion commute with lift to solve some of the later
       lemmas which involve coercions of lift calls. Idealy this should be either easily derivable or
       automatically generated by some kind of generic programming. *)

    Lemma coerce_var_context_lift_var :
      forall G'' T (t : var G'' T) G D (Heq:G'' = G ; D) 
        G' U (H : (G :, U ; D) = (G' :, U ; D)) (H' : G'' = (G' ; D)), 
        coerce_var_context (lift_var G D (coerce_var_context t Heq) U) H = 
        lift_var G' D (coerce_var_context t H') U.
    (* begin hide *)
    Proof.
      induction t ; simpl ; intros ; simpl_term ; try reflexivity.

      destruct D ; simpl in *.
      inversion H ; destruct G0 ; try discriminate.
      inversion Heq ; subst.
      simpl_term ; reflexivity.

      inversion H'.
      subst.
      simpl_term ; reflexivity.

      f_equal.
      destruct D ; simpl in *.
      inversion H ; destruct G0 ; try discriminate.
      inversion Heq ; subst.
      simpl_term ; reflexivity.

      inversion H' ; subst.
      simpl_term.
      pose (IHt _ _ coerceH _ _ coerceH5 (refl_equal (G' ; D))).
      rewrite e.
      f_equal.
      f_equal.
      simpl_term.
      reflexivity.
    Qed.
    (* end hide *)
    
    Lemma coerce_term_context_lift_rec_aux :
      forall G'' T (t : term G'' T) G D (Heq:G'' = G ; D) G' U 
        (H : (G :, U ; D) = (G' :, U ; D)) (H' : G'' = (G' ; D)), 
        coerce_term_context (lift_rec G D (coerce_term_context t Heq) U) H = 
        lift_rec G' D (coerce_term_context t H') U.
    (* begin hide *)
    Proof.
      induction t ; simpl ; intros ; simpl_term ; try reflexivity.
      f_equal.

      apply (coerce_var_context_lift_var v _ _ Heq _ _ H H').

      f_equal.

      pose(H0 := refl_equal (G0 ; (D :, T))).
      assert(G0 :, U ; D :, T = G' :, U ; D :, T) by auto.
      pose (IHt _ _ H0 G' U H1 coerceH0).
      simpl in e ;  rewrite <- e.
      f_equal ; try apply proof_irrelevance.
      f_equal.
      unfold H0.
      simpl_term.
      reflexivity.

      f_equal ; auto.
    Qed.
    (* end hide *)

    Lemma coerce_term_context_lift_rec :
      forall G D T (t : term (G ; D) T) G' U (H : (G :, U ; D) = (G' :, U ; D)) 
        (H' : (G ; D) = (G' ; D)), 
        coerce_term_context (lift_rec G D t U) H = 
        lift_rec G' D (coerce_term_context t H') U.
    Proof.
      intros.
      pose (coerce_term_context_lift_rec_aux t _ _ (refl_equal (G ; D)) _ _ H H').
      revert e ; simpl_term ; auto.
    Qed.

    (** We have to take care of the opaqueness of these constants all the time, spurious unfoldings 
       can occur otherwise, greatly obfuscating the goal. *)

    Opaque coerce_var_context coerce_term_context.
    Opaque lift_rec subst_rec.

    (** We continue on our road to the substitution lemma. Here we prove commutation of [lift_var]. *)
    
    Program Definition lift_lift_var_stmt :=
      forall G' U (t : var G' U) G D D' (Heq : G' = G ; D ; D') T T',
        lift_var (G :, T ; D) D' (lift_var G (D ; D') t T) T' =
        lift_var G (D :, T' ; D') (lift_var (G ; D) D' t T') T.

    Lemma lift_lift_var : lift_lift_var_stmt.
    (* begin hide *)
    Proof.
      red ; repeat rewrite eq_rect_coerce_var ; induction t.

      intros.
      destruct D' ; simpl.
      destruct D ; simpl in *.
      destruct G0 ; simpl in *.
      discriminate.
      inversion Heq ; subst.
      simpl_term ; reflexivity.

      inversion Heq ; subst.
      simpl_term ; reflexivity.
      
      inversion Heq ; subst.
      repeat rewrite eq_rect_coerce_var.
      Transparent coerce_var_context.
      unfold coerce_var_context.
      Opaque coerce_var_context.
      simpl.
      simpl_term ; reflexivity.
      
      intros.
      destruct D' ; simpl.
      destruct D ; simpl in *.
      destruct G0 ; simpl in *.

      discriminate.

      inversion Heq ; subst.
      simpl_term ; reflexivity.

      inversion Heq ; subst.
      simpl_term ; reflexivity.

      inversion Heq ; subst.
      unfold append in * ; fold append in *.
      simpl_uip.

      assert (IH:=IHt G0 D D' (refl_equal (G0 ; D ; D')) T0 T').
      clear IHt.
      revert IH.
      intros.

      revert IH.
      simpl_term.
      intros.
      repeat rewrite eq_rect_coerce_var.
      Transparent coerce_var_context.
      simpl_term.
      Opaque coerce_var_context.
      repeat rewrite <- eq_rect_coerce_var.
      rewrite IH ; clear IH ; clear_eqs.
      reflexivity.
    Qed.
    (* end hide *)

    Program Definition lift_lift_stmt :=
      forall G' U (t : term G' U) G D D' T T' (Heq: G' = G ; D ; D'),
      lift_rec (G :, T ; D) D' (lift_rec G (D ; D') t T) T' =
      lift_rec G (D :, T' ; D') (lift_rec (G ; D) D' t T') T.
    
    (* begin hide *)
    Opaque coerce_var_context coerce_term_context.
    Opaque lift_rec subst_rec.
    Transparent coerce_term_context lift_rec.
    (* end hide *)

    Lemma lift_lift : lift_lift_stmt.
    (* begin hide *)
    Proof.
      red ;induction t ; intros ; repeat rewrite eq_rect_coerce ; simpl_term.

      reflexivity.

      f_equal.
      pose (lift_lift_var v _ _ _ Heq T0 T').
      revert e.
      repeat rewrite eq_rect_coerce_var.
      simpl_term.
      pi_coerce_proofs.
      intros.
      rewrite e.
      reflexivity.

      assert((G0 ; D ; D') :, T = G0 ; D ; D' :, T) by (subst ; auto).
      assert (IH:=IHt G0 D (D' :, T) T0 T'0 H) ; clear IHt.
      revert IH.
      unfold append in * ; fold append in *.
      repeat rewrite eq_rect_coerce.
      simpl_term.
      unfold append in * ; fold append in *.
      simpl_term.
      intros.
      f_equal.
      rewrite IH ; clear IH.
      repeat (f_equal ; try apply proof_irrelevance).

      assert (IH1:=IHt1 G0 D D' T0 T'0 Heq) ; clear IHt1.
      assert (IH2:=IHt2 G0 D D' T0 T'0 Heq) ; clear IHt2.
      revert IH1 ; revert IH2.
      repeat rewrite eq_rect_coerce.
      simpl_term.
      intros.
      f_equal.
      rewrite IH1 ; reflexivity.
      rewrite IH2 ; reflexivity.
    Qed.
    (* end hide *)

    (** Commutation of lifting and substitution, for variables. *)

    Program Definition subst_lift_var_comm_stmt := 
      forall G' T (t : var G' T) G D' D U T' (s : term G U) 
        (Heq: G' = G :, U ; D ; D'),
        subst_var_rec  (D :, T' ; D') (lift_var (G :, U ; D) D' t T') s = 
        lift_rec (G ; D) D' (subst_var_rec (D ; D') t s) T'.
    (* begin hide *)
    Transparent subst_rec lift_rec subst_var_rec lift_var.
    Opaque coerce_var_context coerce_term_context.

    Lemma subst_lift_var_comm : subst_lift_var_comm_stmt.
    Proof.
      red ; induction t ; intros ; rew_eq_coerce ; simpl_term ; try reflexivity.

      Opaque subst_rec lift_rec subst_var_rec lift_var.
      generalize dependent D.
      induction D' ; simpl in *.
      induction D ; simpl in * ; intros.
      inversion Heq ; subst.
      simpl_term.
      Transparent lift_var subst_var_rec.
      simpl_term ; reflexivity.

      clear IHD.
      Opaque lift_var subst_var_rec lift_rec.
      inversion Heq.
      subst.
      simpl_term.
      
      rewrite (lift_var_empty).
      pose (subst_var_rec_comma_first).
      unfold append in * ; fold append in *.
      rewrite e.
      rewrite lift_rec_empty.
      pose (subst_var_rec_comma_next).
      unfold append in * ; fold append in *.
      rewrite e0 with (D := (D :, t)) (G:=G0) (T':=U).
      unfold lift.
      rewrite subst_var_rec_comma_first.
      simpl.
      rewrite lift_rec_empty.
      reflexivity.
      
      clear IHD'.
      intros.
      inversion Heq ; subst.
      simpl_term.
      rewrite subst_var_rec_comma_first.
      simpl_term.
      Transparent coerce_term_context coerce_var_context.
      simpl_term.
      Transparent lift_rec lift_var.
      simpl_term.
      rewrite subst_var_rec_comma_first ; reflexivity.

      generalize dependent D.
      induction D' ; simpl in *.
      induction D ; simpl in * ; intros.

      inversion Heq ; subst.
      simpl_term.
      Transparent lift_var subst_var_rec lift.
      simpl_term. 
      unfold lift ; simpl_term ; reflexivity.

      clear IHD.
      inversion Heq ; subst.
      Opaque lift_var subst_var_rec lift_rec.
      simpl_term.
            
      rewrite (lift_var_empty).
      Transparent lift_var subst_var_rec lift_rec lift.
      simpl_term.
      reflexivity.

      clear IHD'.
      intros.
      inversion Heq ; subst.
      simpl_term.
      assert (IH:=IHt _ _ _ _ T' s (refl_equal (G0 :, U0 ; D ; D'))) ; clear IHt.
      revert IH.
      rew_eq_coerce.
      simpl_term.
      intros.
      rewrite IH ; clear IH.
      unfold lift.
      unfold append in * ; fold append in *.
      simpl_term.
      generalize (subst_var_rec (D ; D') t s).
      intros.
      assert (G0 ; D ; D' = (G0 ; D) ; D' ; empty) by auto.
      pose (lift_lift t1 (G0 ; D) D' empty T' t0 H). 
      revert e.
      rew_eq_coerce.
      simpl in *.
      simpl_term.
      intros.

      rewrite (proof_irrelevance _ H coerceH7).
      revert e.
      clear_eqs.
      intros.
      generalize dependent D.
      intros D.
      repeat rewrite app_assoc.
      intros.
      simpl in *.
      revert e.
      simpl_term.
      auto.
    Qed.
    (* end hide *)
 
    (** Commutation of lifting and substitution, for terms. *)

    Program Definition subst_lift_comm_stmt := 
      forall G' T (t : term G' T) G U D D' T' (s : term G U) 
        (Heq: G' = G :, U ; D ; D'),
        subst_rec  (D :, T' ; D') (lift_rec (G :, U ; D) D' t T') s = 
        lift_rec (G ; D) D' (subst_rec (D ; D') t s) T'.

    (* begin hide *)
    Transparent subst_rec.

    Lemma subst_lift_comm : subst_lift_comm_stmt.
    Proof.
      red ; induction t ; intros ; repeat rewrite eq_rect_coerce ; simpl_term ; try reflexivity.
 
      (* var *)
      pose (subst_lift_var_comm v _ _ T' s Heq).
      revert e.
      rew_eq_coerce ; simpl_term.
      auto.

      (* lam *)
      f_equal.
      assert((G0 :, U ; D ; D') :, T = G0 :, U ; D ; D' :, T) by auto.
      assert (IH:=IHt _ _ _ _ T'0 s H) ; clear IHt ; revert IH.
      rew_eq_coerce ; unfold append in * ; fold append in * ; simpl_term.
      clear_eqs.
      unfold append in * ; fold append in *.
      simpl_term.
      auto.

      (* app *)
      assert (IH1:=IHt1 G0 U D D' T'0 s Heq) ; clear IHt1.
      assert (IH2:=IHt2 G0 U D D' T'0 s Heq) ; clear IHt2.
      revert IH1 ; revert IH2.
      rew_eq_coerce ; simpl_term.
      intros.
      f_equal.
      rewrite IH1 ; reflexivity.
      rewrite IH2 ; reflexivity.
    Qed.
    (* end hide *)

    (** The non-recursive case, with no [D'] context. This time the statement need not 
       contain any coercions. *)

    Lemma subst_lift_comm_full : 
      forall G U D T (t : term (G :, U ; D) T) (s : term G U) T',
        subst_rec  (D :, T') (lift_rec (G :, U ; D) empty t T') s = 
        lift_rec (G ; D) empty (subst_rec D t s) T'.
    (* begin hide *)
    Proof.
      intros.
      pose (@subst_lift_comm _ _ t G U D empty T' s).
      simpl in e.
      assert (H:=e (refl_equal (G :, U ; D))) ; clear e.
      revert H.
      simpl_term.
      auto.
    Qed.
    
    Transparent subst_rec lift_rec.
    Transparent coerce_term_context.
    (* end hide *)

    (** Finally, we can state the subtitution lemma as usual. 
       The proof uses all the lemmas proven above, including commutation of [lift_rec] and 
       [coerce_term_context]. *)

    Program Definition subst_rec_comm_stmt :=
      forall G' T (u : term G' T) D' G D T' T''
        (s : term (G :, T'' ; D) T') (t : term G T'')
        (Heq: G' = (G :, T'' ; D :, T' ; D')),
        subst_rec D' (subst_rec (D :, T' ; D') u t) (subst_rec D s t) =
        subst_rec (D ; D') (subst_rec D' u s) t.

    Lemma subst_rec_comm : subst_rec_comm_stmt.
    (* begin hide *)
    Proof.
      red ; induction u ; intros ; rew_eq_coerce ; simpl_term ; try reflexivity.
 
      (* var *)
      generalize dependent D'.      
      induction v ; intros.
      
      (* first *)
      destruct D'.
      simpl in * |-.
      inversion Heq ; subst.
      simpl_term ; reflexivity.

      inversion Heq ; subst.
      unfold append in * ; fold append in *.
      simpl_term ; reflexivity.

      (* next *)
      destruct D'.
      Opaque subst_var_rec.
      simpl in * |-.
      Transparent subst_var_rec.
      inversion Heq ; subst.
      simpl_term. 
      unfold lift.
      rewrite subst_lift.
      reflexivity.

      inversion Heq ; subst.
      unfold append in * ; fold append in *.
      simpl_term.

      inversion coerceH0.
      inversion coerceH1.
      inversion coerceH2.
      assert (H:=IHv _  (refl_equal (G0 :, T'' ; D :, T' ; D')) coerceH4 H0 H1 H2) ; clear IHv.
      revert H.
      simpl_term.
      clear_eqs.
      intros.
      unfold lift.
      pose (coerce_term_context_lift_rec _ empty (subst_var_rec (D :, T' ; D') v t) _ _ coerceH0 H0).
      unfold append in * ; fold append in *.
      rewrite e ; clear e.
      
      pose (@subst_lift_comm_full (G0 ; D) T' D' T (coerce_term_context (subst_var_rec (D :, T' ; D') v t) H0) (subst_rec D s t) t0).
      rewrite e ; clear e.
      rewrite H ; clear H.

      pose (coerce_term_context_lift_rec _ empty (subst_var_rec D' (coerce_var_context v coerceH4) s) _ _ coerceH2 H2).
      unfold append in * ; fold append in *.
      rewrite e ; clear e.

      set (sv:=(coerce_term_context (subst_var_rec D' (coerce_var_context v coerceH4) s)
              H2)).
      pose (@subst_lift_comm_full G0 T'' (D ; D') _ sv t t0).
      rewrite e ; clear e.

      pose (coerce_term_context_lift_rec _ empty (subst_rec (D ; D') sv t) _ _ coerceH1 H1).
      unfold append in * ; fold append in *.
      rewrite e ; clear e.
      reflexivity.

      (* lam *)
      f_equal.
      assert((G0 :, T'' ; D :, T'0 ; D') :, T = G0 :, T'' ; D :, T'0 ; D' :, T) by auto.
      assert (IH:=IHu _ _ _ _ _ s t H) ; clear IHu ; revert IH.
      rew_eq_coerce ; unfold append in * ; fold append in * ; simpl_term.
      clear_eqs.
      unfold append in * ; fold append in *.
      simpl_term.
      auto.

      (* app *)
      assert (IH1:=IHu1 D' G0 D T'0 T'' s t Heq) ; clear IHu1.
      assert (IH2:=IHu2 D' G0 D T'0 T'' s t Heq) ; clear IHu2.
      revert IH1 ; revert IH2.
      rew_eq_coerce ; simpl_term.
      intros.
      f_equal.
      rewrite IH1 ; reflexivity.
      rewrite IH2 ; reflexivity.
    Qed.
    (* end hide *)

    (** Non-recursive case, where no coercion is needed anymore. *)

    Lemma subst_comm :
      forall G T'' D T' T (u : term (G :, T'' ; D :, T') T)
        (s : term (G :, T'' ; D) T') (t : term G T''),
        subst (subst_rec (D :, T') u t) (subst_rec D s t) =
        subst_rec D (subst u s) t.
    Proof.
      intros.
      pose (subst_rec_comm u empty _ s t (refl_equal (G :, T'' ; D :, T'))).
      simpl in e ; revert e ; simpl_term.
      auto.
    Qed.

  End Substitution.

  (** * Interpretation into CIC.
     
     There is a direct embedding of $\lambda^{\rightarrow}$ into the Calculus of Constructions, which
     we build now. *)

  Section Interpretation.
    
    (** We require interpretations for the constants and their types. *)

    Variable interp_cst_type : constant_types -> Set.
    Variable interp_cst : forall c : constants, interp_cst_type (type_constant c).

    (** Interpret a type into a coq [Set]. We need an impredicate [Set] to work with this definition. *)

    Fixpoint interp_type (t : type) : Set :=
      match t with
        | type_cst c => interp_cst_type c
        | a --> b => interp_type a -> interp_type b
      end.
    
    (** A valuation is a function which associates a term to each variable in a context. *)

    Program Definition valuation (G : ctx) := 
      forall T, var G T -> interp_type T.

    (** We can extend a valuation by a term. *)

    Program Definition augment_valuation (G : ctx) (rho : valuation G) 
      (T : type) (x : interp_type T) : valuation (G :, T) :=
      fun T v => 
        match v with
          | first _ _ => x
          | next G' T' v' _ => rho T' v'
        end.
    
    (** Now we can interpret terms easily. *)

    Fixpoint interp_term (G : ctx) (T : type) (t : term G T) 
      (v : valuation G) {struct t} : interp_type T :=
      match t in term _ T return valuation G -> interp_type T with
        | cst c => fun _ => interp_cst c
        | rel T n => fun v => v T n
        | lam T T' b => (fun v => 
          (fun x : interp_type T => 
            interp_term  b (augment_valuation v x)))
        | app T T' f e => fun v => (interp_term f v) (interp_term e v)
      end v.
    
    (** The empty valuation. *)

    Program Definition nil_valuation : valuation empty := fun n v => !.
    
    (** Interpretation of closed terms. *)

    Definition interp_closed_term (T : type) (t : term empty T) : interp_type T :=
      interp_term t nil_valuation.
  
  End Interpretation.

  (** * A proof of weak normalization.
     
     Inspired by %\cite{DBLP:journals/entcs/BiernackaDS06}%, we build a proof of weak-head normalization
     using a tait-style proof. This is an instance of normalization by evaluation where the semantic
     domain is given by [R], the strong computability predicate.
     *)

  Section WeakNormalization.

    (** Beta-reduction and its contextual closure. *)

    Inductive reduces (G : ctx) : forall T : type, term G T -> term G T -> Prop :=
    | red_beta : forall tau tau' (b : term (G :, tau) tau') (e : term G tau), 
      reduces (app (lam b) e) (subst b e)
    | red_app : forall tau tau' f f', @reduces G (tau --> tau') f f' -> 
      forall e, reduces (app f e) (app f' e).

    (** Evaluation gives the definition of normal forms, either:
       
       - [eval_trans] If a term [t] reduces to [s] which itself evaluates to [r] then
       [t] evaluates to [r]. So evaluation is "backward-closed" by reduction.
       - [eval_lam] Lambda expressions are all in normal form.
       - [eval_cst] A constant is a normal form.
       *)
    
    Inductive evaluates (G : ctx) : forall T : type, term G T -> term G T -> Prop :=
    | eval_trans : forall T (t : term G T) s r, 
      reduces t s -> evaluates s r -> evaluates t r
    | eval_lam : forall tau tau' b, @evaluates G (tau --> tau') (lam b) (lam b)
    | eval_cst : forall c, evaluates (cst G c) (cst G c).
    
    (** [R] is the glueing model in the sense of Coquand et al. We have a syntactic part [v] which is 
       the value of the term [t] and a semantic one given by the function in the arrow case which ensures
       closure by application. It is trivial for constants. 
       Note that [R] lives in [Set] so that we can extract it later. *)
    
    Program Fixpoint R G T (t : term G T) { struct T } : Set :=
      match T with
        | type_cst c => { v : term G T | evaluates t v }
        | tau --> tau' => 
          ({v : term G T | evaluates t v } * 
            (forall s, R s -> R (@app G tau tau' t s)))%type
      end.
    
    (** Extract the "syntactic" part. *)

    Lemma R_eval : forall G T (t : term G T), R t -> { v : term G T | evaluates t v }.
    Proof.
      intros.
      induction T ; simpl in * ; auto.
      destruct H ; auto.
    Qed.

    (** Backward-closedness of evaluation extends to computability. *)

    Lemma red_R_R : forall G T (t s : term G T), reduces t s -> R s -> R t.
    Proof.
      intros.
      generalize dependent G.
      induction T ; simpl ; intros.
      destruct H0.
      exists x. 
      apply eval_trans with s ; auto.
      intuition.
      destruct a.
      exists x.
      apply eval_trans with s ; auto.

      pose (red_app H s0).
      pose (b _ H0).
      apply (@IHT2 G _ _ r r0).
    Qed.

    (** ** Telescopes.

       A substitution is a telescope of terms. *)

    Inductive substitution : ctx -> Set :=
    | SNil : substitution empty
    | SCons : forall G, substitution G -> forall T, term G T -> substitution (G :, T).

    (** Substitute a term by a telescope. *)

    Program Fixpoint mult_subst G D U (u : term (G ; D) U) 
      (s : substitution G) { struct s } : term D U :=
      match s with
        | SNil => u
        | SCons G' s' T t =>
          mult_subst D (subst_rec D u t) s'
      end.

    (** This predicate ensures [R]-ness of all the terms in the telescope once they 
       are substituted by previous terms in the telescope. 
       It needs to be in [Set] as [R] is in [Set]. *)

    Fixpoint substitution_R G (s : substitution G) { struct s } : Set :=
      match s with
        | SNil => unit
        | SCons G' s' T t => (R (mult_subst empty t s') * substitution_R s')%type
      end.

    (** Inversion of non-empty substitutions. *)

    Lemma substitution_cons_aux : forall G (s : substitution G), forall G' T, G = G' :, T -> 
      { (s', t) : substitution G' * term G' T | JMeq s (SCons s' t) }.
    Proof.
      intros.
      induction s.
      discriminate.
      inversion H ; subst. 
      exists (s, t).
      apply JMeq_refl.
    Qed.

    Lemma substitution_cons : forall G T (s : substitution (G :, T)),
      { (s', t) : substitution G * term G T | s = SCons s' t }.
    Proof.
      intros.
      destruct (substitution_cons_aux s (refl_equal (G :, T))).
      destruct x.
      exists (s0, t).
      apply JMeq_eq. apply y.
    Qed.
      
    (** Substitution has no effect on constants. *)

    Lemma subst_cst : forall G c (s : substitution G) D, 
      mult_subst D (cst (G ; D) c) s = cst D c.
    Proof.
      induction s ; intros ; subst ; simpl_term ; auto.
      induction D ; simpl in * ; simpl_term ; auto.
    Qed.

    (** Unfolding of telescope substitution on lambdas. *)

    Lemma mult_subst_lam : forall G (s : substitution G) D T T' (u : term (G ; D :, T) T'),
      mult_subst D (lam u) s = lam (mult_subst (D :, T) u s).
    Proof.
      induction s ; intros ; simpl_term ; simpl in * ; rew_eq_coerce ; simpl_term ; intros ; auto.
    Qed.

    (** Unfolding of telescope substitution on applications. *)

    Lemma mult_subst_app : forall G D T T' (f : term (G ; D) (T --> T')) 
      (e : term (G ; D) T) (s : substitution G),
      mult_subst D (app f e) s = app (mult_subst D f s) (mult_subst D e s).
    Proof.
      induction s ; simpl_term ; auto.
      rew_eq_coerce ; simpl_term ; auto.
    Qed.
    
    (** Commutation of multiple substitutions is needed to prove that [R] is substitutive. 
       It is just an application of the substitution lemma proved previously. *)

    Lemma mult_subst_comm : forall G (s : substitution G) D T' T 
      (u : term (G ; D :, T') T) (s0 : term (G ; D) T'),
      subst (mult_subst (D :, T') u s) (mult_subst D s0 s) = 
        mult_subst D (subst u s0) s.
    Proof.
      induction s.
      simpl.
      intros.
      simpl_term.
      repeat rewrite eq_rect_coerce.
      generalize dependent D.
      intros D.
      unfold append in * ; fold append in *.
      rewrite (app_empty D).
      intros.
      simpl_term ; auto.
      
      intros.
      simpl.
      simpl_term.
      pose subst_comm.
      rewrite (IHs D T' _ (subst_rec (D :, T') u t)).
      f_equal.
      apply e.
    Qed.

    (** We extend [subst_lift] to contexts using substitution of telescopes and lifting by contexts. *)

    Program Definition mult_subst_lift_stmt :=
      forall G (s : substitution G) T (t : term empty T),
        (mult_subst empty (lift_ctx G t) s) = t.
    
    (** We need to have a dynamic coercion to prove these lemmas. *)

    Program Fixpoint coerce_subst_context G (s : substitution G) 
      G' (Heq:G = G') {struct s} : substitution G' :=
      match G' with
        | empty => SNil
        | G' :, T' =>
          match s with
            | SNil => !
            | SCons _ s' T t => 
              @SCons G' (coerce_subst_context s' _) T' t
          end
      end.

    (** Extension of the [on_coerce_proof] tactical. *)

    Ltac on_coerce_proof tac :=
      match goal with
        [ |- ?T ] =>
        match T with
          | context [ coerce_var_context _ ?p ] => tac p
          | context [ coerce_term_context _ ?p ] => tac p
          | context [ eq_rect _ _ _ _ ?p ] => tac p
          | context [ coerce_subst_context _ ?p ] => tac p
        end
      end.
    
    (** The rest is just reinstantiation of tactics with the new [on_coerce_proof]. *)
    (* begin hide *)
    Ltac abstract_coerce_proof := on_coerce_proof 
      ltac:(fun p => let H := fresh "coerceH" in abstract_eq_hyp H p).
    Ltac abstract_coerce_proofs := repeat abstract_coerce_proof.
    
    Lemma coerce_subst_context_id : forall G (s : substitution G), 
      coerce_subst_context s (refl_equal G) = s.
    Proof.
      induction s ; simpl_term ; try abstract_coerce_proof ; simpl_term ; auto.
      rewrite IHs.
      reflexivity.
    Qed.
    
    Ltac pi_coerce_proof := on_coerce_proof ltac:(pi_eq_proof_hyp).
    Ltac pi_coerce_proofs := repeat pi_coerce_proof.

    Hint Rewrite coerce_subst_context_id : coerce_id.
    
    Ltac clear_coerce_proofs := abstract_coerce_proofs ; pi_coerce_proofs.
    
    Ltac clear_coerce_ctx := rewrite_coerce_id ; clear_coerce_proofs.

    Ltac simpl_term := 
      simpl ; simpl_eqs ; clear_coerce_ctx ; clear_refl_eqs ;  
        try subst ; simpl ; repeat simpl_uip ; rewrite_coerce_id.

    Lemma eq_rect_coerce_subst : forall G (t : substitution G) G' (Heq: G = G'), 
      eq_rect _ (fun G' => substitution G') t _ Heq = coerce_subst_context t Heq.
    Proof.
      induction t ; simpl ; intros ; simpl_term ; simpl_term ; try reflexivity.
    Qed.

    Hint Rewrite eq_rect_coerce_subst : eq_rect_coerce.    
    (* end hide *)

    (** We can finaly prove the mult_subst lemma. *)

    Lemma mult_subst_lift : mult_subst_lift_stmt.
    (* begin hide *)
    Proof.
      red ; induction s ; intros ; simpl_term.

      reflexivity.

      rew_eq_coerce ; simpl_term.
      unfold lift.
      rewrite subst_lift.
      rewrite <- (IHs _ t0).
      f_equal. 
      f_equal.
      apply IHs.

      simpl_term.
      rewrite (eq_rect_coerce_subst s coerceH2).
      f_equal ; apply proof_irrelevance.
    Qed.
    (* end hide *)

    (** ** Main lemma.

       A little lemma on variables is all that is missing before proving our main lemma.
       We can destruct variables, keeping the equality handy. *)

    Lemma var_case_aux : forall G' T (v : var G' T), forall G t, G' = G :, t ->
      (t = T /\ JMeq v (first G T)) + { v' : var G T | JMeq v (next v' t) }.
    (* begin hide *)
    Proof.
      destruct v ; program_simpl.
      inversion H ; subst ; clear H.
      intuition.
      
      inversion H ; subst ; clear H.
      right.
      exists v.
      intuition.
    Qed.
    (* end hide *)

    Lemma var_case : forall G t T (v : var (G :, t) T),
      (t = T /\ JMeq v (first G T)) + { v' : var G T | v = next v' t }.
    (* begin hide *)
    Proof.
      intros.    
      destruct (var_case_aux v (refl_equal (G :, t))).
      intuition.
      right ; destruct exist s Hs.
      exists s ; apply JMeq_eq ; auto.
    Qed.
    (* end hide *)

    (** We now prove the main lemma, substitutivity of [R]. Note that we end with a closed term, 
       escaping the problem of variables. *)
    
    Lemma R_substitutive : forall G U (u : term G U) (s : substitution G),
      substitution_R s -> R (mult_subst empty u s).
    (* begin hide *)
    Proof with simpl.
      induction u.
      
      (* cst *)
      intros.
      pose (subst_cst c s empty).
      simpl in e ; rewrite e.
      simpl ; eapply exist ; constructor.

      (* rel *)
      induction G.
      inversion v.

      intros.
      pose (substitution_cons s) ; destruct_exists ; destruct_pairs.
      simpl_JMeq.
      subst.
      simpl.
      Opaque subst_rec.
      simpl_term.
      simpl in H.
      
      destruct (var_case v).
      intuition.
      subst ; simpl_JMeq ; subst.
      Transparent subst_rec.
      simpl_term.
      assumption.

      destruct_exists.
      intuition.
      subst ; simpl_JMeq ; subst.
      simpl_term.
      apply IHG ; auto.

      (* lam *)
      simpl.
      split.

      pose (mult_subst_lam s (D:=empty) u).
      rewrite e.
      eapply exist ; constructor.

      intros.
      rewrite (mult_subst_lam s (D:=empty) u).

      apply red_R_R with (subst (mult_subst (empty :, T) u s) s0).
      apply red_beta.
      pose (@mult_subst_comm _ s empty T T' u).
      pose (s' := coerce_term_context (lift_ctx G s0) (app_empty G)).
      simpl in e.
      assert (Hs:=e s').
      clear e.
      pose (IHu (SCons s s')).
      simpl in r.
      revert r.
      simpl_term.
      intros.
      assert (s0 = mult_subst empty s' s).
      rewrite <- (mult_subst_lift s s0).
      subst s'.
      simpl_term.
      rewrite eq_rect_coerce_subst.

      clear.
      induction G ; simpl ; auto.
      simpl_term.
      simpl in *.
      simpl_term ; reflexivity.

      unfold lift.
      destruct (substitution_cons s).
      destruct_pairs ; simpl_JMeq.
      subst.
      simpl.
      simpl_term.
      rewrite subst_lift.

      unfold append in * ; fold append in *.
      pose (@coerce_term_context_lift_rec (empty ; G) empty _ (lift_ctx G s0) G t).
      simpl in e ; simpl_term.
      assert(empty ; G = G) by auto.
      rewrite (e coerceH H).
      rewrite subst_lift.
      
      apply IHG.

      rewrite H1.
      subst s'.
      rewrite Hs.
      apply r.
      split ; auto.
      rewrite <- H1.
      assumption.

      (* app *) 
      intros.
      rewrite (mult_subst_app empty u1 u2).

      assert (fR:=IHu1 _ H).
      assert (eR:=IHu2 _ H).
      
      unfold R at 1 in fR.
      fold R in *.
      simpl in *.
      destruct fR as [ef sf].
      destruct ef.
      apply sf.
      apply eR.
    Qed.
    (* end hide *)

    (** We get weak normalization as a trivial consequence of the previous lemma and [R_eval]. *)
    
    Lemma term_wn : forall T (t : term empty T), { v : term empty T | evaluates t v }.
    Proof.
      intros.
      cut (R t).
      apply R_eval.
      replace t with (mult_subst empty t SNil).
      apply R_substitutive.
      simpl.
      constructor.
      auto.
      simpl.
      elim_eq_rect ; auto.
    Qed.
  
  End WeakNormalization.

  Section StrongNormalization.

(**    Fixpoint neutral G T (t : term G T) {struct t} : Prop :=
      match t with
        | cst _ => True
        | rel _ _ => True
        | lam _ _ _ => False
        | app _ _ _ _ => True
      end.*)

    Inductive neutral (G : ctx) : type -> Set :=
    | neutral_rel : forall T, var G T -> neutral G T
    | neutral_app : forall T T', neutral G (T --> T') -> nf G T -> neutral G T'

    with nf (G : ctx) : type -> Set :=
    | nf_cst : forall c : constants, nf G (type_constant c)
    | nf_neutral : forall T, neutral G T -> nf G T
    | nf_lam : forall (T T' : type), 
      nf (G :, T) T' -> nf G (T --> T').
(*     | nf_app : forall T T' : type, *)
(*       neutral G (T --> T') -> nf G T -> nf G T'. *)

    Scheme neutral_mutind := Induction for neutral Sort Prop
    with nf_mutind := Induction for nf Sort Prop.

    Combined Scheme neutral_nf_mutind from neutral_mutind, nf_mutind.

    Fixpoint neutral_term G T (n : neutral G T) { struct n } : term G T :=
      match n in neutral _ T return term G T with
        | neutral_rel _ v => rel v
        | neutral_app _ _ f e => app (neutral_term f) (nf_term e)
      end

    with nf_term G T (t : nf G T) { struct t } : term G T :=
      match t in nf _ T return term G T with
        | nf_cst c => cst G c
        | nf_neutral _ v => neutral_term v
        | nf_lam tau tau' b => lam (nf_term b)
(*         | nf_app tau tau' f e => app (neutral_term f) (nf_term e) *)
      end.

    Coercion nf_term : nf >-> term.
    Coercion neutral_term : neutral >-> term.

    (** Beta-reduction and its contextual closure. *)

(*     Inductive reduces (G : ctx) : forall T : type, term G T -> term G T -> Prop := *)
(*     | red_beta : forall tau tau' (b : term (G :, tau) tau') (e : term G tau),  *)
(*       reduces (app (lam b) e) (subst b e) *)
(*     | red_app : forall tau tau' f f', @reduces G (tau --> tau') f f' ->  *)
(*       forall e, reduces (app f e) (app f' e). *)

    (** Evaluation gives the definition of normal forms, either:
       
       - [eval_trans] If a term [t] reduces to [s] which itself evaluates to [r] then
       [t] evaluates to [r]. So evaluation is "backward-closed" by reduction.
       - [eval_lam] Lambda expressions are all in normal form.
       - [eval_cst] A constant is a normal form.
       *)
    
    Reserved Notation " [ t # u ] ==> v " (at level 60).

    Reserved Notation " t ==> n " (at level 60).

    Inductive normalizes (G : ctx) : forall T : type, term G T -> nf G T -> Prop :=
    | norm_cst : forall c, cst G c ==> nf_cst G c
    | norm_rel : forall T (v : var G T), rel v ==> nf_neutral (neutral_rel v)
    | norm_lam : forall tau tau' b b',
      (b ==> b') -> (@normalizes G (tau --> tau') (lam b) (nf_lam b'))
    | norm_app : forall tau tau' (f : term G (tau --> tau')) f' e e' v,
      (f ==> f') -> (e ==> e') -> ([ f' # e' ] ==> v) ->
      (app f e ==> v)
      
      where " t ==> n " := (@normalizes _ _ t n)

    with normalizes_app (G : ctx) : forall T T', nf G (T --> T') -> nf G T -> nf G T' -> Prop :=
    | norm_app_rel : forall T T' (v : neutral G (T --> T')) (t' : nf G T), 
      [ nf_neutral v # t' ] ==> nf_neutral (neutral_app v t')
    | norm_app_lam : forall tau tau' (b : nf (G :, tau) tau') (v : nf G tau) b',
      (subst (nf_term b) (nf_term v) ==> b') -> ([ nf_lam b # v ] ==> b')
(*     | norm_app_app : forall tau tau' tau'' (f : neutral G (tau --> (tau' --> tau''))) e e' v v', *)
(*       ([ nf_neutral f # e ] ==> v) -> ([ v # e' ] ==> v') -> ([nf_neutral (neutral_app f e) # e'] ==> v') *)

      where " [ t # u ] ==> v " := (@normalizes_app _ _ _ t u v).

    Definition is_normalizing G T (s : term G T) := exists s', s ==> s'.

    Definition is_normalizing_app G T T' (s : nf G (T --> T')) s' := exists s'', [ s # s' ] ==> s''.
    
    Scheme normalizes_mutind := Induction for normalizes Sort Prop
    with normalizes_app_mutind := Induction for normalizes_app Sort Prop.

    Combined Scheme normalize_mutind from normalizes_mutind, normalizes_app_mutind.

    Ltac clear_exeq :=
      match goal with
        [ H : existT _ ?x _ = existT _ ?x _ |- _ ] => 
        let Hinj := fresh "Hinj" in
          assert (Hinj:=inj_pair2 _ _ _ _ _ H) ; clear H ; try subst
      end.

    Ltac clear_exeqs := repeat clear_exeq.

    Lemma normalize_det : (forall G T (t : term G T) n, t ==> n -> forall n', t ==> n' -> n = n') /\
      (forall G T T' (t : nf G (T --> T'))  u n, [ t # u ] ==> n -> forall n', [ t # u ] ==> n' -> n = n').
    Proof.
      eapply normalize_mutind ; simpl ; intros ; try inversion H ; subst ; clear_exeqs ; try reflexivity.

      inversion H0 ; clear_exeqs.
      rewrite (H b'0 H2).
      reflexivity.

      inversion H2 ; clear_exeqs.
      assert (Heqe:=H0 _ H9).
      assert (Heqf:=H _ H8) ; subst.
      apply H1 ; auto.

      inversion H0 ; clear_exeqs.
      apply H ; auto.
    Qed.
(*       apply H0. *)
(*       inversion H1 ; clear_exeqs. *)
(*       assert (Hfe:=H _ H6) ; subst. *)
(*       assumption. *)
(*     Qed. *)

    Lemma normalize_term_det : (forall G T (t : term G T) n, t ==> n -> forall n', t ==> n' -> n = n').
    Proof (proj1 normalize_det).

    Lemma normalize_app_det : 
      (forall G T T' (t : nf G (T --> T'))  u n, [ t # u ] ==> n -> forall n', [ t # u ] ==> n' -> n = n').
    Proof (proj2 normalize_det).

    Inductive conv (G : ctx) : forall T, term G T -> term G T -> Prop :=
    | conv_lam : forall tau tau' b b', @conv (G :, tau) tau' b b' -> conv (lam b) (lam b')
    | conv_app : forall tau tau' (f f' : term G (tau --> tau')) e e', 
      conv f f' -> conv e e' -> conv (app f e) (app f' e')
    | conv_refl : forall T (t : term G T), conv t t
    | conv_sym : forall T (t u : term G T), conv t u -> conv u t
    | conv_trans : forall T (t u v : term G T), conv t u -> conv u v -> conv t v
    | conv_red : forall T (t u : term G T), reduces t u -> conv t u.
    
    Lemma normalize_correct : 
      (forall G T (t : term G T) n, t ==> n -> conv t n) /\
      (forall G T T' (t : nf G (T --> T'))  u n, [ t # u ] ==> n -> conv (app t u) n).
    Proof.
      eapply normalize_mutind ; simpl ; intros ; subst ; clear_exeqs ; try reflexivity ; try constructor ; auto ; try solve [ constructor ].

      apply conv_trans with (app f' e'). 
      apply conv_sym ; auto.
      apply conv_app ; apply conv_sym ; auto.
      
      apply conv_sym.
      apply conv_trans with (subst b v).
      apply conv_red.
      constructor.
      assumption.

(*       apply conv_trans with (app v e') ; auto. *)
(*       apply conv_sym ; auto. *)
(*       apply conv_app ; constructor. *)
(*       assumption. *)
    Qed.

    Lemma normalize_term_correct : forall G T (t : term G T) n, t ==> n -> conv t n.
    Proof (proj1 normalize_correct).

    Tactic Notation "subst" "by" constr(t) := 
      let Hsubst := fresh "Hsubst" in
        assert(Hsubst:=t) ; subst.

    (** We need to have a dynamic coercion to prove these lemmas. *)

    Program Fixpoint coerce_neutral_context G T (n : neutral G T) 
      G' (Heq:G = G') {struct n} : neutral G' T :=
      match n in neutral _ T return neutral G' T with
        | neutral_rel T v => @neutral_rel G' T v
        | neutral_app T T' f e => @neutral_app G' T T' (coerce_neutral_context f Heq) (coerce_nf_context e Heq)
      end
      
    with coerce_nf_context G T (n : nf G T) 
      G' (Heq:G = G') {struct n} : nf G' T :=
      match n in nf _ T return nf G' T with
        | nf_cst c => nf_cst G' c
        | nf_neutral T n => @nf_neutral G' T (coerce_neutral_context n Heq)
        | nf_lam tau tau' b => @nf_lam G' tau tau' (coerce_nf_context b _)
(*         | nf_app tau tau' f e => @nf_app G' tau tau' (coerce_neutral_context f Heq) (coerce_nf_context e Heq) *)
      end.

    (** Extension of the [on_coerce_proof] tactical. *)

    Ltac on_coerce_proof tac :=
      match goal with
        [ |- ?T ] =>
        match T with
          | context [ coerce_var_context _ ?p ] => tac p
          | context [ coerce_term_context _ ?p ] => tac p
          | context [ eq_rect _ _ _ _ ?p ] => tac p
          | context [ coerce_subst_context _ ?p ] => tac p
          | context [ coerce_nf_context _ ?p ] => tac p
          | context [ coerce_neutral_context _ ?p ] => tac p
        end
      end.
    
    (** The rest is just reinstantiation of tactics with the new [on_coerce_proof]. *)
    (* begin hide *)
    Ltac abstract_eq_hyp H' p := 
      match type of p with
        ?X = ?Y => 
        match goal with 
          | [ H : X = Y |- _ ] => fail 1
          | _ => set (H':=p) ; clearbody H'
        end
        | context [ _ = _ ] => 
          set (H':=p) ; clearbody H' ; simpl in H' ; 
            (match type of H' with
               ?X = ?Y => revert H' ; (match goal with [ H : X = Y |- _ ] => fail 3 | _ => intros H' end)
             end)
      end.

    Ltac abstract_coerce_proof := on_coerce_proof 
      ltac:(fun p => let H := fresh "coerceH" in abstract_eq_hyp H p).
    Ltac abstract_coerce_proofs := repeat abstract_coerce_proof.
    
    Lemma coerce_neutral_nf_context_id : 
      (forall G T (t : neutral G T),
      coerce_neutral_context t (refl_equal G) = t) /\
      (forall G T (t : nf G T),
        coerce_nf_context t (refl_equal G) = t).    
    Proof.
      apply neutral_nf_mutind ; intros ; simpl_term ; try abstract_coerce_proof ; simpl_term ; auto.

      rewrite H0 ; rewrite H ; reflexivity.
      rewrite H ; auto.
      rewrite H ; auto.
    Qed.

    Lemma coerce_neutral_context_id : 
      forall G T (t : neutral G T),
        coerce_neutral_context t (refl_equal G) = t. 
    Proof proj1 coerce_neutral_nf_context_id.

    Lemma coerce_nf_context_id : forall G T (t : nf G T),
      coerce_nf_context t (refl_equal G) = t.
    Proof proj2 coerce_neutral_nf_context_id.

    Ltac pi_eq_proof_hyp p :=
      match type of p with
        ?X = ?Y => 
        match goal with 
          | [ H : X = Y |- _ ] => 
            match p with
              | H => fail 2
              | _ => rewrite (proof_irrelevance (X = Y) p H)
            end
          | _ => fail " No hypothesis with same type "
        end
        | context [ _ = _ ] => 
          let H := fresh "Hpi" in
            set (H := p) ; change p with H ; simpl in H ; 
              match type of H with
                ?X = ?Y =>
                match goal with 
                  | [ H' : X = Y |- _ ] => 
                    match p with
                      | H' => fail 2
                      | _ => rewrite (proof_irrelevance (X = Y) H H') ; clear H
                    end
                end
              end
      end.

    
    Ltac pi_coerce_proof := on_coerce_proof ltac:(pi_eq_proof_hyp).
    Ltac pi_coerce_proofs := repeat pi_coerce_proof.

    Hint Rewrite coerce_neutral_context_id coerce_nf_context_id : coerce_id.
    
    Ltac clear_coerce_proofs := abstract_coerce_proofs ; pi_coerce_proofs.
    
    Ltac clear_coerce_ctx := rewrite_coerce_id ; clear_coerce_proofs.

    Ltac simpl_term := 
      simpl ; simpl_eqs ; clear_coerce_ctx ; clear_refl_eqs ;  
        subst* ; simpl ; repeat simpl_uip ; rewrite_coerce_id.

    Lemma eq_rect_coerce_neutral : forall G T (t : neutral G T) G' (Heq: G = G'), 
      eq_rect _ (fun G' => neutral G' T) t _ Heq = coerce_neutral_context t Heq.
    Proof.
      induction t ; simpl ; intros ; simpl_term ; simpl_term ; try reflexivity.
    Qed.

    Lemma eq_rect_coerce_nf : forall G T (t : nf G T) G' (Heq: G = G'), 
      eq_rect _ (fun G' => nf G' T) t _ Heq = coerce_nf_context t Heq.
    Proof.
      induction t ; simpl ; intros ; simpl_term ; simpl_term ; try reflexivity.
    Qed.

    Tactic Notation "simpl" "*" := repeat progress (rew_eq_coerce ; simpl_term).
    
    Hint Rewrite eq_rect_coerce_neutral eq_rect_coerce_nf : eq_rect_coerce.
    (* end hide *)

    Section Complete.
      Hypothesis SN : forall G T (t : term G T), is_normalizing t.

      Lemma normalizes_exp_stmt : forall G T (b b' : term G T), 
        forall c, b' ==> c -> reduces b b' -> b ==> c.
      Proof.
        induction b ; simpl ; intros.
        inversion H0.
        inversion H0.
        
        inversion H0.
        inversion H0 ; subst ;  clear_exeqs.
        destruct (SN b2).
        destruct (SN b0).
        eapply norm_app.
        constructor ; apply H2.
        apply H1.
        constructor.
      Admitted.

    Program Definition normalizes_subst_stmt : forall G' T (b : term G' T), 
      forall G tau D, (G' = G :, tau ; D) ->
      forall (e : term G tau) o, subst_rec D b e ==> o ->
      forall b', b ==> b' -> subst_rec D (nf_term b') e ==> o.

    Lemma normalizes_subst : normalizes_subst_stmt.
    Proof with simpl* ; auto.
      red ; induction b ; simpl ; intros ; try (destruct G ; [ discriminate | (inversion H ; try subst) ]) ; simpl in * ; try discriminate ; intros ; simpl_term.

      revert H0...
      inversion H1 ; clear_exeqs...

      revert H0 ; simpl*.
      inversion H1 ; clear_exeqs...

      revert H0...
      inversion H1 ; clear_exeqs...
      pose (IHb G0 tau (D :, T) (refl_equal (G0 :, tau ; D :, T)) e).
      revert n ; clear IHb...
      intros.
      inversion H0 ; clear_exeqs.
      cut(subst_rec (D :, T)
                (eq_rect ((G0 :, tau; D) :, T) (fun G : ctx => term G T') b
                   ((G0 :, tau; D) :, T)
                   (normalizes_subst_stmt_obligation_1 b 
                      (D :, T) (refl_equal ((G0 :, tau; D) :, T)) e b')) e ==>
              b') ; intros.
      assert (n':=n b' H b'0 H2) ; clear n.
      revert n'...
      intros.
      constructor...
      simpl* ; apply H3.

      revert H0...
      inversion H1 ; clear_exeqs...
      intros.
      inversion H0 ; clear_exeqs...
      
      cut (subst_rec D
        (eq_rect G (fun G : ctx => term G (T -->  T')) b1
          (G0 :, tau; D)
          (normalizes_subst_stmt_obligation_1 b1 D H e f'0)) e ==>
        f'0) ; intros ; simpl* ; auto.
      pose (IHb1 _ _ _ H e f'0 H2 f' H6).
      revert n ; simpl* ; intros.
      
      cut (subst_rec D
                   (eq_rect G (fun G : ctx => term G T) b2 
                      (G0 :, tau; D)
                      (normalizes_subst_stmt_obligation_1 b2 D H e e'0)) e ==>
                 e'0) ;
        intros ; simpl* ; auto.
      pose (IHb2 _ _ _ H e _ H3 e' H7).
      revert n0... intros.
      clear H2 H3.
      

      clear IHb1 IHb2.
      

      inversion H8 ; clear_exeqs...

      apply norm_app with f'0 e'0...
      revert n...
      intros.
      inversion n ; clear_exeqs.
      subst*.
    Admitted.
(*       pose (norm_app). *)
      
      
      
      
(*       inversion H8 ; clear_exeqs. *)
(*       subst T0 T'0 v t' f'. *)
(*       simpl*. *)
(*       inversion H6 ; clear_exeqs. *)
(*       subst v0 b1. *)
(*       simpl*. *)
(*       clear IHb1 IHb2. *)
(*       subst T0. *)
(*       intros. *)
(*       inversion H0 ; clear_exeqs. *)
(*       subst e1 f0. *)
(*       subst. *)
      


    Lemma normalize_complete : 
      forall G T (t u : term G T), conv t u -> forall n o, t ==> n -> u ==> o -> n = o.
    Proof.
      induction 1 ; simpl ; intros.

      inversion H0 ; inversion H1 ; clear_exeqs.
      f_equal.
      apply IHconv ; auto.
      
      inversion H1 ; inversion H2 ; clear_exeqs.
      destruct (SN f).
      destruct (SN f').
      assert (Heq:=IHconv1 x x0 H3 H4) ; subst.
      destruct (SN e).
      destruct (SN e').
      assert (Heq:=IHconv2 x x1 H5 H6) ; subst.
      subst by (normalize_term_det H17 H6).
      subst by (normalize_term_det H9 H5).
      subst by (normalize_term_det H16 H4).
      subst by (normalize_term_det H3 H8).
      subst by (normalize_app_det H10 H18).
      reflexivity.

      subst by (normalize_term_det H H0).
      reflexivity.
      
      symmetry.
      apply IHconv ; auto.
      
      destruct (SN u).
      apply trans_eq with x.
      apply (IHconv1 _ _ H1 H3).
      apply (IHconv2 _ _ H3 H2).

      induction H.
      inversion H0 ; clear_exeqs.
      inversion H6 ; clear_exeqs.
      inversion H8 ; clear_exeqs.
    Admitted.
      (*
      assert(subst b e ==> n).
      unfold subst.
      apply normalizes_subst.
      




      assert(Hfx0:=normalize_term_correct H3).
      assert(Hex1:=normalize_term_correct H5).
      assert(conv (app f e) (app x0 x1)) by (constructor ; auto).
      apply (normalize_term_det H1).
      apply norm_app with x0 x1 ; auto.
      inversion H2 ; clear_exeqs.
      apply IHconv2.

      inversion H0 ; inversion H1 ; clear_exeqs.
      f_equal.
      apply IHconv ; auto.
      *)

    End Complete.
      
    Fixpoint SCN G T { struct T } : nf G T -> Prop :=
      match T return nf G T -> Prop with
        | type_cst c => fun t => True
        | tau --> tau' => fun t => forall u : nf G tau, SCN u -> exists n : nf G tau', ([ t # u ] ==> n) /\ SCN n
      end
      
    with SCN_neutral G T { struct T } : neutral G T -> Prop :=
      match T return neutral G T -> Prop with
        | type_cst c => fun t => True
        | tau --> tau' => fun t => forall u : nf G tau, SCN u -> exists n : nf G tau', ([ nf_neutral t # u ] ==> n) /\ SCN n
      end.

    Definition SN G T (t : term G T) :=
      exists n : nf G T, t ==> n /\ SCN n.

    Fixpoint substitution_SN G (s : substitution G) { struct s } : Prop :=
      match s with
        | SNil => True
        | SCons G' s' T t => (SN (mult_subst empty t s') * substitution_SN s')%type
      end.

    Lemma mult_subst_comma_first : 
      forall G (s : substitution G) D T, mult_subst (D :, T) (rel (first (G; D) T)) s = rel (first D T).
    Proof.
      induction s ; intros ; simpl_term ; rew_eq_coerce ; simpl_term ; auto.
    Qed.

    Program Definition strong_normalization_app_stmt :=
      forall G U (t : nf G U), forall T T', (U = T --> T') -> forall (u : nf G T), SCN t -> SCN u -> 
      exists n' : nf G T', ([ t # u ] ==> n') /\ SCN n'.

    Lemma strong_normalization_app :  strong_normalization_app_stmt.
    Proof.
      red ; induction t ; simpl ; intros.
      discriminate.

      destruct T.
      discriminate.
      inversion H ; subst.
      simpl*.
      simpl in H0.
      destruct (H0 _ H1).
      exists x.
      simpl*.
      assumption.

      inversion H ; subst.
      simpl*.
      destruct (H0 _ H1).
      exists x.
      simpl*.
      assumption.
    Qed.

    Lemma neutral_SCN : forall T G (n : neutral G T), SCN (nf_neutral n).
    Proof with simpl* ; auto.
      induction T...
      intros.
      exists (nf_neutral (neutral_app n u)).
      intuition.
      constructor.
    Qed.

    Program Definition SN_substitutive_stmt :=
      forall G' U (u : term G' U) G D (H : G' = G ; D) (s : substitution G),
      substitution_SN s -> SN (mult_subst D u s).

    Lemma SN_substitutive : SN_substitutive_stmt.
    Proof with simpl* ; auto.
      red ; induction u ; simpl ; intros...
      
      exists (nf_cst D c).
      rewrite (subst_cst c s)...
      intuition ; constructor.

      (* rel *)
      generalize dependent G0.
      induction D.
      induction G ; intros.
      inversion v.

      simpl in *.
      destruct G0.
      discriminate.
      inversion H ; subst.

      pose (substitution_cons s) ; destruct_exists ; destruct_pairs.
      simpl_JMeq.
      subst.
      simpl.
      Opaque subst_rec.
      simpl_term.
      simpl in H0.
      
      destruct (var_case v).
      intuition.
      subst ; simpl_JMeq ; subst.
      Transparent subst_rec.
      simpl_term.
      assumption.

      destruct_exists.
      intuition.
      subst ; simpl_JMeq ; subst.
      simpl_term.
      pose (IHG s _ (refl_equal G0) s0 b) ; auto.
      revert s1...

      (* Delta not empty *)
      intros.
      destruct G ; try discriminate.
      inversion H ; subst...
      simpl in *...
      
      destruct (var_case v).
      intuition.
      subst ; simpl_JMeq ; subst.
      rewrite mult_subst_comma_first.
      red.
      exists (nf_neutral (neutral_rel (first D T))) ; intuition.
      constructor.
      apply neutral_SCN.
      
      destruct_exists.
      intuition.
      subst ; simpl_JMeq ; subst.
      admit.


      rewrite mult_subst_lam.
      unfold SN. 
      pose (IHu G0 (D :, T) (refl_equal ((G0 ; D) :, T)) s H0).
      revert s0...
      intros.
      destruct s0.
      exists (nf_lam x).
      intuition.
      constructor ; auto.
      eapply ex_intro ; constructor.
      inversion H1 ; clear_exeqs.
      subst T'.
      pose (strong_normalization_app).
      exists 
        
      pose (IHG _ (refl_equal G0) s0 b T s) ; auto.
      revert s1... auto.

      rewrite mult_subst_cst.


    Lemma strong_computability : forall T G (t : nf G T), SCN t.
    Proof.
      induction T.
      simpl ; auto.

      intros G t.
      remember (T1 --> T2) as T'.
      revert HeqT'.
      induction t ; simpl ; intros ; subst* ; simpl ; intros ; auto.

      exists (nf_neutral (neutral_app n u)).
      split ; auto.
      constructor.

      inversion HeqT' ; simpl*.
      pose (IHT2 _ t).
      clearbody s.
      clear IHt.

      

      cut (SCN (nf_lam t)).
      intros.
      destruct (strong_normalization_app (nf_lam t) (refl_equal (T1 --> T2)) u H0 H).
      exists x.
      revert H1 ; simpl*.
      auto.

      simpl.
      intros.
      

      

      generalize dependent t.
      eapply ex_intro.
      split.
      constructor.
      unfold SCN in IHT1.


    Program Definition SCN_prop :=
      forall G T (t : nf G T) 


    Program Definition SCN_subst_stmt := forall G T (n : nf G T), 
      SCN n -> forall (n' : nf G T), reduces n n' -> SCN n'.
    
    Lemma SCN_subst : SCN_subst_stmt.
    Proof with simpl* ; auto.
      red ; induction n ; intros...

      destruct T ; simpl in * ; auto.
      intros.
      destruct (H _ H1).
      exists x.
      intuition.
      inversion H0 ; clear_exeqs...
      inversion H3 ; clear_exeqs...
      admit.

      inversion H3 ; clear_exeqs...
      admit.
      

      
      

      unfold SCN in s.

            
      

      exists (
      apply nf_app_
      

      

      
      
    
    (** [R] is the glueing model in the sense of Coquand et al. We have a syntactic part [v] which is 
       the value of the term [t] and a semantic one given by the function in the arrow case which ensures
       closure by application. It is trivial for constants. 
       Note that [R] lives in [Set] so that we can extract it later. *)
    
    Program Fixpoint SN G T (t : term G T) { struct T } : Set :=
      match T return term G T -> Set with
        | type_cst c => fun t => { v : term G _ | normalizes t v }
        | tau --> tau' => fun t =>
          ({v : term G (tau --> tau') | normalizes t v } * 
            (forall s, SN s -> SN (@app G tau tau' t s)))%type
      end t.
    
    (** Extract the "syntactic" part. *)

    Lemma SN_eval : forall G T (t : term G T), SN t -> { v : term G T | normalizes t v }.
    Proof.
      intros.
      induction T ; simpl in * ; auto.
      destruct H ; auto.
    Qed.

    (** Backward-closedness of evaluation extends to computability. *)

    Lemma red_SN_SN : forall G T (t s : term G T), reduces t s -> SN s -> SN t.
    Proof.
      intros.
      generalize dependent G.
      induction T ; simpl ; intros.
      destruct H0.
      exists x. 
      apply eval_trans with s ; auto.
      intuition.
      destruct a.
      exists x.
      apply eval_trans with s ; auto.

      pose (red_app H s0).
      pose (b _ H0).
      apply (@IHT2 G _ _ r s1).
    Qed.

    (** All variables are in normal form. *)
    Lemma SN_rel : forall G T (v : var G T), SN (rel v).
    Proof.
      induction T.
      red ; intros.
      exists (rel v).
      constructor.

      intros.
      simpl.
      split.
      exists (rel v) ; constructor.
      intros.
    Admitted.      
      

    (** This predicate ensures [SN]-ness of all the terms in the telescope once they 
       are substituted by previous terms in the telescope. 
       It needs to be in [Set] as [SN] is in [Set]. *)

    Fixpoint substitution_SN G (s : substitution G) { struct s } : Set :=
      match s with
        | SNil => unit
        | SCons G' s' T t => (SN (mult_subst empty t s') * substitution_SN s')%type
      end.

    (** Extension of the [on_coerce_proof] tactical. *)

    Ltac on_coerce_proof tac :=
      match goal with
        [ |- ?T ] =>
        match T with
          | context [ coerce_var_context _ ?p ] => tac p
          | context [ coerce_term_context _ ?p ] => tac p
          | context [ eq_rect _ _ _ _ ?p ] => tac p
          | context [ coerce_subst_context _ ?p ] => tac p
        end
      end.
    
    (** The rest is just reinstantiation of tactics with the new [on_coerce_proof]. *)
    (* begin hide *)
    Ltac abstract_coerce_proof := on_coerce_proof 
      ltac:(fun p => let H := fresh "coerceH" in abstract_eq_hyp H p).
    Ltac abstract_coerce_proofs := repeat abstract_coerce_proof.
    
    Ltac pi_coerce_proof := on_coerce_proof ltac:(pi_eq_proof_hyp).
    Ltac pi_coerce_proofs := repeat pi_coerce_proof.

    Hint Rewrite coerce_subst_context_id : coerce_id.
    
    Ltac clear_coerce_proofs := abstract_coerce_proofs ; pi_coerce_proofs.
    
    Ltac clear_coerce_ctx := rewrite_coerce_id ; clear_coerce_proofs.

    Ltac simpl_term := 
      rew_eq_coerce ; simpl ; simpl_eqs ; clear_coerce_ctx ; clear_refl_eqs ;  
        try subst ; simpl ; repeat simpl_uip ; rewrite_coerce_id.

    Hint Rewrite eq_rect_coerce_subst : eq_rect_coerce.    


    Lemma mult_subst_comma_first : 
      forall G (s : substitution G) D T, mult_subst (D :, T) (rel (first (G; D) T)) s = rel (first D T).
    Proof.
      induction s ; intros ; simpl_term ; rew_eq_coerce ; simpl_term ; auto.
    Qed.
    (* end hide *)

    (** We can finaly prove the mult_subst lemma. *)

    (** ** Main lemma.

       A little lemma on variables is all that is missing before proving our main lemma.
       We can destruct variables, keeping the equality handy. *)

    (** We now prove the main lemma, substitutivity of [SN]. Note that we end with a closed term, 
       escaping the problem of variables. *)
    
    Program Definition SN_substitutive_stmt :=
      forall G' U (u : term G' U) G D (H : G' = G ; D) (s : substitution G),
      substitution_SN s -> SN (mult_subst D u s).
    
    Lemma SN_substitutive : SN_substitutive_stmt.
    Proof with simpl_term.
      red ; induction u ; simpl ; intros...

      (* cst *)
      exists (cst D c).
      rewrite (subst_cst c s)...
      constructor.

      (* rel *)
      generalize dependent G0.
      induction D.
      induction G ; intros.
      inversion v.

      simpl in *.
      destruct G0.
      discriminate.
      inversion H ; subst.

      pose (substitution_cons s) ; destruct_exists ; destruct_pairs.
      simpl_JMeq.
      subst.
      simpl.
      Opaque subst_rec.
      simpl_term.
      simpl in H0.
      
      destruct (var_case v).
      intuition.
      subst ; simpl_JMeq ; subst.
      Transparent subst_rec.
      simpl_term.
      assumption.

      destruct_exists.
      intuition.
      subst ; simpl_JMeq ; subst.
      simpl_term.
      pose (IHG s _ (refl_equal G0) s0 b) ; auto.
      revert s1... auto.

      (* Delta not empty *)
      intros.
      destruct G ; try discriminate.
      inversion H ; subst.
      simpl in *...
      
      destruct (var_case v).
      intuition.
      subst ; simpl_JMeq ; subst.
      rewrite mult_subst_comma_first.
      red.
      simpl.
      
      Transparent subst_rec.
      simpl_term.
      assumption.

      destruct_exists.
      intuition.
      subst ; simpl_JMeq ; subst.
      simpl_term.
      pose (IHG _ (refl_equal G0) s0 b T s) ; auto.
      revert s1... auto.
      

      (* lam *)
      simpl.
      split.

      rewrite mult_subst_lam.
      eapply exist ; constructor.

      intros.
      rewrite mult_subst_lam.

      apply red_SN_SN with (subst (mult_subst (empty :, T) u s) s0).
      apply red_beta.
      pose (@mult_subst_comm _ s empty T T' u).
      pose (s' := coerce_term_context (lift_ctx G s0) (app_empty G)).
      simpl in e.
      assert (Hs:=e s').
      clear e.
      pose (IHu (SCons s s')).
      simpl in r.
      revert r.
      simpl_term.
      intros.
      assert (s0 = mult_subst empty s' s).
      rewrite <- (mult_subst_lift s s0).
      subst s'.
      simpl_term.
      rewrite eq_rect_coerce_subst.

      clear.
      induction G ; simpl ; auto.
      simpl_term.
      simpl in *.
      simpl_term ; reflexivity.

      unfold lift.
      destruct (substitution_cons s).
      destruct_pairs ; simpl_JMeq.
      subst.
      simpl.
      simpl_term.
      rewrite subst_lift.

      unfold append in * ; fold append in *.
      pose (@coerce_term_context_lift_rec (empty ; G) empty _ (lift_ctx G s0) G t).
      simpl in e ; simpl_term.
      assert(empty ; G = G) by auto.
      rewrite (e coerceH H).
      rewrite subst_lift.
      
      apply IHG.

      rewrite H1.
      subst s'.
      rewrite Hs.
      apply r.
      split ; auto.
      rewrite <- H1.
      assumption.

      (* app *) 
      intros.
      rewrite mult_subst_app.

      assert (fR:=IHu1 _ H).
      assert (eR:=IHu2 _ H).
      
      unfold SN at 1 in fR.
      fold SN in *.
      simpl in *.
      destruct fR as [ef sf].
      destruct ef.
      apply sf.
      apply eR.

    Lemma SN_substitutive : forall G U (u : term G U) (s : substitution G),
      substitution_SN s -> SN (mult_subst empty u s).
    (* begin hide *)
    Proof with simpl.
      induction u.
      
      (* cst *)
      intros.
      rewrite subst_cst...
      simpl ; eapply exist ; constructor.

      (* rel *)
      induction G.
      inversion v.

      intros.
      pose (substitution_cons s) ; destruct_exists ; destruct_pairs.
      simpl_JMeq.
      subst.
      simpl.
      Opaque subst_rec.
      simpl_term.
      simpl in H.
      
      destruct (var_case v).
      intuition.
      subst ; simpl_JMeq ; subst.
      Transparent subst_rec.
      simpl_term.
      assumption.

      destruct_exists.
      intuition.
      subst ; simpl_JMeq ; subst.
      simpl_term.
      apply IHG ; auto.

      (* lam *)
      simpl.
      split.

      rewrite mult_subst_lam.
      eapply exist ; constructor.

      intros.
      rewrite mult_subst_lam.

      apply red_SN_SN with (subst (mult_subst (empty :, T) u s) s0).
      apply red_beta.
      pose (@mult_subst_comm _ s empty T T' u).
      pose (s' := coerce_term_context (lift_ctx G s0) (app_empty G)).
      simpl in e.
      assert (Hs:=e s').
      clear e.
      pose (IHu (SCons s s')).
      simpl in r.
      revert r.
      simpl_term.
      intros.
      assert (s0 = mult_subst empty s' s).
      rewrite <- (mult_subst_lift s s0).
      subst s'.
      simpl_term.
      rewrite eq_rect_coerce_subst.

      clear.
      induction G ; simpl ; auto.
      simpl_term.
      simpl in *.
      simpl_term ; reflexivity.

      unfold lift.
      destruct (substitution_cons s).
      destruct_pairs ; simpl_JMeq.
      subst.
      simpl.
      simpl_term.
      rewrite subst_lift.

      unfold append in * ; fold append in *.
      pose (@coerce_term_context_lift_rec (empty ; G) empty _ (lift_ctx G s0) G t).
      simpl in e ; simpl_term.
      assert(empty ; G = G) by auto.
      rewrite (e coerceH H).
      rewrite subst_lift.
      
      apply IHG.

      rewrite H1.
      subst s'.
      rewrite Hs.
      apply r.
      split ; auto.
      rewrite <- H1.
      assumption.

      (* app *) 
      intros.
      rewrite mult_subst_app.

      assert (fR:=IHu1 _ H).
      assert (eR:=IHu2 _ H).
      
      unfold SN at 1 in fR.
      fold SN in *.
      simpl in *.
      destruct fR as [ef sf].
      destruct ef.
      apply sf.
      apply eR.
    Qed.
    (* end hide *)

    (** We get weak normalization as a trivial consequence of the previous lemma and [SN_eval]. *)
    
    Lemma term_wn : forall T (t : term empty T), { v : term empty T | normalizes t v }.
    Proof.
      intros.
      cut (SN t).
      apply SN_eval.
      replace t with (mult_subst empty t SNil).
      apply SN_substitutive.
      simpl.
      constructor.
      auto.
      simpl.
      elim_eq_rect ; auto.
    Qed.

End StrongNormalization.

End L.

(** * Instantiation.

   We will now instantiate [L] with the naturals and booleans.
   Our constants are naturals or booleans of [Coq]. *)

Inductive cst_types : Set := cst_nat_t | cst_bool_t.
Inductive csts : Set :=
| cst_nat : nat -> csts
| cst_bool : bool -> csts.

Definition type_constants (cst : csts) : cst_types :=
  match cst with
    | cst_nat _ => cst_nat_t
    | cst_bool _ => cst_bool_t
  end.

Module C. 
  Definition constant_types : Set := cst_types.
  Definition constants : Set := csts.
  Definition type_constant : constants -> constant_types := type_constants.
End C.

Module LambdaC := L C. Import LambdaC.

(** We construct trivial interpretations of the naturals and booleans in [Coq]. *)

Definition interp_constant_type (cst_t : cst_types) : Set :=
  match cst_t with
    | cst_nat_t => nat
    | cst_bool_t => bool
  end.
  
Definition interp_constant (c : csts) : interp_constant_type (type_constants c) :=
  match c return interp_constant_type (type_constants c) with
    | cst_nat n => n
    | cst_bool b => b
  end.

(** Wrap interpretation using the previous functions. *)

Definition interp_nb_type := interp_type interp_constant_type.
Definition interp_nb := interp_term interp_constant.
Definition interp_closed_nb := interp_closed_term interp_constant_type interp_constant.

(** ** An example term. *)

Definition nat_type : type := type_cst cst_nat_t.

(** The identity on naturals. *)
Program Definition nat_id_term : term empty (nat_type --> nat_type) :=
  lam (rel (first empty nat_type)).

Eval compute in (interp_closed_nb nat_id_term).
Eval compute in (interp_type interp_constant_type (nat_type -->  nat_type)).

(** We can extract the term normalization function from this development. *)
Extraction "nbe.ml" term_wn.