(****************************************************************************)
(*                                                                          *)
(*                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_props.
Require getl_props.
Require pc3_props.
Require ty3_defs.

   Section ty3_lift. (*******************************************************)

      Hints Resolve le_S_n ty3_conv : ld.

      Lemma ty3_lift: (g:?; e:?; t1,t2:?) (ty3 g e t1 t2) ->
                      (c:?; d,h:?) (drop h d c e) ->
                      (ty3 g c (lift h d t1) (lift h d t2)).
      Proof.
      Intros until 1; XElim H; Intros.
(* case 1: ty3_conv *)
      XDEAuto 5.
(* case 2: ty3_sort *)
      Repeat Rewrite lift_sort; XAuto.
(* case 3: ty3_abbr *)
      Apply (lt_le_e n d0); Intros; GetLDis.
(* case 3.1: n < d0 *)
      Rewrite minus_x_Sy in H2; [ Idtac | XAuto ].
      DropClear; Rewrite lift_lref_lt; [ Idtac | XAuto ].
      Arith8 d0 '(S n); Rewrite lift_d; [ Arith8' d0 '(S n) | XAuto ].
      EApply ty3_abbr; XDEAuto 2.
(* case 3.2: n >= d0 *)
      Rewrite lift_lref_ge; [ Idtac | XAuto ].
      Arith7' n; Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
      Rewrite (plus_sym h (S n)); Simpl; XDEAuto 2.
(* case 4: ty3_abst *)
      Apply (lt_le_e n d0); Intros; GetLDis.
(* case 4.1: n < d0 *)
      Rewrite minus_x_Sy in H2; [ Idtac | XAuto ].
      DropClear; Rewrite lift_lref_lt; [ Idtac | XAuto ].
      Arith8 d0 '(S n); Rewrite lift_d; [ Arith8' d0 '(S n) | XAuto ].
      EApply ty3_abst; XDEAuto 2.
(* case 4.2: n >= d0 *)
      Rewrite lift_lref_ge; [ Idtac | XAuto ].
      Arith7' n; Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
      Rewrite (plus_sym h (S n)); Simpl; XDEAuto 2.
(* case 5: ty3_bind *)
      LiftHeadRw; Simpl; EApply ty3_bind; XDEAuto 3.
(* case 6: ty3_appl *)
      LiftHeadRw; Simpl; EApply ty3_appl; [ Idtac | Rewrite <- lift_bind ]; XDEAuto 2.
(* case 7: ty3_cast *)
      LiftHeadRw; XDEAuto 4.
      Qed.

   End ty3_lift.

      Hints Resolve ty3_lift : ld.

      Tactic Definition Ty3Lift b u := (
         Match Context With
            | [ H: (ty3 ?1 ?2 ?3 ?4) |- ? ] ->
               LApply (ty3_lift ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
               LApply (H_x (CHead ?2 (Bind b) u) (0) (1)); [ Clear H_x; Intros | XAuto ]
         ).