8 Require pr3_confluence.
11 Section pc3_trans. (******************************************************)
13 Theorem pc3_t: (t2,c,t1:?) (pc3 c t1 t2) ->
14 (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
15 Intros; Repeat Pc3Unfold; Pr3Confluence; XEAuto.
18 Theorem pc3_pr2_u2: (c:?; t0,t1:?) (pr2 c t0 t1) ->
19 (t2:?) (pc3 c t0 t2) -> (pc3 c t1 t2).
20 Intros; Apply (pc3_t t0); XAuto.
23 Theorem pc3_tail_12: (c:?; u1,u2:?) (pc3 c u1 u2) ->
24 (k:?; t1,t2:?) (pc3 (CTail c k u2) t1 t2) ->
25 (pc3 c (TTail k u1 t1) (TTail k u2 t2)).
27 EApply pc3_t; [ Apply pc3_tail_1 | Apply pc3_tail_2 ]; XAuto.
30 Theorem pc3_tail_21: (c:?; u1,u2:?) (pc3 c u1 u2) ->
31 (k:?; t1,t2:?) (pc3 (CTail c k u1) t1 t2) ->
32 (pc3 c (TTail k u1 t1) (TTail k u2 t2)).
34 EApply pc3_t; [ Apply pc3_tail_2 | Apply pc3_tail_1 ]; XAuto.
39 Hints Resolve pc3_t pc3_tail_12 pc3_tail_21 : ltlc.
41 Tactic Definition Pc3T :=
43 | [ _: (pr3 ?1 ?2 (TTail ?3 ?4 ?5)); _: (pc3 ?1 ?6 ?4) |- ? ] ->
44 LApply (pc3_t (TTail ?3 ?4 ?5) ?1 ?2); [ Intros H_x | XAuto ];
45 LApply (H_x (TTail ?3 ?6 ?5)); [ Clear H_x; Intros | Apply pc3_s; XAuto ]
46 | [ _: (pc3 ?1 ?2 ?3); _: (pr3 ?1 ?3 ?4) |- ? ] ->
47 LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
48 LApply (H_x ?4); [ Clear H_x; Intros | XAuto ]
49 | [ _: (pc3 ?1 ?2 ?3); _: (pc3 ?1 ?4 ?3) |- ? ] ->
50 LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
51 LApply (H_x ?4); [ Clear H_x; Intros | XAuto ].
53 Section pc3_context. (****************************************************)
55 Theorem pc3_pr0_pr2_t: (u1,u2:?) (pr0 u2 u1) ->
56 (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
57 (pc3 (CTail c k u1) t1 t2).
59 Inversion H0; Clear H0; [ XAuto | NewInduction i ].
60 (* case 1: pr2_delta i = 0 *)
61 DropGenBase; Inversion H0; Clear H0 H4 H5 H6 c k t.
62 Rewrite H7 in H; Clear H7 u2.
63 Pr0Subst0; Apply pc3_pr3_t with t0:=x; XEAuto.
64 (* case 2: pr2_delta i > 0 *)
65 NewInduction k; DropGenBase; XEAuto.
68 Theorem pc3_pr2_pr2_t: (c:?; u1,u2:?) (pr2 c u2 u1) ->
69 (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
70 (pc3 (CTail c k u1) t1 t2).
71 Intros until 1; Inversion H; Clear H; Intros.
72 (* case 1: pr2_free *)
73 EApply pc3_pr0_pr2_t; [ Apply H0 | XAuto ].
74 (* case 2: pr2_delta *)
75 Inversion H; [ XAuto | NewInduction i0 ].
76 (* case 2.1: i0 = 0 *)
77 DropGenBase; Inversion H4; Clear H3 H4 H7 t t4.
78 Rewrite <- H9; Rewrite H10 in H; Rewrite <- H11 in H6; Clear H9 H10 H11 d0 k u0.
79 Pr0Subst0; Subst0Subst0; Arith9'In H6 i.
81 EApply pr2_delta; XEAuto.
82 Apply pc3_pr2_x; EApply pr2_delta; [ Idtac | XEAuto | XEAuto ]; XEAuto.
83 (* case 2.2: i0 > 0 *)
84 Clear IHi0; NewInduction k; DropGenBase; XEAuto.
87 Theorem pc3_pr2_pr3_t: (c:?; u2,t1,t2:?; k:?)
88 (pr3 (CTail c k u2) t1 t2) ->
89 (u1:?) (pr2 c u2 u1) ->
90 (pc3 (CTail c k u1) t1 t2).
91 Intros until 1; XElim H; Intros.
92 (* case 1: pr3_refl *)
94 (* case 2: pr3_sing *)
96 EApply pc3_pr2_pr2_t; [ Apply H2 | Apply H ].
100 Theorem pc3_pr3_pc3_t: (c:?; u1,u2:?) (pr3 c u2 u1) ->
101 (t1,t2:?; k:?) (pc3 (CTail c k u2) t1 t2) ->
102 (pc3 (CTail c k u1) t1 t2).
103 Intros until 1; XElim H; Intros.
104 (* case 1: pr3_refl *)
106 (* case 2: pr3_sing *)
108 EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_pr2_pr3_t; XEAuto.
113 Tactic Definition Pc3Context :=
115 | [ H1: (pr0 ?3 ?2); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
116 LApply (pc3_pr0_pr2_t ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
117 LApply (H1 ?1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
118 | [ H1: (pr0 ?3 ?2); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
119 LApply (pc3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
120 LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
121 | [ H1: (pr2 ?1 ?3 ?2); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
122 LApply (pc3_pr2_pr2_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
123 LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
124 | [ H1: (pr2 ?1 ?3 ?2); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
125 LApply (pc3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
126 LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
127 | [ H1: (pr3 ?1 ?3 ?2); H2: (pc3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
128 LApply (pc3_pr3_pc3_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
129 LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
132 Section pc3_lift. (*******************************************************)
134 Theorem pc3_lift: (c,e:?; h,d:?) (drop h d c e) ->
135 (t1,t2:?) (pc3 e t1 t2) ->
136 (pc3 c (lift h d t1) (lift h d t2)).
140 EApply pc3_pr3_t; (EApply pr3_lift; [ XEAuto | Apply H1 Orelse Apply H2 ]).
145 Hints Resolve pc3_lift : ltlc.
147 Section pc3_cpr0. (*******************************************************)
149 Remark pc3_cpr0_t_aux: (c1,c2:?) (cpr0 c1 c2) ->
150 (k:?; u,t1,t2:?) (pr3 (CTail c1 k u) t1 t2) ->
151 (pc3 (CTail c2 k u) t1 t2).
152 Intros; XElim H0; Intros.
153 (* case 1.1: pr3_refl *)
155 (* case 1.2: pr3_sing *)
156 EApply pc3_t; [ Idtac | XEAuto ]. Clear H2 t1 t2.
158 (* case 1.2.1: pr2_free *)
160 (* case 1.2.2: pr2_delta *)
162 EApply pc3_pr2_u; [ EApply pr2_delta; XEAuto | XAuto ].
165 Theorem pc3_cpr0_t: (c1,c2:?) (cpr0 c1 c2) ->
166 (t1,t2:?) (pr3 c1 t1 t2) ->
168 Intros until 1; XElim H; Intros.
169 (* case 1: cpr0_refl *)
171 (* case 2: cpr0_comp *)
172 Pc3Context; Pc3Unfold.
173 EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t_aux; XEAuto.
176 Theorem pc3_cpr0: (c1,c2:?) (cpr0 c1 c2) -> (t1,t2:?) (pc3 c1 t1 t2) ->
179 EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t; XEAuto.
184 Hints Resolve pc3_cpr0 : ltlc.
186 Section pc3_ind_left. (***************************************************)
188 Inductive pc3_left [c:C] : T -> T -> Prop :=
189 | pc3_left_r : (t:?) (pc3_left c t t)
190 | pc3_left_ur: (t1,t2:?) (pr2 c t1 t2) -> (t3:?) (pc3_left c t2 t3) ->
192 | pc3_left_ux: (t1,t2:?) (pr2 c t1 t2) -> (t3:?) (pc3_left c t1 t3) ->
195 Hint pc3_left: ltlc := Constructors pc3_left.
197 Remark pc3_left_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) -> (pc3_left c t1 t2).
198 Intros; XElim H; XEAuto.
201 Remark pc3_left_trans: (c:?; t1,t2:?) (pc3_left c t1 t2) ->
202 (t3:?) (pc3_left c t2 t3) -> (pc3_left c t1 t3).
203 Intros until 1; XElim H; XEAuto.
206 Hints Resolve pc3_left_trans : ltlc.
208 Remark pc3_left_sym: (c:?; t1,t2:?) (pc3_left c t1 t2) ->
210 Intros; XElim H; XEAuto.
213 Hints Resolve pc3_left_sym pc3_left_pr3 : ltlc.
215 Remark pc3_left_pc3: (c:?; t1,t2:?) (pc3 c t1 t2) -> (pc3_left c t1 t2).
216 Intros; Pc3Unfold; XEAuto.
219 Remark pc3_pc3_left: (c:?; t1,t2:?) (pc3_left c t1 t2) -> (pc3 c t1 t2).
220 Intros; XElim H; XEAuto.
223 Hints Resolve pc3_left_pc3 pc3_pc3_left : ltlc.
225 Theorem pc3_ind_left: (c:C; P:(T->T->Prop))
227 ((t1,t2:T) (pr2 c t1 t2) -> (t3:T) (pc3 c t2 t3) -> (P t2 t3) -> (P t1 t3)) ->
228 ((t1,t2:T) (pr2 c t1 t2) -> (t3:T) (pc3 c t1 t3) -> (P t1 t3) -> (P t2 t3)) ->
229 (t,t0:T) (pc3 c t t0) -> (P t t0).
230 Intros; ElimType (pc3_left c t t0); XEAuto.