(****************************************************************************) (* *) (* The formal system \lambda\delta *) (* *) (* Author: Ferruccio Guidi *) (* *) (* This file is distributed under the terms of the *) (* GNU General Public License Version 2 *) (* *) (****************************************************************************) Require pr2_confluence. Require pr3_defs. Section pr3_confluence. (*************************************************) Hints Resolve pr3_sing : ld. Lemma pr3_strip: (c:?; t0,t1:?) (pr3 c t0 t1) -> (t2:?) (pr2 c t0 t2) -> (EX t | (pr3 c t1 t) & (pr3 c t2 t)). Proof. Intros until 1; XElim H; Intros. (* case 1 : pr3_refl *) XDEAuto 3. (* case 2 : pr3_sing *) Pr2Confluence. LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ]. XElim H1; Intros; XDEAuto 3. Qed. Hints Resolve pr3_t : ld. Theorem pr3_confluence: (c:?; t0,t1:?) (pr3 c t0 t1) -> (t2:?) (pr3 c t0 t2) -> (EX t | (pr3 c t1 t) & (pr3 c t2 t)). Proof. Intros until 1; XElim H; Intros. (* case 1 : pr3_refl *) XDEAuto 2. (* case 2 : pr3_sing *) LApply (pr3_strip c t3 t5); [ Clear H2; Intros H2 | XAuto ]. LApply (H2 t2); [ Clear H H2; Intros H | XAuto ]. XElim H; Intros. LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ]. XElim H1; Intros; XDEAuto 3. Qed. End pr3_confluence. Tactic Definition Pr3Confluence := ( Match Context With | [ H1: (pr3 ?1 ?2 ?3); H2: (pr2 ?1 ?2 ?4) |-? ] -> LApply (pr3_strip ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ]; LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ]; XElim H1; Intros | [ H1: (pr3 ?1 ?2 ?3); H2: (pr3 ?1 ?2 ?4) |-? ] -> LApply (pr3_confluence ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ]; LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ]; XElim H1; Intros | [ |- ? ] -> Pr2Confluence ).