1 include "turing/auxiliary_machines1.ma".
2 include "turing/multi_to_mono/shift_trace_aux.ma".
4 (******************************************************************************)
5 (* mtiL: complete move L for tape i. We reaching the left border of trace i, *)
6 (* add a blank if there is no more tape, then move the i-trace and finally *)
7 (* come back to the head position. *)
8 (******************************************************************************)
10 (* we say that a tape is regular if for any trace after the first blank we
11 only have other blanks *)
13 definition all_blanks_in ≝ λsig,l.
14 ∀x. mem ? x l → x = blank sig.
16 definition regular_i ≝ λsig,n.λl:list (multi_sig sig n).λi.
17 all_blanks_in ? (after_blank ? (trace sig n i l)).
19 definition regular_trace ≝ λsig,n,a.λls,rs:list (multi_sig sig n).λi.
20 Or (And (regular_i sig n (a::ls) i) (regular_i sig n rs i))
21 (And (regular_i sig n ls i) (regular_i sig n (a::rs) i)).
23 axiom regular_tail: ∀sig,n,l,i.
24 regular_i sig n l i → regular_i sig n (tail ? l) i.
26 axiom regular_extend: ∀sig,n,l,i.
27 regular_i sig n l i → regular_i sig n (l@[all_blanks sig n]) i.
29 axiom all_blank_after_blank: ∀sig,n,l1,b,l2,i.
30 nth i ? (vec … b) (blank ?) = blank ? →
31 regular_i sig n (l1@b::l2) i → all_blanks_in ? (trace sig n i l2).
33 lemma regular_trace_extl: ∀sig,n,a,ls,rs,i.
34 regular_trace sig n a ls rs i →
35 regular_trace sig n a (ls@[all_blanks sig n]) rs i.
36 #sig #n #a #ls #rs #i *
37 [* #H1 #H2 % % // @(regular_extend … H1)
38 |* #H1 #H2 %2 % // @(regular_extend … H1)
42 lemma regular_cons_hd_rs: ∀sig,n.∀a:multi_sig sig n.∀ls,rs1,rs2,i.
43 regular_trace sig n a ls (rs1@rs2) i →
44 regular_trace sig n a ls (rs1@((hd ? rs2 (all_blanks …))::(tail ? rs2))) i.
45 #sig #n #a #ls #rs1 #rs2 #i cases rs2 [2: #b #tl #H @H]
46 *[* #H1 >append_nil #H2 %1 %
47 [@H1 | whd in match (hd ???); @(regular_extend … rs1) //]
48 |* #H1 >append_nil #H2 %2 %
49 [@H1 | whd in match (hd ???); @(regular_extend … (a::rs1)) //]
53 lemma eq_trace_to_regular : ∀sig,n.∀a1,a2:multi_sig sig n.∀ls1,ls2,rs1,rs2,i.
54 nth i ? (vec … a1) (blank ?) = nth i ? (vec … a2) (blank ?) →
55 trace sig n i ls1 = trace sig n i ls2 →
56 trace sig n i rs1 = trace sig n i rs2 →
57 regular_trace sig n a1 ls1 rs1 i →
58 regular_trace sig n a2 ls2 rs2 i.
59 #sig #n #a1 #a2 #ls1 #ls2 #rs1 #rs2 #i #H1 #H2 #H3 #H4
60 whd in match (regular_trace ??????); whd in match (regular_i ????);
61 whd in match (regular_i ?? rs2 ?); whd in match (regular_i ?? ls2 ?);
62 whd in match (regular_i ?? (a2::rs2) ?); whd in match (trace ????);
63 <trace_def whd in match (trace ??? (a2::rs2)); <trace_def
67 (******************************* move_to_blank_L ******************************)
68 (* we compose machines together to reduce the number of output cases, and
71 definition move_to_blank_L ≝ λsig,n,i.
72 (move_until ? L (not_blank sig n i)) · extend ? (all_blanks sig n).
75 definition R_move_to_blank_L ≝ λsig,n,i,t1,t2.
76 (current ? t1 = None ? →
77 t2 = midtape (multi_sig sig n) (left ? t1) (all_blank …) (right ? t1)) ∧
78 ∀ls,a,rs.t1 = midtape ? ls a rs →
79 ((no_blank sig n i a = false) ∧ t2 = t1) ∨
81 (no_blank sig n i b = false) ∧
82 (∀j.j ≤n → to_blank_i ?? j (ls1@b::ls2) = to_blank_i ?? j ls) ∧
83 t2 = midtape ? ls2 b ((reverse ? (a::ls1))@rs)).
86 definition R_move_to_blank_L ≝ λsig,n,i,t1,t2.
87 (current ? t1 = None ? →
88 t2 = midtape (multi_sig sig n) (left ? t1) (all_blanks …) (right ? t1)) ∧
90 t1 = midtape (multi_sig sig n) ls a rs →
91 regular_i sig n (a::ls) i →
92 (∀j. j ≠ i → regular_trace … a ls rs j) →
94 (regular_i sig n (ls1@b::ls2) i) ∧
95 (∀j. j ≠ i → regular_trace …
96 (hd ? (ls1@b::ls2) (all_blanks …)) (tail ? (ls1@b::ls2)) rs j) ∧
97 (not_blank sig n i b = false) ∧
98 (hd (multi_sig sig n) (ls1@[b]) (all_blanks …) = a) ∧ (* not implied by the next fact *)
99 (∀j.j < n → to_blank_i ?? j (ls1@b::ls2) = to_blank_i ?? j (a::ls)) ∧
100 t2 = midtape ? ls2 b ((reverse ? ls1)@rs)).
102 theorem sem_move_to_blank_L: ∀sig,n,i.
103 move_to_blank_L sig n i ⊨ R_move_to_blank_L sig n i.
106 (ssem_move_until_L ? (not_blank sig n i)) (sem_extend ? (all_blanks sig n)))
107 #tin #tout * #t1 * * #Ht1a #Ht1b * #Ht2a #Ht2b %
108 [#Hcur >(Ht1a Hcur) in Ht2a; /2 by /
109 |#ls #a #rs #Htin #Hreg #Hreg2 -Ht1a cases (Ht1b … Htin)
110 [* #Hnb #Ht1 -Ht1b -Ht2a >Ht1 in Ht2b; >Htin #H
112 %[%[%[%[%[@Hreg|@Hreg2]|@Hnb]|//]|//]|@H normalize % #H1 destruct (H1)]
114 [(* we find the blank *)
115 * #ls1 * #b * #ls2 * * * #H1 #H2 #H3 #Ht1
116 >Ht1 in Ht2b; #Hout -Ht1b
117 %{b} %{(a::ls1)} %{ls2}
118 %[%[%[%[%[>H1 in Hreg; #H @H
119 |#j #jneqi whd in match (hd ???); whd in match (tail ??);
120 <H1 @(Hreg2 j jneqi)]|@H2] |//]|>H1 //]
121 |@Hout normalize % normalize #H destruct (H)
123 |* #b * #lss * * #H1 #H2 #Ht1 -Ht1b >Ht1 in Ht2a;
124 whd in match (left ??); whd in match (right ??); #Hout
125 %{(all_blanks …)} %{(lss@[b])} %{[]}
126 %[%[%[%[%[<H2 @regular_extend //
127 |<H2 #j #jneqi whd in match (hd ???); whd in match (tail ??);
128 @regular_trace_extl @Hreg2 //]
129 |whd in match (not_blank ????); >blank_all_blanks //]
131 |#j #lejn <H2 @sym_eq @to_blank_i_ext]
132 |>reverse_append >reverse_single @Hout normalize //
138 (******************************************************************************)
140 definition shift_i_L ≝ λsig,n,i.
141 ncombf_r (multi_sig …) (shift_i sig n i) (all_blanks sig n) ·
143 extend ? (all_blanks sig n).
145 definition R_shift_i_L ≝ λsig,n,i,t1,t2.
147 t1 = midtape ? ls a rs →
150 nth i ? (vec … b) (blank ?) = (blank ?) ∧
151 (∀x. mem ? x rs1 → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
152 shift_l sig n i (a::rs1) (a1::rss) ∧
153 t2 = midtape (multi_sig sig n) ((reverse ? (a1::rss))@ls) b rs2) ∨
155 (∀x. mem ? x rs → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
156 shift_l sig n i (a::rs) (rss@[b]) ∧
157 t2 = midtape (multi_sig sig n)
158 ((reverse ? (rss@[b]))@ls) (all_blanks sig n) [ ]))).
160 definition R_shift_i_L_new ≝ λsig,n,i,t1,t2.
162 t1 = midtape ? ls a rs →
164 b = hd ? rs2 (all_blanks sig n) ∧
165 nth i ? (vec … b) (blank ?) = (blank ?) ∧
167 (∀x. mem ? x rs1 → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
168 shift_l sig n i (a::rs1) rss ∧
169 t2 = midtape (multi_sig sig n) ((reverse ? rss)@ls) b (tail ? rs2)).
171 theorem sem_shift_i_L: ∀sig,n,i. shift_i_L sig n i ⊨ R_shift_i_L sig n i.
174 (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blanks sig n))
175 (sem_seq ????? (ssem_mti sig n i)
176 (sem_extend ? (all_blanks sig n))))
177 #tin #tout * #t1 * * #Ht1a #Ht1b * #t2 * * #Ht2a #Ht2b * #Htout1 #Htout2
179 [#Htin %2 %{(shift_i sig n i a (all_blanks sig n))} %{[ ]}
180 %[%[#x @False_ind | @daemon]
181 |lapply (Ht1a … Htin) -Ht1a -Ht1b #Ht1
182 lapply (Ht2a … Ht1) -Ht2a -Ht2b #Ht2 >Ht2 in Htout1;
183 >Ht1 whd in match (left ??); whd in match (right ??); #Htout @Htout //
186 lapply (Ht1b … Htin) -Ht1a -Ht1b #Ht1
187 lapply (Ht2b … Ht1) -Ht2a -Ht2b *
188 [(* a1 is blank *) * #H1 #H2 %1
189 %{[ ]} %{a1} %{rs1} %{(shift_i sig n i a a1)} %{[ ]}
190 %[%[%[%[// |//] |#x @False_ind] | @daemon]
191 |>Htout2 [>H2 >reverse_single @Ht1 |>H2 >Ht1 normalize % #H destruct (H)]
194 [* #rs10 * #b * #rs2 * #rss * * * * #H1 #H2 #H3 #H4
196 %{(a1::rs10)} %{b} %{rs2} %{(shift_i sig n i a a1)} %{rss}
197 %[%[%[%[>H1 //|//] |@H3] |@daemon ]
198 |>reverse_cons >associative_append
199 >H2 in Htout2; #Htout >Htout [@Ht2| >Ht2 normalize % #H destruct (H)]
201 |* #b * #rss * * #H1 #H2
203 %{(shift_i sig n i b (all_blanks sig n))} %{(shift_i sig n i a a1::rss)}
205 |>Ht2 in Htout1; #Htout >Htout //
206 whd in match (left ??); whd in match (right ??);
207 >reverse_append >reverse_single >associative_append >reverse_cons
208 >associative_append //
215 theorem sem_shift_i_L_new: ∀sig,n,i.
216 shift_i_L sig n i ⊨ R_shift_i_L_new sig n i.
218 @(Realize_to_Realize … (sem_shift_i_L sig n i))
219 #t1 #t2 #H #a #ls #rs #Ht1 lapply (H a ls rs Ht1) *
220 [* #rs1 * #b * #rs2 * #a1 * #rss * * * * #H1 #H2 #H3 #H4 #Ht2
221 %{rs1} %{b} %{(b::rs2)} %{(a1::rss)}
222 %[%[%[%[%[//|@H2]|@H1]|@H3]|@H4] | whd in match (tail ??); @Ht2]
223 |* #b * #rss * * #H1 #H2 #Ht2
224 %{rs} %{(all_blanks sig n)} %{[]} %{(rss@[b])}
225 %[%[%[%[%[//|@blank_all_blanks]|//]|@H1]|@H2] | whd in match (tail ??); @Ht2]
230 (*******************************************************************************
231 The following machine implements a full move for a trace: we reach the left
232 border, shift the i-th trace and come back to the head position.
233 The head may hold additional information A, so we suppose that the tape alphabet
234 is the disjoint sum between A and the alphabet sig of the multi tape machine. *)
236 definition TA ≝ λA,sig. FinSum A sig.
237 definition MTA ≝ λA,sig,n.multi_sig (TA A sig) n.
239 definition is_head ≝ λA,sig.λc:sig_ext (TA A sig).
242 | Some a ⇒ match a with
246 definition is_sig ≝ λA,sig.λc:sig_ext (TA A sig).
249 | Some a ⇒ match a with
253 definition not_head ≝ λA,sig,n.λc:multi_sig (TA A sig) (S n).
254 ¬(is_head A sig (nth n ? (vec … c) (blank ?))).
256 lemma not_head_all_blanks : ∀A,sig,n.
257 not_head A sig n (all_blanks … (S n)) = true.
258 #A #sig #n whd in ⊢ (??%?); >blank_all_blanks //
261 definition no_head_in ≝ λA,sig,n,l.
262 ∀x. mem ? x (trace (TA A sig) (S n) n l) → is_head … x = false.
265 lemma not_head_true: ∀A,sig,n,c. not_head A sig n c = true →
266 is_head … (nth n ? (vec … c) (blank ?)) = false.
269 lemma hd_nil : ∀A,d. hd A [ ] d = d.
272 definition mtiL ≝ λA,sig,n,i.
273 move_to_blank_L (TA A sig) (S n) i ·
274 shift_i_L (TA A sig) (S n) i ·
275 move_until ? L (not_head A sig n).
277 definition Rmtil ≝ λA,sig,n,i,t1,t2.
279 t1 = midtape (MTA A sig (S n)) ls a rs →
280 is_head A sig (nth n ? (vec … a) (blank ?)) = true →
281 (∀i.regular_trace (TA A sig) (S n) a ls rs i) →
282 (* next: we cannot be on rightof on trace i *)
283 (nth i ? (vec … a) (blank ?) = (blank ?)
284 → nth i ? (vec … (hd ? rs (all_blanks …))) (blank ?) ≠ (blank ?)) →
288 t2 = midtape (MTA A sig (S n)) ls1 a1 rs1 ∧
289 (∀i.regular_trace … a1 ls1 rs1 i) ∧
290 (∀j. j ≤ n → j ≠ i → to_blank_i ? (S n) j (a1::ls1) = to_blank_i ? (S n) j (a::ls)) ∧
291 (∀j. j ≤ n → j ≠ i → to_blank_i ? (S n) j rs1 = to_blank_i ? (S n) j rs) ∧
292 (to_blank_i ? (S n) i ls1 = to_blank_i ? (S n) i (a::ls)) ∧
293 (to_blank_i ? (S n) i (a1::rs1)) = to_blank_i ? (S n) i rs).
295 theorem sem_Rmtil: ∀A,sig,n,i. i < n → mtiL A sig n i ⊨ Rmtil A sig n i.
298 (sem_move_to_blank_L … )
299 (sem_seq ????? (sem_shift_i_L_new …)
300 (ssem_move_until_L ? (not_head A sig n))))
301 #tin #tout * #t1 * * #_ #Ht1 * #t2 * #Ht2 * #_ #Htout
302 (* we start looking into Rmitl *)
303 #ls #a #rs #Htin (* tin is a midtape *)
304 #Hheada #Hreg #no_rightof #Hnohead_ls #Hnohead_rs
305 cut (regular_i ? (S n) (a::ls) i)
307 cases (true_or_false (nth i ? (vec … a) (blank ?) == (blank ?))) #Htest
308 [#_ @daemon (* absurd, since hd rs non e' blank *)
309 |#H #_ @daemon]] #Hreg1
310 lapply (Ht1 … Htin Hreg1 ?) [#j #_ @Hreg] -Ht1 -Htin
311 * #b * #ls1 * #ls2 * * * * * #reg_ls1_i #reg_ls1_j #Hno_blankb #Hhead #Hls1 #Ht1
312 lapply (Ht2 … Ht1) -Ht2 -Ht1
313 * #rs1 * #b0 * #rs2 * #rss * * * * * #Hb0 #Hb0blank #Hrs1 #Hrs1b #Hrss #Ht2
314 (* we need to recover the position of the head of the emulated machine
315 that is the head of ls1. This is somewhere inside rs1 *)
316 cut (∃rs11. rs1 = (reverse ? ls1)@rs11)
317 [cut (ls1 = [ ] ∨ ∃aa,tlls1. ls1 = aa::tlls1)
318 [cases ls1 [%1 // | #aa #tlls1 %2 %{aa} %{tlls1} //]] *
319 [#H1ls1 %{rs1} >H1ls1 //
320 |* #aa * #tlls1 #H1ls1 >H1ls1 in Hrs1;
321 cut (aa = a) [>H1ls1 in Hls1; #H @(to_blank_hd … H)] #eqaa >eqaa
322 #Hrs1_aux cases (compare_append … (sym_eq … Hrs1_aux)) #l *
324 |(* this is absurd : if l is empty, the case is as before.
325 if l is not empty then it must start with a blank, since it is the
326 first character in rs2. But in this case we would have a blank
327 inside ls1=a::tls1 that is absurd *)
332 [@(injective_append_l … (reverse … ls1)) >Hrs1 <associative_append <H1 //] #H2
333 lapply (Htout … Ht2) -Htout -Ht2 *
334 [(* the current character on trace i holds the head-mark.
335 The case is absurd, since b0 is the head of rs2, that is a sublist of rs,
336 and the head-mark is not in rs *)
337 * #H3 @False_ind @(absurd (true=false)) [2://] <H3 @sym_eq
338 <(notb_notb true) @(eq_f … notb) @Hnohead_rs >H2 >trace_append @mem_append_l2
340 [>hd_nil #H >H in H3; >not_head_all_blanks #Habs destruct (Habs)
344 [(* we reach the head position *)
345 (* cut (trace sig n j (a1::ls20)=trace sig n j (ls1@b::ls2)) *)
346 * #ls10 * #a1 * #ls20 * * * #Hls20 #Ha1 #Hnh #Htout
348 trace ? (S n) j (reverse (multi_sig (TA A sig) (S n)) rs1@b::ls2) =
349 trace ? (S n) j (ls10@a1::ls20))
350 [#j #ineqj >append_cons <reverse_cons >trace_def <map_append <reverse_map
351 lapply (trace_shift_neq … (le_S … lt_in) ? (sym_not_eq … ineqj) … Hrss) [//] #Htr
352 <(trace_def … (b::rs1)) <Htr >reverse_map >map_append @eq_f @Hls20 ]
354 cut (trace ? (S n) i (reverse (multi_sig (TA A sig) (S n)) (rs1@[b0])@ls2) =
355 trace ? (S n) i (ls10@a1::ls20))
356 [>trace_def <map_append <reverse_map <map_append <(trace_def … [b0])
357 cut (trace ? (S n) i [b0] = [blank ?]) [@daemon] #Hcut >Hcut
358 lapply (trace_shift … (le_S … lt_in) … Hrss) [//] whd in match (tail ??); #Htr <Htr
359 >reverse_map >map_append <trace_def <Hls20 %
363 (trace ? (S n) j (reverse (MTA A sig (S n)) rs11) = trace ? (S n) j ls10) ∧
364 (trace ? (S n) j (ls1@b::ls2) = trace ? (S n) j (a1::ls20)))
366 #j #ineqj @(first_P_to_eq ? (λx. x ≠ head ?))
367 [lapply (Htracej … ineqj) >trace_def in ⊢ (%→?); <map_append
368 >trace_def in ⊢ (%→?); <map_append #H @H
370 cut ((trace ? (S n) i (b0::reverse ? rs11) = trace ? (S n) i (ls10@[a1])) ∧
371 (trace ? (S n) i (ls1@ls2) = trace ? (S n) i ls20))
372 [>H1 in Htracei; >reverse_append >reverse_single >reverse_append
373 >reverse_reverse >associative_append >associative_append
377 trace ? (S n) j (reverse ? ls10@rs2) = trace ? (S n) j rs)
378 [#j #jneqi @(injective_append_l … (trace ? (S n) j (reverse ? ls1)))
379 >map_append >map_append >Hrs1 >H1 >associative_append
380 <map_append <map_append in ⊢ (???%); @eq_f
381 <map_append <map_append @eq_f2 // @sym_eq
382 <(reverse_reverse … rs11) <reverse_map <reverse_map in ⊢ (???%);
383 @eq_f @(proj1 … (H2 j jneqi))] #Hrs_j
384 %{ls20} %{a1} %{(reverse ? (b0::ls10)@tail ? rs2)}
386 |#j cases (decidable_eq_nat j i)
387 [#eqji >eqji (* by cases wether a1 is blank *)
389 |#jneqi lapply (reg_ls1_j … jneqi) #H4
390 >reverse_cons >associative_append >Hb0 @regular_cons_hd_rs
391 @(eq_trace_to_regular … H4)
392 [<hd_trace >(proj2 … (H2 … jneqi)) >hd_trace %
393 |<tail_trace >(proj2 … (H2 … jneqi)) >tail_trace %
397 |#j #lejn #jneqi <(Hls1 … (le_S_S … lejn))
398 >to_blank_i_def >to_blank_i_def @eq_f @sym_eq @(proj2 … (H2 j jneqi))]
399 |#j #lejn #jneqi >reverse_cons >associative_append >Hb0
400 <to_blank_hd_cons >to_blank_i_def >to_blank_i_def @eq_f @Hrs_j //]
401 |<(Hls1 i) [2:@le_S //]
402 lapply (all_blank_after_blank … reg_ls1_i)
403 [@(\P ?) @daemon] #allb_ls2
404 whd in match (to_blank_i ????); <(proj2 … H3)
406 |>reverse_cons >associative_append
407 cut (to_blank_i ? (S n) i rs = to_blank_i ? (S n) i (rs11@[b0])) [@daemon]
408 #Hcut >Hcut >(to_blank_i_chop … b0 (a1::reverse …ls10)) [2: @Hb0blank]
409 >to_blank_i_def >to_blank_i_def @eq_f
410 >trace_def >trace_def @injective_reverse >reverse_map >reverse_cons
411 >reverse_reverse >reverse_map >reverse_append >reverse_single @sym_eq
414 |(*we do not find the head: this is absurd *)
415 * #b1 * #lss * * #H2 @False_ind
416 cut (∀x0. mem ? x0 (trace ? (S n) n (b0::reverse ? rss@ls2)) → is_head … x0 = false)
418 lapply (trace_shift_neq ? (S n) i n … (le_S … lt_in) … Hrss)
419 [@lt_to_not_eq @lt_in | // ]
421 (is_head … (nth n ? (vec … (hd ? (ls1@[b]) (all_blanks … (S n)))) (blank ?)) = true))
423 |@eqnot_to_noteq @H2 >trace_def %2 <map_append @mem_append_l1 <reverse_map <trace_def
424 >H3 >H1 >trace_def >reverse_map >reverse_cons >reverse_append
425 >reverse_reverse >associative_append <map_append @mem_append_l2
426 cases ls1 [%1 % |#x #ll %1 %]