(****************************************************************************)
(*                                                                          *)
(*                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 subst1_gen.
Require csubst1_defs.
Require pr0_lift.
Require pr0_subst1.
Require wcpr0_defs.
Require pc1_props.
Require pc3_props.
Require pc3_gen.
Require ty3_defs.
Require ty3_gen.
Require ty3_lift.
Require ty3_props.
Require ty3_subst0.
Require ty3_gen_context.
Require csubt_defs.
Require csubt_props.

   Section ty3_sred_wcpr0_pr0. (*********************************************)

      Tactic Definition IH H c2 t2 :=
         LApply (H c2); [ Intros H_x | XDEAuto 2 ];
         LApply (H_x t2); [ Clear H_x; Intros | XDEAuto 2 ].

      Tactic Definition IH0 := (
         Match Context With
            | [ H1: (c2:?) (wcpr0 ?2 c2)->(t2:?)(pr0 ?3 t2)->(ty3 ?1 c2 t2 ?4);
                H2: (wcpr0 ?2 ?5); H3: (ty3 ?1 ?2 ?3 ?4) |- ? ] ->
               IH H1 ?5 ?3
         ).

      Tactic Definition IH0c := (
         Match Context With
            | [ H1: (c2:?) (wcpr0 ?2 c2)->(t2:?)(pr0 ?3 t2)->(ty3 ?1 c2 t2 ?4);
                H2: (wcpr0 ?2 ?5); H3: (ty3 ?1 ?2 ?3 ?4) |- ? ] ->
               IH H1 ?5 ?3; Clear H1
         ).

      Tactic Definition IH0B := (
         Match Context With
            | [ H1: (c2:?) (wcpr0 (CHead ?2 (Bind ?6) ?7) c2)->(t2:?)(pr0 ?3 t2)->(ty3 ?1 c2 t2 ?4);
                H2: (wcpr0 ?2 ?5); H3: (ty3 ?1 (CHead ?2 (Bind ?6) ?7) ?3 ?4) |- ? ] ->
               IH H1 '(CHead ?5 (Bind ?6) ?7) ?3
         ).

      Tactic Definition IH0Bc := (
         Match Context With
            | [ H1: (c2:?) (wcpr0 (CHead ?2 (Bind ?6) ?7) c2)->(t2:?)(pr0 ?3 t2)->(ty3 ?1 c2 t2 ?4);
                H2: (wcpr0 ?2 ?5); H3: (ty3 ?1 (CHead ?2 (Bind ?6) ?7) ?3 ?4) |- ? ] ->
               IH H1 '(CHead ?5 (Bind ?6) ?7) ?3; Clear H1
         ).

      Tactic Definition IH1 := (
         Match Context With
            | [ H1: (c2:?) (wcpr0 ?2 c2)->(t2:?)(pr0 ?3 t2)->(ty3 ?1 c2 t2 ?4);
                H2: (wcpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
               IH H1 ?5 ?6
         ).

      Tactic Definition IH1c := (
         Match Context With
            | [ H1: (c2:?) (wcpr0 ?2 c2)->(t2:?)(pr0 ?3 t2)->(ty3 ?1 c2 t2 ?4);
                H2: (wcpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
               IH H1 ?5 ?6; Clear H1
         ).

      Tactic Definition IH1Bc := (
         Match Context With
            | [ H1: (c2:?) (wcpr0 (CHead ?2 (Bind ?7) ?8) c2)->(t2:?)(pr0 ?3 t2)->(ty3 ?1 c2 t2 ?4);
                H2: (wcpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
               IH H1 '(CHead ?5 (Bind ?7) ?8) ?6; Clear H1
         ).

      Tactic Definition IH1BLc := (
         Match Context With
            | [ H1: (c2:?) (wcpr0 (CHead ?2 (Bind ?7) ?8) c2)->(t2:?)(pr0 (lift ?10 ?11 ?3) t2)->(ty3 ?1 c2 t2 ?4);
                H2: (wcpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
               IH H1 '(CHead ?5 (Bind ?7) ?8) '(lift ?10 ?11 ?6); Clear H1
         ).

      Tactic Definition IH1T := (
         Match Context With
            | [ H1: (c2:?) (wcpr0 ?2 c2)->(t2:?)(pr0 (THead ?7 ?8 ?3) t2)->(ty3 ?1 c2 t2 ?4);
                H2: (wcpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
               IH H1 ?5 '(THead ?7 ?8 ?6)
         ).

      Tactic Definition IH1T2c := (
         Match Context With
            | [ H1: (c2:?) (wcpr0 ?2 c2)->(t2:?)(pr0 (THead ?7 ?8 ?3) t2)->(ty3 ?1 c2 t2 ?4);
                H2: (wcpr0 ?2 ?5); H3: (pr0 ?3 ?6); H4: (pr0 ?8 ?9) |- ? ] ->
               IH H1 ?5 '(THead ?7 ?9 ?6); Clear H1
         ).

      Tactic Definition IH3B := (
         Match Context With
            | [ H1: (c2:?) (wcpr0 (CHead ?2 (Bind ?7) ?8) c2)->(t2:?)(pr0 ?3 t2)->(ty3 ?1 c2 t2 ?4);
                H2: (wcpr0 ?2 ?5); H3: (pr0 ?3 ?6); H4: (pr0 ?8 ?9) |- ? ] ->
               IH H1 '(CHead ?5 (Bind ?7) ?9) ?6
         ).

      Hints Resolve getl_drop pc3_s pc3_wcpr0 ty3_subst0 csubt_ty3_ld : ld.

      Lemma ty3_sred_wcpr0_pr0: (g:?; c1:?; t1,t:?) (ty3 g c1 t1 t) ->
                                (c2:?) (wcpr0 c1 c2) ->
                                (t2:?) (pr0 t1 t2) -> (ty3 g c2 t2 t).
      Proof.
      Intros until 1; XElim H; Clear c1 t1 t; Intros.
(* case 1: ty3_conv *)
      IH1c; IH0c; EApply ty3_conv; XDEAuto 2.
(* case 2: ty3_sort *)
      Pr0GenBase; Subst; XAuto.
(* case 3: ty3_abbr *)
      Pr0GenBase; Subst; WCpr0GetL; IH1c; XDEAuto 2.
(* case 4: ty3_abst *)
      Pr0GenBase; Subst; WCpr0GetL; IH0; IH1.
      EApply ty3_conv;
      [ EApply ty3_lift; [ Idtac | XDEAuto 2 ]
      | EApply ty3_abst
      | EApply pc3_lift ]; XDEAuto 3.
(* case 5: ty3_bind *)
      Inversion H4; Clear H4; Subst.
(* case 5.1: pr0_refl *)
      IH0c; IH0Bc.
      EApply ty3_bind; XDEAuto 2.
(* case 5.2: pr0_cont *)
      IH0; IH0B; Ty3Correct; IH3B; Ty3Correct.
      EApply ty3_conv; [ EApply ty3_bind | EApply ty3_bind | Idtac ]; XDEAuto 4.
(* case 5.3: pr0_delta *)
      IH0; IH0B; Ty3Correct; IH3B; Ty3Correct.
      EApply ty3_conv; [ EApply ty3_bind | EApply ty3_bind | Idtac ]; XDEAuto 4.
(* case 5.4: pr0_zeta *)
      IH0; IH1BLc; Ty3Correct; Move H5 after H2; Clear H H0 H1 H3 c.
      NewInduction b.
(* case 5.4.1: Abbr *)
      Ty3GenContext; Subst1Gen; LiftGen; Subst.
      EApply ty3_conv;
      [ EApply ty3_bind; XDEAuto 2 | XDEAuto 2
      | EApply pc3_pr3_x;
        EApply (pr3_t (THead (Bind Abbr) u (lift (1) (0) x1))); XDEAuto 4 ].
(* case 5.4.2: Abst *)
      EqFalse.
(* case 5.4.3: Void *)
      Ty3GenContext; Subst; LiftGen; Subst.
      EApply ty3_conv; [ EApply ty3_bind; XDEAuto 2 | XDEAuto 2 | XAuto ].
(* case 6: ty3_appl *)
      Inversion H4; Clear H4; Subst.
(* case 6.1: pr0_refl *)
      IH0c; IH0c; EApply ty3_appl; XDEAuto 2.
(* case 6.2: pr0_cont *)
      IH0; Ty3Correct; Ty3GenBase; IH1c; IH0; IH1c.
      EApply ty3_conv;
      [ EApply ty3_appl; [ XDEAuto 2 | EApply ty3_bind; XDEAuto 2 ]
      | EApply ty3_appl; XDEAuto 2
      | XDEAuto 4 ].
(* case 6.3: pr0_beta *)
      IH1T; IH0c; Ty3Correct; Ty3GenBase; IH0; IH1c.
      Move H4 after H11; Ty3GenBase; Pc3Gen; Repeat CSub0Ty3.
      EApply ty3_conv;
      [ Apply ty3_appl; [ Idtac | EApply ty3_bind ]
      | EApply ty3_bind
      | Apply (pc3_t (THead (Bind Abbr) v2 t))
      ]; XDEAuto 4.
(* case 6.4: pr0_delta *)
      IH1T2c; Clear H1; Ty3Correct; NonLinear; Ty3GenBase; IH1; IH0c.
      Move H4 after H1; Ty3GenBase; Pc3Gen; Rewrite lift_bind in H0.
      Move H1 after H0; Ty3Lift b u2; Rewrite lift_bind in H14.
      Ty3GenBase.
      EApply ty3_conv;
      [ Apply ty3_appl; [ Idtac | EApply ty3_bind ]; XDEAuto 2
      | EApply ty3_bind;
        [ Idtac
        | EApply ty3_appl; [ EApply ty3_lift | EApply ty3_conv ]
        ]; XDEAuto 2
      | Idtac ].
      Rewrite <- lift_bind; Apply pc3_pc1.
      Apply (pc1_pr0_u2 (THead (Flat Appl) v2 (THead (Bind b) u2 (lift (1) (0) (THead (Bind Abst) u t))))); XAuto.
(* case 7: ty3_cast *)
      Inversion H4; Clear H4; Subst.
(* case 7.1: pr0_refl *)
      IH0c; IH0c; XDEAuto 3.
(* case 7.2: pr0_cont *)
      IH0; Ty3Correct; IH1c; IH1c.
      EApply ty3_conv;
      [ XDEAuto 2
      | EApply ty3_cast; [ EApply ty3_conv; XDEAuto 3 | XDEAuto 2 ]
      | XAuto ].
(* case 7.3: pr0_tau *)
      IH0; Ty3Correct; EApply ty3_conv; XDEAuto 4.
      Qed.

   End ty3_sred_wcpr0_pr0.

   Section ty3_sred_pr3. (**********************************************)

      Lemma ty3_sred_pr0: (t1,t2:?) (pr0 t1 t2) ->
                          (g:?; c:?; t:?) (ty3 g c t1 t) ->
                          (ty3 g c t2 t).
      Proof.
      Intros; EApply ty3_sred_wcpr0_pr0; XDEAuto 2.
      Qed.

      Lemma ty3_sred_pr1: (t1,t2:?) (pr1 t1 t2) ->
                          (g:?; c:?; t:?) (ty3 g c t1 t) ->
                          (ty3 g c t2 t).
      Proof.
      Intros until 1; XElim H; Clear t1 t2; Intros.
(* case 1: pr1_r *)
      XAuto.
(* case 2: pr1_u *)
      EApply H1; EApply ty3_sred_pr0; XDEAuto 2.
      Qed.

      Lemma ty3_sred_pr2: (c:?; t1,t2:?) (pr2 c t1 t2) ->
                          (g:?; t:?) (ty3 g c t1 t) ->
                          (ty3 g c t2 t).
      Proof.
      Intros until 1; XElim H; Clear c t1 t2; Intros.
(* case 1: pr2_free *)
      EApply ty3_sred_wcpr0_pr0; XDEAuto 2.
(* case 2: pr2_u *)
      EApply ty3_subst0; Try EApply ty3_sred_wcpr0_pr0; XDEAuto 2.
      Qed.

      Lemma ty3_sred_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) ->
                          (g:?; t:?) (ty3 g c t1 t) ->
                          (ty3 g c t2 t).
      Proof.
      Intros until 1; XElim H; Clear t1 t2; Intros.
(* case 1: pr3_refl *)
      XAuto.
(* case 2: pr3_sing *)
      EApply H1; EApply ty3_sred_pr2; XDEAuto 2.
      Qed.

   End ty3_sred_pr3.

      Tactic Definition Ty3SRed := (
         Match Context With
            | [ H1: (pr3 ?0 ?1 ?); H2: (ty3 ? ?0 ?1 ?) |- ? ] ->
               XPoseClear H2 '(ty3_sred_pr3 ? ? ? H1 ? ? H2)
            | [ H1: (pr0 ?1 ?); H2: (ty3 ? ? ?1 ?) |- ? ] ->
               XPoseClear H2 '(ty3_sred_pr0 ? ? H1 ? ? ? H2)
         ).

   Section ty3_cred_pr3. (***************************************************)

      Lemma ty3_cred_pr2: (g:?; c:?; v1,v2:?) (pr2 c v1 v2) -> (b:?; t1,t2:?)
                          (ty3 g (CHead c (Bind b) v1) t1 t2) ->
                          (ty3 g (CHead c (Bind b) v2) t1 t2).
      Proof.
      Intros until 1; XElim H; Clear c v1 v2; Intros.
(* case 1: pr2_free *)
      EApply ty3_sred_wcpr0_pr0; XDEAuto 2.
(* case 2: pr2_delta *)
      EApply ty3_csubst0;
      Try EApply ty3_sred_wcpr0_pr0 with c2:=(CHead c (Bind b) t2); XDEAuto 2.
      Qed.

      Hints Resolve ty3_cred_pr2 : ld.

      Lemma ty3_cred_pr3: (g:?; c:?; v1,v2:?) (pr3 c v1 v2) -> (b:?; t1,t2:?)
                          (ty3 g (CHead c (Bind b) v1) t1 t2) ->
                          (ty3 g (CHead c (Bind b) v2) t1 t2).
      Proof.
      Intros until 1; XElim H; Clear v1 v2; XDEAuto 3.
      Qed.

   End ty3_cred_pr3.