(****************************************************************************)
(*                                                                          *)
(*                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_gen.
Require lift_props.
Require subst0_defs.

   Section subst0_gen_lift_lt. (*********************************************)

      Tactic Definition IH := (
         Match Context With
            | [ H1: (x:?; i,h,d:?) (subst0 i (lift h d ?1) (lift h (S (plus i d)) ?2) x) -> ?;
                H2: (subst0 ?3 (lift ?4 ?5 ?1) (lift ?4 (S (plus ?3 ?5)) ?2) ?6) |- ? ] ->
               LApply (H1 ?6 ?3 ?4 ?5); [ Clear H1 H2; Intros H1 | XAuto ];
               XElim H1; Intros
         ).

      Lemma subst0_gen_lift_lt: (u,t1,x:?; i,h,d:?) (subst0 i (lift h d u) (lift h (S (plus i d)) t1) x) ->
                                (EX t2 | x = (lift h (S (plus i d)) t2) & (subst0 i u t1 t2)).
      Proof.
      XElim t1; Intros.
(* case 1: TSort *)
      Rewrite lift_sort in H; Subst0GenBase.
(* case 2: TLRef n *)
      Apply (lt_le_e n (S (plus i d))); Intros.
(* case 2.1: n < 1 + i + d *)
      Rewrite lift_lref_lt in H; [ Idtac | XAuto ].
      Subst0GenBase; Rewrite H1; Rewrite H.
      Rewrite <- lift_d; Simpl; XDEAuto 2.
(* case 2.2: n >= 1 + i + d *)
      Rewrite lift_lref_ge in H; [ Idtac | XAuto ].
      Subst0GenBase; Rewrite <- H in H0.
      EApply le_false; [ Idtac | Apply H0 ]; XAuto.
(* case 3: THead k *)
      Rewrite lift_head in H1; Subst0GenBase; Rewrite H1; Clear H1 x.
(* case 3.1: subst0_fst *)
      IH; Rewrite H; Rewrite <- lift_head; XDEAuto 3.
(* case 3.2: subst0_snd *)
      SRwIn H2; IH; Rewrite H0; SRwBack; Rewrite <- lift_head; XDEAuto 3.
(* case 3.2: subst0_snd *)
      SRwIn H3; Repeat IH; Rewrite H; Rewrite H0; SRwBack;
      Rewrite <- lift_head; XDEAuto 3.
      Qed.

   End subst0_gen_lift_lt.

   Section subst0_gen_lift_false. (******************************************)

      Hints Resolve lt_le_S simpl_lt_plus_r : ld.

      Lemma subst0_gen_lift_false: (t,u,x:?; h,d,i:?)
                                   (le d i) -> (lt i (plus d h)) ->
                                   (subst0 i u (lift h d t) x) ->
                                   (P:Prop) P.
      Proof.
      XElim t; Intros.
(* case 1: TSort *)
      Rewrite lift_sort in H1; Subst0GenBase.
(* case 2: TLRef n *)
      Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
      Rewrite lift_lref_lt in H1; [ Idtac | XAuto ].
      Subst0GenBase; Rewrite H1 in H2.
      EApply le_false; [ Apply H | XAuto ].
(* case 2.2: n >= d *)
      Rewrite lift_lref_ge in H1; [ Idtac | XAuto ].
      Subst0GenBase; Rewrite <- H1 in H0.
      EApply le_false; [ Apply H2 | XDEAuto 3 ].
(* case 3: THead k *)
      Rewrite lift_head in H3; Subst0GenBase.
(* case 3.1: subst0_fst *)
      EApply H; XDEAuto 2.
(* case 3.2: subst0_snd *)
      EApply H0; [ Idtac | Idtac | XDEAuto 2 ]; [ Idtac | SRwBack ]; XAuto.
(* case 3.3: subst0_both *)
      EApply H; XDEAuto 2.
      Qed.

   End subst0_gen_lift_false.

   Section subst0_gen_lift_ge. (*********************************************)

      Hints Resolve le_trans_plus_r : ld.

      Tactic Definition IH := (
         Match Context With
            | [ H1: (x:?; i,h,d:?) (subst0 i ?1 (lift h d ?2) x) -> ?;
                H2: (subst0 ?3 ?1 (lift ?4 ?5 ?2) ?6) |- ? ] ->
               LApply (H1 ?6 ?3 ?4 ?5); [ Clear H1 H2; Intros H1 | XAuto ];
               LApply H1; [ Clear H1; Intros H1 | SRwBack; XAuto ];
               XElim H1; Intros
         ).

      Lemma subst0_gen_lift_ge: (u,t1,x:?; i,h,d:?) (subst0 i u (lift h d t1) x) ->
                                (le (plus d h) i) ->
                                (EX t2 | x = (lift h d t2) & (subst0 (minus i h) u t1 t2)).
      Proof.
      XElim t1; Intros.
(* case 1: TSort *)
      Rewrite lift_sort in H; Subst0GenBase.
(* case 2: TLRef n *)
      Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
      Rewrite lift_lref_lt in H; [ Idtac | XAuto ].
      Subst0GenBase; Rewrite H in H1.
      EApply le_false; [ Apply H0 | XAuto ].
(* case 2.2: n >= d *)
      Rewrite lift_lref_ge in H; [ Idtac | XAuto ].
      Subst0GenBase; Rewrite <- H; Rewrite H2.
      Rewrite minus_plus_r.
      EApply ex2_intro; [ Idtac | XAuto ].
      Rewrite lift_free; [ Idtac | XDEAuto 4 (**) | XAuto ].
      Rewrite plus_sym; Rewrite plus_n_Sm; XAuto.
(* case 3: THead k *)
      Rewrite lift_head in H1; Subst0GenBase; Rewrite H1; Clear H1 x;
      Repeat IH; Try Rewrite H; Try Rewrite H0;
      Rewrite <- lift_head; Try Rewrite <- s_minus in H1; XDEAuto 3.
      Qed.

   End subst0_gen_lift_ge.

   Section subst0_gen_lift_rev_ge. (*****************************************)

      Hints Resolve le_trans le_minus : ld.

      Lemma subst0_gen_lift_rev_ge: (t1,v,u2:?; i,h,d:?)
                                    (subst0 i v t1 (lift h d u2)) ->
                                    (le (plus d h) i) ->
                                    (EX u1 | (subst0 (minus i h) v u1 u2) &
                                             t1 = (lift h d u1)
                                    ).
      Proof.
      XElim t1; Intros; Subst0GenBase; Subst.
(* case 1: subst0_lref *)
      Pattern 2 n; Rewrite (le_plus_minus_sym h n); [ Idtac | XDEAuto 2 ].
      Rewrite <- lift_lref_ge with d:=d; [ Idtac | XAuto ].
      Rewrite (le_plus_minus h n) in H1; [ Idtac | XDEAuto 2 ].
      Rewrite plus_n_Sm in H1.
      Rewrite <- lift_free with e:=d in H1; [ Idtac | Simpl; XDEAuto 3 | XAuto ].
      LiftGen; Subst; XDEAuto 2.
(* case 2: subst0_fst *)
      Clear H0; SymEqual; LiftXGenBase.
      XDecomPoseClear H '(H ? ? ? ? ? H3 H2); Clear H3 H2; Subst.
      Rewrite <- lift_head; XDEAuto 3.
(* case 3: subst0_snd *)
      Clear H; SymEqual; LiftXGenBase.
      XPoseClear H0 '(H0 ? ? ? ? ? H3); Clear H3.
      SRwBackIn H0; Rewrite <- s_minus in H0; [ Idtac | XDEAuto 2 ].
      XLApply H0; XDecompose H0; Subst.
      Rewrite <- lift_head; XDEAuto 3.
(* case 4: subst0_both *)
      SymEqual; LiftXGenBase.
      XDecomPoseClear H '(H ? ? ? ? ? H3 H2); Clear H3; Subst.
      XPoseClear H0 '(H0 ? ? ? ? ? H4); Clear H4.
      SRwBackIn H0; Rewrite <- s_minus in H0; [ Idtac | XDEAuto 2 ].
      XLApply H0; XDecompose H0; Subst.
      Rewrite <- lift_head; XDEAuto 3.
      Qed.

   End subst0_gen_lift_rev_ge.

      Tactic Definition Subst0Gen := (
         Match Context With
            | [ H: (subst0 ?0 (lift ?1 ?2 ?3) (lift ?1 (S (plus ?0 ?2)) ?4) ?5) |- ? ] ->
               LApply (subst0_gen_lift_lt ?3 ?4 ?5 ?0 ?1 ?2); [ Clear H; Intros H | XAuto ];
               XElim H; Intros
            | [ H: (subst0 ?0 ?1 (lift (1) ?0 ?2) ?3) |- ? ] ->
               LApply (subst0_gen_lift_false ?2 ?1 ?3 (1) ?0 ?0); [ Intros H_x | XAuto ];
               LApply H_x; [ Clear H_x; Intros H_x | Rewrite plus_sym; XAuto ];
               LApply H_x; [ Clear H H_x; Intros H | XAuto ];
               Apply H
            | [ _: (le ?1 ?2); _: (lt ?2 (plus ?1 ?3));
                _: (subst0 ?2 ?4 (lift ?3 ?1 ?5) ?6) |- ? ] ->
               Apply (subst0_gen_lift_false ?5 ?4 ?6 ?3 ?1 ?2); XAuto
            | [ _: (subst0 ?1 ?2 (lift (S ?1) (0) ?3) ?4) |- ? ] ->
               Apply (subst0_gen_lift_false ?3 ?2 ?4 (S ?1) (0) ?1); XAuto
            | [ H: (subst0 ?1 ? (lift ?2 (0) ?) ?) |- ? ] ->
               Apply (lt_le_e ?1 ?2);
               [ Intros; EApply subst0_gen_lift_false;
                 [ Idtac | Idtac | EApply H ]; XAuto
               | Intros Hle;
                 XDecomPoseClear H '(subst0_gen_lift_ge ? ? ? ? ? ? H Hle);
                 Subst
               ]
            | [ H: (subst0 ?0 ?1 (lift ?2 ?3 ?4) ?5) |- ? ] ->
               LApply (subst0_gen_lift_ge ?1 ?4 ?5 ?0 ?2 ?3); [ Clear H; Intros H | XAuto ];
               LApply H; [ Clear H; Intros H | Simpl; XAuto ];
               XElim H; Intros
            | [ |- ? ] -> Subst0GenBase
         ).