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

   Section sty0_props. (*****************************************************)

      Hints Resolve le_S_n : ld.

      Lemma sty0_lift: (g:?; e:?; t1,t2:?) (sty0 g e t1 t2) ->
                       (c:?; h,d:?) (drop h d c e) ->
                       (sty0 g c (lift h d t1) (lift h d t2)).
      Proof.
      Intros until 1; XElim H; Clear e t1 t2; Intros.
(* case 1: sty0_sort *)
      Repeat Rewrite lift_sort; XAuto.
(* case 2: sty0_abbr *)
      Apply (lt_le_e i d0); Intros; GetLDis.
(* case 2.1: n < d0 *)
      Rewrite minus_x_Sy in H2; [ Idtac | XAuto ].
      DropClear; Rewrite lift_lref_lt; [ Idtac | XAuto ].
      Arith8 d0 '(S i); Rewrite lift_d; [ Arith8' d0 '(S i) | XAuto ].
      XDEAuto 4.
(* case 2.2: n >= d0 *)
      Rewrite lift_lref_ge; [ Idtac | XAuto ].
      Arith7' i; Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
      Rewrite (plus_sym h (S i)); Simpl; XDEAuto 2.
(* case 3: sty0_abst *)
      Apply (lt_le_e i 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 i); Rewrite lift_d; [ Arith8' d0 '(S i) | XAuto ].
      XDEAuto 4.
(* case 3.2: n >= d0 *)
      Rewrite lift_lref_ge; [ Idtac | XAuto ].
      Arith7' i; Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
      Rewrite (plus_sym h (S i)); Simpl; XDEAuto 2.
(* case 4: sty0_bind *)
      LiftHeadRw; Simpl; XDEAuto 4.
(* case 5: sty0_appl *)
      LiftHeadRw; XDEAuto 3.
(* case 6: sty0_cast *)
      LiftHeadRw; XDEAuto 4.
      Qed.

      Hints Resolve sty0_lift: ld.

      Lemma sty0_correct: (g:?; c:?; t1, t:?) (sty0 g c t1 t) ->
                          (EX t2 | (sty0 g c t t2)).
      Proof.
      Intros until 1; XElim H; Clear c t1 t; Intros.
(* case 1: sty0_sort *)
      XDEAuto 2.
(* case 2: sty0_abbr *)
      XDecompose H1; GetLDrop; XDEAuto 3.
(* case 3: sty0_abst *)
      XDecompose H1; GetLDrop; XDEAuto 3.
(* case 4: sty0_bind *)
      XDecompose H0; XDEAuto 3.
(* case 5: sty0_appl *)
      XDecompose H0; XDEAuto 3.
(* case 6: sty0_cast *)
      XDecompose H0; XDecompose H2; XDEAuto 3.
      Qed.

   End sty0_props.

      Hints Resolve sty0_lift: ld.