(*#* #stop file *)

Require pr2_gen.
Require pr3_defs.
Require pr3_props.

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

(*#* #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)).
      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_refl *)
      XEAuto.
(* case 2 : pr3_sing *)
      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.

   Section pr3_gen_lref. (***************************************************)

      Theorem pr3_gen_lref: (c:?; x:?; n:?) (pr3 c (TLRef n) x) ->
                            x = (TLRef n) \/
                            (EX d u v | (drop n (0) c (CTail d (Bind Abbr) u)) &
			                (pr3 d u v) &
                                        x = (lift (S n) (0) v)
                            ).
      Intros; InsertEq H '(TLRef n); XElim H; Clear y x; Intros.
(* case 1: pr3_refl *)
      XAuto.
(* case 2: pr3_sing *)
      Rewrite H2 in H; Clear H2 t1; Pr2GenBase.
(* case 2.1: pr2_free *)
      XAuto.
(* case 2.2: pr2_delta *)
      Rewrite H4 in H0; Clear H1 H4 t2.
      LApply (pr3_gen_lift c x1 t3 (S n) (0)); [ Clear H0; Intros | XAuto ].
      LApply (H x0); [ Clear H; Intros | XEAuto ].
      XElim H; XEAuto.
      Qed. 

   End pr3_gen_lref.

   Section pr3_gen_bind. (***************************************************)

      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 ];
               XDecompose H
            | [ H: (u,t:T) (TTail (Bind Abbr) ?1 ?2) = (TTail (Bind Abbr) u t) -> ? |- ? ] ->
               LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
               XDecompose H.

      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)
                            ) \/
                            (pr3 (CTail c (Bind Void) u1) 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_refl *)
      Rewrite H; XEAuto.
(* case 2 : pr3_sing *)
      Rewrite H2 in H; Clear H2 t0; Pr2Gen.
(* case 2.1 : short step: compatibility *)
      Rewrite H3 in H1; Clear H0 H3 t2. 
      IH; Try Pr3Context; Try Rewrite H2; XEAuto.
(* case 2.2 : short step: zeta *)
      XEAuto.
      Qed.

      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) & 
				        (pr3 (CTail c (Bind Abbr) u1) t1 t2)
                            ) \/
                            (pr3 (CTail c (Bind Abbr) u1) 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_refl *)
      Rewrite H; XEAuto.
(* case 2: pr3_sing *)
      Rewrite H2 in H; Clear H2 t1; Pr2Gen.
(* case 2.1: short step: compatibility *)
      Rewrite H3 in H1; Clear H0 H3 t2.
      IH; Repeat Pr3Context;
      Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro);
      XEAuto.
(* case 2.2: short step: beta *)
      Rewrite H3 in H1; Clear H0 H3 t1. 
      IH; Repeat Pr3Context; 
      Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro);
      XEAuto.
(* case 2.3: short step: delta *)
      Rewrite H3 in H1; Clear H0 H3 t2.
      IH; Repeat Pr3Context; 
      Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro);
      XDEAuto 7.     
(* case 2.4: short step: zeta *)
      XEAuto.
      Qed.

   End pr3_gen_bind.

      Tactic Definition Pr3Gen :=
         Match Context With
            | [ H: (pr3 ?1 (TLRef ?2) ?3) |- ? ] ->
               LApply (pr3_gen_lref ?1 ?3 ?2); [ Clear H; Intros H | XAuto ];
	       XDecompose H 
            | [ H: (pr3 ?1 (TTail (Bind Void) ?2 ?3) ?4) |- ? ] ->
               LApply (pr3_gen_void ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
               XDecompose H
            | [ H: (pr3 ?1 (TTail (Bind Abbr) ?2 ?3) ?4) |- ? ] ->
               LApply (pr3_gen_abbr ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
               XDecompose H
            | [ 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 ];
               XDecompose H0
            | _ -> Pr3GenBase.