]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/turing/universal/marks.ma
2a819926684c70df9863981782e8ec8ebc1a1510
[helm.git] / matita / matita / lib / turing / universal / marks.ma
1 (*
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.           
5     ||I||                                                            
6     ||T||  
7     ||A||  
8     \   /  This file is distributed under the terms of the       
9      \ /   GNU General Public License Version 2   
10       V_____________________________________________________________*)
11
12
13 (* COMPARE BIT
14
15 *)
16
17 include "turing/if_machine.ma".
18 include "turing/basic_machines.ma".
19 include "turing/universal/alphabet.ma".
20
21 (* ADVANCE TO MARK (right)
22
23    sposta la testina a destra fino a raggiungere il primo carattere marcato 
24    
25 *)
26
27 (* 0, a ≠ mark _ ⇒ 0, R
28 0, a = mark _ ⇒ 1, N *)
29
30 definition atm_states ≝ initN 3.
31
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 …)).
35
36 definition atmr_step ≝ 
37   λalpha:FinSet.λtest:alpha→bool.
38   mk_TM alpha atm_states
39   (λp.let 〈q,a〉 ≝ p in
40    match a with
41    [ None ⇒ 〈atm1, None ?〉
42    | Some a' ⇒ 
43      match test a' with
44      [ true ⇒ 〈atm1,None ?〉
45      | false ⇒ 〈atm2,Some ? 〈a',R〉〉 ]])
46   atm0 (λx.notb (x == atm0)).
47
48 definition Ratmr_step_true ≝ 
49   λalpha,test,t1,t2.
50    ∃ls,a,rs.
51    t1 = midtape alpha ls a rs ∧ test a = false ∧ 
52    t2 = mk_tape alpha (a::ls) (option_hd ? rs) (tail ? rs).
53    
54 definition Ratmr_step_false ≝ 
55   λalpha,test,t1,t2.
56     t1 = t2 ∧
57     (current alpha t1 = None ? ∨
58      (∃a.current ? t1 = Some ? a ∧ test a = true)).
59      
60 lemma atmr_q0_q1 :
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
65     (midtape … ls a0 rs).
66 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
67 whd in match (trans … 〈?,?〉); >Htest %
68 qed.
69      
70 lemma atmr_q0_q2 :
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 //
78 qed.
79
80 lemma sem_atmr_step :
81   ∀alpha,test.
82   accRealize alpha (atmr_step alpha test) 
83     atm2 (Ratmr_step_true alpha test) (Ratmr_step_false alpha test).
84 #alpha #test *
85 [ @(ex_intro ?? 2)
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 ?))
95     [| % 
96       [ % 
97         [ whd in ⊢ (??%?); >atmr_q0_q1 //
98         | whd in ⊢ ((??%%)→?); #Hfalse destruct ]
99       | #_ % // %2 @(ex_intro ?? c) % // ]
100     ]
101   | @(ex_intro ?? (mk_config ?? atm2 (mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs))))
102     % 
103     [ %
104       [ whd in ⊢ (??%?); >atmr_q0_q2 //
105       | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
106         % // % //
107       ]
108     | #Hfalse @False_ind @(absurd ?? Hfalse) %
109     ]
110   ]
111 ]
112 qed.
113
114 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
115   ∀ls,c,rs.
116   (t1 = midtape alpha ls c rs  → 
117   ((test c = true ∧ t2 = t1) ∨
118    (test c = false ∧
119     ∀rs1,b,rs2. rs = rs1@b::rs2 → 
120      test b = true → (∀x.memb ? x rs1 = true → test x = false) → 
121      t2 = midtape ? (reverse ? rs1@c::ls) b rs2))).
122      
123 definition adv_to_mark_r ≝ 
124   λalpha,test.whileTM alpha (atmr_step alpha test) atm2.
125
126 lemma wsem_adv_to_mark_r :
127   ∀alpha,test.
128   WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
129 #alpha #test #t #i #outc #Hloop
130 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
131 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
132 [ #tapea * #Htapea *
133   [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
134     #Hfalse destruct (Hfalse)
135   | * #a * #Ha #Htest #ls #c #rs #H2 %
136     >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
137     <Htapea //
138   ]
139 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
140   lapply (IH HRfalse) -IH #IH
141   #ls #c #rs #Htapea %2
142   cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
143   
144   >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
145   [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
146     cases (IH … Htapeb)
147     [ * #_ #Houtc >Houtc >Htapeb %
148     | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
149   | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
150     cases (IH … Htapeb)
151     [ * #Hfalse >(Hmemb …) in Hfalse;
152       [ #Hft destruct (Hft)
153       | @memb_hd ]
154     | * #Htestr1 #H1 >reverse_cons >associative_append
155       @H1 // #x #Hx @Hmemb @memb_cons //
156     ]
157   ]
158 qed.
159
160 lemma terminate_adv_to_mark_r :
161   ∀alpha,test.
162   ∀t.Terminate alpha (adv_to_mark_r alpha test) t.
163 #alpha #test #t
164 @(terminate_while … (sem_atmr_step alpha test))
165   [ %
166   | cases t
167     [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse) 
168     |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse) 
169     | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
170       elim rs
171       [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
172        #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1; 
173        % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
174        normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
175       | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
176         #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
177         >Ht1 @IH
178       ]
179     ]
180   ]
181 qed.
182
183 lemma sem_adv_to_mark_r :
184   ∀alpha,test.
185   Realize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
186 /2/
187 qed.
188
189 (* MARK machine
190
191    marks the current character 
192  *)
193  
194 definition mark_states ≝ initN 2.
195
196 definition ms0 : mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
197 definition ms1 : mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
198
199 definition mark ≝ 
200   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
201   (λp.let 〈q,a〉 ≝ p in
202     match a with
203     [ None ⇒ 〈ms1,None ?〉
204     | Some a' ⇒ match (pi1 … q) with
205       [ O ⇒ let 〈a'',b〉 ≝ a' in 〈ms1,Some ? 〈〈a'',true〉,N〉〉
206       | S q ⇒ 〈ms1,None ?〉 ] ])
207   ms0 (λq.q == ms1).
208   
209 definition R_mark ≝ λalpha,t1,t2.
210   ∀ls,c,b,rs.
211   t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs → 
212   t2 = midtape ? ls 〈c,true〉 rs.
213     
214 lemma sem_mark :
215   ∀alpha.Realize ? (mark alpha) (R_mark alpha).
216 #alpha #intape @(ex_intro ?? 2) cases intape
217 [ @ex_intro
218   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
219 |#a #al @ex_intro
220   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
221 |#a #al @ex_intro
222   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
223 | #ls * #c #b #rs
224   @ex_intro [| % [ % | #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ] ] ]
225 qed.
226
227
228 (* MOVE RIGHT AND MARK machine
229
230    marks the first character on the right
231    
232    (could be rewritten using (mark; move_right))
233  *)
234  
235 definition mrm_states ≝ initN 3.
236
237 definition mrm0 : mrm_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
238 definition mrm1 : mrm_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
239 definition mrm2 : mrm_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
240
241 definition move_right_and_mark ≝ 
242   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mrm_states
243   (λp.let 〈q,a〉 ≝ p in
244     match a with
245     [ None ⇒ 〈mrm2,None ?〉
246     | Some a' ⇒ match pi1 … q with
247       [ O ⇒ 〈mrm1,Some ? 〈a',R〉〉
248       | S q ⇒ match q with
249         [ O ⇒ let 〈a'',b〉 ≝ a' in
250               〈mrm2,Some ? 〈〈a'',true〉,N〉〉
251         | S _ ⇒ 〈mrm2,None ?〉 ] ] ])
252   mrm0 (λq.q == mrm2).
253   
254 definition R_move_right_and_mark ≝ λalpha,t1,t2.
255   ∀ls,c,d,b,rs.
256   t1 = midtape (FinProd … alpha FinBool) ls c (〈d,b〉::rs) → 
257   t2 = midtape ? (c::ls) 〈d,true〉 rs.
258     
259 lemma sem_move_right_and_mark :
260   ∀alpha.Realize ? (move_right_and_mark alpha) (R_move_right_and_mark alpha).
261 #alpha #intape @(ex_intro ?? 3) cases intape
262 [ @ex_intro
263   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
264 |#a #al @ex_intro
265   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
266 |#a #al @ex_intro
267   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
268 | #ls #c *
269   [ @ex_intro [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #Hfalse destruct ] ]
270   | * #d #b #rs @ex_intro
271     [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #H1 destruct (H1) % ] ] ] ]
272 qed.
273
274 (* CLEAR MARK machine
275
276    clears the mark in the current character 
277  *)
278  
279 definition clear_mark_states ≝ initN 3.
280
281 definition clear0 : clear_mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
282 definition clear1 : clear_mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
283 definition claer2 : clear_mark_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
284
285 definition clear_mark ≝ 
286   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) clear_mark_states
287   (λp.let 〈q,a〉 ≝ p in
288     match a with
289     [ None ⇒ 〈clear1,None ?〉
290     | Some a' ⇒ match pi1 … q with
291       [ O ⇒ let 〈a'',b〉 ≝ a' in 〈clear1,Some ? 〈〈a'',false〉,N〉〉
292       | S q ⇒ 〈clear1,None ?〉 ] ])
293   clear0 (λq.q == clear1).
294   
295 definition R_clear_mark ≝ λalpha,t1,t2.
296   ∀ls,c,b,rs.
297   t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs → 
298   t2 = midtape ? ls 〈c,false〉 rs.
299     
300 lemma sem_clear_mark :
301   ∀alpha.Realize ? (clear_mark alpha) (R_clear_mark alpha).
302 #alpha #intape @(ex_intro ?? 2) cases intape
303 [ @ex_intro
304   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
305 |#a #al @ex_intro
306   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
307 |#a #al @ex_intro
308   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
309 | #ls * #c #b #rs
310   @ex_intro [| % [ % | #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ] ] ]
311 qed.
312
313 (* ADVANCE MARK RIGHT machine
314
315    clears mark on current char,
316    moves right, and marks new current char
317    
318 *)
319
320 definition adv_mark_r ≝ 
321   λalpha:FinSet.
322     clear_mark alpha · move_r ? · mark alpha.
323       
324 definition R_adv_mark_r ≝ λalpha,t1,t2.
325   ∀ls,c,d,b,rs.
326   t1 = midtape (FinProd … alpha FinBool) ls 〈c,true〉 (〈d,b〉::rs) → 
327   t2 = midtape ? (〈c,false〉::ls) 〈d,true〉 rs.
328   
329 lemma sem_adv_mark_r : 
330   ∀alpha.Realize ? (adv_mark_r alpha) (R_adv_mark_r alpha).
331 #alpha #intape
332 cases (sem_seq ????? (sem_clear_mark …) 
333          (sem_seq ????? (sem_move_r ?) (sem_mark alpha)) intape)
334 #k * #outc * #Hloop whd in ⊢ (%→?);
335 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→%→?); #Hs2 #Hs3
336 @(ex_intro ?? k) @(ex_intro ?? outc) %
337 [ @Hloop
338 | -Hloop #ls #c #d #b #rs #Hintape @(Hs3 … b)
339   @(Hs2 ls 〈c,false〉 (〈d,b〉::rs))
340   @(Hs1 … Hintape)
341 ]
342 qed.
343
344 (* ADVANCE TO MARK (left)
345
346 axiomatized
347
348 *)
349
350 definition R_adv_to_mark_l ≝ λalpha,test,t1,t2.
351   ∀ls,c,rs.
352   (t1 = midtape alpha ls c rs  → 
353   ((test c = true ∧ t2 = t1) ∨
354    (test c = false ∧
355     ∀ls1,b,ls2. ls = ls1@b::ls2 → 
356      test b = true → (∀x.memb ? x ls1 = true → test x = false) → 
357      t2 = midtape ? ls2 b (reverse ? ls1@c::rs)))).
358
359 axiom adv_to_mark_l : ∀alpha:FinSet.(alpha → bool) → TM alpha.
360 (* definition adv_to_mark_l ≝ 
361   λalpha,test.whileTM alpha (atml_step alpha test) 2. *)
362
363 axiom wsem_adv_to_mark_l :
364   ∀alpha,test.
365   WRealize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
366 (*
367 #alpha #test #t #i #outc #Hloop
368 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
369 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
370 [ #tapea * #Htapea *
371   [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
372     #Hfalse destruct (Hfalse)
373   | * #a * #Ha #Htest #ls #c #rs #H2 %
374     >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
375     <Htapea //
376   ]
377 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
378   lapply (IH HRfalse) -IH #IH
379   #ls #c #rs #Htapea %2
380   cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
381   
382   >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
383   [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
384     cases (IH … Htapeb)
385     [ * #_ #Houtc >Houtc >Htapeb %
386     | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
387   | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
388     cases (IH … Htapeb)
389     [ * #Hfalse >(Hmemb …) in Hfalse;
390       [ #Hft destruct (Hft)
391       | @memb_hd ]
392     | * #Htestr1 #H1 >reverse_cons >associative_append
393       @H1 // #x #Hx @Hmemb @memb_cons //
394     ]
395   ]
396 qed.
397 *)
398
399 axiom terminate_adv_to_mark_l :
400   ∀alpha,test.
401   ∀t.Terminate alpha (adv_to_mark_l alpha test) t.
402 (*
403 #alpha #test #t
404 @(terminate_while … (sem_atmr_step alpha test))
405   [ %
406   | cases t
407     [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse) 
408     |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse) 
409     | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
410       elim rs
411       [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
412        #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1; 
413        % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
414        normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
415       | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
416         #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
417         >Ht1 @IH
418       ]
419     ]
420   ]
421 qed.
422 *)
423
424 lemma sem_adv_to_mark_l :
425   ∀alpha,test.
426   Realize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
427 /2/
428 qed.
429
430 (*
431    ADVANCE BOTH MARKS machine
432    
433    l1 does not contain marks ⇒
434    
435
436    input:
437    l0 x* a l1 x0* a0 l2
438               ^
439    
440    output:
441    l0 x a* l1 x0 a0* l2
442         ^
443 *)
444
445 definition adv_both_marks ≝ λalpha.
446   adv_mark_r alpha · move_l ? ·
447     adv_to_mark_l (FinProd alpha FinBool) (is_marked alpha) · 
448       adv_mark_r alpha.
449
450 definition R_adv_both_marks ≝ 
451   λalpha,t1,t2.
452     ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) → 
453     t1 = midtape (FinProd … alpha FinBool) 
454         (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) → 
455     t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2).
456
457 lemma sem_adv_both_marks :
458   ∀alpha.Realize ? (adv_both_marks alpha) (R_adv_both_marks alpha).    
459 #alpha #intape
460 cases (sem_seq ????? (sem_adv_mark_r …) 
461         (sem_seq ????? (sem_move_l …)
462           (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?)) 
463             (sem_adv_mark_r alpha))) intape)
464 #k * #outc * #Hloop whd in ⊢ (%→?);
465 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→?); #Hs2
466 * #tc * whd in ⊢ (%→%→?); #Hs3 #Hs4
467 @(ex_intro ?? k) @(ex_intro ?? outc) %
468 [ @Hloop
469 | -Hloop #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
470   @(Hs4 … false) -Hs4
471   lapply (Hs1 … Hintape) #Hta
472   lapply (Hs2 … Hta) #Htb
473   cases (Hs3 … Htb)
474   [ * #Hfalse normalize in Hfalse; destruct (Hfalse)
475   | * #_ -Hs3 #Hs3 
476     lapply (Hs3 (l1@[〈a,false〉]) 〈x,true〉 l0 ???)
477     [ #x1 #Hx1 cases (memb_append … Hx1)
478       [ @Hl1
479       | #Hx1' >(memb_single … Hx1') % ]
480     | % 
481     | >associative_append %
482     | >reverse_append #Htc @Htc ]
483   ]
484 qed.
485
486 (* 
487    MATCH AND ADVANCE(f)
488    
489    input:
490    l0 x* a l1 x0* a0 l2
491               ^
492     
493    output:
494    l0 x a* l1 x0 a0* l2   (f(x0) == true)
495         ^
496    l0 x* a l1 x0* a0 l2   (f(x0) == false)
497               ^
498 *)
499
500 definition match_and_adv ≝ 
501   λalpha,f.ifTM ? (test_char ? f)
502      (adv_both_marks alpha) (clear_mark ?) tc_true.
503
504 definition R_match_and_adv ≝ 
505   λalpha,f,t1,t2.
506     ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) → 
507     t1 = midtape (FinProd … alpha FinBool) 
508         (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) → 
509     (f 〈x0,true〉 = true ∧ t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2))
510     ∨ (f 〈x0,true〉 = false ∧ 
511     t2 = midtape ? (l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)).
512
513 lemma sem_match_and_adv : 
514   ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv alpha f).
515 #alpha #f #intape
516 cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape)
517 #k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
518 % [ @Hloop ] -Hloop
519 cases Hif
520 [ * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
521   #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
522   >Hintape in Hta; #Hta cases (Hta … (refl ??)) -Hta #Hf #Hta % % 
523   [ @Hf | @Houtc [ @Hl1 | @Hta ] ]
524 | * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
525   #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
526   >Hintape in Hta; #Hta cases (Hta … (refl ??)) -Hta #Hf #Hta %2 %
527   [ @Hf | >(Houtc … Hta) % ]
528 ]
529 qed.
530
531 (*
532  if x = c
533       then move_right; ----
534            adv_to_mark_r;
535            if current (* x0 *) = 0
536               then advance_mark ----
537                    adv_to_mark_l;
538                    advance_mark
539               else STOP
540       else M
541 *)
542
543 definition comp_step_subcase ≝ λalpha,c,elseM.
544   ifTM ? (test_char ? (λx.x == c))
545     (move_r … · adv_to_mark_r ? (is_marked alpha) · match_and_adv ? (λx.x == c))
546     elseM tc_true.
547
548 definition R_comp_step_subcase ≝ 
549   λalpha,c,RelseM,t1,t2.
550     ∀l0,x,rs.t1 = midtape (FinProd … alpha FinBool) l0 〈x,true〉 rs → 
551     (〈x,true〉 = c ∧
552      ∀a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) → 
553      rs = 〈a,false〉::l1@〈x0,true〉::〈a0,false〉::l2 → 
554      ((x = x0 ∧
555       t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1@〈x0,false〉::〈a0,true〉::l2)) ∨
556       (x ≠ x0 ∧
557       t2 = midtape (FinProd … alpha FinBool) 
558         (reverse ? l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)))) ∨
559     (〈x,true〉 ≠ c ∧ RelseM t1 t2).
560
561 lemma sem_comp_step_subcase : 
562   ∀alpha,c,elseM,RelseM.
563   Realize ? elseM RelseM → 
564   Realize ? (comp_step_subcase alpha c elseM) 
565     (R_comp_step_subcase alpha c RelseM).
566 #alpha #c #elseM #RelseM #Helse #intape
567 cases (sem_if ? (test_char ? (λx.x == c)) … tc_true 
568         (sem_test_char ? (λx.x == c)) 
569         (sem_seq ????? (sem_move_r …)
570           (sem_seq ????? (sem_adv_to_mark_r ? (is_marked alpha))
571              (sem_match_and_adv ? (λx.x == c)))) Helse intape)
572 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc)
573 % [ @Hloop ] -Hloop cases HR -HR
574 [ * #ta * whd in ⊢ (%→?); #Hta * #tb * whd in ⊢ (%→?); #Htb
575   * #tc * whd in ⊢ (%→?); #Htc whd in ⊢ (%→?); #Houtc
576   #l0 #x #rs #Hintape cases (true_or_false (〈x,true〉==c)) #Hc
577   [ % % [ @(\P Hc) ] 
578     #a #l1 #x0 #a0 #l2 #Hl1 #Hrs >Hrs in Hintape; #Hintape
579     >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta
580     #Hx #Hta lapply (Htb … Hta) -Htb #Htb
581     cases (Htc … Htb) [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
582     -Htc * #_ #Htc lapply (Htc l1 〈x0,true〉 (〈a0,false〉::l2) (refl ??) (refl ??) Hl1)
583     -Htc #Htc cases (Houtc ???????? Htc) -Houtc
584     [ * #Hx0 #Houtc % 
585       % [ <(\P Hx0) in Hx; #Hx lapply (\P Hx) #Hx' destruct (Hx') %
586         | >Houtc >reverse_reverse % ]
587     | * #Hx0 #Houtc %2
588       % [ <(\P Hx) in Hx0; #Hx0 lapply (\Pf Hx0) @not_to_not #Hx' >Hx' %
589         | >Houtc % ]
590     | #x #membx @Hl1 <(reverse_reverse …l1) @memb_reverse @membx ]
591   | %2 % [ @(\Pf Hc) ]
592     >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hx #Hta
593     >Hx in Hc;#Hc destruct (Hc) ]
594 | * #ta * whd in ⊢ (%→?); #Hta #Helse #ls #c0 #rs #Hintape %2
595   >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hc #Hta %
596   [ @(\Pf Hc) | <Hta @Helse ]
597 ]
598 qed.
599
600 (* 
601 - se marcato, itero
602 - se non è marcato
603   + se è un bit, ho fallito il confronto della tupla corrente
604   + se è un separatore, la tupla fa match
605
606
607 ifTM ? (test_char ? is_marked)
608   (single_finalTM … (comp_step_subcase unialpha 〈bit false,true〉
609     (comp_step_subcase unialpha 〈bit true,true〉
610       (clear_mark …))))
611   (nop ?)
612 *)
613
614 definition comp_step ≝ 
615   ifTM ? (test_char ? (is_marked ?))
616   (single_finalTM … (comp_step_subcase FSUnialpha 〈bit false,true〉
617     (comp_step_subcase FSUnialpha 〈bit true,true〉
618       (comp_step_subcase FSUnialpha 〈null,true〉
619         (clear_mark …)))))
620   (nop ?)
621   tc_true.
622   
623 definition R_comp_step_true ≝ 
624   λt1,t2.
625     ∀l0,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) l0 c rs → 
626     ∃c'. c = 〈c',true〉 ∧
627     ((bit_or_null c' = true ∧
628      ∀a,l1,c0,a0,l2.
629       rs = 〈a,false〉::l1@〈c0,true〉::〈a0,false〉::l2 → 
630       (∀c.memb ? c l1 = true → is_marked ? c = false) → 
631       (c0 = c' ∧
632        t2 = midtape ? (〈c',false〉::l0) 〈a,true〉 (l1@〈c0,false〉::〈a0,true〉::l2)) ∨
633       (c0 ≠ c' ∧
634        t2 = midtape (FinProd … FSUnialpha FinBool) 
635         (reverse ? l1@〈a,false〉::〈c',true〉::l0) 〈c0,false〉 (〈a0,false〉::l2))) ∨
636      (bit_or_null c' = false ∧ t2 = midtape ? l0 〈c',false〉 rs)).
637
638 definition R_comp_step_false ≝ 
639   λt1,t2.
640    ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs → 
641    is_marked ? c = false ∧ t2 = t1.
642    
643 lemma sem_comp_step : 
644   accRealize ? comp_step (inr … (inl … (inr … start_nop))) 
645     R_comp_step_true R_comp_step_false.
646 #intape
647 cases (acc_sem_if … (sem_test_char ? (is_marked ?))
648         (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
649           (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ?? 
650             (sem_comp_step_subcase FSUnialpha 〈null,true〉 ?? 
651               (sem_clear_mark …))))
652         (sem_nop …) intape)
653 #k * #outc * * #Hloop #H1 #H2
654 @(ex_intro ?? k) @(ex_intro ?? outc) %
655 [ % [@Hloop ] ] -Hloop
656 [ #Hstate lapply (H1 Hstate) -H1 -Hstate -H2 *
657   #ta * whd in ⊢ (%→?); #Hleft #Hright #ls #c #rs #Hintape
658   >Hintape in Hleft; #Hleft cases (Hleft ? (refl ??)) -Hleft
659   cases c in Hintape; #c' #b #Hintape whd in ⊢ (??%?→?); 
660   #Hb >Hb #Hta @(ex_intro ?? c') % //
661   cases (Hright … Hta)
662   [ * #Hc' #H1 % % [destruct (Hc') % ]
663     #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
664     cases (H1 … Hl1 Hrs)
665     [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
666     | * #Hneq #Houtc %2 %
667       [ @sym_not_eq //
668       | @Houtc ]
669     ]
670   | * #Hc #Helse1 cases (Helse1 … Hta)
671     [ * #Hc' #H1 % % [destruct (Hc') % ]
672       #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
673       cases (H1 … Hl1 Hrs)
674       [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
675       | * #Hneq #Houtc %2 %
676         [ @sym_not_eq //
677         | @Houtc ]
678       ]
679     | * #Hc' #Helse2 cases (Helse2 … Hta)
680       [ * #Hc'' #H1 % % [destruct (Hc'') % ]
681         #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
682         cases (H1 … Hl1 Hrs)
683         [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
684         | * #Hneq #Houtc %2 %
685           [ @sym_not_eq //
686           | @Houtc ]
687         ]
688       | * #Hc'' whd in ⊢ (%→?); #Helse3 %2 %
689         [ generalize in match Hc''; generalize in match Hc'; generalize in match Hc;
690           cases c'
691           [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
692               | #Hfalse @False_ind @(absurd ?? Hfalse) % ]
693           | #_ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
694           |*: #_ #_ #_ % ]
695         | @(Helse3 … Hta)
696         ]
697       ]
698     ]
699   ]
700 | #Hstate lapply (H2 Hstate) -H1 -Hstate -H2 *
701   #ta * whd in ⊢ (%→%→?); #Hleft #Hright #ls #c #rs #Hintape
702   >Hintape in Hleft; #Hleft
703   cases (Hleft ? (refl ??)) -Hleft
704   #Hc #Hta % // >Hright //
705 ]
706 qed.
707
708 definition compare ≝ 
709   whileTM ? comp_step (inr … (inl … (inr … start_nop))).
710
711 (*
712 definition R_compare :=
713   λt1,t2.
714   (t
715   
716   ∀ls,c,b,rs.t1 = midtape ? ls 〈c,b〉 rs →
717   (b = true → rs = ....) → 
718   (b = false ∧ ....) ∨
719   (b = true ∧ 
720    
721    rs = cs@l1@〈c0,true〉::cs0@l2
722    (
723  
724   
725   ls 〈c,b〉 cs l1 〈c0,b0〉 cs0 l2
726   
727
728 ACCETTAZIONE:  
729   ls (hd (Ls@〈grid,false〉))* (tail (Ls@〈grid,false〉)) l1 (hd (Ls@〈comma,false〉))* (tail (Ls@〈comma,false〉)) l2
730      ^^^^^^^^^^^^^^^^^^^^^^^
731   
732   ls Ls 〈grid,false〉 l1 Ls 〈comma,true〉 l2
733         ^^^^^^^^^^^^
734
735 RIFIUTO: c ≠ d
736   
737   ls (hd (Ls@〈c,false〉))* (tail (Ls@〈c,false〉)) l1 (hd (Ls@〈d,false〉))* (tail (Ls@〈d,false〉)) l2
738      ^^^^^^^^^^^^^^^^^^^^^^^
739   
740   
741   ls Ls 〈c,true〉 l1 Ls 〈d,false〉 l2
742                        ^^^^^^^^
743   
744   ).
745   
746   |bs| = |b0s| → 
747   (∃la,d.〈b,true〉::bs = la@[〈grid,d〉] ∧ ∀x.memb ? x la → is_bit (\fst x) = true) → 
748   (∃lb,d0.〈b0,true〉::b0s = lb@[〈comma,d0〉] ∧ ∀x.memb ? x lb → is_bit (\fst x) = true) → 
749   t1 = midtape ? l0 〈b,true〉 (bs@l1@〈b0,true〉::b0s@l2 → 
750   
751   mk_tape left (option current) right
752   
753   (b = grid ∧ b0 = comma ∧ bs = [] ∧ b0s = [] ∧
754    t2 = midtape ? l0 〈grid,false〉 (l1@〈comma,true〉::l2)) ∨
755   (b = bit x ∧ b = c ∧ bs = b0s
756   *)
757 definition R_compare :=
758   λt1,t2.
759   ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs → 
760   (∀c'.bit_or_null c' = false → c = 〈c',true〉 → t2 = midtape ? ls 〈c',false〉 rs) ∧
761   (∀c'. c = 〈c',false〉 → t2 = t1) ∧
762   ∀b,b0,bs,b0s,l1,l2.
763   |bs| = |b0s| → 
764   (∀c.memb (FinProd … FSUnialpha FinBool) c bs = true → bit_or_null (\fst c) = true) → 
765   (∀c.memb (FinProd … FSUnialpha FinBool) c b0s = true → bit_or_null (\fst c) = true) → 
766   (∀c.memb ? c bs = true → is_marked ? c = false) → 
767   (∀c.memb ? c b0s = true → is_marked ? c = false) → 
768   (∀c.memb ? c l1 = true → is_marked ? c = false) → 
769   c = 〈b,true〉 → bit_or_null b = true → 
770   rs = bs@〈grid,false〉::l1@〈b0,true〉::b0s@〈comma,false〉::l2 → 
771   (〈b,true〉::bs = 〈b0,true〉::b0s ∧
772    t2 = midtape ? (reverse ? bs@〈b,false〉::ls)
773           〈grid,false〉 (l1@〈b0,false〉::b0s@〈comma,true〉::l2)) ∨
774   (∃la,c',d',lb,lc.c' ≠ d' ∧
775     〈b,false〉::bs = la@〈c',false〉::lb ∧
776     〈b0,false〉::b0s = la@〈d',false〉::lc ∧
777     t2 = midtape (FinProd … FSUnialpha FinBool) (reverse ? la@
778                     reverse ? l1@
779                     〈grid,false〉::
780                     reverse ? lb@
781                     〈c',true〉::
782                     reverse ? la@ls)
783                     〈d',false〉 (lc@〈comma,false〉::l2)).
784                     
785 lemma wsem_compare : WRealize ? compare R_compare.
786 #t #i #outc #Hloop
787 lapply (sem_while ?????? sem_comp_step t i outc Hloop) [%]
788 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
789 [ #tapea whd in ⊢ (%→?); #Rfalse #ls #c #rs #Htapea %
790   [ %
791     [ #c' #Hc' #Hc lapply (Rfalse … Htapea) -Rfalse * >Hc
792       whd in ⊢ (??%?→?); #Hfalse destruct (Hfalse)
793     | #c' #Hc lapply (Rfalse … Htapea) -Rfalse * #_
794       #Htrue @Htrue ]
795   | #b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1 #Hc
796     cases (Rfalse … Htapea) -Rfalse >Hc whd in ⊢ (??%?→?);#Hfalse destruct (Hfalse)
797   ]
798 | #tapea #tapeb #tapec #Hleft #Hright #IH #Htapec lapply (IH Htapec) -Htapec -IH #IH
799   whd in Hleft; #ls #c #rs #Htapea cases (Hleft … Htapea) -Hleft
800   #c' * #Hc >Hc cases (true_or_false (bit_or_null c')) #Hc'
801   [2: * 
802     [ * >Hc' #H @False_ind destruct (H)
803     | * #_ #Htapeb cases (IH … Htapeb) * #_ #H #_ %
804       [% 
805         [#c1 #Hc1 #Heqc destruct (Heqc) <Htapeb @(H c1) %
806         |#c1 #Hfalse destruct (Hfalse)
807         ]
808       |#b #b0 #bs #b0s #l1 #l2 #_ #_ #_ #_ #_ #_
809        #Heq destruct (Heq) >Hc' #Hfalse @False_ind destruct (Hfalse)
810       ]
811     ]
812  |#Hleft %
813     [ %
814       [ #c'' #Hc'' #Heq destruct (Heq) >Hc'' in Hc'; #H destruct (H) 
815       | #c0 #Hfalse destruct (Hfalse)
816       ]
817     |#b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1
818      #Heq destruct (Heq) #_ #Hrs cases Hleft -Hleft
819       [2: * >Hc' #Hfalse @False_ind destruct ] * #_
820        @(list_cases2 … Hlen)
821        [ #Hbs #Hb0s generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
822        -Hrs #Hrs normalize in Hrs; #Hleft cases (Hleft ????? Hrs ?) -Hleft
823          [ * #Heqb #Htapeb cases (IH … Htapeb) -IH * #IH #_ #_
824           % %
825             [ >Heqb >Hbs >Hb0s %
826             | >Hbs >Hb0s @IH %
827             ] 
828          |* #Hneqb #Htapeb %2
829           @(ex_intro … [ ]) @(ex_intro … b)
830           @(ex_intro … b0) @(ex_intro … [ ]) 
831           @(ex_intro … [ ]) %
832             [ % [ % [@sym_not_eq //| >Hbs %] | >Hb0s %]
833             | cases (IH … Htapeb) -IH * #_ #IH #_ >(IH ? (refl ??))
834               @Htapeb
835             ]
836          | @Hl1 ]
837       | * #b' #bitb' * #b0' #bitb0' #bs' #b0s' #Hbs #Hb0s 
838         generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
839         cut (bit_or_null b' = true ∧ bit_or_null b0' = true ∧ 
840              bitb' = false ∧ bitb0' = false)
841         [ % [ % [ % [ >Hbs in Hbs1; #Hbs1 @(Hbs1 〈b',bitb'〉) @memb_hd
842             | >Hb0s in Hb0s1; #Hb0s1 @(Hb0s1 〈b0',bitb0'〉) @memb_hd ]
843             | >Hbs in Hbs2; #Hbs2 @(Hbs2 〈b',bitb'〉) @memb_hd ]
844             | >Hb0s in Hb0s2; #Hb0s2 @(Hb0s2 〈b0',bitb0'〉) @memb_hd ]
845         | * * * #Ha #Hb #Hc #Hd >Hc >Hd
846           #Hrs #Hleft 
847           cases (Hleft b' (bs'@〈grid,false〉::l1) b0 b0' 
848                          (b0s'@〈comma,false〉::l2) ??) -Hleft
849           [ 3: >Hrs normalize @eq_f >associative_append %
850           | * #Hb0 #Htapeb cases (IH …Htapeb) -IH * #_ #_ #IH
851             cases (IH b' b0' bs' b0s' (l1@[〈b0,false〉]) l2 ??????? Ha ?) -IH
852             [ * #Heq #Houtc % %
853               [ >Hb0 @eq_f >Hbs in Heq; >Hb0s in ⊢ (%→?); #Heq
854                 destruct (Heq) >Hb0s >Hc >Hd %
855               | >Houtc >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append
856                 >associative_append %
857               ]
858             | * #la * #c' * #d' * #lb * #lc * * * #H1 #H2 #H3 #H4 %2
859               @(ex_intro … (〈b,false〉::la)) @(ex_intro … c') @(ex_intro … d')
860               @(ex_intro … lb) @(ex_intro … lc)
861               % [ % [ % // >Hbs >Hc >H2 % | >Hb0s >Hd >H3 >Hb0 % ] 
862                 | >H4 >Hbs >Hb0s >Hc >Hd >Hb0 >reverse_append
863                   >reverse_cons >reverse_cons
864                   >associative_append >associative_append
865                   >associative_append >associative_append %
866                 ]
867             | generalize in match Hlen; >Hbs >Hb0s
868               normalize #Hlen destruct (Hlen) @e0
869             | #c0 #Hc0 @Hbs1 >Hbs @memb_cons // 
870             | #c0 #Hc0 @Hb0s1 >Hb0s @memb_cons // 
871             | #c0 #Hc0 @Hbs2 >Hbs @memb_cons // 
872             | #c0 #Hc0 @Hb0s2 >Hb0s @memb_cons // 
873             | #c0 #Hc0 cases (memb_append … Hc0) 
874               [ @Hl1 | #Hc0' >(memb_single … Hc0') % ]
875             | %
876             | >associative_append >associative_append % ]
877          | * #Hneq #Htapeb %2
878             @(ex_intro … []) @(ex_intro … b) @(ex_intro … b0)
879             @(ex_intro … bs) @(ex_intro … b0s) %
880            [ % // % // @sym_not_eq // 
881            | >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append
882              >reverse_append in Htapeb; >reverse_cons
883              >associative_append >associative_append
884              #Htapeb <Htapeb
885              cases (IH … Htapeb) -Htapeb -IH * #_ #IH #_ @(IH ? (refl ??))
886            ]
887          | #c1 #Hc1 cases (memb_append … Hc1) #Hyp
888            [ @Hbs2 >Hbs @memb_cons @Hyp
889            | cases (orb_true_l … Hyp)
890              [ #Hyp2 >(\P Hyp2) %
891              | @Hl1
892              ]
893            ]
894          ]
895 ]]]]]
896 qed.       
897
898 axiom sem_compare : Realize ? compare R_compare.