(****************************************************************************)
(*                                                                          *)
(*                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 lift_defs.

      Fixpoint trans [hds:PList] : nat -> nat :=
         [i:?] Cases hds of
            | PNil            => i
            | (PCons h d hds) =>
                 let j = (trans hds i) in
                 if (blt j d) then j else (plus j h)
         end.

      Fixpoint lift1 [hds:PList] : T -> T :=
         [t:?] Cases hds of
            | PNil            => t
            | (PCons h d hds) => (lift h d (lift1 hds t))
      end.

      Fixpoint lifts1 [hds:PList; ts:TList] : TList :=
         Cases ts of
            | TNil         => TNil
            | (TCons t ts) => (TCons (lift1 hds t) (lifts1 hds ts))
         end.

   Section lift1_rw. (*******************************************************)

      Lemma lift1_sort: (n:?; is:?) (lift1 is (TSort n)) = (TSort n).
      Proof.
      XElim is; Intros; Simpl; Try Rewrite H; XAuto.
      Qed.

      Lemma lift1_lref: (hds:?; i:?)
                        (lift1 hds (TLRef i)) = (TLRef (trans hds i)).
      Proof.
      XElim hds; Intros; Simpl; Try Rewrite H; XAuto.
      Qed.

      Lemma lift1_bind: (b:?; hds:?; u,t:?)
                        (lift1 hds (THead (Bind b) u t)) =
                        (THead (Bind b) (lift1 hds u) (lift1 (Ss hds) t)).
      Proof.
      XElim hds; Intros; Simpl; Try Rewrite H; Try Rewrite lift_bind; XAuto.
      Qed.

      Lemma lift1_flat: (f:?; hds:?; u,t:?)
                        (lift1 hds (THead (Flat f) u t)) =
                        (THead (Flat f) (lift1 hds u) (lift1 hds t)).
      Proof.
      XElim hds; Intros; Simpl; Try Rewrite H; Try Rewrite lift_flat; XAuto.
      Qed.

      Lemma lift1_cons_tail: (t:?; h,d:?; hds:?)
                             (lift1 (PConsTail hds h d) t) = (lift1 hds (lift h d t)).
      Proof.
      XElim hds; Simpl; Intros; Try Rewrite H; XAuto.
      Qed.

   End lift1_rw.

   Section lift1_props_base.

      Lemma lift1_lift1: (is1,is2:?; t:?)
                         (lift1 is1 (lift1 is2 t)) = (lift1 (papp is1 is2) t).
      Proof.
      XElim is1; Intros; Simpl; XAuto.
      Qed.

   End lift1_props_base.

   Section lifts1_rw. (******************************************************)

      Lemma lifts1_flat: (f:?; hds:?; t:?; ts:?)
                         (lift1 hds (THeads (Flat f) ts t)) =
                         (THeads (Flat f) (lifts1 hds ts) (lift1 hds t)).
      Proof.
      XElim ts; Intros; Simpl; Try Rewrite lift1_flat; Try Rewrite H; XAuto.
      Qed.

      Lemma lifts1_nil: (ts:?) (lifts1 PNil ts) = ts.
      Proof.
      XElim ts; Simpl; Intros; Try Rewrite H; XAuto.
      Qed.

      Lemma lifts1_cons: (h,d:?; hds:?; ts:?)
                         (lifts1 (PCons h d hds) ts) = (lifts h d (lifts1 hds ts)).
      Proof.
      XElim ts; Simpl; Intros; Try Rewrite H; XAuto.
      Qed.

   End lifts1_rw.