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

Require tlt_defs.
Require lift_defs.

   Section lift_tlt_props. (*************************************************)

      Lemma lift_weight_map: (t:?; h,d:?; f:?)
                             ((m:?) (le d m) -> (f m)=(0)) ->
                             (weight_map f (lift h d t)) = (weight_map f t).
      Proof.
      XElim t; Intros.
(* case 1: TSort *)
      XAuto.
(* case 2: TLRef n *)
      Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
      Rewrite lift_lref_lt; XAuto.
(* case 2.2: n >= d *)
      Rewrite lift_lref_ge; [ Simpl | XAuto ].
      Rewrite (H n); XAuto.
(* case 3: THead k *)
      XElim k; Intros; LiftHeadRw; Simpl.
(* case 3.1: Bind *)
      XElim b; [ Rewrite H; [ Idtac | XAuto ] | Idtac | Idtac ];
      Rewrite H0; Intros; Try (LeLtGen; Rewrite H2; Simpl); XAuto.
(* case 3.2: Flat *)
      XAuto.
      Qed.

      Hints Resolve lift_weight_map : ld.

      Lemma lift_weight: (t:?; h,d:?) (weight (lift h d t)) = (weight t).
      Proof.
      Unfold weight; XAuto.
      Qed.

      Hints Resolve sym_equal : ld.

      Lemma lift_weight_add: (w:?; t:?; h,d:?; f,g:?)
                             ((m:?) (lt m d) -> (g m) = (f m)) ->
                             (g d) = w ->
                             ((m:?) (le d m) -> (g (S m)) = (f m)) ->
                             (weight_map f (lift h d t)) =
                             (weight_map g (lift (S h) d t)).
      Proof.
      XElim t; Intros.
(* case 1: TSort *)
      XAuto.
(* case 2: TLRef *)
      Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
      Repeat Rewrite lift_lref_lt; Simpl; XAuto.
(* case 2.2: n >= d *)
      Repeat Rewrite lift_lref_ge; Simpl; Try Rewrite <- plus_n_Sm; XAuto.
(* case 3: THead k *)
      XElim k; Intros; LiftHeadRw; Simpl.
(* case 1 : bind b *)
      XElim b; Simpl;
      Apply (f_equal nat);
      (Apply (f_equal2 nat nat); [ XAuto | Idtac ]);
      ( Apply H0; Simpl; Intros; Try (LeLtGen; Rewrite H4; Simpl); XAuto).
(* case 2 : Flat *)
      XAuto.
      Qed.

      Lemma lift_weight_add_O: (w:?; t:?; h:?; f:?)
                               (weight_map f (lift h (0) t)) =
                               (weight_map (wadd f w) (lift (S h) (0) t)).
      Proof.
      Intros.
      EApply lift_weight_add; XAuto.
      Intros; LeLtGen.
      Qed.

      Lemma lift_tlt_dx: (k:?; u,t:?; h,d:?)
                         (tlt t (THead k u (lift h d t))).
      Proof.
      Unfold tlt; Intros.
      Rewrite <- (lift_weight t h d).
      Fold (tlt (lift h d t) (THead k u (lift h d t))); XAuto.
      Qed.

   End lift_tlt_props.

      Hints Resolve lift_tlt_dx : ld.