(****************************************************************************)
(*                                                                          *)
(*                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 pr3_props.
Require pr3_gen.
Require pc3_defs.
Require pc3_props.

   Section pc3_gen. (********************************************************)

      Lemma pc3_gen_sort: (c:?; m,n:?) (pc3 c (TSort m) (TSort n)) -> m = n.
      Proof.
      Intros; Pc3Unfold; Repeat Pr3GenBase; Subst; XInv; XAuto.
      Qed.

      Lemma pc3_gen_abst: (c:?; u1,u2,t1,t2:?)
                          (pc3 c (THead (Bind Abst) u1 t1)
                                 (THead (Bind Abst) u2 t2)
                          ) ->
                          (pc3 c u1 u2) /\
                          (b:?; u:?) (pc3 (CHead c (Bind b) u) t1 t2).
      Proof.
      Intros.
      Pc3Unfold; Repeat Pr3GenBase; Subst; XInv; Subst; XDEAuto 4.
      Qed.

      Lemma pc3_gen_abst_shift: (c:?; u,t1,t2:?)
                                (pc3 c (THead (Bind Abst) u t1)
                                       (THead (Bind Abst) u t2)
                                ) ->
                                (pc3 (CHead c (Bind Abst) u) t1 t2).
      Proof.
      Intros; XDecomPoseClear H '(pc3_gen_abst ? ? ? ? ? H); XAuto.
      Qed.

      Lemma pc3_gen_lift: (c:?; t1,t2:?; h,d:?)
                          (pc3 c (lift h d t1) (lift h d t2)) ->
                          (e:?) (drop h d c e) ->
                          (pc3 e t1 t2).
      Proof.
      Intros.
      Pc3Unfold; Repeat Pr3Gen; Subst; LiftGen; Subst; XDEAuto 2.
      Qed.

      Lemma pc3_gen_not_abst: (b:?) ~b=Abst -> (c:?; t1,t2,u1,u2:?)
                              (pc3 c (THead (Bind b) u1 t1)
                                     (THead (Bind Abst) u2 t2)
                              ) ->
                              (pc3 (CHead c (Bind b) u1) t1
                                   (lift (1) (0) (THead (Bind Abst) u2 t2))
                              ).
      Proof.
      XElim b; Intros;
      Try EqFalse; Pc3Unfold; Repeat Pr3Gen; Subst; XInv; Subst;
      EApply pc3_pr3_t; XDEAuto 4.
      Qed.

      Lemma pc3_gen_lift_abst: (c:?; t,t2,u2:?; h,d:?)
                               (pc3 c (lift h d t)
                                      (THead (Bind Abst) u2 t2)
                               ) ->
                               (e:?) (drop h d c e) ->
                               (EX u1 t1 | (pr3 e t (THead (Bind Abst) u1 t1)) &
                                           (pr3 c u2 (lift h d u1)) &
                                           (b:B; u:T)(pr3 (CHead c (Bind b) u) t2 (lift h (S d) t1))
                               ).
      Proof.
      Intros.
      Pc3Unfold; Repeat Pr3Gen; Subst; LiftGenBase; Subst; XDEAuto 2.
      Qed.

      Lemma pc3_gen_sort_abst: (c:?; u,t:?; n:?)
                               (pc3 c (TSort n) (THead (Bind Abst) u t)) ->
                               (P:Prop) P.
      Proof.
      Intros; Pc3Unfold; Repeat Pr3GenBase; Subst; XInv.
      Qed.

      Axiom pc3_gen_appls_sort_abst: (c:?; vs:?; w,u:?; n:?)
                                     (pc3 c (THeads (Flat Appl) vs (TSort n))
                                            (THead (Bind Abst) w u)
                                     ) -> False.

      Axiom pc3_gen_appls_lref_abst: (c,d:?; v:?; i:?)
                                     (getl i c (CHead d (Bind Abst) v)) ->
                                     (vs:?; w,u:?)
                                     (pc3 c (THeads (Flat Appl) vs (TLRef i))
                                            (THead (Bind Abst) w u)
                                     ) -> False.

      Axiom pc3_gen_appls_lref_sort: (c,d:?; v:?; i:?)
                                     (getl i c (CHead d (Bind Abst) v)) ->
                                     (vs, ws:?; n:?)
                                     (pc3 c (THeads (Flat Appl) vs (TLRef i))
                                            (THeads (Flat Appl) ws (TSort n))
                                     ) -> False.

   End pc3_gen.

      Tactic Definition Pc3Gen := (
         Match Context With
            | [H: (pc3 ?1 (TSort ?2) (TSort ?3)) |- ? ] ->
               LApply (pc3_gen_sort ?1 ?2 ?3); [ Clear H; Intros | XAuto ]
            | [ _: (pc3 ?1 (lift ?2 ?3 ?4) (lift ?2 ?3 ?5));
                _: (drop ?2 ?3 ?1 ?6) |- ? ] ->
               LApply (pc3_gen_lift ?1 ?4 ?5 ?2 ?3); [ Intros H_x | XAuto ];
               LApply (H_x ?6); [ Clear H_x; Intros | XAuto ]
            | [ H: (pc3 ? (THead (Bind Abst) ?1 ?) (THead (Bind Abst) ?1 ?)) |- ? ] ->
               XPoseClear H '(pc3_gen_abst_shift ? ? ? ? H)
            | [ H: (pc3 ?1 (THead (Bind Abst) ?2 ?3) (THead (Bind Abst) ?4 ?5)) |- ? ] ->
               LApply (pc3_gen_abst ?1 ?2 ?4 ?3 ?5);[ Clear H; Intros H | XAuto ];
               XElim H; Intros
            | [ H: (pc3 ?1 (THead (Bind ?2) ?3 ?4) (THead (Bind Abst) ?5 ?6));
                _: ~ ?2 = Abst |- ? ] ->
               LApply (pc3_gen_not_abst ?2); [ Intros H_x | XAuto ];
               LApply (H_x ?1 ?4 ?6 ?3 ?5); [ Clear H H_x; Intros | XAuto ]
            | [ _: (pc3 ?1 (lift ?2 ?3 ?4) (THead (Bind Abst) ?5 ?6));
                _: (drop ?2 ?3 ?1 ?7) |- ? ] ->
               LApply (pc3_gen_lift_abst ?1 ?4 ?6 ?5 ?2 ?3); [ Intros H_x | XAuto ];
               LApply (H_x ?7); [ Clear H_x; Intros H_x | XAuto ];
               XElim H_x; Intros
            | [H: (pc3 ? (TSort ?) (THead (Bind Abst) ? ? )) |- ? ] ->
               EApply pc3_gen_sort_abst; Apply H
            | [H: (pc3 ? (THead (Bind Abst) ? ? ) (TSort ?)) |- ? ] ->
               EApply pc3_gen_sort_abst; Apply pc3_s; Apply H
            | [H: (pc3 ? (THeads (Flat Appl) ? (TSort ?))
                         (THead (Bind Abst) ? ?)
                  ) |- ? ] ->
               XDecomPose '(pc3_gen_appls_sort_abst ? ? ? ? ? H)
            | [H: (pc3 ?1 (THeads (Flat Appl) ? (TLRef ?2))
                          (THead (Bind Abst) ? ?)
                  ) |- False ] ->
               EApply pc3_gen_appls_lref_abst with c:=?1 i:=?2; [ XAuto | Apply H ]
            | [H: (pc3 ?1 (THead (Bind Abst) ? ?) (TLRef ?2)) |- ? ] ->
               Cut False; [ Intros H_x; XDecompose H_x | Idtac ];
               EApply pc3_gen_appls_lref_abst with c:=?1 i:=?2 vs:=TNil; [ XDEAuto 5 | Apply pc3_s; Simpl; Apply H ]
            | [H: (pc3 ?1 (TLRef ?2) (THead (Bind Abst) ? ?)) |- ? ] ->
               Cut False; [ Intros H_x; XDecompose H_x | Idtac ];
               EApply pc3_gen_appls_lref_abst with c:=?1 i:=?2 vs:=TNil; [ XDEAuto 5 | Simpl; Apply H ]
            | [H: (pc3 ?1 (TSort ?) (TLRef ?2)) |- ? ] ->
               Cut False; [ Intros H_x; XDecompose H_x | Idtac ];
               EApply pc3_gen_appls_lref_sort with c:=?1 i:=?2 vs:=TNil ws:=TNil; [ XDEAuto 5 | Apply pc3_s; Simpl; Apply H ]
            | [ |- ? ] -> Pr3Gen
         ).