(****************************************************************************)
(*                                                                          *)
(*                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 pr2_defs.
Require Export pr3_defs.
Require Export nf2_defs.
Require Export pc1_defs.

      Definition pc3 : C -> T -> T -> Prop :=
         [c:?; t1,t2:?] (EX t | (pr3 c t1 t) & (pr3 c t2 t)).

      Hints Unfold pc3 : ld.

      Tactic Definition Pc3Unfold := (
         Match Context With
            | [ H: (pc3 ? ? ?) |- ? ] -> Unfold pc3 in H; XDecompose H
         ).

      Inductive pc3_left [c:C] : T -> T -> Prop :=
         | pc3_left_r : (t:?) (pc3_left c t t)
         | pc3_left_ur: (t1,t2:?) (pr2 c t1 t2) -> (t3:?) (pc3_left c t2 t3) ->
                        (pc3_left c t1 t3)
         | pc3_left_ux: (t1,t2:?) (pr2 c t1 t2) -> (t3:?) (pc3_left c t1 t3) ->
                        (pc3_left c t2 t3).

      Hints Resolve pc3_left_r : ld.

   Section pc3_clear. (******************************************************)

      Hints Resolve clear_pr3_trans : ld.

      Lemma clear_pc3_trans: (c2:?; t1,t2:?) (pc3 c2 t1 t2) ->
                             (c1:?) (clear c1 c2) -> (pc3 c1 t1 t2).
      Proof.
      Intros; Pc3Unfold; XDEAuto 5.
      Qed.

   End pc3_clear.

   Section pc3_props. (******************************************************)

      Lemma pc3_pr2_r: (c,t1,t2:?) (pr2 c t1 t2) -> (pc3 c t1 t2).
      Proof.
      XDEAuto 4.
      Qed.

      Lemma pc3_pr2_x: (c,t1,t2:?) (pr2 c t2 t1) -> (pc3 c t1 t2).
      Proof.
      XDEAuto 4.
      Qed.

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

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

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

      Lemma pc3_refl: (c:?; t:?) (pc3 c t t).
      Proof.
      XDEAuto 3.
      Qed.

      Lemma pc3_s: (c,t2,t1:?) (pc3 c t1 t2) -> (pc3 c t2 t1).
      Proof.
      Intros; Pc3Unfold; XDEAuto 3.
      Qed.

      Lemma pc3_thin_dx: (c:?; t1,t2:?) (pc3 c t1 t2) ->
                         (u:?; f:?) (pc3 c (THead (Flat f) u t1)
                                           (THead (Flat f) u t2)).
      Proof.
      Intros; Pc3Unfold; XDEAuto 5.
      Qed.

      Lemma pc3_head_1: (c:?; u1,u2:?) (pc3 c u1 u2) ->
                        (k:?; t:?) (pc3 c (THead k u1 t) (THead k u2 t)).
      Proof.
      Intros; Pc3Unfold; XDEAuto 5.
      Qed.

      Lemma pc3_head_2: (c:?; u,t1,t2:?; k:?) (pc3 (CHead c k u) t1 t2) ->
                        (pc3 c (THead k u t1) (THead k u t2)).
      Proof.
      Intros; Pc3Unfold; XDEAuto 5.
      Qed.

      Lemma pc3_pc1: (t1,t2:?) (pc1 t1 t2) -> (c:?) (pc3 c t1 t2).
      Proof.
      Intros; Pc1Unfold; XDEAuto 5.
      Qed.

      Hints Resolve pr3_sing : ld.

      Lemma pc3_pr2_u: (c:?; t2,t1:?) (pr2 c t1 t2) ->
                       (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
      Proof.
      Intros; Pc3Unfold; XDEAuto 4.
      Qed.

   End pc3_props.

      Hints Resolve pc3_refl pc3_pr2_r pc3_pr2_x pc3_pr3_r pc3_pr3_x
                    pc3_pr3_t pc3_thin_dx pc3_head_1 pc3_head_2
                    pc3_pc1 : ld.

   Section pc3_nf2. (********************************************************)

      Lemma pc3_nf2: (c:?; t1,t2:?) (pc3 c t1 t2) ->
                     (nf2 c t1) -> (nf2 c t2) -> t1 = t2.
      Proof.
      Intros; Pc3Unfold.
      XPoseClear H0 '(nf2_pr3_unfold ? ? ? H2 H0); Subst; Clear H2.
      XPoseClear H1 '(nf2_pr3_unfold ? ? ? H3 H1); Subst; Clear H3; XAuto.
      Qed.

      Lemma pc3_nf2_unfold: (c:?; t1,t2:?) (pc3 c t1 t2) -> (nf2 c t2) ->
                            (pr3 c t1 t2).
      Proof.
      Intros; Pc3Unfold.
      XPoseClear H0 '(nf2_pr3_unfold ? ? ? H2 H0); Clear H2.
      Subst; XAuto.
      Qed.

   End pc3_nf2.