(****************************************************************************)
(*                                                                          *)
(*                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 lift_props.
Require subst0_gen.
Require pr0_defs.
Require pr0_lift.

   Section pr0_gen. (********************************************************)

      Lemma pr0_gen_abbr: (u1,t1,x:?) (pr0 (THead (Bind Abbr) u1 t1) x) ->
                          (EX u2 t2 | x = (THead (Bind Abbr) u2 t2) &
                                      (pr0 u1 u2) &
                                      (pr0 t1 t2) \/
                                      (EX y | (pr0 t1 y) & (subst0 (0) u2 y t2))
                          ) \/
                          (pr0 t1 (lift (1) (0) x)).
      Proof.
      Intros; InsertEq H '(THead (Bind Abbr) u1 t1); XElim H; Clear y x;
      Intros; XInv; Subst; XDEAuto 6.
      Qed.

      Lemma pr0_gen_void: (u1,t1,x:?) (pr0 (THead (Bind Void) u1 t1) x) ->
                          (EX u2 t2 | x = (THead (Bind Void) u2 t2) &
                                      (pr0 u1 u2) & (pr0 t1 t2)
                          ) \/
                          (pr0 t1 (lift (1) (0) x)).
      Proof.
      Intros; InsertEq H '(THead (Bind Void) u1 t1); XElim H; Clear y x;
      Intros; XInv; Subst; XDEAuto 3.
      Qed.

      Tactic Definition IH := (
         Match Context With
            | [ H: (_:?; _:?) ?0 = (lift ? ? ?) -> ?;
                H0: ?0 = (lift ? ?2 ?3) |- ? ] ->
               LApply (H ?3 ?2); [ Clear H H0; Intros H_x | XAuto ];
               XElim H_x; Intro; Intros H_x; Intro;
               Try Rewrite H_x; Try Rewrite H_x in H3; Clear H_x
         ).

      Hints Resolve sym_eq lift_bind lift_flat : ld.

      Lemma pr0_gen_lift: (t1,x:?; h,d:?) (pr0 (lift h d t1) x) ->
                          (EX t2 | x = (lift h d t2) & (pr0 t1 t2)).
      Proof.
      Intros until 1; InsertEq H '(lift h d t1);
      UnIntro H d; UnIntro H t1; XElim H; Clear y x; Intros;
      Rename x into t3; Rename x0 into d.
(* case 1 : pr0_refl *)
      XDEAuto 2.
(* case 2 : pr0_comp *)
      NewInduction k; LiftGen; Rewrite H3; Clear H3 t0;
      IH; IH; XDEAuto 4.
(* case 3 : pr0_beta *)
      LiftGen; Rewrite H3; Clear H3 t0.
      LiftGen; Rewrite H3; Clear H3 H5 x1 k.
      IH; IH; XDEAuto 4.
(* case 4 : pr0_upsilon *)
      LiftGen; Rewrite H6; Clear H6 t0.
      LiftGen; Rewrite H6; Clear H6 x1.
      IH; IH; IH.
      Rewrite <- lift_d; [ Simpl | XAuto ].
      Rewrite <- lift_flat; XDEAuto 4.
(* case 5 : pr0_delta *)
      LiftGen; Rewrite H4; Clear H4 t0.
      IH; IH; Arith3In H3 d; Subst0Gen.
      Rewrite H3; XDEAuto 4.
(* case 6 : pr0_zeta *)
      LiftGen; Rewrite H2; Clear H2 t0.
      Arith7In H4 d; LiftGen; Rewrite H2; Clear H2 x1.
      IH; XDEAuto 3.
(* case 7 : pr0_tau *)
      LiftGen; Rewrite H1; Clear H1 t0.
      IH; XDEAuto 3.
      Qed.

   End pr0_gen.

      Tactic Definition Pr0Gen := (
         Match Context With
            | [ H: (pr0 (THead (Bind Abbr) ?1 ?2) ?3) |- ? ] ->
               LApply (pr0_gen_abbr ?1 ?2 ?3); [ 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: (pr0 (THead (Bind Void) ?1 ?2) ?3) |- ? ] ->
               LApply (pr0_gen_void ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
               XElim H; [ Intros H; XElim H; Intros | Intros ]
            | [ H: (pr0 (lift ?0 ?1 ?2) ?3) |- ? ] ->
               LApply (pr0_gen_lift ?2 ?3 ?0 ?1); [ Clear H; Intros H | XAuto ];
               XElim H; Intros
            | [ |- ? ] -> Pr0GenBase
         ).