1 include "turing/basic_machines.ma".
2 include "turing/if_machine.ma".
3 include "turing/auxiliary_machines1.ma".
4 include "turing/multi_to_mono/trace_alphabet.ma".
6 (* a machine that moves the i trace r: we reach the left margin of the i-trace
7 and make a (shifted) copy of the old tape up to the end of the right margin of
8 the i-trace. Then come back to the origin. *)
10 definition shift_i ≝ λsig,n,i.λa,b:Vector (sig_ext sig) n.
11 change_vec (sig_ext sig) n a (nth i ? b (blank ?)) i.
13 (* vec is a coercion. Why should I insert it? *)
14 definition mti_step ≝ λsig:FinSet.λn,i.
15 ifTM (multi_sig sig n) (test_char ? (λc:multi_sig sig n.¬(nth i ? (vec … c) (blank ?))==blank ?))
16 (single_finalTM … (ncombf_r (multi_sig sig n) (shift_i sig n i) (all_blank sig n)))
19 definition Rmti_step_true ≝
21 ∃b:multi_sig sig n. (nth i ? (vec … b) (blank ?) ≠ blank ?) ∧
23 t1 = midtape (multi_sig sig n) ls b (a::rs) ∧
24 t2 = midtape (multi_sig sig n) ((shift_i sig n i b a)::ls) a rs) ∨
26 t1 = midtape ? ls b [] ∧
27 t2 = rightof ? (shift_i sig n i b (all_blank sig n)) ls)).
29 (* 〈combf0,all_blank sig n〉 *)
30 definition Rmti_step_false ≝
32 (∀ls,b,rs. t1 = midtape (multi_sig sig n) ls b rs →
33 (nth i ? (vec … b) (blank ?) = blank ?)) ∧ t2 = t1.
38 [inr … (inl … (inr … start_nop)): Rmti_step_true sig n i, Rmti_step_false sig n i].
40 @(acc_sem_if_app (multi_sig sig n) ??????????
41 (sem_test_char …) (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
42 (sem_nop (multi_sig sig n)))
43 [#intape #outtape #tapea whd in ⊢ (%→%→%); * * #c *
44 #Hcur cases (current_to_midtape … Hcur) #ls * #rs #Hintape
45 #ctest #Htapea * #Hout1 #Hout2 @(ex_intro … c) %
46 [@(\Pf (injective_notb … )) @ctest]
47 generalize in match Hintape; -Hintape cases rs
48 [#Hintape %2 @(ex_intro …ls) % // @Hout1 >Htapea @Hintape
50 @(ex_intro … ls) @(ex_intro … a) @(ex_intro … rs1) % //
51 @Hout2 >Htapea @Hintape
53 |#intape #outtape #tapea whd in ⊢ (%→%→%);
54 * #Htest #tapea #outtape
56 #intape lapply (Htest b ?) [>intape //] -Htest #Htest
57 lapply (injective_notb ? true Htest) -Htest #Htest @(\P Htest)
61 (* move tape i machine *)
63 λsig,n,i.whileTM (multi_sig sig n) (mti_step sig n i) (inr … (inl … (inr … start_nop))).
65 (* v2 is obtained from v1 shifting left the i-th trace *)
66 definition shift_l ≝ λsig,n,i,v1,v2. (* multi_sig sig n*)
68 ∀j.nth j ? v2 (all_blank sig n) =
69 change_vec ? n (nth j ? v1 (all_blank sig n))
70 (nth i ? (vec … (nth (S j) ? v1 (all_blank sig n))) (blank ?)) i.
72 lemma trace_shift: ∀sig,n,i,v1,v2. i < n → 0 < |v1| →
73 shift_l sig n i v1 v2 → trace ? n i v2 = tail ? (trace ? n i v1)@[blank sig].
74 #sig #n #i #v1 #v2 #lein #Hlen * #Hlen1 #Hnth @(nth_to_eq … (blank ?))
75 [>length_trace <Hlen1 generalize in match Hlen; cases v1
76 [normalize #H @(le_n_O_elim … H) //
77 |#b #tl #_ normalize >length_append >length_trace normalize //
79 |#j >nth_trace >Hnth >nth_change_vec // >tail_trace
80 cut (trace ? n i [all_blank sig n] = [blank sig])
81 [normalize >blank_all_blank //]
82 #Hcut <Hcut <trace_append >nth_trace
87 lemma trace_shift_neq: ∀sig,n,i,j,v1,v2. i < n → 0 < |v1| → i ≠ j →
88 shift_l sig n i v1 v2 → trace ? n j v2 = trace ? n j v1.
89 #sig #n #i #j #v1 #v2 #lein #Hlen #Hneq * #Hlen1 #Hnth @(nth_to_eq … (blank ?))
90 [>length_trace >length_trace @sym_eq @Hlen1
91 |#k >nth_trace >Hnth >nth_change_vec_neq // >nth_trace //
95 axiom daemon: ∀P:Prop.P.
99 (∀a,rs. t1 = rightof ? a rs → t2 = t1) ∧
101 t1 = midtape (multi_sig sig n) ls a rs →
102 (nth i ? (vec … a) (blank ?) = blank ? ∧ t2 = t1) ∨
105 nth i ? (vec … b) (blank ?) = (blank ?) ∧
106 (∀x. mem ? x (a::rs1) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
107 shift_l sig n i (a::rs1) rss ∧
108 t2 = midtape (multi_sig sig n) ((reverse ? rss)@ls) b rs2) ∨
110 (∀x. mem ? x (a::rs) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
111 shift_l sig n i (a::rs) (rss@[b]) ∧
112 t2 = rightof (multi_sig sig n) (shift_i sig n i b (all_blank sig n))
113 ((reverse ? rss)@ls)))).
117 WRealize (multi_sig sig n) (mti sig n i) (R_mti sig n i).
118 #sig #n #i #inc #j #outc #Hloop
119 lapply (sem_while … (sem_mti_step sig n i) inc j outc Hloop) [%]
120 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
121 [ whd in ⊢ (% → ?); * #H1 #H2 %
123 |#a #ls #rs #Htapea % % [@(H1 … Htapea) |@H2]
125 | #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
126 lapply (IH HRfalse) -IH -HRfalse whd in ⊢ (%→%);
128 [#b0 #ls #Htapeb cases Hstar1 #b * #_ *
129 [* #ls0 * #a * #rs0 * >Htapeb #H destruct (H)
130 |* #ls0 * >Htapeb #H destruct (H)
132 |#b0 #ls #rs #Htapeb cases Hstar1 #b * #btest *
133 [* #ls1 * #a * #rs1 * >Htapeb #H destruct (H) #Htapec
134 %2 cases (IH2 … Htapec)
137 %{[ ]} %{a} %{rs1} %{[shift_i sig n i b a]} %
138 [%[%[% // |#x #Hb >(mem_single ??? Hb) // ]
140 |>Hout >reverse_single @Htapec
143 [ (* case a \= None and exists b = None *) -IH1 -IH2 #IH
144 %1 cases IH -IH #rs10 * #b0 * #rs2 * #rss * * * *
146 %{(a::rs10)} %{b0} %{rs2} %{(shift_i sig n i b a::rss)}
148 |#x * [#eqxa >eqxa (*?? *) @daemon|@H3]]
150 |>H5 >reverse_cons >associative_append //
152 | (* case a \= None and we reach the end of the (full) tape *) -IH1 -IH2 #IH
153 %2 cases IH -IH #b0 * #rss * * #H1 #H2 #H3
154 %{b0} %{(shift_i sig n i b a::rss)}
155 %[%[#x * [#eqxb >eqxb @btest|@H1]
157 |>H3 >reverse_cons >associative_append //
161 |(* b \= None but the left tape is empty *)
162 * #ls0 * >Htapeb #H destruct (H) #Htapec
164 %[%[#x * [#eqxb >eqxb @btest|@False_ind]
165 |@daemon (*shift of dingle char OK *)]
166 |>(IH1 … Htapec) >Htapec //
171 lemma WF_mti_niltape:
172 ∀sig,n,i. WF ? (inv ? (Rmti_step_true sig n i)) (niltape ?).
173 #sig #n #i @wf #t1 whd in ⊢ (%→?); * #b * #_ *
174 [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
177 lemma WF_mti_rightof:
178 ∀sig,n,i,a,ls. WF ? (inv ? (Rmti_step_true sig n i)) (rightof ? a ls).
179 #sig #n #i #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ *
180 [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
184 ∀sig,n,i,a,ls. WF ? (inv ? (Rmti_step_true sig n i)) (leftof ? a ls).
185 #sig #n #i #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ *
186 [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
190 ∀sig,n,i.∀t. Terminate ? (mti sig n i) t.
191 #sig #n #i #t @(terminate_while … (sem_mti_step sig n i)) [%]
192 cases t // #ls #c #rs lapply c -c lapply ls -ls elim rs
193 [#ls #c @wf #t1 whd in ⊢ (%→?); * #b * #_ *
194 [* #ls1 * #a * #rs1 * #H destruct
195 |* #ls1 * #H destruct #Ht1 >Ht1 //
197 |#a #rs1 #Hind #ls #c @wf #t1 whd in ⊢ (%→?); * #b * #_ *
198 [* #ls1 * #a2 * #rs2 * #H destruct (H) #Ht1 >Ht1 //
199 |* #ls1 * #H destruct
204 lemma ssem_mti: ∀sig,n,i.
205 Realize ? (mti sig n i) (R_mti sig n i).
208 (******************************************************************************)
209 (* mtiL: complete move L for tape i. We reaching the left border of trace i, *)
210 (* add a blank if there is no more tape, then move the i-trace and finally *)
211 (* come back to the head position. *)
212 (******************************************************************************)
214 definition no_blank ≝ λsig,n,i.λc:multi_sig sig n.
215 ¬(nth i ? (vec … c) (blank ?))==blank ?.
217 definition no_head ≝ λsig,n.λc:multi_sig sig n.
218 ¬((nth n ? (vec … c) (blank ?))==head ?).
220 let rec to_blank sig l on l ≝
224 if a == blank sig then [ ] else a::(to_blank sig tl)].
226 definition to_blank_i ≝ λsig,n,i,l. to_blank ? (trace sig n i l).
228 lemma to_blank_i_def : ∀sig,n,i,l.
229 to_blank_i sig n i l = to_blank ? (trace sig n i l).
235 let ai ≝ nth i ? (vec … n a) (blank sig) in
236 if ai == blank ? then [ ] else ai::(to_blank sig n i tl)]. *)
238 lemma to_blank_cons_b : ∀sig,n,i,a,l.
239 nth i ? (vec … n a) (blank sig) = blank ? →
240 to_blank_i sig n i (a::l) = [ ].
241 #sig #n #i #a #l #H whd in match (to_blank_i ????);
245 lemma to_blank_cons_nb: ∀sig,n,i,a,l.
246 nth i ? (vec … n a) (blank sig) ≠ blank ? →
247 to_blank_i sig n i (a::l) =
248 nth i ? (vec … n a) (blank sig)::(to_blank_i sig n i l).
249 #sig #n #i #a #l #H whd in match (to_blank_i ????);
253 axiom to_blank_hd : ∀sig,n,a,b,l1,l2.
254 (∀i. i ≤ n → to_blank_i sig n i (a::l1) = to_blank_i sig n i (b::l2)) → a = b.
256 lemma to_blank_i_ext : ∀sig,n,i,l.
257 to_blank_i sig n i l = to_blank_i sig n i (l@[all_blank …]).
259 [@sym_eq @to_blank_cons_b @blank_all_blank
260 |#a #tl #Hind whd in match (to_blank_i ????); >Hind <to_blank_i_def >Hind %
264 lemma to_blank_hd_cons : ∀sig,n,i,l1,l2.
265 to_blank_i sig n i (l1@l2) =
266 to_blank_i … i (l1@(hd … l2 (all_blank …))::tail … l2).
267 #sig #n #i #l1 #l2 cases l2
268 [whd in match (hd ???); whd in match (tail ??); >append_nil @to_blank_i_ext
273 lemma to_blank_i_chop : ∀sig,n,i,a,l1,l2.
274 (nth i ? (vec … a) (blank ?))= blank ? →
275 to_blank_i sig n i (l1@a::l2) = to_blank_i sig n i l1.
276 #sig #n #i #a #l1 elim l1
277 [#l2 #H @to_blank_cons_b //
278 |#x #tl #Hind #l2 #H whd in match (to_blank_i ????);
279 >(Hind l2 H) <to_blank_i_def >(Hind l2 H) %
283 (******************************* move_to_blank_L ******************************)
284 (* we compose machines together to reduce the number of output cases, and
287 definition move_to_blank_L ≝ λsig,n,i.
288 (move_until ? L (no_blank sig n i)) · extend ? (all_blank sig n).
290 definition R_move_to_blank_L ≝ λsig,n,i,t1,t2.
291 (current ? t1 = None ? →
292 t2 = midtape (multi_sig sig n) (left ? t1) (all_blank …) (right ? t1)) ∧
293 ∀ls,a,rs.t1 = midtape ? ls a rs →
294 ((no_blank sig n i a = false) ∧ t2 = t1) ∨
296 (no_blank sig n i b = false) ∧
297 (∀j.j ≤n → to_blank_i ?? j (ls1@b::ls2) = to_blank_i ?? j ls) ∧
298 t2 = midtape ? ls2 b ((reverse ? (a::ls1))@rs)).
300 definition R_move_to_blank_L_new ≝ λsig,n,i,t1,t2.
301 (current ? t1 = None ? →
302 t2 = midtape (multi_sig sig n) (left ? t1) (all_blank …) (right ? t1)) ∧
303 ∀ls,a,rs.t1 = midtape ? ls a rs →
305 (no_blank sig n i b = false) ∧
306 (hd ? (ls1@[b]) (all_blank …) = a) ∧ (* not implied by the next fact *)
307 (∀j.j ≤n → to_blank_i ?? j (ls1@b::ls2) = to_blank_i ?? j (a::ls)) ∧
308 t2 = midtape ? ls2 b ((reverse ? ls1)@rs)).
310 theorem sem_move_to_blank_L: ∀sig,n,i.
311 move_to_blank_L sig n i ⊨ R_move_to_blank_L sig n i.
314 (ssem_move_until_L ? (no_blank sig n i)) (sem_extend ? (all_blank sig n)))
315 #tin #tout * #t1 * * #Ht1a #Ht1b * #Ht2a #Ht2b %
316 [#Hcur >(Ht1a Hcur) in Ht2a; /2 by /
317 |#ls #a #rs #Htin -Ht1a cases (Ht1b … Htin)
318 [* #Hnb #Ht1 -Ht1b -Ht2a >Ht1 in Ht2b; >Htin #H %1
319 % [//|@H normalize % #H1 destruct (H1)]
321 [(* we find the blank *)
322 * #ls1 * #b * #ls2 * * * #H1 #H2 #H3 #H4 %2
325 |-Ht1b -Ht2a >H4 in Ht2b; #H5 @H5
326 % normalize #H6 destruct (H6)
328 |* #b * #lss * * #H1 #H2 #H3 %2
329 %{(all_blank …)} %{ls} %{[ ]}
330 %[%[whd in match (no_blank ????); >blank_all_blank // @daemon
331 |@daemon (* make a lemma *)]
332 |-Ht1b -Ht2b >H3 in Ht2a;
333 whd in match (left ??); whd in match (right ??); #H4
334 >H2 >reverse_append >reverse_single @H4 normalize //
340 theorem sem_move_to_blank_L_new: ∀sig,n,i.
341 move_to_blank_L sig n i ⊨ R_move_to_blank_L_new sig n i.
343 @(Realize_to_Realize … (sem_move_to_blank_L sig n i))
344 #t1 #t2 * #H1 #H2 % [@H1]
345 #ls #a #rs #Ht1 lapply (H2 ls a rs Ht1) -H2 *
346 [* #Ha #Ht2 >Ht2 %{a} %{[ ]} %{ls}
347 %[%[%[@Ha| //]| normalize //] | @Ht1]
348 |* #b * #ls1 * #ls2 * * * #Hblank #Ht2
349 %{b} %{(a::ls1)} %{ls2}
351 #j #lejn whd in match (to_blank_i ????);
352 whd in match (to_blank_i ???(a::ls));
353 lapply (Hblank j lejn) whd in match (to_blank_i ????);
354 whd in match (to_blank_i ???(a::ls)); #H >H %
358 (******************************************************************************)
360 definition shift_i_L ≝ λsig,n,i.
361 ncombf_r (multi_sig …) (shift_i sig n i) (all_blank sig n) ·
363 extend ? (all_blank sig n).
365 definition R_shift_i_L ≝ λsig,n,i,t1,t2.
366 (* ∀b:multi_sig sig n.∀ls.
367 (t1 = midtape ? ls b [ ] →
368 t2 = midtape (multi_sig sig n)
369 ((shift_i sig n i b (all_blank sig n))::ls) (all_blank sig n) [ ]) ∧ *)
371 t1 = midtape ? ls a rs →
374 nth i ? (vec … b) (blank ?) = (blank ?) ∧
375 (∀x. mem ? x rs1 → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
376 shift_l sig n i (a::rs1) (a1::rss) ∧
377 t2 = midtape (multi_sig sig n) ((reverse ? (a1::rss))@ls) b rs2) ∨
379 (∀x. mem ? x rs → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
380 shift_l sig n i (a::rs) (rss@[b]) ∧
381 t2 = midtape (multi_sig sig n)
382 ((reverse ? (rss@[b]))@ls) (all_blank sig n) [ ]))).
384 definition R_shift_i_L_new ≝ λsig,n,i,t1,t2.
386 t1 = midtape ? ls a rs →
388 b = hd ? rs2 (all_blank sig n) ∧
389 nth i ? (vec … b) (blank ?) = (blank ?) ∧
391 (∀x. mem ? x rs1 → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
392 shift_l sig n i (a::rs1) rss ∧
393 t2 = midtape (multi_sig sig n) ((reverse ? rss)@ls) b (tail ? rs2)).
395 theorem sem_shift_i_L: ∀sig,n,i. shift_i_L sig n i ⊨ R_shift_i_L sig n i.
398 (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
399 (sem_seq ????? (ssem_mti sig n i)
400 (sem_extend ? (all_blank sig n))))
401 #tin #tout * #t1 * * #Ht1a #Ht1b * #t2 * * #Ht2a #Ht2b * #Htout1 #Htout2
403 [#Htin lapply (Ht1a … Htin) -Ht1a -Ht1b #Ht1
404 lapply (Ht2a … Ht1) -Ht2a -Ht2b #Ht2 >Ht2 in Htout1;
405 >Ht1 whd in match (left ??); whd in match (right ??); #Htout @Htout // *)
407 [#Htin %2 %{(shift_i sig n i a (all_blank sig n))} %{[ ]}
408 %[%[#x @False_ind | @daemon]
409 |lapply (Ht1a … Htin) -Ht1a -Ht1b #Ht1
410 lapply (Ht2a … Ht1) -Ht2a -Ht2b #Ht2 >Ht2 in Htout1;
411 >Ht1 whd in match (left ??); whd in match (right ??); #Htout @Htout //
414 lapply (Ht1b … Htin) -Ht1a -Ht1b #Ht1
415 lapply (Ht2b … Ht1) -Ht2a -Ht2b *
416 [(* a1 is blank *) * #H1 #H2 %1
417 %{[ ]} %{a1} %{rs1} %{(shift_i sig n i a a1)} %{[ ]}
418 %[%[%[%[// |//] |#x @False_ind] | @daemon]
419 |>Htout2 [>H2 >reverse_single @Ht1 |>H2 >Ht1 normalize % #H destruct (H)]
422 [* #rs10 * #b * #rs2 * #rss * * * * #H1 #H2 #H3 #H4
424 %{(a1::rs10)} %{b} %{rs2} %{(shift_i sig n i a a1)} %{rss}
425 %[%[%[%[>H1 //|//] |@H3] |@daemon ]
426 |>reverse_cons >associative_append
427 >H2 in Htout2; #Htout >Htout [@Ht2| >Ht2 normalize % #H destruct (H)]
429 |* #b * #rss * * #H1 #H2
431 %{(shift_i sig n i b (all_blank sig n))} %{(shift_i sig n i a a1::rss)}
433 |>Ht2 in Htout1; #Htout >Htout //
434 whd in match (left ??); whd in match (right ??);
435 >reverse_append >reverse_single >associative_append >reverse_cons
436 >associative_append //
443 theorem sem_shift_i_L_new: ∀sig,n,i.
444 shift_i_L sig n i ⊨ R_shift_i_L_new sig n i.
446 @(Realize_to_Realize … (sem_shift_i_L sig n i))
447 #t1 #t2 #H #a #ls #rs #Ht1 lapply (H a ls rs Ht1) *
448 [* #rs1 * #b * #rs2 * #a1 * #rss * * * * #H1 #H2 #H3 #H4 #Ht2
449 %{rs1} %{b} %{(b::rs2)} %{(a1::rss)}
450 %[%[%[%[%[//|@H2]|@H1]|@H3]|@H4] | whd in match (tail ??); @Ht2]
451 |* #b * #rss * * #H1 #H2 #Ht2
452 %{rs} %{(all_blank sig n)} %{[]} %{(rss@[b])}
453 %[%[%[%[%[//|@blank_all_blank]|//]|@H1]|@H2] | whd in match (tail ??); @Ht2]
458 (******************************************************************************)
459 definition no_head_in ≝ λsig,n,l.
460 ∀x. mem ? x (trace sig n n l) → x ≠ head ?.
462 lemma no_head_true: ∀sig,n,a.
463 nth n ? (vec … n a) (blank sig) ≠ head ? → no_head … a = true.
464 #sig #n #a normalize cases (nth n ? (vec … n a) (blank sig))
465 normalize // * normalize // * #H @False_ind @H //
468 lemma no_head_false: ∀sig,n,a.
469 nth n ? (vec … n a) (blank sig) = head ? → no_head … a = false.
470 #sig #n #a #H normalize >H //
473 definition mtiL ≝ λsig,n,i.
474 move_to_blank_L sig n i ·
476 move_until ? L (no_head sig n).
478 definition Rmtil ≝ λsig,n,i,t1,t2.
480 t1 = midtape (multi_sig sig n) ls a rs →
481 nth n ? (vec … a) (blank ?) = head ? →
485 t2 = midtape (multi_sig …) ls1 a1 rs1 ∧
486 (∀j. j ≤ n → j ≠ i → to_blank_i ? n j (a1::ls1) = to_blank_i ? n j (a::ls)) ∧
487 (∀j. j ≤ n → j ≠ i → to_blank_i ? n j rs1 = to_blank_i ? n j rs) ∧
488 (to_blank_i ? n i ls1 = to_blank_i ? n i (a::ls)) ∧
489 (to_blank_i ? n i (a1::rs1)) = to_blank_i ? n i rs).
491 lemma reverse_map: ∀A,B,f,l.
492 reverse B (map … f l) = map … f (reverse A l).
493 #A #B #f #l elim l //
494 #a #l #Hind >reverse_cons >reverse_cons <map_append >Hind //
497 theorem sem_Rmtil: ∀sig,n,i. i < n → mtiL sig n i ⊨ Rmtil sig n i.
500 (sem_move_to_blank_L_new … )
501 (sem_seq ????? (sem_shift_i_L_new …)
502 (ssem_move_until_L ? (no_head sig n))))
503 #tin #tout * #t1 * * #_ #Ht1 * #t2 * #Ht2 * #_ #Htout
504 (* we start looking into Rmitl *)
505 #ls #a #rs #Htin (* tin is a midtape *)
506 #Hhead #Hnohead_ls #Hnohead_rs
507 lapply (Ht1 … Htin) -Ht1 -Htin
508 * #b * #ls1 * #ls2 * * * #Hno_blankb #Hhead #Hls1 #Ht1
509 lapply (Ht2 … Ht1) -Ht2 -Ht1
510 * #rs1 * #b0 * #rs2 * #rss * * * * * #Hb0 #Hb0blank #Hrs1 #Hrs1b #Hrss #Ht2
511 (* we need to recover the position of the head of the emulated machine
512 that is the head of ls1. This is somewhere inside rs1 *)
513 cut (∃rs11. rs1 = (reverse ? ls1)@rs11)
514 [cut (ls1 = [ ] ∨ ∃aa,tlls1. ls1 = aa::tlls1)
515 [cases ls1 [%1 // | #aa #tlls1 %2 %{aa} %{tlls1} //]] *
516 [#H1ls1 %{rs1} >H1ls1 //
517 |* #aa * #tlls1 #H1ls1 >H1ls1 in Hrs1;
518 cut (aa = a) [>H1ls1 in Hls1; #H @(to_blank_hd … H)] #eqaa >eqaa
519 #Hrs1_aux cases (compare_append … (sym_eq … Hrs1_aux)) #l *
521 |(* this is absurd : if l is empty, the case is as before.
522 if l is not empty then it must start with a blank, since it is the
523 frist character in rs2. But in this case we would have a blank
524 inside ls1=attls1 that is absurd *)
528 lapply (Htout … Ht2) -Htout -Ht2 *
529 [(* the current character on trace i hold the head-mark.
530 The case is absurd, since b0 is the head of rs2, that is a sublist of rs,
531 and the head-mark is not in rs *)
533 (* something is missing
534 * #H @False_ind @(absurd ? H) @eqnot_to_noteq whd in ⊢ (???%);
535 cut (rs2 = [ ] ∨ ∃c,rs21. rs2 = c::rs21)
536 [cases rs2 [ %1 // | #c #rs22 %2 %{c} %{rs22} //]]
537 * (* by cases on rs2 *)
538 [#Hrs2 >Hb0 >Hrs2 normalize >all_blank_n //
539 |* #c * #rs22 #Hrs2 destruct (Hrs2) @no_head_true @Hnohead_rs
542 [(* we reach the head position *)
543 (* cut (trace sig n j (a1::ls20)=trace sig n j (ls1@b::ls2)) *)
544 * #ls10 * #a1 * #ls20 * * * #Hls20 #Ha1 #Hnh #Htout
546 trace sig n j (reverse (multi_sig sig n) rs1@b::ls2) =
547 trace sig n j (ls10@a1::ls20))
548 [#j #ineqj >append_cons <reverse_cons >trace_def <map_append <reverse_map
549 lapply (trace_shift_neq …lt_in ? (sym_not_eq … ineqj) … Hrss) [//] #Htr
550 <(trace_def … (b::rs1)) <Htr >reverse_map >map_append @eq_f @Hls20 ]
552 cut (trace sig n i (reverse (multi_sig sig n) (rs1@[b0])@ls2) =
553 trace sig n i (ls10@a1::ls20))
554 [>trace_def <map_append <reverse_map <map_append <(trace_def … [b0])
555 cut (trace sig n i [b0] = [blank ?]) [@daemon] #Hcut >Hcut
556 lapply (trace_shift … lt_in … Hrss) [//] whd in match (tail ??); #Htr <Htr
557 >reverse_map >map_append <trace_def <Hls20 %
561 (trace sig n j (reverse (multi_sig sig n) rs11) = trace sig n j ls10) ∧
562 (trace sig n j (ls1@b::ls2) = trace sig n j (a1::ls20)))
564 #j #ineqj @(first_P_to_eq ? (λx. x ≠ head ?))
565 [lapply (Htracej … ineqj) >trace_def in ⊢ (%→?); <map_append
566 >trace_def in ⊢ (%→?); <map_append #H @H
568 cut ((trace sig n i (b0::reverse ? rs11) = trace sig n i (ls10@[a1])) ∧
569 (trace sig n i (ls1@ls2) = trace sig n i ls20))
570 [>H1 in Htracei; >reverse_append >reverse_single >reverse_append
571 >reverse_reverse >associative_append >associative_append
574 %{ls20} %{a1} %{(reverse ? (b0::ls10)@tail (multi_sig sig n) rs2)}
576 |#j #lejn #jneqi <(Hls1 … lejn)
577 >to_blank_i_def >to_blank_i_def @eq_f @sym_eq @(proj2 … (H2 j jneqi))]
578 |#j #lejn #jneqi >reverse_cons >associative_append >Hb0
579 <to_blank_hd_cons >to_blank_i_def >to_blank_i_def @eq_f
580 @(injective_append_l … (trace sig n j (reverse ? ls1))) (* >trace_def >trace_def *)
581 >map_append >map_append >Hrs1 >H1 >associative_append
582 <map_append <map_append in ⊢ (???%); @eq_f
583 <map_append <map_append @eq_f2 // @sym_eq
584 <(reverse_reverse … rs11) <reverse_map <reverse_map in ⊢ (???%);
585 @eq_f @(proj1 … (H2 j jneqi))]
586 |<(Hls1 i) [2:@lt_to_le //] (* manca un invariante: dopo un blank
587 posso avere solo blank *) @daemon ]
588 |>reverse_cons >associative_append
589 cut (to_blank_i sig n i rs = to_blank_i sig n i (rs11@[b0])) [@daemon]
590 #Hcut >Hcut >(to_blank_i_chop … b0 (a1::reverse …ls10)) [2: @Hb0blank]
591 >to_blank_i_def >to_blank_i_def @eq_f
592 >trace_def >trace_def @injective_reverse >reverse_map >reverse_cons
593 >reverse_reverse >reverse_map >reverse_append >reverse_single @sym_eq
596 |(*we do not find the head: this is absurd *)
597 * #b1 * #lss * * #H2 @False_ind
598 cut (∀x0. mem ? x0 (trace sig n n (b0::reverse ? rss@ls2)) → x0 ≠ head ?)
600 lapply (trace_shift_neq sig n i n … lt_in … Hrss)
601 [@lt_to_not_eq @lt_in | // ]
603 (nth n ? (vec … (hd ? (ls1@[b]) (all_blank sig n))) (blank ?) = head ?))
605 |@H2 >trace_def %2 <map_append @mem_append_l1 <reverse_map <trace_def
606 >H3 >H1 >trace_def >reverse_map >reverse_cons >reverse_append
607 >reverse_reverse >associative_append <map_append @mem_append_l2
608 cases ls1 [%1 % |#x #ll %1 %]
617 trace sig n j (reverse (multi_sig sig n) rss@ls2) =
618 trace sig n j (ls10@a1::ls20))
619 [#j #ineqj >trace_def <map_append in ⊢ (??%?);
620 <reverse_map lapply (trace_shift_neq …lt_in ? ineqj … Hrss) [//] #Htr
621 <trace_def <trace_def >Htr >reverse_cons *)
623 %{ls20} %{a1} %{(reverse ? (b0::ls10)@tail (multi_sig sig n) rs2)}
625 |#j #lejn #jneqi <(Hls1 … lejn) -Hls1
626 >to_blank_i_def >to_blank_i_def @eq_f
627 @(injective_append_l … (trace sig n j (reverse ? rs))) (* >trace_def >trace_def *)
628 >map_append >map_append
637 [(* the current character on trace i is blank *)
638 * #Hblank #Ht1 <Ht1 in Htin; #Ht1a >Ht1a in Ht2;
639 #Ht2 lapply (Ht2 … (refl …)) *
640 [(* we reach the margin of the i-th trace *)
641 * #rs1 * #b * #rs2 * #a1 * #rss * * * * #H1 #H2 #H3 #H4 #Ht2
642 lapply (Htout … Ht2) -Htout *
643 [(* the head is on b: this is absurd *)
644 * #Hhb @False_ind >Hnohead_rs in Hhb;
645 [#H destruct (H) | >H1 @mem_append_l2 %1 //]
647 [(* we reach the head position *)
648 * #ls1 * #b0 * #ls2 * * * #H5 #H6 #H7 #Htout
649 %{ls2} %{b0} %{(reverse ? (b::ls1)@rs2)}
651 [@daemon (* da finire
652 lapply H5 lapply H4 -H5 -H4 cases rss
653 [* normalize in ⊢ (%→?); #H destruct (H)
654 |#rssa #rsstl #H >reverse_cons >associative_append
655 normalize in ⊢ (??(???%)%→?); #H8 @sym_eq
656 @(first_P_to_eq (multi_sig sig n)
657 (λa.nth n (sig_ext sig) (vec … a) (blank ?) = head ?) ?????? H8)
660 %[%[%[%[%[@Htout|>Hls //]
661 | #j #lejn #neji >to_blank_i_def >to_blank_i_def
662 @eq_f >H1 >trace_def >trace_def >reverse_cons
663 >associative_append <map_append <map_append in ⊢ (???%); @eq_f2 //
666 |* #H @False_ind @H @daemon
670 |(* we do not find the head: absurd *)
671 cut (nth n (sig_ext sig) (vec … a1) (blank sig)=head sig)
672 [lapply (trace_shift_neq ??? n … lt_in … H4)
673 [@lt_to_not_eq // |//]
674 whd in match (trace ????); whd in match (trace ???(a::rs1));
675 #H <Hhead @(cons_injective_l … H)]
676 #Hcut * #b0 * #lss * * #H @False_ind
677 @(absurd (true=false)) [2://] <(H a1)
678 [whd in match (no_head ???); >Hcut //
679 |%2 @mem_append_l1 >reverse_cons @mem_append_l2 %1 //
683 theorem sem_Rmtil: ∀sig,n,i. i < n → mtiL sig n i ⊨ Rmtil sig n i.
686 (sem_move_to_blank_L … )
687 (sem_seq ????? (sem_shift_i_L …)
688 (ssem_move_until_L ? (no_head sig n))))
689 #tin #tout * #t1 * * #_ #Ht1 * #t2 * #Ht2 * #_ #Htout
690 (* we start looking into Rmitl *)
691 #ls #a #rs #Htin (* tin is a midtape *)
692 #Hhead #Hnohead_ls #Hnohead_rs
693 cases (Ht1 … Htin) -Ht1
694 [(* the current character on trace i is blank *)
695 * #Hblank #Ht1 <Ht1 in Htin; #Ht1a >Ht1a in Ht2;
696 #Ht2 lapply (Ht2 … (refl …)) *
697 [(* we reach the margin of the i-th trace *)
698 * #rs1 * #b * #rs2 * #a1 * #rss * * * * #H1 #H2 #H3 #H4 #Ht2
699 lapply (Htout … Ht2) -Htout *
700 [(* the head is on b: this is absurd *)
701 * #Hhb @False_ind >Hnohead_rs in Hhb;
702 [#H destruct (H) | >H1 @mem_append_l2 %1 //]
704 [(* we reach the head position *)
705 * #ls1 * #b0 * #ls2 * * * #H5 #H6 #H7 #Htout
706 %{ls2} %{b0} %{(reverse ? (b::ls1)@rs2)}
708 [@daemon (* da finire
709 lapply H5 lapply H4 -H5 -H4 cases rss
710 [* normalize in ⊢ (%→?); #H destruct (H)
711 |#rssa #rsstl #H >reverse_cons >associative_append
712 normalize in ⊢ (??(???%)%→?); #H8 @sym_eq
713 @(first_P_to_eq (multi_sig sig n)
714 (λa.nth n (sig_ext sig) (vec … a) (blank ?) = head ?) ?????? H8)
717 %[%[%[%[%[@Htout|>Hls //]
718 | #j #lejn #neji >to_blank_i_def >to_blank_i_def
719 @eq_f >H1 >trace_def >trace_def >reverse_cons
720 >associative_append <map_append <map_append in ⊢ (???%); @eq_f2 //
723 |* #H @False_ind @H @daemon
727 |(* we do not find the head: absurd *)
728 cut (nth n (sig_ext sig) (vec … a1) (blank sig)=head sig)
729 [lapply (trace_shift_neq ??? n … lt_in … H4)
730 [@lt_to_not_eq // |//]
731 whd in match (trace ????); whd in match (trace ???(a::rs1));
732 #H <Hhead @(cons_injective_l … H)]
733 #Hcut * #b0 * #lss * * #H @False_ind
734 @(absurd (true=false)) [2://] <(H a1)
735 [whd in match (no_head ???); >Hcut //
736 |%2 @mem_append_l1 >reverse_cons @mem_append_l2 %1 //
741 theorem sem_Rmtil: ∀sig,n,i. mtiL sig n i ⊨ Rmtil sig n i.
744 (ssem_move_until_L ? (no_blank sig n i))
745 (sem_seq ????? (sem_extend ? (all_blank sig n))
746 (sem_seq ????? (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
747 (sem_seq ????? (ssem_mti sig n i)
748 (sem_seq ????? (sem_extend ? (all_blank sig n))
749 (ssem_move_until_L ? (no_head sig n)))))))
750 #tin #tout * #t1 * * #_ #Ht1 * #t2 * * #Ht2a #Ht2b * #t3 * * #Ht3a #Ht3b
751 * #t4 * * #Ht4a #Ht4b * #t5 * * #Ht5a #Ht5b * #t6 #Htout
752 (* we start looking into Rmitl *)
753 #ls #a #rs #Htin (* tin is a midtape *)
754 #Hhead #Hnohead_ls #Hnohead_rs
755 cases (Ht1 … Htin) -Ht1
756 [(* the current character on trace i is blank *)
757 -Ht2a * #Hblank #Ht1 <Ht1 in Htin; #Ht1a >Ht1a in Ht2b;
758 #Ht2b lapply (Ht2b ?) [% normalize #H destruct] -Ht2b -Ht1 -Ht1a
759 lapply Hnohead_rs -Hnohead_rs
760 (* by cases on rs *) cases rs
761 [#_ (* rs is empty *) #Ht2 -Ht3b lapply (Ht3a … Ht2)
762 #Ht3 -Ht4b lapply (Ht4a … Ht3) -Ht4a #Ht4 -Ht5b
763 >Ht4 in Ht5a; >Ht3 #Ht5a lapply (Ht5a (refl … )) -Ht5a #Ht5
764 cases (Htout … Ht5) -Htout
765 [(* the current symbol on trace n is the head: this is absurd *)
766 * whd in ⊢ (??%?→?); >all_blank_n whd in ⊢ (??%?→?); #H destruct (H)
768 [(* we return to the head *)
769 * #ls1 * #b * #ls2 * * * whd in ⊢ (??%?→?);
771 (* ls1 must be empty *)
773 [lapply H3 lapply H1 -H3 -H1 cases ls1 // #c #ls3
774 whd in ⊢ (???%→?); #H1 destruct (H1)
775 >blank_all_blank [|@daemon] #H @False_ind
776 lapply (H … (change_vec (sig_ext sig) n a (blank sig) i) ?)
777 [%2 %1 // | whd in match (no_head ???); >nth_change_vec_neq [|@daemon]
778 >Hhead whd in ⊢ (??%?→?); #H1 destruct (H1)]]
779 #Hls1_nil >Hls1_nil in H1; whd in ⊢ (???%→?); #H destruct (H)
780 >reverse_single >blank_all_blank [|@daemon]
781 whd in match (right ??) ; >append_nil #Htout
782 %{ls2} %{(change_vec (sig_ext sig) n a (blank sig) i)} %{[all_blank sig n]}
783 %[%[%[%[%[//|//]|@daemon]|//] |(*absurd*)@daemon]
784 |normalize >nth_change_vec // @daemon]
785 |(* we do not find the head: this is absurd *)
786 * #b * #lss * * whd in match (left ??); #HF @False_ind
787 lapply (HF … (shift_i sig n i a (all_blank sig n)) ?) [%2 %1 //]
788 whd in match (no_head ???); >nth_change_vec_neq [|@daemon]
789 >Hhead whd in ⊢ (??%?→?); #H destruct (H)
793 #c #rs1 #Hnohead_rs #Ht2 -Ht3a lapply (Ht3b … Ht2) -Ht3b
794 #Ht3 -Ht4a lapply (Ht4b … Ht3) -Ht4b *
795 [(* the first character is blank *) *
796 #Hblank #Ht4 -Ht5a >Ht4 in Ht5b; >Ht3
797 normalize in ⊢ ((%→?)→?); #Ht5 lapply (Ht5 ?) [% #H destruct (H)]
798 -Ht2 -Ht3 -Ht4 -Ht5 #Ht5 cases (Htout … Ht5) -Htout
799 [(* the current symbol on trace n is the head: this is absurd *)
800 * >Hnohead_rs [#H destruct (H) |%1 //]
802 [(* we return to the head *)
803 * #ls1 * #b * #ls2 * * * whd in ⊢ (??%?→?);
805 (* ls1 must be empty *)
807 [lapply H3 lapply H1 -H3 -H1 cases ls1 // #x #ls3
808 whd in ⊢ (???%→?); #H1 destruct (H1) #H @False_ind
809 lapply (H (change_vec (sig_ext sig) n a (nth i (sig_ext sig) (vec … c) (blank sig)) i) ?)
810 [%2 %1 // | whd in match (no_head ???); >nth_change_vec_neq [|@daemon]
811 >Hhead whd in ⊢ (??%?→?); #H1 destruct (H1)]]
812 #Hls1_nil >Hls1_nil in H1; whd in ⊢ (???%→?); #H destruct (H)
813 >reverse_single #Htout
814 %{ls2} %{(change_vec (sig_ext sig) n a (nth i (sig_ext sig) (vec … c) (blank sig)) i)}
816 %[%[%[%[%[@Htout|//]|//]|//] |(*absurd*)@daemon]
818 [>(to_blank_cons_b … Hblank) //| >nth_change_vec [@Hblank |@daemon]]
820 |(* we do not find the head: this is absurd *)
821 * #b * #lss * * #HF @False_ind
822 lapply (HF … (shift_i sig n i a c) ?) [%2 %1 //]
823 whd in match (no_head ???); >nth_change_vec_neq [|@daemon]
824 >Hhead whd in ⊢ (??%?→?); #H destruct (H)
829 (* end of the first case !! *)
835 cut (∃rs11,rs12. b::rs1 = rs11@a::rs12 ∧ no_head_in ?? rs11)
836 [cut (ls1 = [ ] ∨ ∃aa,tlls1. ls1 = aa::tlls1)
837 [cases ls1 [%1 // | #aa #tlls1 %2 %{aa} %{tlls1} //]] *
838 [#H1ls1 %{[ ]} %{rs1} %
839 [ @eq_f2 // >H1ls1 in Hls1; whd in match ([]@b::ls2);
840 #Hls1 @(to_blank_hd … Hls1)
841 |normalize #x @False_ind
843 |* #aa * #tlls1 #H1ls1 >H1ls1 in Hrs1;
844 cut (aa = a) [>H1ls1 in Hls1; #H @(to_blank_hd … H)] #eqaa >eqaa
845 #Hrs1_aux cases (compare_append … (sym_eq … Hrs1_aux)) #l *
846 [* #H1 #H2 %{(b::(reverse ? tlls1))} %{l} %
847 [@eq_f >H1 >reverse_cons >associative_append //
848 |@daemon (* is a sublit of the tail of ls1, and hence of ls *)
850 |(* this is absurd : if l is empty, the case is as before.
851 if l is not empty then it must start with a blank, since it is the
852 frist character in rs2. But in this case we would have a blank
853 inside ls1=attls1 that is absurd *)