8 Require pr3_confluence.
11 Section pc3_confluence. (*************************************************)
13 Theorem pc3_confluence: (c:?; t1,t2:?) (pc3 c t1 t2) ->
14 (EX t0 | (pr3 c t1 t0) & (pr3 c t2 t0)).
15 Intros; XElim H; Intros.
19 Clear H0; XElim H1; Intros.
20 Inversion_clear H; [ XEAuto | Pr3Confluence; XEAuto ].
25 Tactic Definition Pc3Confluence :=
27 [ H: (pc3 ?1 ?2 ?3) |- ? ] ->
28 LApply (pc3_confluence ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
31 Section pc3_context. (****************************************************)
33 Theorem pc3_pr0_pr2_t: (u1,u2:?) (pr0 u2 u1) ->
34 (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
35 (pc3 (CTail c k u1) t1 t2).
37 Inversion H0; Clear H0; [ XAuto | NewInduction i ].
38 (* case 1: pr2_delta i = 0 *)
39 DropGenBase; Inversion H0; Clear H0 H4 H5 H6 c k t.
40 Rewrite H7 in H; Clear H7 u2.
41 Pr0Subst0; Apply pc3_pr3_t with t0:=x; XEAuto.
42 (* case 2: pr2_delta i > 0 *)
43 NewInduction k; DropGenBase; XEAuto.
46 Theorem pc3_pr2_pr2_t: (c:?; u1,u2:?) (pr2 c u2 u1) ->
47 (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
48 (pc3 (CTail c k u1) t1 t2).
49 Intros until 1; Inversion H; Clear H; Intros.
50 (* case 1: pr2_free *)
51 EApply pc3_pr0_pr2_t; [ Apply H0 | XAuto ].
52 (* case 2: pr2_delta *)
53 Inversion H; [ XAuto | NewInduction i0 ].
54 (* case 2.1: i0 = 0 *)
55 DropGenBase; Inversion H4; Clear H3 H4 H7 t t4.
56 Rewrite <- H9; Rewrite H10 in H; Rewrite <- H11 in H6; Clear H9 H10 H11 d0 k u0.
57 Pr0Subst0; Subst0Subst0; Arith9'In H6 i.
59 EApply pr2_delta; XEAuto.
60 Apply pc3_pr2_x; EApply pr2_delta; [ Idtac | XEAuto | XEAuto ]; XEAuto.
61 (* case 2.2: i0 > 0 *)
62 Clear IHi0; NewInduction k; DropGenBase; XEAuto.
65 Theorem pc3_pr2_pr3_t: (c:?; u2,t1,t2:?; k:?)
66 (pr3 (CTail c k u2) t1 t2) ->
67 (u1:?) (pr2 c u2 u1) ->
68 (pc3 (CTail c k u1) t1 t2).
69 Intros until 1; XElim H; Intros.
70 (* case 1: pr3_refl *)
72 (* case 2: pr3_sing *)
74 EApply pc3_pr2_pr2_t; [ Apply H2 | Apply H ].
78 Theorem pc3_pr3_pc3_t: (c:?; u1,u2:?) (pr3 c u2 u1) ->
79 (t1,t2:?; k:?) (pc3 (CTail c k u2) t1 t2) ->
80 (pc3 (CTail c k u1) t1 t2).
81 Intros until 1; XElim H; Intros.
82 (* case 1: pr3_refl *)
84 (* case 2: pr3_sing *)
85 Apply H1; Pc3Confluence.
86 EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_pr2_pr3_t; XEAuto.
91 Tactic Definition Pc3Context :=
93 | [ H1: (pr0 ?3 ?2); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
94 LApply (pc3_pr0_pr2_t ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
95 LApply (H1 ?1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
96 | [ H1: (pr0 ?3 ?2); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
97 LApply (pc3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
98 LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
99 | [ H1: (pr2 ?1 ?3 ?2); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
100 LApply (pc3_pr2_pr2_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
101 LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
102 | [ H1: (pr2 ?1 ?3 ?2); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
103 LApply (pc3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
104 LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
105 | [ H1: (pr3 ?1 ?3 ?2); H2: (pc3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
106 LApply (pc3_pr3_pc3_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
107 LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
110 Section pc3_lift. (*******************************************************)
112 Theorem pc3_lift: (c,e:?; h,d:?) (drop h d c e) ->
113 (t1,t2:?) (pc3 e t1 t2) ->
114 (pc3 c (lift h d t1) (lift h d t2)).
118 EApply pc3_pr3_t; (EApply pr3_lift; [ XEAuto | Apply H0 Orelse Apply H1 ]).
123 Hints Resolve pc3_lift : ltlc.
125 Section pc3_cpr0. (*******************************************************)
127 Remark pc3_cpr0_t_aux: (c1,c2:?) (cpr0 c1 c2) ->
128 (k:?; u,t1,t2:?) (pr3 (CTail c1 k u) t1 t2) ->
129 (pc3 (CTail c2 k u) t1 t2).
130 Intros; XElim H0; Intros.
131 (* case 1.1: pr3_refl *)
133 (* case 1.2: pr3_sing *)
134 EApply pc3_t; [ Idtac | XEAuto ]. Clear H2 t1 t2.
136 (* case 1.2.1: pr2_free *)
138 (* case 1.2.2: pr2_delta *)
140 EApply pc3_pr3_u; [ EApply pr2_delta; XEAuto | XAuto ].
143 Theorem pc3_cpr0_t: (c1,c2:?) (cpr0 c1 c2) ->
144 (t1,t2:?) (pr3 c1 t1 t2) ->
146 Intros until 1; XElim H; Intros.
147 (* case 1: cpr0_refl *)
149 (* case 2: cpr0_comp *)
150 Pc3Context; Pc3Confluence.
151 EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t_aux; XEAuto.
154 Theorem pc3_cpr0: (c1,c2:?) (cpr0 c1 c2) -> (t1,t2:?) (pc3 c1 t1 t2) ->
156 Intros; Pc3Confluence.
157 EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t; XEAuto.
162 Hints Resolve pc3_cpr0 : ltlc.