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

Require getl_props.
Require csubst0_defs.
Require fsubst0_defs.
Require pc3_props.
Require pc3_subst0.
Require ty3_defs.
Require ty3_gen.
Require ty3_lift.
Require ty3_props.

   Section ty3_fsubst0. (****************************************************)

      Hints Resolve getl_drop : ld.

      Tactic Definition IH H0 v1 v2 v3 v4 v5 :=
         LApply (H0 v1 v2 v3 v4); [ Intros H_x | XDEAuto 3 ];
         LApply (H_x v5); [ Clear H_x; Intros | XDEAuto 2 ].

      Tactic Definition IHT := (
         Match Context With
            | [ H: (i:?; u0:?; c2:?; t2:?) (fsubst0 i u0 ?1 ?2 c2 t2) ->
                   (e:?) (getl i ?1 (CHead e (Bind Abbr) u0)) -> ?;
                _: (subst0 ?4 ?5 ?2 ?6);
                _: (getl ?4 ?1 (CHead ?9 (Bind Abbr) ?5)) |- ? ] ->
                 IH H ?4 ?5 ?1 ?6 ?9
         ).

      Tactic Definition IHTb1 := (
         Match Context With
            | [ H: (i:?; u0:?; c2:?; t2:?) (fsubst0 i u0 (CHead ?1 (Bind ?11) ?10) ?2 c2 t2) ->
                   (e:?) (getl i (CHead ?1 (Bind ?11) ?10) (CHead e (Bind Abbr) u0)) -> ?;
                _: (subst0 ?4 ?5 ?10 ?6);
                _: (getl ?4 ?1 (CHead ?9 (Bind Abbr) ?5)) |- ? ] ->
                 IH H '(S ?4) ?5 '(CHead ?1 (Bind ?11) ?6) ?2 ?9
         ).

      Tactic Definition IHTb2 := (
         Match Context With
            | [ H: (i:?; u0:?; c2:?; t2:?) (fsubst0 i u0 (CHead ?1 (Bind ?11) ?10) ?2 c2 t2) ->
                   (e:?) (getl i (CHead ?1 (Bind ?11) ?10) (CHead e (Bind Abbr) u0)) -> ?;
                _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?6);
                _: (getl ?4 ?1 (CHead ?9 (Bind Abbr) ?5)) |- ? ] ->
                 IH H '(S ?4) ?5 '(CHead ?1 (Bind ?11) ?10) ?6 ?9
         ).

      Tactic Definition IHC := (
         Match Context With
            | [ H: (i:?; u0:?; c2:?; t2:?) (fsubst0 i u0 ?1 ?2 c2 t2) ->
                   (e:?) (getl i ?1 (CHead e (Bind Abbr) u0)) -> ?;
                _: (csubst0 ?4 ?5 ?1 ?6);
                _: (getl ?4 ?1 (CHead ?9 (Bind Abbr) ?5)) |- ? ] ->
                 IH H ?4 ?5 ?6 ?2 ?9
         ).

      Tactic Definition IHCb := (
         Match Context With
            | [ H: (i:?; u0:?; c2:?; t2:?) (fsubst0 i u0 (CHead ?1 (Bind ?11) ?10) ?2 c2 t2) ->
                   (e:?) (getl i (CHead ?1 (Bind ?11) ?10) (CHead e (Bind Abbr) u0)) -> ?;
                _: (csubst0 ?4 ?5 ?1 ?6);
                _: (getl ?4 ?1 (CHead ?9 (Bind Abbr) ?5)) |- ? ] ->
                 IH H '(S ?4) ?5 '(CHead ?6 (Bind ?11) ?10) ?2 ?9
         ).

      Tactic Definition IHTTb := (
         Match Context With
            | [ H: (i:?; u0:?; c2:?; t2:?) (fsubst0 i u0 (CHead ?1 (Bind ?11) ?10) ?2 c2 t2) ->
                   (e:?) (getl i (CHead ?1 (Bind ?11) ?10) (CHead e (Bind Abbr) u0)) -> ?;
                _: (subst0 ?4 ?5 ?10 ?6);
                _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?7);
                _: (getl ?4 ?1 (CHead ?9 (Bind Abbr) ?5)) |- ? ] ->
                 IH H '(S ?4) ?5 '(CHead ?1 (Bind ?11) ?6) ?7 ?9
         ).

      Tactic Definition IHCT := (
         Match Context With
            | [ H: (i:?; u0:?; c2:?; t2:?) (fsubst0 i u0 ?1 ?2 c2 t2) ->
                   (e:?) (getl i ?1 (CHead e (Bind Abbr) u0)) -> ?;
                _: (csubst0 ?4 ?5 ?1 ?6);
                _: (subst0 ?4 ?5 ?2 ?7);
                _: (getl ?4 ?1 (CHead ?9 (Bind Abbr) ?5)) |- ? ] ->
                 IH H ?4 ?5 ?6 ?7 ?9
         ).

      Tactic Definition IHCTb1 := (
         Match Context With
            | [ H: (i:?; u0:?; c2:?; t2:?) (fsubst0 i u0 (CHead ?1 (Bind ?11) ?10) ?2 c2 t2) ->
                   (e:?) (getl i (CHead ?1 (Bind ?11) ?10) (CHead e (Bind Abbr) u0)) -> ?;
                _: (csubst0 ?4 ?5 ?1 ?6);
                _: (subst0 ?4 ?5 ?10 ?7);
                _: (getl ?4 ?1 (CHead ?9 (Bind Abbr) ?5)) |- ? ] ->
                 IH H '(S ?4) ?5 '(CHead ?6 (Bind ?11) ?7) ?2 ?9
         ).

      Tactic Definition IHCTb2 := (
         Match Context With
            | [ H: (i:?; u0:?; c2:?; t2:?) (fsubst0 i u0 (CHead ?1 (Bind ?11) ?10) ?2 c2 t2) ->
                   (e:?) (getl i (CHead ?1 (Bind ?11) ?10) (CHead e (Bind Abbr) u0)) -> ?;
                _: (csubst0 ?4 ?5 ?1 ?6);
                _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?7);
                _: (getl ?4 ?1 (CHead ?9 (Bind Abbr) ?5)) |- ? ] ->
                 IH H '(S ?4) ?5 '(CHead ?6 (Bind ?11) ?10) ?7 ?9
         ).

      Tactic Definition IHCTTb := (
         Match Context With
            | [ H: (i:?; u0:?; c2:?; t2:?) (fsubst0 i u0 (CHead ?1 (Bind ?11) ?10) ?2 c2 t2) ->
                   (e:?) (getl i (CHead ?1 (Bind ?11) ?10) (CHead e (Bind Abbr) u0)) -> ?;
                _: (csubst0 ?4 ?5 ?1 ?6);
                _: (subst0 ?4 ?5 ?10 ?7);
                _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?8);
                _: (getl ?4 ?1 (CHead ?9 (Bind Abbr) ?5)) |- ? ] ->
                 IH H '(S ?4) ?5 '(CHead ?6 (Bind ?11) ?7) ?8 ?9
         ).

      Hints Resolve le_S_n : ld.

(* NOTE: This breaks the mutual recursion between ty3_subst0 and ty3_csubst0 *)
      Lemma ty3_fsubst0: (g:?; c1:?; t1,t:?) (ty3 g c1 t1 t) ->
                         (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
                         (e:?) (getl i c1 (CHead e (Bind Abbr) u)) ->
                         (ty3 g c2 t2 t).
      Proof.
      Intros until 1; XElim H; Clear c1 t1 t.
(* case 1: ty3_conv *)
      Intros until 6; XElim H4; Clear c2 t0; Intros.
(* case 1.1: fsubst0_snd *)
      IHT; EApply ty3_conv; XDEAuto 2.
(* case 1.2: fsubst0_fst *)
      IHC; EApply ty3_conv; Try EApply pc3_fsubst0; XDEAuto 3.
(* case 1.3: fsubst0_both *)
      IHCT; IHCT; EApply ty3_conv; Try EApply pc3_fsubst0; XDEAuto 3.
(* case 2: ty3_sort *)
      Intros until 1; XElim H; Clear c2 t2; Intros.
(* case 2.1: fsubst0_snd *)
      Subst0GenBase.
(* case 2.2: fsubst0_fst *)
      XAuto.
(* case 2.3: fsubst0_both *)
      Subst0GenBase.
(* case 3: ty3_abbr *)
      Intros until 4; XElim H2; Clear c2 t2; Intros.
(* case 3.1: fsubst0_snd *)
      Subst0GenBase; Subst; GetLDis; XInv; Subst; XDEAuto 3.
(* case 3.2: fsubst0_fst *)
      Apply (lt_le_e n i); Intros; CSubst0GetL.
(* case 3.2.1: n < i, none *)
      EApply ty3_abbr; XDEAuto 2.
(* case 3.2.2: n < i, csubst0_snd *)
      XInv; CSubst0GetL; Subst.
      GetLDis; Rewrite minus_x_Sy in H; [ GetLGenBase; Subst | XAuto ].
      IHT; EApply ty3_abbr; XDEAuto 2.
(* case 3.2.3: n < i, csubst0_fst *)
      XInv; CSubst0GetL; Subst.
      GetLDis; Rewrite minus_x_Sy in H; [ GetLGenBase; CSubst0GetL | XAuto ].
      IHC; EApply ty3_abbr; XDEAuto 2.
(* case 3.2.4: n < i, csubst0_both *)
      XInv; CSubst0GetL; Subst.
      GetLDis; Rewrite minus_x_Sy in H; [ GetLGenBase; CSubst0GetL | XAuto ].
      IHCT; EApply ty3_abbr; XDEAuto 2.
(* case 3.2.5: n >= i *)
      EApply ty3_abbr; XDEAuto 2.
(* case 3.3: fsubst0_both *)
      Subst0GenBase; Subst; GetLDis; XInv; Subst; CSubst0GetL; XDEAuto 3.
(* case 4: ty3_abst *)
      Intros until 4; XElim H2; Clear c2 t2; Intros.
(* case 4.1: fsubst0_snd *)
      Subst0GenBase; Subst; GetLDis; XInv.
(* case 4.2: fsubst0_fst *)
      Apply (lt_le_e n i); Intros; CSubst0GetL.
(* case 4.2.1: n < i, none *)
      EApply ty3_abst; XDEAuto 2.
(* case 4.2.2: n < i, csubst0_snd *)
      XInv; CSubst0GetL; Subst.
      GetLDis; Rewrite minus_x_Sy in H; [ GetLGenBase | XAuto ].
      IHT; EApply ty3_conv;
      [ EApply ty3_lift | EApply ty3_abst | EApply pc3_lift ]; XDEAuto 3.
(* case 4.2.3: n < i, csubst0_fst *)
      XInv; CSubst0GetL; Subst.
      GetLDis; Rewrite minus_x_Sy in H; [ GetLGenBase; CSubst0GetL | XAuto ].
      IHC; EApply ty3_abst; XDEAuto 2.
(* case 4.2.4: n < i, csubst0_both *)
      XInv; CSubst0GetL; Subst.
      GetLDis; Rewrite minus_x_Sy in H; [ GetLGenBase; CSubst0GetL | XAuto ].
      IHCT; IHC; EApply ty3_conv;
      [ EApply ty3_lift | EApply ty3_abst
      | EApply pc3_lift; Try EApply pc3_fsubst0; Try Apply H
      ]; XDEAuto 2.
(* case 4.2.4: n >= i *)
      EApply ty3_abst; XDEAuto 2.
(* case 4.3: fsubst0_both *)
      Subst0GenBase; Subst; GetLDis; XInv.
(* case 5: ty3_bind *)
      Intros until 5; XElim H3; Clear c2 t0; Intros.
(* case 5.1: fsubst0_snd *)
      Subst0GenBase; Subst.
(* case 5.1.1: subst0 on left argument *)
      Ty3Correct; IHT; IHTb1; Ty3Correct.
      EApply ty3_conv;
      [ EApply ty3_bind | EApply ty3_bind | EApply pc3_fsubst0 ]; XDEAuto 3.
(* case 5.1.2: subst0 on right argument *)
      IHTb2; Ty3Correct; EApply ty3_bind; XDEAuto 2.
(* case 5.1.3: subst0 on both arguments *)
      Ty3Correct; IHT; IHTb1; IHTTb; Ty3Correct.
      EApply ty3_conv;
      [ EApply ty3_bind | EApply ty3_bind | EApply pc3_fsubst0 ]; XDEAuto 3.
(* case 5.2: fsubst0_fst *)
      IHC; IHCb; Ty3Correct; EApply ty3_bind; XDEAuto 2.
(* case 5.3: fsubst0_both *)
      Subst0GenBase; Subst.
(* case 5.3.1: subst0 on left argument *)
      IHC; IHCb; Ty3Correct; Ty3Correct; IHCT; IHCTb1; Ty3Correct.
      EApply ty3_conv;
      [ EApply ty3_bind | EApply ty3_bind
      | EApply pc3_fsubst0; [ Idtac | Idtac | XDEAuto 2 ] ]; XDEAuto 3.
(* case 5.3.2: subst0 on right argument *)
      IHC; IHCTb2; Ty3Correct; EApply ty3_bind; XDEAuto 2.
(* case 5.3.3: subst0 on both arguments *)
      IHC; IHCb; Ty3Correct; Ty3Correct; IHCT; IHCTTb; Ty3Correct.
      EApply ty3_conv;
      [ EApply ty3_bind | EApply ty3_bind
      | EApply pc3_fsubst0; [ Idtac | Idtac | XDEAuto 2 ] ]; XDEAuto 3.
(* case 6: ty3_appl *)
      Intros until 5; XElim H3; Clear c2 t2; Intros.
(* case 6.1: fsubst0_snd *)
      Subst0GenBase; Subst.
(* case 6.1.1: subst0 on left argument *)
      Ty3Correct; Ty3GenBase; IHT; Ty3Correct.
      EApply ty3_conv;
      [ EApply ty3_appl | EApply ty3_appl | EApply pc3_fsubst0 ]; XDEAuto 3.
(* case 6.1.2: subst0 on right argument *)
      IHT; EApply ty3_appl; XDEAuto 2.
(* case 6.1.3: subst0 on both arguments *)
      Ty3Correct; Ty3GenBase; Move H after H8; Ty3Correct; IHT; Clear H2; IHT.
      EApply ty3_conv;
      [ EApply ty3_appl | EApply ty3_appl | EApply pc3_fsubst0 ]; XDEAuto 3.
(* case 6.2: fsubst0_fst *)
      IHC; Clear H2; IHC; EApply ty3_appl; XDEAuto 2.
(* case 6.3: fsubst0_both *)
      Subst0GenBase; Subst.
(* case 6.3.1: subst0 on left argument *)
      IHC; Ty3Correct; Ty3GenBase; Clear H2; IHC; IHCT.
      EApply ty3_conv;
      [ EApply ty3_appl | EApply ty3_appl
      | EApply pc3_fsubst0; [ Idtac | Idtac | XDEAuto 2 ] ]; XDEAuto 3.
(* case 6.3.2: subst0 on right argument *)
      IHCT; Clear H2; IHC; EApply ty3_appl; XDEAuto 2.
(* case 6.3.3: subst0 on both arguments *)
      IHC; Ty3Correct; Ty3GenBase; IHCT; Clear H2; IHC; Ty3Correct; IHCT.
      EApply ty3_conv;
      [ EApply ty3_appl | EApply ty3_appl
      | EApply pc3_fsubst0; [ Idtac | Idtac | XDEAuto 2 ] ]; XDEAuto 3.
(* case 7: ty3_cast *)
      Intros until 5; XElim H3; Clear c2 t3; Intros.
(* case 7.1: fsubst0_snd *)
      Subst0GenBase; Subst.
(* case 7.1.1: subst0 on left argument *)
      IHT; Ty3Correct; EApply ty3_conv;
      [ Idtac
      | EApply ty3_cast;
        [ EApply ty3_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0 ]
        | Idtac ]
      | EApply pc3_fsubst0 ]; XDEAuto 2.
      XDEAuto 3.
(* case 7.1.2: subst0 on right argument *)
      IHT; EApply ty3_cast; XDEAuto 2.
(* case 7.1.3: subst0 on both arguments *)
      IHT; Clear H2; Ty3Correct; IHT.
      EApply ty3_conv;
      [ Idtac
      | EApply ty3_cast;
        [ EApply ty3_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0 ]
        | Idtac ]
      | EApply pc3_fsubst0 ]; XDEAuto 2.
      XDEAuto 3.
(* case 7.2: fsubst0_fst *)
      IHC; Clear H2; IHC; EApply ty3_cast; XDEAuto 2.
(* case 6.3: fsubst0_both *)
      Subst0GenBase; Subst.
(* case 7.3.1: subst0 on left argument *)
      IHC; Ty3Correct; IHCT; Clear H2; IHC.
      EApply ty3_conv;
      [ Idtac
      | EApply ty3_cast;
        [ EApply ty3_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0; [ Idtac | Idtac | XDEAuto 2 ] ]
        | Idtac ]
      | EApply pc3_fsubst0; [ Idtac | Idtac | XDEAuto 2 ] ]; XDEAuto 2.
      XDEAuto 3.
(* case 7.3.2: subst0 on right argument *)
      IHCT; IHC; EApply ty3_cast; XDEAuto 2.
(* case 7.3.3: subst0 on both arguments *)
      IHC; Ty3Correct; IHCT; Clear H2; IHCT.
      EApply ty3_conv;
      [ Idtac
      | EApply ty3_cast;
        [ EApply ty3_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0; [ Idtac | Idtac | XDEAuto 2 ] ]
        | Idtac ]
      | EApply pc3_fsubst0; [ Idtac | Idtac | XDEAuto 2 ] ]; XDEAuto 2.
      XDEAuto 3.
      Qed.

      Lemma ty3_csubst0: (g:?; c1:?; t1,t2:?) (ty3 g c1 t1 t2) ->
                         (e:?; u:?; i:?) (getl i c1 (CHead e (Bind Abbr) u)) ->
                         (c2:?) (csubst0 i u c1 c2) -> (ty3 g c2 t1 t2).
      Proof.
      Intros; EApply ty3_fsubst0; XDEAuto 2.
      Qed.

      Lemma ty3_subst0: (g:?; c:?; t1,t:?) (ty3 g c t1 t) ->
                        (e:?; u:?; i:?) (getl i c (CHead e (Bind Abbr) u)) ->
                        (t2:?) (subst0 i u t1 t2) -> (ty3 g c t2 t).
      Proof.
      Intros; EApply ty3_fsubst0; XDEAuto 2.
      Qed.

   End ty3_fsubst0.