2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_____________________________________________________________*)
17 include "turing/while_machine.ma".
19 (* ADVANCE TO MARK (right)
21 sposta la testina a destra fino a raggiungere il primo carattere marcato
25 (* 0, a ≠ mark _ ⇒ 0, R
26 0, a = mark _ ⇒ 1, N *)
28 definition atm_states ≝ initN 3.
30 definition atmr_step ≝
31 λalpha:FinSet.λtest:alpha→bool.
32 mk_TM alpha atm_states
39 | false ⇒ 〈2,Some ? 〈a',R〉〉 ]])
42 definition Ratmr_step_true ≝
45 t1 = midtape alpha ls a rs ∧ test a = false ∧
46 t2 = mk_tape alpha (a::ls) (option_hd ? rs) (tail ? rs).
48 definition Ratmr_step_false ≝
51 (current alpha t1 = None ? ∨
52 (∃a.current ? t1 = Some ? a ∧ test a = true)).
55 ∀alpha,test,ls,a0,rs. test a0 = true →
56 step alpha (atmr_step alpha test)
57 (mk_config ?? 0 (midtape … ls a0 rs)) =
58 mk_config alpha (states ? (atmr_step alpha test)) 1
60 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
64 ∀alpha,test,ls,a0,rs. test a0 = false →
65 step alpha (atmr_step alpha test)
66 (mk_config ?? 0 (midtape … ls a0 rs)) =
67 mk_config alpha (states ? (atmr_step alpha test)) 2
68 (mk_tape … (a0::ls) (option_hd ? rs) (tail ? rs)).
69 #alpha #test #ls #a0 #ts #Htest normalize >Htest cases ts //
74 accRealize alpha (atmr_step alpha test)
75 2 (Ratmr_step_true alpha test) (Ratmr_step_false alpha test).
78 @(ex_intro ?? (mk_config ?? 1 (niltape ?))) %
79 [ % // #Hfalse destruct | #_ % // % % ]
80 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (leftof ? a al)))
81 % [ % // #Hfalse destruct | #_ % // % % ]
82 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (rightof ? a al)))
83 % [ % // #Hfalse destruct | #_ % // % % ]
84 | #ls #c #rs @(ex_intro ?? 2)
85 cases (true_or_false (test c)) #Htest
86 [ @(ex_intro ?? (mk_config ?? 1 ?))
89 [ whd in ⊢ (??%?); >atmr_q0_q1 //
91 | #_ % // %2 @(ex_intro ?? c) % // ]
93 | @(ex_intro ?? (mk_config ?? 2 (mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs))))
96 [ whd in ⊢ (??%?); >atmr_q0_q2 //
97 | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
100 | #Hfalse @False_ind @(absurd ?? Hfalse) %
107 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
109 t1 = mk_tape alpha ls c rs →
110 (c = None ? ∧ t2 = t1) ∨
112 ((test c' = true ∧ t2 = t1) ∨
114 (((∀x.memb ? x rs = true → test x = false) ∧
115 t2 = mk_tape ? (reverse ? rs@c'::ls) (None ?) []) ∨
116 (∃rs1,b,rs2.rs = rs1@b::rs2 ∧
117 test b = true ∧ (∀x.memb ? x rs1 = true → test x = false) ∧
118 t2 = midtape ? (reverse ? rs1@c'::rs) b rs2))))).
120 definition adv_to_mark_r ≝
121 λalpha,test.whileTM alpha (atmr_step alpha test) 2.
123 lemma wsem_adv_to_mark_r :
125 WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
126 #alpha #test #t #i #outc #Hloop
127 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
128 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
130 [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
131 #Hfalse destruct (Hfalse)
132 | * #a * #Ha #Htest #ls #c #rs cases c
133 [ #Htapea' % % // >Htapea %
134 | #c' #Htapea' %2 @(ex_intro ?? c') % //
135 cases (true_or_false (test c')) #Htestc
137 | %2 % // generalize in match Htapea'; -Htapea'
140 [ normalize #x #Hfalse destruct (Hfalse)
145 >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % // <Htapea //
147 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
148 lapply (IH HRfalse) -IH #IH
150 cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
151 >Htapea' in Htapea; #Htapea destruct (Htapea) %2 % //
152 generalize in match Htapeb; -Htapeb
153 generalize in match Htapea'; -Htapea'
155 [ #Htapea #Htapeb % %
156 [ #x0 normalize #Hfalse destruct (Hfalse)
157 | normalize in Htapeb; cases (IH
161 cases (true_or_false (test c))
165 [ #Htapea %2 % [ %2 // ]
170 [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
172 [ * #_ #Houtc >Houtc >Htapeb %
173 | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
174 | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
176 [ * #Hfalse >(Hmemb …) in Hfalse;
177 [ #Hft destruct (Hft)
179 | * #Htestr1 #H1 >reverse_cons >associative_append
180 @H1 // #x #Hx @Hmemb @memb_cons //
185 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
187 (t1 = midtape alpha ls c rs →
188 ((test c = true ∧ t2 = t1) ∨
190 ∀rs1,b,rs2. rs = rs1@b::rs2 →
191 test b = true → (∀x.memb ? x rs1 = true → test x = false) →
192 t2 = midtape ? (reverse ? rs1@c::ls) b rs2))).
194 definition adv_to_mark_r ≝
195 λalpha,test.whileTM alpha (atmr_step alpha test) 2.
197 lemma wsem_adv_to_mark_r :
199 WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
200 #alpha #test #t #i #outc #Hloop
201 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
202 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
204 [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
205 #Hfalse destruct (Hfalse)
206 | * #a * #Ha #Htest #ls #c #rs #H2 %
207 >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
210 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
211 lapply (IH HRfalse) -IH #IH
212 #ls #c #rs #Htapea %2
213 cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
215 >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
216 [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
218 [ * #_ #Houtc >Houtc >Htapeb %
219 | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
220 | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
222 [ * #Hfalse >(Hmemb …) in Hfalse;
223 [ #Hft destruct (Hft)
225 | * #Htestr1 #H1 >reverse_cons >associative_append
226 @H1 // #x #Hx @Hmemb @memb_cons //
231 lemma terminate_adv_to_mark_r :
233 ∀t.Terminate alpha (adv_to_mark_r alpha test) t.
235 @(terminate_while … (sem_atmr_step alpha test))
238 [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
239 |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
240 | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
242 [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
243 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
244 % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
245 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
246 | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
247 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
254 lemma sem_adv_to_mark_r :
256 Realize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
265 definition nop_states ≝ initN 1.
268 λalpha:FinSet.mk_TM alpha nop_states
269 (λp.let 〈q,a〉 ≝ p in 〈q,None ?〉)
272 definition R_nop ≝ λalpha.λt1,t2:tape alpha.t2 = t1.
275 ∀alpha.Realize alpha (nop alpha) (R_nop alpha).
276 #alpha #intape @(ex_intro ?? 1) @ex_intro [| % normalize % ]
281 q1 〈a,false〉 → qF, 〈a,true〉, N
282 q1 〈a,true〉 → qF, _ , N
286 definition mark_states ≝ initN 3.
289 λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
293 | Some a' ⇒ match q with
294 [ O ⇒ 〈1,Some ? 〈a',R〉〉
296 [ O ⇒ let 〈a'',b〉 ≝ a' in
297 〈2,Some ? 〈〈a'',true〉,N〉〉
298 | S _ ⇒ 〈2,None ?〉 ] ] ])
301 definition R_mark ≝ λalpha,t1,t2.
303 t1 = midtape (FinProd … alpha FinBool) ls c (〈d,b〉::rs) →
304 t2 = midtape ? (c::ls) 〈d,true〉 rs.
308 step alpha (mark alpha)
309 (mk_config ?? 0 (midtape … ls c rs)) =
310 mk_config alpha (states ? (mark alpha)) 1
311 (midtape … (ls a0 rs).*)
314 ∀alpha.Realize ? (mark alpha) (R_mark alpha).
315 #alpha #intape @(ex_intro ?? 3) cases intape
317 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
319 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
321 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
323 [ @ex_intro [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #Hfalse destruct ] ]
324 | * #d #b #rs @ex_intro
325 [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #H1 destruct (H1) % ] ] ] ]
328 include "turing/if_machine.ma".
332 stato finale diverso a seconda che il carattere
333 corrente soddisfi un test booleano oppure no
335 q1 = true or no current char
339 definition tc_states ≝ initN 3.
341 definition test_char ≝
342 λalpha:FinSet.λtest:alpha→bool.
343 mk_TM alpha tc_states
350 | false ⇒ 〈2,None ?〉 ]])
351 O (λx.notb (x == 0)).
353 definition Rtc_true ≝
355 ∀c. current alpha t1 = Some ? c →
356 test c = true ∧ t2 = t1.
358 definition Rtc_false ≝
360 ∀c. current alpha t1 = Some ? c →
361 test c = false ∧ t2 = t1.
364 ∀alpha,test,ls,a0,rs. test a0 = true →
365 step alpha (test_char alpha test)
366 (mk_config ?? 0 (midtape … ls a0 rs)) =
367 mk_config alpha (states ? (test_char alpha test)) 1
368 (midtape … ls a0 rs).
369 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
373 ∀alpha,test,ls,a0,rs. test a0 = false →
374 step alpha (test_char alpha test)
375 (mk_config ?? 0 (midtape … ls a0 rs)) =
376 mk_config alpha (states ? (test_char alpha test)) 2
377 (midtape … ls a0 rs).
378 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
381 lemma sem_test_char :
383 accRealize alpha (test_char alpha test)
384 1 (Rtc_true alpha test) (Rtc_false alpha test).
387 @(ex_intro ?? (mk_config ?? 1 (niltape ?))) %
388 [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
389 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (leftof ? a al)))
390 % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
391 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (rightof ? a al)))
392 % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
393 | #ls #c #rs @(ex_intro ?? 2)
394 cases (true_or_false (test c)) #Htest
395 [ @(ex_intro ?? (mk_config ?? 1 ?))
398 [ whd in ⊢ (??%?); >tc_q0_q1 //
399 | #_ #c0 #Hc0 % // normalize in Hc0; destruct // ]
400 | * #Hfalse @False_ind @Hfalse % ]
402 | @(ex_intro ?? (mk_config ?? 2 (midtape ? ls c rs)))
405 [ whd in ⊢ (??%?); >tc_q0_q2 //
406 | #Hfalse destruct (Hfalse) ]
407 | #_ #c0 #Hc0 % // normalize in Hc0; destruct (Hc0) //
413 axiom myalpha : FinSet.
414 axiom is_bar : FinProd … myalpha FinBool → bool.
415 axiom is_grid : FinProd … myalpha FinBool → bool.
416 definition bar_or_grid ≝ λc.is_bar c ∨ is_grid c.
417 axiom bar : FinProd … myalpha FinBool.
418 axiom grid : FinProd … myalpha FinBool.
420 definition mark_next_tuple ≝
421 seq ? (adv_to_mark_r ? bar_or_grid)
422 (ifTM ? (test_char ? is_bar)
425 definition R_mark_next_tuple ≝
428 (* c non può essere un separatore ... speriamo *)
429 t1 = midtape ? ls c (rs1@grid::rs2) →
430 memb ? grid rs1 = false → bar_or_grid c = false →
431 (∃rs3,rs4,d,b.rs1 = rs3 @ bar :: rs4 ∧
432 memb ? bar rs3 = false ∧
433 Some ? 〈d,b〉 = option_hd ? (rs4@grid::rs2) ∧
434 t2 = midtape ? (bar::reverse ? rs3@c::ls) 〈d,true〉 (tail ? (rs4@grid::rs2)))
436 (memb ? bar rs1 = false ∧
437 t2 = midtape ? (reverse ? rs1@c::ls) grid rs2).
441 (∀x.memb A x l = true → f x = false) ∨
442 (∃l1,c,l2.f c = true ∧ l = l1@c::l2 ∧ ∀x.memb ? x l1 = true → f c = false).
444 [ % #x normalize #Hfalse *)
446 theorem sem_mark_next_tuple :
447 Realize ? mark_next_tuple R_mark_next_tuple.
449 lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid)
450 (ifTM ? (test_char ? is_bar) (mark ?) (nop ?) 1) ????)
453 |||#Hif cases (Hif intape) -Hif
454 #j * #outc * #Hloop * #ta * #Hleft #Hright
455 @(ex_intro ?? j) @ex_intro [|% [@Hloop] ]
457 #ls #c #rs1 #rs2 #Hrs #Hrs1 #Hc
459 [ * #Hfalse >Hfalse in Hc; #Htf destruct (Htf)
460 | * #_ #Hta cases (tech_split ? is_bar rs1)
461 [ #H1 lapply (Hta rs1 grid rs2 (refl ??) ? ?)
462 [ (* Hrs1, H1 *) @daemon
463 | (* bar_or_grid grid = true *) @daemon
464 | -Hta #Hta cases Hright
465 [ * #tb * whd in ⊢ (%→?); #Hcurrent
466 @False_ind cases(Hcurrent grid ?)
467 [ #Hfalse (* grid is not a bar *) @daemon
469 | * #tb * whd in ⊢ (%→?); #Hcurrent
470 cases (Hcurrent grid ?)
471 [ #_ #Htb whd in ⊢ (%→?); #Houtc
474 | >Houtc >Htb >Hta % ]
478 | * #rs3 * #c0 * #rs4 * * #Hc0 #Hsplit #Hrs3
479 % @(ex_intro ?? rs3) @(ex_intro ?? rs4)
480 lapply (Hta rs3 c0 (rs4@grid::rs2) ???)
481 [ #x #Hrs3' (* Hrs1, Hrs3, Hsplit *) @daemon
482 | (* bar → bar_or_grid *) @daemon
483 | >Hsplit >associative_append % ] -Hta #Hta
485 [ * #tb * whd in ⊢ (%→?); #Hta'
488 [ #_ #Htb' >Htb' in Htb; #Htb
489 generalize in match Hsplit; -Hsplit
491 [ >(eq_pair_fst_snd … grid)
492 #Hta #Hsplit >(Htb … Hta)
494 [ @(ex_intro ?? (\fst grid)) @(ex_intro ?? (\snd grid))
495 % [ % [ % [ (* Hsplit *) @daemon |(*Hrs3*) @daemon ] | % ] | % ]
496 | (* Hc0 *) @daemon ]
497 | #r5 #rs5 >(eq_pair_fst_snd … r5)
498 #Hta #Hsplit >(Htb … Hta)
500 [ @(ex_intro ?? (\fst r5)) @(ex_intro ?? (\snd r5))
501 % [ % [ % [ (* Hc0, Hsplit *) @daemon | (*Hrs3*) @daemon ] | % ]
502 | % ] | (* Hc0 *) @daemon ] ] | >Hta % ]
503 | * #tb * whd in ⊢ (%→?); #Hta'
506 [ #Hfalse @False_ind >Hfalse in Hc0;