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

Require Export getl_defs.
Require Export pr0_defs.

      Inductive wcpr0: C -> C -> Prop :=
         | wcpr0_refl: (c:?) (wcpr0 c c)
         | wcpr0_comp: (c1,c2:?) (wcpr0 c1 c2) -> (u1,u2:?) (pr0 u1 u2) ->
                       (k:?) (wcpr0 (CHead c1 k u1) (CHead c2 k u2)).

      Hint wcpr0 : ld := Constructors wcpr0.

   Section wcpr0_gen_base. (*************************************************)

      Lemma wcpr0_gen_sort: (x:?; n:?) (wcpr0 (CSort n) x) -> x = (CSort n).
      Proof.
      Intros; InsertEq H '(CSort n); XElim H; Clear y x;
      Intros; XInv; Subst; XAuto.
      Qed.

      Lemma wcpr0_gen_head: (k:?; c1,x:?; u1:?) (wcpr0 (CHead c1 k u1) x) ->
                            x = (CHead c1 k u1) \/
                            (EX c2 u2 | x = (CHead c2 k u2) &
                                        (wcpr0 c1 c2) & (pr0 u1 u2)
                            ).
      Proof.
      Intros; InsertEq H '(CHead c1 k u1); XElim H; Clear y x;
      Intros; XInv; Subst; XDEAuto 3.
      Qed.

   End wcpr0_gen_base.

      Tactic Definition CPrGenBase := (
         Match Context With
            | [ H: (wcpr0 (CSort ?2) ?1) |- ? ] ->
               LApply (wcpr0_gen_sort ?1 ?2); [ Clear H; Intros | XAuto ];
               Subst
            | [ H: (wcpr0 (CHead ?2 ?3 ?4) ?1) |- ? ] ->
               LApply (wcpr0_gen_head ?3 ?2 ?1 ?4); [ Clear H; Intros H | XAuto ];
               XDecompose H; Subst
         ).

   Section wcpr0_drop. (*****************************************************)

      Lemma wcpr0_drop: (c1,c2:?) (wcpr0 c1 c2) -> (h:?; e1:?; u1:?; k:?)
                        (drop h (0) c1 (CHead e1 k u1)) ->
                        (EX e2 u2 | (drop h (0) c2 (CHead e2 k u2)) &
                                    (wcpr0 e1 e2) & (pr0 u1 u2)
                        ).
      Proof.
      Intros until 1; XElim H; Clear c1 c2.
(* case 1 : wcpr0_refl *)
      XDEAuto 2.
(* case 2 : wcpr0_comp *)
      XElim h.
(* case 2.1 : h = 0 *)
      Intros; DropGenBase; XInv; Subst; XDEAuto 2.
(* case 2.2 : h > 0 *)
      XElim k; Intros; DropGenBase.
(* case 2.2.1 : Bind *)
      LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
      XDecompose H0; XDEAuto 3.
(* case 2.2.2 : Flat *)
      LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
      XDecompose H0; XDEAuto 3.
      Qed.

      Lemma wcpr0_drop_back: (c1,c2:?) (wcpr0 c2 c1) -> (h:?; e1:?; u1:?; k:?)
                             (drop h (0) c1 (CHead e1 k u1)) ->
                             (EX e2 u2 | (drop h (0) c2 (CHead e2 k u2)) &
                                         (wcpr0 e2 e1) & (pr0 u2 u1)
                             ).
      Proof.
      Intros until 1; XElim H; Clear c1 c2.
(* case 1 : wcpr0_refl *)
      XDEAuto 2.
(* case 2 : wcpr0_comp *)
      XElim h.
(* case 2.1 : h = 0 *)
      Intros; DropGenBase; XInv; Subst; XDEAuto 2.
(* case 2.2 : h > 0 *)
      XElim k; Intros; DropGenBase.
(* case 2.2.1 : Bind *)
      LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
      XDecompose H0; XDEAuto 3.
(* case 2.2.2 : Flat *)
      LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
      XDecompose H0; XDEAuto 3.
      Qed.

   End wcpr0_drop.

      Tactic Definition WCpr0Drop := (
         Match Context With
            | [ _: (drop ?1 (0) ?2 (CHead ?3 ?4 ?5));
                _: (wcpr0 ?2 ?6) |- ? ] ->
               LApply (wcpr0_drop ?2 ?6); [ Intros H_x | XAuto ];
               LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
               XElim H_x; Intros
            | [ _: (drop ?1 (0) ?2 (CHead ?3 ?4 ?5));
                _: (wcpr0 ?6 ?2) |- ? ] ->
               LApply (wcpr0_drop_back ?2 ?6); [ Intros H_x | XAuto ];
               LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
               XElim H_x; Intros
            | [ _: (drop ?1 (0) (CHead ?2 ?7 ?8) (CHead ?3 ?4 ?5));
                _: (wcpr0 ?2 ?6) |- ? ] ->
               LApply (wcpr0_drop (CHead ?2 ?7 ?8) (CHead ?6 ?7 ?8)); [ Intros H_x | XAuto ];
               LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
               XElim H_x; Intros
            | [ _: (drop ?1 (0) (CHead ?2 ?7 ?8) (CHead ?3 ?4 ?5));
                _: (wcpr0 ?6 ?2) |- ? ] ->
               LApply (wcpr0_drop_back (CHead ?2 ?7 ?8) (CHead ?6 ?7 ?8)); [ Intros H_x | XAuto ];
               LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
               XElim H_x; Intros
         ).

   Section wcpr0_getl. (*****************************************************)

      Lemma wcpr0_getl: (c1,c2:?) (wcpr0 c1 c2) -> (h:?; e1:?; u1:?; k:?)
                        (getl h c1 (CHead e1 k u1)) ->
                        (EX e2 u2 | (getl h c2 (CHead e2 k u2)) &
                                    (wcpr0 e1 e2) & (pr0 u1 u2)
                        ).
      Proof.
      Intros until 1; XElim H; Clear c1 c2.
(* case 1: wcpr0_refl *)
      XDEAuto 2.
(* case 2  wcpr0_comp *)
      XElim h.
(* case 2.1: h = 0 *)
      Intros; GetLGenBase; NewInduction k; ClearGenBase.
(* case 2.1.1: Bind *)
      XInv; Subst; XDEAuto 3.
(* case 2.1.2: Flat *)
      LApply (H0 (0) e1 u0 k0); [ Clear H0 H2; Intros H0 | XDEAuto 2 ].
      XDecompose H0; XDEAuto 3.
(* case 2.2 : h > 0 *)
      XElim k; Intros; GetLGenBase.
(* case 2.2.1 : Bind *)
      LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
      XDecompose H0; XDEAuto 3.
(* case 2.2.2 : Flat *)
      LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
      XDecompose H0; XDEAuto 3.
      Qed.

      Lemma wcpr0_getl_back: (c1,c2:?) (wcpr0 c2 c1) -> (h:?; e1:?; u1:?; k:?)
                             (getl h c1 (CHead e1 k u1)) ->
                             (EX e2 u2 | (getl h c2 (CHead e2 k u2)) &
                                         (wcpr0 e2 e1) & (pr0 u2 u1)
                             ).
      Proof.
      Intros until 1; XElim H; Clear c1 c2.
(* case 1 : wcpr0_refl *)
      XDEAuto 2.
(* case 2 : wcpr0_comp *)
      XElim h.
(* case 2.1 : h = 0 *)
      Intros; GetLGenBase; NewInduction k; ClearGenBase.
(* case 2.1.1: Bind *)
      XInv; Subst; XDEAuto 3.
(* case 2.1.2: Flat *)
      LApply (H0 (0) e1 u0 k0); [ Clear H0 H2; Intros H0 | XDEAuto 2 ].
      XDecompose H0; XDEAuto 3.
(* case 2.2 : h > 0 *)
      XElim k; Intros; GetLGenBase.
(* case 2.2.1 : Bind *)
      LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
      XDecompose H0; XDEAuto 3.
(* case 2.2.2 : Flat *)
      LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
      XDecompose H0; XDEAuto 3.
      Qed.

   End wcpr0_getl.

      Tactic Definition WCpr0GetL := (
         Match Context With
            | [ _: (getl ?1 ?2 (CHead ?3 ?4 ?5));
                _: (wcpr0 ?2 ?6) |- ? ] ->
               LApply (wcpr0_getl ?2 ?6); [ Intros H_x | XAuto ];
               LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
               XElim H_x; Intros
            | [ _: (getl ?1 ?2 (CHead ?3 ?4 ?5));
                _: (wcpr0 ?6 ?2) |- ? ] ->
               LApply (wcpr0_getl_back ?2 ?6); [ Intros H_x | XAuto ];
               LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
               XElim H_x; Intros
            | [ _: (getl ?1 (CHead ?2 ?7 ?8) (CHead ?3 ?4 ?5));
                _: (wcpr0 ?2 ?6) |- ? ] ->
               LApply (wcpr0_getl (CHead ?2 ?7 ?8) (CHead ?6 ?7 ?8)); [ Intros H_x | XAuto ];
               LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
               XElim H_x; Intros
            | [ _: (getl ?1 (CHead ?2 ?7 ?8) (CHead ?3 ?4 ?5));
                _: (wcpr0 ?6 ?2) |- ? ] ->
               LApply (wcpr0_getl_back (CHead ?2 ?7 ?8) (CHead ?6 ?7 ?8)); [ Intros H_x | XAuto ];
               LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
               XElim H_x; Intros
         ).