(****************************************************************************)
(*                                                                          *)
(*                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 subst1_defs.
Require subst1_lift.
Require pr0_subst0.
Require pr0_subst1.
Require wcpr0_defs.
Require pr2_lift.
Require pr2_gen.
Require pr3_defs.

   Section pr3_context. (****************************************************)

      Hints Resolve pr3_sing : ld.

      Lemma pr3_pr0_pr2_t: (u1,u2:?) (pr0 u1 u2) ->
                           (c:?; t1,t2:?; k:?) (pr2 (CHead c k u2) t1 t2) ->
                           (pr3 (CHead c k u1) t1 t2).
      Proof.
      Intros; InsertEq H0 '(CHead c k u2); XElim H0; Clear y t1 t2;
      Intros; Subst; XAuto.
      NewInduction i; NewInduction k; GetLGenBase.
(* case 1 : pr2_delta, i = 0, Bind *)
      ClearGenBase; XInv; Subst; Pr0Subst0; XDEAuto 5.
(* case 2 : pr2_delta, i = 0, Flat *)
      ClearGenBase; XDEAuto 5.
(* case 3 : pr2_delta, i > 0, Bind *)
      XDEAuto 4.
(* case 4 : pr2_delta, i > 0, Bind *)
      XDEAuto 4.
      Qed.

      Hints Resolve sym_eq : ld.

      Lemma pr3_pr2_pr2_t: (c:?; u1,u2:?) (pr2 c u1 u2) ->
                           (t1,t2:?; k:?) (pr2 (CHead c k u2) t1 t2) ->
                           (pr3 (CHead c k u1) t1 t2).
      Proof.
      Intros until 1; XElim H; Clear c u1 u2; Intros.
(* case 1 : pr2_free *)
      EApply pr3_pr0_pr2_t; XDEAuto 2.
(* case 2 : pr2_delta *)
      InsertEq H2 '(CHead c k t); XElim H2; Clear y t0 t3;
      Intros; Subst; [ XDEAuto 3 | NewInduction i0 ].
(* case 2.1 : i0 = 0 *)
      GetLGenBase; Subst; NewInduction k; ClearGenBase.
(* case 2.1.1: Bind *)
      XInv; Subst.
      Subst0Subst0; Arith9'In H5 i; Clear H1 H4.
      Pr0Subst0; XDEAuto 6.
(* case 2.1.2: Flat *)
      XDEAuto 5.
(* case 2.2 : i0 > 0 *)
      Clear IHi0; NewInduction k; GetLGenBase; XDEAuto 4.
      Qed.

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

      Theorem pr3_pr3_pr3_t: (c:?; u1,u2:?) (pr3 c u1 u2) ->
                             (t1,t2:?; k:?) (pr3 (CHead c k u2) t1 t2) ->
                             (pr3 (CHead c k u1) t1 t2).
      Proof.
      Intros until 1; XElim H; Intros.
(* case 1 : pr3_refl *)
      XAuto.
(* case 2 : pr3_sing *)
      EApply pr3_pr2_pr3_t; [ Apply H1; XAuto | XAuto ].
      Qed.

   End pr3_context.

      Tactic Definition Pr3Context := (
         Match Context With
            | [ H1: (pr0 ?2 ?3); H2: (pr2 (CHead ?1 ?4 ?3) ?5 ?6) |- ? ] ->
               LApply (pr3_pr0_pr2_t ?2 ?3); [ Intros H_x | XAuto ];
               LApply (H_x ?1 ?5 ?6 ?4); [ Clear H_x H2; Intros | XAuto ]
            | [ H1: (pr0 ?2 ?3); H2: (pr3 (CHead ?1 ?4 ?3) ?5 ?6) |- ? ] ->
               LApply (pr3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
               LApply (H2 ?2); [ Clear H2; Intros | XAuto ]
            | [ H1: (pr2 ?1 ?2 ?3); H2: (pr2 (CHead ?1 ?4 ?3) ?5 ?6) |- ? ] ->
               LApply (pr3_pr2_pr2_t ?1 ?2 ?3); [ Intros H_x | XAuto ];
               LApply (H_x ?5 ?6 ?4); [ Clear H_x H2; Intros | XAuto ]
            | [ H1: (pr2 ?1 ?2 ?3); H2: (pr3 (CHead ?1 ?4 ?3) ?5 ?6) |- ? ] ->
               LApply (pr3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
               LApply (H2 ?2); [ Clear H2; Intros | XAuto ]
            | [ H1: (pr3 ?1 ?2 ?3); H2: (pr3 (CHead ?1 ?4 ?3) ?5 ?6) |- ? ] ->
               LApply (pr3_pr3_pr3_t ?1 ?2 ?3); [ Intros H_x | XAuto ];
               LApply (H_x ?5 ?6 ?4); [ Clear H_x H2; Intros | XAuto ]
         ).

   Section pr3_lift. (*******************************************************)

      Hints Resolve pr3_sing : ld.

      Lemma pr3_lift: (c,e:?; h,d:?) (drop h d c e) ->
                      (t1,t2:?) (pr3 e t1 t2) ->
                      (pr3 c (lift h d t1) (lift h d t2)).
      Proof.
      Intros until 2; XElim H0; Intros; XDEAuto 3.
      Qed.

   End pr3_lift.

      Hints Resolve pr3_lift : ld.

   Section pr3_wcpr0. (******************************************************)

      Hints Resolve pr3_sing : ld.

      Lemma pr3_wcpr0_t: (c1,c2:?) (wcpr0 c2 c1) ->
                         (t1,t2:?) (pr3 c1 t1 t2) ->
                         (pr3 c2 t1 t2).
      Proof.
      Intros until 1; XElim H; Intros.
(* case 1 : wcpr0_refl *)
      XAuto.
(* case 2 : wcpr0_comp *)
      Pr3Context; Clear H1.
      XElim H2; Intros.
(* case 2.1 : pr3_refl *)
      XAuto.
(* case 2.2 : pr3_sing *)
      EApply pr3_t; [ Idtac | XDEAuto 2 ]. Clear H2 H3 c1 c2 t1 t2 t4 u2.
      InsertEq H1 '(CHead c3 k u1); XElim H1; Clear y t3 t0.
(* case 2.2.1 : pr2_free *)
      XAuto.
(* case 2.2.1 : pr2_delta *)
      Intros; Subst; WCpr0GetL; Pr0Subst0; XDEAuto 5.
      Qed.

   End pr3_wcpr0.

   Section pr3_eta. (********************************************************)

      Hints Resolve pr1_sing : ld.

      Lemma pr3_eta: (c:?; w,u:?) let t = (THead (Bind Abst) w u) in
                     (v:?) (pr3 c v w) ->
                     (pr3 c (THead (Bind Abst) v
                            (THead (Flat Appl) (TLRef (0)) (lift (1) (0) t)))
                          t).
      Proof.
      Intros; Unfold t; Clear t.
      Rewrite lift_bind.
      LApply (subst1_lift_S u (0) (0)); [ Intros | XAuto ].
      Apply pr3_head_12; [ XDEAuto 2 | Clear H].
      Apply pr3_pr1.
      EApply pr1_sing; [ EApply pr0_beta; XDEAuto 2 | XDEAuto 5 ].
      Qed.

   End pr3_eta.

   Hints Resolve pr3_eta : ld.