(****************************************************************************)
(*                                                                          *)
(*                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_confluence.
Require getl_props.
Require pr0_subst0.
Require pr0_confluence.
Require pr2_defs.

   Section pr2_confluence. (*************************************************)

(* case 1.1 : pr2_free pr2_free *********************************************)

      Remark pr2_free_free: (c:?; t0,t1,t2:?)
                            (pr0 t0 t1) -> (pr0 t0 t2) ->
                            (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
      Proof.
      Intros; Pr0Confluence; XDEAuto 4.
      Qed.

(* case 1.2 : pr2_free pr2_delta ********************************************)

      Remark pr2_free_delta: (c,d:?; t0,t1,t2,t4,u:?; i:?)
                             (pr0 t0 t1) ->
                             (getl i c (CHead d (Bind Abbr) u)) ->
                             (pr0 t0 t4) ->
                             (subst0 i u t4 t2) ->
                             (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
      Proof.
      Intros; Pr0Confluence; Pr0Subst0; XDEAuto 4.
      Qed.

(* case 2.2 : pr2_delta pr2_delta *******************************************)

      Hints Resolve sym_not_eq : ld.

      Remark pr2_delta_delta: (c,d,d0:?; t0,t1,t2,t3,t4,u,u0:?; i,i0:?)
                              (getl i c (CHead d (Bind Abbr) u)) ->
                              (pr0 t0 t3) ->
                              (subst0 i u t3 t1) ->
                              (getl i0 c (CHead d0 (Bind Abbr) u0)) ->
                              (pr0 t0 t4) ->
                              (subst0 i0 u0 t4 t2) ->
                              (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
      Proof.
      Intros; Pr0Confluence; Repeat Pr0Subst0;
      [ XDEAuto 4 | XDEAuto 4 | XDEAuto 4 | Idtac ].
      Apply (neq_eq_e i i0); Intros; Subst.
(* case 1 : i != i0 *)
      Subst0Confluence; XDEAuto 4.
(* case 2 : i = i0 *)
      GetLDis; XInv; Subst.
      Subst0Confluence; Subst; XDEAuto 4.
      Qed.

(* main *********************************************************************)

      Hints Resolve pr2_free_free pr2_free_delta pr2_delta_delta : ld.
      Hints Resolve ex2_sym : ld.

      Theorem pr2_confluence: (c,t0,t1:?) (pr2 c t0 t1) ->
                              (t2:?) (pr2 c t0 t2) ->
                              (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
      Proof.
      Intros; Inversion H; Inversion H0; XDEAuto 3.
      Qed.

   End pr2_confluence.

      Tactic Definition Pr2Confluence := (
         Match Context With
            | [ H1: (pr2 ?1 ?2 ?3); H2: (pr2 ?1 ?2 ?4) |-? ] ->
               LApply (pr2_confluence ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];
               XElim H1; Intros
            | [ |- ? ] -> Pr0Confluence
         ).