(*#* #stop file *)

Require pr2_gen.
Require pr3_defs.
Require pr3_props.

   Section pr3_gen_void. (***************************************************)

      Tactic Definition IH :=
         Match Context With
            [ H: (u,t:T) (TTail (Bind Void) ?1 ?2) = (TTail (Bind Void) u t) -> ? |- ? ] ->
               LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
               XElim H1; Intros H1; XElim H1; Intros.

      Theorem pr3_gen_void : (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Void) u1 t1) x) ->
                             (EX u2 t2 | x = (TTail (Bind Void) u2 t2) &
                                         (pr3 c u1 u2) & (b:?; u:?)
                                         (pr3 (CTail c (Bind b) u) t1 t2)
                             ) \/
                             (EX u | (pr3 c u1 u) &
                                     (pr3 (CTail c (Bind Void) u) t1 (lift (1) (0) x))
                             ).
      Intros until 1; InsertEq H '(TTail (Bind Void) u1 t1);
      UnIntro t1 H; UnIntro u1 H; XElim H; Intros.
(* case 1 : pr3_r *)
      Rewrite H; XEAuto.
(* case 2 : pr3_u *)
      Rewrite H2 in H; Clear H2 t0; Pr2Gen.
(* case 2.1 : short step: compatibility *)
      Rewrite H in H0; Rewrite H in H1; Clear H t2; IH.
(* case 2.1.1 : long step: compatibility *)
      Rewrite H; Rewrite H in H0; XEAuto.
(* case 2.1.2 : long step: zeta *)
      XEAuto.
(* case 2.2 : short step: zeta *)
      Clear H1; Right.
      EApply ex2_intro; [ XAuto | Idtac ].
      EApply pr3_u; [ Idtac | EApply pr3_lift ].
      XEAuto. XAuto. XAuto.
      Qed.

   End pr3_gen_void.

   Section pr3_gen_abbr. (***************************************************)

      Tactic Definition IH :=
         LApply (H1 x0 x1); [ Clear H1; Intros H1 | XAuto ];
         XElim H1;
         [ Intros H1; XElim H1;
           Do 4 Intro; Intros H_x; XElim H_x;
           [ Intros | Intros H_x; XElim H_x; Intros ]
         | Intros H1; XElim H1; Intros ].

      Theorem pr3_gen_abbr : (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Abbr) u1 t1) x) ->
                             (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) &
                                         (pr3 c u1 u2) &
                                         ((b:?; u:?) (pr3 (CTail c (Bind b) u) t1 t2)) \/
                                         (EX u3 t3 y | (pr3 c (TTail (Bind Abbr) u3 t3) x) &
                                                       (pr3 c u1 u3) &
                                                       (b:?; u:?) (pr3 (CTail c (Bind b) u) t1 y) &
                                                       (subst0 (0) u3 y t3)
                                         )
                             ) \/
                             (EX u | (pr3 c u1 u) &
                                     (pr3 (CTail c (Bind Abbr) u) t1 (lift (1) (0) x))
                             ).
      Intros until 1; InsertEq H '(TTail (Bind Abbr) u1 t1);
      UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros;
      Rename x into u1; Rename x0 into t4.
(* case 1 : pr3_r *)
      Rewrite H; XEAuto.
(* case 2 : pr3_u *)
      Rewrite H2 in H; Clear H2 t1; Pr2Gen.
(* case 2.1 : short step: compatibility *)
      Rewrite H in H0; Rewrite H in H1; Clear H t2; IH.
(* case 2.1.1 : long step: compatibility *)
      Rewrite H; Rewrite H in H0; Clear H t3.
      Left; EApply ex3_2_intro; XEAuto.
(* case 2.1.2 : long step: delta *)
      Rewrite H; Rewrite H in H0; Rewrite H in H4; Clear H t3.
      Left; EApply ex3_2_intro;
      [ XEAuto | XEAuto
      | Right; EApply ex4_3_intro;
        [ EApply pr3_t; [ XAuto | Apply H4 ] | XEAuto | Idtac | Apply H7 ] ].
      XEAuto.
(* case 2.1.3 : long step: zeta *)
      XEAuto.
(* case 2.2 : short step: delta *)
      Rewrite H in H0; Rewrite H in H1; Clear H t2; IH.
(* case 2.2.1 : long step: compatibility *)
      Left; EApply ex3_2_intro;
      [ XEAuto | XEAuto
      | Right; EApply ex4_3_intro; [ Rewrite H | Idtac | Idtac | Apply H4 ] ].
      XAuto. XAuto. XAuto.
(* case 2.2.2 : long step: delta *)
      Left; EApply ex3_2_intro;
      [ XEAuto | XEAuto
      | Right; EApply ex4_3_intro;
        [ EApply pr3_t; [ Apply pr3_tail_12 | Apply H5 ]
        | Idtac | Idtac | Apply H4 ] ].
      XAuto. EApply pr3_t; [ Apply H7 | XEAuto ]. XAuto. XAuto.
(* case 2.2.3 : long step: zeta *)
      Right; Apply ex2_intro with x := x0; [ XAuto | Idtac ].
      Apply pr3_u with t2 := x; [ XAuto | Idtac ].
      Apply pr3_u with t2 := x1; [ XEAuto | Idtac ].
      Pr3Context; XAuto.
(* case 2.3 : short step: zeta *)
      Clear H1; Right.
      EApply ex2_intro; [ XAuto | Idtac ].
      EApply pr3_u; [ Idtac | EApply pr3_lift ].
      XEAuto. XAuto. XAuto.
      Qed.

   End pr3_gen_abbr.

   Section pr3_gen_abst. (***************************************************)

      Theorem pr3_gen_abst : (c:?; u1,t1,x:?)
                             (pr3 c (TTail (Bind Abst) u1 t1) x) ->
                             (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
                                         (pr3 c u1 u2) & (b:?; u:?)
                                         (pr3 (CTail c (Bind b) u) t1 t2)
                             ).
      Intros until 1; InsertEq H '(TTail (Bind Abst) u1 t1);
      UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros;
      Rename x into u1; Rename x0 into t4.
(* case 1 : pr3_r *)
      Rewrite H; XEAuto.
(* case 2 : pr3_u *)
      Rewrite H2 in H; Clear H2 t1.
      Pr2GenBase.
      LApply (H1 x0 x1); [ Clear H H1; Intros | XAuto ].
      XElim H; XEAuto.
      Qed.

   End pr3_gen_abst.

   Section pr3_gen_lift. (***************************************************)

(*#* #start file *)

(*#* #caption "generation lemma for lift" *)
(*#* #cap #cap c #alpha e in D, t1 in U1, t2 in U2, x in T, d in i *)

      Theorem pr3_gen_lift : (c:?; t1,x:?; h,d:?) (pr3 c (lift h d t1) x) ->
                             (e:?) (drop h d c e) ->
                             (EX t2 | x = (lift h d t2) & (pr3 e t1 t2)).

(*#* #stop file *)

      Intros until 1; InsertEq H '(lift h d t1);
      UnIntro H t1; XElim H; Clear y x; Intros; Rename x into t4.
(* case 1 : pr3_r *)
      XEAuto.
(* case 2 : pr3_u *)
      Rewrite H2 in H; Pr2Gen.
      LApply (H1 x); [ Clear H1; Intros H1 | XAuto ].
      LApply (H1 e); [ Clear H1; Intros H1 | XAuto ].
      XElim H1; XEAuto.
      Qed.

   End pr3_gen_lift.

      Tactic Definition Pr3Gen :=
         Match Context With
            | [ H: (pr3 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] ->
               LApply (pr3_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
               XElim H; Intros
            | [ H: (pr3 ?1 (TTail (Bind Abbr) ?2 ?3) ?4) |- ? ] ->
               LApply (pr3_gen_abbr ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
               XElim H;
               [ Intros H; XElim H;
                 Do 4 Intro; Intros H_x; XElim H_x;
                 [ Intros | Intros H_x; XElim H_x; Intros ]
               | Intros H; XElim H; Intros ]
            | [ H: (pr3 ?1 (TTail (Bind Void) ?2 ?3) ?4) |- ? ] ->
               LApply (pr3_gen_void ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
               XElim H; Intros H; XElim H; Intros
            | [ H0: (pr3 ?1 (lift ?2 ?3 ?4) ?5);
                H1: (drop ?2 ?3 ?1 ?6) |- ? ] ->
               LApply (pr3_gen_lift ?1 ?4 ?5 ?2 ?3); [ Clear H0; Intros H0 | XAuto ];
               LApply (H0 ?6); [ Clear H0; Intros H0 | XAuto ];
               XElim H0; Intros
            | _ -> Pr2Gen.