3 Require pr0_confluence.
6 (*#* #caption "main properties of predicate \\texttt{pr1}" *)
7 (*#* #clauses pr1_props *)
9 Section pr1_confluence. (*************************************************)
11 (*#* #caption "confluence with single step reduction: strip lemma" *)
12 (*#* #cap #cap t0, t1, t2, t *)
14 Theorem pr1_strip : (t0,t1:?) (pr1 t0 t1) -> (t2:?) (pr0 t0 t2) ->
15 (EX t | (pr1 t1 t) & (pr1 t2 t)).
16 Intros until 1; XElim H; Intros.
21 LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
22 XElim H1; Intros; XEAuto.
25 (*#* #caption "confluence with itself: Church-Rosser property" *)
26 (*#* #cap #cap t0, t1, t2, t *)
28 Theorem pr1_confluence : (t0,t1:?) (pr1 t0 t1) -> (t2:?) (pr1 t0 t2) ->
29 (EX t | (pr1 t1 t) & (pr1 t2 t)).
30 Intros until 1; XElim H; Intros.
34 LApply (pr1_strip t3 t5); [ Clear H2; Intros H2 | XAuto ].
35 LApply (H2 t2); [ Clear H H2; Intros H | XAuto ].
37 LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
38 XElim H1; Intros; XEAuto.
43 Tactic Definition Pr1Confluence :=
45 | [ H1: (pr1 ?1 ?2); H2: (pr0 ?1 ?3) |-? ] ->
46 LApply (pr1_strip ?1 ?2); [ Clear H1; Intros H1 | XAuto ];
47 LApply (H1 ?3); [ Clear H1 H2; Intros H1 | XAuto ];
49 | [ H1: (pr1 ?1 ?2); H2: (pr1 ?1 ?3) |-? ] ->
50 LApply (pr1_confluence ?1 ?2); [ Clear H1; Intros H1 | XAuto ];
51 LApply (H1 ?3); [ Clear H1 H2; Intros H1 | XAuto ];