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 lemma dec_test: ∀alpha,rs,test.
115 decidable (∀c.memb alpha c rs = true → test c = false).
116 #alpha #rs #test elim rs
117 [%1 #n normalize #H destruct
118 |#a #tl cases (true_or_false (test a)) #Ha
119 [#_ %2 % #Hall @(absurd ?? not_eq_true_false) <Ha
121 |* [#Hall %1 #c #memc cases (orb_true_l … memc)
122 [#eqca >(\P eqca) @Ha |@Hall]
123 |#Hnall %2 @(not_to_not … Hnall) #Hall #c #memc @Hall @memb_cons //
127 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
128 (current ? t1 = None ? → t1 = t2) ∧
130 (t1 = midtape alpha ls c rs →
131 ((test c = true ∧ t2 = t1) ∨
133 (∀rs1,b,rs2. rs = rs1@b::rs2 →
134 test b = true → (∀x.memb ? x rs1 = true → test x = false) →
135 t2 = midtape ? (reverse ? rs1@c::ls) b rs2) ∧
136 ((∀x.memb ? x rs = true → test x = false) →
137 ∀a,l.reverse ? (c::rs) = a::l →
138 t2 = rightof alpha a (l@ls))))).
140 definition adv_to_mark_r ≝
141 λalpha,test.whileTM alpha (atmr_step alpha test) atm2.
143 lemma wsem_adv_to_mark_r :
145 WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
146 #alpha #test #t #i #outc #Hloop
147 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
148 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
152 |#ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
153 #Hfalse destruct (Hfalse)
155 | * #a * #Ha #Htest %
156 [ >Ha #H destruct (H);
158 >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
162 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
163 lapply (IH HRfalse) -IH #IH %
164 [cases Hleft #ls * #a * #rs * * #Htapea #_ #_ >Htapea
165 whd in ⊢((??%?)→?); #H destruct (H);
166 |#ls #c #rs #Htapea %2
167 cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
168 >Htapea' in Htapea; #Htapea destruct (Htapea) % [ % // ]
170 [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
171 cases (proj2 ?? IH … Htapeb)
172 [ * #_ #Houtc >Houtc >Htapeb %
173 | * * >Htestb #Hfalse destruct (Hfalse) ]
174 | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
175 cases (proj2 ?? IH … Htapeb)
176 [ * #Hfalse >(Hmemb …) in Hfalse;
177 [ #Hft destruct (Hft)
179 | * * #Htestr1 #H1 #_ >reverse_cons >associative_append
180 @H1 // #x #Hx @Hmemb @memb_cons //
183 |cases rs in Htapeb; normalize in ⊢ (%→?);
184 [#Htapeb #_ #a0 #l whd in ⊢ ((??%?)→?); #Hrev destruct (Hrev)
185 >Htapeb in IH; #IH cases (proj1 ?? IH … (refl …)) //
186 |#r1 #rs1 #Htapeb #Hmemb
187 cases (proj2 ?? IH … Htapeb) [ * >Hmemb [ #Hfalse destruct(Hfalse) ] @memb_hd ]
188 * #_ #H1 #a #l <(reverse_reverse … l) cases (reverse … l)
189 [#H cut (c::r1::rs1 = [a])
190 [<(reverse_reverse … (c::r1::rs1)) >H //]
191 #Hrev destruct (Hrev)
192 |#a1 #l2 >reverse_cons >reverse_cons >reverse_cons
193 #Hrev cut ([c] = [a1])
194 [@(append_l2_injective_r ?? (a::reverse … l2) … Hrev) //]
195 #Ha <Ha >associative_append @H1
196 [#x #membx @Hmemb @memb_cons @membx
197 |<(append_l1_injective_r ?? (a::reverse … l2) … Hrev) //
201 lemma terminate_adv_to_mark_r :
203 ∀t.Terminate alpha (adv_to_mark_r alpha test) t.
205 @(terminate_while … (sem_atmr_step alpha test))
208 [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
209 |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
210 | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
212 [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
213 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
214 % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
215 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
216 | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
217 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
224 lemma sem_adv_to_mark_r :
226 Realize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
232 marks the current character
235 definition mark_states ≝ initN 2.
237 definition ms0 : mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
238 definition ms1 : mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
241 λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
244 [ None ⇒ 〈ms1,None ?〉
245 | Some a' ⇒ match (pi1 … q) with
246 [ O ⇒ let 〈a'',b〉 ≝ a' in 〈ms1,Some ? 〈〈a'',true〉,N〉〉
247 | S q ⇒ 〈ms1,None ?〉 ] ])
250 definition R_mark ≝ λalpha,t1,t2.
252 t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
253 t2 = midtape ? ls 〈c,true〉 rs) ∧
254 (current ? t1 = None ? → t2 = t1).
257 ∀alpha.Realize ? (mark alpha) (R_mark alpha).
258 #alpha #intape @(ex_intro ?? 2) cases intape
260 [| % [ % | % [#ls #c #b #rs #Hfalse destruct | // ]]]
262 [| % [ % | % [#ls #c #b #rs #Hfalse destruct | // ]]]
264 [| % [ % | % [#ls #c #b #rs #Hfalse destruct ] // ]]
266 @ex_intro [| % [ % | %
267 [#ls0 #c0 #b0 #rs0 #H1 destruct (H1) %
268 | whd in ⊢ ((??%?)→?); #H1 destruct (H1)]]]
272 (* MOVE RIGHT AND MARK machine
274 marks the first character on the right
276 (could be rewritten using (mark; move_right))
279 definition mrm_states ≝ initN 3.
281 definition mrm0 : mrm_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
282 definition mrm1 : mrm_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
283 definition mrm2 : mrm_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
285 definition move_right_and_mark ≝
286 λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mrm_states
289 [ None ⇒ 〈mrm2,None ?〉
290 | Some a' ⇒ match pi1 … q with
291 [ O ⇒ 〈mrm1,Some ? 〈a',R〉〉
293 [ O ⇒ let 〈a'',b〉 ≝ a' in
294 〈mrm2,Some ? 〈〈a'',true〉,N〉〉
295 | S _ ⇒ 〈mrm2,None ?〉 ] ] ])
298 definition R_move_right_and_mark ≝ λalpha,t1,t2.
300 t1 = midtape (FinProd … alpha FinBool) ls c (〈d,b〉::rs) →
301 t2 = midtape ? (c::ls) 〈d,true〉 rs.
303 lemma sem_move_right_and_mark :
304 ∀alpha.Realize ? (move_right_and_mark alpha) (R_move_right_and_mark alpha).
305 #alpha #intape @(ex_intro ?? 3) cases intape
307 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
309 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
311 [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
313 [ @ex_intro [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #Hfalse destruct ] ]
314 | * #d #b #rs @ex_intro
315 [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #H1 destruct (H1) % ] ] ] ]
318 (* CLEAR MARK machine
320 clears the mark in the current character
323 definition clear_mark_states ≝ initN 3.
325 definition clear0 : clear_mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
326 definition clear1 : clear_mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
327 definition claer2 : clear_mark_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
329 definition clear_mark ≝
330 λalpha:FinSet.mk_TM (FinProd … alpha FinBool) clear_mark_states
333 [ None ⇒ 〈clear1,None ?〉
334 | Some a' ⇒ match pi1 … q with
335 [ O ⇒ let 〈a'',b〉 ≝ a' in 〈clear1,Some ? 〈〈a'',false〉,N〉〉
336 | S q ⇒ 〈clear1,None ?〉 ] ])
337 clear0 (λq.q == clear1).
339 definition R_clear_mark ≝ λalpha,t1,t2.
340 (current ? t1 = None ? → t1 = t2) ∧
342 t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
343 t2 = midtape ? ls 〈c,false〉 rs.
345 lemma sem_clear_mark :
346 ∀alpha.Realize ? (clear_mark alpha) (R_clear_mark alpha).
347 #alpha #intape @(ex_intro ?? 2) cases intape
349 [| % [ % | % [#_ %|#ls #c #b #rs #Hfalse destruct ]]]
351 [| % [ % | % [#_ %|#ls #c #b #rs #Hfalse destruct ]]]
353 [| % [ % | % [#_ %|#ls #c #b #rs #Hfalse destruct ]]]
355 @ex_intro [| % [ % | %
356 [whd in ⊢ (??%?→?); #H destruct| #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ]]]]
359 (* ADVANCE MARK RIGHT machine
361 clears mark on current char,
362 moves right, and marks new current char
366 definition adv_mark_r ≝
368 clear_mark alpha · move_r ? · mark alpha.
370 definition R_adv_mark_r ≝ λalpha,t1,t2.
373 t1 = midtape (FinProd … alpha FinBool) ls 〈c,true〉 (〈d,b〉::rs) →
374 t2 = midtape ? (〈c,false〉::ls) 〈d,true〉 rs) ∧
375 (t1 = midtape (FinProd … alpha FinBool) ls 〈c,true〉 [ ] →
376 t2 = rightof ? 〈c,false〉 ls)) ∧
377 (current ? t1 = None ? → t1 = t2).
379 lemma sem_adv_mark_r :
380 ∀alpha.Realize ? (adv_mark_r alpha) (R_adv_mark_r alpha).
382 @(sem_seq_app … (sem_clear_mark …)
383 (sem_seq ????? (sem_move_r ?) (sem_mark alpha)) …)
384 #intape #outtape whd in ⊢ (%→?); * #ta *
385 whd in ⊢ (%→?); #Hs1 whd in ⊢ (%→?); * #tb * #Hs2 whd in ⊢ (%→?); #Hs3 %
387 [#d #b #rs #Hintape @(proj1 … Hs3 ?? b ?)
388 @(proj2 … Hs2 ls 〈c,false〉 (〈d,b〉::rs))
389 @(proj2 ?? Hs1 … Hintape)
390 |#Hintape lapply (proj2 ?? Hs1 … Hintape) #Hta lapply (proj2 … Hs2 … Hta)
391 whd in ⊢ ((???%)→?); #Htb <Htb @(proj2 … Hs3) >Htb //
393 |#Hcur lapply(proj1 ?? Hs1 … Hcur) #Hta >Hta >Hta in Hcur; #Hcur
394 lapply (proj1 ?? Hs2 … Hcur) #Htb >Htb >Htb in Hcur; #Hcur
395 @sym_eq @(proj2 ?? Hs3) @Hcur
399 (* ADVANCE TO MARK (left)
404 definition atml_step ≝
405 λalpha:FinSet.λtest:alpha→bool.
406 mk_TM alpha atm_states
409 [ None ⇒ 〈atm1, None ?〉
412 [ true ⇒ 〈atm1,None ?〉
413 | false ⇒ 〈atm2,Some ? 〈a',L〉〉 ]])
414 atm0 (λx.notb (x == atm0)).
416 definition Ratml_step_true ≝
419 t1 = midtape alpha ls a rs ∧ test a = false ∧
420 t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a :: rs).
422 definition Ratml_step_false ≝
425 (current alpha t1 = None ? ∨
426 (∃a.current ? t1 = Some ? a ∧ test a = true)).
429 ∀alpha,test,ls,a0,rs. test a0 = true →
430 step alpha (atml_step alpha test)
431 (mk_config ?? atm0 (midtape … ls a0 rs)) =
432 mk_config alpha (states ? (atml_step alpha test)) atm1
433 (midtape … ls a0 rs).
434 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
435 whd in match (trans … 〈?,?〉); >Htest %
439 ∀alpha,test,ls,a0,rs. test a0 = false →
440 step alpha (atml_step alpha test)
441 (mk_config ?? atm0 (midtape … ls a0 rs)) =
442 mk_config alpha (states ? (atml_step alpha test)) atm2
443 (mk_tape … (tail ? ls) (option_hd ? ls) (a0 :: rs)).
444 #alpha #test #ls #a0 #rs #Htest whd in ⊢ (??%?);
445 whd in match (trans … 〈?,?〉); >Htest cases ls //
448 lemma sem_atml_step :
450 accRealize alpha (atml_step alpha test)
451 atm2 (Ratml_step_true alpha test) (Ratml_step_false alpha test).
454 @(ex_intro ?? (mk_config ?? atm1 (niltape ?))) %
455 [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
456 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (leftof ? a al)))
457 % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
458 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (rightof ? a al)))
459 % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
460 | #ls #c #rs @(ex_intro ?? 2)
461 cases (true_or_false (test c)) #Htest
462 [ @(ex_intro ?? (mk_config ?? atm1 ?))
465 [ whd in ⊢ (??%?); >atml_q0_q1 //
466 | whd in ⊢ ((??%%)→?); #Hfalse destruct ]
467 | #_ % // %2 @(ex_intro ?? c) % // ]
469 | @(ex_intro ?? (mk_config ?? atm2 (mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs))))
472 [ whd in ⊢ (??%?); >atml_q0_q2 //
473 | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
476 | #Hfalse @False_ind @(absurd ?? Hfalse) %
482 definition R_adv_to_mark_l ≝ λalpha,test,t1,t2.
483 (current ? t1 = None ? → t1 = t2) ∧
485 (t1 = midtape alpha ls c rs →
486 ((test c = true → t2 = t1) ∧
488 (∀ls1,b,ls2. ls = ls1@b::ls2 →
489 test b = true → (∀x.memb ? x ls1 = true → test x = false) →
490 t2 = midtape ? ls2 b (reverse ? ls1@c::rs)) ∧
491 ((∀x.memb ? x ls = true → test x = false) →
492 ∀a,l. reverse ? (c::ls) = a::l → t2 = leftof ? a (l@rs))
495 definition adv_to_mark_l ≝
496 λalpha,test.whileTM alpha (atml_step alpha test) atm2.
498 lemma wsem_adv_to_mark_l :
500 WRealize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
501 #alpha #test #t #i #outc #Hloop
502 lapply (sem_while … (sem_atml_step alpha test) t i outc Hloop) [%]
503 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
507 |#ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
508 #Hfalse destruct (Hfalse)
510 | * #a * #Ha #Htest %
511 [>Ha #H destruct (H);
514 |#Hc @False_ind >H2 in Ha; whd in ⊢ ((??%?)→?);
519 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
520 lapply (IH HRfalse) -IH #IH %
521 [cases Hleft #ls0 * #a0 * #rs0 * * #Htapea #_ #_ >Htapea
522 whd in ⊢ ((??%?)→?); #H destruct (H)
523 |#ls #c #rs #Htapea %
524 [#Hc cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest @False_ind
525 >Htapea' in Htapea; #H destruct /2/
526 |cases Hleft #ls0 * #a * #rs0 *
527 * #Htapea1 >Htapea in Htapea1; #H destruct (H) #_ #Htapeb
530 [#b #ls2 #Hls >Hls in Htapeb; #Htapeb #Htestb #_
531 cases (proj2 ?? IH … Htapeb) #H1 #_ >H1 // >Htapeb %
532 |#l1 #ls1 #b #ls2 #Hls >Hls in Htapeb; #Htapeb #Htestb #Hmemb
533 cases (proj2 ?? IH … Htapeb) #_ #H1 >reverse_cons >associative_append
534 @(proj1 ?? (H1 ?) … (refl …) Htestb …)
536 |#x #memx @Hmemb @memb_cons @memx
539 |cases ls0 in Htapeb; normalize in ⊢ (%→?);
540 [#Htapeb #Htest #a0 #l whd in ⊢ ((??%?)→?); #Hrev destruct (Hrev)
541 >Htapeb in IH; #IH cases (proj1 ?? IH … (refl …)) //
543 cases (proj2 ?? IH … Htapeb) #_ #H1 #Htest #a0 #l
544 <(reverse_reverse … l) cases (reverse … l)
545 [#H cut (a::l1::ls1 = [a0])
546 [<(reverse_reverse … (a::l1::ls1)) >H //]
547 #Hrev destruct (Hrev)
548 |#a1 #l2 >reverse_cons >reverse_cons >reverse_cons
549 #Hrev cut ([a] = [a1])
550 [@(append_l2_injective_r ?? (a0::reverse … l2) … Hrev) //]
551 #Ha <Ha >associative_append @(proj2 ?? (H1 ?))
553 |#x #membx @Htest @memb_cons @membx
554 |<(append_l1_injective_r ?? (a0::reverse … l2) … Hrev) //
563 lemma terminate_adv_to_mark_l :
565 ∀t.Terminate alpha (adv_to_mark_l alpha test) t.
567 @(terminate_while … (sem_atml_step alpha test))
570 [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
571 |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
573 [#c #rs % #t1 * #ls0 * #c0 * #rs0 * *
574 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
575 % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
576 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
577 | #rs0 #r0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
578 #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
585 lemma sem_adv_to_mark_l :
587 Realize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
592 ADVANCE BOTH MARKS machine
594 l1 does not contain marks ⇒
606 definition adv_both_marks ≝ λalpha.
607 adv_mark_r alpha · move_l ? ·
608 adv_to_mark_l (FinProd alpha FinBool) (is_marked alpha) ·
611 definition R_adv_both_marks ≝ λalpha,t1,t2.
613 t1 = midtape (FinProd … alpha FinBool) ls 〈x0,true〉 rs →
614 (rs = [ ] → (* first case: rs empty *)
615 t2 = rightof (FinProd … alpha FinBool) 〈x0,false〉 ls) ∧
616 (∀l0,x,a,a0,b,l1,l1',l2.
617 ls = (l1@〈x,true〉::l0) →
618 (∀c.memb ? c l1 = true → is_marked ? c = false) →
620 reverse ? (〈x0,false〉::l1) = 〈a,false〉::l1' →
621 t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1'@〈a0,true〉::l2)).
623 lemma sem_adv_both_marks :
624 ∀alpha.Realize ? (adv_both_marks alpha) (R_adv_both_marks alpha).
626 @(sem_seq_app … (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))) …)
630 #intape #outtape * #tapea * #Hta * #tb * #Htb * #tc * #Htc #Hout
631 #ls #c #rs #Hintape %
632 [#Hrs >Hrs in Hintape; #Hintape lapply (proj2 ?? (proj1 ?? Hta … ) … Hintape) -Hta #Hta
633 lapply (proj1 … Htb) >Hta -Htb #Htb lapply (Htb (refl …)) -Htb #Htb
634 lapply (proj1 ?? Htc) <Htb -Htc #Htc lapply (Htc (refl …)) -Htc #Htc
635 @sym_eq >Htc @(proj2 ?? Hout …) <Htc %
636 |#l0 #x #a #a0 #b #l1 #l1' #l2 #Hls #Hmarks #Hrs #Hrev
637 >Hrs in Hintape; >Hls #Hintape
638 @(proj1 ?? (proj1 ?? Hout … ) ? false) -Hout
639 lapply (proj1 … (proj1 … Hta …) … Hintape) #Htapea
640 lapply (proj2 … Htb … Htapea) -Htb
641 whd in match (mk_tape ????) ; #Htapeb
642 lapply (proj1 ?? (proj2 ?? (proj2 ?? Htc … Htapeb) (refl …))) -Htc #Htc
643 change with ((?::?)@?) in match (cons ???); <Hrev >reverse_cons
644 >associative_append @Htc [%|%|@Hmarks]
649 definition R_adv_both_marks ≝
651 ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
652 (t1 = midtape (FinProd … alpha FinBool)
653 (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
654 t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2)) ∧
655 (t1 = midtape (FinProd … alpha FinBool)
656 (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 [] →
657 t2 = rightof ? 〈x0,false〉 (l1@〈a,false〉::〈x,true〉::l0)).
659 lemma sem_adv_both_marks :
660 ∀alpha.Realize ? (adv_both_marks alpha) (R_adv_both_marks alpha).
662 cases (sem_seq ????? (sem_adv_mark_r …)
663 (sem_seq ????? (sem_move_l …)
664 (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?))
665 (sem_adv_mark_r alpha))) intape)
666 #k * #outc * #Hloop whd in ⊢ (%→?);
667 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→?); #Hs2
668 * #tc * whd in ⊢ (%→%→?); #Hs3 #Hs4
669 @(ex_intro ?? k) @(ex_intro ?? outc) %
671 | -Hloop #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
673 lapply (Hs1 … Hintape) #Hta
674 lapply (proj2 … Hs2 … Hta) #Htb
676 [ * #Hfalse normalize in Hfalse; destruct (Hfalse)
678 lapply (Hs3 (l1@[〈a,false〉]) 〈x,true〉 l0 ???)
679 [ #x1 #Hx1 cases (memb_append … Hx1)
681 | #Hx1' >(memb_single … Hx1') % ]
683 | >associative_append %
684 | >reverse_append #Htc @Htc ]
696 l0 x a* l1 x0 a0* l2 (f(x0) == true)
698 l0 x* a l1 x0* a0 l2 (f(x0) == false)
702 definition match_and_adv ≝
703 λalpha,f.ifTM ? (test_char ? f)
704 (adv_both_marks alpha) (clear_mark ?) tc_true.
706 definition R_match_and_adv ≝
709 t1 = midtape (FinProd … alpha FinBool) ls 〈x0,true〉 rs →
710 ((* first case: (f 〈x0,true〉 = false) *)
711 (f 〈x0,true〉 = false) →
712 t2 = midtape (FinProd … alpha FinBool) ls 〈x0,false〉 rs) ∧
713 ((f 〈x0,true〉 = true) → rs = [ ] → (* second case: rs empty *)
714 t2 = rightof (FinProd … alpha FinBool) 〈x0,false〉 ls) ∧
715 ((f 〈x0,true〉 = true) →
716 ∀l0,x,a,a0,b,l1,l1',l2.
717 (* third case: we expect to have a mark on the left! *)
718 ls = (l1@〈x,true〉::l0) →
719 (∀c.memb ? c l1 = true → is_marked ? c = false) →
721 reverse ? (〈x0,false〉::l1) = 〈a,false〉::l1' →
722 t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1'@〈a0,true〉::l2)).
724 lemma sem_match_and_adv :
725 ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv alpha f).
727 cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape)
728 #k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
731 @(sem_if_app … (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?))
732 #intape #outape #Htb * #H *)
734 [ * #ta * whd in ⊢ (%→%→?); * * #c * #Hcurrent #fc #Hta #Houtc
735 #ls #x #rs #Hintape >Hintape in Hcurrent; whd in ⊢ ((??%?)→?); #H destruct (H) %
736 [%[>fc #H destruct (H)
737 |#_ #Hrs >Hrs in Hintape; #Hintape >Hintape in Hta; #Hta
738 cases (Houtc … Hta) #Houtc #_ @Houtc //
740 |#l0 #x0 #a #a0 #b #l1 #l1' #l2 #Hls #Hmarks #Hrs #Hrev >Hintape in Hta; #Hta
741 @(proj2 ?? (Houtc … Hta) … Hls Hmarks Hrs Hrev)
743 | * #ta * * #H #Hta * #_ #Houtc #ls #c #rs #Hintape
744 >Hintape in H; #H lapply(H … (refl …)) #fc %
745 [%[#_ >Hintape in Hta; #Hta @(Houtc … Hta)
754 lemma sem_match_and_adv :
755 ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv alpha f).
757 cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape)
758 #k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
761 [ * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
762 #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape >Hintape in Hta;
763 * * #x1 * whd in ⊢ ((??%?)→?); #H destruct (H) #Hf #Hta % %
764 [ @Hf | >append_cons >append_cons in Hta; #Hta @(proj1 ?? (Houtc …) …Hta)
765 [ #x #memx cases (memb_append …memx)
766 [@Hl1 | -memx #memx >(memb_single … memx) %]
767 |>reverse_cons >reverse_append % ] ]
768 | * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
769 #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape >Hintape in Hta;
770 * #Hf #Hta %2 % [ @Hf % | >(proj2 ?? Houtc … Hta) % ]
775 definition R_match_and_adv_of ≝
776 λalpha,t1,t2.current (FinProd … alpha FinBool) t1 = None ? → t2 = t1.
778 lemma sem_match_and_adv_of :
779 ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv_of alpha).
781 cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape)
782 #k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
785 [ * #ta * whd in ⊢ (%→%→?); #Hta #Houtc #Hcur
786 cases Hta * #x >Hcur * #Hfalse destruct (Hfalse)
787 | * #ta * whd in ⊢ (%→%→?); * #_ #Hta * #Houtc #_ <Hta #Hcur >(Houtc Hcur) % ]
790 lemma sem_match_and_adv_full :
791 ∀alpha,f.Realize ? (match_and_adv alpha f)
792 (R_match_and_adv alpha f ∩ R_match_and_adv_of alpha).
793 #alpha #f #intape cases (sem_match_and_adv ? f intape)
794 #i * #outc * #Hloop #HR1 %{i} %{outc} % // % //
795 cases (sem_match_and_adv_of ? f intape) #i0 * #outc0 * #Hloop0 #HR2
796 >(loop_eq … Hloop Hloop0) //
801 then move_right; ----
803 if current (* x0 *) = 0
804 then advance_mark ----
811 definition comp_step_subcase ≝ λalpha,c,elseM.
812 ifTM ? (test_char ? (λx.x == c))
813 (move_r … · adv_to_mark_r ? (is_marked alpha) · match_and_adv ? (λx.x == c))
816 definition R_comp_step_subcase ≝
817 λalpha,c,RelseM,t1,t2.
818 ∀ls,x,rs.t1 = midtape (FinProd … alpha FinBool) ls 〈x,true〉 rs →
820 ((* test true but no marks in rs *)
821 (∀c.memb ? c rs = true → is_marked ? c = false) →
822 ∀a,l. (a::l) = reverse ? (〈x,true〉::rs) →
823 t2 = rightof (FinProd alpha FinBool) a (l@ls)) ∧
825 (∀c.memb ? c l1 = true → is_marked ? c = false) →
826 rs = l1@〈x0,true〉::l2 →
828 l2 = [ ] → (* test true but l2 is empty *)
829 t2 = rightof ? 〈x0,false〉 ((reverse ? l1)@〈x,true〉::ls)) ∧
831 ∀a,a0,b,l1',l2'. (* test true and l2 is not empty *)
832 〈a,false〉::l1' = l1@[〈x0,false〉] →
834 t2 = midtape ? (〈x,false〉::ls) 〈a,true〉 (l1'@〈a0,true〉::l2')) ∧
835 (x ≠ x0 →(* test false *)
836 t2 = midtape (FinProd … alpha FinBool) ((reverse ? l1)@〈x,true〉::ls) 〈x0,false〉 l2)) ∧
837 (〈x,true〉 ≠ c → RelseM t1 t2).
839 lemma dec_marked: ∀alpha,rs.
840 decidable (∀c.memb ? c rs = true → is_marked alpha c = false).
842 [%1 #n normalize #H destruct
843 |#a #tl cases (true_or_false (is_marked ? a)) #Ha
844 [#_ %2 % #Hall @(absurd ?? not_eq_true_false) <Ha
846 |* [#Hall %1 #c #memc cases (orb_true_l … memc)
847 [#eqca >(\P eqca) @Ha |@Hall]
848 |#Hnall %2 @(not_to_not … Hnall) #Hall #c #memc @Hall @memb_cons //
852 (* axiom daemon:∀P:Prop.P. *)
854 lemma sem_comp_step_subcase :
855 ∀alpha,c,elseM,RelseM.
856 Realize ? elseM RelseM →
857 Realize ? (comp_step_subcase alpha c elseM)
858 (R_comp_step_subcase alpha c RelseM).
859 #alpha #c #elseM #RelseM #Helse #intape
860 cases (sem_if ? (test_char ? (λx.x == c)) … tc_true
861 (sem_test_char ? (λx.x == c))
862 (sem_seq ????? (sem_move_r …)
863 (sem_seq ????? (sem_adv_to_mark_r ? (is_marked alpha))
864 (sem_match_and_adv_full ? (λx.x == c)))) Helse intape)
865 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc)
866 % [ @Hloop ] -Hloop cases HR -HR
867 [* #ta * whd in ⊢ (%→?); * * #cin * #Hcin #Hcintrue #Hta * #tb * whd in ⊢ (%→?); #Htb
868 * #tc * whd in ⊢ (%→?); #Htc * whd in ⊢ (%→%→?); #Houtc #Houtc1
869 #ls #x #rs #Hintape >Hintape in Hcin; whd in ⊢ ((??%?)→?); #H destruct (H) %
870 [#_ cases (dec_marked ? rs) #Hdec
873 >Hintape in Hta; #Hta
874 lapply (proj2 ?? Htb … Hta) -Htb -Hta cases rs in Hdec;
876 [#_ whd in ⊢ ((???%)→?); #Htb >Htb in Htc; #Htc
877 lapply (proj1 ?? Htc (refl …)) -Htc #Htc <Htc in Houtc1; #Houtc1
878 normalize in ⊢ (???%→?); #Hl1 destruct(Hl1) @(Houtc1 (refl …))
879 |#r0 #rs0 #Hdec whd in ⊢ ((???%)→?); #Htb >Htb in Htc; #Htc
880 >reverse_cons >reverse_cons #Hl1
881 cases (proj2 ?? Htc … (refl …))
882 [* >(Hdec …) [ #Hfalse destruct(Hfalse) ] @memb_hd
883 |* #_ -Htc #Htc cut (∃l2.l1 = l2@[〈x,true〉])
884 [generalize in match Hl1; -Hl1 <(reverse_reverse … l1)
886 [#Hl1 cut ([a]=〈x,true〉::r0::rs0)
887 [ <(reverse_reverse … (〈x,true〉::r0::rs0))
888 >reverse_cons >reverse_cons <Hl1 %
889 | #Hfalse destruct(Hfalse)]
890 |#a0 #l10 >reverse_cons #Heq
891 lapply (append_l2_injective_r ? (a::reverse ? l10) ???? Heq) //
892 #Ha0 destruct(Ha0) /2/ ]
893 |* #l2 #Hl2 >Hl2 in Hl1; #Hl1
894 lapply (append_l1_injective_r ? (a::l2) … Hl1) // -Hl1 #Hl1
895 >reverse_cons in Htc; #Htc lapply (Htc … (sym_eq … Hl1))
896 [ #x0 #Hmemb @Hdec @memb_cons @Hmemb ]
897 -Htc #Htc >Htc in Houtc1; #Houtc1 >associative_append @Houtc1 %
901 |#l1 #x0 #l2 #_ #Hrs @False_ind
902 @(absurd ?? not_eq_true_false)
903 change with (is_marked ? 〈x0,true〉) in match true;
904 @Hdec >Hrs @memb_append_l2 @memb_hd
906 |% [#H @False_ind @(absurd …H Hdec)]
907 (* by cases on l1 *) *
908 [#x0 #l2 #Hdec normalize in ⊢ (%→?); #Hrs >Hrs in Hintape; #Hintape
909 >Hintape in Hta; (* * * #x1 * whd in ⊢ ((??%?)→?); #H destruct (H) #Hx *)
910 #Hta lapply (proj2 … Htb … Hta) -Htb -Hta
911 whd in match (mk_tape ????); whd in match (tail ??); #Htb cases Htc -Htc
912 #_ #Htc cases (Htc … Htb) -Htc
913 [2: * * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
914 * * #Htc >Htb in Htc; -Htb #Htc cases (Houtc … Htc) -Houtc *
915 #H1 #H2 #H3 cases (true_or_false (x==x0)) #eqxx0
916 [>(\P eqxx0) % [2: #H @False_ind /2/] %
917 [#_ #Hl2 >(H2 … Hl2) <(\P eqxx0) [% | @Hcintrue]
918 |#_ #a #a0 #b #l1' #l2' normalize in ⊢ (%→?); #Hdes destruct (Hdes)
919 #Hl2 @(H3 … Hdec … Hl2) <(\P eqxx0) [@Hcintrue | % | @reverse_single]
921 |% [% #eqx @False_ind lapply (\Pf eqxx0) #Habs @(absurd … eqx Habs)]
922 #_ @H1 @(\bf ?) @(not_to_not ??? (\Pf eqxx0)) <(\P Hcintrue)
923 #Hdes destruct (Hdes) %
925 |#l1hd #l1tl #x0 #l2 #Hdec normalize in ⊢ (%→?); #Hrs >Hrs in Hintape; #Hintape
926 >Hintape in Hta; (* * * #x1 * whd in ⊢ ((??%?)→?); #H destruct (H) #Hx *)
927 #Hta lapply (proj2 … Htb … Hta) -Htb -Hta
928 whd in match (mk_tape ????); whd in match (tail ??); #Htb cases Htc -Htc
929 #_ #Htc cases (Htc … Htb) -Htc
930 [* #Hfalse @False_ind >(Hdec … (memb_hd …)) in Hfalse; #H destruct]
931 * * #_ #Htc lapply (Htc … (refl …) (refl …) ?) -Htc
932 [#x1 #membx1 @Hdec @memb_cons @membx1] #Htc
933 cases (Houtc … Htc) -Houtc *
934 #H1 #H2 #H3 #_ cases (true_or_false (x==x0)) #eqxx0
935 [>(\P eqxx0) % [2: #H @False_ind /2/] %
936 [#_ #Hl2 >(H2 … Hl2) <(\P eqxx0)
937 [>reverse_cons >associative_append % | @Hcintrue]
938 |#_ #a #a0 #b #l1' #l2' normalize in ⊢ (%→?); #Hdes (* destruct (Hdes) *)
939 #Hl2 @(H3 ?????? (reverse … (l1hd::l1tl)) … Hl2) <(\P eqxx0)
941 |>reverse_cons >associative_append %
942 |#c0 #memc @Hdec <(reverse_reverse ? (l1hd::l1tl)) @memb_reverse @memc
943 |>Hdes >reverse_cons >reverse_reverse >(\P eqxx0) %
946 |% [% #eqx @False_ind lapply (\Pf eqxx0) #Habs @(absurd … eqx Habs)]
947 #_ >reverse_cons >associative_append @H1 @(\bf ?)
948 @(not_to_not ??? (\Pf eqxx0)) <(\P Hcintrue) #Hdes
953 |>(\P Hcintrue) * #Hfalse @False_ind @Hfalse %
955 | * #ta * * #Hcur #Hta #Houtc
956 #l0 #x #rs #Hintape >Hintape in Hcur; #Hcur lapply (Hcur ? (refl …)) -Hcur #Hc %
957 [ #Hfalse >Hfalse in Hc; #Hc cases (\Pf Hc) #Hc @False_ind @Hc %
958 | -Hc #Hc <Hintape <Hta @Houtc ] ]
964 + se è un bit, ho fallito il confronto della tupla corrente
965 + se è un separatore, la tupla fa match
968 ifTM ? (test_char ? is_marked)
969 (single_finalTM … (comp_step_subcase unialpha 〈bit false,true〉
970 (comp_step_subcase unialpha 〈bit true,true〉
975 definition comp_step ≝
976 ifTM ? (test_char ? (is_marked ?))
977 (single_finalTM … (comp_step_subcase FSUnialpha 〈bit false,true〉
978 (comp_step_subcase FSUnialpha 〈bit true,true〉
979 (comp_step_subcase FSUnialpha 〈null,true〉
986 lemma mem_append : ∀A,x,l1,l2. mem A x (l1@l2) →
987 mem A x l1 ∨ mem A x l2.
988 #A #x #l1 elim l1 normalize [/2/]
989 #a #tl #Hind #l2 * [#eqxa %1 /2/ |#memx cases (Hind … memx) /3/]
992 let rec split_on A (l:list A) f acc on l ≝
996 if f a then 〈acc,a::tl〉 else split_on A tl f (a::acc)
999 lemma split_on_spec: ∀A:DeqSet.∀l,f,acc,res1,res2.
1000 split_on A l f acc = 〈res1,res2〉 →
1001 (∃l1. res1 = l1@acc ∧
1002 reverse ? l1@res2 = l ∧
1003 ∀x. memb ? x l1 =true → f x = false) ∧
1004 ∀a,tl. res2 = a::tl → f a = true.
1006 [#acc #res1 #res2 normalize in ⊢ (%→?); #H destruct %
1007 [@(ex_intro … []) % normalize [% % | #x #H destruct]
1010 |#a #tl #Hind #acc #res1 #res2 normalize in ⊢ (%→?);
1011 cases (true_or_false (f a)) #Hfa >Hfa normalize in ⊢ (%→?);
1013 [% [@(ex_intro … []) % normalize [% % | #x #H destruct]
1014 |#a1 #tl1 #H destruct (H) //]
1015 |cases (Hind (a::acc) res1 res2 H) * #l1 * *
1016 #Hres1 #Htl #Hfalse #Htrue % [2:@Htrue] @(ex_intro … (l1@[a])) %
1017 [% [>associative_append @Hres1 | >reverse_append <Htl % ]
1018 |#x #Hmemx cases (memb_append ???? Hmemx)
1019 [@Hfalse | #H >(memb_single … H) //]
1025 axiom mem_reverse: ∀A,l,x. mem A x (reverse ? l) → mem A x l.
1027 lemma split_on_spec_ex: ∀A:DeqSet.∀l,f.∃l1,l2.
1028 l1@l2 = l ∧ (∀x:A. memb ? x l1 = true → f x = false) ∧
1029 ∀a,tl. l2 = a::tl → f a = true.
1030 #A #l #f @(ex_intro … (reverse … (\fst (split_on A l f []))))
1031 @(ex_intro … (\snd (split_on A l f [])))
1032 cases (split_on_spec A l f [ ] ?? (eq_pair_fst_snd …)) * #l1 * *
1033 >append_nil #Hl1 >Hl1 #Hl #Hfalse #Htrue %
1034 [% [@Hl|#x #memx @Hfalse <(reverse_reverse … l1) @memb_reverse //] | @Htrue]
1037 (* versione esistenziale *)
1039 definition R_comp_step_true ≝ λt1,t2.
1040 ∃ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls 〈c,true〉 rs ∧
1041 ((* bit_or_null c = false *)
1042 (bit_or_null c = false → t2 = midtape ? ls 〈c,false〉 rs) ∧
1043 (* no marks in rs *)
1044 (bit_or_null c = true →
1045 (∀c.memb ? c rs = true → is_marked ? c = false) →
1046 ∀a,l. (a::l) = reverse ? (〈c,true〉::rs) →
1047 t2 = rightof (FinProd FSUnialpha FinBool) a (l@ls)) ∧
1049 bit_or_null c = true →
1050 (∀c.memb ? c l1 = true → is_marked ? c = false) →
1051 rs = l1@〈c0,true〉::l2 →
1053 l2 = [ ] → (* test true but l2 is empty *)
1054 t2 = rightof ? 〈c0,false〉 ((reverse ? l1)@〈c,true〉::ls)) ∧
1056 ∀a,a0,b,l1',l2'. (* test true and l2 is not empty *)
1057 〈a,false〉::l1' = l1@[〈c0,false〉] →
1059 t2 = midtape ? (〈c,false〉::ls) 〈a,true〉 (l1'@〈a0,true〉::l2')) ∧
1060 (c ≠ c0 →(* test false *)
1061 t2 = midtape (FinProd … FSUnialpha FinBool)
1062 ((reverse ? l1)@〈c,true〉::ls) 〈c0,false〉 l2))).
1064 definition R_comp_step_false ≝
1066 ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
1067 is_marked ? c = false ∧ t2 = t1.
1069 lemma is_marked_to_exists: ∀alpha,c. is_marked alpha c = true →
1071 #alpha * #c * [#_ @(ex_intro … c) //| normalize #H destruct]
1074 lemma exists_current: ∀alpha,c,t.
1075 current alpha t = Some alpha c → ∃ls,rs. t= midtape ? ls c rs.
1077 [whd in ⊢ (??%?→?); #H destruct
1078 |#a #l whd in ⊢ (??%?→?); #H destruct
1079 |#a #l whd in ⊢ (??%?→?); #H destruct
1080 |#ls #c1 #rs whd in ⊢ (??%?→?); #H destruct
1081 @(ex_intro … ls) @(ex_intro … rs) //
1085 lemma sem_comp_step :
1086 accRealize ? comp_step (inr … (inl … (inr … start_nop)))
1087 R_comp_step_true R_comp_step_false.
1088 @(acc_sem_if_app … (sem_test_char ? (is_marked ?))
1089 (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
1090 (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ??
1091 (sem_comp_step_subcase FSUnialpha 〈null,true〉 ??
1092 (sem_clear_mark …))))
1094 [#intape #outape #ta #Hta #Htb cases Hta * #cm * #Hcur
1095 cases (exists_current … Hcur) #ls * #rs #Hintape #cmark
1096 cases (is_marked_to_exists … cmark) #c #Hcm
1097 >Hintape >Hcm -Hintape -Hcm #Hta
1098 @(ex_intro … ls) @(ex_intro … c) @(ex_intro …rs) % [//] lapply Hta -Hta
1099 (* #ls #c #rs #Hintape whd in Hta;
1100 >Hintape in Hta; * #_ -Hintape forse non serve *)
1101 cases (true_or_false (c==bit false)) #Hc
1103 [%[whd in ⊢ ((??%?)→?); #Hdes destruct
1104 |#Hc @(proj1 ?? (proj1 ?? (Htb … Hta) (refl …)))
1106 |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (Htb … Hta) (refl …)))
1108 |cases (true_or_false (c==bit true)) #Hc1
1110 cut (〈bit true, true〉 ≠ 〈bit false, true〉) [% #Hdes destruct] #Hneq %
1111 [%[whd in ⊢ ((??%?)→?); #Hdes destruct
1112 |#Hc @(proj1 … (proj1 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) (refl …)))
1114 |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (proj2 ?? (Htb … Hta) Hneq … Hta)(refl …)))
1116 |cases (true_or_false (c==null)) #Hc2
1118 cut (〈null, true〉 ≠ 〈bit false, true〉) [% #Hdes destruct] #Hneq
1119 cut (〈null, true〉 ≠ 〈bit true, true〉) [% #Hdes destruct] #Hneq1 %
1120 [%[whd in ⊢ ((??%?)→?); #Hdes destruct
1121 |#Hc @(proj1 … (proj1 ?? (proj2 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) Hneq1 … Hta) (refl …)))
1123 |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (proj2 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) Hneq1 … Hta) (refl …)))
1125 |#Hta cut (bit_or_null c = false)
1126 [lapply Hc; lapply Hc1; lapply Hc2 -Hc -Hc1 -Hc2
1127 cases c normalize [* normalize /2/] /2/] #Hcut %
1128 [%[cases (Htb … Hta) #_ -Htb #Htb
1129 cases (Htb … Hta) [2: % #H destruct (H) normalize in Hc; destruct] #_ -Htb #Htb
1130 cases (Htb … Hta) [2: % #H destruct (H) normalize in Hc1; destruct] #_ -Htb #Htb
1131 lapply (Htb ?) [% #H destruct (H) normalize in Hc2; destruct]
1132 * #_ #Houttape #_ @(Houttape … Hta)
1135 |#l1 #c0 #l2 >Hcut #H destruct
1140 |#intape #outape #ta #Hta #Htb #ls #c #rs #Hintape
1141 >Hintape in Hta; whd in ⊢ (%→?); * #Hmark #Hta % [@Hmark //]
1146 (* old universal version
1148 definition R_comp_step_true ≝ λt1,t2.
1149 ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls 〈c,true〉 rs →
1150 (* bit_or_null c = false *)
1151 (bit_or_null c = false → t2 = midtape ? ls 〈c,false〉 rs) ∧
1152 (* no marks in rs *)
1153 (bit_or_null c = true →
1154 (∀c.memb ? c rs = true → is_marked ? c = false) →
1155 ∀a,l. (a::l) = reverse ? (〈c,true〉::rs) →
1156 t2 = rightof (FinProd FSUnialpha FinBool) a (l@ls)) ∧
1158 bit_or_null c = true →
1159 (∀c.memb ? c l1 = true → is_marked ? c = false) →
1160 rs = l1@〈c0,true〉::l2 →
1162 l2 = [ ] → (* test true but l2 is empty *)
1163 t2 = rightof ? 〈c0,false〉 ((reverse ? l1)@〈c,true〉::ls)) ∧
1165 ∀a,a0,b,l1',l2'. (* test true and l2 is not empty *)
1166 〈a,false〉::l1' = l1@[〈c0,false〉] →
1168 t2 = midtape ? (〈c,false〉::ls) 〈a,true〉 (l1'@〈a0,true〉::l2')) ∧
1169 (c ≠ c0 →(* test false *)
1170 t2 = midtape (FinProd … FSUnialpha FinBool)
1171 ((reverse ? l1)@〈c,true〉::ls) 〈c0,false〉 l2)).
1173 definition R_comp_step_false ≝
1175 ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
1176 is_marked ? c = false ∧ t2 = t1.
1179 lemma is_marked_to_exists: ∀alpha,c. is_marked alpha c = true →
1183 lemma sem_comp_step :
1184 accRealize ? comp_step (inr … (inl … (inr … start_nop)))
1185 R_comp_step_true R_comp_step_false.
1186 @(acc_sem_if_app … (sem_test_char ? (is_marked ?))
1187 (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
1188 (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ??
1189 (sem_comp_step_subcase FSUnialpha 〈null,true〉 ??
1190 (sem_clear_mark …))))
1192 [#intape #outape #ta #Hta #Htb #ls #c #rs #Hintape whd in Hta;
1193 >Hintape in Hta; * #_ -Hintape (* forse non serve *)
1194 cases (true_or_false (c==bit false)) #Hc
1196 [%[whd in ⊢ ((??%?)→?); #Hdes destruct
1197 |#Hc @(proj1 ?? (proj1 ?? (Htb … Hta) (refl …)))
1199 |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (Htb … Hta) (refl …)))
1201 |cases (true_or_false (c==bit true)) #Hc1
1203 cut (〈bit true, true〉 ≠ 〈bit false, true〉) [% #Hdes destruct] #Hneq %
1204 [%[whd in ⊢ ((??%?)→?); #Hdes destruct
1205 |#Hc @(proj1 … (proj1 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) (refl …)))
1207 |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (proj2 ?? (Htb … Hta) Hneq … Hta)(refl …)))
1209 |cases (true_or_false (c==null)) #Hc2
1211 cut (〈null, true〉 ≠ 〈bit false, true〉) [% #Hdes destruct] #Hneq
1212 cut (〈null, true〉 ≠ 〈bit true, true〉) [% #Hdes destruct] #Hneq1 %
1213 [%[whd in ⊢ ((??%?)→?); #Hdes destruct
1214 |#Hc @(proj1 … (proj1 ?? (proj2 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) Hneq1 … Hta) (refl …)))
1216 |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (proj2 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) Hneq1 … Hta) (refl …)))
1218 |#Hta cut (bit_or_null c = false)
1219 [lapply Hc; lapply Hc1; lapply Hc2 -Hc -Hc1 -Hc2
1220 cases c normalize [* normalize /2/] /2/] #Hcut %
1221 [%[cases (Htb … Hta) #_ -Htb #Htb
1222 cases (Htb … Hta) [2: % #H destruct (H) normalize in Hc; destruct] #_ -Htb #Htb
1223 cases (Htb … Hta) [2: % #H destruct (H) normalize in Hc1; destruct] #_ -Htb #Htb
1224 lapply (Htb ?) [% #H destruct (H) normalize in Hc2; destruct]
1225 * #_ #Houttape #_ @(Houttape … Hta)
1228 |#l1 #c0 #l2 >Hcut #H destruct
1233 |#intape #outape #ta #Hta #Htb #ls #c #rs #Hintape
1234 >Hintape in Hta; whd in ⊢ (%→?); * #Hmark #Hta % [@Hmark //]
1240 definition R_comp_step_true ≝
1242 ∀l0,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) l0 c rs →
1243 ∃c'. c = 〈c',true〉 ∧
1244 ((bit_or_null c' = true ∧
1246 rs = 〈a,false〉::l1@〈c0,true〉::〈a0,false〉::l2 →
1247 (∀c.memb ? c l1 = true → is_marked ? c = false) →
1249 t2 = midtape ? (〈c',false〉::l0) 〈a,true〉 (l1@〈c0,false〉::〈a0,true〉::l2)) ∨
1251 t2 = midtape (FinProd … FSUnialpha FinBool)
1252 (reverse ? l1@〈a,false〉::〈c',true〉::l0) 〈c0,false〉 (〈a0,false〉::l2))) ∨
1253 (bit_or_null c' = false ∧ t2 = midtape ? l0 〈c',false〉 rs)).
1255 definition R_comp_step_false ≝
1257 ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
1258 is_marked ? c = false ∧ t2 = t1.
1260 lemma sem_comp_step :
1261 accRealize ? comp_step (inr … (inl … (inr … start_nop)))
1262 R_comp_step_true R_comp_step_false.
1264 cases (acc_sem_if … (sem_test_char ? (is_marked ?))
1265 (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
1266 (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ??
1267 (sem_comp_step_subcase FSUnialpha 〈null,true〉 ??
1268 (sem_clear_mark …))))
1270 #k * #outc * * #Hloop #H1 #H2
1271 @(ex_intro ?? k) @(ex_intro ?? outc) %
1272 [ % [@Hloop ] ] -Hloop
1273 [ #Hstate lapply (H1 Hstate) -H1 -Hstate -H2 *
1274 #ta * whd in ⊢ (%→?); #Hleft #Hright #ls #c #rs #Hintape
1275 >Hintape in Hleft; * *
1276 cases c in Hintape; #c' #b #Hintape #x * whd in ⊢ (??%?→?); #H destruct (H)
1277 whd in ⊢ (??%?→?); #Hb >Hb #Hta @(ex_intro ?? c') % //
1278 cases (Hright … Hta)
1279 [ * #Hc' #H1 % % [destruct (Hc') % ]
1280 #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
1281 cases (H1 … Hl1 Hrs)
1282 [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
1283 | * #Hneq #Houtc %2 %
1287 | * #Hc #Helse1 cases (Helse1 … Hta)
1288 [ * #Hc' #H1 % % [destruct (Hc') % ]
1289 #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
1290 cases (H1 … Hl1 Hrs)
1291 [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
1292 | * #Hneq #Houtc %2 %
1296 | * #Hc' #Helse2 cases (Helse2 … Hta)
1297 [ * #Hc'' #H1 % % [destruct (Hc'') % ]
1298 #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
1299 cases (H1 … Hl1 Hrs)
1300 [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
1301 | * #Hneq #Houtc %2 %
1305 | * #Hc'' whd in ⊢ (%→?); #Helse3 %2 %
1306 [ generalize in match Hc''; generalize in match Hc'; generalize in match Hc;
1308 [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
1309 | #Hfalse @False_ind @(absurd ?? Hfalse) % ]
1310 | #_ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
1317 | #Hstate lapply (H2 Hstate) -H1 -Hstate -H2 *
1318 #ta * whd in ⊢ (%→%→?); #Hleft #Hright #ls #c #rs #Hintape
1319 >Hintape in Hleft; * #Hc #Hta % [@Hc % | >Hright //]
1323 definition compare ≝
1324 whileTM ? comp_step (inr … (inl … (inr … start_nop))).
1327 definition R_compare :=
1331 ∀ls,c,b,rs.t1 = midtape ? ls 〈c,b〉 rs →
1332 (b = true → rs = ....) →
1333 (b = false ∧ ....) ∨
1336 rs = cs@l1@〈c0,true〉::cs0@l2
1340 ls 〈c,b〉 cs l1 〈c0,b0〉 cs0 l2
1344 ls (hd (Ls@〈grid,false〉))* (tail (Ls@〈grid,false〉)) l1 (hd (Ls@〈comma,false〉))* (tail (Ls@〈comma,false〉)) l2
1345 ^^^^^^^^^^^^^^^^^^^^^^^
1347 ls Ls 〈grid,false〉 l1 Ls 〈comma,true〉 l2
1352 ls (hd (Ls@〈c,false〉))* (tail (Ls@〈c,false〉)) l1 (hd (Ls@〈d,false〉))* (tail (Ls@〈d,false〉)) l2
1353 ^^^^^^^^^^^^^^^^^^^^^^^
1356 ls Ls 〈c,true〉 l1 Ls 〈d,false〉 l2
1362 (∃la,d.〈b,true〉::bs = la@[〈grid,d〉] ∧ ∀x.memb ? x la → is_bit (\fst x) = true) →
1363 (∃lb,d0.〈b0,true〉::b0s = lb@[〈comma,d0〉] ∧ ∀x.memb ? x lb → is_bit (\fst x) = true) →
1364 t1 = midtape ? l0 〈b,true〉 (bs@l1@〈b0,true〉::b0s@l2 →
1366 mk_tape left (option current) right
1368 (b = grid ∧ b0 = comma ∧ bs = [] ∧ b0s = [] ∧
1369 t2 = midtape ? l0 〈grid,false〉 (l1@〈comma,true〉::l2)) ∨
1370 (b = bit x ∧ b = c ∧ bs = b0s
1373 definition list_cases2: ∀A.∀P:list A →list A →Prop.∀l1,l2. |l1| = |l2| →
1374 P [ ] [ ] → (∀a1,a2:A.∀tl1,tl2. |tl1| = |tl2| → P (a1::tl1) (a2::tl2)) → P l1 l2.
1375 #A #P #l1 #l2 #Hlen lapply Hlen @(list_ind2 … Hlen) //
1376 #tl1 #tl2 #hd1 #hd2 #Hind normalize #HlenS #H1 #H2 @H2 //
1379 definition R_compare :=
1381 ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
1382 (∀c'.bit_or_null c' = false → c = 〈c',true〉 → t2 = midtape ? ls 〈c',false〉 rs) ∧
1383 (∀c'. c = 〈c',false〉 → t2 = t1) ∧
1384 (* forse manca il caso no marks in rs *)
1387 (∀c.memb (FinProd … FSUnialpha FinBool) c bs = true → bit_or_null (\fst c) = true) →
1388 (∀c.memb (FinProd … FSUnialpha FinBool) c b0s = true → bit_or_null (\fst c) = true) →
1389 (∀c.memb ? c bs = true → is_marked ? c = false) →
1390 (∀c.memb ? c b0s = true → is_marked ? c = false) →
1391 (∀c.memb ? c l1 = true → is_marked ? c = false) →
1392 c = 〈b,true〉 → bit_or_null b = true →
1393 rs = bs@〈grid,false〉::l1@〈b0,true〉::b0s@〈comma,false〉::l2 →
1394 (〈b,true〉::bs = 〈b0,true〉::b0s ∧
1395 t2 = midtape ? (reverse ? bs@〈b,false〉::ls)
1396 〈grid,false〉 (l1@〈b0,false〉::b0s@〈comma,true〉::l2)) ∨
1397 (∃la,c',d',lb,lc.c' ≠ d' ∧
1398 〈b,false〉::bs = la@〈c',false〉::lb ∧
1399 〈b0,false〉::b0s = la@〈d',false〉::lc ∧
1400 t2 = midtape (FinProd … FSUnialpha FinBool) (reverse ? la@
1406 〈d',false〉 (lc@〈comma,false〉::l2)).
1408 lemma wsem_compare : WRealize ? compare R_compare.
1410 lapply (sem_while ?????? sem_comp_step t i outc Hloop) [%]
1411 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
1412 [ #tapea whd in ⊢ (%→?); #Rfalse #ls #c #rs #Htapea %
1414 [ #c' #Hc' #Hc lapply (Rfalse … Htapea) -Rfalse * >Hc
1415 whd in ⊢ (??%?→?); #Hfalse destruct (Hfalse)
1416 | #c' #Hc lapply (Rfalse … Htapea) -Rfalse * #_
1418 | #b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1 #Hc
1419 cases (Rfalse … Htapea) -Rfalse >Hc whd in ⊢ (??%?→?);#Hfalse destruct (Hfalse)
1421 | #tapea #tapeb #tapec #Hleft #Hright #IH #Htapec lapply (IH Htapec) -Htapec -IH #IH
1422 whd in Hleft; #ls #c #rs #Htapea cases Hleft -Hleft
1423 #ls0 * #c' * #rs0 * >Htapea #Hdes destruct (Hdes) * *
1424 cases (true_or_false (bit_or_null c')) #Hc'
1425 [2: #Htapeb lapply (Htapeb Hc') -Htapeb #Htapeb #_ #_ %
1426 [%[#c1 #Hc1 #Heqc destruct (Heqc)
1427 cases (IH … Htapeb) * #_ #H #_ <Htapeb @(H … (refl…))
1428 |#c1 #Heqc destruct (Heqc)
1430 |#b #b0 #bs #b0s #l1 #l2 #_ #_ #_ #_ #_ #_
1431 #Heq destruct (Heq) >Hc' #Hfalse @False_ind destruct (Hfalse)
1433 |#_ (* no marks in rs ??? *) #_ #Hleft %
1435 [ #c'' #Hc'' #Heq destruct (Heq) >Hc'' in Hc'; #H destruct (H)
1436 | #c0 #Hfalse destruct (Hfalse)
1438 |#b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1
1439 #Heq destruct (Heq) #_ >append_cons; <associative_append #Hrs
1440 cases (Hleft … Hc' … Hrs) -Hleft
1441 [2: #c1 #memc1 cases (memb_append … memc1) -memc1 #memc1
1442 [cases (memb_append … memc1) -memc1 #memc1
1443 [@Hbs2 @memc1 |>(memb_single … memc1) %]
1446 |* (* manca il caso in cui dopo una parte uguale il
1447 secondo nastro finisca ... ???? *)
1448 #_ cases (true_or_false (b==b0)) #eqbb0
1449 [2: #_ #Htapeb %2 lapply (Htapeb … (\Pf eqbb0)) -Htapeb #Htapeb
1450 cases (IH … Htapeb) * #_ #Hout #_
1451 @(ex_intro … []) @(ex_intro … b) @(ex_intro … b0)
1452 @(ex_intro … bs) @(ex_intro … b0s) %
1453 [%[%[@(\Pf eqbb0) | %] | %]
1454 |>(Hout … (refl …)) -Hout >Htapeb @eq_f3 [2,3:%]
1455 >reverse_append >reverse_append >associative_append
1456 >associative_append %
1458 |lapply Hbs1 lapply Hb0s1 lapply Hbs2 lapply Hb0s2 lapply Hrs
1459 -Hbs1 -Hb0s1 -Hbs2 -Hb0s2 -Hrs
1460 @(list_cases2 … Hlen)
1461 [#Hrs #_ #_ #_ #_ >associative_append >associative_append #Htapeb #_
1462 lapply (Htapeb … (\P eqbb0) … (refl …) (refl …)) -Htapeb #Htapeb
1463 cases (IH … Htapeb) -IH * #Hout #_ #_ %1 %
1465 |>(Hout grid (refl …) (refl …)) @eq_f
1466 normalize >associative_append %
1468 |* #a1 #ba1 * #a2 #ba2 #tl1 #tl2 #HlenS #Hrs #Hb0s2 #Hbs2 #Hb0s1 #Hbs1
1469 cut (ba1 = false) [@(Hbs2 〈a1,ba1〉) @memb_hd] #Hba1 >Hba1
1470 >associative_append >associative_append #Htapeb #_
1471 lapply (Htapeb … (\P eqbb0) … (refl …) (refl …)) -Htapeb #Htapeb
1472 cases (IH … Htapeb) -IH * #_ #_
1473 cut (ba2=false) [@(Hb0s2 〈a2,ba2〉) @memb_hd] #Hba2 >Hba2
1474 #IH cases(IH a1 a2 ?? (l1@[〈b0,false〉]) l2 HlenS ????? (refl …) ??)
1475 [3:#x #memx @Hbs1 @memb_cons @memx
1476 |4:#x #memx @Hb0s1 @memb_cons @memx
1477 |5:#x #memx @Hbs2 @memb_cons @memx
1478 |6:#x #memx @Hb0s2 @memb_cons @memx
1479 |7:#x #memx cases (memb_append …memx) -memx #memx
1480 [@Hl1 @memx | >(memb_single … memx) %]
1481 |8:@(Hbs1 〈a1,ba1〉) @memb_hd
1482 |9: >associative_append >associative_append %
1483 |-IH -Hbs1 -Hb0s1 -Hbs2 -Hrs *
1485 [>(\P eqbb0) @eq_f destruct (Ha1a2) %
1487 [>reverse_cons >associative_append %
1489 |>associative_append %
1492 |-IH -Hbs1 -Hb0s1 -Hbs2 -Hrs *
1493 #la * #c' * #d' * #lb * #lc * * *
1494 #Hcd #H1 #H2 #Houtc %2
1495 @(ex_intro … (〈b,false〉::la)) @(ex_intro … c') @(ex_intro … d')
1496 @(ex_intro … lb) @(ex_intro … lc) %
1497 [%[%[@Hcd | >H1 %] |>(\P eqbb0) >Hba2 >H2 %]
1499 [>(\P eqbb0) >reverse_append >reverse_cons
1500 >reverse_cons >associative_append >associative_append
1501 >associative_append >associative_append %
1515 lemma WF_cst_niltape:
1516 WF ? (inv ? R_comp_step_true) (niltape (FinProd FSUnialpha FinBool)).
1517 @wf #t1 whd in ⊢ (%→?); * #ls * #c * #rs * #H destruct
1520 lemma WF_cst_rightof:
1521 ∀a,ls. WF ? (inv ? R_comp_step_true) (rightof (FinProd FSUnialpha FinBool) a ls).
1522 #a #ls @wf #t1 whd in ⊢ (%→?); * #ls * #c * #rs * #H destruct
1525 lemma WF_cst_leftof:
1526 ∀a,ls. WF ? (inv ? R_comp_step_true) (leftof (FinProd FSUnialpha FinBool) a ls).
1527 #a #ls @wf #t1 whd in ⊢ (%→?); * #ls * #c * #rs * #H destruct
1530 lemma WF_cst_midtape_false:
1531 ∀ls,c,rs. WF ? (inv ? R_comp_step_true)
1532 (midtape (FinProd … FSUnialpha FinBool) ls 〈c,false〉 rs).
1533 #ls #c #rs @wf #t1 whd in ⊢ (%→?); * #ls' * #c' * #rs' * #H destruct
1537 lemma not_nil_to_exists:∀A.∀l: list A. l ≠ [ ] →
1539 #A * [* #H @False_ind @H // | #a #tl #_ @(ex_intro … a) @(ex_intro … tl) //]
1542 axiom daemon : ∀P:Prop.P.
1544 lemma terminate_compare:
1545 ∀t. Terminate ? compare t.
1546 #t @(terminate_while … sem_comp_step) [%]
1547 cases t // #ls * #c * //
1548 #rs lapply ls; lapply c; -ls -c
1549 (* we cannot proceed by structural induction on the right tape,
1550 since compare moves the marks! *)
1552 [#c #ls @wf #t1 whd in ⊢ (%→?); * #ls0 * #c0 * #rs0 * #Hmid destruct (Hmid)
1553 * * #H1 #H2 #_ cases (true_or_false (bit_or_null c0)) #Hc0
1554 [>(H2 Hc0 … (refl …)) // #x whd in ⊢ ((??%?)→?); #Hdes destruct
1557 |#a #rs' #Hind #c #ls @wf #t1 whd in ⊢ (%→?); * #ls0 * #c0 * #rs0 * #Hmid destruct (Hmid)
1558 * * #H1 #H2 #H3 cases (true_or_false (bit_or_null c0)) #Hc0
1559 [-H1 cases (split_on_spec_ex ? (a::rs') (is_marked ?)) #rs1 * #rs2
1561 [(* no marks in right tape *)
1562 * * >append_nil #H >H -H #Hmarks #_
1563 cases (not_nil_to_exists ? (reverse (FSUnialpha×bool) (〈c0,true〉::a::rs')) ?)
1564 [2: % >reverse_cons #H cases (nil_to_nil … H) #_ #H1 destruct]
1565 #a0 * #tl #H4 >(H2 Hc0 Hmarks a0 tl H4) //
1566 |(* the first marked element is a0 *)
1567 * #a0 #a0b #rs3 * * #H4 #H5 #H6 lapply (H3 ? a0 rs3 … Hc0 H5 ?)
1568 [<H4 @eq_f @eq_f2 [@eq_f @(H6 〈a0,a0b〉 … (refl …)) | %]
1569 |cases (true_or_false (c0==a0)) #eqc0a0 (* comparing a0 with c0 *)
1570 [* * (* we check if we have elements at the right of a0 *) cases rs3
1571 [#Ht1 #_ #_ >(Ht1 (\P eqc0a0) (refl …)) //
1572 |(* a1 will be marked *)
1573 cases (not_nil_to_exists ? (rs1@[〈a0,false〉]) ?)
1574 [2: % #H cases (nil_to_nil … H) #_ #H1 destruct]
1575 * #a2 #a2b * #tl2 #H7 * #a1 #a1b #rs4 #_ #Ht1 #_
1576 cut (a2b =false) [@daemon] #Ha2b >Ha2b in H7; #H7
1577 >(Ht1 (\P eqc0a0) … H7 (refl …))
1578 cut (rs' = tl2@〈a1,true〉::rs4)
1579 cut (a0b=false) [@(H6 〈a0,a0b〉)
1585 axiom sem_compare : Realize ? compare R_compare.