1 (* include "turing/auxiliary_machines.ma". *)
3 include "turing/multi_to_mono/shift_trace.ma".
5 (******************************************************************************)
7 (* exec_move_R : before shifting the trace left - to simulate a right move of
8 the head - we must be sure we are not in rightoverflow, that is that the symbol
9 at the right of the head, if any, is not blank *)
11 (* a simple look-ahead machine *)
12 definition mtestR ≝ λsig,test.
14 (ifTM ? (test_char ? test)
15 (single_finalTM ? (move sig L))
16 (move sig L) tc_true).
19 definition RmtestR_true ≝ λsig,test.λt1,t2.
21 t1 = midtape sig ls c rs →
22 ∃c1,rs1. rs = c1::rs1 ∧ t1 = t2 ∧ (test c1 = true).
24 definition RmtestR_false ≝ λsig,test.λt1,t2.
26 t1 = midtape sig ls c (c1::rs) →
27 t1 = t2 ∧ (test c1 = false)) ∧
29 t1 = midtape sig ls c [] → t1 = t2).
31 definition mtestR_acc: ∀sig,test.states ? (mtestR sig test).
32 #sig #test @inr @inr @inl @inr @start_nop
35 lemma sem_mtestR: ∀sig,test.
38 RmtestR_true sig test, RmtestR_false sig test].
40 @(acc_sem_seq_app sig … (sem_move_single … )
42 (sem_test_char sig test)
44 (sem_move_single … )))
45 [#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in ⊢ (%→?); * *
46 #cx * #Hcx #H1cx #Htx #Ht2 #ls #c #rs #Ht1
47 >Ht1 in Hmove; cases rs
48 [#H >H in Hcx; whd in ⊢ (??%?→?); #H1 destruct (H1)
49 |#c1 #rs1 #Ht3 %{c1} %{rs1} %
50 [% [//|>Htx in Ht2; >Ht3 whd in ⊢ (%→?); #H @sym_eq @H ]
51 |>Ht3 in Hcx; whd in ⊢ (??%?→?); #H1 destruct (H1) //
54 |#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in ⊢ (%→?); *
57 >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
58 >Ht3 in Hcx; #Hcx lapply (Hcx ? (refl ??))
59 #Htest % // >Heqtx in Htx; >Ht3 whd in ⊢ (%→?); #H @sym_eq @H
60 |#ls0 #c0 #Ht1 >Ht1 in Hmove; whd in match (tape_move ???);
61 <Heqtx #H1tx >H1tx in Htx; #H @sym_eq @H
66 definition guarded_M ≝ λsig,n,i,M.
67 (ifTM ? (test_char ? (not_blank sig n i))
69 (ifTM ? (mtestR ? (not_blank sig n i))
71 (nop ?) (mtestR_acc …)) tc_true).
73 definition R_guarded_M ≝ λsig,n,i,RM,t1,t2.
74 ∀ls,a,rs. t1 = midtape ? ls a rs →
75 (not_blank sig n i a = false →
76 not_blank sig n i (hd ? rs (all_blanks …)) = false → t1=t2) ∧
77 (not_blank sig n i a = true ∨
78 not_blank sig n i (hd ? rs (all_blanks …)) = true → RM t1 t2).
80 lemma sem_R_guarded: ∀sig,n,i,M,RM. M ⊨ RM →
81 guarded_M sig n i M ⊨ R_guarded_M sig n i RM.
83 @(sem_if_app … (sem_test_char … ) HM
84 (sem_if … (sem_mtestR … ) HM (sem_nop ?)))
86 [* * * #c * #Hc #H1c #Ht1 #Htout #ls #a #rs #Htin
87 >Htin in Hc; normalize in ⊢ (%→?); #H1 destruct (H1) %
88 [>H1c #H2 @False_ind destruct (H2)
89 |#H1 <Htin <Ht1 @Htout
91 |* * #Hc #Ht1 #H #ls #a #rs lapply (Hc a) <Ht1 -Ht1 #Ha #Ht1
93 [* #t2 * #Ht2 lapply (Ht2 … Ht1)
94 * #c1 * #rs1 * * #H1 #H2 #H3 #H4 % [2: //]
95 #Ha >H1 whd in match (hd ???); >H3 #H destruct (H)
96 |lapply Ht1 -Ht1 cases rs
97 [#Ht1 * #t2 * * #_ #Ht2 lapply (Ht2 … Ht1) -Ht2 #Ht2
98 whd in ⊢ (%→?); #Htout % [//] *
99 [>Ha [#H destruct (H)| >Ht1 %]
100 |whd in ⊢ (??%?→?); >blank_all_blanks whd in ⊢ (??%?→?);
103 |#c #rs1 #Ht1 * #t2 * * #Ht2 #_ lapply (Ht2 … Ht1) -Ht2 *
104 #Ht2 whd in ⊢ (??%?→?); #Hnb whd in ⊢ (%→?); #Htout % [//] *
105 [>Ha [#H destruct (H)| >Ht1 %]
106 |whd in ⊢ (??%?→?); whd in match (hd ???); >Hnb whd in ⊢ (??%?→?);
114 definition move_R_i ≝ λA,sig,n,i.
115 guarded_M ? (S n) i (mtiL A sig n i).
117 definition Rmove_R_i ≝ λA,sig,n,i.
118 R_guarded_M ? (S n) i (Rmtil A sig n i).
120 (**************************** Vector Operations *******************************)
122 let rec resize A (l:list A) i d on i ≝
125 | S j ⇒ (hd ? l d)::resize A (tail ? l) j d
128 lemma length_resize : ∀A,l,i,d. |resize A l i d| = i.
129 #A #l #i lapply l -l elim i
132 [#d normalize @eq_f @Hind
133 |#a #tl #d normalize @eq_f @Hind
138 lemma resize_id : ∀A,n,l,d. |l| = n →
141 [#l #d #H >(lenght_to_nil … H) //
142 |#m #Hind * #d normalize
143 [#H destruct |#a #tl #H @eq_f @Hind @injective_S // ]
147 definition resize_vec :∀A,n.Vector A n → ∀i.A→Vector A i.
148 #A #n #a #i #d @(mk_Vector A i (resize A a i d) ) @length_resize
151 axiom nth_resize_vec :∀A,n.∀v:Vector A n.∀d,i,j. i < j →i < n →
152 nth i ? (resize_vec A n v j d) d = nth i ? v d.
154 lemma resize_vec_id : ∀A,n.∀v:Vector A n.∀d.
155 resize_vec A n v n d = v.
156 #A #n #v #d @(eq_vec … d) #i #ltin @nth_resize_vec //
159 definition vec_single: ∀A,a. Vector A 1 ≝ λA,a.
160 mk_Vector A 1 [a] (refl ??).
162 definition vec_cons_right : ∀A.∀a:A.∀n. Vector A n → Vector A (S n).
163 #A #a #n #v >(plus_n_O n) >plus_n_Sm @(vec_append … v (vec_single A a))
164 >length_append >(len A n v) //
167 lemma eq_cons_right : ∀A,a1,a2.∀n.∀v1,v2:Vector A n.
168 a1 = a2 → v1 = v2 → vec_cons_right A a1 n v1 = vec_cons_right A a2 n v2.
171 axiom nth_cons_right_n: ∀A.∀a:A.∀n.∀v:Vector A n.∀d.
172 nth n ? (vec_cons_right A a n v) d = a.
174 axiom nth_cons_right_lt: ∀A.∀a:A.∀n.∀v:Vector A n.∀d.∀i. i < n →
175 nth i ? (vec_cons_right A a n v) d = nth i ? v d.
178 [#v #d >(vector_nil … v) //
179 |#m #Hind #v #d >(vec_expand … v) whd in ⊢ (??%?);
180 whd in match (vec_cons_right ????);
183 axiom resize_cons_right: ∀A.∀a:A.∀n.∀v:Vector A n.∀d.
184 resize_vec ? (S n) (vec_cons_right A a n v) n d = v.
185 (*************************** readback of the tape *****************************)
187 definition opt_cur ≝ λsig,a.
188 if a == blank sig then None ? else Some ? a.
190 definition rb_trace ≝ λsig,ls,a,rs.
191 mk_tape ? (to_blank ? ls) (opt_cur sig a) (to_blank ? rs).
193 lemma rb_trace_def: ∀sig,ls,a,rs.
194 rb_trace sig ls a rs =
195 mk_tape ? (to_blank ? ls) (opt_cur sig a) (to_blank ? rs).
198 definition rb_trace_i ≝ λsig,n,ls,a,rs,i.
199 rb_trace sig (trace ? n i ls) (nth i ? a (blank ?)) (trace ? n i rs).
201 lemma rb_trace_i_def: ∀sig,n,ls,a,rs,i.
202 rb_trace_i sig n ls a rs i =
203 rb_trace sig (trace ? n i ls) (nth i ? a (blank ?)) (trace ? n i rs).
207 definition readback :∀sig,n,ls,a,rs,i.Vector (tape (sig_ext sig)) i ≝
208 vec_map (rb_trace_i *)
210 lemma orb_false_l: ∀b1,b2:bool.
211 (b1 ∨ b2) = false → (b1 = false) ∧ (b2 = false).
212 * * normalize /2/ qed.
214 lemma no_blank_true_to_not_blank: ∀sig,n,a,i.
215 (not_blank sig n i a = true) → nth i ? (vec … n a) (blank sig) ≠ blank ?.
216 #sig #n #a #i #H @(not_to_not … (eqnot_to_noteq … false H))
220 lemma rb_move_R : ∀A,sig,n,ls,a,rs,outt,i.
221 (∀i.regular_trace (TA A sig) (S n) a ls rs i) →
222 is_head ?? (nth n ? (vec … a) (blank ?)) = true →
225 Rmove_R_i … i (midtape ? ls a rs) outt →
227 outt = midtape ? ls1 a1 rs1 ∧
228 (∀i.regular_trace (TA A sig) (S n) a1 ls1 rs1 i) ∧
229 rb_trace_i ? (S n) ls1 (vec … a1) rs1 i =
230 tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs i) R ∧
232 rb_trace_i ? (S n) ls1 (vec … a1) rs1 j =
233 rb_trace_i ? (S n) ls (vec … a) rs j.
234 #A #sig #n #ls #a #rs #outt #i #Hreg #Hha #Hhls #Hhrs #Hmove
235 lapply (Hmove … (refl …)) -Hmove * #HMove1 #HMove2
236 cases (true_or_false (not_blank ? (S n) i a ∨
237 not_blank ? (S n) i (hd ? rs (all_blanks ? (S n)))))
238 [2: #Hcase cases (orb_false_l … Hcase) -Hcase #Hb1 #Hb2
239 lapply (HMove1 … Hb1 Hb2) #Hout %{ls} %{a} %{rs}
240 %[%[%[@sym_eq @Hout |@Hreg]
242 cut (nth i ? (vec … a) (blank ?) = blank ?)
243 [@(\P ?) @injective_notb @Hb1] #Ha >Ha
244 >rb_trace_def whd in match (opt_cur ??);
245 cut (to_blank ? (trace ? (S n) i rs) = [])
247 cases (to_blank ? (trace ? (S n) i ls)) //
251 lapply(HMove2 (orb_true_l … Hb) … (refl …) Hha Hreg ? Hhls Hhrs) -HMove2
252 [#Hb1 lapply Hb -Hb whd in match (not_blank ? (S n) i a);
253 >Hb1 #H @no_blank_true_to_not_blank @H]
254 * #ls1 * #a1 * #rs1 * * * * * #H1 #H2 #H3 #H4 #H5 #H6
257 |(* either a is blank or not *)
258 cases (true_or_false (not_blank ? (S n) i a)) #Hba
260 >rb_trace_i_def >rb_trace_def <to_blank_i_def >H5 >to_blank_cons_nb
261 [2: @no_blank_true_to_not_blank //]
262 lapply H6 -H6 #Hrs >(rb_trace_i_def … rs i) >rb_trace_def
263 <(to_blank_i_def … rs) <Hrs
264 cut (opt_cur ? (nth i ? (vec … a) (blank ?)) =
265 Some ? (nth i ? (vec … a) (blank ?))) [@daemon] #Ha >Ha
266 (* either a1 is blank or not *)
267 cases (true_or_false (not_blank ? (S n) i a1)) #Hba1
268 [cut (opt_cur ? (nth i ? (vec … a1) (blank ?)) =
269 Some ? (nth i ? (vec … a1) (blank ?))) [@daemon] #Ha1 >Ha1
270 >to_blank_cons_nb [%|@(\Pf ?) @injective_notb @Hba1]
271 |cut (opt_cur ? (nth i ? (vec … a1) (blank ?)) = None ?) [@daemon]
273 cut (to_blank_i … i (a1::rs1) = [ ]) [@daemon] #Ha1rs1 >Ha1rs1
274 cut (to_blank_i … i rs1 = [ ]) [@daemon] #Hrs1 <to_blank_i_def >Hrs1 %
276 |>rb_trace_i_def >rb_trace_def <to_blank_i_def (* >H5 >to_blank_cons_nb *)
277 >rb_trace_i_def >rb_trace_def <(to_blank_i_def … rs) <H6 >H5
278 cut (to_blank_i … i (a::ls) = [ ]) [@daemon] #Hals >Hals
279 cut (to_blank_i … i ls = [ ]) [@daemon] #Hls <(to_blank_i_def … ls) >Hls
280 cut (opt_cur ? (nth i ? (vec … a) (blank ?)) = None ?) [@daemon] #Ha >Ha
281 cut (nth i ? (vec … a1) (blank ?) ≠ blank ?) [@daemon] #Ha1
282 >(to_blank_cons_nb … Ha1)
283 cut (opt_cur ? (nth i ? (vec … a1) (blank ?)) =
284 Some ? (nth i ? (vec … a1) (blank ?))) [@daemon] -Ha1 #Ha1 >Ha1 %
288 #j #Hle #Hneq >rb_trace_i_def >rb_trace_i_def >rb_trace_def >rb_trace_def
289 <(to_blank_i_def … rs) <(to_blank_i_def … rs1) >(H4 j Hle Hneq)
290 cut ((to_blank_i ? (S n) j ls1 = to_blank_i ? (S n) j ls) ∧
291 (opt_cur ? (nth j ? (vec … a1) (blank ?)) =
292 opt_cur ? (nth j ? (vec … a) (blank ?))))
293 [@daemon] * #H7 #H8 <to_blank_i_def >H7 >H8 //
298 definition Rmove_R_i_rb ≝ λA,sig,n,i,t1,t2.
300 t1 = midtape ? ls a rs →
301 (∀i.regular_trace (TA A sig) (S n) a ls rs i) →
302 is_head ?? (nth n ? (vec … a) (blank ?)) = true →
306 t2 = midtape (MTA A sig (S n)) ls1 a1 rs1 ∧
307 (∀i.regular_trace (TA A sig) (S n) a1 ls1 rs1 i) ∧
308 rb_trace_i ? (S n) ls1 (vec … a1) rs1 i =
309 tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs i) R ∧
311 rb_trace_i ? (S n) ls1 (vec … a1) rs1 j =
312 rb_trace_i ? (S n) ls (vec … a) rs j.
314 lemma sem_move_R_i : ∀A,sig,n,i.i < n →
315 move_R_i A sig n i ⊨ Rmove_R_i_rb A sig n i.
316 #A #sig #n #i #ltin @(Realize_to_Realize … (Rmove_R_i A sig n i))
317 [#t1 #t2 #H #ls #a #rs #H1 #H2 #H3 #H4 #H5 @rb_move_R // <H1 //
318 |@sem_R_guarded @sem_Rmtil //
322 (* move_L_i axiomatized *)
324 axiom move_L_i : ∀A,sig.∀n,i:nat.TM (MTA A sig (S n)).
326 definition Rmove_L_i_rb ≝ λA,sig,n,i,t1,t2.
328 t1 = midtape ? ls a rs →
329 (∀i.regular_trace (TA A sig) (S n) a ls rs i) →
330 is_head ?? (nth n ? (vec … a) (blank ?)) = true →
334 t2 = midtape (MTA A sig (S n)) ls1 a1 rs1 ∧
335 (∀i.regular_trace ? (S n) a1 ls1 rs1 i) ∧
336 rb_trace_i ? (S n) ls1 (vec … a1) rs1 i =
337 tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs i) L ∧
339 rb_trace_i ? (S n) ls1 (vec … a1) rs1 j =
340 rb_trace_i ? (S n) ls (vec … a) rs j.
342 axiom sem_move_L_i : ∀A,sig,n,i.i < n →
343 move_L_i A sig n i ⊨ Rmove_L_i_rb A sig n i.
346 lemma rb_move_L : ∀sig,n,ls,a,rs,outt,i.
347 (∀i.regular_trace sig n a ls rs i) →
348 nth n ? (vec … a) (blank ?) = head ? →
351 Rmove_L_i … i (midtape ? ls a rs) outt →
353 outt = midtape ? ls1 a1 rs1 ∧
354 rb_trace_i sig n ls1 (vec … a1) rs1 i =
355 tape_move ? (rb_trace_i sig n ls (vec … a) rs i) L ∧
357 rb_trace_i sig n ls1 (vec … a1) rs1 j =
358 rb_trace_i sig n ls (vec … a) rs j. *)
360 (* The following function read a move from a vector of moves and executes it *)
362 (* The head character contains a state and a sequence of moves *)
364 definition HC ≝ λQ,n.FinProd Q (FinVector FinMove n).
366 let rec all_N n on n : FinVector FinMove n ≝
368 [ O ⇒ Vector_of_list ? []
369 | S m ⇒ vec_cons ? N m (all_N m)
372 definition get_moves ≝ λQ,sig,n.λa:MTA (HC Q n) sig (S n).
373 match nth n ? (vec … a) (blank ?) with
375 | Some x ⇒ match x with
379 definition get_move ≝ λQ,sig,n.λa:MTA (HC Q n) sig (S n).λi.
380 nth i ? (vec … (get_moves Q sig n a)) N.
382 lemma get_moves_cons_right: ∀Q,sig,n,q,moves,a.
383 get_moves Q sig (S n)
384 (vec_cons_right ? (Some ? (inl ?? 〈q,moves〉)) (S n) a) = moves.
385 #Q #sig #n #q #moves #a whd in ⊢(??%?); >nth_cons_right_n //
388 definition exec_move_i ≝ λQ,sig,n,i.
389 (ifTM ? (test_char ? (λa. (get_move Q sig n a i == R)))
390 (move_R_i (HC Q n) sig n i)
391 (ifTM ? (test_char ? (λa. (get_move Q sig n a i == L)))
392 (move_L_i (HC Q n) sig n i)
393 (nop ?) tc_true) tc_true).
395 definition R_exec_move_i ≝ λQ,sig,n,i,t1,t2.
397 t1 = midtape (MTA (HC Q n) sig (S n)) ls a rs →
398 (∀i.regular_trace ? (S n) a ls rs i) →
399 is_head ?? (nth n ? (vec … a) (blank ?)) = true →
403 t2 = midtape (MTA (HC Q n) sig (S n)) ls1 a1 rs1 ∧
404 (∀i.regular_trace ? (S n) a1 ls1 rs1 i) ∧
405 rb_trace_i ? (S n) ls1 (vec … a1) rs1 i =
406 tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs i) (get_move Q sig n a i) ∧
408 rb_trace_i ? (S n) ls1 (vec … a1) rs1 j =
409 rb_trace_i ? (S n) ls (vec … a) rs j.
411 lemma tape_move_N: ∀A,t. tape_move A t N = t.
414 lemma sem_exec_move_i: ∀Q,sig,n,i. i < n →
415 exec_move_i Q sig n i ⊨ R_exec_move_i Q sig n i.
417 @(sem_if_app … (sem_test_char …)
418 (sem_move_R_i … ltin)
419 (sem_if … (sem_test_char …)
420 (sem_move_L_i … ltin) (sem_nop ?)))
422 [* * * #c * #Hc #HR #Ht1 #HMR
423 #a #ls #rs #Htin >Htin in Hc; whd in ⊢ (??%?→?); #H destruct (H)
424 >(\P HR) whd in HMR; @HMR >Ht1 @Htin
426 [* #t2 * * * #c * #Hc #HL #Ht2 #HML
427 #a #ls #rs #Htin >Htin in Hc; whd in ⊢ (??%?→?); #H destruct (H)
428 >(\P HL) @HML >Ht2 @Htin
429 |* #t2 * * #HL #Ht2 >Ht2 whd in ⊢ (%→?); #Htout >Htout
430 #a #ls #rs #Htin >Htin in HR; #HR >Htin in HL; #HL
431 cut (get_move Q sig n a i = N)
432 [lapply (HR a (refl … )) lapply (HL a (refl … ))
433 cases (get_move Q sig n a i) normalize
434 [#H destruct (H) |#_ #H destruct (H) | //]]
435 #HN >HN >tape_move_N #Hreg #_ #_ #_
437 %[%[%[%|@Hreg] |%] | //]
442 axiom reg_inv : ∀A,sig,n,a,ls,rs,a1,ls1,rs1.
443 regular_trace (TA A sig) (S n) a1 ls1 rs1 n →
444 (rb_trace_i ? (S n) ls1 (vec … a1) rs1 n =
445 rb_trace_i ? (S n) ls (vec … a) rs n) →
446 is_head ?? (nth n ? (vec … (S n) a) (blank ?)) = true →
449 is_head ?? (nth n ? (vec … a1) (blank ?)) = true ∧
450 no_head_in … ls1 ∧ no_head_in … rs1.