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/if_machine.ma".
18 include "turing/basic_machines.ma".
19 include "turing/universal/alphabet.ma".
21 (* ADVANCE TO MARK (right)
23 sposta la testina a destra fino a raggiungere il primo carattere marcato
27 (* 0, a ≠ mark _ ⇒ 0, R
28 0, a = mark _ ⇒ 1, N *)
30 definition atm_states ≝ initN 3.
32 definition atm0 : atm_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
33 definition atm1 : atm_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
34 definition atm2 : atm_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
36 definition atmr_step ≝
37 λalpha:FinSet.λtest:alpha→bool.
38 mk_TM alpha atm_states
41 [ None ⇒ 〈atm1, None ?〉
44 [ true ⇒ 〈atm1,None ?〉
45 | false ⇒ 〈atm2,Some ? 〈a',R〉〉 ]])
46 atm0 (λx.notb (x == atm0)).
48 definition Ratmr_step_true ≝
51 t1 = midtape alpha ls a rs ∧ test a = false ∧
52 t2 = mk_tape alpha (a::ls) (option_hd ? rs) (tail ? rs).
54 definition Ratmr_step_false ≝
57 (current alpha t1 = None ? ∨
58 (∃a.current ? t1 = Some ? a ∧ test a = true)).
61 ∀alpha,test,ls,a0,rs. test a0 = true →
62 step alpha (atmr_step alpha test)
63 (mk_config ?? atm0 (midtape … ls a0 rs)) =
64 mk_config alpha (states ? (atmr_step alpha test)) atm1
66 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
67 whd in match (trans … 〈?,?〉); >Htest %
71 ∀alpha,test,ls,a0,rs. test a0 = false →
72 step alpha (atmr_step alpha test)
73 (mk_config ?? atm0 (midtape … ls a0 rs)) =
74 mk_config alpha (states ? (atmr_step alpha test)) atm2
75 (mk_tape … (a0::ls) (option_hd ? rs) (tail ? rs)).
76 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
77 whd in match (trans … 〈?,?〉); >Htest cases ts //
82 accRealize alpha (atmr_step alpha test)
83 atm2 (Ratmr_step_true alpha test) (Ratmr_step_false alpha test).
86 @(ex_intro ?? (mk_config ?? atm1 (niltape ?))) %
87 [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
88 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (leftof ? a al)))
89 % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
90 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (rightof ? a al)))
91 % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
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 //
98 | whd in ⊢ ((??%%)→?); #Hfalse destruct ]
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) %
114 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
116 (t1 = midtape alpha ls c rs →
117 ((test c = true ∧ t2 = t1) ∨
119 ∀rs1,b,rs2. rs = rs1@b::rs2 →
120 test b = true → (∀x.memb ? x rs1 = true → test x = false) →
121 t2 = midtape ? (reverse ? rs1@c::ls) b rs2))).
123 definition adv_to_mark_r ≝
124 λalpha,test.whileTM alpha (atmr_step alpha test) atm2.
126 lemma wsem_adv_to_mark_r :
128 WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
129 #alpha #test #t #i #outc #Hloop
130 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
131 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
133 [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
134 #Hfalse destruct (Hfalse)
135 | * #a * #Ha #Htest #ls #c #rs #H2 %
136 >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
139 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
140 lapply (IH HRfalse) -IH #IH
141 #ls #c #rs #Htapea %2
142 cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
144 >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
145 [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
147 [ * #_ #Houtc >Houtc >Htapeb %
148 | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
149 | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
151 [ * #Hfalse >(Hmemb …) in Hfalse;
152 [ #Hft destruct (Hft)
154 | * #Htestr1 #H1 >reverse_cons >associative_append
155 @H1 // #x #Hx @Hmemb @memb_cons //
160 lemma terminate_adv_to_mark_r :
162 ∀t.Terminate alpha (adv_to_mark_r alpha test) t.
164 @(terminate_while … (sem_atmr_step alpha test))
167 [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
168 |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
169 | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
171 [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
172 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
173 % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
174 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
175 | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
176 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
183 lemma sem_adv_to_mark_r :
185 Realize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
191 marks the current character
194 definition mark_states ≝ initN 2.
196 definition ms0 : mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
197 definition ms1 : mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
200 λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
203 [ None ⇒ 〈ms1,None ?〉
204 | Some a' ⇒ match (pi1 … q) with
205 [ O ⇒ let 〈a'',b〉 ≝ a' in 〈ms1,Some ? 〈〈a'',true〉,N〉〉
206 | S q ⇒ 〈ms1,None ?〉 ] ])
209 definition R_mark ≝ λalpha,t1,t2.
211 t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
212 t2 = midtape ? ls 〈c,true〉 rs.
215 ∀alpha.Realize ? (mark alpha) (R_mark alpha).
216 #alpha #intape @(ex_intro ?? 2) cases intape
218 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
220 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
222 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
224 @ex_intro [| % [ % | #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ] ] ]
228 (* MOVE RIGHT AND MARK machine
230 marks the first character on the right
232 (could be rewritten using (mark; move_right))
235 definition mrm_states ≝ initN 3.
237 definition mrm0 : mrm_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
238 definition mrm1 : mrm_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
239 definition mrm2 : mrm_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
241 definition move_right_and_mark ≝
242 λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mrm_states
245 [ None ⇒ 〈mrm2,None ?〉
246 | Some a' ⇒ match pi1 … q with
247 [ O ⇒ 〈mrm1,Some ? 〈a',R〉〉
249 [ O ⇒ let 〈a'',b〉 ≝ a' in
250 〈mrm2,Some ? 〈〈a'',true〉,N〉〉
251 | S _ ⇒ 〈mrm2,None ?〉 ] ] ])
254 definition R_move_right_and_mark ≝ λalpha,t1,t2.
256 t1 = midtape (FinProd … alpha FinBool) ls c (〈d,b〉::rs) →
257 t2 = midtape ? (c::ls) 〈d,true〉 rs.
259 lemma sem_move_right_and_mark :
260 ∀alpha.Realize ? (move_right_and_mark alpha) (R_move_right_and_mark alpha).
261 #alpha #intape @(ex_intro ?? 3) cases intape
263 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
265 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
267 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
269 [ @ex_intro [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #Hfalse destruct ] ]
270 | * #d #b #rs @ex_intro
271 [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #H1 destruct (H1) % ] ] ] ]
274 (* CLEAR MARK machine
276 clears the mark in the current character
279 definition clear_mark_states ≝ initN 3.
281 definition clear0 : clear_mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
282 definition clear1 : clear_mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
283 definition claer2 : clear_mark_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
285 definition clear_mark ≝
286 λalpha:FinSet.mk_TM (FinProd … alpha FinBool) clear_mark_states
289 [ None ⇒ 〈clear1,None ?〉
290 | Some a' ⇒ match pi1 … q with
291 [ O ⇒ let 〈a'',b〉 ≝ a' in 〈clear1,Some ? 〈〈a'',false〉,N〉〉
292 | S q ⇒ 〈clear1,None ?〉 ] ])
293 clear0 (λq.q == clear1).
295 definition R_clear_mark ≝ λalpha,t1,t2.
297 t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
298 t2 = midtape ? ls 〈c,false〉 rs.
300 lemma sem_clear_mark :
301 ∀alpha.Realize ? (clear_mark alpha) (R_clear_mark alpha).
302 #alpha #intape @(ex_intro ?? 2) cases intape
304 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
306 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
308 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
310 @ex_intro [| % [ % | #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ] ] ]
313 (* ADVANCE MARK RIGHT machine
315 clears mark on current char,
316 moves right, and marks new current char
320 definition adv_mark_r ≝
322 clear_mark alpha · move_r ? · mark alpha.
324 definition R_adv_mark_r ≝ λalpha,t1,t2.
326 t1 = midtape (FinProd … alpha FinBool) ls 〈c,true〉 (〈d,b〉::rs) →
327 t2 = midtape ? (〈c,false〉::ls) 〈d,true〉 rs.
329 lemma sem_adv_mark_r :
330 ∀alpha.Realize ? (adv_mark_r alpha) (R_adv_mark_r alpha).
332 cases (sem_seq ????? (sem_clear_mark …)
333 (sem_seq ????? (sem_move_r ?) (sem_mark alpha)) intape)
334 #k * #outc * #Hloop whd in ⊢ (%→?);
335 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→%→?); #Hs2 #Hs3
336 @(ex_intro ?? k) @(ex_intro ?? outc) %
338 | -Hloop #ls #c #d #b #rs #Hintape @(Hs3 … b)
339 @(Hs2 ls 〈c,false〉 (〈d,b〉::rs))
344 (* ADVANCE TO MARK (left)
349 definition atml_step ≝
350 λalpha:FinSet.λtest:alpha→bool.
351 mk_TM alpha atm_states
354 [ None ⇒ 〈atm1, None ?〉
357 [ true ⇒ 〈atm1,None ?〉
358 | false ⇒ 〈atm2,Some ? 〈a',L〉〉 ]])
359 atm0 (λx.notb (x == atm0)).
361 definition Ratml_step_true ≝
364 t1 = midtape alpha ls a rs ∧ test a = false ∧
365 t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a :: rs).
367 definition Ratml_step_false ≝
370 (current alpha t1 = None ? ∨
371 (∃a.current ? t1 = Some ? a ∧ test a = true)).
374 ∀alpha,test,ls,a0,rs. test a0 = true →
375 step alpha (atml_step alpha test)
376 (mk_config ?? atm0 (midtape … ls a0 rs)) =
377 mk_config alpha (states ? (atml_step alpha test)) atm1
378 (midtape … ls a0 rs).
379 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
380 whd in match (trans … 〈?,?〉); >Htest %
384 ∀alpha,test,ls,a0,rs. test a0 = false →
385 step alpha (atml_step alpha test)
386 (mk_config ?? atm0 (midtape … ls a0 rs)) =
387 mk_config alpha (states ? (atml_step alpha test)) atm2
388 (mk_tape … (tail ? ls) (option_hd ? ls) (a0 :: rs)).
389 #alpha #test #ls #a0 #rs #Htest whd in ⊢ (??%?);
390 whd in match (trans … 〈?,?〉); >Htest cases ls //
393 lemma sem_atml_step :
395 accRealize alpha (atml_step alpha test)
396 atm2 (Ratml_step_true alpha test) (Ratml_step_false alpha test).
399 @(ex_intro ?? (mk_config ?? atm1 (niltape ?))) %
400 [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
401 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (leftof ? a al)))
402 % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
403 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (rightof ? a al)))
404 % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
405 | #ls #c #rs @(ex_intro ?? 2)
406 cases (true_or_false (test c)) #Htest
407 [ @(ex_intro ?? (mk_config ?? atm1 ?))
410 [ whd in ⊢ (??%?); >atml_q0_q1 //
411 | whd in ⊢ ((??%%)→?); #Hfalse destruct ]
412 | #_ % // %2 @(ex_intro ?? c) % // ]
414 | @(ex_intro ?? (mk_config ?? atm2 (mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs))))
417 [ whd in ⊢ (??%?); >atml_q0_q2 //
418 | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
421 | #Hfalse @False_ind @(absurd ?? Hfalse) %
427 definition R_adv_to_mark_l ≝ λalpha,test,t1,t2.
429 (t1 = midtape alpha ls c rs →
430 ((test c = true ∧ t2 = t1) ∨
432 ∀ls1,b,ls2. ls = ls1@b::ls2 →
433 test b = true → (∀x.memb ? x ls1 = true → test x = false) →
434 t2 = midtape ? ls2 b (reverse ? ls1@c::rs)))).
436 definition adv_to_mark_l ≝
437 λalpha,test.whileTM alpha (atml_step alpha test) atm2.
439 lemma wsem_adv_to_mark_l :
441 WRealize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
442 #alpha #test #t #i #outc #Hloop
443 lapply (sem_while … (sem_atml_step alpha test) t i outc Hloop) [%]
444 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
446 [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
447 #Hfalse destruct (Hfalse)
448 | * #a * #Ha #Htest #ls #c #rs #H2 %
449 >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
452 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
453 lapply (IH HRfalse) -IH #IH
454 #ls #c #rs #Htapea %2
455 cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
456 >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
457 [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
459 [ * #_ #Houtc >Houtc >Htapeb %
460 | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
461 | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
463 [ * #Hfalse >(Hmemb …) in Hfalse;
464 [ #Hft destruct (Hft)
466 | * #Htestr1 #H1 >reverse_cons >associative_append
467 @H1 // #x #Hx @Hmemb @memb_cons //
472 lemma terminate_adv_to_mark_l :
474 ∀t.Terminate alpha (adv_to_mark_l alpha test) t.
476 @(terminate_while … (sem_atml_step alpha test))
479 [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
480 |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
482 [#c #rs % #t1 * #ls0 * #c0 * #rs0 * *
483 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
484 % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
485 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
486 | #rs0 #r0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
487 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
494 lemma sem_adv_to_mark_l :
496 Realize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
501 ADVANCE BOTH MARKS machine
503 l1 does not contain marks ⇒
515 definition adv_both_marks ≝ λalpha.
516 adv_mark_r alpha · move_l ? ·
517 adv_to_mark_l (FinProd alpha FinBool) (is_marked alpha) ·
520 definition R_adv_both_marks ≝
522 ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
523 t1 = midtape (FinProd … alpha FinBool)
524 (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
525 t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2).
527 lemma sem_adv_both_marks :
528 ∀alpha.Realize ? (adv_both_marks alpha) (R_adv_both_marks alpha).
530 cases (sem_seq ????? (sem_adv_mark_r …)
531 (sem_seq ????? (sem_move_l …)
532 (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?))
533 (sem_adv_mark_r alpha))) intape)
534 #k * #outc * #Hloop whd in ⊢ (%→?);
535 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→?); #Hs2
536 * #tc * whd in ⊢ (%→%→?); #Hs3 #Hs4
537 @(ex_intro ?? k) @(ex_intro ?? outc) %
539 | -Hloop #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
541 lapply (Hs1 … Hintape) #Hta
542 lapply (Hs2 … Hta) #Htb
544 [ * #Hfalse normalize in Hfalse; destruct (Hfalse)
546 lapply (Hs3 (l1@[〈a,false〉]) 〈x,true〉 l0 ???)
547 [ #x1 #Hx1 cases (memb_append … Hx1)
549 | #Hx1' >(memb_single … Hx1') % ]
551 | >associative_append %
552 | >reverse_append #Htc @Htc ]
564 l0 x a* l1 x0 a0* l2 (f(x0) == true)
566 l0 x* a l1 x0* a0 l2 (f(x0) == false)
570 definition match_and_adv ≝
571 λalpha,f.ifTM ? (test_char ? f)
572 (adv_both_marks alpha) (clear_mark ?) tc_true.
574 definition R_match_and_adv ≝
576 ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
577 t1 = midtape (FinProd … alpha FinBool)
578 (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
579 (f 〈x0,true〉 = true ∧ t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2))
580 ∨ (f 〈x0,true〉 = false ∧
581 t2 = midtape ? (l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)).
583 lemma sem_match_and_adv :
584 ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv alpha f).
586 cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape)
587 #k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
590 [ * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
591 #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
592 >Hintape in Hta; #Hta cases (Hta … (refl ??)) -Hta #Hf #Hta % %
593 [ @Hf | @Houtc [ @Hl1 | @Hta ] ]
594 | * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
595 #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
596 >Hintape in Hta; #Hta cases (Hta … (refl ??)) -Hta #Hf #Hta %2 %
597 [ @Hf | >(Houtc … Hta) % ]
603 then move_right; ----
605 if current (* x0 *) = 0
606 then advance_mark ----
613 definition comp_step_subcase ≝ λalpha,c,elseM.
614 ifTM ? (test_char ? (λx.x == c))
615 (move_r … · adv_to_mark_r ? (is_marked alpha) · match_and_adv ? (λx.x == c))
618 definition R_comp_step_subcase ≝
619 λalpha,c,RelseM,t1,t2.
620 ∀l0,x,rs.t1 = midtape (FinProd … alpha FinBool) l0 〈x,true〉 rs →
622 ∀a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
623 rs = 〈a,false〉::l1@〈x0,true〉::〈a0,false〉::l2 →
625 t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1@〈x0,false〉::〈a0,true〉::l2)) ∨
627 t2 = midtape (FinProd … alpha FinBool)
628 (reverse ? l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)))) ∨
629 (〈x,true〉 ≠ c ∧ RelseM t1 t2).
631 lemma sem_comp_step_subcase :
632 ∀alpha,c,elseM,RelseM.
633 Realize ? elseM RelseM →
634 Realize ? (comp_step_subcase alpha c elseM)
635 (R_comp_step_subcase alpha c RelseM).
636 #alpha #c #elseM #RelseM #Helse #intape
637 cases (sem_if ? (test_char ? (λx.x == c)) … tc_true
638 (sem_test_char ? (λx.x == c))
639 (sem_seq ????? (sem_move_r …)
640 (sem_seq ????? (sem_adv_to_mark_r ? (is_marked alpha))
641 (sem_match_and_adv ? (λx.x == c)))) Helse intape)
642 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc)
643 % [ @Hloop ] -Hloop cases HR -HR
644 [ * #ta * whd in ⊢ (%→?); #Hta * #tb * whd in ⊢ (%→?); #Htb
645 * #tc * whd in ⊢ (%→?); #Htc whd in ⊢ (%→?); #Houtc
646 #l0 #x #rs #Hintape cases (true_or_false (〈x,true〉==c)) #Hc
648 #a #l1 #x0 #a0 #l2 #Hl1 #Hrs >Hrs in Hintape; #Hintape
649 >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta
650 #Hx #Hta lapply (Htb … Hta) -Htb #Htb
651 cases (Htc … Htb) [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
652 -Htc * #_ #Htc lapply (Htc l1 〈x0,true〉 (〈a0,false〉::l2) (refl ??) (refl ??) Hl1)
653 -Htc #Htc cases (Houtc ???????? Htc) -Houtc
655 % [ <(\P Hx0) in Hx; #Hx lapply (\P Hx) #Hx' destruct (Hx') %
656 | >Houtc >reverse_reverse % ]
658 % [ <(\P Hx) in Hx0; #Hx0 lapply (\Pf Hx0) @not_to_not #Hx' >Hx' %
660 | #x #membx @Hl1 <(reverse_reverse …l1) @memb_reverse @membx ]
662 >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hx #Hta
663 >Hx in Hc;#Hc destruct (Hc) ]
664 | * #ta * whd in ⊢ (%→?); #Hta #Helse #ls #c0 #rs #Hintape %2
665 >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hc #Hta %
666 [ @(\Pf Hc) | <Hta @Helse ]
673 + se è un bit, ho fallito il confronto della tupla corrente
674 + se è un separatore, la tupla fa match
677 ifTM ? (test_char ? is_marked)
678 (single_finalTM … (comp_step_subcase unialpha 〈bit false,true〉
679 (comp_step_subcase unialpha 〈bit true,true〉
684 definition comp_step ≝
685 ifTM ? (test_char ? (is_marked ?))
686 (single_finalTM … (comp_step_subcase FSUnialpha 〈bit false,true〉
687 (comp_step_subcase FSUnialpha 〈bit true,true〉
688 (comp_step_subcase FSUnialpha 〈null,true〉
693 definition R_comp_step_true ≝
695 ∀l0,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) l0 c rs →
697 ((bit_or_null c' = true ∧
699 rs = 〈a,false〉::l1@〈c0,true〉::〈a0,false〉::l2 →
700 (∀c.memb ? c l1 = true → is_marked ? c = false) →
702 t2 = midtape ? (〈c',false〉::l0) 〈a,true〉 (l1@〈c0,false〉::〈a0,true〉::l2)) ∨
704 t2 = midtape (FinProd … FSUnialpha FinBool)
705 (reverse ? l1@〈a,false〉::〈c',true〉::l0) 〈c0,false〉 (〈a0,false〉::l2))) ∨
706 (bit_or_null c' = false ∧ t2 = midtape ? l0 〈c',false〉 rs)).
708 definition R_comp_step_false ≝
710 ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
711 is_marked ? c = false ∧ t2 = t1.
713 lemma sem_comp_step :
714 accRealize ? comp_step (inr … (inl … (inr … start_nop)))
715 R_comp_step_true R_comp_step_false.
717 cases (acc_sem_if … (sem_test_char ? (is_marked ?))
718 (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
719 (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ??
720 (sem_comp_step_subcase FSUnialpha 〈null,true〉 ??
721 (sem_clear_mark …))))
723 #k * #outc * * #Hloop #H1 #H2
724 @(ex_intro ?? k) @(ex_intro ?? outc) %
725 [ % [@Hloop ] ] -Hloop
726 [ #Hstate lapply (H1 Hstate) -H1 -Hstate -H2 *
727 #ta * whd in ⊢ (%→?); #Hleft #Hright #ls #c #rs #Hintape
728 >Hintape in Hleft; #Hleft cases (Hleft ? (refl ??)) -Hleft
729 cases c in Hintape; #c' #b #Hintape whd in ⊢ (??%?→?);
730 #Hb >Hb #Hta @(ex_intro ?? c') % //
732 [ * #Hc' #H1 % % [destruct (Hc') % ]
733 #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
735 [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
736 | * #Hneq #Houtc %2 %
740 | * #Hc #Helse1 cases (Helse1 … Hta)
741 [ * #Hc' #H1 % % [destruct (Hc') % ]
742 #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
744 [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
745 | * #Hneq #Houtc %2 %
749 | * #Hc' #Helse2 cases (Helse2 … Hta)
750 [ * #Hc'' #H1 % % [destruct (Hc'') % ]
751 #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
753 [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
754 | * #Hneq #Houtc %2 %
758 | * #Hc'' whd in ⊢ (%→?); #Helse3 %2 %
759 [ generalize in match Hc''; generalize in match Hc'; generalize in match Hc;
761 [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
762 | #Hfalse @False_ind @(absurd ?? Hfalse) % ]
763 | #_ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
770 | #Hstate lapply (H2 Hstate) -H1 -Hstate -H2 *
771 #ta * whd in ⊢ (%→%→?); #Hleft #Hright #ls #c #rs #Hintape
772 >Hintape in Hleft; #Hleft
773 cases (Hleft ? (refl ??)) -Hleft
774 #Hc #Hta % // >Hright //
779 whileTM ? comp_step (inr … (inl … (inr … start_nop))).
782 definition R_compare :=
786 ∀ls,c,b,rs.t1 = midtape ? ls 〈c,b〉 rs →
787 (b = true → rs = ....) →
791 rs = cs@l1@〈c0,true〉::cs0@l2
795 ls 〈c,b〉 cs l1 〈c0,b0〉 cs0 l2
799 ls (hd (Ls@〈grid,false〉))* (tail (Ls@〈grid,false〉)) l1 (hd (Ls@〈comma,false〉))* (tail (Ls@〈comma,false〉)) l2
800 ^^^^^^^^^^^^^^^^^^^^^^^
802 ls Ls 〈grid,false〉 l1 Ls 〈comma,true〉 l2
807 ls (hd (Ls@〈c,false〉))* (tail (Ls@〈c,false〉)) l1 (hd (Ls@〈d,false〉))* (tail (Ls@〈d,false〉)) l2
808 ^^^^^^^^^^^^^^^^^^^^^^^
811 ls Ls 〈c,true〉 l1 Ls 〈d,false〉 l2
817 (∃la,d.〈b,true〉::bs = la@[〈grid,d〉] ∧ ∀x.memb ? x la → is_bit (\fst x) = true) →
818 (∃lb,d0.〈b0,true〉::b0s = lb@[〈comma,d0〉] ∧ ∀x.memb ? x lb → is_bit (\fst x) = true) →
819 t1 = midtape ? l0 〈b,true〉 (bs@l1@〈b0,true〉::b0s@l2 →
821 mk_tape left (option current) right
823 (b = grid ∧ b0 = comma ∧ bs = [] ∧ b0s = [] ∧
824 t2 = midtape ? l0 〈grid,false〉 (l1@〈comma,true〉::l2)) ∨
825 (b = bit x ∧ b = c ∧ bs = b0s
827 definition R_compare :=
829 ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
830 (∀c'.bit_or_null c' = false → c = 〈c',true〉 → t2 = midtape ? ls 〈c',false〉 rs) ∧
831 (∀c'. c = 〈c',false〉 → t2 = t1) ∧
834 (∀c.memb (FinProd … FSUnialpha FinBool) c bs = true → bit_or_null (\fst c) = true) →
835 (∀c.memb (FinProd … FSUnialpha FinBool) c b0s = true → bit_or_null (\fst c) = true) →
836 (∀c.memb ? c bs = true → is_marked ? c = false) →
837 (∀c.memb ? c b0s = true → is_marked ? c = false) →
838 (∀c.memb ? c l1 = true → is_marked ? c = false) →
839 c = 〈b,true〉 → bit_or_null b = true →
840 rs = bs@〈grid,false〉::l1@〈b0,true〉::b0s@〈comma,false〉::l2 →
841 (〈b,true〉::bs = 〈b0,true〉::b0s ∧
842 t2 = midtape ? (reverse ? bs@〈b,false〉::ls)
843 〈grid,false〉 (l1@〈b0,false〉::b0s@〈comma,true〉::l2)) ∨
844 (∃la,c',d',lb,lc.c' ≠ d' ∧
845 〈b,false〉::bs = la@〈c',false〉::lb ∧
846 〈b0,false〉::b0s = la@〈d',false〉::lc ∧
847 t2 = midtape (FinProd … FSUnialpha FinBool) (reverse ? la@
853 〈d',false〉 (lc@〈comma,false〉::l2)).
855 lemma wsem_compare : WRealize ? compare R_compare.
857 lapply (sem_while ?????? sem_comp_step t i outc Hloop) [%]
858 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
859 [ #tapea whd in ⊢ (%→?); #Rfalse #ls #c #rs #Htapea %
861 [ #c' #Hc' #Hc lapply (Rfalse … Htapea) -Rfalse * >Hc
862 whd in ⊢ (??%?→?); #Hfalse destruct (Hfalse)
863 | #c' #Hc lapply (Rfalse … Htapea) -Rfalse * #_
865 | #b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1 #Hc
866 cases (Rfalse … Htapea) -Rfalse >Hc whd in ⊢ (??%?→?);#Hfalse destruct (Hfalse)
868 | #tapea #tapeb #tapec #Hleft #Hright #IH #Htapec lapply (IH Htapec) -Htapec -IH #IH
869 whd in Hleft; #ls #c #rs #Htapea cases (Hleft … Htapea) -Hleft
870 #c' * #Hc >Hc cases (true_or_false (bit_or_null c')) #Hc'
872 [ * >Hc' #H @False_ind destruct (H)
873 | * #_ #Htapeb cases (IH … Htapeb) * #_ #H #_ %
875 [#c1 #Hc1 #Heqc destruct (Heqc) <Htapeb @(H c1) %
876 |#c1 #Hfalse destruct (Hfalse)
878 |#b #b0 #bs #b0s #l1 #l2 #_ #_ #_ #_ #_ #_
879 #Heq destruct (Heq) >Hc' #Hfalse @False_ind destruct (Hfalse)
884 [ #c'' #Hc'' #Heq destruct (Heq) >Hc'' in Hc'; #H destruct (H)
885 | #c0 #Hfalse destruct (Hfalse)
887 |#b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1
888 #Heq destruct (Heq) #_ #Hrs cases Hleft -Hleft
889 [2: * >Hc' #Hfalse @False_ind destruct ] * #_
890 @(list_cases2 … Hlen)
891 [ #Hbs #Hb0s generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
892 -Hrs #Hrs normalize in Hrs; #Hleft cases (Hleft ????? Hrs ?) -Hleft
893 [ * #Heqb #Htapeb cases (IH … Htapeb) -IH * #IH #_ #_
899 @(ex_intro … [ ]) @(ex_intro … b)
900 @(ex_intro … b0) @(ex_intro … [ ])
902 [ % [ % [@sym_not_eq //| >Hbs %] | >Hb0s %]
903 | cases (IH … Htapeb) -IH * #_ #IH #_ >(IH ? (refl ??))
907 | * #b' #bitb' * #b0' #bitb0' #bs' #b0s' #Hbs #Hb0s
908 generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
909 cut (bit_or_null b' = true ∧ bit_or_null b0' = true ∧
910 bitb' = false ∧ bitb0' = false)
911 [ % [ % [ % [ >Hbs in Hbs1; #Hbs1 @(Hbs1 〈b',bitb'〉) @memb_hd
912 | >Hb0s in Hb0s1; #Hb0s1 @(Hb0s1 〈b0',bitb0'〉) @memb_hd ]
913 | >Hbs in Hbs2; #Hbs2 @(Hbs2 〈b',bitb'〉) @memb_hd ]
914 | >Hb0s in Hb0s2; #Hb0s2 @(Hb0s2 〈b0',bitb0'〉) @memb_hd ]
915 | * * * #Ha #Hb #Hc #Hd >Hc >Hd
917 cases (Hleft b' (bs'@〈grid,false〉::l1) b0 b0'
918 (b0s'@〈comma,false〉::l2) ??) -Hleft
919 [ 3: >Hrs normalize @eq_f >associative_append %
920 | * #Hb0 #Htapeb cases (IH …Htapeb) -IH * #_ #_ #IH
921 cases (IH b' b0' bs' b0s' (l1@[〈b0,false〉]) l2 ??????? Ha ?) -IH
923 [ >Hb0 @eq_f >Hbs in Heq; >Hb0s in ⊢ (%→?); #Heq
924 destruct (Heq) >Hb0s >Hc >Hd %
925 | >Houtc >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append
926 >associative_append %
928 | * #la * #c' * #d' * #lb * #lc * * * #H1 #H2 #H3 #H4 %2
929 @(ex_intro … (〈b,false〉::la)) @(ex_intro … c') @(ex_intro … d')
930 @(ex_intro … lb) @(ex_intro … lc)
931 % [ % [ % // >Hbs >Hc >H2 % | >Hb0s >Hd >H3 >Hb0 % ]
932 | >H4 >Hbs >Hb0s >Hc >Hd >Hb0 >reverse_append
933 >reverse_cons >reverse_cons
934 >associative_append >associative_append
935 >associative_append >associative_append %
937 | generalize in match Hlen; >Hbs >Hb0s
938 normalize #Hlen destruct (Hlen) @e0
939 | #c0 #Hc0 @Hbs1 >Hbs @memb_cons //
940 | #c0 #Hc0 @Hb0s1 >Hb0s @memb_cons //
941 | #c0 #Hc0 @Hbs2 >Hbs @memb_cons //
942 | #c0 #Hc0 @Hb0s2 >Hb0s @memb_cons //
943 | #c0 #Hc0 cases (memb_append … Hc0)
944 [ @Hl1 | #Hc0' >(memb_single … Hc0') % ]
946 | >associative_append >associative_append % ]
948 @(ex_intro … []) @(ex_intro … b) @(ex_intro … b0)
949 @(ex_intro … bs) @(ex_intro … b0s) %
950 [ % // % // @sym_not_eq //
951 | >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append
952 >reverse_append in Htapeb; >reverse_cons
953 >associative_append >associative_append
955 cases (IH … Htapeb) -Htapeb -IH * #_ #IH #_ @(IH ? (refl ??))
957 | #c1 #Hc1 cases (memb_append … Hc1) #Hyp
958 [ @Hbs2 >Hbs @memb_cons @Hyp
959 | cases (orb_true_l … Hyp)
968 axiom sem_compare : Realize ? compare R_compare.