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

Require subst0_subst0.
Require fsubst0_defs.
Require pr0_subst0.
Require pc3_defs.
Require pc3_props.

   Section pc3_fsubst0. (****************************************************)

      Lemma pc3_pr2_fsubst0: (c1:?; t1,t:?) (pr2 c1 t1 t) ->
                             (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
                             (e:?) (getl i c1 (CHead e (Bind Abbr) u)) ->
                             (pc3 c2 t2 t).
      Proof.
      Intros until 1; XElim H; Clear c1 t1 t.
(* case 1: pr2_free *)
      Intros until 2; XElim H0; Intros.
(* case 1.1: fsubst0_snd *)
      Pr0Subst0; [ XAuto | Apply (pc3_pr2_u c x); XDEAuto 3 ].
(* case 1.2: fsubst0_fst *)
      XAuto.
(* case 1.3: fsubst0_both *)
      Pr0Subst0; CSubst0GetL; [ XAuto | Apply (pc3_pr2_u c0 x); XDEAuto 3 ].
(* case 2 : pr2_delta *)
      Intros until 4; XElim H2; Intros.
(* case 2.1: fsubst0_snd. *)
      Apply (pc3_t t1); [ Apply pc3_s; XDEAuto 3 | XDEAuto 3 ].
(* case 2.2: fsubst0_fst. *)
      Apply (lt_le_e i i0); Intros; CSubst0GetL.
(* case 2.2.1: i < i0, none *)
      XDEAuto 3.
(* case 2.2.2: i < i0, csubst0_snd *)
      XInv; Subst.
      Subst0Subst0; Rewrite <- lt_plus_minus_r in H5; [ CSubst0GetL | XAuto ].
      Apply (pc3_pr2_u c0 x); XDEAuto 3.
(* case 2.2.3: i < i0, csubst0_fst *)
      XInv; Subst; Apply pc3_pr2_r; XDEAuto 2.
(* case 2.2.4: i < i0, csubst0_both *)
      XInv; Subst.
      Subst0Subst0; Rewrite <- lt_plus_minus_r in H5; [ CSubst0GetL | XAuto ].
      Apply (pc3_pr2_u c0 x); XDEAuto 3.
(* case 2.2.5: i >= i0 *)
      XDEAuto 3.
(* case 2.3: fsubst0_both *)
      Apply (lt_le_e i i0); Intros; CSubst0GetL.
(* case 2.3.1 : i < i0, none *)
      CSubst0GetL; Apply pc3_pr2_u2 with t0 := t1; XDEAuto 3.
(* case 2.3.2 : i < i0, csubst0_snd *)
      XInv; Subst.
      Subst0Subst0; Rewrite <- lt_plus_minus_r in H6; [ CSubst0GetL | XAuto ].
      Apply (pc3_pr2_u2 c0 t1); [ Idtac | Apply (pc3_pr2_u c0 x) ]; XDEAuto 3.
(* case 2.3.3: i < i0, csubst0_fst *)
      XInv; Subst.
      CSubst0GetL; Apply (pc3_pr2_u2 c0 t1); [ Idtac | Apply pc3_pr2_r ]; XDEAuto 2.
(* case 2.3.4: i < i0, csubst0_both *)
      XInv; Subst.
      Subst0Subst0; Rewrite <- lt_plus_minus_r in H6; [ CSubst0GetL | XAuto ].
      Apply (pc3_pr2_u2 c0 t1); [ Idtac | Apply (pc3_pr2_u c0 x) ]; XDEAuto 3.
(* case 2.3.5: i >= i0 *)
      CSubst0GetL; Apply (pc3_pr2_u2 c0 t1); XDEAuto 3.
      Qed.

      Hints Resolve pr3_sing : ld.

      Lemma pc3_pr2_fsubst0_back: (c1:?; t,t1:?) (pr2 c1 t t1) ->
                                  (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
                                  (e:?) (getl i c1 (CHead e (Bind Abbr) u)) ->
                                  (pc3 c2 t t2).
      Proof.
      Intros until 1; XElim H; Clear c1 t t1.
(* case 1: pr2_free *)
      Intros until 2; XElim H0; Intros.
(* case 1.1: fsubst0_snd. *)
      Apply (pc3_pr2_u c t2); XDEAuto 3.
(* case 1.2: fsubst0_fst. *)
      XAuto.
(* case 1.3: fsubst0_both. *)
      CSubst0GetL; Apply (pc3_pr2_u c0 t2); XDEAuto 3.
(* case 2: pr2_delta *)
      Intros until 4; XElim H2; Intros.
(* case 2.1: fsubst0_snd. *)
      Apply (pc3_t t2); Apply pc3_pr3_r; XDEAuto 5.
(* case 2.2: fsubst0_fst. *)
      Apply (lt_le_e i i0); Intros; CSubst0GetL.
(* case 2.2.1: i < i0, none *)
      XDEAuto 3.
(* case 2.2.2: i < i0, csubst0_bind *)
      XInv; Subst.
      Subst0Subst0; Rewrite <- lt_plus_minus_r in H5; [ CSubst0GetL | XAuto ].
      Apply (pc3_pr2_u c0 x); XDEAuto 3.
(* case 2.2.3: i < i0, csubst0_fst *)
      XInv; Subst; Apply pc3_pr2_r; XDEAuto 2.
(* case 2.2.4: i < i0, csubst0_both *)
      XInv; Subst.
      Subst0Subst0; Rewrite <- lt_plus_minus_r in H5; [ CSubst0GetL | XAuto ].
      Apply (pc3_pr2_u c0 x); XDEAuto 3.
(* case 2.2.5: i >= i0 *)
      XDEAuto 3.
(* case 2.3: fsubst0_both *)
      Apply (lt_le_e i i0); Intros; CSubst0GetL.
(* case 2.3.1 : i < i0, none *)
      CSubst0GetL; Apply pc3_pr2_u with t2:=t2; Try Apply pc3_pr3_r; XDEAuto 5.
(* case 2.3.2 : i < i0, csubst0_snd *)
      XInv; Subst.
      Subst0Subst0; Rewrite <- lt_plus_minus_r in H6; [ CSubst0GetL | XAuto ].
      Apply (pc3_pr2_u c0 x); [ Idtac | Apply (pc3_pr2_u2 c0 t) ]; XDEAuto 3.
(* case 2.3.3: i < i0, csubst0_fst *)
      XInv; Subst.
      CSubst0GetL; Apply (pc3_pr2_u c0 t); [ Idtac | Apply pc3_pr2_r ]; XDEAuto 2.
(* case 2.3.4: i < i0, csubst0_both *)
      XInv; Subst.
      Subst0Subst0; Rewrite <- lt_plus_minus_r in H6; [ CSubst0GetL | XAuto ].
      Apply (pc3_pr2_u c0 x); [ Idtac | Apply (pc3_pr2_u2 c0 t) ]; XDEAuto 3.
(* case 2.3.5: i >= i0 *)
      CSubst0GetL; Apply (pc3_pr2_u c0 t); XDEAuto 3.
      Qed.

      Opaque pc3.

      Lemma pc3_fsubst0: (c1:?; t1,t:?) (pc3 c1 t1 t) ->
                         (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
                         (e:?) (getl i c1 (CHead e (Bind Abbr) u)) ->
                         (pc3 c2 t2 t).
      Proof.
      Intros until 1; XElimUsing pc3_ind_left H.
(* case 1: pc3_refl *)
      Intros until 1; XElim H; Intros; Try CSubst0GetL; XDEAuto 3.
(* case 2: pc3_pr2_u *)
      Intros until 4; XElim H2; Intros;
      (Apply (pc3_t t2); [ EApply pc3_pr2_fsubst0; XDEAuto 2 | XDEAuto 3 ]).
(* case 2: pc3_pr2_u2 *)
      Intros until 4; XElim H2; Intros;
      (Apply (pc3_t t0); [ Apply pc3_s; EApply pc3_pr2_fsubst0_back; XDEAuto 2 | XDEAuto 3 ]).
      Qed.

   End pc3_fsubst0.