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

Require pr0_confluence.
Require pr1_defs.

   Section pr1_confluence. (*************************************************)

      Hints Resolve pr1_t : ld.

      Lemma pr1_strip: (t0,t1:?) (pr1 t0 t1) -> (t2:?) (pr0 t0 t2) ->
                       (EX t | (pr1 t1 t) & (pr1 t2 t)).
      Proof.
      Intros until 1; XElim H; Intros.
(* case 1 : pr1_r *)
      XDEAuto 3.
(* case 2 : pr1_u *)
      Pr0Confluence.
      LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
      XDecompose H1; XDEAuto 4.
      Qed.

      Theorem pr1_confluence: (t0,t1:?) (pr1 t0 t1) -> (t2:?) (pr1 t0 t2) ->
                              (EX t | (pr1 t1 t) & (pr1 t2 t)).
      Proof.
      Intros until 1; XElim H; Intros.
(* case 1 : pr1_r *)
      XDEAuto 2.
(* case 2 : pr1_u *)
      XDecomPoseClear H '(pr1_strip ? ? H2 ? H); Clear H2.
      XDecomPoseClear H1 '(H1 ? H4); Clear H4.
      XDEAuto 3.
      Qed.

   End pr1_confluence.

      Tactic Definition Pr1Confluence := (
         Match Context With
            | [ H1: (pr1 ?1 ?2); H2: (pr0 ?1 ?3) |-? ] ->
               LApply (pr1_strip ?1 ?2); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?3); [ Clear H1 H2; Intros H1 | XAuto ];
               XElim H1; Intros
            | [ H1: (pr1 ?1 ?2); H2: (pr1 ?1 ?3) |-? ] ->
               LApply (pr1_confluence ?1 ?2); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?3); [ Clear H1 H2; Intros H1 | XAuto ];
               XElim H1; Intros
            | [ |- ? ] -> Pr0Confluence
         ).