1 Require pr2_confluence.
4 Section pr3_confluence. (*************************************************)
8 (*#* #caption "confluence with single step reduction: strip lemma" *)
9 (*#* #cap #cap c, t0, t1, t2, t *)
11 Theorem pr3_strip : (c:?; t0,t1:?) (pr3 c t0 t1) -> (t2:?) (pr2 c t0 t2) ->
12 (EX t | (pr3 c t1 t) & (pr3 c t2 t)).
13 Intros until 1; XElim H; Intros.
14 (* case 1 : pr3_refl *)
16 (* case 2 : pr3_sing *)
18 LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
19 XElim H1; Intros; XEAuto.
22 (*#* #start theorem *)
24 (*#* #caption "confluence with itself: Church-Rosser property" *)
25 (*#* #cap #cap c, t0, t1, t2, t *)
27 Theorem pr3_confluence : (c:?; t0,t1:?) (pr3 c t0 t1) -> (t2:?) (pr3 c t0 t2) ->
28 (EX t | (pr3 c t1 t) & (pr3 c t2 t)).
32 Intros until 1; XElim H; Intros.
33 (* case 1 : pr3_refl *)
35 (* case 2 : pr3_sing *)
36 LApply (pr3_strip c t3 t5); [ Clear H2; Intros H2 | XAuto ].
37 LApply (H2 t2); [ Clear H H2; Intros H | XAuto ].
39 LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
40 XElim H1; Intros; XEAuto.
45 Tactic Definition Pr3Confluence :=
47 | [ H1: (pr3 ?1 ?2 ?3); H2: (pr2 ?1 ?2 ?4) |-? ] ->
48 LApply (pr3_strip ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
49 LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];
51 | [ H1: (pr3 ?1 ?2 ?3); H2: (pr3 ?1 ?2 ?4) |-? ] ->
52 LApply (pr3_confluence ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
53 LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];