1 Require Export pr1_defs.
2 Require Export pr2_defs.
4 (*#* #caption "axioms for the relation $\\PrT{}{}{}$",
5 "reflexivity", "single step transitivity"
7 (*#* #cap #cap c, t, t1, t2, t3 *)
9 Inductive pr3 [c:C] : T -> T -> Prop :=
10 | pr3_refl: (t:?) (pr3 c t t)
11 | pr3_sing: (t2,t1:?) (pr2 c t1 t2) ->
12 (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3).
16 Hint pr3: ltlc := Constructors pr3.
18 Section pr3_gen_base. (***************************************************)
20 Theorem pr3_gen_sort: (c:?; x:?; n:?) (pr3 c (TSort n) x) ->
22 Intros; InsertEq H '(TSort n); XElim H; Clear y x; Intros.
23 (* case 1: pr3_refl *)
25 (* case 2: pr3_sing *)
26 Rewrite H2 in H; Clear H2 t1; Pr2GenBase; XAuto.
29 Tactic Definition IH :=
31 | [ H: (u,t:T) (TTail (Bind Abst) ?1 ?2) = (TTail (Bind Abst) u t) -> ? |- ? ] ->
32 LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
34 | [ H: (u,t:T) (TTail (Flat Appl) ?1 ?2) = (TTail (Flat Appl) u t) -> ? |- ? ] ->
35 LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
37 | [ H: (u,t:T) (TTail (Flat Cast) ?1 ?2) = (TTail (Flat Cast) u t) -> ? |- ? ] ->
38 LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
41 Theorem pr3_gen_abst: (c:?; u1,t1,x:?)
42 (pr3 c (TTail (Bind Abst) u1 t1) x) ->
43 (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
44 (pr3 c u1 u2) & (b:?; u:?)
45 (pr3 (CTail c (Bind b) u) t1 t2)
47 Intros until 1; InsertEq H '(TTail (Bind Abst) u1 t1);
48 UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros;
49 Rename x into u0; Rename x0 into t0.
50 (* case 1 : pr3_refl *)
52 (* case 2 : pr3_sing *)
53 Rewrite H2 in H; Clear H0 H2 t1; Pr2GenBase.
54 Rewrite H0 in H1; Clear H0 t2; IH; XEAuto.
57 Theorem pr3_gen_appl: (c:?; u1,t1,x:?)
58 (pr3 c (TTail (Flat Appl) u1 t1) x) -> (OR
59 (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
60 (pr3 c u1 u2) & (pr3 c t1 t2)
62 (EX y1 z1 u2 t2 | (pr3 c (TTail (Bind Abbr) u2 t2) x) &
64 (pr3 c t1 (TTail (Bind Abst) y1 z1)) &
65 (b:?; u:?) (pr3 (CTail c (Bind b) u) z1 t2)
67 (EX b y1 z1 z2 u2 v2 t2 |
68 (pr3 c (TTail (Bind b) v2 z2) x) & ~b=Abst &
70 (pr3 c t1 (TTail (Bind b) y1 z1)) &
71 (pr3 c y1 v2) & (pr0 z1 t2))
73 Intros; InsertEq H '(TTail (Flat Appl) u1 t1).
74 UnIntro t1 H; UnIntro u1 H.
75 XElim H; Clear y x; Intros;
76 Rename x into u0; Rename x0 into t0.
77 (* case 1: pr3_refl *)
79 (* case 2: pr3_sing *)
80 Rewrite H2 in H; Clear H2 t1; Pr2GenBase.
81 (* case 2.1: short step: compatibility *)
82 Rewrite H3 in H1; Clear H0 H3 t2.
83 IH; Try (Rewrite H0; Clear H0 t3); XDEAuto 6.
84 (* case 2.2: short step: beta *)
85 Rewrite H4 in H0; Rewrite H3; Clear H1 H3 H4 t0 t2; XEAuto.
86 (* case 2.3: short step: upsilon *)
87 Rewrite H5 in H0; Rewrite H4; Clear H1 H4 H5 t0 t2; XEAuto.
90 Theorem pr3_gen_cast: (c:?; u1,t1,x:?)
91 (pr3 c (TTail (Flat Cast) u1 t1) x) ->
92 (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) &
93 (pr3 c u1 u2) & (pr3 c t1 t2)
96 Intros; InsertEq H '(TTail (Flat Cast) u1 t1);
97 UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros;
98 Rename x into u0; Rename x0 into t0.
99 (* case 1: pr3_refl *)
100 Rewrite H; Clear H t; XEAuto.
101 (* case 2: pr3_sing *)
102 Rewrite H2 in H; Clear H2 t1; Pr2GenBase.
103 (* case 2.1: short step: compatinility *)
104 Rewrite H3 in H1; Clear H0 H3 t2;
105 IH; Try Rewrite H0; XEAuto.
106 (* case 2.2: short step: epsilon *)
112 Tactic Definition Pr3GenBase :=
114 | [ H: (pr3 ?1 (TSort ?2) ?3) |- ? ] ->
115 LApply (pr3_gen_sort ?1 ?3 ?2); [ Clear H; Intros | XAuto ]
116 | [ H: (pr3 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] ->
117 LApply (pr3_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
119 | [ H: (pr3 ?1 (TTail (Flat Appl) ?2 ?3) ?4) |- ? ] ->
120 LApply (pr3_gen_appl ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
122 | [ H: (pr3 ?1 (TTail (Flat Cast) ?2 ?3) ?4) |- ? ] ->
123 LApply (pr3_gen_cast ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
126 Section pr3_props. (******************************************************)
128 Theorem pr3_pr2: (c,t1,t2:?) (pr2 c t1 t2) -> (pr3 c t1 t2).
132 Theorem pr3_t: (t2,t1,c:?) (pr3 c t1 t2) ->
133 (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3).
134 Intros until 1; XElim H; XEAuto.
137 Theorem pr3_thin_dx: (c:?; t1,t2:?) (pr3 c t1 t2) ->
138 (u:?; f:?) (pr3 c (TTail (Flat f) u t1)
139 (TTail (Flat f) u t2)).
140 Intros; XElim H; XEAuto.
143 Theorem pr3_tail_1: (c:?; u1,u2:?) (pr3 c u1 u2) ->
144 (k:?; t:?) (pr3 c (TTail k u1 t) (TTail k u2 t)).
145 Intros until 1; XElim H; Intros.
146 (* case 1: pr3_refl *)
148 (* case 2: pr3_sing *)
149 EApply pr3_sing; [ Apply pr2_tail_1; Apply H | XAuto ].
152 Theorem pr3_tail_2: (c:?; u,t1,t2:?; k:?) (pr3 (CTail c k u) t1 t2) ->
153 (pr3 c (TTail k u t1) (TTail k u t2)).
154 Intros until 1; XElim H; Intros.
155 (* case 1: pr3_refl *)
157 (* case 2: pr3_sing *)
158 EApply pr3_sing; [ Apply pr2_tail_2; Apply H | XAuto ].
161 Hints Resolve pr3_tail_1 pr3_tail_2 : ltlc.
163 Theorem pr3_tail_21: (c:?; u1,u2:?) (pr3 c u1 u2) ->
164 (k:?; t1,t2:?) (pr3 (CTail c k u1) t1 t2) ->
165 (pr3 c (TTail k u1 t1) (TTail k u2 t2)).
167 EApply pr3_t; [ Apply pr3_tail_2 | Apply pr3_tail_1 ]; XAuto.
170 Theorem pr3_tail_12: (c:?; u1,u2:?) (pr3 c u1 u2) ->
171 (k:?; t1,t2:?) (pr3 (CTail c k u2) t1 t2) ->
172 (pr3 c (TTail k u1 t1) (TTail k u2 t2)).
174 EApply pr3_t; [ Apply pr3_tail_1 | Apply pr3_tail_2 ]; XAuto.
177 Theorem pr3_shift: (h:?; c,e:?) (drop h (0) c e) ->
178 (t1,t2:?) (pr3 c t1 t2) ->
179 (pr3 e (app c h t1) (app c h t2)).
180 Intros until 2; XElim H0; Clear t1 t2; Intros.
181 (* case 1: pr3_refl *)
183 (* case 2: pr3_sing *)
187 Theorem pr3_pr1: (t1,t2:?) (pr1 t1 t2) -> (c:?) (pr3 c t1 t2).
188 Intros until 1; XElim H; XEAuto.
193 Hints Resolve pr3_pr2 pr3_t pr3_pr1
194 pr3_thin_dx pr3_tail_12 pr3_tail_21 pr3_shift : ltlc.