(****************************************************************************)
(*                                                                          *)
(*                The formal system \lambda\delta                           *)
(*                                                                          *)
(*                Author: Ferruccio Guidi                                   *)
(*                                                                          *)
(*                This file is distributed under the terms of the           *)
(*                GNU General Public License Version 2                      *)
(*                                                                          *)
(****************************************************************************)

Require Export subst0_defs.

      Fixpoint subst [d:nat; v,t:T] : T := Cases t of
         | (TSort n)     => (TSort n)
         | (TLRef i)     =>
            if (blt i d) then (TLRef i) else
            if (blt d i) then (TLRef (pred i)) else (lift d (0) v)
         | (THead k u t) =>
            (THead k (subst d v u) (subst (s k d) v t))
      end.

   Section subst2_rw. (******************************************************)

      Lemma subst_sort: (v:?; d,k:?) (subst d v (TSort k)) = (TSort k).
      Proof.
      XAuto.
      Qed.

      Lemma subst_lref_lt: (v:?; d,i:?) (lt i d) ->
                           (subst d v (TLRef i)) = (TLRef i).
      Proof.
      Intros; Simpl; Rewrite lt_blt; XAuto.
      Qed.

      Lemma subst_lref_eq: (v:?; i:?)
                           (subst i v (TLRef i)) = (lift i (0) v).
      Proof.
      Intros; Simpl; Rewrite le_bge; XAuto.
      Qed.

      Hints Resolve lt_le_weak : ld.

      Lemma subst_lref_gt: (v:?; d,i:?) (lt d i) ->
                           (subst d v (TLRef i)) = (TLRef (pred i)).
      Proof.
      Intros; Simpl; Rewrite le_bge; [ Idtac | XAuto ].
      Rewrite lt_blt; XAuto.
      Qed.

      Lemma subst_head: (k:?; w,u,t:?; d:?)
                        (subst d w (THead k u t)) =
                        (THead k (subst d w u) (subst (s k d) w t)).
      Proof.
      XAuto.
      Qed.

   End subst2_rw.

   Section subst_base_props. (***********************************************)

      Hints Resolve sym_eq : ld.

      Lemma subst_lift_SO: (v,t:?; d:?) (subst d v (lift (1) d t)) = t.
      Proof.
      XElim t; Intros.
(* case 1: TSort *)
      Rewrite lift_sort; Rewrite subst_sort; XAuto.
(* case 2: TLRef *)
      Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
      Rewrite lift_lref_lt; Try Rewrite subst_lref_lt; XAuto.
(* case 2.2: n >= d *)
      Rewrite lift_lref_ge; [ Rewrite <- plus_n_Sm | XAuto ].
      Rewrite subst_lref_gt; Try Rewrite <- pred_Sn; XAuto.
(* case 3: THead *)
      Rewrite lift_head; Rewrite subst_head; XAuto.
      Qed.

   End subst_base_props.