1 (* This file contains the definition of the alphabet for the mono-tape machine
2 simulating a multi-tape machine, and a library of functions operating on them *)
4 include "basics/vector_finset.ma".
6 (* a multi_sig characheter is composed by n+1 sub-characters: n for each tape
7 of a multitape machine.
8 We extend the tape alphabet with a special symbol None to pad shorter tapes.
9 For the moment, the actual content of the tape alphabet is left unspecifed,
10 but we shall need characters to store states and moves of the multitape
11 machines and to mark the head position *)
13 definition sig_ext ≝ λsig. FinOption sig.
14 definition blank : ∀sig.sig_ext sig ≝ λsig. None sig.
16 (* definition head : ∀sig.sig_ext sig ≝ λsig. inl … true. *)
18 definition multi_sig ≝ λsig:FinSet.λn.FinVector (sig_ext sig) n.
20 (* a character containing blank characters in each trace *)
21 let rec all_blanks sig n on n : multi_sig sig n ≝
23 [ O ⇒ Vector_of_list ? []
24 | S m ⇒ vec_cons ? (blank ?) m (all_blanks sig m)
27 lemma blank_all_blanks: ∀sig,n,i.
28 nth i ? (vec … (all_blanks sig n)) (blank sig) = blank ?.
29 #sig #n elim n normalize [#i >nth_nil // |#m #Hind #i cases i // #j @Hind ]
32 lemma all_blank_n: ∀sig,n.
33 nth n ? (vec … (all_blanks sig n)) (blank sig) = blank ?.
34 #sig #n @blank_all_blanks
37 (* boolen test functions *)
39 definition not_blank ≝ λsig,n,i.λc:multi_sig sig n.
40 ¬(nth i ? (vec … c) (blank ?))==blank ?.
43 definition no_head ≝ λsig,n.λc:multi_sig sig n.
44 ¬((nth n ? (vec … c) (blank ?))==head ?).
46 lemma no_head_true: ∀sig,n,a.
47 nth n ? (vec … n a) (blank sig) ≠ head ? → no_head … a = true.
48 #sig #n #a normalize cases (nth n ? (vec … n a) (blank sig))
49 normalize // * normalize // * #H @False_ind @H //
52 lemma no_head_false: ∀sig,n,a.
53 nth n ? (vec … n a) (blank sig) = head ? → no_head … a = false.
54 #sig #n #a #H normalize >H //
57 (**************************** extract the i-th trace **************************)
58 definition trace ≝ λsig,n,i,l.
59 map ?? (λa. nth i ? (vec … n a) (blank sig)) l.
61 lemma trace_def : ∀sig,n,i,l.
62 trace sig n i l = map ?? (λa. nth i ? (vec … n a) (blank sig)) l.
65 lemma hd_trace: ∀sig,n,i,l.
66 hd ? (trace sig n i l) (blank ?) =
67 nth i ? (hd ? l (all_blanks … )) (blank ?).
68 #sig #n #i #l elim l // normalize >blank_all_blanks %
71 lemma tail_trace: ∀sig,n,i,l.
72 tail ? (trace sig n i l) = trace sig n i (tail ? l).
73 #sig #n #i #l elim l //
76 lemma trace_append : ∀sig,n,i,l1,l2.
77 trace sig n i (l1 @ l2) = trace sig n i l1 @ trace sig n i l2.
78 #sig #n #i #l1 #l2 elim l1 // #a #tl #Hind normalize >Hind //
81 lemma trace_reverse : ∀sig,n,i,l.
82 trace sig n i (reverse ? l) = reverse (sig_ext sig) (trace sig n i l).
83 #sig #n #i #l elim l //
84 #a #tl #Hind whd in match (trace ??? (a::tl)); >reverse_cons >reverse_cons
85 >trace_append >Hind //
88 lemma length_trace: ∀sig,n,i,l.
89 |trace sig n i l| = |l|.
90 #sig #n #i #l elim l // #a #tl #Hind normalize @eq_f @Hind
93 lemma nth_trace : ∀sig,n,i,j,l.
94 nth j ? (trace sig n i l) (blank ?) =
95 nth i ? (nth j ? l (all_blanks sig n)) (blank ?).
97 [#l cases l normalize // >blank_all_blanks //
98 |-j #j #Hind #l whd in match (nth ????); whd in match (nth ????);
100 [normalize >nth_nil >nth_nil >blank_all_blanks //
101 |#a #tl normalize @Hind]
106 definition no_head_in ≝ λsig,n,l.
107 ∀x. mem ? x (trace sig n n l) → x ≠ head ?.
110 (* some lemmas over lists, to be moved *)
111 lemma injective_append_l: ∀A,l. injective ?? (append A l).
113 [#l1 #l2 normalize //
114 |#a #tl #Hind #l1 #l2 normalize #H @Hind @(cons_injective_r … H)
118 lemma injective_append_r: ∀A,l. injective ?? (λl1.append A l1 l).
120 cut (reverse ? (l1@l) = reverse ? (l2@l)) [//]
121 >reverse_append >reverse_append #Hrev
122 lapply (injective_append_l … Hrev) -Hrev #Hrev
123 <(reverse_reverse … l1) <(reverse_reverse … l2) //
126 lemma reverse_map: ∀A,B,f,l.
127 reverse B (map … f l) = map … f (reverse A l).
128 #A #B #f #l elim l //
129 #a #l #Hind >reverse_cons >reverse_cons <map_append >Hind //
132 lemma injective_reverse: ∀A. injective ?? (reverse A).
133 #A #l1 #l2 #H <(reverse_reverse … l1) <(reverse_reverse … l2) //
136 lemma first_P_to_eq : ∀A:Type[0].∀P:A→Prop.∀l1,l2,l3,l4,a1,a2.
137 l1@a1::l2 = l3@a2::l4 → (∀x. mem A x l1 → P x) → (∀x. mem A x l2 → P x) →
138 ¬ P a1 → ¬ P a2 → l1 = l3 ∧ a1::l2 = a2::l4.
141 [#l4 #a1 #a2 normalize #H destruct /2/
142 |#c #tl #l4 #a1 #a2 normalize #H destruct
143 #_ #H #_ #H1 @False_ind @(absurd ?? H1) @H @mem_append_l2 %1 //
146 [#l4 #a1 #a2 normalize #H destruct
147 #H1 #_ #_ #H2 @False_ind @(absurd ?? H2) @H1 %1 //
148 |#c #tl2 #l4 #a1 #a2 normalize #H1 #H2 #H3 #H4 #H5
149 lapply (Hind l2 tl2 l4 … H4 H5)
150 [destruct @H3 |#x #H6 @H2 %2 // | destruct (H1) //
151 |* #H6 #H7 % // >H7 in H1; #H1 @(injective_append_r … (a2::l4)) @H1
156 lemma nth_to_eq: ∀A,l1,l2,a. |l1| = |l2| →
157 (∀i. nth i A l1 a = nth i A l2 a) → l1 = l2.
159 [* // #a #tl #d normalize #H destruct (H)
161 [#d normalize #H destruct (H)
162 |#b #tl1 #d #Hlen #Hnth @eq_f2
163 [@(Hnth 0) | @(Hind tl1 d) [@injective_S @Hlen | #i @(Hnth (S i)) ]]
168 lemma nth_extended: ∀A,i,l,a.
169 nth i A l a = nth i A (l@[a]) a.
170 #A #i elim i [* // |#j #Hind * // #b #tl #a normalize @Hind]
173 (******************************* shifting a trace *****************************)
175 (* (shift_i sig n i a b) replace the i-th trace of the character a with the
178 definition shift_i ≝ λsig,n,i.λa,b:Vector (sig_ext sig) n.
179 change_vec (sig_ext sig) n a (nth i ? b (blank ?)) i.
181 (* given two strings v1 and v2 of the mono-tape machine, (shift_l … i v1 v2)
182 asserts that v1 is obtained from v2 by shifting_left the i-trace *)
184 definition shift_l ≝ λsig,n,i,v1,v2. (* multi_sig sig n *)
186 ∀j.nth j ? v2 (all_blanks sig n) =
187 change_vec ? n (nth j ? v1 (all_blanks sig n))
188 (nth i ? (vec … (nth (S j) ? v1 (all_blanks sig n))) (blank ?)) i.
190 (* supposing (shift_l … i v1 v2), the i-th trace of v2 is equal to the tail of
191 the i-th trace of v1, plus a trailing blank *)
193 lemma trace_shift: ∀sig,n,i,v1,v2. i < n → 0 < |v1| →
194 shift_l sig n i v1 v2 → trace ? n i v2 = tail ? (trace ? n i v1)@[blank sig].
195 #sig #n #i #v1 #v2 #lein #Hlen * #Hlen1 #Hnth @(nth_to_eq … (blank ?))
196 [>length_trace <Hlen1 generalize in match Hlen; cases v1
197 [normalize #H @(le_n_O_elim … H) //
198 |#b #tl #_ normalize >length_append >length_trace normalize //
200 |#j >nth_trace >Hnth >nth_change_vec // >tail_trace
201 cut (trace ? n i [all_blanks sig n] = [blank sig])
202 [normalize >blank_all_blanks //]
203 #Hcut <Hcut <trace_append >nth_trace
208 (* supposing (shift_l … i v1 v2), and j≠i, the j-th trace of v2 is equal to the
211 lemma trace_shift_neq: ∀sig,n,i,j,v1,v2. i < n → 0 < |v1| → i ≠ j →
212 shift_l sig n i v1 v2 → trace ? n j v2 = trace ? n j v1.
213 #sig #n #i #j #v1 #v2 #lein #Hlen #Hneq * #Hlen1 #Hnth @(nth_to_eq … (blank ?))
214 [>length_trace >length_trace @sym_eq @Hlen1
215 |#k >nth_trace >Hnth >nth_change_vec_neq // >nth_trace //
219 (******************************************************************************)
221 let rec to_blank sig l on l ≝
225 if a == blank sig then [ ] else a::(to_blank sig tl)].
227 let rec after_blank sig l on l ≝
231 if a == blank sig then (a::tl) else (after_blank sig tl)].
233 definition to_blank_i ≝ λsig,n,i,l. to_blank ? (trace sig n i l).
235 lemma to_blank_i_def : ∀sig,n,i,l.
236 to_blank_i sig n i l = to_blank ? (trace sig n i l).
239 lemma to_blank_cons_b : ∀sig,n,i,a,l.
240 nth i ? (vec … n a) (blank sig) = blank ? →
241 to_blank_i sig n i (a::l) = [ ].
242 #sig #n #i #a #l #H whd in match (to_blank_i ????);
246 lemma to_blank_cons_nb: ∀sig,n,i,a,l.
247 nth i ? (vec … n a) (blank sig) ≠ blank ? →
248 to_blank_i sig n i (a::l) =
249 nth i ? (vec … n a) (blank sig)::(to_blank_i sig n i l).
250 #sig #n #i #a #l #H whd in match (to_blank_i ????);
254 axiom to_blank_hd : ∀sig,n,a,b,l1,l2.
255 (∀i. i < n → to_blank_i sig n i (a::l1) = to_blank_i sig n i (b::l2)) → a = b.
257 lemma to_blank_i_ext : ∀sig,n,i,l.
258 to_blank_i sig n i l = to_blank_i sig n i (l@[all_blanks …]).
260 [@sym_eq @to_blank_cons_b @blank_all_blanks
261 |#a #tl #Hind whd in match (to_blank_i ????); >Hind <to_blank_i_def >Hind %
265 lemma to_blank_hd_cons : ∀sig,n,i,l1,l2.
266 to_blank_i sig n i (l1@l2) =
267 to_blank_i … i (l1@(hd … l2 (all_blanks …))::tail … l2).
268 #sig #n #i #l1 #l2 cases l2
269 [whd in match (hd ???); whd in match (tail ??); >append_nil @to_blank_i_ext
274 lemma to_blank_i_chop : ∀sig,n,i,a,l1,l2.
275 (nth i ? (vec … a) (blank ?))= blank ? →
276 to_blank_i sig n i (l1@a::l2) = to_blank_i sig n i l1.
277 #sig #n #i #a #l1 elim l1
278 [#l2 #H @to_blank_cons_b //
279 |#x #tl #Hind #l2 #H whd in match (to_blank_i ????);
280 >(Hind l2 H) <to_blank_i_def >(Hind l2 H) %