7 Require pr3_confluence.
12 Section pc3_confluence. (*************************************************)
14 Theorem pc3_confluence : (c:?; t1,t2:?) (pc3 c t1 t2) ->
15 (EX t0 | (pr3 c t1 t0) & (pr3 c t2 t0)).
16 Intros; XElim H; Intros.
20 Clear H0; XElim H1; Intros.
21 Inversion_clear H; [ XEAuto | Pr3Confluence; XEAuto ].
26 Tactic Definition Pc3Confluence :=
28 [ H: (pc3 ?1 ?2 ?3) |- ? ] ->
29 LApply (pc3_confluence ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
32 Section pc3_context. (****************************************************)
34 Theorem pc3_pr0_pr2_t : (u1,u2:?) (pr0 u2 u1) ->
35 (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
36 (pc3 (CTail c k u1) t1 t2).
38 Inversion H0; Clear H0; [ XAuto | NewInduction i ].
39 (* case 1 : pr2_delta i = 0 *)
40 DropGenBase; Inversion H0; Clear H0 H3 H4 c k.
41 Rewrite H5 in H; Clear H5 u2.
43 (* case 2 : pr2_delta i > 0 *)
44 NewInduction k; DropGenBase; XEAuto.
47 Theorem pc3_pr2_pr2_t : (c:?; u1,u2:?) (pr2 c u2 u1) ->
48 (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
49 (pc3 (CTail c k u1) t1 t2).
50 Intros until 1; Inversion H; Clear H; Intros.
51 (* case 1 : pr2_pr0 *)
52 EApply pc3_pr0_pr2_t; [ Apply H0 | XAuto ].
53 (* case 2 : pr2_delta *)
54 Inversion H; [ XAuto | NewInduction i0 ].
55 (* case 2.1 : i0 = 0 *)
56 DropGenBase; Inversion H2; Clear H2.
57 Rewrite <- H5; Rewrite H6 in H; Rewrite <- H7 in H3; Clear H5 H6 H7 d0 k u0.
58 Subst0Subst0; Arith9'In H4 i.
60 EApply pr2_delta; XEAuto.
61 Apply pc3_pr2_x; EApply pr2_delta; [ Idtac | XEAuto ]; XEAuto.
62 (* case 2.2 : i0 > 0 *)
63 Clear IHi0; NewInduction k; DropGenBase; XEAuto.
66 Theorem pc3_pr2_pr3_t : (c:?; u2,t1,t2:?; k:?)
67 (pr3 (CTail c k u2) t1 t2) ->
68 (u1:?) (pr2 c u2 u1) ->
69 (pc3 (CTail c k u1) t1 t2).
70 Intros until 1; XElim H; Intros.
75 EApply pc3_pr2_pr2_t; [ Apply H2 | Apply H ].
79 Theorem pc3_pr3_pc3_t : (c:?; u1,u2:?) (pr3 c u2 u1) ->
80 (t1,t2:?; k:?) (pc3 (CTail c k u2) t1 t2) ->
81 (pc3 (CTail c k u1) t1 t2).
82 Intros until 1; XElim H; Intros.
86 Apply H1; Pc3Confluence.
87 EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_pr2_pr3_t; XEAuto.
92 Tactic Definition Pc3Context :=
94 | [ H1: (pr0 ?3 ?2); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
95 LApply (pc3_pr0_pr2_t ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
96 LApply (H1 ?1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
97 | [ H1: (pr0 ?3 ?2); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
98 LApply (pc3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
99 LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
100 | [ H1: (pr2 ?1 ?3 ?2); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
101 LApply (pc3_pr2_pr2_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
102 LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
103 | [ H1: (pr2 ?1 ?3 ?2); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
104 LApply (pc3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
105 LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
106 | [ H1: (pr3 ?1 ?3 ?2); H2: (pc3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
107 LApply (pc3_pr3_pc3_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
108 LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
111 Section pc3_lift. (*******************************************************)
113 Theorem pc3_lift : (c,e:?; h,d:?) (drop h d c e) ->
114 (t1,t2:?) (pc3 e t1 t2) ->
115 (pc3 c (lift h d t1) (lift h d t2)).
119 EApply pc3_pr3_t; (EApply pr3_lift; [ XEAuto | Apply H0 Orelse Apply H1 ]).
124 Hints Resolve pc3_lift : ltlc.
126 Section pc3_cpr0. (*******************************************************)
128 Remark pc3_cpr0_t_aux : (c1,c2:?) (cpr0 c1 c2) ->
129 (k:?; u,t1,t2:?) (pr3 (CTail c1 k u) t1 t2) ->
130 (pc3 (CTail c2 k u) t1 t2).
131 Intros; XElim H0; Intros.
132 (* case 1.1 : pr3_r *)
134 (* case 1.2 : pr3_u *)
135 EApply pc3_t; [ Idtac | XEAuto ]. Clear H2 t1 t2.
137 (* case 1.2.1 : pr2_pr0 *)
139 (* case 1.2.2 : pr2_delta *)
141 EApply pc3_pr3_u; [ EApply pr2_delta; XEAuto | XAuto ].
144 Theorem pc3_cpr0_t : (c1,c2:?) (cpr0 c1 c2) ->
145 (t1,t2:?) (pr3 c1 t1 t2) ->
147 Intros until 1; XElim H; Intros.
148 (* case 1 : cpr0_refl *)
150 (* case 2 : cpr0_cont *)
151 Pc3Context; Pc3Confluence.
152 EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t_aux; XEAuto.
155 Theorem pc3_cpr0 : (c1,c2:?) (cpr0 c1 c2) -> (t1,t2:?) (pc3 c1 t1 t2) ->
157 Intros; Pc3Confluence.
158 EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t; XEAuto.
163 Hints Resolve pc3_cpr0 : ltlc.