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, and an additional one to mark the position of the head.
8 We extend the tape alphabet with two new symbols true and false.
9 false is used to pad shorter tapes, and true to mark the head of the tape *)
11 definition sig_ext ≝ λsig. FinSum FinBool sig.
12 definition blank : ∀sig.sig_ext sig ≝ λsig. inl … false.
13 definition head : ∀sig.sig_ext sig ≝ λsig. inl … true.
15 definition multi_sig ≝ λsig:FinSet.λn.FinVector (sig_ext sig) n.
17 (* a character containing blank characters in each trace *)
18 let rec all_blank sig n on n : multi_sig sig n ≝
20 [ O ⇒ Vector_of_list ? []
21 | S m ⇒ vec_cons ? (blank ?) m (all_blank sig m)
24 lemma blank_all_blank: ∀sig,n,i.
25 nth i ? (vec … (all_blank sig n)) (blank sig) = blank ?.
26 #sig #n elim n normalize [#i >nth_nil // |#m #Hind #i cases i // #j @Hind ]
29 lemma all_blank_n: ∀sig,n.
30 nth n ? (vec … (all_blank sig n)) (blank sig) = blank ?.
31 #sig #n @blank_all_blank
34 (* boolen test functions *)
36 definition no_blank ≝ λsig,n,i.λc:multi_sig sig n.
37 ¬(nth i ? (vec … c) (blank ?))==blank ?.
39 definition no_head ≝ λsig,n.λc:multi_sig sig n.
40 ¬((nth n ? (vec … c) (blank ?))==head ?).
42 lemma no_head_true: ∀sig,n,a.
43 nth n ? (vec … n a) (blank sig) ≠ head ? → no_head … a = true.
44 #sig #n #a normalize cases (nth n ? (vec … n a) (blank sig))
45 normalize // * normalize // * #H @False_ind @H //
48 lemma no_head_false: ∀sig,n,a.
49 nth n ? (vec … n a) (blank sig) = head ? → no_head … a = false.
50 #sig #n #a #H normalize >H //
53 (**************************** extract the i-th trace **************************)
54 definition trace ≝ λsig,n,i,l.
55 map ?? (λa. nth i ? (vec … n a) (blank sig)) l.
57 lemma trace_def : ∀sig,n,i,l.
58 trace sig n i l = map ?? (λa. nth i ? (vec … n a) (blank sig)) l.
61 lemma hd_trace: ∀sig,n,i,l.
62 hd ? (trace sig n i l) (blank ?) =
63 nth i ? (hd ? l (all_blank … )) (blank ?).
64 #sig #n #i #l elim l // normalize >blank_all_blank %
67 lemma tail_trace: ∀sig,n,i,l.
68 tail ? (trace sig n i l) = trace sig n i (tail ? l).
69 #sig #n #i #l elim l //
72 lemma trace_append : ∀sig,n,i,l1,l2.
73 trace sig n i (l1 @ l2) = trace sig n i l1 @ trace sig n i l2.
74 #sig #n #i #l1 #l2 elim l1 // #a #tl #Hind normalize >Hind //
77 lemma trace_reverse : ∀sig,n,i,l.
78 trace sig n i (reverse ? l) = reverse (sig_ext sig) (trace sig n i l).
79 #sig #n #i #l elim l //
80 #a #tl #Hind whd in match (trace ??? (a::tl)); >reverse_cons >reverse_cons
81 >trace_append >Hind //
84 lemma length_trace: ∀sig,n,i,l.
85 |trace sig n i l| = |l|.
86 #sig #n #i #l elim l // #a #tl #Hind normalize @eq_f @Hind
89 lemma nth_trace : ∀sig,n,i,j,l.
90 nth j ? (trace sig n i l) (blank ?) =
91 nth i ? (nth j ? l (all_blank sig n)) (blank ?).
93 [#l cases l normalize // >blank_all_blank //
94 |-j #j #Hind #l whd in match (nth ????); whd in match (nth ????);
96 [normalize >nth_nil >nth_nil >blank_all_blank //
97 |#a #tl normalize @Hind]
101 definition no_head_in ≝ λsig,n,l.
102 ∀x. mem ? x (trace sig n n l) → x ≠ head ?.
105 (* some lemmas over lists, to be moved *)
106 lemma injective_append_l: ∀A,l. injective ?? (append A l).
108 [#l1 #l2 normalize //
109 |#a #tl #Hind #l1 #l2 normalize #H @Hind @(cons_injective_r … H)
113 lemma injective_append_r: ∀A,l. injective ?? (λl1.append A l1 l).
115 cut (reverse ? (l1@l) = reverse ? (l2@l)) [//]
116 >reverse_append >reverse_append #Hrev
117 lapply (injective_append_l … Hrev) -Hrev #Hrev
118 <(reverse_reverse … l1) <(reverse_reverse … l2) //
121 lemma reverse_map: ∀A,B,f,l.
122 reverse B (map … f l) = map … f (reverse A l).
123 #A #B #f #l elim l //
124 #a #l #Hind >reverse_cons >reverse_cons <map_append >Hind //
127 lemma injective_reverse: ∀A. injective ?? (reverse A).
128 #A #l1 #l2 #H <(reverse_reverse … l1) <(reverse_reverse … l2) //
131 lemma first_P_to_eq : ∀A:Type[0].∀P:A→Prop.∀l1,l2,l3,l4,a1,a2.
132 l1@a1::l2 = l3@a2::l4 → (∀x. mem A x l1 → P x) → (∀x. mem A x l2 → P x) →
133 ¬ P a1 → ¬ P a2 → l1 = l3 ∧ a1::l2 = a2::l4.
136 [#l4 #a1 #a2 normalize #H destruct /2/
137 |#c #tl #l4 #a1 #a2 normalize #H destruct
138 #_ #H #_ #H1 @False_ind @(absurd ?? H1) @H @mem_append_l2 %1 //
141 [#l4 #a1 #a2 normalize #H destruct
142 #H1 #_ #_ #H2 @False_ind @(absurd ?? H2) @H1 %1 //
143 |#c #tl2 #l4 #a1 #a2 normalize #H1 #H2 #H3 #H4 #H5
144 lapply (Hind l2 tl2 l4 … H4 H5)
145 [destruct @H3 |#x #H6 @H2 %2 // | destruct (H1) //
146 |* #H6 #H7 % // >H7 in H1; #H1 @(injective_append_r … (a2::l4)) @H1
151 lemma nth_to_eq: ∀A,l1,l2,a. |l1| = |l2| →
152 (∀i. nth i A l1 a = nth i A l2 a) → l1 = l2.
154 [* // #a #tl #d normalize #H destruct (H)
156 [#d normalize #H destruct (H)
157 |#b #tl1 #d #Hlen #Hnth @eq_f2
158 [@(Hnth 0) | @(Hind tl1 d) [@injective_S @Hlen | #i @(Hnth (S i)) ]]
163 lemma nth_extended: ∀A,i,l,a.
164 nth i A l a = nth i A (l@[a]) a.
165 #A #i elim i [* // |#j #Hind * // #b #tl #a normalize @Hind]
168 (******************************* shifting a trace *****************************)
170 (* (shift_i sig n i a b) replace the i-th trace of the character a with the
173 definition shift_i ≝ λsig,n,i.λa,b:Vector (sig_ext sig) n.
174 change_vec (sig_ext sig) n a (nth i ? b (blank ?)) i.
176 (* given two strings v1 and v2 of the mono-tape machine, (shift_l … i v1 v2)
177 asserts that v1 is obtained from v2 by shifting_left the i-trace *)
179 definition shift_l ≝ λsig,n,i,v1,v2. (* multi_sig sig n *)
181 ∀j.nth j ? v2 (all_blank sig n) =
182 change_vec ? n (nth j ? v1 (all_blank sig n))
183 (nth i ? (vec … (nth (S j) ? v1 (all_blank sig n))) (blank ?)) i.
185 (* supposing (shift_l … i v1 v2), the i-th trace of v2 is equal to the tail of
186 the i-th trace of v1, plus a trailing blank *)
188 lemma trace_shift: ∀sig,n,i,v1,v2. i < n → 0 < |v1| →
189 shift_l sig n i v1 v2 → trace ? n i v2 = tail ? (trace ? n i v1)@[blank sig].
190 #sig #n #i #v1 #v2 #lein #Hlen * #Hlen1 #Hnth @(nth_to_eq … (blank ?))
191 [>length_trace <Hlen1 generalize in match Hlen; cases v1
192 [normalize #H @(le_n_O_elim … H) //
193 |#b #tl #_ normalize >length_append >length_trace normalize //
195 |#j >nth_trace >Hnth >nth_change_vec // >tail_trace
196 cut (trace ? n i [all_blank sig n] = [blank sig])
197 [normalize >blank_all_blank //]
198 #Hcut <Hcut <trace_append >nth_trace
203 (* supposing (shift_l … i v1 v2), and j≠i, the j-th trace of v2 is equal to the
206 lemma trace_shift_neq: ∀sig,n,i,j,v1,v2. i < n → 0 < |v1| → i ≠ j →
207 shift_l sig n i v1 v2 → trace ? n j v2 = trace ? n j v1.
208 #sig #n #i #j #v1 #v2 #lein #Hlen #Hneq * #Hlen1 #Hnth @(nth_to_eq … (blank ?))
209 [>length_trace >length_trace @sym_eq @Hlen1
210 |#k >nth_trace >Hnth >nth_change_vec_neq // >nth_trace //
214 (******************************************************************************)
216 let rec to_blank sig l on l ≝
220 if a == blank sig then [ ] else a::(to_blank sig tl)].
222 let rec after_blank sig l on l ≝
226 if a == blank sig then (a::tl) else (after_blank sig tl)].
228 definition to_blank_i ≝ λsig,n,i,l. to_blank ? (trace sig n i l).
230 lemma to_blank_i_def : ∀sig,n,i,l.
231 to_blank_i sig n i l = to_blank ? (trace sig n i l).
234 lemma to_blank_cons_b : ∀sig,n,i,a,l.
235 nth i ? (vec … n a) (blank sig) = blank ? →
236 to_blank_i sig n i (a::l) = [ ].
237 #sig #n #i #a #l #H whd in match (to_blank_i ????);
241 lemma to_blank_cons_nb: ∀sig,n,i,a,l.
242 nth i ? (vec … n a) (blank sig) ≠ blank ? →
243 to_blank_i sig n i (a::l) =
244 nth i ? (vec … n a) (blank sig)::(to_blank_i sig n i l).
245 #sig #n #i #a #l #H whd in match (to_blank_i ????);
249 axiom to_blank_hd : ∀sig,n,a,b,l1,l2.
250 (∀i. i ≤ n → to_blank_i sig n i (a::l1) = to_blank_i sig n i (b::l2)) → a = b.
252 lemma to_blank_i_ext : ∀sig,n,i,l.
253 to_blank_i sig n i l = to_blank_i sig n i (l@[all_blank …]).
255 [@sym_eq @to_blank_cons_b @blank_all_blank
256 |#a #tl #Hind whd in match (to_blank_i ????); >Hind <to_blank_i_def >Hind %
260 lemma to_blank_hd_cons : ∀sig,n,i,l1,l2.
261 to_blank_i sig n i (l1@l2) =
262 to_blank_i … i (l1@(hd … l2 (all_blank …))::tail … l2).
263 #sig #n #i #l1 #l2 cases l2
264 [whd in match (hd ???); whd in match (tail ??); >append_nil @to_blank_i_ext
269 lemma to_blank_i_chop : ∀sig,n,i,a,l1,l2.
270 (nth i ? (vec … a) (blank ?))= blank ? →
271 to_blank_i sig n i (l1@a::l2) = to_blank_i sig n i l1.
272 #sig #n #i #a #l1 elim l1
273 [#l2 #H @to_blank_cons_b //
274 |#x #tl #Hind #l2 #H whd in match (to_blank_i ????);
275 >(Hind l2 H) <to_blank_i_def >(Hind l2 H) %