(****************************************************************************)
(*                                                                          *)
(*                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_props.
Require getl_props.
Require sty0_defs.
Require pc3_props.
Require pc3_gen.
Require ty3_defs.
Require ty3_gen.
Require ty3_props.
Require ty3_sred.

   Section ty3_gen. (********************************************************)

      Hints Resolve le_S_minus pc3_t ty3_conv : ld.

      Tactic Definition IH e := (
         Match Context With
            | [ H: (t:?; d:?) (lift ?2 ?3 ?4) = (lift ?2 d t) -> ? |- ? ] ->
             LApply (H ?4 ?3); [ Clear H; Intros H | XAuto ];
             LApply (H e); [ Clear H; Intros H | XDEAuto 2 ];
             XDecompose H; Intros
         ).

      Hints Resolve le_trans : ld.

      Lemma ty3_gen_lift: (g:?; c:?; t1,x:?; h,d:?)
                          (ty3 g c (lift h d t1) x) ->
                          (e:?) (drop h d c e) ->
                          (EX t2 | (pc3 c (lift h d t2) x) & (ty3 g e t1 t2)).
      Proof.
      Intros until 1; InsertEq H '(lift h d t1);
      UnIntro H d; UnIntro H t1; XElim H; Clear c y x; Intros; Subst;
      Rename x into t3; Rename x0 into d0.
(* case 1: ty3_conv *)
      IH e; XDEAuto 3.
(* case 2: ty3_sort *)
      LiftGenBase; Subst.
      EApply ex2_intro; [ Rewrite lift_sort; XAuto | XAuto ].
(* case 3: ty3_abbr *)
      LiftXGenBase; Subst.
(* case 3.1: n < d0 *)
      GetLDrop.
      Rewrite (lt_plus_minus n d0) in H3; [ GetLDis; Subst; IH x1 | XAuto ].
      Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
      EApply ex2_intro;
      [ Rewrite lift_d; [ EApply pc3_lift; XDEAuto 2 | XDEAuto 2 ]
      | EApply ty3_abbr; XDEAuto 2 ].
(* case 3.2: n >= d0 + h *)
      GetLDis; Subst.
      EApply ex2_intro; [ Idtac | EApply ty3_abbr; XDEAuto 2 ].
      Rewrite lift_free; [ Idtac | XDEAuto 3 | XAuto ].
      Rewrite <- plus_n_Sm; Rewrite <- le_plus_minus; XDEAuto 2.
(* case 4: ty3_abst *)
      LiftXGenBase; Subst.
(* case 4.1: n < d0 *)
      Rewrite (lt_plus_minus n d0) in H3; [ GetLDis; Subst; IH x1 | XAuto ].
      Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
      EApply ex2_intro; [ Idtac | EApply ty3_abst; XDEAuto 2 ].
      Rewrite lift_d; [ Rewrite <- le_plus_minus | Idtac ]; XAuto.
(* case 4.2: n >= d0 + h *)
      GetLDis; Subst.
      EApply ex2_intro; [ Idtac | EApply ty3_abst; XDEAuto 2 ].
      Rewrite lift_free; [ Idtac | XDEAuto 3 | XAuto ].
      Rewrite <- plus_n_Sm; Rewrite <- le_plus_minus; XDEAuto 2.
(* case 5: ty3_bind *)
      LiftGenBase; Subst.
      Move H after H2; IH e; IH '(CHead e (Bind b) x0); Ty3Correct.
      EApply ex2_intro; [ Rewrite lift_bind; XDEAuto 2 | XDEAuto 2 ].
(* case 6: ty3_appl *)
      LiftGenBase; Subst; IH e; IH e; Pc3Gen; Pc3T; Pc3Gen; Pc3T.
      Move H6 after H11; Ty3Correct; Ty3SRed; Ty3GenBase.
      EApply ex2_intro;
      [ Rewrite lift_flat; Apply pc3_thin_dx;
        Rewrite lift_bind; Apply pc3_head_21; [ EApply pc3_pr3_x | Idtac ]
      | EApply ty3_appl;
        [ EApply ty3_conv
        | EApply ty3_conv; [ EApply ty3_bind | Idtac | Idtac ] ]
      ]; XDEAuto 2.
(* case 7: ty3_cast *)
      LiftGenBase; Subst; IH e; IH e; Pc3Gen.
      EApply ex2_intro; [ Rewrite lift_flat | Idtac ]; XDEAuto 3.
      Qed.

   End ty3_gen.

      Tactic Definition Ty3Gen := (
         Match Context With
            | [ H0: (ty3 ?1 ?2 (lift ?3 ?4 ?5) ?6);
                H1: (drop ?3 ?4 ?2 ?7) |- ? ] ->
               LApply (ty3_gen_lift ?1 ?2 ?5 ?6 ?3 ?4); [ Clear H0; Intros H0 | XAuto ];
               LApply (H0 ?7); [ Clear H0; Intros H0 | XDEAuto 2 ];
               LApply H0; [ Clear H0 H1; Intros H0 | XAuto ];
               XElim H0; Intros
            | [ H: (ty3 ? (CHead ?0 (Bind ?) ?) (lift (S O) O ?) ?) |- ? ] ->
               LApply (ty3_gen_lift ? ? ? ? ? ? H ?0); [ Clear H; Intros H; XDecompose H | XAuto ]
            | [ |- ? ] -> Ty3GenContext
         ).

   Section ty3_sred_props. (*************************************************)

      Lemma ty3_tred: (g:?; c:?; u,t1:?) (ty3 g c u t1) ->
                      (t2:?) (pr3 c t1 t2) -> (ty3 g c u t2).
      Proof.
      Intros; Ty3Correct; Ty3SRed; EApply ty3_conv; XDEAuto 2.
      Qed.

      Hints Resolve ty3_unique : ld.

      Theorem ty3_sconv_pc3: (g:?; c:?; u1,t1:?) (ty3 g c u1 t1) ->
                             (u2,t2:?) (ty3 g c u2 t2) ->
                             (pc3 c u1 u2) -> (pc3 c t1 t2).
      Proof.
      Intros; Pc3Unfold; Repeat Ty3SRed; XDEAuto 2.
      Qed.

      Hints Resolve ty3_conv ty3_sred_pr3 : ld.

      Lemma ty3_sred_back: (g:?; c:?; t1,t0:?) (ty3 g c t1 t0) ->
                           (t2:?) (pr3 c t1 t2) ->
                           (t:?) (ty3 g c t2 t) -> (ty3 g c t1 t).
      Proof.
      Intros; Ty3Correct; XDEAuto 4.
      Qed.

      Hints Resolve ty3_sred_back : ld.

      Theorem ty3_sconv: (g:?; c:?; u1,t1:?) (ty3 g c u1 t1) ->
                         (u2,t2:?) (ty3 g c u2 t2) ->
                         (pc3 c u1 u2) -> (ty3 g c u1 t2).
      Proof.
      Intros; Pc3Unfold; XDEAuto 3.
      Qed.

      Lemma ty3_sty0: (g:?; c:?; u,t1:?) (ty3 g c u t1) ->
                      (t2:?) (sty0 g c u t2) -> (ty3 g c u t2).
      Proof.
      Intros until 1; XElim H; Clear c u t1;
      Intros; Try STy0GenBase; Try GetLDis; XInv; Subst; XDEAuto 3.
(* case 6: ty3_appl *)
      XPoseClear H2 '(H2 ? H4); Clear H0 H4.
      XPose H0 '(ty3_unique ? ? ? ? H2 ? H1).
      Ty3Correct; Move H after H3; Ty3Correct.
      Move H1 after H4; Ty3Correct; Ty3GenBase.
      EApply ty3_conv;
      [ EApply ty3_appl;
        [ XDEAuto 2
        | EApply ty3_sconv; [ XDEAuto 2 | Idtac | Apply H0 ]; XDEAuto 2
        ]
      | XDEAuto 3
      | XDEAuto 3
      ].
(* case 7: ty3_cast *)
      XPoseClear H0 '(H0 ? H5); Clear H5.
      XPoseClear H2 '(H2 ? H4); Clear H4.
      XPose H3 '(ty3_unique ? ? ? ? H0 ? H).
      Ty3Correct; Move H0 after H4; Ty3Correct.
      EApply ty3_conv;
      [ EApply ty3_cast; [ EApply ty3_sconv; XDEAuto 2 | XDEAuto 2 ]
      | XDEAuto 2
      | XDEAuto 5
      ].
      Qed.

   End ty3_sred_props.