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 atm0 : initN 3 ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
31 definition atm1 : initN 3 ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
32 definition atm2 : initN 3 ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
35 definition atmr_step ≝
36 λalpha:FinSet.λtest:alpha→bool.
37 mk_TM alpha atm_states
40 [ None ⇒ 〈atm1, None ?〉
43 [ true ⇒ 〈atm1,None ?〉
44 | false ⇒ 〈atm2,Some ? 〈a',R〉〉 ]])
45 atm0 (λx.notb (x == atm0)).
47 definition Ratmr_step_true ≝
50 t1 = midtape alpha ls a rs ∧ test a = false ∧
51 t2 = mk_tape alpha (a::ls) (option_hd ? rs) (tail ? rs).
53 definition Ratmr_step_false ≝
56 (current alpha t1 = None ? ∨
57 (∃a.current ? t1 = Some ? a ∧ test a = true)).
60 ∀alpha,test,ls,a0,rs. test a0 = true →
61 step alpha (atmr_step alpha test)
62 (mk_config ?? atm0 (midtape … ls a0 rs)) =
63 mk_config alpha (states ? (atmr_step alpha test)) atm1
65 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
66 whd in match (trans … 〈?,?〉); >Htest %
70 ∀alpha,test,ls,a0,rs. test a0 = false →
71 step alpha (atmr_step alpha test)
72 (mk_config ?? atm0 (midtape … ls a0 rs)) =
73 mk_config alpha (states ? (atmr_step alpha test)) atm2
74 (mk_tape … (a0::ls) (option_hd ? rs) (tail ? rs)).
75 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
76 whd in match (trans … 〈?,?〉); >Htest cases ts //
81 accRealize alpha (atmr_step alpha test)
82 atm2 (Ratmr_step_true alpha test) (Ratmr_step_false alpha test).
83 #alpha #test cut (∀P:Prop.atm1 = atm2 →P) [#P normalize #Hfalse destruct] #Hfalse
86 @(ex_intro ?? (mk_config ?? atm1 (niltape ?))) %
87 [ % // @Hfalse | #_ % // % % ]
88 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (leftof ? a al)))
89 % [ % // @Hfalse | #_ % // % % ]
90 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (rightof ? a al)))
91 % [ % // @Hfalse | #_ % // % % ]
92 | #ls #c #rs @(ex_intro ?? 2)
93 cases (true_or_false (test c)) #Htest
94 [ @(ex_intro ?? (mk_config ?? atm1 ?))
97 [ whd in ⊢ (??%?); >atmr_q0_q1 //
99 | #_ % // %2 @(ex_intro ?? c) % // ]
101 | @(ex_intro ?? (mk_config ?? atm2 (mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs))))
104 [ whd in ⊢ (??%?); >atmr_q0_q2 //
105 | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
108 | #Hfalse @False_ind @(absurd ?? Hfalse) %
115 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
117 t1 = mk_tape alpha ls c rs →
118 (c = None ? ∧ t2 = t1) ∨
120 ((test c' = true ∧ t2 = t1) ∨
122 (((∀x.memb ? x rs = true → test x = false) ∧
123 t2 = mk_tape ? (reverse ? rs@c'::ls) (None ?) []) ∨
124 (∃rs1,b,rs2.rs = rs1@b::rs2 ∧
125 test b = true ∧ (∀x.memb ? x rs1 = true → test x = false) ∧
126 t2 = midtape ? (reverse ? rs1@c'::rs) b rs2))))).
128 definition adv_to_mark_r ≝
129 λalpha,test.whileTM alpha (atmr_step alpha test) 2.
131 lemma wsem_adv_to_mark_r :
133 WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
134 #alpha #test #t #i #outc #Hloop
135 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
136 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
138 [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
139 #Hfalse destruct (Hfalse)
140 | * #a * #Ha #Htest #ls #c #rs cases c
141 [ #Htapea' % % // >Htapea %
142 | #c' #Htapea' %2 @(ex_intro ?? c') % //
143 cases (true_or_false (test c')) #Htestc
145 | %2 % // generalize in match Htapea'; -Htapea'
148 [ normalize #x #Hfalse destruct (Hfalse)
153 >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % // <Htapea //
155 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
156 lapply (IH HRfalse) -IH #IH
158 cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
159 >Htapea' in Htapea; #Htapea destruct (Htapea) %2 % //
160 generalize in match Htapeb; -Htapeb
161 generalize in match Htapea'; -Htapea'
163 [ #Htapea #Htapeb % %
164 [ #x0 normalize #Hfalse destruct (Hfalse)
165 | normalize in Htapeb; cases (IH
169 cases (true_or_false (test c))
173 [ #Htapea %2 % [ %2 // ]
178 [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
180 [ * #_ #Houtc >Houtc >Htapeb %
181 | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
182 | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
184 [ * #Hfalse >(Hmemb …) in Hfalse;
185 [ #Hft destruct (Hft)
187 | * #Htestr1 #H1 >reverse_cons >associative_append
188 @H1 // #x #Hx @Hmemb @memb_cons //
193 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
195 (t1 = midtape alpha ls c rs →
196 ((test c = true ∧ t2 = t1) ∨
198 ∀rs1,b,rs2. rs = rs1@b::rs2 →
199 test b = true → (∀x.memb ? x rs1 = true → test x = false) →
200 t2 = midtape ? (reverse ? rs1@c::ls) b rs2))).
202 definition adv_to_mark_r ≝
203 λalpha,test.whileTM alpha (atmr_step alpha test) atm2.
205 lemma wsem_adv_to_mark_r :
207 WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
208 #alpha #test #t #i #outc #Hloop
209 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
210 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
212 [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
213 #Hfalse destruct (Hfalse)
214 | * #a * #Ha #Htest #ls #c #rs #H2 %
215 >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
218 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
219 lapply (IH HRfalse) -IH #IH
220 #ls #c #rs #Htapea %2
221 cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
223 >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
224 [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
226 [ * #_ #Houtc >Houtc >Htapeb %
227 | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
228 | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
230 [ * #Hfalse >(Hmemb …) in Hfalse;
231 [ #Hft destruct (Hft)
233 | * #Htestr1 #H1 >reverse_cons >associative_append
234 @H1 // #x #Hx @Hmemb @memb_cons //
239 lemma terminate_adv_to_mark_r :
241 ∀t.Terminate alpha (adv_to_mark_r alpha test) t.
243 @(terminate_while … (sem_atmr_step alpha test))
246 [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
247 |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
248 | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
250 [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
251 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
252 % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
253 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
254 | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
255 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
262 lemma sem_adv_to_mark_r :
264 Realize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
270 q1 〈a,false〉 → qF, 〈a,true〉, N
271 q1 〈a,true〉 → qF, _ , N
275 definition mark_states ≝ initN 3.
277 definition mark0 : initN 3 ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
278 definition mark1 : initN 3 ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
279 definition mark2 : initN 3 ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
282 λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
285 [ None ⇒ 〈mark2,None ?〉
286 | Some a' ⇒ match pi1 … q with
287 [ O ⇒ 〈mark1,Some ? 〈a',R〉〉
289 [ O ⇒ let 〈a'',b〉 ≝ a' in
290 〈mark2,Some ? 〈〈a'',true〉,N〉〉
291 | S _ ⇒ 〈mark2,None ?〉 ] ] ])
292 mark0 (λq.q == mark2).
294 definition R_mark ≝ λalpha,t1,t2.
296 t1 = midtape (FinProd … alpha FinBool) ls c (〈d,b〉::rs) →
297 t2 = midtape ? (c::ls) 〈d,true〉 rs.
301 step alpha (mark alpha)
302 (mk_config ?? 0 (midtape … ls c rs)) =
303 mk_config alpha (states ? (mark alpha)) 1
304 (midtape … (ls a0 rs).*)
307 ∀alpha.Realize ? (mark alpha) (R_mark alpha).
308 #alpha #intape @(ex_intro ?? 3) cases intape
310 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
312 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
314 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
316 [ @ex_intro [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #Hfalse destruct ] ]
317 | * #d #b #rs @ex_intro
318 [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #H1 destruct (H1) % ] ] ] ]
321 include "turing/if_machine.ma".
325 stato finale diverso a seconda che il carattere
326 corrente soddisfi un test booleano oppure no
328 q1 = true or no current char
332 definition tc_states ≝ initN 3.
334 definition tc0 : initN 3 ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
335 definition tc1 : initN 3 ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
336 definition atm2 : initN 3 ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
338 definition test_char ≝
339 λalpha:FinSet.λtest:alpha→bool.
340 mk_TM alpha tc_states
347 | false ⇒ 〈2,None ?〉 ]])
348 O (λx.notb (x == 0)).
350 definition Rtc_true ≝
352 ∀c. current alpha t1 = Some ? c →
353 test c = true ∧ t2 = t1.
355 definition Rtc_false ≝
357 ∀c. current alpha t1 = Some ? c →
358 test c = false ∧ t2 = t1.
361 ∀alpha,test,ls,a0,rs. test a0 = true →
362 step alpha (test_char alpha test)
363 (mk_config ?? 0 (midtape … ls a0 rs)) =
364 mk_config alpha (states ? (test_char alpha test)) 1
365 (midtape … ls a0 rs).
366 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
370 ∀alpha,test,ls,a0,rs. test a0 = false →
371 step alpha (test_char alpha test)
372 (mk_config ?? 0 (midtape … ls a0 rs)) =
373 mk_config alpha (states ? (test_char alpha test)) 2
374 (midtape … ls a0 rs).
375 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
378 lemma sem_test_char :
380 accRealize alpha (test_char alpha test)
381 1 (Rtc_true alpha test) (Rtc_false alpha test).
384 @(ex_intro ?? (mk_config ?? 1 (niltape ?))) %
385 [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
386 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (leftof ? a al)))
387 % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
388 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (rightof ? a al)))
389 % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
390 | #ls #c #rs @(ex_intro ?? 2)
391 cases (true_or_false (test c)) #Htest
392 [ @(ex_intro ?? (mk_config ?? 1 ?))
395 [ whd in ⊢ (??%?); >tc_q0_q1 //
396 | #_ #c0 #Hc0 % // normalize in Hc0; destruct // ]
397 | * #Hfalse @False_ind @Hfalse % ]
399 | @(ex_intro ?? (mk_config ?? 2 (midtape ? ls c rs)))
402 [ whd in ⊢ (??%?); >tc_q0_q2 //
403 | #Hfalse destruct (Hfalse) ]
404 | #_ #c0 #Hc0 % // normalize in Hc0; destruct (Hc0) //
410 axiom myalpha : FinSet.
411 axiom is_bar : FinProd … myalpha FinBool → bool.
412 axiom is_grid : FinProd … myalpha FinBool → bool.
413 definition bar_or_grid ≝ λc.is_bar c ∨ is_grid c.
414 axiom bar : FinProd … myalpha FinBool.
415 axiom grid : FinProd … myalpha FinBool.
417 definition mark_next_tuple ≝
418 seq ? (adv_to_mark_r ? bar_or_grid)
419 (ifTM ? (test_char ? is_bar)
422 definition R_mark_next_tuple ≝
425 (* c non può essere un separatore ... speriamo *)
426 t1 = midtape ? ls c (rs1@grid::rs2) →
427 memb ? grid rs1 = false → bar_or_grid c = false →
428 (∃rs3,rs4,d,b.rs1 = rs3 @ bar :: rs4 ∧
429 memb ? bar rs3 = false ∧
430 Some ? 〈d,b〉 = option_hd ? (rs4@grid::rs2) ∧
431 t2 = midtape ? (bar::reverse ? rs3@c::ls) 〈d,true〉 (tail ? (rs4@grid::rs2)))
433 (memb ? bar rs1 = false ∧
434 t2 = midtape ? (reverse ? rs1@c::ls) grid rs2).
438 (∀x.memb A x l = true → f x = false) ∨
439 (∃l1,c,l2.f c = true ∧ l = l1@c::l2 ∧ ∀x.memb ? x l1 = true → f c = false).
441 [ % #x normalize #Hfalse *)
443 theorem sem_mark_next_tuple :
444 Realize ? mark_next_tuple R_mark_next_tuple.
446 lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid)
447 (ifTM ? (test_char ? is_bar) (mark ?) (nop ?) 1) ????)
450 |||#Hif cases (Hif intape) -Hif
451 #j * #outc * #Hloop * #ta * #Hleft #Hright
452 @(ex_intro ?? j) @ex_intro [|% [@Hloop] ]
454 #ls #c #rs1 #rs2 #Hrs #Hrs1 #Hc
456 [ * #Hfalse >Hfalse in Hc; #Htf destruct (Htf)
457 | * #_ #Hta cases (tech_split ? is_bar rs1)
458 [ #H1 lapply (Hta rs1 grid rs2 (refl ??) ? ?)
459 [ (* Hrs1, H1 *) @daemon
460 | (* bar_or_grid grid = true *) @daemon
461 | -Hta #Hta cases Hright
462 [ * #tb * whd in ⊢ (%→?); #Hcurrent
463 @False_ind cases(Hcurrent grid ?)
464 [ #Hfalse (* grid is not a bar *) @daemon
466 | * #tb * whd in ⊢ (%→?); #Hcurrent
467 cases (Hcurrent grid ?)
468 [ #_ #Htb whd in ⊢ (%→?); #Houtc
471 | >Houtc >Htb >Hta % ]
475 | * #rs3 * #c0 * #rs4 * * #Hc0 #Hsplit #Hrs3
476 % @(ex_intro ?? rs3) @(ex_intro ?? rs4)
477 lapply (Hta rs3 c0 (rs4@grid::rs2) ???)
478 [ #x #Hrs3' (* Hrs1, Hrs3, Hsplit *) @daemon
479 | (* bar → bar_or_grid *) @daemon
480 | >Hsplit >associative_append % ] -Hta #Hta
482 [ * #tb * whd in ⊢ (%→?); #Hta'
485 [ #_ #Htb' >Htb' in Htb; #Htb
486 generalize in match Hsplit; -Hsplit
488 [ >(eq_pair_fst_snd … grid)
489 #Hta #Hsplit >(Htb … Hta)
491 [ @(ex_intro ?? (\fst grid)) @(ex_intro ?? (\snd grid))
492 % [ % [ % [ (* Hsplit *) @daemon |(*Hrs3*) @daemon ] | % ] | % ]
493 | (* Hc0 *) @daemon ]
494 | #r5 #rs5 >(eq_pair_fst_snd … r5)
495 #Hta #Hsplit >(Htb … Hta)
497 [ @(ex_intro ?? (\fst r5)) @(ex_intro ?? (\snd r5))
498 % [ % [ % [ (* Hc0, Hsplit *) @daemon | (*Hrs3*) @daemon ] | % ]
499 | % ] | (* Hc0 *) @daemon ] ] | >Hta % ]
500 | * #tb * whd in ⊢ (%→?); #Hta'
503 [ #Hfalse @False_ind >Hfalse in Hc0;