3 Require Export terms_defs.
5 Fixpoint lref_map [g:nat->nat; d:nat; t:T] : T := Cases t of
6 | (TSort n) => (TSort n)
8 if (blt n d) then (TLRef n) else (TLRef (g n))
10 (TTail k (lref_map g d u) (lref_map g (s k d) t))
13 Definition lift : nat -> nat -> T -> T :=
14 [h](lref_map [x](plus x h)).
16 Section lift_rw. (********************************************************)
18 Theorem lift_sort: (n:?; h,d:?) (lift h d (TSort n)) = (TSort n).
22 Theorem lift_lref_lt: (n:?; h,d:?) (lt n d) ->
23 (lift h d (TLRef n)) = (TLRef n).
24 Intros; Unfold lift; Simpl.
25 Replace (blt n d) with true; XAuto.
28 Theorem lift_lref_ge: (n:?; h,d:?) (le d n) ->
29 (lift h d (TLRef n)) = (TLRef (plus n h)).
31 Intros; Unfold lift; Simpl.
32 Replace (blt n d) with false; XAuto.
35 Theorem lift_tail: (k:?; u,t:?; h,d:?)
36 (lift h d (TTail k u t)) =
37 (TTail k (lift h d u) (lift h (s k d) t)).
41 Theorem lift_bind: (b:?; u,t:?; h,d:?)
42 (lift h d (TTail (Bind b) u t)) =
43 (TTail (Bind b) (lift h d u) (lift h (S d) t)).
47 Theorem lift_flat: (f:?; u,t:?; h,d:?)
48 (lift h d (TTail (Flat f) u t)) =
49 (TTail (Flat f) (lift h d u) (lift h d t)).
55 Hints Resolve lift_lref_lt lift_bind lift_flat : ltlc.
57 Tactic Definition LiftTailRw :=
58 Repeat (Rewrite lift_tail Orelse Rewrite lift_bind Orelse Rewrite lift_flat).
60 Tactic Definition LiftTailRwBack :=
61 Repeat (Rewrite <- lift_tail Orelse Rewrite <- lift_bind Orelse Rewrite <- lift_flat).
63 Section lift_gen. (*******************************************************)
65 Theorem lift_gen_sort: (h,d,n:?; t:?) (TSort n) = (lift h d t) ->
70 (* case 2 : TLRef n0 *)
71 Apply (lt_le_e n0 d); Intros.
72 (* case 2.1 : n0 < d *)
73 Rewrite lift_lref_lt in H; [ Inversion H | XAuto ].
74 (* case 2.2 : n0 >= d *)
75 Rewrite lift_lref_ge in H; [ Inversion H | XAuto ].
76 (* case 3 : TTail k *)
77 Rewrite lift_tail in H1; Inversion H1.
80 Theorem lift_gen_lref_lt: (h,d,n:?) (lt n d) ->
81 (t:?) (TLRef n) = (lift h d t) ->
86 (* case 2 : TLRef n0 *)
87 Apply (lt_le_e n0 d); Intros.
88 (* case 2.1 : n0 < d *)
89 Rewrite lift_lref_lt in H0; XAuto.
90 (* case 2.2 : n0 >= d *)
91 Rewrite lift_lref_ge in H0; [ Inversion H0; Clear H0 | XAuto ].
92 Rewrite H3 in H; Clear H3 n.
93 EApply le_false; [ Apply H1 | XEAuto ].
94 (* case 3 : TTail k *)
95 Rewrite lift_tail in H2; Inversion H2.
98 Theorem lift_gen_lref_false: (h,d,n:?) (le d n) -> (lt n (plus d h)) ->
99 (t:?) (TLRef n) = (lift h d t) ->
104 (* case 2 : TLRef n0 *)
105 Apply (lt_le_e n0 d); Intros.
106 (* case 2.1 : n0 < d *)
107 Rewrite lift_lref_lt in H1; [ Inversion H1; Clear H1 | XAuto ].
108 Rewrite <- H4 in H2; Clear H4 n0.
109 EApply le_false; [ Apply H | XEAuto ].
110 (* case 2.2 : n0 >= d *)
111 Rewrite lift_lref_ge in H1; [ Inversion H1; Clear H1 | XAuto ].
112 Rewrite H4 in H0; Clear H4.
113 EApply le_false; [ Apply H2 | XEAuto ].
114 (* case 3 : TTail k *)
115 Rewrite lift_tail in H3; Inversion H3.
118 Theorem lift_gen_lref_ge: (h,d,n:?) (le d n) ->
119 (t:?) (TLRef (plus n h)) = (lift h d t) ->
124 (* case 2 : TLRef n0 *)
125 Apply (lt_le_e n0 d); Intros.
126 (* case 2.1 : n0 < d *)
127 Rewrite lift_lref_lt in H0; [ Inversion H0; Clear H0 | XAuto ].
128 Rewrite <- H3 in H1; Clear H3 n0.
129 EApply le_false; [ Apply H | XEAuto ].
130 (* case 2.2 : n0 >= d *)
131 Rewrite lift_lref_ge in H0; [ Inversion H0; XEAuto | XAuto ].
132 (* case 3 : TTail k *)
133 Rewrite lift_tail in H2; Inversion H2.
136 (* NOTE: lift_gen_tail should be used instead of these two *) (**)
137 Theorem lift_gen_bind: (b:?; u,t,x:?; h,d:?)
138 (TTail (Bind b) u t) = (lift h d x) ->
139 (EX y z | x = (TTail (Bind b) y z) &
146 (* case 2 : TLRef n *)
147 Apply (lt_le_e n d); Intros.
148 (* case 2.1 : n < d *)
149 Rewrite lift_lref_lt in H; [ Inversion H | XAuto ].
150 (* case 2.2 : n >= d *)
151 Rewrite lift_lref_ge in H; [ Inversion H | XAuto ].
152 (* case 3 : TTail k *)
153 Rewrite lift_tail in H1; Inversion H1.
157 Theorem lift_gen_flat: (f:?; u,t,x:?; h,d:?)
158 (TTail (Flat f) u t) = (lift h d x) ->
159 (EX y z | x = (TTail (Flat f) y z) &
166 (* case 2 : TLRef n *)
167 Apply (lt_le_e n d); Intros.
168 (* case 2.1 : n < d *)
169 Rewrite lift_lref_lt in H; [ Inversion H | XAuto ].
170 (* case 2.2 : n >= d *)
171 Rewrite lift_lref_ge in H; [ Inversion H | XAuto ].
172 (* case 3 : TTail k *)
173 Rewrite lift_tail in H1; Inversion H1.
179 Tactic Definition LiftGenBase :=
181 | [ H: (TSort ?0) = (lift ?1 ?2 ?3) |- ? ] ->
182 LApply (lift_gen_sort ?1 ?2 ?0 ?3); [ Clear H; Intros | XAuto ]
183 | [ H1: (le ?1 ?2); H2: (lt ?2 (plus ?1 ?3));
184 H3: (TLRef ?2) = (lift ?3 ?1 ?4) |- ? ] ->
185 Apply (lift_gen_lref_false ?3 ?1 ?2 H1 H2 ?4 H3); XAuto
186 | [ _: (TLRef ?1) = (lift (S ?1) (0) ?2) |- ? ] ->
187 EApply lift_gen_lref_false; [ Idtac | Idtac | XEAuto ]; XEAuto
188 | [ H: (TLRef ?1) = (lift (1) ?1 ?2) |- ? ] ->
189 LApply (lift_gen_lref_false (1) ?1 ?1); [ Intros H_x | XAuto ];
190 LApply H_x; [ Clear H_x; Intros H_x | Arith7' ?1; XAuto ];
191 LApply (H_x ?2); [ Clear H_x; Intros H_x | XAuto ];
193 | [ H: (TLRef (plus ?0 ?1)) = (lift ?1 ?2 ?3) |- ? ] ->
194 LApply (lift_gen_lref_ge ?1 ?2 ?0); [ Intros H_x | XAuto ];
195 LApply (H_x ?3); [ Clear H_x H; Intros | XAuto ]
196 | [ H1: (TLRef ?0) = (lift ?1 ?2 ?3); H2: (lt ?0 ?4) |- ? ] ->
197 LApply (lift_gen_lref_lt ?1 ?2 ?0);
198 [ Intros H_x | Apply lt_le_trans with m:=?4; XEAuto ];
199 LApply (H_x ?3); [ Clear H_x H1; Intros | XAuto ]
200 | [ H: (TLRef ?0) = (lift ?1 ?2 ?3) |- ? ] ->
201 LApply (lift_gen_lref_lt ?1 ?2 ?0); [ Intros H_x | XEAuto ];
202 LApply (H_x ?3); [ Clear H_x H; Intros | XAuto ]
203 | [ H: (TTail (Bind ?0) ?1 ?2) = (lift ?3 ?4 ?5) |- ? ] ->
204 LApply (lift_gen_bind ?0 ?1 ?2 ?5 ?3 ?4); [ Clear H; Intros H | XAuto ];
206 | [ H: (TTail (Flat ?0) ?1 ?2) = (lift ?3 ?4 ?5) |- ? ] ->
207 LApply (lift_gen_flat ?0 ?1 ?2 ?5 ?3 ?4); [ Clear H; Intros H | XAuto ];
210 Section lift_props. (*****************************************************)
212 Theorem lift_r: (t:?; d:?) (lift (0) d t) = t.
216 (* case 2: TLRef n *)
217 Apply (lt_le_e n d); Intros.
218 (* case 2.1: n < d *)
219 Rewrite lift_lref_lt; XAuto.
220 (* case 2.2: n >= d *)
221 Rewrite lift_lref_ge; XAuto.
226 Theorem lift_lref_gt : (d,n:?) (lt d n) ->
227 (lift (1) d (TLRef (pred n))) = (TLRef n).
229 Rewrite lift_lref_ge.
230 (* case 1: first branch *)
231 Rewrite <- plus_sym; Simpl; Rewrite <- (S_pred n d); XAuto.
232 (* case 2: second branch *)
233 Apply le_S_n; Rewrite <- (S_pred n d); XAuto.
238 Hints Resolve lift_r lift_lref_gt : ltlc.