(****************************************************************************)
(*                                                                          *)
(*                The formal system \lambda\delta                           *)
(*                                                                          *)
(*                Author: Ferruccio Guidi                                   *)
(*                                                                          *)
(*                This file is distributed under the terms of the           *)
(*                GNU General Public License Version 2                      *)
(*                                                                          *)
(****************************************************************************)

Require subst0_subst0.
Require pr0_subst0.
Require wcpr0_defs.
Require pr3_defs.
Require pr3_props.
Require pr3_confluence.
Require pc3_defs.

   Section pc3_trans. (******************************************************)

      Hints Resolve pr3_t : ld.

      Theorem pc3_t: (t2,c,t1:?) (pc3 c t1 t2) ->
                     (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
      Proof.
      Intros; Repeat Pc3Unfold; Pr3Confluence; XDEAuto 4.
      Qed.

      Lemma pc3_pr2_u2: (c:?; t0,t1:?) (pr2 c t0 t1) ->
                        (t2:?) (pc3 c t0 t2) -> (pc3 c t1 t2).
      Proof.
      Intros; Apply (pc3_t t0); XAuto.
      Qed.

      Hints Resolve pc3_t : ld.

      Lemma pc3_pr3_conf: (c:?; t,t1:?) (pc3 c t t1) ->
                          (t2:?) (pr3 c t t2) -> (pc3 c t2 t1).
      Proof.
      XDEAuto 3.
      Qed.

      Theorem pc3_head_12: (c:?; u1,u2:?) (pc3 c u1 u2) ->
                           (k:?; t1,t2:?) (pc3 (CHead c k u2) t1 t2) ->
                           (pc3 c (THead k u1 t1) (THead k u2 t2)).
      Proof.
      Intros.
      EApply pc3_t; [ Apply pc3_head_1 | Apply pc3_head_2 ]; XAuto.
      Qed.

      Theorem pc3_head_21: (c:?; u1,u2:?) (pc3 c u1 u2) ->
                           (k:?; t1,t2:?) (pc3 (CHead c k u1) t1 t2) ->
                           (pc3 c (THead k u1 t1) (THead k u2 t2)).
      Proof.
      Intros.
      EApply pc3_t; [ Apply pc3_head_2 | Apply pc3_head_1 ]; XAuto.
      Qed.

   End pc3_trans.

      Hints Resolve pc3_head_12 pc3_head_21 : ld.

      Tactic Definition Pc3T := (
         Match Context With
            | [ _: (pr3 ?1 ?2 (THead ?3 ?4 ?5)); _: (pc3 ?1 ?6 ?4) |- ? ] ->
               LApply (pc3_t (THead ?3 ?4 ?5) ?1 ?2); [ Intros H_x | XAuto ];
               LApply (H_x (THead ?3 ?6 ?5)); [ Clear H_x; Intros | Apply pc3_s; XAuto ]
            | [ _: (pc3 ?1 ?2 ?3); _: (pr3 ?1 ?3 ?4) |- ? ] ->
               LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
               LApply (H_x ?4); [ Clear H_x; Intros | XAuto ]
            | [ _: (pc3 ?1 ?2 ?3); _: (pc3 ?1 ?4 ?3) |- ? ] ->
               LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
               LApply (H_x ?4); [ Clear H_x; Intros | XAuto ]
         ).

   Section pc3_context. (****************************************************)

      Lemma pc3_pr0_pr2_t: (u1,u2:?) (pr0 u2 u1) ->
                           (c:?; t1,t2:?; k:?) (pr2 (CHead c k u2) t1 t2) ->
                           (pc3 (CHead c k u1) t1 t2).
      Proof.
      Intros; InsertEq H0 '(CHead c k u2); XElim H0; Clear y t1 t2;
      Intros; XInv; Subst; [ XAuto | NewInduction i ].
(* case 1: pr2_delta i = 0 *)
      GetLGenBase; NewInduction k; ClearGenBase.
(* case 1.1: Bind *)
      XInv; Subst.
      Pr0Subst0; Apply pc3_pr3_t with t0:=x; XDEAuto 3.
(* case 1.1: Flat *)
      EApply clear_pc3_trans; XDEAuto 3.
(* case 2: pr2_delta i > 0 *)
      GetLGenBase; NewInduction k; XDEAuto 4.
      Qed.

      Hints Resolve sym_eq : ld.

      Lemma pc3_pr2_pr2_t: (c:?; u1,u2:?) (pr2 c u2 u1) ->
                           (t1,t2:?; k:?) (pr2 (CHead c k u2) t1 t2) ->
                           (pc3 (CHead c k u1) t1 t2).
      Proof.
      Intros until 1; XElim H; Clear c u1 u2; Intros; Subst.
(* case 1: pr2_free *)
      EApply pc3_pr0_pr2_t; [ Apply H | XAuto ].
(* case 2: pr2_delta *)
      InsertEq H2 '(CHead c k t1); XElim H2; Clear y t0 t3;
      Intros; Subst; [ XAuto | NewInduction i0 ].
(* case 2.1: i0 = 0 *)
      GetLGenBase; NewInduction k; ClearGenBase.
(* case 2.1.1: Bind *)
      XInv; Subst; Pr0Subst0; Subst0Subst0; Arith9'In H5 i.
      EApply pc3_pr2_u.
      EApply pr2_delta; XDEAuto 2.
      Apply pc3_pr2_x; EApply pr2_delta; [ Idtac | XDEAuto 2 | XDEAuto 2 ]; XDEAuto 2.
(* case 2.1.2: Flat *)
      EApply clear_pc3_trans; XDEAuto 3.
(* case 2.2: i0 > 0 *)
      Clear IHi0; GetLGenBase; NewInduction k; XDEAuto 4.
      Qed.

      Lemma pc3_pr2_pr3_t: (c:?; u2,t1,t2:?; k:?)
                           (pr3 (CHead c k u2) t1 t2) ->
                           (u1:?) (pr2 c u2 u1) ->
                           (pc3 (CHead c k u1) t1 t2).
      Proof.
      Intros until 1; XElim H; Intros.
(* case 1: pr3_refl *)
      XAuto.
(* case 2: pr3_sing *)
      EApply pc3_t.
      EApply pc3_pr2_pr2_t; [ Apply H2 | Apply H ].
      XAuto.
      Qed.

      Lemma pc3_pr3_pc3_t: (c:?; u1,u2:?) (pr3 c u2 u1) ->
                           (t1,t2:?; k:?) (pc3 (CHead c k u2) t1 t2) ->
                           (pc3 (CHead c k u1) t1 t2).
      Proof.
      Intros until 1; XElim H; Intros.
(* case 1: pr3_refl *)
      XAuto.
(* case 2: pr3_sing *)
      Apply H1; Pc3Unfold.
      EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_pr2_pr3_t; XDEAuto 2.
      Qed.

   End pc3_context.

      Tactic Definition Pc3Context := (
         Match Context With
            | [ H1: (pr0 ?3 ?2); H2: (pr2 (CHead ?1 ?4 ?3) ?5 ?6) |- ? ] ->
               LApply (pc3_pr0_pr2_t ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
            | [ H1: (pr0 ?3 ?2); H2: (pr3 (CHead ?1 ?4 ?3) ?5 ?6) |- ? ] ->
               LApply (pc3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
               LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
            | [ H1: (pr2 ?1 ?3 ?2); H2: (pr2 (CHead ?1 ?4 ?3) ?5 ?6) |- ? ] ->
               LApply (pc3_pr2_pr2_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
            | [ H1: (pr2 ?1 ?3 ?2); H2: (pr3 (CHead ?1 ?4 ?3) ?5 ?6) |- ? ] ->
               LApply (pc3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
               LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
            | [ H1: (pr3 ?1 ?3 ?2); H2: (pc3 (CHead ?1 ?4 ?3) ?5 ?6) |- ? ] ->
               LApply (pc3_pr3_pc3_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
            | [ |- ? ] -> Pr3Context
         ).

   Section pc3_lift. (*******************************************************)

      Lemma pc3_lift: (c,e:?; h,d:?) (drop h d c e) ->
                      (t1,t2:?) (pc3 e t1 t2) ->
                      (pc3 c (lift h d t1) (lift h d t2)).

      Proof.
      Intros.
      Pc3Unfold.
      EApply pc3_pr3_t; (EApply pr3_lift; [ XDEAuto 2 | Apply H1 Orelse Apply H2 ]).
      Qed.

   End pc3_lift.

      Hints Resolve pc3_lift : ld.

   Section pc3_wcpr0. (******************************************************)

      Remark pc3_wcpr0_t_aux: (c1,c2:?) (wcpr0 c1 c2) ->
                              (k:?; u,t1,t2:?) (pr3 (CHead c1 k u) t1 t2) ->
                              (pc3 (CHead c2 k u) t1 t2).
      Proof.
      Intros; XElim H0; Clear t1 t2; Intros.
(* case 1.1: pr3_refl *)
      XAuto.
(* case 1.2: pr3_sing *)
      EApply pc3_t; [ Idtac | XDEAuto 2 ]. Clear H2.
      InsertEq H0 '(CHead c1 k u); XElim H0; Clear y t1; Intros; Subst.
(* case 1.2.1: pr2_free *)
      XAuto.
(* case 1.2.2: pr2_delta *)
      WCpr0GetL; Pr0Subst0.
      EApply pc3_pr2_u; [ EApply pr2_delta; XDEAuto 2 | XAuto ].
      Qed.

      Lemma pc3_wcpr0_t: (c1,c2:?) (wcpr0 c1 c2) ->
                         (t1,t2:?) (pr3 c1 t1 t2) -> (pc3 c2 t1 t2).
      Proof.
      Intros until 1; XElim H; Intros.
(* case 1: wcpr0_refl *)
      XAuto.
(* case 2: wcpr0_comp *)
      Pc3Context; Pc3Unfold.
      EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_wcpr0_t_aux; XDEAuto 2.
      Qed.

      Lemma pc3_wcpr0: (c1,c2:?) (wcpr0 c1 c2) -> (t1,t2:?) (pc3 c1 t1 t2) ->
                       (pc3 c2 t1 t2).
      Proof.
      Intros; Pc3Unfold.
      EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_wcpr0_t; XDEAuto 2.
      Qed.

   End pc3_wcpr0.

   Section pc3_ind_left. (***************************************************)

      Hints Resolve pc3_left_ur pc3_left_ux : ld.

      Remark pc3_left_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) -> (pc3_left c t1 t2).
      Proof.
      Intros; XElim H; XDEAuto 2.
      Qed.

      Remark pc3_left_trans: (c:?; t1,t2:?) (pc3_left c t1 t2) ->
                             (t3:?) (pc3_left c t2 t3) -> (pc3_left c t1 t3).
      Proof.
      Intros until 1; XElim H; XDEAuto 4.
      Qed.

      Hints Resolve pc3_left_trans : ld.

      Remark pc3_left_sym: (c:?; t1,t2:?) (pc3_left c t1 t2) ->
                           (pc3_left c t2 t1).
      Proof.
      Intros; XElim H; XDEAuto 4.
      Qed.

      Hints Resolve pc3_left_sym pc3_left_pr3 : ld.

      Remark pc3_left_pc3: (c:?; t1,t2:?) (pc3 c t1 t2) -> (pc3_left c t1 t2).
      Proof.
      Intros; Pc3Unfold; XDEAuto 5.
      Qed.

      Hints Resolve pc3_t : ld.

      Remark pc3_pc3_left: (c:?; t1,t2:?) (pc3_left c t1 t2) -> (pc3 c t1 t2).
      Proof.
      Intros; XElim H; XDEAuto 3.
      Qed.

      Hints Resolve pc3_left_pc3 pc3_pc3_left : ld.

      Lemma pc3_ind_left: (c:C; P:(T->T->Prop))
                          ((t:T) (P t t)) ->
                          ((t1,t2:T) (pr2 c t1 t2) -> (t3:T) (pc3 c t2 t3) -> (P t2 t3) -> (P t1 t3)) ->
                          ((t1,t2:T) (pr2 c t1 t2) -> (t3:T) (pc3 c t1 t3) -> (P t1 t3) -> (P t2 t3)) ->
                          (t,t0:T) (pc3 c t t0) -> (P t t0).
      Proof.
      Intros; ElimType (pc3_left c t t0); XDEAuto 4.
      Qed.

   End pc3_ind_left.

   Section pc3_eta. (********************************************************)

      Lemma pc3_eta: (c:?; t,w,u:?) (pc3 c t (THead (Bind Abst) w u)) ->
                     (v:?) (pc3 c v w) ->
                     (pc3 c (THead (Bind Abst) v
                            (THead (Flat Appl) (TLRef (0)) (lift (1) (0) t)))
                          t).
      Proof.
      Intros.
      EApply pc3_t;
      [ EApply pc3_head_21;
        [ XDEAuto 2 | EApply pc3_thin_dx; EApply pc3_lift; XDEAuto 2 ]
      | Idtac ].
      EApply pc3_t; [ Idtac | Apply pc3_s; XDEAuto 2 ].
      XAuto.
      Qed.

   End pc3_eta.