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

      Tactic Definition IH := (
         Match Context With
            | [ H1: (lift ?1 ?2 t) = (lift ?1 ?2 ?3) |- ? ] ->
               LApply (H ?3 ?1 ?2); [ Clear H H1; Intros | XAuto ]
            | [ H1: (lift ?1 ?2 t0) = (lift ?1 ?2 ?3) |- ? ] ->
               LApply (H0 ?3 ?1 ?2); [ Clear H0 H1; Intros | XAuto ]
         ).

      Hints Resolve sym_eq : ld.

      Lemma lift_inj : (x,t:?; h,d:?) (lift h d x) = (lift h d t) -> x = t.
      Proof.
      XElim x.
(* case 1 : TSort *)
      Intros; Rewrite lift_sort in H; LiftGenBase; XAuto.
(* case 2 : TLRef n *)
      Intros; Apply (lt_le_e n d); Intros.
(* case 2.1 : n < d *)
      Rewrite lift_lref_lt in H; [ LiftGenBase; XAuto | XAuto ].
(* case 2.2 : n >= d *)
      Rewrite lift_lref_ge in H; [ LiftGenBase; XAuto | XAuto ].
(* case 3 : THead k *)
      XElim k; Intros; [ Rewrite lift_bind in H1 | Rewrite lift_flat in H1 ];
      LiftGenBase; Rewrite H1; IH; IH; XAuto.
      Qed.

   End lift_ini.

   Section lift_gen_lift. (**************************************************)

      Tactic Definition IH := (
         Match Context With
            | [ H_x: (lift ?0 ?1 t) = (lift ?2 (plus ?3 ?0) ?4) |- ? ] ->
               LApply (H ?4 ?0 ?2 ?1 ?3); [ Clear H; Intros H | XAuto ];
               LApply H; [ Clear H H_x; Intros H | XAuto ];
               XElim H; Intros
            | [ H_x: (lift ?0 ?1 t0) = (lift ?2 (plus ?3 ?0) ?4) |- ? ] ->
               LApply (H0 ?4 ?0 ?2 ?1 ?3); [ Clear H0; Intros H0 | XAuto ];
               LApply H0; [ Clear H0 H_x; Intros H0 | XAuto ];
               XElim H0; Intros
         ).

      Hints Resolve sym_eq le_trans lt_le_trans le_minus : ld.

      Lemma lift_gen_lift: (t1,x:?; h1,h2,d1,d2:?) (le d1 d2) ->
                           (lift h1 d1 t1) = (lift h2 (plus d2 h1) x) ->
                           (EX t2 | x = (lift h1 d1 t2) &
                                    t1 = (lift h2 d2 t2)
                           ).
      Proof.
      XElim t1; Intros.
(* case 1 : TSort *)
      Rewrite lift_sort in H0.
      LiftGenBase; Rewrite H0; Clear H0 x.
      EApply ex2_intro; Rewrite lift_sort; XAuto.
(* case 2 : TLRef n *)
      Apply (lt_le_e n d1); Intros.
(* case 2.1 : n < d1 *)
      Rewrite lift_lref_lt in H0; [ Idtac | XAuto ].
      LiftGenBase; Rewrite H0; Clear H0 x.
      EApply ex2_intro; Rewrite lift_lref_lt; XDEAuto 2.
(* case 2.2 : n >= d1 *)
      Rewrite lift_lref_ge in H0; [ Idtac | XAuto ].
      Apply (lt_le_e n d2); Intros.
(* case 2.2.1 : n < d2 *)
      LiftGenBase; Rewrite H0; Clear H0 x.
      EApply ex2_intro; [ Rewrite lift_lref_ge | Rewrite lift_lref_lt ]; XDEAuto 2.
(* case 2.2.2 : n >= d2 *)
      Apply (lt_le_e n (plus d2 h2)); Intros.
(* case 2.2.2.1 : n < d2 + h2 *)
      EApply lift_gen_lref_false; [ Idtac | Idtac | Apply H0 ];
      [ XAuto | Rewrite plus_permute_2_in_3; XAuto ].
(* case 2.2.2.2 : n >= d2 + h2 *)
      Rewrite (le_plus_minus_sym h2 (plus n h1)) in H0; [ Idtac | XDEAuto 3 ].
      LiftGenBase; Rewrite H0; Clear H0 x.
      EApply ex2_intro;
      [ Rewrite le_minus_plus; [ Idtac | XDEAuto 2 ]
      | Rewrite (le_plus_minus_sym h2 n); [ Idtac | XDEAuto 2 ] ];
      Rewrite lift_lref_ge; XDEAuto 4.
(* case 3 : THead k *)
      NewInduction k.
(* case 3.1 : Bind *)
      Rewrite lift_bind in H2.
      LiftGenBase; Rewrite H2; Clear H2 x.
      IH; Rewrite H; Rewrite H2; Clear H H2 x0.
      Arith4In H4 d2 h1; IH; Rewrite H; Rewrite H0; Clear H H0 x1 t t0.
      EApply ex2_intro; Rewrite lift_bind; XAuto.
(* case 3.2 : Flat *)
      Rewrite lift_flat in H2.
      LiftGenBase; Rewrite H2; Clear H2 x.
      IH; Rewrite H; Rewrite H2; Clear H H2 x0.
      IH; Rewrite H; Rewrite H0; Clear H H0 x1 t t0.
      EApply ex2_intro; Rewrite lift_flat; XAuto.
      Qed.

   End lift_gen_lift.

      Tactic Definition LiftGen := (
         Match Context With
            | [ H: (lift ?1 ?2 ?3) = (lift ?1 ?2 ?4) |- ? ] ->
               LApply (lift_inj ?3 ?4 ?1 ?2); [ Clear H; Intros | XAuto ]
            | [ H: (lift ?0 ?1 ?2) = (lift ?3 (plus ?4 ?0) ?5) |- ? ] ->
               LApply (lift_gen_lift ?2 ?5 ?0 ?3 ?1 ?4); [ Intros H_x | XAuto ];
               LApply H_x; [ Clear H H_x; Intros H | XAuto ];
               XElim H; Intros
            | [ H: (lift (1) (0) ?1) = (lift (1) (S ?2) ?3) |- ? ] ->
               LApply (lift_gen_lift ?1 ?3 (1) (1) (0) ?2); [ Intros H_x | XAuto ];
               LApply H_x; [ Clear H_x H; Intros H | Arith7' ?2; XAuto ];
               XElim H; Intros
            | [ |- ? ] -> LiftGenBase
         ).

   Section lifts_inj. (******************************************************)

      Lemma lifts_inj: (xs,ts:?; h,d:?)
                       (lifts h d xs) = (lifts h d ts) -> xs = ts.
      Proof.
      XElim xs; XElim ts; Simpl; Intros; XInv; Try LiftGen; Subst; XDEAuto 3.
      Qed.

   End lifts_inj.