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".
18 include "turing/if_machine.ma".
19 include "turing/universal/alphabet.ma".
20 include "turing/universal/tests.ma".
22 (* ADVANCE TO MARK (right)
24 sposta la testina a destra fino a raggiungere il primo carattere marcato
28 (* 0, a ≠ mark _ ⇒ 0, R
29 0, a = mark _ ⇒ 1, N *)
31 definition atm_states ≝ initN 3.
33 definition atmr_step ≝
34 λalpha:FinSet.λtest:alpha→bool.
35 mk_TM alpha atm_states
42 | false ⇒ 〈2,Some ? 〈a',R〉〉 ]])
45 definition Ratmr_step_true ≝
48 t1 = midtape alpha ls a rs ∧ test a = false ∧
49 t2 = mk_tape alpha (a::ls) (option_hd ? rs) (tail ? rs).
51 definition Ratmr_step_false ≝
54 (current alpha t1 = None ? ∨
55 (∃a.current ? t1 = Some ? a ∧ test a = true)).
58 ∀alpha,test,ls,a0,rs. test a0 = true →
59 step alpha (atmr_step alpha test)
60 (mk_config ?? 0 (midtape … ls a0 rs)) =
61 mk_config alpha (states ? (atmr_step alpha test)) 1
63 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
67 ∀alpha,test,ls,a0,rs. test a0 = false →
68 step alpha (atmr_step alpha test)
69 (mk_config ?? 0 (midtape … ls a0 rs)) =
70 mk_config alpha (states ? (atmr_step alpha test)) 2
71 (mk_tape … (a0::ls) (option_hd ? rs) (tail ? rs)).
72 #alpha #test #ls #a0 #ts #Htest normalize >Htest cases ts //
77 accRealize alpha (atmr_step alpha test)
78 2 (Ratmr_step_true alpha test) (Ratmr_step_false alpha test).
81 @(ex_intro ?? (mk_config ?? 1 (niltape ?))) %
82 [ % // #Hfalse destruct | #_ % // % % ]
83 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (leftof ? a al)))
84 % [ % // #Hfalse destruct | #_ % // % % ]
85 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (rightof ? a al)))
86 % [ % // #Hfalse destruct | #_ % // % % ]
87 | #ls #c #rs @(ex_intro ?? 2)
88 cases (true_or_false (test c)) #Htest
89 [ @(ex_intro ?? (mk_config ?? 1 ?))
92 [ whd in ⊢ (??%?); >atmr_q0_q1 //
94 | #_ % // %2 @(ex_intro ?? c) % // ]
96 | @(ex_intro ?? (mk_config ?? 2 (mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs))))
99 [ whd in ⊢ (??%?); >atmr_q0_q2 //
100 | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
103 | #Hfalse @False_ind @(absurd ?? Hfalse) %
109 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
111 (t1 = midtape alpha ls c rs →
112 ((test c = true ∧ t2 = t1) ∨
114 ∀rs1,b,rs2. rs = rs1@b::rs2 →
115 test b = true → (∀x.memb ? x rs1 = true → test x = false) →
116 t2 = midtape ? (reverse ? rs1@c::ls) b rs2))).
118 definition adv_to_mark_r ≝
119 λalpha,test.whileTM alpha (atmr_step alpha test) 2.
121 lemma wsem_adv_to_mark_r :
123 WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
124 #alpha #test #t #i #outc #Hloop
125 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
126 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
128 [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
129 #Hfalse destruct (Hfalse)
130 | * #a * #Ha #Htest #ls #c #rs #H2 %
131 >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
134 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
135 lapply (IH HRfalse) -IH #IH
136 #ls #c #rs #Htapea %2
137 cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
139 >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
140 [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
142 [ * #_ #Houtc >Houtc >Htapeb %
143 | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
144 | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
146 [ * #Hfalse >(Hmemb …) in Hfalse;
147 [ #Hft destruct (Hft)
149 | * #Htestr1 #H1 >reverse_cons >associative_append
150 @H1 // #x #Hx @Hmemb @memb_cons //
155 lemma terminate_adv_to_mark_r :
157 ∀t.Terminate alpha (adv_to_mark_r alpha test) t.
159 @(terminate_while … (sem_atmr_step alpha test))
162 [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
163 |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
164 | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
166 [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
167 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
168 % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
169 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
170 | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
171 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
178 lemma sem_adv_to_mark_r :
180 Realize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
186 marks the current character
189 definition mark_states ≝ initN 2.
192 λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
196 | Some a' ⇒ match q with
197 [ O ⇒ let 〈a'',b〉 ≝ a' in 〈1,Some ? 〈〈a'',true〉,N〉〉
198 | S q ⇒ 〈1,None ?〉 ] ])
201 definition R_mark ≝ λalpha,t1,t2.
203 t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
204 t2 = midtape ? ls 〈c,true〉 rs.
207 ∀alpha.Realize ? (mark alpha) (R_mark alpha).
208 #alpha #intape @(ex_intro ?? 2) cases intape
210 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
212 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
214 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
216 @ex_intro [| % [ % | #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ] ] ]
221 moves the head one step to the right
225 definition move_states ≝ initN 2.
228 λalpha:FinSet.mk_TM alpha move_states
232 | Some a' ⇒ match q with
233 [ O ⇒ 〈1,Some ? 〈a',R〉〉
234 | S q ⇒ 〈1,None ?〉 ] ])
237 definition R_move_r ≝ λalpha,t1,t2.
239 t1 = midtape alpha ls c rs →
240 t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
243 ∀alpha.Realize ? (move_r alpha) (R_move_r alpha).
244 #alpha #intape @(ex_intro ?? 2) cases intape
246 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
248 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
250 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
252 @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
258 moves the head one step to the right
263 λalpha:FinSet.mk_TM alpha move_states
267 | Some a' ⇒ match q with
268 [ O ⇒ 〈1,Some ? 〈a',L〉〉
269 | S q ⇒ 〈1,None ?〉 ] ])
272 definition R_move_l ≝ λalpha,t1,t2.
274 t1 = midtape alpha ls c rs →
275 t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
278 ∀alpha.Realize ? (move_l alpha) (R_move_l alpha).
279 #alpha #intape @(ex_intro ?? 2) cases intape
281 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
283 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
285 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
287 @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
291 (* MOVE RIGHT AND MARK machine
293 marks the first character on the right
295 (could be rewritten using (mark; move_right))
298 definition mrm_states ≝ initN 3.
300 definition move_right_and_mark ≝
301 λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mrm_states
305 | Some a' ⇒ match q with
306 [ O ⇒ 〈1,Some ? 〈a',R〉〉
308 [ O ⇒ let 〈a'',b〉 ≝ a' in
309 〈2,Some ? 〈〈a'',true〉,N〉〉
310 | S _ ⇒ 〈2,None ?〉 ] ] ])
313 definition R_move_right_and_mark ≝ λalpha,t1,t2.
315 t1 = midtape (FinProd … alpha FinBool) ls c (〈d,b〉::rs) →
316 t2 = midtape ? (c::ls) 〈d,true〉 rs.
318 lemma sem_move_right_and_mark :
319 ∀alpha.Realize ? (move_right_and_mark alpha) (R_move_right_and_mark alpha).
320 #alpha #intape @(ex_intro ?? 3) cases intape
322 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
324 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
326 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
328 [ @ex_intro [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #Hfalse destruct ] ]
329 | * #d #b #rs @ex_intro
330 [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #H1 destruct (H1) % ] ] ] ]
333 (* CLEAR MARK machine
335 clears the mark in the current character
338 definition clear_mark_states ≝ initN 3.
340 definition clear_mark ≝
341 λalpha:FinSet.mk_TM (FinProd … alpha FinBool) clear_mark_states
345 | Some a' ⇒ match q with
346 [ O ⇒ let 〈a'',b〉 ≝ a' in 〈1,Some ? 〈〈a'',false〉,N〉〉
347 | S q ⇒ 〈1,None ?〉 ] ])
350 definition R_clear_mark ≝ λalpha,t1,t2.
352 t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
353 t2 = midtape ? ls 〈c,false〉 rs.
355 lemma sem_clear_mark :
356 ∀alpha.Realize ? (clear_mark alpha) (R_clear_mark alpha).
357 #alpha #intape @(ex_intro ?? 2) cases intape
359 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
361 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
363 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
365 @ex_intro [| % [ % | #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ] ] ]
368 (* ADVANCE MARK RIGHT machine
370 clears mark on current char,
371 moves right, and marks new current char
375 definition adv_mark_r ≝
377 seq ? (clear_mark alpha)
378 (seq ? (move_r ?) (mark alpha)).
380 definition R_adv_mark_r ≝ λalpha,t1,t2.
382 t1 = midtape (FinProd … alpha FinBool) ls 〈c,true〉 (〈d,b〉::rs) →
383 t2 = midtape ? (〈c,false〉::ls) 〈d,true〉 rs.
385 lemma sem_adv_mark_r :
386 ∀alpha.Realize ? (adv_mark_r alpha) (R_adv_mark_r alpha).
388 cases (sem_seq ????? (sem_clear_mark …)
389 (sem_seq ????? (sem_move_r ?) (sem_mark alpha)) intape)
390 #k * #outc * #Hloop whd in ⊢ (%→?);
391 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→%→?); #Hs2 #Hs3
392 @(ex_intro ?? k) @(ex_intro ?? outc) %
394 | -Hloop #ls #c #d #b #rs #Hintape @(Hs3 … b)
395 @(Hs2 ls 〈c,false〉 (〈d,b〉::rs))
400 (* ADVANCE TO MARK (left)
406 definition R_adv_to_mark_l ≝ λalpha,test,t1,t2.
408 (t1 = midtape alpha ls c rs →
409 ((test c = true ∧ t2 = t1) ∨
411 ∀ls1,b,ls2. ls = ls1@b::ls2 →
412 test b = true → (∀x.memb ? x ls1 = true → test x = false) →
413 t2 = midtape ? ls2 b (reverse ? ls1@c::rs)))).
415 axiom adv_to_mark_l : ∀alpha:FinSet.(alpha → bool) → TM alpha.
416 (* definition adv_to_mark_l ≝
417 λalpha,test.whileTM alpha (atml_step alpha test) 2. *)
419 axiom wsem_adv_to_mark_l :
421 WRealize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
423 #alpha #test #t #i #outc #Hloop
424 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
425 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
427 [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
428 #Hfalse destruct (Hfalse)
429 | * #a * #Ha #Htest #ls #c #rs #H2 %
430 >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
433 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
434 lapply (IH HRfalse) -IH #IH
435 #ls #c #rs #Htapea %2
436 cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
438 >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
439 [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
441 [ * #_ #Houtc >Houtc >Htapeb %
442 | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
443 | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
445 [ * #Hfalse >(Hmemb …) in Hfalse;
446 [ #Hft destruct (Hft)
448 | * #Htestr1 #H1 >reverse_cons >associative_append
449 @H1 // #x #Hx @Hmemb @memb_cons //
455 axiom terminate_adv_to_mark_l :
457 ∀t.Terminate alpha (adv_to_mark_l alpha test) t.
460 @(terminate_while … (sem_atmr_step alpha test))
463 [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
464 |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
465 | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
467 [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
468 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
469 % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
470 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
471 | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
472 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
480 lemma sem_adv_to_mark_l :
482 Realize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
487 ADVANCE BOTH MARKS machine
489 l1 does not contain marks ⇒
501 definition is_marked ≝
502 λalpha.λp:FinProd … alpha FinBool.
505 definition adv_both_marks ≝
506 λalpha.seq ? (adv_mark_r alpha)
508 (seq ? (adv_to_mark_l (FinProd alpha FinBool) (is_marked alpha))
509 (adv_mark_r alpha))).
511 definition R_adv_both_marks ≝
513 ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
514 t1 = midtape (FinProd … alpha FinBool)
515 (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
516 t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2).
518 lemma sem_adv_both_marks :
519 ∀alpha.Realize ? (adv_both_marks alpha) (R_adv_both_marks alpha).
521 cases (sem_seq ????? (sem_adv_mark_r …)
522 (sem_seq ????? (sem_move_l …)
523 (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?))
524 (sem_adv_mark_r alpha))) intape)
525 #k * #outc * #Hloop whd in ⊢ (%→?);
526 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→?); #Hs2
527 * #tc * whd in ⊢ (%→%→?); #Hs3 #Hs4
528 @(ex_intro ?? k) @(ex_intro ?? outc) %
530 | -Hloop #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
532 lapply (Hs1 … Hintape) #Hta
533 lapply (Hs2 … Hta) #Htb
535 [ * #Hfalse normalize in Hfalse; destruct (Hfalse)
537 lapply (Hs3 (l1@[〈a,false〉]) 〈x,true〉 l0 ???)
538 [ #x1 #Hx1 cases (memb_append … Hx1)
540 | #Hx1' >(memb_single … Hx1') % ]
542 | >associative_append %
543 | >reverse_append #Htc @Htc ]
555 l0 x a* l1 x0 a0* l2 (f(x0) == true)
557 l0 x* a l1 x0* a0 l2 (f(x0) == false)
561 definition match_and_adv ≝
562 λalpha,f.ifTM ? (test_char ? f)
563 (adv_both_marks alpha) (clear_mark ?) tc_true.
565 definition R_match_and_adv ≝
567 ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
568 t1 = midtape (FinProd … alpha FinBool)
569 (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
570 (f 〈x0,true〉 = true ∧ t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2))
571 ∨ (f 〈x0,true〉 = false ∧
572 t2 = midtape ? (l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)).
574 lemma sem_match_and_adv :
575 ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv alpha f).
577 cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape)
578 #k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
581 [ * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
582 #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
583 >Hintape in Hta; #Hta cases (Hta … (refl ??)) -Hta #Hf #Hta % %
584 [ @Hf | @Houtc [ @Hl1 | @Hta ] ]
585 | * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
586 #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
587 >Hintape in Hta; #Hta cases (Hta … (refl ??)) -Hta #Hf #Hta %2 %
588 [ @Hf | >(Houtc … Hta) % ]
594 then move_right; ----
596 if current (* x0 *) = 0
597 then advance_mark ----
604 definition comp_step_subcase ≝
605 λalpha,c,elseM.ifTM ? (test_char ? (λx.x == c))
607 (seq ? (adv_to_mark_r ? (is_marked alpha))
608 (match_and_adv ? (λx.x == c))))
611 definition R_comp_step_subcase ≝
612 λalpha,c,RelseM,t1,t2.
613 ∀l0,x,rs.t1 = midtape (FinProd … alpha FinBool) l0 〈x,true〉 rs →
615 ∀a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
616 rs = 〈a,false〉::l1@〈x0,true〉::〈a0,false〉::l2 →
618 t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1@〈x0,false〉::〈a0,true〉::l2)) ∨
620 t2 = midtape (FinProd … alpha FinBool)
621 (reverse ? l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)))) ∨
622 (〈x,true〉 ≠ c ∧ RelseM t1 t2).
624 lemma sem_comp_step_subcase :
625 ∀alpha,c,elseM,RelseM.
626 Realize ? elseM RelseM →
627 Realize ? (comp_step_subcase alpha c elseM)
628 (R_comp_step_subcase alpha c RelseM).
629 #alpha #c #elseM #RelseM #Helse #intape
630 cases (sem_if ? (test_char ? (λx.x == c)) … tc_true
631 (sem_test_char ? (λx.x == c))
632 (sem_seq ????? (sem_move_r …)
633 (sem_seq ????? (sem_adv_to_mark_r ? (is_marked alpha))
634 (sem_match_and_adv ? (λx.x == c)))) Helse intape)
635 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc)
636 % [ @Hloop ] -Hloop cases HR -HR
637 [ * #ta * whd in ⊢ (%→?); #Hta * #tb * whd in ⊢ (%→?); #Htb
638 * #tc * whd in ⊢ (%→?); #Htc whd in ⊢ (%→?); #Houtc
639 #l0 #x #rs #Hintape cases (true_or_false (〈x,true〉==c)) #Hc
641 #a #l1 #x0 #a0 #l2 #Hl1 #Hrs >Hrs in Hintape; #Hintape
642 >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta
643 #Hx #Hta lapply (Htb … Hta) -Htb #Htb
644 cases (Htc … Htb) [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
645 -Htc * #_ #Htc lapply (Htc l1 〈x0,true〉 (〈a0,false〉::l2) (refl ??) (refl ??) Hl1)
646 -Htc #Htc cases (Houtc ???????? Htc) -Houtc
648 % [ <(\P Hx0) in Hx; #Hx lapply (\P Hx) #Hx' destruct (Hx') %
649 | >Houtc >reverse_reverse % ]
651 % [ <(\P Hx) in Hx0; #Hx0 lapply (\Pf Hx0) @not_to_not #Hx' >Hx' %
653 | (* members of lists are invariant under reverse *) @daemon ]
655 >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hx #Hta
656 >Hx in Hc;#Hc destruct (Hc) ]
657 | * #ta * whd in ⊢ (%→?); #Hta #Helse #ls #c0 #rs #Hintape %2
658 >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hc #Hta %
659 [ @(\Pf Hc) | <Hta @Helse ]
666 + se è un bit, ho fallito il confronto della tupla corrente
667 + se è un separatore, la tupla fa match
670 ifTM ? (test_char ? is_marked)
671 (single_finalTM … (comp_step_subcase unialpha 〈bit false,true〉
672 (comp_step_subcase unialpha 〈bit true,true〉
677 definition comp_step ≝
678 ifTM ? (test_char ? (is_marked ?))
679 (single_finalTM … (comp_step_subcase FSUnialpha 〈bit false,true〉
680 (comp_step_subcase FSUnialpha 〈bit true,true〉
685 definition R_comp_step_true ≝
687 ∀l0,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) l0 c rs →
691 rs = 〈a,false〉::l1@〈c0,true〉::〈a0,false〉::l2 →
692 (∀c.memb ? c l1 = true → is_marked ? c = false) →
694 t2 = midtape ? (〈c',false〉::l0) 〈a,true〉 (l1@〈c0,false〉::〈a0,true〉::l2)) ∨
696 t2 = midtape (FinProd … FSUnialpha FinBool)
697 (reverse ? l1@〈a,false〉::〈c',true〉::l0) 〈c0,false〉 (〈a0,false〉::l2))) ∨
698 (is_bit c' = false ∧ t2 = midtape ? l0 〈c',false〉 rs)).
700 definition R_comp_step_false ≝
702 ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
703 is_marked ? c = false ∧ t2 = t1.
705 lemma sem_comp_step :
706 accRealize ? comp_step (inr … (inl … (inr … 0)))
707 R_comp_step_true R_comp_step_false.
709 cases (acc_sem_if … (sem_test_char ? (is_marked ?))
710 (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
711 (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ??
714 #k * #outc * * #Hloop #H1 #H2
715 @(ex_intro ?? k) @(ex_intro ?? outc) %
716 [ % [@Hloop ] ] -Hloop
717 [ #Hstate lapply (H1 Hstate) -H1 -Hstate -H2 *
718 #ta * whd in ⊢ (%→?); #Hleft #Hright #ls #c #rs #Hintape
719 >Hintape in Hleft; #Hleft cases (Hleft ? (refl ??)) -Hleft
720 cases c in Hintape; #c' #b #Hintape whd in ⊢ (??%?→?);
721 #Hb >Hb #Hta @(ex_intro ?? c') % //
723 [ * #Hc' #H1 % % [destruct (Hc') % ]
724 #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
726 [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
727 | * #Hneq #Houtc %2 %
731 | * #Hc #Helse1 cases (Helse1 … Hta)
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' whd in ⊢ (%→?); #Helse2 %2 %
741 [ generalize in match Hc'; generalize in match Hc;
743 [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
744 | #Hfalse @False_ind @(absurd ?? Hfalse) % ]
750 | #Hstate lapply (H2 Hstate) -H1 -Hstate -H2 *
751 #ta * whd in ⊢ (%→%→?); #Hleft #Hright #ls #c #rs #Hintape
752 >Hintape in Hleft; #Hleft
753 cases (Hleft ? (refl ??)) -Hleft
754 #Hc #Hta % // >Hright //
759 whileTM ? comp_step (inr … (inl … (inr … 0))).
762 definition R_compare :=
766 ∀ls,c,b,rs.t1 = midtape ? ls 〈c,b〉 rs →
767 (b = true → rs = ....) →
771 rs = cs@l1@〈c0,true〉::cs0@l2
775 ls 〈c,b〉 cs l1 〈c0,b0〉 cs0 l2
779 ls (hd (Ls@〈grid,false〉))* (tail (Ls@〈grid,false〉)) l1 (hd (Ls@〈comma,false〉))* (tail (Ls@〈comma,false〉)) l2
780 ^^^^^^^^^^^^^^^^^^^^^^^
782 ls Ls 〈grid,false〉 l1 Ls 〈comma,true〉 l2
787 ls (hd (Ls@〈c,false〉))* (tail (Ls@〈c,false〉)) l1 (hd (Ls@〈d,false〉))* (tail (Ls@〈d,false〉)) l2
788 ^^^^^^^^^^^^^^^^^^^^^^^
791 ls Ls 〈c,true〉 l1 Ls 〈d,false〉 l2
797 (∃la,d.〈b,true〉::bs = la@[〈grid,d〉] ∧ ∀x.memb ? x la → is_bit (\fst x) = true) →
798 (∃lb,d0.〈b0,true〉::b0s = lb@[〈comma,d0〉] ∧ ∀x.memb ? x lb → is_bit (\fst x) = true) →
799 t1 = midtape ? l0 〈b,true〉 (bs@l1@〈b0,true〉::b0s@l2 →
801 mk_tape left (option current) right
803 (b = grid ∧ b0 = comma ∧ bs = [] ∧ b0s = [] ∧
804 t2 = midtape ? l0 〈grid,false〉 (l1@〈comma,true〉::l2)) ∨
805 (b = bit x ∧ b = c ∧ bs = b0s
807 definition R_compare :=
809 ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
810 (∀c'.is_bit c' = false → c = 〈c',true〉 → t2 = midtape ? ls 〈c',false〉 rs) ∧
811 (∀c'. c = 〈c',false〉 → t2 = t1) ∧
814 (∀c.memb (FinProd … FSUnialpha FinBool) c bs = true → is_bit (\fst c) = true) →
815 (∀c.memb (FinProd … FSUnialpha FinBool) c b0s = true → is_bit (\fst c) = true) →
816 (∀c.memb ? c bs = true → is_marked ? c = false) →
817 (∀c.memb ? c b0s = true → is_marked ? c = false) →
818 (∀c.memb ? c l1 = true → is_marked ? c = false) →
819 c = 〈b,true〉 → is_bit b = true →
820 rs = bs@〈grid,false〉::l1@〈b0,true〉::b0s@〈comma,false〉::l2 →
821 (〈b,true〉::bs = 〈b0,true〉::b0s ∧
822 t2 = midtape ? (reverse ? bs@〈b,false〉::ls)
823 〈grid,false〉 (l1@〈b0,false〉::b0s@〈comma,true〉::l2)) ∨
824 (∃la,c',d',lb,lc.c' ≠ d' ∧
825 〈b,false〉::bs = la@〈c',false〉::lb ∧
826 〈b0,false〉::b0s = la@〈d',false〉::lc ∧
827 t2 = midtape (FinProd … FSUnialpha FinBool) (reverse ? la@
833 〈d',false〉 (lc@〈comma,false〉::l2)).
836 ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
837 length ? l1 = length ? l2 →
839 (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) →
841 #T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
842 generalize in match Hl; generalize in match l2;
844 [#l2 cases l2 // normalize #t2 #tl2 #H destruct
845 |#t1 #tl1 #IH #l2 cases l2
846 [normalize #H destruct
847 |#t2 #tl2 #H @Pcons @IH normalize in H; destruct // ]
852 ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:Prop.
853 length ? l1 = length ? l2 →
854 (l1 = [] → l2 = [] → P) →
855 (∀hd1,hd2,tl1,tl2.l1 = hd1::tl1 → l2 = hd2::tl2 → P) → P.
856 #T1 #T2 #l1 #l2 #P #Hl @(list_ind2 … Hl)
857 [ #Pnil #Pcons @Pnil //
858 | #tl1 #tl2 #hd1 #hd2 #IH1 #IH2 #Hp @Hp // ]
861 lemma wsem_compare : WRealize ? compare R_compare.
863 lapply (sem_while ?????? sem_comp_step t i outc Hloop) [%]
864 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
865 [ #tapea whd in ⊢ (%→?); #Rfalse #ls #c #rs #Htapea %
867 [ #c' #Hc' #Hc lapply (Rfalse … Htapea) -Rfalse * >Hc
868 whd in ⊢ (??%?→?); #Hfalse destruct (Hfalse)
869 | #c' #Hc lapply (Rfalse … Htapea) -Rfalse * #_
871 | #b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1 #Hc
872 cases (Rfalse … Htapea) -Rfalse >Hc whd in ⊢ (??%?→?);#Hfalse destruct (Hfalse)
874 | #tapea #tapeb #tapec #Hleft #Hright #IH #Htapec lapply (IH Htapec) -Htapec -IH #IH
875 whd in Hleft; #ls #c #rs #Htapea cases (Hleft … Htapea) -Hleft
876 #c' * #Hc >Hc cases (true_or_false (is_bit c')) #Hc'
878 [ * >Hc' #H @False_ind destruct (H)
879 | * #_ #Htapeb cases (IH … Htapeb) * #_ #H #_ %
881 [#c1 #Hc1 #Heqc destruct (Heqc) <Htapeb @(H c1) %
882 |#c1 #Hfalse destruct (Hfalse)
884 |#b #b0 #bs #b0s #l1 #l2 #_ #_ #_ #_ #_ #_
885 #Heq destruct (Heq) >Hc' #Hfalse @False_ind destruct (Hfalse)
890 [ #c'' #Hc'' #Heq destruct (Heq) >Hc'' in Hc'; #H destruct (H)
891 | #c0 #Hfalse destruct (Hfalse)
893 |#b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1
894 #Heq destruct (Heq) #_ #Hrs cases Hleft -Hleft
895 [2: * >Hc' #Hfalse @False_ind destruct ] * #_
896 @(list_cases_2 … Hlen)
897 [ #Hbs #Hb0s generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
898 -Hrs #Hrs normalize in Hrs; #Hleft cases (Hleft ????? Hrs ?) -Hleft
899 [ * #Heqb #Htapeb cases (IH … Htapeb) -IH * #IH #_ #_
905 @(ex_intro … [ ]) @(ex_intro … b)
906 @(ex_intro … b0) @(ex_intro … [ ])
908 [ % [ % [@sym_not_eq //| >Hbs %] | >Hb0s %]
909 | cases (IH … Htapeb) -IH * #_ #IH #_ >(IH ? (refl ??))
913 | * #b' #bitb' * #b0' #bitb0' #bs' #b0s' #Hbs #Hb0s
914 generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
915 cut (is_bit b' = true ∧ is_bit b0' = true ∧
916 bitb' = false ∧ bitb0' = false)
917 [ % [ % [ % [ >Hbs in Hbs1; #Hbs1 @(Hbs1 〈b',bitb'〉) @memb_hd
918 | >Hb0s in Hb0s1; #Hb0s1 @(Hb0s1 〈b0',bitb0'〉) @memb_hd ]
919 | >Hbs in Hbs2; #Hbs2 @(Hbs2 〈b',bitb'〉) @memb_hd ]
920 | >Hb0s in Hb0s2; #Hb0s2 @(Hb0s2 〈b0',bitb0'〉) @memb_hd ]
921 | * * * #Ha #Hb #Hc #Hd >Hc >Hd
923 cases (Hleft b' (bs'@〈grid,false〉::l1) b0 b0'
924 (b0s'@〈comma,false〉::l2) ??) -Hleft
925 [ 3: >Hrs normalize @eq_f >associative_append %
926 | * #Hb0 #Htapeb cases (IH …Htapeb) -IH * #_ #_ #IH
927 cases (IH b' b0' bs' b0s' (l1@[〈b0,false〉]) l2 ??????? Ha ?) -IH
929 [ >Hb0 @eq_f >Hbs in Heq; >Hb0s in ⊢ (%→?); #Heq
930 destruct (Heq) >Hb0s >Hc >Hd %
931 | >Houtc >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append
932 >associative_append %
934 | * #la * #c' * #d' * #lb * #lc * * * #H1 #H2 #H3 #H4 %2
935 @(ex_intro … (〈b,false〉::la)) @(ex_intro … c') @(ex_intro … d')
936 @(ex_intro … lb) @(ex_intro … lc)
937 % [ % [ % // >Hbs >Hc >H2 % | >Hb0s >Hd >H3 >Hb0 % ]
938 | >H4 >Hbs >Hb0s >Hc >Hd >Hb0 >reverse_append
939 >reverse_cons >reverse_cons
940 >associative_append >associative_append
941 >associative_append >associative_append %
943 | generalize in match Hlen; >Hbs >Hb0s
944 normalize #Hlen destruct (Hlen) @e0
945 | #c0 #Hc0 @Hbs1 >Hbs @memb_cons //
946 | #c0 #Hc0 @Hb0s1 >Hb0s @memb_cons //
947 | #c0 #Hc0 @Hbs2 >Hbs @memb_cons //
948 | #c0 #Hc0 @Hb0s2 >Hb0s @memb_cons //
949 | #c0 #Hc0 cases (memb_append … Hc0)
950 [ @Hl1 | #Hc0' >(memb_single … Hc0') % ]
952 | >associative_append >associative_append % ]
954 @(ex_intro … []) @(ex_intro … b) @(ex_intro … b0)
955 @(ex_intro … bs) @(ex_intro … b0s) %
956 [ % // % // @sym_not_eq //
957 | >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append
958 >reverse_append in Htapeb; >reverse_cons
959 >associative_append >associative_append
961 cases (IH … Htapeb) -Htapeb -IH * #_ #IH #_ @(IH ? (refl ??))
963 | #c1 #Hc1 cases (memb_append … Hc1) #Hyp
964 [ @Hbs2 >Hbs @memb_cons @Hyp
965 | cases (orb_true_l … Hyp)
974 axiom sem_compare : Realize ? compare R_compare.