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

Require lift_defs.

   Section lift_props. (*****************************************************)

      Hints Resolve le_trans lt_le_trans : ld.

      Hint discr : ld := Extern 4 (le ? (plus (s ? ?) ?)) SRwBack.

      Lemma lift_free: (t:?; h,k,d,e:?) (le e (plus d h)) -> (le d e) ->
                       (lift k e (lift h d t)) = (lift (plus k h) d t).
      Proof.
      XElim t; Intros.
(* case 1: TSort *)
      Repeat Rewrite lift_sort; XAuto.
(* case 2: TLRef n *)
      Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
      Repeat Rewrite lift_lref_lt; XDEAuto 2.
(* case 2.2: n >= d *)
      Repeat Rewrite lift_lref_ge; XDEAuto 3.
(* case 3: THead k *)
      LiftHeadRw; XAuto.
      Qed.

      Lemma lift_free_sym: (t:?; h,k,d,e:?) (le e (plus d h)) -> (le d e) ->
                           (lift k e (lift h d t)) = (lift (plus h k) d t).
      Proof.
      Intros; Rewrite plus_sym; Apply lift_free; XAuto.
      Qed.

      Lemma lift_d: (t:?; h,k,d,e:?) (le e d) ->
                    (lift h (plus k d) (lift k e t)) = (lift k e (lift h d t)).
      Proof.
      XElim t; Intros.
(* case 1: TSort *)
      Repeat Rewrite lift_sort; XAuto.
(* case 2: TLRef n *)
      Apply (lt_le_e n e); Intros.
(* case 2.1: n < e *)
      Cut (lt n d); Intros; Repeat Rewrite lift_lref_lt; XDEAuto 2.
(* case 2.2: n >= e *)
      Rewrite lift_lref_ge; [ Idtac | XAuto ].
      Rewrite plus_sym; Apply (lt_le_e n d); Intros.
(* case 2.2.1: n < d *)
      Do 2 (Rewrite lift_lref_lt; [ Idtac | XAuto ]).
      Rewrite lift_lref_ge; XAuto.
(* case 2.2.2: n >= d *)
      Repeat Rewrite lift_lref_ge; XAuto.
(* case 3: THead k *)
      LiftHeadRw; SRw; XAuto.
      Qed.

   End lift_props.