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/tests.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 atmr_step ≝
33 λalpha:FinSet.λtest:alpha→bool.
34 mk_TM alpha atm_states
41 | false ⇒ 〈2,Some ? 〈a',R〉〉 ]])
44 definition Ratmr_step_true ≝
47 t1 = midtape alpha ls a rs ∧ test a = false ∧
48 t2 = mk_tape alpha (a::ls) (option_hd ? rs) (tail ? rs).
50 definition Ratmr_step_false ≝
53 (current alpha t1 = None ? ∨
54 (∃a.current ? t1 = Some ? a ∧ test a = true)).
57 ∀alpha,test,ls,a0,rs. test a0 = true →
58 step alpha (atmr_step alpha test)
59 (mk_config ?? 0 (midtape … ls a0 rs)) =
60 mk_config alpha (states ? (atmr_step alpha test)) 1
62 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
66 ∀alpha,test,ls,a0,rs. test a0 = false →
67 step alpha (atmr_step alpha test)
68 (mk_config ?? 0 (midtape … ls a0 rs)) =
69 mk_config alpha (states ? (atmr_step alpha test)) 2
70 (mk_tape … (a0::ls) (option_hd ? rs) (tail ? rs)).
71 #alpha #test #ls #a0 #ts #Htest normalize >Htest cases ts //
76 accRealize alpha (atmr_step alpha test)
77 2 (Ratmr_step_true alpha test) (Ratmr_step_false alpha test).
80 @(ex_intro ?? (mk_config ?? 1 (niltape ?))) %
81 [ % // #Hfalse destruct | #_ % // % % ]
82 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (leftof ? a al)))
83 % [ % // #Hfalse destruct | #_ % // % % ]
84 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (rightof ? a al)))
85 % [ % // #Hfalse destruct | #_ % // % % ]
86 | #ls #c #rs @(ex_intro ?? 2)
87 cases (true_or_false (test c)) #Htest
88 [ @(ex_intro ?? (mk_config ?? 1 ?))
91 [ whd in ⊢ (??%?); >atmr_q0_q1 //
93 | #_ % // %2 @(ex_intro ?? c) % // ]
95 | @(ex_intro ?? (mk_config ?? 2 (mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs))))
98 [ whd in ⊢ (??%?); >atmr_q0_q2 //
99 | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
102 | #Hfalse @False_ind @(absurd ?? Hfalse) %
108 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
110 (t1 = midtape alpha ls c rs →
111 ((test c = true ∧ t2 = t1) ∨
113 ∀rs1,b,rs2. rs = rs1@b::rs2 →
114 test b = true → (∀x.memb ? x rs1 = true → test x = false) →
115 t2 = midtape ? (reverse ? rs1@c::ls) b rs2))).
117 definition adv_to_mark_r ≝
118 λalpha,test.whileTM alpha (atmr_step alpha test) 2.
120 lemma wsem_adv_to_mark_r :
122 WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
123 #alpha #test #t #i #outc #Hloop
124 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
125 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
127 [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
128 #Hfalse destruct (Hfalse)
129 | * #a * #Ha #Htest #ls #c #rs #H2 %
130 >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
133 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
134 lapply (IH HRfalse) -IH #IH
135 #ls #c #rs #Htapea %2
136 cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
138 >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
139 [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
141 [ * #_ #Houtc >Houtc >Htapeb %
142 | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
143 | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
145 [ * #Hfalse >(Hmemb …) in Hfalse;
146 [ #Hft destruct (Hft)
148 | * #Htestr1 #H1 >reverse_cons >associative_append
149 @H1 // #x #Hx @Hmemb @memb_cons //
154 lemma terminate_adv_to_mark_r :
156 ∀t.Terminate alpha (adv_to_mark_r alpha test) t.
158 @(terminate_while … (sem_atmr_step alpha test))
161 [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
162 |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
163 | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
165 [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
166 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
167 % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
168 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
169 | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
170 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
177 lemma sem_adv_to_mark_r :
179 Realize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
185 marks the current character
188 definition mark_states ≝ initN 2.
191 λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
195 | Some a' ⇒ match q with
196 [ O ⇒ let 〈a'',b〉 ≝ a' in 〈1,Some ? 〈〈a'',true〉,N〉〉
197 | S q ⇒ 〈1,None ?〉 ] ])
200 definition R_mark ≝ λalpha,t1,t2.
202 t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
203 t2 = midtape ? ls 〈c,true〉 rs.
206 ∀alpha.Realize ? (mark alpha) (R_mark alpha).
207 #alpha #intape @(ex_intro ?? 2) cases intape
209 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
211 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
213 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
215 @ex_intro [| % [ % | #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ] ] ]
220 moves the head one step to the right
224 definition move_states ≝ initN 2.
227 λalpha:FinSet.mk_TM alpha move_states
231 | Some a' ⇒ match q with
232 [ O ⇒ 〈1,Some ? 〈a',R〉〉
233 | S q ⇒ 〈1,None ?〉 ] ])
236 definition R_move_r ≝ λalpha,t1,t2.
238 t1 = midtape alpha ls c rs →
239 t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
242 ∀alpha.Realize ? (move_r alpha) (R_move_r alpha).
243 #alpha #intape @(ex_intro ?? 2) cases intape
245 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
247 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
249 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
251 @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
257 moves the head one step to the right
262 λalpha:FinSet.mk_TM alpha move_states
266 | Some a' ⇒ match q with
267 [ O ⇒ 〈1,Some ? 〈a',L〉〉
268 | S q ⇒ 〈1,None ?〉 ] ])
271 definition R_move_l ≝ λalpha,t1,t2.
273 t1 = midtape alpha ls c rs →
274 t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
277 ∀alpha.Realize ? (move_l alpha) (R_move_l alpha).
278 #alpha #intape @(ex_intro ?? 2) cases intape
280 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
282 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
284 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
286 @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
290 (* MOVE RIGHT AND MARK machine
292 marks the first character on the right
294 (could be rewritten using (mark; move_right))
297 definition mrm_states ≝ initN 3.
299 definition move_right_and_mark ≝
300 λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mrm_states
304 | Some a' ⇒ match q with
305 [ O ⇒ 〈1,Some ? 〈a',R〉〉
307 [ O ⇒ let 〈a'',b〉 ≝ a' in
308 〈2,Some ? 〈〈a'',true〉,N〉〉
309 | S _ ⇒ 〈2,None ?〉 ] ] ])
312 definition R_move_right_and_mark ≝ λalpha,t1,t2.
314 t1 = midtape (FinProd … alpha FinBool) ls c (〈d,b〉::rs) →
315 t2 = midtape ? (c::ls) 〈d,true〉 rs.
317 lemma sem_move_right_and_mark :
318 ∀alpha.Realize ? (move_right_and_mark alpha) (R_move_right_and_mark alpha).
319 #alpha #intape @(ex_intro ?? 3) cases intape
321 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
323 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
325 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
327 [ @ex_intro [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #Hfalse destruct ] ]
328 | * #d #b #rs @ex_intro
329 [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #H1 destruct (H1) % ] ] ] ]
332 (* CLEAR MARK machine
334 clears the mark in the current character
337 definition clear_mark_states ≝ initN 3.
339 definition clear_mark ≝
340 λalpha:FinSet.mk_TM (FinProd … alpha FinBool) clear_mark_states
344 | Some a' ⇒ match q with
345 [ O ⇒ let 〈a'',b〉 ≝ a' in 〈1,Some ? 〈〈a'',false〉,N〉〉
346 | S q ⇒ 〈1,None ?〉 ] ])
349 definition R_clear_mark ≝ λalpha,t1,t2.
351 t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
352 t2 = midtape ? ls 〈c,false〉 rs.
354 lemma sem_clear_mark :
355 ∀alpha.Realize ? (clear_mark alpha) (R_clear_mark alpha).
356 #alpha #intape @(ex_intro ?? 2) cases intape
358 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
360 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
362 [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
364 @ex_intro [| % [ % | #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ] ] ]
367 (* ADVANCE MARK RIGHT machine
369 clears mark on current char,
370 moves right, and marks new current char
374 definition adv_mark_r ≝
376 seq ? (clear_mark alpha)
377 (seq ? (move_r ?) (mark alpha)).
379 definition R_adv_mark_r ≝ λalpha,t1,t2.
381 t1 = midtape (FinProd … alpha FinBool) ls 〈c,true〉 (〈d,b〉::rs) →
382 t2 = midtape ? (〈c,false〉::ls) 〈d,true〉 rs.
384 lemma sem_adv_mark_r :
385 ∀alpha.Realize ? (adv_mark_r alpha) (R_adv_mark_r alpha).
387 cases (sem_seq ????? (sem_clear_mark …)
388 (sem_seq ????? (sem_move_r ?) (sem_mark alpha)) intape)
389 #k * #outc * #Hloop whd in ⊢ (%→?);
390 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→%→?); #Hs2 #Hs3
391 @(ex_intro ?? k) @(ex_intro ?? outc) %
393 | -Hloop #ls #c #d #b #rs #Hintape @(Hs3 … b)
394 @(Hs2 ls 〈c,false〉 (〈d,b〉::rs))
399 (* ADVANCE TO MARK (left)
405 definition R_adv_to_mark_l ≝ λalpha,test,t1,t2.
407 (t1 = midtape alpha ls c rs →
408 ((test c = true ∧ t2 = t1) ∨
410 ∀ls1,b,ls2. ls = ls1@b::ls2 →
411 test b = true → (∀x.memb ? x ls1 = true → test x = false) →
412 t2 = midtape ? ls2 b (reverse ? ls1@c::rs)))).
414 axiom adv_to_mark_l : ∀alpha:FinSet.(alpha → bool) → TM alpha.
415 (* definition adv_to_mark_l ≝
416 λalpha,test.whileTM alpha (atml_step alpha test) 2. *)
418 axiom wsem_adv_to_mark_l :
420 WRealize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
422 #alpha #test #t #i #outc #Hloop
423 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
424 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
426 [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
427 #Hfalse destruct (Hfalse)
428 | * #a * #Ha #Htest #ls #c #rs #H2 %
429 >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
432 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
433 lapply (IH HRfalse) -IH #IH
434 #ls #c #rs #Htapea %2
435 cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
437 >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
438 [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
440 [ * #_ #Houtc >Houtc >Htapeb %
441 | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
442 | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
444 [ * #Hfalse >(Hmemb …) in Hfalse;
445 [ #Hft destruct (Hft)
447 | * #Htestr1 #H1 >reverse_cons >associative_append
448 @H1 // #x #Hx @Hmemb @memb_cons //
454 axiom terminate_adv_to_mark_l :
456 ∀t.Terminate alpha (adv_to_mark_l alpha test) t.
459 @(terminate_while … (sem_atmr_step alpha test))
462 [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
463 |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
464 | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
466 [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
467 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
468 % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
469 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
470 | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
471 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
479 lemma sem_adv_to_mark_l :
481 Realize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
486 ADVANCE BOTH MARKS machine
488 l1 does not contain marks ⇒
500 definition is_marked ≝
501 λalpha.λp:FinProd … alpha FinBool.
504 definition adv_both_marks ≝
505 λalpha.seq ? (adv_mark_r alpha)
507 (seq ? (adv_to_mark_l (FinProd alpha FinBool) (is_marked alpha))
508 (adv_mark_r alpha))).
510 definition R_adv_both_marks ≝
512 ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
513 t1 = midtape (FinProd … alpha FinBool)
514 (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
515 t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2).
517 lemma sem_adv_both_marks :
518 ∀alpha.Realize ? (adv_both_marks alpha) (R_adv_both_marks alpha).
520 cases (sem_seq ????? (sem_adv_mark_r …)
521 (sem_seq ????? (sem_move_l …)
522 (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?))
523 (sem_adv_mark_r alpha))) intape)
524 #k * #outc * #Hloop whd in ⊢ (%→?);
525 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→?); #Hs2
526 * #tc * whd in ⊢ (%→%→?); #Hs3 #Hs4
527 @(ex_intro ?? k) @(ex_intro ?? outc) %
529 | -Hloop #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
531 lapply (Hs1 … Hintape) #Hta
532 lapply (Hs2 … Hta) #Htb
534 [ * #Hfalse normalize in Hfalse; destruct (Hfalse)
536 lapply (Hs3 (l1@[〈a,false〉]) 〈x,true〉 l0 ???)
537 [ #x1 #Hx1 cases (memb_append … Hx1)
539 | #Hx1' >(memb_single … Hx1') % ]
541 | >associative_append %
542 | >reverse_append #Htc @Htc ]
546 inductive unialpha : Type[0] ≝
547 | bit : bool → unialpha
552 definition unialpha_eq ≝
554 [ bit x ⇒ match a2 with [ bit y ⇒ ¬ xorb x y | _ ⇒ false ]
555 | comma ⇒ match a2 with [ comma ⇒ true | _ ⇒ false ]
556 | bar ⇒ match a2 with [ bar ⇒ true | _ ⇒ false ]
557 | grid ⇒ match a2 with [ grid ⇒ true | _ ⇒ false ] ].
559 definition DeqUnialpha ≝ mk_DeqSet unialpha unialpha_eq ?.
560 * [ #x * [ #y cases x cases y normalize % // #Hfalse destruct
561 | *: normalize % #Hfalse destruct ]
562 |*: * [1,5,9,13: #y ] normalize % #H1 destruct % ]
565 definition FSUnialpha ≝
566 mk_FinSet DeqUnialpha [bit true;bit false;comma;bar;grid] ?.
578 l0 x a* l1 x0 a0* l2 (f(x0) == true)
580 l0 x* a l1 x0* a0 l2 (f(x0) == false)
584 definition match_and_adv ≝
585 λalpha,f.ifTM ? (test_char ? f)
586 (adv_both_marks alpha) (clear_mark ?) tc_true.
588 definition R_match_and_adv ≝
590 ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
591 t1 = midtape (FinProd … alpha FinBool)
592 (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
593 (f 〈x0,true〉 = true ∧ t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2))
594 ∨ (f 〈x0,true〉 = false ∧
595 t2 = midtape ? (l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)).
597 lemma sem_match_and_adv :
598 ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv alpha f).
600 cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape)
601 #k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
604 [ * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
605 #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
606 >Hintape in Hta; #Hta cases (Hta … (refl ??)) -Hta #Hf #Hta % %
607 [ @Hf | @Houtc [ @Hl1 | @Hta ] ]
608 | * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
609 #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
610 >Hintape in Hta; #Hta cases (Hta … (refl ??)) -Hta #Hf #Hta %2 %
611 [ @Hf | >(Houtc … Hta) % ]
617 then move_right; ----
619 if current (* x0 *) = 0
620 then advance_mark ----
627 definition comp_step_subcase ≝
628 λalpha,c,elseM.ifTM ? (test_char ? (λx.x == c))
630 (seq ? (adv_to_mark_r ? (is_marked alpha))
631 (match_and_adv ? (λx.x == c))))
634 definition R_comp_step_subcase ≝
635 λalpha,c,RelseM,t1,t2.
636 ∀l0,x,rs.t1 = midtape (FinProd … alpha FinBool) l0 〈x,true〉 rs →
638 ∀a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
639 rs = 〈a,false〉::l1@〈x0,true〉::〈a0,false〉::l2 →
641 t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1@〈x0,false〉::〈a0,true〉::l2)) ∨
643 t2 = midtape (FinProd … alpha FinBool)
644 (reverse ? l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)))) ∨
645 (〈x,true〉 ≠ c ∧ RelseM t1 t2).
647 lemma sem_comp_step_subcase :
648 ∀alpha,c,elseM,RelseM.
649 Realize ? elseM RelseM →
650 Realize ? (comp_step_subcase alpha c elseM)
651 (R_comp_step_subcase alpha c RelseM).
652 #alpha #c #elseM #RelseM #Helse #intape
653 cases (sem_if ? (test_char ? (λx.x == c)) … tc_true
654 (sem_test_char ? (λx.x == c))
655 (sem_seq ????? (sem_move_r …)
656 (sem_seq ????? (sem_adv_to_mark_r ? (is_marked alpha))
657 (sem_match_and_adv ? (λx.x == c)))) Helse intape)
658 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc)
659 % [ @Hloop ] -Hloop cases HR -HR
660 [ * #ta * whd in ⊢ (%→?); #Hta * #tb * whd in ⊢ (%→?); #Htb
661 * #tc * whd in ⊢ (%→?); #Htc whd in ⊢ (%→?); #Houtc
662 #l0 #x #rs #Hintape cases (true_or_false (〈x,true〉==c)) #Hc
664 #a #l1 #x0 #a0 #l2 #Hl1 #Hrs >Hrs in Hintape; #Hintape
665 >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta
666 #Hx #Hta lapply (Htb … Hta) -Htb #Htb
667 cases (Htc … Htb) [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
668 -Htc * #_ #Htc lapply (Htc l1 〈x0,true〉 (〈a0,false〉::l2) (refl ??) (refl ??) Hl1)
669 -Htc #Htc cases (Houtc ???????? Htc) -Houtc
671 % [ <(\P Hx0) in Hx; #Hx lapply (\P Hx) #Hx' destruct (Hx') %
672 | >Houtc >reverse_reverse % ]
674 % [ <(\P Hx) in Hx0; #Hx0 lapply (\Pf Hx0) @not_to_not #Hx' >Hx' %
676 | (* members of lists are invariant under reverse *) @daemon ]
678 >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hx #Hta
679 >Hx in Hc;#Hc destruct (Hc) ]
680 | * #ta * whd in ⊢ (%→?); #Hta #Helse #ls #c0 #rs #Hintape %2
681 >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hc #Hta %
682 [ @(\Pf Hc) | <Hta @Helse ]
689 + se è un bit, ho fallito il confronto della tupla corrente
690 + se è un separatore, la tupla fa match
693 ifTM ? (test_char ? is_marked)
694 (single_finalTM … (comp_step_subcase unialpha 〈bit false,true〉
695 (comp_step_subcase unialpha 〈bit true,true〉
700 definition comp_step ≝
701 ifTM ? (test_char ? (is_marked ?))
702 (single_finalTM … (comp_step_subcase FSUnialpha 〈bit false,true〉
703 (comp_step_subcase FSUnialpha 〈bit true,true〉
708 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
710 definition R_comp_step_true ≝
712 ∀l0,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) l0 c rs →
716 rs = 〈a,false〉::l1@〈c0,true〉::〈a0,false〉::l2 →
717 (∀c.memb ? c l1 = true → is_marked ? c = false) →
719 t2 = midtape ? (〈c',false〉::l0) 〈a,true〉 (l1@〈c0,false〉::〈a0,true〉::l2)) ∨
721 t2 = midtape (FinProd … FSUnialpha FinBool)
722 (reverse ? l1@〈a,false〉::〈c',true〉::l0) 〈c0,false〉 (〈a0,false〉::l2))) ∨
723 (is_bit c' = false ∧ t2 = midtape ? l0 〈c',false〉 rs)).
725 definition R_comp_step_false ≝
727 ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
728 is_marked ? c = false ∧ t2 = t1.
730 lemma sem_comp_step :
731 accRealize ? comp_step (inr … (inl … (inr … 0)))
732 R_comp_step_true R_comp_step_false.
734 cases (acc_sem_if … (sem_test_char ? (is_marked ?))
735 (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
736 (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ??
739 #k * #outc * * #Hloop #H1 #H2
740 @(ex_intro ?? k) @(ex_intro ?? outc) %
741 [ % [@Hloop ] ] -Hloop
742 [ #Hstate lapply (H1 Hstate) -H1 -Hstate -H2 *
743 #ta * whd in ⊢ (%→?); #Hleft #Hright #ls #c #rs #Hintape
744 >Hintape in Hleft; #Hleft cases (Hleft ? (refl ??)) -Hleft
745 cases c in Hintape; #c' #b #Hintape whd in ⊢ (??%?→?);
746 #Hb >Hb #Hta @(ex_intro ?? c') % //
748 [ * #Hc' #H1 % % [destruct (Hc') % ]
749 #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
751 [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
752 | * #Hneq #Houtc %2 %
756 | * #Hc #Helse1 cases (Helse1 … Hta)
757 [ * #Hc' #H1 % % [destruct (Hc') % ]
758 #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
760 [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
761 | * #Hneq #Houtc %2 %
765 | * #Hc' whd in ⊢ (%→?); #Helse2 %2 %
766 [ generalize in match Hc'; generalize in match Hc;
768 [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
769 | #Hfalse @False_ind @(absurd ?? Hfalse) % ]
775 | #Hstate lapply (H2 Hstate) -H1 -Hstate -H2 *
776 #ta * whd in ⊢ (%→%→?); #Hleft #Hright #ls #c #rs #Hintape
777 >Hintape in Hleft; #Hleft
778 cases (Hleft ? (refl ??)) -Hleft
779 #Hc #Hta % // >Hright //
784 whileTM ? comp_step (inr … (inl … (inr … 0))).
787 definition R_compare :=
791 ∀ls,c,b,rs.t1 = midtape ? ls 〈c,b〉 rs →
792 (b = true → rs = ....) →
796 rs = cs@l1@〈c0,true〉::cs0@l2
800 ls 〈c,b〉 cs l1 〈c0,b0〉 cs0 l2
804 ls (hd (Ls@〈grid,false〉))* (tail (Ls@〈grid,false〉)) l1 (hd (Ls@〈comma,false〉))* (tail (Ls@〈comma,false〉)) l2
805 ^^^^^^^^^^^^^^^^^^^^^^^
807 ls Ls 〈grid,false〉 l1 Ls 〈comma,true〉 l2
812 ls (hd (Ls@〈c,false〉))* (tail (Ls@〈c,false〉)) l1 (hd (Ls@〈d,false〉))* (tail (Ls@〈d,false〉)) l2
813 ^^^^^^^^^^^^^^^^^^^^^^^
816 ls Ls 〈c,true〉 l1 Ls 〈d,false〉 l2
822 (∃la,d.〈b,true〉::bs = la@[〈grid,d〉] ∧ ∀x.memb ? x la → is_bit (\fst x) = true) →
823 (∃lb,d0.〈b0,true〉::b0s = lb@[〈comma,d0〉] ∧ ∀x.memb ? x lb → is_bit (\fst x) = true) →
824 t1 = midtape ? l0 〈b,true〉 (bs@l1@〈b0,true〉::b0s@l2 →
826 mk_tape left (option current) right
828 (b = grid ∧ b0 = comma ∧ bs = [] ∧ b0s = [] ∧
829 t2 = midtape ? l0 〈grid,false〉 (l1@〈comma,true〉::l2)) ∨
830 (b = bit x ∧ b = c ∧ bs = b0s
832 definition R_compare :=
834 ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
835 (c = 〈grid,true〉 → t2 = midtape ? ls 〈grid,false〉 rs) ∧
836 (∀c'. c = 〈c',false〉 → t2 = t1) ∧
839 (∀c.memb (FinProd … FSUnialpha FinBool) c bs = true → is_bit (\fst c) = true) →
840 (∀c.memb (FinProd … FSUnialpha FinBool) c b0s = true → is_bit (\fst c) = true) →
841 (∀c.memb ? c bs = true → is_marked ? c = false) →
842 (∀c.memb ? c b0s = true → is_marked ? c = false) →
843 (∀c.memb ? c l1 = true → is_marked ? c = false) →
845 rs = bs@〈grid,false〉::l1@〈b0,true〉::b0s@〈comma,false〉::l2 →
846 (〈b,true〉::bs = 〈b0,true〉::b0s ∧
847 ∀l3,c.〈b0,false〉::b0s = l3@[〈c,false〉] →
848 t2 = midtape ? (reverse ? bs@〈b,false〉::ls)
849 〈grid,false〉 (l1@l3@〈c,true〉::〈comma,false〉::l2)) ∨
850 (∃la,c',d',lb,lc.c' ≠ d' ∧
851 〈b,false〉::bs = la@〈c',false〉::lb ∧
852 〈b0,false〉::b0s = la@〈d',false〉::lc ∧
853 t2 = midtape (FinProd … FSUnialpha FinBool) (reverse ? la@
859 〈d',false〉 (lc@〈comma,false〉::l2)).
862 ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
863 length ? l1 = length ? l2 →
865 (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) →
867 #T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
868 generalize in match Hl; generalize in match l2;
870 [#l2 cases l2 // normalize #t2 #tl2 #H destruct
871 |#t1 #tl1 #IH #l2 cases l2
872 [normalize #H destruct
873 |#t2 #tl2 #H @Pcons @IH normalize in H; destruct // ]
878 ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:Prop.
879 length ? l1 = length ? l2 →
880 (l1 = [] → l2 = [] → P) →
881 (∀hd1,hd2,tl1,tl2.l1 = hd1::tl1 → l2 = hd2::tl2 → P) → P.
882 #T1 #T2 #l1 #l2 #P #Hl @(list_ind2 … Hl)
883 [ #Pnil #Pcons @Pnil //
884 | #tl1 #tl2 #hd1 #hd2 #IH1 #IH2 #Hp @Hp // ]
887 lemma wsem_compare : WRealize ? compare R_compare.
889 lapply (sem_while ?????? sem_comp_step t i outc Hloop) [%]
890 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
891 [ #tapea whd in ⊢ (%→?); #Hsem #ls #c #rs #Htapea %
893 [ #Hc lapply (Hsem … Htapea) -Hsem * >Hc
894 whd in ⊢ (??%?→?); #Hfalse destruct (Hfalse)
895 | #c' #Hc lapply (Hsem … Htapea) -Hsem * #_
897 | #b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1 #Hc
898 cases (Hsem … Htapea) -Hsem >Hc whd in ⊢ (??%?→?);#Hfalse destruct (Hfalse)
900 | #tapea #tapeb #tapec #Hleft #Hright #IH #Htapec lapply (IH Htapec) -IH #IH
901 whd in Hleft; #ls #c #rs #Htapea cases (Hleft … Htapea) -Hleft
902 #c' * #Hc destruct (Hc) *
903 [ * #Hc' STOP cases tapeb
906 @(list_cases_2 … Hlen)
907 [ #Hbs #Hb0s destruct (Hbs Hb0s)
908 cases (Htapeb grid l1 b0 comma l2 (refl ??) ?) -Htapeb
909 [ * #Hb0c #Htapeb % %
911 | #l3 #c0 #Hl3 whd in Htapec;
917 #b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1
918 #Htapea cases (Hleft … Htapea) -Hleft
919 #c * #Hc destruct (Hc) *
920 [ * #Hc #Htapeb @(list_cases_2 … Hlen)
921 [ #Hbs #Hb0s destruct (Hbs Hb0s)
922 cases (Htapeb grid l1 b0 comma l2 (refl ??) ?) -Htapeb
923 [ * #Hb0c #Htapeb % %
925 | #l3 #c0 #Hl3 whd in Htapec;
928 =midtape (FinProd FSUnialpha FinBool) l0 〈b,true〉
929 (bs@〈grid,false〉::l1@〈b0,true〉::b0s@〈comma,false〉::l2)
934 lapply (IH HRfalse) -IH #IH
935 #ls #c #rs #Htapea %2
936 cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
938 >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
939 [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
941 [ * #_ #Houtc >Houtc >Htapeb %
942 | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
943 | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
945 [ * #Hfalse >(Hmemb …) in Hfalse;
946 [ #Hft destruct (Hft)
948 | * #Htestr1 #H1 >reverse_cons >associative_append
949 @H1 // #x #Hx @Hmemb @memb_cons //
957 l0 x* a l1 x0* a0 l2 ------> l0 x a* l1 x0 a0* l2
960 if current (* x *) = #
963 then move_right; ----
965 if current (* x0 *) = 0
966 then advance_mark ----
970 else x = 1 (* analogo *)
976 MARK NEXT TUPLE machine
977 (partially axiomatized)
979 marks the first character after the first bar (rightwards)
982 axiom myalpha : FinSet.
983 axiom is_bar : FinProd … myalpha FinBool → bool.
984 axiom is_grid : FinProd … myalpha FinBool → bool.
985 definition bar_or_grid ≝ λc.is_bar c ∨ is_grid c.
986 axiom bar : FinProd … myalpha FinBool.
987 axiom grid : FinProd … myalpha FinBool.
989 definition mark_next_tuple ≝
990 seq ? (adv_to_mark_r ? bar_or_grid)
991 (ifTM ? (test_char ? is_bar)
992 (move_r_and_mark ?) (nop ?) 1).
994 definition R_mark_next_tuple ≝
997 (* c non può essere un separatore ... speriamo *)
998 t1 = midtape ? ls c (rs1@grid::rs2) →
999 memb ? grid rs1 = false → bar_or_grid c = false →
1000 (∃rs3,rs4,d,b.rs1 = rs3 @ bar :: rs4 ∧
1001 memb ? bar rs3 = false ∧
1002 Some ? 〈d,b〉 = option_hd ? (rs4@grid::rs2) ∧
1003 t2 = midtape ? (bar::reverse ? rs3@c::ls) 〈d,true〉 (tail ? (rs4@grid::rs2)))
1005 (memb ? bar rs1 = false ∧
1006 t2 = midtape ? (reverse ? rs1@c::ls) grid rs2).
1010 (∀x.memb A x l = true → f x = false) ∨
1011 (∃l1,c,l2.f c = true ∧ l = l1@c::l2 ∧ ∀x.memb ? x l1 = true → f c = false).
1013 [ % #x normalize #Hfalse *)
1015 theorem sem_mark_next_tuple :
1016 Realize ? mark_next_tuple R_mark_next_tuple.
1018 lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid)
1019 (ifTM ? (test_char ? is_bar) (mark ?) (nop ?) 1) ????)
1022 |||#Hif cases (Hif intape) -Hif
1023 #j * #outc * #Hloop * #ta * #Hleft #Hright
1024 @(ex_intro ?? j) @ex_intro [|% [@Hloop] ]
1026 #ls #c #rs1 #rs2 #Hrs #Hrs1 #Hc
1028 [ * #Hfalse >Hfalse in Hc; #Htf destruct (Htf)
1029 | * #_ #Hta cases (tech_split ? is_bar rs1)
1030 [ #H1 lapply (Hta rs1 grid rs2 (refl ??) ? ?)
1031 [ (* Hrs1, H1 *) @daemon
1032 | (* bar_or_grid grid = true *) @daemon
1033 | -Hta #Hta cases Hright
1034 [ * #tb * whd in ⊢ (%→?); #Hcurrent
1035 @False_ind cases(Hcurrent grid ?)
1036 [ #Hfalse (* grid is not a bar *) @daemon
1038 | * #tb * whd in ⊢ (%→?); #Hcurrent
1039 cases (Hcurrent grid ?)
1040 [ #_ #Htb whd in ⊢ (%→?); #Houtc
1043 | >Houtc >Htb >Hta % ]
1047 | * #rs3 * #c0 * #rs4 * * #Hc0 #Hsplit #Hrs3
1048 % @(ex_intro ?? rs3) @(ex_intro ?? rs4)
1049 lapply (Hta rs3 c0 (rs4@grid::rs2) ???)
1050 [ #x #Hrs3' (* Hrs1, Hrs3, Hsplit *) @daemon
1051 | (* bar → bar_or_grid *) @daemon
1052 | >Hsplit >associative_append % ] -Hta #Hta
1054 [ * #tb * whd in ⊢ (%→?); #Hta'
1055 whd in ⊢ (%→?); #Htb
1057 [ #_ #Htb' >Htb' in Htb; #Htb
1058 generalize in match Hsplit; -Hsplit
1060 [ >(eq_pair_fst_snd … grid)
1061 #Hta #Hsplit >(Htb … Hta)
1063 [ @(ex_intro ?? (\fst grid)) @(ex_intro ?? (\snd grid))
1064 % [ % [ % [ (* Hsplit *) @daemon |(*Hrs3*) @daemon ] | % ] | % ]
1065 | (* Hc0 *) @daemon ]
1066 | #r5 #rs5 >(eq_pair_fst_snd … r5)
1067 #Hta #Hsplit >(Htb … Hta)
1069 [ @(ex_intro ?? (\fst r5)) @(ex_intro ?? (\snd r5))
1070 % [ % [ % [ (* Hc0, Hsplit *) @daemon | (*Hrs3*) @daemon ] | % ]
1071 | % ] | (* Hc0 *) @daemon ] ] | >Hta % ]
1072 | * #tb * whd in ⊢ (%→?); #Hta'
1073 whd in ⊢ (%→?); #Htb
1075 [ #Hfalse @False_ind >Hfalse in Hc0;