6 (*#* #caption "main properties of predicate \\texttt{pr3}" *)
11 Section pr3_context. (****************************************************)
13 Theorem pr3_pr0_pr2_t : (u1,u2:?) (pr0 u1 u2) ->
14 (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
15 (pr3 (CTail c k u1) t1 t2).
17 Inversion H0; Clear H0; XAuto.
19 (* case 1 : pr2_delta i = 0 *)
20 DropGenBase; Inversion H0; Clear H0 H3 H4 c k.
21 Rewrite H5 in H; Clear H5 u2.
23 (* case 2 : pr2_delta i > 0 *)
24 NewInduction k; DropGenBase; XEAuto.
27 Theorem pr3_pr2_pr2_t : (c:?; u1,u2:?) (pr2 c u1 u2) ->
28 (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
29 (pr3 (CTail c k u1) t1 t2).
30 Intros until 1; Inversion H; Clear H; Intros.
31 (* case 1 : pr2_pr0 *)
32 EApply pr3_pr0_pr2_t; [ Apply H0 | XAuto ].
33 (* case 2 : pr2_delta *)
34 Inversion H; [ XAuto | NewInduction i0 ].
35 (* case 2.1 : i0 = 0 *)
36 DropGenBase; Inversion H2; Clear H2.
37 Rewrite <- H5; Rewrite H6 in H; Rewrite <- H7 in H3; Clear H5 H6 H7 d0 k u0.
38 Subst0Subst0; Arith9'In H4 i; XDEAuto 7.
39 (* case 2.2 : i0 > 0 *)
40 Clear IHi0; NewInduction k; DropGenBase; XEAuto.
43 Theorem pr3_pr2_pr3_t : (c:?; u2,t1,t2:?; k:?)
44 (pr3 (CTail c k u2) t1 t2) ->
45 (u1:?) (pr2 c u1 u2) ->
46 (pr3 (CTail c k u1) t1 t2).
47 Intros until 1; XElim H; Intros.
52 EApply pr3_pr2_pr2_t; [ Apply H2 | Apply H ].
58 (*#* #caption "reduction inside context items" *)
59 (*#* #cap #cap t1, t2 #alpha c in E, u1 in V1, u2 in V2, k in z *)
61 Theorem pr3_pr3_pr3_t : (c:?; u1,u2:?) (pr3 c u1 u2) ->
62 (t1,t2:?; k:?) (pr3 (CTail c k u2) t1 t2) ->
63 (pr3 (CTail c k u1) t1 t2).
67 Intros until 1; XElim H; Intros.
71 EApply pr3_pr2_pr3_t; [ Apply H1; XAuto | XAuto ].
76 Tactic Definition Pr3Context :=
78 | [ H1: (pr0 ?2 ?3); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
79 LApply (pr3_pr0_pr2_t ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
80 LApply (H1 ?1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
81 | [ H1: (pr0 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
82 LApply (pr3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
83 LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
84 | [ H1: (pr2 ?1 ?2 ?3); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
85 LApply (pr3_pr2_pr2_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
86 LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
87 | [ H1: (pr2 ?1 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
88 LApply (pr3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
89 LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
90 | [ H1: (pr3 ?1 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
91 LApply (pr3_pr3_pr3_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
92 LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ].
94 Section pr3_lift. (*******************************************************)
98 (*#* #caption "conguence with lift" *)
99 (*#* #cap #cap c, t1, t2 #alpha e in D, d in i *)
101 Theorem pr3_lift : (c,e:?; h,d:?) (drop h d c e) ->
102 (t1,t2:?) (pr3 e t1 t2) ->
103 (pr3 c (lift h d t1) (lift h d t2)).
107 Intros until 2; XElim H0; Intros; XEAuto.
112 Hints Resolve pr3_lift : ltlc.