1 Require Export drop_defs.
2 Require Export pr0_defs.
4 (*#* #caption "current axioms for the relation $\\PrS{}{}{}$",
5 "context-free case", "context-dependent $\\delta$-expansion"
7 (*#* #cap #cap c, d, t, t1, t2 #alpha u in V *)
9 Inductive pr2 [c:C; t1:T] : T -> Prop :=
10 (* structural rules *)
11 | pr2_free : (t2:?) (pr0 t1 t2) -> (pr2 c t1 t2)
13 | pr2_delta: (d:?; u:?; i:?)
14 (drop i (0) c (CTail d (Bind Abbr) u)) ->
15 (t2:?) (pr0 t1 t2) -> (t:?) (subst0 i u t2 t) ->
20 Hint pr2 : ltlc := Constructors pr2.
22 Section pr2_gen_base. (***************************************************)
24 Theorem pr2_gen_sort: (c:?; x:?; n:?) (pr2 c (TSort n) x) ->
26 Intros; Inversion H; Pr0GenBase;
27 [ XAuto | Rewrite H1 in H2; Subst0GenBase ].
30 Theorem pr2_gen_lref: (c:?; x:?; n:?) (pr2 c (TLRef n) x) ->
32 (EX d u | (drop n (0) c (CTail d (Bind Abbr) u)) &
33 x = (lift (S n) (0) u)
35 Intros; Inversion H; Pr0GenBase;
36 [ XAuto | Rewrite H1 in H2; Subst0GenBase; Rewrite <- H2 in H0; XEAuto ].
39 Theorem pr2_gen_abst: (c:?; u1,t1,x:?)
40 (pr2 c (TTail (Bind Abst) u1 t1) x) ->
41 (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
42 (pr2 c u1 u2) & (b:?; u:?)
43 (pr2 (CTail c (Bind b) u) t1 t2)
45 Intros; Inversion H; Pr0GenBase;
46 [ XEAuto | Rewrite H1 in H2; Subst0GenBase; XDEAuto 6 ].
49 Theorem pr2_gen_appl: (c:?; u1,t1,x:?)
50 (pr2 c (TTail (Flat Appl) u1 t1) x) -> (OR
51 (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
52 (pr2 c u1 u2) & (pr2 c t1 t2)
54 (EX y1 z1 u2 t2 | t1 = (TTail (Bind Abst) y1 z1) &
55 x = (TTail (Bind Abbr) u2 t2) &
56 (pr2 c u1 u2) & (b:?; u:?)
57 (pr2 (CTail c (Bind b) u) z1 t2)
59 (EX b y1 z1 z2 u2 v2 t2 |
61 t1 = (TTail (Bind b) y1 z1) &
62 x = (TTail (Bind b) v2 z2) &
63 (pr2 c u1 u2) & (pr2 c y1 v2) & (pr0 z1 t2))
65 Intros; Inversion H; Pr0GenBase;
66 Try Rewrite H1 in H2; Try Rewrite H4 in H2; Try Rewrite H5 in H2;
67 Try Subst0GenBase; XDEAuto 7.
70 Theorem pr2_gen_cast: (c:?; u1,t1,x:?)
71 (pr2 c (TTail (Flat Cast) u1 t1) x) ->
72 (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) &
73 (pr2 c u1 u2) & (pr2 c t1 t2)
76 Intros; Inversion H; Pr0GenBase;
77 Try Rewrite H1 in H2; Try Subst0GenBase; XEAuto.
82 Tactic Definition Pr2GenBase :=
84 | [ H: (pr2 ?1 (TSort ?2) ?3) |- ? ] ->
85 LApply (pr2_gen_sort ?1 ?3 ?2); [ Clear H; Intros | XAuto ]
86 | [ H: (pr2 ?1 (TLRef ?2) ?3) |- ? ] ->
87 LApply (pr2_gen_lref ?1 ?3 ?2); [ Clear H; Intros H | XAuto ];
89 | [ H: (pr2 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] ->
90 LApply (pr2_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
92 | [ H: (pr2 ?1 (TTail (Flat Appl) ?2 ?3) ?4) |- ? ] ->
93 LApply (pr2_gen_appl ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
95 | [ H: (pr2 ?1 (TTail (Flat Cast) ?2 ?3) ?4) |- ? ] ->
96 LApply (pr2_gen_cast ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
99 Section pr2_props. (******************************************************)
101 Theorem pr2_thin_dx: (c:?; t1,t2:?) (pr2 c t1 t2) ->
102 (u:?; f:?) (pr2 c (TTail (Flat f) u t1)
103 (TTail (Flat f) u t2)).
104 Intros; XElim H; XEAuto.
107 Theorem pr2_tail_1: (c:?; u1,u2:?) (pr2 c u1 u2) ->
108 (k:?; t:?) (pr2 c (TTail k u1 t) (TTail k u2 t)).
109 Intros; XElim H; XEAuto.
112 Theorem pr2_tail_2: (c:?; u,t1,t2:?; k:?) (pr2 (CTail c k u) t1 t2) ->
113 (pr2 c (TTail k u t1) (TTail k u t2)).
115 XElim H; [ XAuto | XElim i; Intros; DropGenBase; CGenBase; XEAuto ]).
118 Hints Resolve pr2_tail_2 : ltlc.
120 Theorem pr2_shift: (i:?; c,e:?) (drop i (0) c e) ->
121 (t1,t2:?) (pr2 c t1 t2) ->
122 (pr2 e (app c i t1) (app c i t2)).
125 Intros; DropGenBase; Rewrite H in H0.
126 Repeat Rewrite app_O; XAuto.
129 (* case 2.1: CSort *)
130 Intros; DropGenBase; Rewrite H0; XAuto.
131 (* case 2.2: CTail *)
132 XElim k; Intros; Simpl; DropGenBase; XAuto.
137 Hints Resolve pr2_thin_dx pr2_tail_1 pr2_tail_2 pr2_shift : ltlc.