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.
115 (current ? t1 = None ? → t1 = t2) ∧
117 (t1 = midtape alpha ls c rs →
118 ((test c = true ∧ t2 = t1) ∨
120 ∀rs1,b,rs2. rs = rs1@b::rs2 →
121 test b = true → (∀x.memb ? x rs1 = true → test x = false) →
122 t2 = midtape ? (reverse ? rs1@c::ls) b rs2))).
124 definition adv_to_mark_r ≝
125 λalpha,test.whileTM alpha (atmr_step alpha test) atm2.
127 lemma wsem_adv_to_mark_r :
129 WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
130 #alpha #test #t #i #outc #Hloop
131 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
132 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
136 |#ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
137 #Hfalse destruct (Hfalse)
139 | * #a * #Ha #Htest %
140 [ >Ha #H destruct (H);
142 >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
146 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
147 lapply (IH HRfalse) -IH #IH %
148 [cases Hleft #ls * #a * #rs * * #Htapea #_ #_ >Htapea
149 whd in ⊢((??%?)→?); #H destruct (H);
150 |#ls #c #rs #Htapea %2
151 cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
152 >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
153 [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
154 cases (proj2 ?? IH … Htapeb)
155 [ * #_ #Houtc >Houtc >Htapeb %
156 | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
157 | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
158 cases (proj2 ?? IH … Htapeb)
159 [ * #Hfalse >(Hmemb …) in Hfalse;
160 [ #Hft destruct (Hft)
162 | * #Htestr1 #H1 >reverse_cons >associative_append
163 @H1 // #x #Hx @Hmemb @memb_cons //
168 lemma terminate_adv_to_mark_r :
170 ∀t.Terminate alpha (adv_to_mark_r alpha test) t.
172 @(terminate_while … (sem_atmr_step alpha test))
175 [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
176 |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
177 | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
179 [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
180 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
181 % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
182 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
183 | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
184 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
191 lemma sem_adv_to_mark_r :
193 Realize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
199 marks the current character
202 definition mark_states ≝ initN 2.
204 definition ms0 : mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
205 definition ms1 : mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
208 λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
211 [ None ⇒ 〈ms1,None ?〉
212 | Some a' ⇒ match (pi1 … q) with
213 [ O ⇒ let 〈a'',b〉 ≝ a' in 〈ms1,Some ? 〈〈a'',true〉,N〉〉
214 | S q ⇒ 〈ms1,None ?〉 ] ])
217 definition R_mark ≝ λalpha,t1,t2.
219 t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
220 t2 = midtape ? ls 〈c,true〉 rs) ∧
221 (current ? t1 = None ? → t2 = t1).
224 ∀alpha.Realize ? (mark alpha) (R_mark alpha).
225 #alpha #intape @(ex_intro ?? 2) cases intape
227 [| % [ % | % [#ls #c #b #rs #Hfalse destruct | // ]]]
229 [| % [ % | % [#ls #c #b #rs #Hfalse destruct | // ]]]
231 [| % [ % | % [#ls #c #b #rs #Hfalse destruct ] // ]]
233 @ex_intro [| % [ % | %
234 [#ls0 #c0 #b0 #rs0 #H1 destruct (H1) %
235 | whd in ⊢ ((??%?)→?); #H1 destruct (H1)]]]
239 (* MOVE RIGHT AND MARK machine
241 marks the first character on the right
243 (could be rewritten using (mark; move_right))
246 definition mrm_states ≝ initN 3.
248 definition mrm0 : mrm_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
249 definition mrm1 : mrm_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
250 definition mrm2 : mrm_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
252 definition move_right_and_mark ≝
253 λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mrm_states
256 [ None ⇒ 〈mrm2,None ?〉
257 | Some a' ⇒ match pi1 … q with
258 [ O ⇒ 〈mrm1,Some ? 〈a',R〉〉
260 [ O ⇒ let 〈a'',b〉 ≝ a' in
261 〈mrm2,Some ? 〈〈a'',true〉,N〉〉
262 | S _ ⇒ 〈mrm2,None ?〉 ] ] ])
265 definition R_move_right_and_mark ≝ λalpha,t1,t2.
267 t1 = midtape (FinProd … alpha FinBool) ls c (〈d,b〉::rs) →
268 t2 = midtape ? (c::ls) 〈d,true〉 rs.
270 lemma sem_move_right_and_mark :
271 ∀alpha.Realize ? (move_right_and_mark alpha) (R_move_right_and_mark alpha).
272 #alpha #intape @(ex_intro ?? 3) cases intape
274 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
276 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
278 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
280 [ @ex_intro [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #Hfalse destruct ] ]
281 | * #d #b #rs @ex_intro
282 [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #H1 destruct (H1) % ] ] ] ]
285 (* CLEAR MARK machine
287 clears the mark in the current character
290 definition clear_mark_states ≝ initN 3.
292 definition clear0 : clear_mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
293 definition clear1 : clear_mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
294 definition claer2 : clear_mark_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
296 definition clear_mark ≝
297 λalpha:FinSet.mk_TM (FinProd … alpha FinBool) clear_mark_states
300 [ None ⇒ 〈clear1,None ?〉
301 | Some a' ⇒ match pi1 … q with
302 [ O ⇒ let 〈a'',b〉 ≝ a' in 〈clear1,Some ? 〈〈a'',false〉,N〉〉
303 | S q ⇒ 〈clear1,None ?〉 ] ])
304 clear0 (λq.q == clear1).
306 definition R_clear_mark ≝ λalpha,t1,t2.
307 (current ? t1 = None ? → t1 = t2) ∧
309 t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
310 t2 = midtape ? ls 〈c,false〉 rs.
312 lemma sem_clear_mark :
313 ∀alpha.Realize ? (clear_mark alpha) (R_clear_mark alpha).
314 #alpha #intape @(ex_intro ?? 2) cases intape
316 [| % [ % | % [#_ %|#ls #c #b #rs #Hfalse destruct ]]]
318 [| % [ % | % [#_ %|#ls #c #b #rs #Hfalse destruct ]]]
320 [| % [ % | % [#_ %|#ls #c #b #rs #Hfalse destruct ]]]
322 @ex_intro [| % [ % | %
323 [whd in ⊢ (??%?→?); #H destruct| #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ]]]]
326 (* ADVANCE MARK RIGHT machine
328 clears mark on current char,
329 moves right, and marks new current char
333 definition adv_mark_r ≝
335 clear_mark alpha · move_r ? · mark alpha.
337 definition R_adv_mark_r ≝ λalpha,t1,t2.
340 t1 = midtape (FinProd … alpha FinBool) ls 〈c,true〉 (〈d,b〉::rs) →
341 t2 = midtape ? (〈c,false〉::ls) 〈d,true〉 rs) ∧
342 (t1 = midtape (FinProd … alpha FinBool) ls 〈c,true〉 [ ] →
343 t2 = rightof ? 〈c,false〉 ls)) ∧
344 (current ? t1 = None ? → t1 = t2).
346 lemma sem_adv_mark_r :
347 ∀alpha.Realize ? (adv_mark_r alpha) (R_adv_mark_r alpha).
349 @(sem_seq_app … (sem_clear_mark …)
350 (sem_seq ????? (sem_move_r ?) (sem_mark alpha)) …)
351 #intape #outtape whd in ⊢ (%→?); * #ta *
352 whd in ⊢ (%→?); #Hs1 whd in ⊢ (%→?); * #tb * #Hs2 whd in ⊢ (%→?); #Hs3 %
354 [#d #b #rs #Hintape @(proj1 … Hs3 ?? b ?)
355 @(proj2 … Hs2 ls 〈c,false〉 (〈d,b〉::rs))
356 @(proj2 ?? Hs1 … Hintape)
357 |#Hintape lapply (proj2 ?? Hs1 … Hintape) #Hta lapply (proj2 … Hs2 … Hta)
358 whd in ⊢ ((???%)→?); #Htb <Htb @(proj2 … Hs3) >Htb //
360 |#Hcur lapply(proj1 ?? Hs1 … Hcur) #Hta >Hta >Hta in Hcur; #Hcur
361 lapply (proj1 ?? Hs2 … Hcur) #Htb >Htb >Htb in Hcur; #Hcur
362 @sym_eq @(proj2 ?? Hs3) @Hcur
366 (* ADVANCE TO MARK (left)
371 definition atml_step ≝
372 λalpha:FinSet.λtest:alpha→bool.
373 mk_TM alpha atm_states
376 [ None ⇒ 〈atm1, None ?〉
379 [ true ⇒ 〈atm1,None ?〉
380 | false ⇒ 〈atm2,Some ? 〈a',L〉〉 ]])
381 atm0 (λx.notb (x == atm0)).
383 definition Ratml_step_true ≝
386 t1 = midtape alpha ls a rs ∧ test a = false ∧
387 t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a :: rs).
389 definition Ratml_step_false ≝
392 (current alpha t1 = None ? ∨
393 (∃a.current ? t1 = Some ? a ∧ test a = true)).
396 ∀alpha,test,ls,a0,rs. test a0 = true →
397 step alpha (atml_step alpha test)
398 (mk_config ?? atm0 (midtape … ls a0 rs)) =
399 mk_config alpha (states ? (atml_step alpha test)) atm1
400 (midtape … ls a0 rs).
401 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
402 whd in match (trans … 〈?,?〉); >Htest %
406 ∀alpha,test,ls,a0,rs. test a0 = false →
407 step alpha (atml_step alpha test)
408 (mk_config ?? atm0 (midtape … ls a0 rs)) =
409 mk_config alpha (states ? (atml_step alpha test)) atm2
410 (mk_tape … (tail ? ls) (option_hd ? ls) (a0 :: rs)).
411 #alpha #test #ls #a0 #rs #Htest whd in ⊢ (??%?);
412 whd in match (trans … 〈?,?〉); >Htest cases ls //
415 lemma sem_atml_step :
417 accRealize alpha (atml_step alpha test)
418 atm2 (Ratml_step_true alpha test) (Ratml_step_false alpha test).
421 @(ex_intro ?? (mk_config ?? atm1 (niltape ?))) %
422 [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
423 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (leftof ? a al)))
424 % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
425 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (rightof ? a al)))
426 % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
427 | #ls #c #rs @(ex_intro ?? 2)
428 cases (true_or_false (test c)) #Htest
429 [ @(ex_intro ?? (mk_config ?? atm1 ?))
432 [ whd in ⊢ (??%?); >atml_q0_q1 //
433 | whd in ⊢ ((??%%)→?); #Hfalse destruct ]
434 | #_ % // %2 @(ex_intro ?? c) % // ]
436 | @(ex_intro ?? (mk_config ?? atm2 (mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs))))
439 [ whd in ⊢ (??%?); >atml_q0_q2 //
440 | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
443 | #Hfalse @False_ind @(absurd ?? Hfalse) %
449 definition R_adv_to_mark_l ≝ λalpha,test,t1,t2.
450 (current ? t1 = None ? → t1 = t2) ∧
452 (t1 = midtape alpha ls c rs →
453 ((test c = true → t2 = t1) ∧
455 (∀ls1,b,ls2. ls = ls1@b::ls2 →
456 test b = true → (∀x.memb ? x ls1 = true → test x = false) →
457 t2 = midtape ? ls2 b (reverse ? ls1@c::rs)) ∧
458 ((∀x.memb ? x ls = true → test x = false) →
459 ∀a,l. reverse ? (c::ls) = a::l → t2 = leftof ? a (l@rs))
462 definition adv_to_mark_l ≝
463 λalpha,test.whileTM alpha (atml_step alpha test) atm2.
465 lemma wsem_adv_to_mark_l :
467 WRealize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
468 #alpha #test #t #i #outc #Hloop
469 lapply (sem_while … (sem_atml_step alpha test) t i outc Hloop) [%]
470 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
474 |#ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
475 #Hfalse destruct (Hfalse)
477 | * #a * #Ha #Htest %
478 [>Ha #H destruct (H);
481 |#Hc @False_ind >H2 in Ha; whd in ⊢ ((??%?)→?);
486 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
487 lapply (IH HRfalse) -IH #IH %
488 [cases Hleft #ls0 * #a0 * #rs0 * * #Htapea #_ #_ >Htapea
489 whd in ⊢ ((??%?)→?); #H destruct (H)
490 |#ls #c #rs #Htapea %
491 [#Hc cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest @False_ind
492 >Htapea' in Htapea; #H destruct /2/
493 |cases Hleft #ls0 * #a * #rs0 *
494 * #Htapea1 >Htapea in Htapea1; #H destruct (H) #_ #Htapeb
497 [#b #ls2 #Hls >Hls in Htapeb; #Htapeb #Htestb #_
498 cases (proj2 ?? IH … Htapeb) #H1 #_ >H1 // >Htapeb %
499 |#l1 #ls1 #b #ls2 #Hls >Hls in Htapeb; #Htapeb #Htestb #Hmemb
500 cases (proj2 ?? IH … Htapeb) #_ #H1 >reverse_cons >associative_append
501 @(proj1 ?? (H1 ?) … (refl …) Htestb …)
503 |#x #memx @Hmemb @memb_cons @memx
506 |cases ls0 in Htapeb; normalize in ⊢ (%→?);
507 [#Htapeb #Htest #a0 #l whd in ⊢ ((??%?)→?); #Hrev destruct (Hrev)
508 >Htapeb in IH; #IH cases (proj1 ?? IH … (refl …)) //
510 cases (proj2 ?? IH … Htapeb) #_ #H1 #Htest #a0 #l
511 <(reverse_reverse … l) cases (reverse … l)
512 [#H cut (a::l1::ls1 = [a0])
513 [<(reverse_reverse … (a::l1::ls1)) >H //]
514 #Hrev destruct (Hrev)
515 |#a1 #l2 >reverse_cons >reverse_cons >reverse_cons
516 #Hrev cut ([a] = [a1])
517 [@(append_l2_injective_r ?? (a0::reverse … l2) … Hrev) //]
518 #Ha <Ha >associative_append @(proj2 ?? (H1 ?))
520 |#x #membx @Htest @memb_cons @membx
521 |<(append_l1_injective_r ?? (a0::reverse … l2) … Hrev) //
530 lemma terminate_adv_to_mark_l :
532 ∀t.Terminate alpha (adv_to_mark_l alpha test) t.
534 @(terminate_while … (sem_atml_step alpha test))
537 [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
538 |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
540 [#c #rs % #t1 * #ls0 * #c0 * #rs0 * *
541 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
542 % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
543 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
544 | #rs0 #r0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
545 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
552 lemma sem_adv_to_mark_l :
554 Realize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
559 ADVANCE BOTH MARKS machine
561 l1 does not contain marks ⇒
573 definition adv_both_marks ≝ λalpha.
574 adv_mark_r alpha · move_l ? ·
575 adv_to_mark_l (FinProd alpha FinBool) (is_marked alpha) ·
578 definition R_adv_both_marks ≝
580 ∀l0,x,a,l1,x0. (∀c.memb ? c l1 = true → is_marked ? c = false) →
581 (∀l1',a0,l2. t1 = midtape (FinProd … alpha FinBool)
582 (l1@〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
583 reverse ? (〈x0,false〉::l1) = 〈a,false〉::l1' →
584 t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1'@〈a0,true〉::l2)) ∧
585 (t1 = midtape (FinProd … alpha FinBool)
586 (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 [ ] →
587 t2 = rightof ? 〈x0,false〉 (l1@〈a,false〉::〈x,true〉::l0)).
589 lemma sem_adv_both_marks :
590 ∀alpha.Realize ? (adv_both_marks alpha) (R_adv_both_marks alpha).
592 @(sem_seq_app … (sem_adv_mark_r …)
593 (sem_seq ????? (sem_move_l …)
594 (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?))
595 (sem_adv_mark_r alpha))) …)
596 #intape #outtape * #tapea * #Hta * #tb * #Htb * #tc * #Htc #Hout
597 #l0 #x #a #l1 #x0 #Hmarks %
598 [#l1' #a0 #l2 #Hintape #Hrev @(proj1 ?? (proj1 ?? Hout … ) ? false) -Hout
599 lapply (proj1 … (proj1 … Hta …) … Hintape) #Htapea
600 lapply (proj2 … Htb … Htapea) -Htb
601 whd in match (mk_tape ????) ; #Htapeb
602 lapply (proj1 ?? (proj2 ?? (proj2 ?? Htc … Htapeb) (refl …))) -Htc #Htc
603 change with ((?::?)@?) in match (cons ???); <Hrev >reverse_cons
604 >associative_append @Htc [%|%|@Hmarks]
605 |#Hintape lapply (proj2 ?? (proj1 ?? Hta … ) … Hintape) -Hta #Hta
606 lapply (proj1 … Htb) >Hta -Htb #Htb lapply (Htb (refl …)) -Htb #Htb
607 lapply (proj1 ?? Htc) <Htb -Htc #Htc lapply (Htc (refl …)) -Htc #Htc
608 @sym_eq >Htc @(proj2 ?? Hout …) <Htc %
613 definition R_adv_both_marks ≝
615 ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
616 (t1 = midtape (FinProd … alpha FinBool)
617 (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
618 t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2)) ∧
619 (t1 = midtape (FinProd … alpha FinBool)
620 (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 [] →
621 t2 = rightof ? 〈x0,false〉 (l1@〈a,false〉::〈x,true〉::l0)).
623 lemma sem_adv_both_marks :
624 ∀alpha.Realize ? (adv_both_marks alpha) (R_adv_both_marks alpha).
626 cases (sem_seq ????? (sem_adv_mark_r …)
627 (sem_seq ????? (sem_move_l …)
628 (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?))
629 (sem_adv_mark_r alpha))) intape)
630 #k * #outc * #Hloop whd in ⊢ (%→?);
631 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→?); #Hs2
632 * #tc * whd in ⊢ (%→%→?); #Hs3 #Hs4
633 @(ex_intro ?? k) @(ex_intro ?? outc) %
635 | -Hloop #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
637 lapply (Hs1 … Hintape) #Hta
638 lapply (proj2 … Hs2 … Hta) #Htb
640 [ * #Hfalse normalize in Hfalse; destruct (Hfalse)
642 lapply (Hs3 (l1@[〈a,false〉]) 〈x,true〉 l0 ???)
643 [ #x1 #Hx1 cases (memb_append … Hx1)
645 | #Hx1' >(memb_single … Hx1') % ]
647 | >associative_append %
648 | >reverse_append #Htc @Htc ]
660 l0 x a* l1 x0 a0* l2 (f(x0) == true)
662 l0 x* a l1 x0* a0 l2 (f(x0) == false)
666 definition match_and_adv ≝
667 λalpha,f.ifTM ? (test_char ? f)
668 (adv_both_marks alpha) (clear_mark ?) tc_true.
670 definition R_match_and_adv ≝
672 ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
673 t1 = midtape (FinProd … alpha FinBool)
674 (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
675 (f 〈x0,true〉 = true ∧ t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2))
676 ∨ (f 〈x0,true〉 = false ∧
677 t2 = midtape ? (l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)).
679 lemma sem_match_and_adv :
680 ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv alpha f).
682 cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape)
683 #k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
686 [ * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
687 #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape >Hintape in Hta;
688 * * #x1 * whd in ⊢ ((??%?)→?); #H destruct (H) #Hf #Hta % %
689 [ @Hf | >append_cons >append_cons in Hta; #Hta @(proj1 ?? (Houtc …) …Hta)
690 [ #x #memx cases (memb_append …memx)
691 [@Hl1 | -memx #memx >(memb_single … memx) %]
692 |>reverse_cons >reverse_append % ] ]
693 | * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
694 #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape >Hintape in Hta;
695 * #Hf #Hta %2 % [ @Hf % | >(proj2 ?? Houtc … Hta) % ]
701 then move_right; ----
703 if current (* x0 *) = 0
704 then advance_mark ----
711 definition comp_step_subcase ≝ λalpha,c,elseM.
712 ifTM ? (test_char ? (λx.x == c))
713 (move_r … · adv_to_mark_r ? (is_marked alpha) · match_and_adv ? (λx.x == c))
716 definition R_comp_step_subcase ≝
717 λalpha,c,RelseM,t1,t2.
718 ∀l0,x,rs.t1 = midtape (FinProd … alpha FinBool) l0 〈x,true〉 rs →
720 ((∀c.memb ? c rs = true → is_marked ? c = false) →
721 ∀a,l. (a::l) = reverse ? (〈x,true〉::rs) → t2 = rightof (FinProd alpha FinBool) a (l@l0)) ∧
722 ∀a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
723 rs = 〈a,false〉::l1@〈x0,true〉::〈a0,false〉::l2 →
725 t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1@〈x0,false〉::〈a0,true〉::l2)) ∨
727 t2 = midtape (FinProd … alpha FinBool)
728 (reverse ? l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)))) ∨
729 (〈x,true〉 ≠ c → RelseM t1 t2).
731 lemma dec_marked: ∀alpha,rs.
732 decidable (∀c.memb ? c rs = true → is_marked alpha c = false).
734 [%1 #n normalize #H destruct
735 |#a #tl cases (true_or_false (is_marked ? a)) #Ha
736 [#_ %2 % #Hall @(absurd ?? not_eq_true_false) <Ha
738 |* [#Hall %1 #c #memc cases (orb_true_l … memc)
739 [#eqca >(\P eqca) @Ha |@Hall]
740 |#Hnall %2 @(not_to_not … Hnall) #Hall #c #memc @Hall @memb_cons //
744 lemma sem_comp_step_subcase :
745 ∀alpha,c,elseM,RelseM.
746 Realize ? elseM RelseM →
747 Realize ? (comp_step_subcase alpha c elseM)
748 (R_comp_step_subcase alpha c RelseM).
749 #alpha #c #elseM #RelseM #Helse #intape
750 cases (sem_if ? (test_char ? (λx.x == c)) … tc_true
751 (sem_test_char ? (λx.x == c))
752 (sem_seq ????? (sem_move_r …)
753 (sem_seq ????? (sem_adv_to_mark_r ? (is_marked alpha))
754 (sem_match_and_adv ? (λx.x == c)))) Helse intape)
755 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc)
756 % [ @Hloop ] -Hloop cases HR -HR
757 [* #ta * whd in ⊢ (%→?); #Hta * #tb * whd in ⊢ (%→?); #Htb
758 * #tc * whd in ⊢ (%→?); #Htc whd in ⊢ (%→?); #Houtc
759 #l0 #x #rs #Hintape cases (true_or_false (〈x,true〉==c)) #Hc
760 [%1 #_ cases (dec_marked ? rs) #Hdec
763 >Hintape in Hta; * #_(* #x1 * whd in ⊢ ((??%?)→?); #H destruct (H) #Hx *)
764 #Hta lapply (proj2 … Htb … Hta) -Htb -Hta cases rs
765 [whd in ⊢ ((???%)→?); #Htb >Htb in Htc; #Htc
766 lapply (proj1 ?? Htc (refl …)) -Htc #Htc <Htc in Houtc;
767 |#a #l1 #x0 #a0 #l2 #_ #Hrs @False_ind
768 @(absurd ?? not_eq_true_false)
769 change with (is_marked ? 〈x0,true〉) in match true;
770 @Hdec >Hrs @memb_cons @memb_append_l2 @memb_hd
772 |% [#H @False_ind @(absurd …H Hdec)]
773 #a #l1 #x0 #a0 #l2 #Hl1 #Hrs >Hrs in Hintape; #Hintape
774 >Hintape in Hta; * #_(* #x1 * whd in ⊢ ((??%?)→?); #H destruct (H) #Hx *)
775 #Hta lapply (proj2 … Htb … Hta) -Htb -Hta
776 whd in match (mk_tape ????); #Htb cases Htc -Htc #_ #Htc
777 cases (Htc … Htb) [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
778 -Htc * #_ #Htc lapply (Htc l1 〈x0,true〉 (〈a0,false〉::l2) (refl ??) (refl ??) Hl1)
779 -Htc #Htc cases (Houtc ???????? Htc) -Houtc
780 [* #Hx0 #Houtc %1 #Hx >Houtc >reverse_reverse %
781 |* #Hx0 #Houtc %2 #_ >Houtc %
782 |#x #membx @Hl1 <(reverse_reverse …l1) @memb_reverse @membx
785 |%2 >Hintape in Hta; * * #x1 * whd in ⊢ ((??%?)→?); #H destruct (H)
788 |* #ta * whd in ⊢ (%→?); * #Hc #Hta #Helse #ls #c0 #rs #Hintape %2
789 #_ >Hintape in Hta; #Hta <Hta @Helse
796 + se è un bit, ho fallito il confronto della tupla corrente
797 + se è un separatore, la tupla fa match
800 ifTM ? (test_char ? is_marked)
801 (single_finalTM … (comp_step_subcase unialpha 〈bit false,true〉
802 (comp_step_subcase unialpha 〈bit true,true〉
807 definition comp_step ≝
808 ifTM ? (test_char ? (is_marked ?))
809 (single_finalTM … (comp_step_subcase FSUnialpha 〈bit false,true〉
810 (comp_step_subcase FSUnialpha 〈bit true,true〉
811 (comp_step_subcase FSUnialpha 〈null,true〉
818 lemma mem_append : ∀A,x,l1,l2. mem A x (l1@l2) →
819 mem A x l1 ∨ mem A x l2.
820 #A #x #l1 elim l1 normalize [/2/]
821 #a #tl #Hind #l2 * [#eqxa %1 /2/ |#memx cases (Hind … memx) /3/]
824 let rec split_on A (l:list A) f acc on l ≝
828 if f a then 〈acc,a::tl〉 else split_on A tl f (a::acc)
831 lemma split_on_spec: ∀A,l,f,acc,res1,res2.
832 split_on A l f acc = 〈res1,res2〉 →
833 (∃l1. res1 = l1@acc ∧
834 reverse ? l1@res2 = l ∧
835 ∀x. mem ? x l1 → f x = false) ∧
836 ∀a,tl. res2 = a::tl → f a = true.
838 [#acc #res1 #res2 normalize in ⊢ (%→?); #H destruct %
839 [@(ex_intro … []) % normalize [% % | #x @False_ind]
842 |#a #tl #Hind #acc #res1 #res2 normalize in ⊢ (%→?);
843 cases (true_or_false (f a)) #Hfa >Hfa normalize in ⊢ (%→?);
845 [% [@(ex_intro … []) % normalize [% % | #x @False_ind]
846 |#a1 #tl1 #H destruct (H) //]
847 |cases (Hind (a::acc) res1 res2 H) * #l1 * *
848 #Hres1 #Htl #Hfalse #Htrue % [2:@Htrue] @(ex_intro … (l1@[a])) %
849 [% [>associative_append @Hres1 | >reverse_append <Htl % ]
850 |#x #Hmemx cases (mem_append ???? Hmemx)
851 [@Hfalse | normalize * [#H >H //| @False_ind]
857 axiom mem_reverse: ∀A,l,x. mem A x (reverse ? l) → mem A x l.
859 lemma split_on_spec_ex: ∀A,l,f.∃l1,l2.
860 l1@l2 = l ∧ (∀x:A. mem ? x l1 → f x = false) ∧
861 ∀a,tl. l2 = a::tl → f a = true.
862 #A #l #f @(ex_intro … (reverse … (\fst (split_on A l f []))))
863 @(ex_intro … (\snd (split_on A l f [])))
864 cases (split_on_spec A l f [ ] ?? (eq_pair_fst_snd …)) * #l1 * *
865 >append_nil #Hl1 >Hl1 #Hl #Hfalse #Htrue %
866 [% [@Hl|#x #memx @Hfalse @mem_reverse //] | @Htrue]
869 definition R_comp_step_true ≝ λt1,t2.
870 ∃l0,c,a,l1,c0,l1',a0,l2.
871 t1 = midtape (FinProd … FSUnialpha FinBool)
872 l0 〈c,true〉 (l1@〈c0,true〉::〈a0,false〉::l2) ∧
873 l1@[〈c0,false〉] = 〈a,false〉::l1' ∧
874 (∀c.memb ? c l1 = true → is_marked ? c = false) ∧
875 (bit_or_null c = true → c0 = c →
876 t2 = midtape ? (〈c,false〉::l0) 〈a,true〉 (l1'@〈c0,false〉::〈a0,true〉::l2)) ∧
877 (bit_or_null c = true → c0 ≠ c →
878 t2 = midtape (FinProd … FSUnialpha FinBool)
879 (reverse ? l1@〈a,false〉::〈c,true〉::l0) 〈c0,false〉 (〈a0,false〉::l2)) ∧
880 (bit_or_null c = false →
881 t2 = midtape ? l0 〈c,false〉 (〈a,false〉::l1@〈c0,true〉::〈a0,false〉::l2)).
883 definition R_comp_step_false ≝
885 ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
886 is_marked ? c = false ∧ t2 = t1.
889 lemma is_marked_to_exists: ∀alpha,c. is_marked alpha c = true →
893 lemma sem_comp_step :
894 accRealize ? comp_step (inr … (inl … (inr … start_nop)))
895 R_comp_step_true R_comp_step_false.
896 @(acc_sem_if_app … (sem_test_char ? (is_marked ?))
897 (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
898 (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ??
899 (sem_comp_step_subcase FSUnialpha 〈null,true〉 ??
900 (sem_clear_mark …))))
902 [#intape #outtape #midtape * * * #c #b * #Hcurrent
903 whd in ⊢ ((??%?)→?); #Hb #Hmidtape >Hmidtape -Hmidtape
904 cases (current_to_midtape … Hcurrent) #ls * #rs >Hb #Hintape >Hintape -Hb
905 whd in ⊢ (%→?); #Htapea lapply (Htapea … (refl …)) -Htapea
906 cases (split_on_spec_ex ? rs (is_marked ?)) #l1 * #l2 * * #Hrs #Hl1 #Hl2
907 cases (true_or_false (c == bit false))
908 [(* c = bit false *) #Hc * [2: * >(\P Hc) * #H @False_ind @H //]
913 [ #Hstate lapply (H1 Hstate) -H1 -Hstate -H2 *
914 #ta * whd in ⊢ (%→?); #Hleft #Hright #ls #c #rs #Hintape
915 >Hintape in Hleft; * *
916 cases c in Hintape; #c' #b #Hintape #x * whd in ⊢ (??%?→?); #H destruct (H)
917 whd in ⊢ (??%?→?); #Hb >Hb #Hta @(ex_intro ?? c') % //
919 [ * #Hc' #H1 % % [destruct (Hc') % ]
920 #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
922 [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
923 | * #Hneq #Houtc %2 %
927 | * #Hc #Helse1 cases (Helse1 … Hta)
928 [ * #Hc' #H1 % % [destruct (Hc') % ]
929 #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
931 [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
932 | * #Hneq #Houtc %2 %
936 | * #Hc' #Helse2 cases (Helse2 … Hta)
937 [ * #Hc'' #H1 % % [destruct (Hc'') % ]
938 #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
940 [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
941 | * #Hneq #Houtc %2 %
945 | * #Hc'' whd in ⊢ (%→?); #Helse3 %2 %
946 [ generalize in match Hc''; generalize in match Hc'; generalize in match Hc;
948 [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
949 | #Hfalse @False_ind @(absurd ?? Hfalse) % ]
950 | #_ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
957 | #Hstate lapply (H2 Hstate) -H1 -Hstate -H2 *
958 #ta * whd in ⊢ (%→%→?); #Hleft #Hright #ls #c #rs #Hintape
959 >Hintape in Hleft; * #Hc #Hta % [@Hc % | >Hright //]
962 definition R_comp_step_true ≝
964 ∀l0,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) l0 c rs →
966 ((bit_or_null c' = true ∧
968 rs = 〈a,false〉::l1@〈c0,true〉::〈a0,false〉::l2 →
969 (∀c.memb ? c l1 = true → is_marked ? c = false) →
971 t2 = midtape ? (〈c',false〉::l0) 〈a,true〉 (l1@〈c0,false〉::〈a0,true〉::l2)) ∨
973 t2 = midtape (FinProd … FSUnialpha FinBool)
974 (reverse ? l1@〈a,false〉::〈c',true〉::l0) 〈c0,false〉 (〈a0,false〉::l2))) ∨
975 (bit_or_null c' = false ∧ t2 = midtape ? l0 〈c',false〉 rs)).
977 definition R_comp_step_false ≝
979 ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
980 is_marked ? c = false ∧ t2 = t1.
982 lemma sem_comp_step :
983 accRealize ? comp_step (inr … (inl … (inr … start_nop)))
984 R_comp_step_true R_comp_step_false.
986 cases (acc_sem_if … (sem_test_char ? (is_marked ?))
987 (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
988 (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ??
989 (sem_comp_step_subcase FSUnialpha 〈null,true〉 ??
990 (sem_clear_mark …))))
992 #k * #outc * * #Hloop #H1 #H2
993 @(ex_intro ?? k) @(ex_intro ?? outc) %
994 [ % [@Hloop ] ] -Hloop
995 [ #Hstate lapply (H1 Hstate) -H1 -Hstate -H2 *
996 #ta * whd in ⊢ (%→?); #Hleft #Hright #ls #c #rs #Hintape
997 >Hintape in Hleft; * *
998 cases c in Hintape; #c' #b #Hintape #x * whd in ⊢ (??%?→?); #H destruct (H)
999 whd in ⊢ (??%?→?); #Hb >Hb #Hta @(ex_intro ?? c') % //
1000 cases (Hright … Hta)
1001 [ * #Hc' #H1 % % [destruct (Hc') % ]
1002 #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
1003 cases (H1 … Hl1 Hrs)
1004 [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
1005 | * #Hneq #Houtc %2 %
1009 | * #Hc #Helse1 cases (Helse1 … Hta)
1010 [ * #Hc' #H1 % % [destruct (Hc') % ]
1011 #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
1012 cases (H1 … Hl1 Hrs)
1013 [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
1014 | * #Hneq #Houtc %2 %
1018 | * #Hc' #Helse2 cases (Helse2 … Hta)
1019 [ * #Hc'' #H1 % % [destruct (Hc'') % ]
1020 #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
1021 cases (H1 … Hl1 Hrs)
1022 [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
1023 | * #Hneq #Houtc %2 %
1027 | * #Hc'' whd in ⊢ (%→?); #Helse3 %2 %
1028 [ generalize in match Hc''; generalize in match Hc'; generalize in match Hc;
1030 [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
1031 | #Hfalse @False_ind @(absurd ?? Hfalse) % ]
1032 | #_ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
1039 | #Hstate lapply (H2 Hstate) -H1 -Hstate -H2 *
1040 #ta * whd in ⊢ (%→%→?); #Hleft #Hright #ls #c #rs #Hintape
1041 >Hintape in Hleft; * #Hc #Hta % [@Hc % | >Hright //]
1045 definition compare ≝
1046 whileTM ? comp_step (inr … (inl … (inr … start_nop))).
1049 definition R_compare :=
1053 ∀ls,c,b,rs.t1 = midtape ? ls 〈c,b〉 rs →
1054 (b = true → rs = ....) →
1055 (b = false ∧ ....) ∨
1058 rs = cs@l1@〈c0,true〉::cs0@l2
1062 ls 〈c,b〉 cs l1 〈c0,b0〉 cs0 l2
1066 ls (hd (Ls@〈grid,false〉))* (tail (Ls@〈grid,false〉)) l1 (hd (Ls@〈comma,false〉))* (tail (Ls@〈comma,false〉)) l2
1067 ^^^^^^^^^^^^^^^^^^^^^^^
1069 ls Ls 〈grid,false〉 l1 Ls 〈comma,true〉 l2
1074 ls (hd (Ls@〈c,false〉))* (tail (Ls@〈c,false〉)) l1 (hd (Ls@〈d,false〉))* (tail (Ls@〈d,false〉)) l2
1075 ^^^^^^^^^^^^^^^^^^^^^^^
1078 ls Ls 〈c,true〉 l1 Ls 〈d,false〉 l2
1084 (∃la,d.〈b,true〉::bs = la@[〈grid,d〉] ∧ ∀x.memb ? x la → is_bit (\fst x) = true) →
1085 (∃lb,d0.〈b0,true〉::b0s = lb@[〈comma,d0〉] ∧ ∀x.memb ? x lb → is_bit (\fst x) = true) →
1086 t1 = midtape ? l0 〈b,true〉 (bs@l1@〈b0,true〉::b0s@l2 →
1088 mk_tape left (option current) right
1090 (b = grid ∧ b0 = comma ∧ bs = [] ∧ b0s = [] ∧
1091 t2 = midtape ? l0 〈grid,false〉 (l1@〈comma,true〉::l2)) ∨
1092 (b = bit x ∧ b = c ∧ bs = b0s
1094 definition R_compare :=
1096 ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
1097 (∀c'.bit_or_null c' = false → c = 〈c',true〉 → t2 = midtape ? ls 〈c',false〉 rs) ∧
1098 (∀c'. c = 〈c',false〉 → t2 = t1) ∧
1101 (∀c.memb (FinProd … FSUnialpha FinBool) c bs = true → bit_or_null (\fst c) = true) →
1102 (∀c.memb (FinProd … FSUnialpha FinBool) c b0s = true → bit_or_null (\fst c) = true) →
1103 (∀c.memb ? c bs = true → is_marked ? c = false) →
1104 (∀c.memb ? c b0s = true → is_marked ? c = false) →
1105 (∀c.memb ? c l1 = true → is_marked ? c = false) →
1106 c = 〈b,true〉 → bit_or_null b = true →
1107 rs = bs@〈grid,false〉::l1@〈b0,true〉::b0s@〈comma,false〉::l2 →
1108 (〈b,true〉::bs = 〈b0,true〉::b0s ∧
1109 t2 = midtape ? (reverse ? bs@〈b,false〉::ls)
1110 〈grid,false〉 (l1@〈b0,false〉::b0s@〈comma,true〉::l2)) ∨
1111 (∃la,c',d',lb,lc.c' ≠ d' ∧
1112 〈b,false〉::bs = la@〈c',false〉::lb ∧
1113 〈b0,false〉::b0s = la@〈d',false〉::lc ∧
1114 t2 = midtape (FinProd … FSUnialpha FinBool) (reverse ? la@
1120 〈d',false〉 (lc@〈comma,false〉::l2)).
1122 lemma wsem_compare : WRealize ? compare R_compare.
1124 lapply (sem_while ?????? sem_comp_step t i outc Hloop) [%]
1125 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
1126 [ #tapea whd in ⊢ (%→?); #Rfalse #ls #c #rs #Htapea %
1128 [ #c' #Hc' #Hc lapply (Rfalse … Htapea) -Rfalse * >Hc
1129 whd in ⊢ (??%?→?); #Hfalse destruct (Hfalse)
1130 | #c' #Hc lapply (Rfalse … Htapea) -Rfalse * #_
1132 | #b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1 #Hc
1133 cases (Rfalse … Htapea) -Rfalse >Hc whd in ⊢ (??%?→?);#Hfalse destruct (Hfalse)
1135 | #tapea #tapeb #tapec #Hleft #Hright #IH #Htapec lapply (IH Htapec) -Htapec -IH #IH
1136 whd in Hleft; #ls #c #rs #Htapea cases (Hleft … Htapea) -Hleft
1137 #c' * #Hc >Hc cases (true_or_false (bit_or_null c')) #Hc'
1139 [ * >Hc' #H @False_ind destruct (H)
1140 | * #_ #Htapeb cases (IH … Htapeb) * #_ #H #_ %
1142 [#c1 #Hc1 #Heqc destruct (Heqc) <Htapeb @(H c1) %
1143 |#c1 #Hfalse destruct (Hfalse)
1145 |#b #b0 #bs #b0s #l1 #l2 #_ #_ #_ #_ #_ #_
1146 #Heq destruct (Heq) >Hc' #Hfalse @False_ind destruct (Hfalse)
1151 [ #c'' #Hc'' #Heq destruct (Heq) >Hc'' in Hc'; #H destruct (H)
1152 | #c0 #Hfalse destruct (Hfalse)
1154 |#b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1
1155 #Heq destruct (Heq) #_ #Hrs cases Hleft -Hleft
1156 [2: * >Hc' #Hfalse @False_ind destruct ] * #_
1157 @(list_cases2 … Hlen)
1158 [ #Hbs #Hb0s generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
1159 -Hrs #Hrs normalize in Hrs; #Hleft cases (Hleft ????? Hrs ?) -Hleft
1160 [ * #Heqb #Htapeb cases (IH … Htapeb) -IH * #IH #_ #_
1162 [ >Heqb >Hbs >Hb0s %
1165 |* #Hneqb #Htapeb %2
1166 @(ex_intro … [ ]) @(ex_intro … b)
1167 @(ex_intro … b0) @(ex_intro … [ ])
1169 [ % [ % [@sym_not_eq //| >Hbs %] | >Hb0s %]
1170 | cases (IH … Htapeb) -IH * #_ #IH #_ >(IH ? (refl ??))
1174 | * #b' #bitb' * #b0' #bitb0' #bs' #b0s' #Hbs #Hb0s
1175 generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
1176 cut (bit_or_null b' = true ∧ bit_or_null b0' = true ∧
1177 bitb' = false ∧ bitb0' = false)
1178 [ % [ % [ % [ >Hbs in Hbs1; #Hbs1 @(Hbs1 〈b',bitb'〉) @memb_hd
1179 | >Hb0s in Hb0s1; #Hb0s1 @(Hb0s1 〈b0',bitb0'〉) @memb_hd ]
1180 | >Hbs in Hbs2; #Hbs2 @(Hbs2 〈b',bitb'〉) @memb_hd ]
1181 | >Hb0s in Hb0s2; #Hb0s2 @(Hb0s2 〈b0',bitb0'〉) @memb_hd ]
1182 | * * * #Ha #Hb #Hc #Hd >Hc >Hd
1184 cases (Hleft b' (bs'@〈grid,false〉::l1) b0 b0'
1185 (b0s'@〈comma,false〉::l2) ??) -Hleft
1186 [ 3: >Hrs normalize @eq_f >associative_append %
1187 | * #Hb0 #Htapeb cases (IH …Htapeb) -IH * #_ #_ #IH
1188 cases (IH b' b0' bs' b0s' (l1@[〈b0,false〉]) l2 ??????? Ha ?) -IH
1190 [ >Hb0 @eq_f >Hbs in Heq; >Hb0s in ⊢ (%→?); #Heq
1191 destruct (Heq) >Hb0s >Hc >Hd %
1192 | >Houtc >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append
1193 >associative_append %
1195 | * #la * #c' * #d' * #lb * #lc * * * #H1 #H2 #H3 #H4 %2
1196 @(ex_intro … (〈b,false〉::la)) @(ex_intro … c') @(ex_intro … d')
1197 @(ex_intro … lb) @(ex_intro … lc)
1198 % [ % [ % // >Hbs >Hc >H2 % | >Hb0s >Hd >H3 >Hb0 % ]
1199 | >H4 >Hbs >Hb0s >Hc >Hd >Hb0 >reverse_append
1200 >reverse_cons >reverse_cons
1201 >associative_append >associative_append
1202 >associative_append >associative_append %
1204 | generalize in match Hlen; >Hbs >Hb0s
1205 normalize #Hlen destruct (Hlen) @e0
1206 | #c0 #Hc0 @Hbs1 >Hbs @memb_cons //
1207 | #c0 #Hc0 @Hb0s1 >Hb0s @memb_cons //
1208 | #c0 #Hc0 @Hbs2 >Hbs @memb_cons //
1209 | #c0 #Hc0 @Hb0s2 >Hb0s @memb_cons //
1210 | #c0 #Hc0 cases (memb_append … Hc0)
1211 [ @Hl1 | #Hc0' >(memb_single … Hc0') % ]
1213 | >associative_append >associative_append % ]
1214 | * #Hneq #Htapeb %2
1215 @(ex_intro … []) @(ex_intro … b) @(ex_intro … b0)
1216 @(ex_intro … bs) @(ex_intro … b0s) %
1217 [ % // % // @sym_not_eq //
1218 | >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append
1219 >reverse_append in Htapeb; >reverse_cons
1220 >associative_append >associative_append
1222 cases (IH … Htapeb) -Htapeb -IH * #_ #IH #_ @(IH ? (refl ??))
1224 | #c1 #Hc1 cases (memb_append … Hc1) #Hyp
1225 [ @Hbs2 >Hbs @memb_cons @Hyp
1226 | cases (orb_true_l … Hyp)
1227 [ #Hyp2 >(\P Hyp2) %
1235 axiom sem_compare : Realize ? compare R_compare.