1 Require Export pr2_defs.
2 Require Export pr3_defs.
3 Require Export pc1_defs.
7 Inductive pc2 [c:C; t1,t2:T] : Prop :=
8 | pc2_r : (pr2 c t1 t2) -> (pc2 c t1 t2)
9 | pc2_x : (pr2 c t2 t1) -> (pc2 c t1 t2).
11 Hint pc2 : ltlc := Constructors pc2.
15 (*#* #caption "axioms for the relation $\\PcT{}{}{}$",
16 "reflexivity", "single step transitivity"
18 (*#* #cap #cap c, t, t1, t2, t3 *)
20 Inductive pc3 [c:C] : T -> T -> Prop :=
21 | pc3_r : (t:?) (pc3 c t t)
22 | pc3_u : (t2,t1:?) (pc2 c t1 t2) ->
23 (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
27 Hint pc3 : ltlc := Constructors pc3.
29 Section pc2_props. (******************************************************)
31 Theorem pc2_s : (c,t2,t1:?) (pc2 c t1 t2) -> (pc2 c t2 t1).
36 Theorem pc2_shift : (h:?; c,e:?) (drop h (0) c e) ->
37 (t1,t2:?) (pc2 c t1 t2) ->
38 (pc2 e (app c h t1) (app c h t2)).
39 Intros until 2; XElim H0; Intros.
48 Hints Resolve pc2_s pc2_shift : ltlc.
50 Section pc3_props. (******************************************************)
52 Theorem pc3_pr2_r : (c,t1,t2:?) (pr2 c t1 t2) -> (pc3 c t1 t2).
56 Theorem pc3_pr2_x : (c,t1,t2:?) (pr2 c t2 t1) -> (pc3 c t1 t2).
60 Theorem pc3_pc2 : (c,t1,t2:?) (pc2 c t1 t2) -> (pc3 c t1 t2).
64 Theorem pc3_t : (t2,c,t1:?) (pc3 c t1 t2) ->
65 (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
66 Intros t2 c t1 H; XElim H; XEAuto.
69 Hints Resolve pc3_t : ltlc.
71 Theorem pc3_s : (c,t2,t1:?) (pc3 c t1 t2) -> (pc3 c t2 t1).
72 Intros; XElim H; [ XAuto | XEAuto ].
75 Hints Resolve pc3_s : ltlc.
77 Theorem pc3_pr3_r : (c:?; t1,t2) (pr3 c t1 t2) -> (pc3 c t1 t2).
78 Intros; XElim H; XEAuto.
81 Theorem pc3_pr3_x : (c:?; t1,t2) (pr3 c t2 t1) -> (pc3 c t1 t2).
82 Intros; XElim H; XEAuto.
85 Hints Resolve pc3_pr3_r pc3_pr3_x : ltlc.
87 Theorem pc3_pr3_t : (c:?; t1,t0:?) (pr3 c t1 t0) ->
88 (t2:?) (pr3 c t2 t0) -> (pc3 c t1 t2).
89 Intros; Apply (pc3_t t0); XAuto.
92 Theorem pc3_thin_dx : (c:? ;t1,t2:?) (pc3 c t1 t2) ->
93 (u:?; f:?) (pc3 c (TTail (Flat f) u t1)
94 (TTail (Flat f) u t2)).
95 Intros; XElim H; [XAuto | Intros ].
96 EApply pc3_u; [ Inversion H | Apply H1 ]; XAuto.
99 Theorem pc3_tail_1 : (c:?; u1,u2:?) (pc3 c u1 u2) ->
100 (k:?; t:?) (pc3 c (TTail k u1 t) (TTail k u2 t)).
101 Intros until 1; XElim H; Intros.
105 EApply pc3_u; [ Inversion H | Apply H1 ]; XAuto.
108 Theorem pc3_tail_2 : (c:?; u,t1,t2:?; k:?) (pc3 (CTail c k u) t1 t2) ->
109 (pc3 c (TTail k u t1) (TTail k u t2)).
111 XElim H; [ Idtac | Intros; Inversion H ]; XEAuto.
114 Theorem pc3_tail_12 : (c:?; u1,u2:?) (pc3 c u1 u2) ->
115 (k:?; t1,t2:?) (pc3 (CTail c k u2) t1 t2) ->
116 (pc3 c (TTail k u1 t1) (TTail k u2 t2)).
118 EApply pc3_t; [ Apply pc3_tail_1 | Apply pc3_tail_2 ]; XAuto.
121 Theorem pc3_tail_21 : (c:?; u1,u2:?) (pc3 c u1 u2) ->
122 (k:?; t1,t2:?) (pc3 (CTail c k u1) t1 t2) ->
123 (pc3 c (TTail k u1 t1) (TTail k u2 t2)).
125 EApply pc3_t; [ Apply pc3_tail_2 | Apply pc3_tail_1 ]; XAuto.
128 Theorem pc3_pr3_u : (c:?; t2,t1:?) (pr2 c t1 t2) ->
129 (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
133 Theorem pc3_pr3_u2 : (c:?; t0,t1:?) (pr2 c t0 t1) ->
134 (t2:?) (pc3 c t0 t2) -> (pc3 c t1 t2).
135 Intros; Apply (pc3_t t0); XAuto.
138 Theorem pc3_shift : (h:?; c,e:?) (drop h (0) c e) ->
139 (t1,t2:?) (pc3 c t1 t2) ->
140 (pc3 e (app c h t1) (app c h t2)).
141 Intros until 2; XElim H0; Clear t1 t2; Intros.
148 Theorem pc3_pc1: (t1,t2:?) (pc1 t1 t2) -> (c:?) (pc3 c t1 t2).
149 Intros; XElim H; Intros.
158 Hints Resolve pc3_pr2_r pc3_pr2_x pc3_pc2 pc3_pr3_r pc3_pr3_x
159 pc3_t pc3_s pc3_pr3_t pc3_thin_dx pc3_tail_1 pc3_tail_2
160 pc3_tail_12 pc3_tail_21 pc3_pr3_u pc3_shift pc3_pc1 : ltlc.
162 Tactic Definition Pc3T :=
164 | [ _: (pr3 ?1 ?2 (TTail ?3 ?4 ?5)); _: (pc3 ?1 ?6 ?4) |- ? ] ->
165 LApply (pc3_t (TTail ?3 ?4 ?5) ?1 ?2); [ Intros H_x | XAuto ];
166 LApply (H_x (TTail ?3 ?6 ?5)); [ Clear H_x; Intros | Apply pc3_s; XAuto ]
167 | [ _: (pc3 ?1 ?2 ?3); _: (pr3 ?1 ?3 ?4) |- ? ] ->
168 LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
169 LApply (H_x ?4); [ Clear H_x; Intros | XAuto ]
170 | [ _: (pc3 ?1 ?2 ?3); _: (pc3 ?1 ?4 ?3) |- ? ] ->
171 LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
172 LApply (H_x ?4); [ Clear H_x; Intros | XAuto ].