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_____________________________________________________________*)
12 include "turing/move_char.ma".
13 include "turing/universal/marks.ma".
14 include "turing/universal/tuples.ma".
16 definition init_cell_states ≝ initN 2.
18 definition ics0 : init_cell_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
19 definition ics1 : init_cell_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
21 definition init_cell ≝
22 mk_TM STape init_cell_states
26 [ None ⇒ 〈ics1, Some ? 〈〈null,false〉,N〉〉
27 | Some _ ⇒ 〈ics1, None ?〉 ]
28 | S _ ⇒ 〈ics1,None ?〉 ])
31 definition R_init_cell ≝ λt1,t2.
32 (∃c.current STape t1 = Some ? c ∧ t2 = t1) ∨
33 (current STape t1 = None ? ∧ t2 = midtape ? (left ? t1) 〈null,false〉 (right ? t1)).
35 axiom sem_init_cell : Realize ? init_cell R_init_cell.
40 ls # current c # table # d? rs
42 ls # current c # table # d? rs init
44 ls # current c # table # d? rs
46 ls # current c # table # d rs ----------------------
48 ls # current c # table # d rs
50 ls # current c # table d # rs --------------------
52 ls # current c # table d # rs
54 ls # current c # d table # rs sub1
56 ls # current c # d table # rs
58 ls # current c d # table # rs -------------------
60 ls # current c d # table # rs -------------------
62 ls # current c d # table # rs
64 ls # c current d # table # rs sub1
66 ls # c current d # table # rs
68 ls c # current d # table # rs ------------------
90 (* l1 # l2 r ---> l1 r # l2
94 seq ? (move_l …) (seq ? (move_char_l STape 〈grid,false〉)
95 (swap STape 〈grid,false〉)).
96 definition R_mtr_aux ≝ λt1,t2.
97 ∀l1,l2,l3,r. t1 = midtape STape (l2@〈grid,false〉::l1) r l3 → no_grids l2 →
98 t2 = midtape STape l1 r (〈grid,false〉::reverse ? l2@l3).
100 lemma sem_mtr_aux : Realize ? mtr_aux R_mtr_aux.
102 cases (sem_seq … (sem_move_l …) (sem_seq … (ssem_move_char_l STape 〈grid,false〉)
103 (sem_swap STape 〈grid,false〉)) intape)
104 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
105 #l1 #l2 #l3 #r #Hintape #Hl2
106 cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta #Hta
107 * #tb * whd in ⊢(%→?); generalize in match Hta; -Hta cases l2 in Hl2;
108 [ #_ #Hta #Htb lapply (Htb … Hta) -Htb * #Htb lapply (Htb (refl ??)) -Htb #Htb #_
109 whd in ⊢(%→?); >Htb #Houtc lapply (Houtc … Hta) -Houtc #Houtc @Houtc
110 | #c0 #l0 #Hnogrids #Hta #Htb lapply (Htb … Hta) -Htb * #_ #Htb
111 lapply (Htb … (refl ??) ??)
112 [ cases (true_or_false (memb STape 〈grid,false〉 l0)) #Hmemb
113 [ @False_ind lapply (Hnogrids 〈grid,false〉 ?)
114 [ @memb_cons // | normalize #Hfalse destruct (Hfalse) ]
116 | % #Hc0 lapply (Hnogrids c0 ?)
117 [ @memb_hd | >Hc0 normalize #Hfalse destruct (Hfalse) ]
118 | #Htb whd in ⊢(%→?); >Htb #Houtc lapply (Houtc … (refl ??)) -Houtc #Houtc
119 >reverse_cons >associative_append @Houtc
123 definition move_tape_r ≝
124 seq ? (move_r …) (seq ? init_cell (seq ? (move_l …)
125 (seq ? (swap STape 〈grid,false〉)
126 (seq ? mtr_aux (seq ? (move_l …) (seq ? mtr_aux (move_r …))))))).
128 definition R_move_tape_r ≝ λt1,t2.
129 ∀rs,n,table,c0,bc0,curconfig,ls0.
130 bit_or_null c0 = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) →
131 t1 = midtape STape (table@〈grid,false〉::〈c0,bc0〉::curconfig@〈grid,false〉::ls0)
134 t2 = midtape STape (〈c0,bc0〉::ls0) 〈grid,false〉 (reverse STape curconfig@〈null,false〉::
135 〈grid,false〉::reverse STape table@[〈grid,false〉])) ∨
136 (∃r0,rs0.rs = r0::rs0 ∧
137 t2 = midtape STape (〈c0,bc0〉::ls0) 〈grid,false〉 (reverse STape curconfig@r0::
138 〈grid,false〉::reverse STape table@〈grid,false〉::rs0)).
140 lemma sem_move_tape_r : Realize ? move_tape_r R_move_tape_r.
142 cases (sem_seq …(sem_move_r …) (sem_seq … sem_init_cell (sem_seq … (sem_move_l …)
143 (sem_seq … (sem_swap STape 〈grid,false〉) (sem_seq … sem_mtr_aux
144 (sem_seq … (sem_move_l …) (sem_seq … sem_mtr_aux (sem_move_r …))))))) tapein)
145 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
146 #rs #n #table #c0 #bc0 #curconfig #ls0 #Hbitnullc0 #Hbitnullcc #Htable #Htapein
147 cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Htapein) -Hta #Hta
148 * #tb * whd in ⊢ (%→?); *
150 generalize in match Hta; generalize in match Htapein; -Htapein -Hta cases rs
151 [ #_ #Hta >Hta normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
152 #r1 #rs1 #Htapein #Hta change with (midtape ?? r1 rs1) in Hta:(???%); >Hta
153 #Hr0 whd in Hr0:(??%?); #Htb * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc #Htc
154 * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd #Htd
155 * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?) [ (*memb_reverse @(no_grids_in_table … Htable)*) @daemon ] -Hte #Hte
156 * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf #Htf
157 * #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?) [ #x #Hx @bit_or_null_not_grid @Hbitnullcc // ] -Htg #Htg
158 whd in ⊢ (%→?); #Houtc lapply (Houtc … Htg) -Houtc #Houtc
159 %2 @(ex_intro ?? r1) @(ex_intro ?? rs1) % [%] @Houtc
160 | * generalize in match Hta; generalize in match Htapein; -Htapein -Hta cases rs
161 [|#r1 #rs1 #_ #Hta >Hta normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
162 #Htapein #Hta change with (rightof ???) in Hta:(???%); >Hta
163 #Hr0 whd in Hr0:(??%?); #Htb * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc #Htc
164 * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd #Htd
165 * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?) [(*same as above @(no_grids_in_table … Htable) *) @daemon ] -Hte #Hte
166 * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf #Htf
167 * #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?) [ #x #Hx @bit_or_null_not_grid @Hbitnullcc // ] -Htg #Htg
168 whd in ⊢ (%→?); #Houtc lapply (Houtc … Htg) -Houtc #Houtc
175 ls d? # current c # table # rs
176 ^ move_l; adv_to_mark_l
177 ls d? # current c # table # rs
178 ^ move_l; adv_to_mark_l
179 ls d? # current c # table # rs
181 ls d? # current c # table # rs
183 ls d # current c # table # rs
185 ls # current c d # table # rs
187 ls # current d c # table # rs
189 ls # current d # table c # rs
191 ls # current d # table # c rs
192 ^ move_l; adv_to_mark_l
193 ls # current d # table # c rs
194 ^ move_l; adv_to_mark_l
195 ls # current d # table # c rs
199 seq ? (swap STape 〈grid,false〉)
200 (seq ? (move_r …) (seq ? (move_r …) (seq ? (move_char_r STape 〈grid,false〉) (move_l …)))).
201 definition R_mtl_aux ≝ λt1,t2.
202 ∀l1,l2,l3,r. t1 = midtape STape l1 r (〈grid,false〉::l2@〈grid,false〉::l3) → no_grids l2 →
203 t2 = midtape STape (reverse ? l2@〈grid,false〉::l1) r (〈grid,false〉::l3).
205 lemma sem_mtl_aux : Realize ? mtl_aux R_mtl_aux.
207 cases (sem_seq … (sem_swap STape 〈grid,false〉) (sem_seq … (sem_move_r …)
208 (sem_seq … (sem_move_r …) (sem_seq … (ssem_move_char_r STape 〈grid,false〉)
209 (sem_move_l …)))) intape)
210 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
211 #l1 #l2 #l3 #r #Hintape #Hl2
212 cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta #Hta
213 * #tb * whd in ⊢(%→?); #Htb lapply (Htb … Hta) -Htb -Hta whd in ⊢ (???%→?); #Htb
214 * #tc * whd in ⊢(%→?); #Htc lapply (Htc … Htb) -Htc -Htb cases l2 in Hl2;
215 [ #_ #Htc * #td * whd in ⊢(%→?); #Htd lapply (Htd … Htc) -Htd >Htc -Htc * #Htd #_
216 whd in ⊢ (%→?); #Houtc lapply (Htd (refl ??)) -Htd @Houtc
217 | #c0 #l0 #Hnogrids #Htc *
218 #td * whd in ⊢(%→?); #Htd lapply (Htd … Htc) -Htd -Htc * #_ #Htd
219 lapply (Htd … (refl ??) ??)
220 [ cases (true_or_false (memb STape 〈grid,false〉 l0)) #Hmemb
221 [ @False_ind lapply (Hnogrids 〈grid,false〉 ?)
222 [ @memb_cons // | normalize #Hfalse destruct (Hfalse) ]
224 | % #Hc0 lapply (Hnogrids c0 ?)
225 [ @memb_hd | >Hc0 normalize #Hfalse destruct (Hfalse) ]
226 | #Htd whd in ⊢(%→?); >Htd #Houtc lapply (Houtc … (refl ??)) -Houtc #Houtc
227 >reverse_cons >associative_append @Houtc
231 definition R_ml_atml ≝ λt1,t2.
232 ∀ls1,ls2,rs.no_grids ls1 →
233 t1 = midtape STape (ls1@〈grid,false〉::ls2) 〈grid,false〉 rs →
234 t2 = midtape STape ls2 〈grid,false〉 (reverse ? ls1@〈grid,false〉::rs).
237 Realize ? ((move_l …) · (adv_to_mark_l … (λc:STape.is_grid (\fst c)))) R_ml_atml.
239 cases (sem_seq … (sem_move_l …) (sem_adv_to_mark_l … (λc:STape.is_grid (\fst c))) intape)
240 #k * #outc * #Hloop #HR %{k} %{outc} % [@Hloop] -Hloop
241 #ls1 #ls2 #rs #Hnogrids #Hintape cases HR -HR
242 #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta
243 cases ls1 in Hnogrids;
244 [ #_ #Hta whd in ⊢ (%→?); #Houtc cases (Houtc … Hta) -Houtc
245 [ * #_ >Hta #Houtc @Houtc
246 | * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
247 | #c0 #l0 #Hnogrids #Hta whd in ⊢ (%→?); #Houtc cases (Houtc … Hta) -Houtc
248 [ * #Hc0 lapply (Hnogrids c0 (memb_hd …)) >Hc0 #Hfalse destruct (Hfalse)
249 | * #_ #Htb >reverse_cons >associative_append @Htb //
250 #x #Hx @Hnogrids @memb_cons //
255 definition move_tape_l : TM STape ≝
256 seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c))))
257 (seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c))))
261 (seq ? (swap_r STape 〈grid,false〉)
263 (seq ? (swap STape 〈grid,false〉)
264 (seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c))))
265 (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c)))))))))))).
267 (* seq ? (move_r …) (seq ? init_cell (seq ? (move_l …)
268 (seq ? (swap STape 〈grid,false〉)
269 (seq ? mtr_aux (seq ? (move_l …) mtr_aux))))). *)
271 definition R_move_tape_l ≝ λt1,t2.
272 ∀rs,n,table,c0,bc0,curconfig,ls0.
273 bit_or_null c0 = true → only_bits_or_nulls curconfig →
274 table_TM n (reverse ? table) → only_bits ls0 →
275 t1 = midtape STape (table@〈grid,false〉::〈c0,bc0〉::curconfig@〈grid,false〉::ls0)
278 t2 = midtape STape [] 〈grid,false〉
279 (reverse ? curconfig@〈null,false〉::〈grid,false〉::reverse ? table@〈grid,false〉::〈c0,bc0〉::rs)) ∨
280 (∃l1,ls1. ls0 = l1::ls1 ∧
281 t2 = midtape STape ls1 〈grid,false〉
282 (reverse ? curconfig@l1::〈grid,false〉::reverse ? table@〈grid,false〉::〈c0,bc0〉::rs)).
284 lemma sem_move_tape_l : Realize ? move_tape_l R_move_tape_l.
286 cases (sem_seq … sem_ml_atml
287 (sem_seq … sem_ml_atml
288 (sem_seq … (sem_move_l …)
289 (sem_seq … sem_init_cell
290 (sem_seq … sem_mtl_aux
291 (sem_seq … (sem_swap_r STape 〈grid,false〉)
292 (sem_seq … sem_mtl_aux
293 (sem_seq … (sem_swap STape 〈grid,false〉)
294 (sem_seq … sem_ml_atml sem_ml_atml)))))))) tapein)
295 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
296 #rs #n #table #c0 #bc0 #curconfig #ls0 #Hbitnullc0 #Hbitnullcc #Htable #Hls0 #Htapein
297 cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Htapein)
298 [ @daemon (* by no_grids_in_table, manca un lemma sulla reverse *) ]
299 -Hta #Hta * #tb * whd in ⊢ (%→?); #Htb lapply (Htb (〈c0,bc0〉::curconfig) … Hta)
300 [ @daemon ] -Hta -Htb #Htb
301 * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htb -Htc #Htc
302 * #td * whd in ⊢ (%→?); *
303 [ * #c1 * generalize in match Htc; generalize in match Htapein; -Htapein -Htc
305 [ #_ #_ #Htc >Htc normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
306 #l1 #ls1 #Hls0 #Htapein #Htc change with (midtape ? ls1 l1 ?) in Htc:(???%); >Htc
307 #Hl1 whd in Hl1:(??%?); #Htd
308 * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?)
309 [ (* memb_reverse *) @daemon ] -Hte -Htd >reverse_reverse #Hte
310 * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf -Hte #Htf
311 * #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?)
312 [ @(no_grids_in_table … Htable) ] -Htg -Htf >reverse_reverse #Htg
313 * #th * whd in ⊢ (%→?); #Hth lapply (Hth … Htg) -Hth -Htg #Hth
314 * #ti * whd in ⊢ (%→?); #Hti lapply (Hti … Hth)
315 [ (* memb_reverse *) @daemon ] -Hti -Hth #Hti
316 whd in ⊢ (%→?); #Houtc lapply (Houtc (l1::curconfig) … Hti)
317 [ #x #Hx cases (orb_true_l … Hx) -Hx #Hx
318 [ >(\P Hx) lapply (Hls0 l1 (memb_hd …)) @bit_not_grid
319 | lapply (Hbitnullcc ? Hx) @bit_or_null_not_grid ] ]
320 -Houtc >reverse_cons >associative_append #Houtc %2 %{l1} %{ls1} % [%] @Houtc
321 | * generalize in match Htc; generalize in match Htapein; -Htapein -Htc
323 [| #l1 #ls1 #_ #Htc >Htc normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
324 #Htapein #Htc change with (leftof ???) in Htc:(???%); >Htc #_ #Htd
325 * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?)
326 [ (*memb_reverse*) @daemon ] -Hte -Htd >reverse_reverse #Hte
327 * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf -Hte #Htf
328 * #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?)
329 [ @(no_grids_in_table … Htable) ] -Htg -Htf >reverse_reverse #Htg
330 * #th * whd in ⊢ (%→?); #Hth lapply (Hth … Htg) -Hth -Htg #Hth
331 * #ti * whd in ⊢ (%→?); #Hti lapply (Hti … Hth)
332 [ (*memb_reverse*) @daemon ] -Hti -Hth #Hti
333 whd in ⊢ (%→?); #Houtc lapply (Houtc (〈null,false〉::curconfig) … Hti)
334 [ #x #Hx cases (orb_true_l … Hx) -Hx #Hx
336 | lapply (Hbitnullcc ? Hx) @bit_or_null_not_grid ] ]
337 -Houtc >reverse_cons >associative_append
338 >reverse_cons >associative_append #Houtc % % [%] @Houtc
342 (*definition mtl_aux ≝
343 seq ? (move_r …) (seq ? (move_char_r STape 〈grid,false〉) (move_l …)).
344 definition R_mtl_aux ≝ λt1,t2.
345 ∀l1,l2,l3,r. t1 = midtape STape l1 r (l2@〈grid,false〉::l3) → no_grids l2 →
346 t2 = midtape STape (reverse ? l2@l1) r (〈grid,false〉::l3).
348 lemma sem_mtl_aux : Realize ? mtl_aux R_mtl_aux.
350 cases (sem_seq … (sem_move_r …) (sem_seq … (ssem_move_char_r STape 〈grid,false〉) (sem_move_l …)) intape)
351 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
352 #l1 #l2 #l3 #r #Hintape #Hl2
353 cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta #Hta
354 * #tb * whd in ⊢(%→?); generalize in match Hta; -Hta cases l2 in Hl2;
355 [ #_ #Hta #Htb lapply (Htb … Hta) -Htb * #Htb #_ whd in ⊢ (%→?); #Houtc
356 lapply (Htb (refl ??)) -Htb >Hta @Houtc
357 | #c0 #l0 #Hnogrids #Hta #Htb lapply (Htb … Hta) -Htb * #_ #Htb
358 lapply (Htb … (refl ??) ??)
359 [ cases (true_or_false (memb STape 〈grid,false〉 l0)) #Hmemb
360 [ @False_ind lapply (Hnogrids 〈grid,false〉 ?)
361 [ @memb_cons // | normalize #Hfalse destruct (Hfalse) ]
363 | % #Hc0 lapply (Hnogrids c0 ?)
364 [ @memb_hd | >Hc0 normalize #Hfalse destruct (Hfalse) ]
365 | #Htb whd in ⊢(%→?); >Htb #Houtc lapply (Houtc … (refl ??)) -Houtc #Houtc
366 >reverse_cons >associative_append @Houtc
375 case bit false: move_tape_l
376 case bit true: move_tape_r
377 case null: adv_to_grid_l; move_l; adv_to_grid_l;
380 definition lift_tape ≝ λls,c,rs.
382 let c' ≝ match c0 with
386 mk_tape STape ls c' rs.
388 definition sim_current_of_tape ≝ λt.
389 match current STape t with
390 [ None ⇒ 〈null,false〉
394 definition move_of_unialpha ≝
396 [ bit x ⇒ match x with [ true ⇒ R | false ⇒ L ]
399 definition R_uni_step ≝ λt1,t2.
400 ∀n,table,c,c1,ls,rs,curs,curc,news,newc,mv.
402 match_in_table n (〈c,false〉::curs) 〈curc,false〉
403 (〈c1,false〉::news) 〈newc,false〉 〈mv,false〉 table →
404 t1 = midtape STape (〈grid,false〉::ls) 〈c,false〉
405 (curs@〈curc,false〉::〈grid,false〉::table@〈grid,false〉::rs) →
406 ∀t1',ls1,rs1.t1' = lift_tape ls 〈curc,false〉 rs →
407 (t2 = midtape STape (〈grid,false〉::ls1) 〈c1,false〉
408 (news@〈newc,false〉::〈grid,false〉::table@〈grid,false〉::rs1) ∧
409 lift_tape ls1 〈newc,false〉 rs1 =
410 tape_move STape t1' (Some ? 〈〈newc,false〉,move_of_unialpha mv〉)).
412 definition no_nulls ≝
413 λl:list STape.∀x.memb ? x l = true → is_null (\fst x) = false.
415 definition current_of_alpha ≝ λc:STape.
416 match \fst c with [ null ⇒ None ? | _ ⇒ Some ? c ].
424 definition legal_tape ≝ λls,c,rs.
425 no_marks (c::ls@rs) ∧ only_bits (ls@rs) ∧ bit_or_null (\fst c) = true ∧
426 (\fst c ≠ null ∨ ls = [] ∨ rs = []).
428 lemma legal_tape_left :
429 ∀ls,c,rs.legal_tape ls c rs →
430 left ? (mk_tape STape ls (current_of_alpha c) rs) = ls.
431 #ls * #c #bc #rs * * * #_ #_ #_ *
435 | * #Hfalse @False_ind /2/
437 | #Hls >Hls cases c // cases rs //
439 | #Hrs >Hrs cases c // cases ls //
443 axiom legal_tape_current :
444 ∀ls,c,rs.legal_tape ls c rs →
445 current ? (mk_tape STape ls (current_of_alpha c) rs) = current_of_alpha c.
447 axiom legal_tape_right :
448 ∀ls,c,rs.legal_tape ls c rs →
449 right ? (mk_tape STape ls (current_of_alpha c) rs) = rs.
452 lemma legal_tape_cases :
453 ∀ls,c,rs.legal_tape ls c rs →
454 \fst c ≠ null ∨ (\fst c = null ∧ (ls = [] ∨ rs = [])).
455 #ls #c #rs cases c #c0 #bc0 cases c0
456 [ #c1 normalize #_ % % #Hfalse destruct (Hfalse)
461 | #r0 #rs0 normalize * * #_ #Hrs destruct (Hrs) ]
463 |*: #_ % % #Hfalse destruct (Hfalse) ]
466 axiom legal_tape_conditions :
467 ∀ls,c,rs.(\fst c ≠ null ∨ ls = [] ∨ rs = []) → legal_tape ls c rs.
470 [ >(eq_pair_fst_snd ?? c) cases (\fst c)
472 | * #Hfalse @False_ind /2/
475 | cases ls [ * #Hfalse @False_ind /2/ ]
482 definition R_move_tape_r_abstract ≝ λt1,t2.
483 ∀rs,n,table,curc,curconfig,ls.
484 is_bit curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) →
485 t1 = midtape STape (table@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls)
487 legal_tape ls 〈curc,false〉 rs →
488 ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs →
490 (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉::
491 〈grid,false〉::reverse ? table@〈grid,false〉::rs1) ∧
492 lift_tape ls1 〈newc,false〉 rs1 =
493 tape_move_right STape ls 〈curc,false〉 rs ∧ legal_tape ls1 〈newc,false〉 rs1).
495 lemma lift_tape_not_null :
496 ∀ls,c,rs. is_null (\fst c) = false →
497 lift_tape ls c rs = mk_tape STape ls (Some ? c) rs.
498 #ls * #c0 #bc0 #rs cases c0
499 [|normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
503 axiom bit_not_null : ∀d.is_bit d = true → is_null d = false.
505 lemma mtr_concrete_to_abstract :
506 ∀t1,t2.R_move_tape_r t1 t2 → R_move_tape_r_abstract t1 t2.
507 #t1 #t2 whd in ⊢(%→?); #Hconcrete
508 #rs #n #table #curc #curconfig #ls #Hbitcurc #Hcurconfig #Htable #Ht1
509 * * * #Hnomarks #Hbits #Hcurc #Hlegal #t1' #Ht1'
510 cases (Hconcrete … Htable Ht1) //
512 @(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? [])
513 @(ex_intro ?? null) %
518 [ >append_nil #x #Hx cases (orb_true_l … Hx) #Hx'
520 | @Hnomarks @(memb_append_l1 … Hx') ]
521 | >append_nil #x #Hx cases (orb_true_l … Hx) #Hx'
523 | @Hbits @(memb_append_l1 … Hx') ]]
527 | * * #r0 #br0 * #rs0 * #Hrs
529 [ @(Hnomarks 〈r0,br0〉) @memb_cons @memb_append_l2 >Hrs @memb_hd]
530 #Hbr0 >Hbr0 in Hrs; #Hrs #Ht2
531 @(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? rs0)
535 | >Hrs >lift_tape_not_null
537 | @bit_not_null @(Hbits 〈r0,false〉) >Hrs @memb_append_l2 @memb_hd ] ]
539 [ #x #Hx cases (orb_true_l … Hx) #Hx'
541 | cases (memb_append … Hx') #Hx'' @Hnomarks
542 [ @(memb_append_l1 … Hx'')
543 | >Hrs @memb_cons @memb_append_l2 @(memb_cons … Hx'') ]
545 | whd in ⊢ (?%); #x #Hx cases (orb_true_l … Hx) #Hx'
547 | cases (memb_append … Hx') #Hx'' @Hbits
548 [ @(memb_append_l1 … Hx'') | >Hrs @memb_append_l2 @(memb_cons … Hx'') ]
550 | whd in ⊢ (??%?); >(Hbits 〈r0,false〉) //
551 @memb_append_l2 >Hrs @memb_hd ]
552 | % % % #Hr0 lapply (Hbits 〈r0,false〉?)
553 [ @memb_append_l2 >Hrs @memb_hd
554 | >Hr0 normalize #Hfalse destruct (Hfalse)
558 definition R_move_tape_l_abstract ≝ λt1,t2.
559 ∀rs,n,table,curc,curconfig,ls.
560 is_bit curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) →
561 t1 = midtape STape (table@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls)
563 legal_tape ls 〈curc,false〉 rs →
564 ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs →
566 (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉::
567 〈grid,false〉::reverse ? table@〈grid,false〉::rs1) ∧
568 lift_tape ls1 〈newc,false〉 rs1 =
569 tape_move_left STape ls 〈curc,false〉 rs ∧ legal_tape ls1 〈newc,false〉 rs1).
571 lemma mtl_concrete_to_abstract :
572 ∀t1,t2.R_move_tape_l t1 t2 → R_move_tape_l_abstract t1 t2.
573 #t1 #t2 whd in ⊢(%→?); #Hconcrete
574 #rs #n #table #curc #curconfig #ls #Hcurc #Hcurconfig #Htable #Ht1
575 * * * #Hnomarks #Hbits #Hcurc #Hlegal #t1' #Ht1'
576 cases (Hconcrete … Htable ? Ht1) //
579 @(ex_intro ?? (〈curc,false〉::rs))
580 @(ex_intro ?? null) %
585 [ #x #Hx cases (orb_true_l … Hx) #Hx'
587 | @Hnomarks >Hls @Hx' ]
588 | #x #Hx cases (orb_true_l … Hx) #Hx'
590 | @Hbits >Hls @Hx' ]]
594 | * * #l0 #bl0 * #ls0 * #Hls
596 [ @(Hnomarks 〈l0,bl0〉) @memb_cons @memb_append_l1 >Hls @memb_hd]
597 #Hbl0 >Hbl0 in Hls; #Hls #Ht2
598 @(ex_intro ?? ls0) @(ex_intro ?? (〈curc,false〉::rs))
602 | >Hls >lift_tape_not_null
604 | @bit_not_null @(Hbits 〈l0,false〉) >Hls @memb_append_l1 @memb_hd ] ]
606 [ #x #Hx cases (orb_true_l … Hx) #Hx'
608 | cases (memb_append … Hx') #Hx'' @Hnomarks
609 [ >Hls @memb_cons @memb_cons @(memb_append_l1 … Hx'')
610 | cases (orb_true_l … Hx'') #Hx'''
611 [ >(\P Hx''') @memb_hd
612 | @memb_cons @(memb_append_l2 … Hx''')]
615 | whd in ⊢ (?%); #x #Hx cases (memb_append … Hx) #Hx'
616 [ @Hbits >Hls @memb_cons @(memb_append_l1 … Hx')
617 | cases (orb_true_l … Hx') #Hx''
619 | @Hbits @(memb_append_l2 … Hx'')
621 | whd in ⊢ (??%?); >(Hbits 〈l0,false〉) //
622 @memb_append_l1 >Hls @memb_hd ]
623 | % % % #Hl0 lapply (Hbits 〈l0,false〉?)
624 [ @memb_append_l1 >Hls @memb_hd
625 | >Hl0 normalize #Hfalse destruct (Hfalse)
627 | #x #Hx @Hbits @memb_append_l1 @Hx ]
630 lemma sem_move_tape_l_abstract : Realize … move_tape_l R_move_tape_l_abstract.
631 @(Realize_to_Realize … mtl_concrete_to_abstract) //
634 lemma sem_move_tape_r_abstract : Realize … move_tape_r R_move_tape_r_abstract.
635 @(Realize_to_Realize … mtr_concrete_to_abstract) //
639 t1 = ls # cs c # table # rs
641 let simt ≝ lift_tape ls c rs in
642 let simt' ≝ move_left simt' in
644 t2 = left simt'# cs (sim_current_of_tape simt') # table # right simt'
650 definition R_exec_move ≝ λt1,t2.
651 ∀ls,current,table1,newcurrent,table2,rs.
652 t1 = midtape STape (current@〈grid,false〉::ls) 〈grid,false〉
653 (table1@〈comma,true〉::newcurrent@〈comma,false〉::move::table2@
655 table_TM (table1@〈comma,false〉::newcurrent@〈comma,false〉::move::table2) →
663 if is_true(current) (* current state is final *)
668 if is_marked(current) = false (* match ok *)
675 definition move_tape ≝
676 ifTM ? (test_char ? (λc:STape.c == 〈bit false,false〉))
677 (* spostamento a sinistra: verificare se per caso non conviene spostarsi
678 sulla prima grid invece dell'ultima *)
679 (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c))) move_tape_l)
680 (ifTM ? (test_char ? (λc:STape.c == 〈bit true,false〉))
681 (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c))) move_tape_r)
682 (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
683 (seq ? (move_l …) (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))))
686 definition R_move_tape ≝ λt1,t2.
687 ∀rs,n,table1,mv,table2,curc,curconfig,ls.
688 bit_or_null mv = true → only_bits_or_nulls curconfig →
689 (is_bit mv = true → is_bit curc = true) →
690 table_TM n (reverse ? table1@〈mv,false〉::table2) →
691 t1 = midtape STape (table1@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls)
692 〈mv,false〉 (table2@〈grid,false〉::rs) →
693 legal_tape ls 〈curc,false〉 rs →
694 ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs →
696 legal_tape ls1 〈newc,false〉 rs1 ∧
697 (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉::
698 〈grid,false〉::reverse ? table1@〈mv,false〉::table2@〈grid,false〉::rs1) ∧
699 ((mv = bit false ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_left STape ls 〈curc,false〉 rs) ∨
700 (mv = bit true ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_right STape ls 〈curc,false〉 rs) ∨
701 (mv = null ∧ ls1 = ls ∧ rs1 = rs ∧ curc = newc))).
703 lemma sem_move_tape : Realize ? move_tape R_move_tape.
705 cases (sem_if ? (test_char ??) … tc_true (sem_test_char ? (λc:STape.c == 〈bit false,false〉))
706 (sem_seq … (sem_adv_to_mark_r ? (λc:STape.is_grid (\fst c))) sem_move_tape_l_abstract)
707 (sem_if ? (test_char ??) … tc_true (sem_test_char ? (λc:STape.c == 〈bit true,false〉))
708 (sem_seq … (sem_adv_to_mark_r ? (λc:STape.is_grid (\fst c))) sem_move_tape_r_abstract)
709 (sem_seq … (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
710 (sem_seq … (sem_move_l …) (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c)))))) intape)
711 #k * #outc * #Hloop #HR
712 @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
713 #rs #n #table1 #mv #table2 #curc #curconfig #ls
714 #Hmv #Hcurconfig #Hmvcurc #Htable #Hintape #Htape #t1' #Ht1'
715 generalize in match HR; -HR *
716 [ * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈mv,false〉 ?)
717 [| >Hintape % ] -Hta #Hceq #Hta lapply (\P Hceq) -Hceq #Hceq destruct (Hta Hceq)
718 * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hintape) -Htb -Hintape
719 [ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
720 * #_ #Htb lapply (Htb … (refl ??) (refl ??) ?)
721 [ @daemon ] -Htb >append_cons <associative_append #Htb
722 whd in ⊢ (%→?); #Houtc lapply (Houtc … Htb … Ht1') //
723 [ >reverse_append >reverse_append >reverse_reverse @Htable
726 -Houtc -Htb * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal
727 @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) %
730 [ >Houtc >reverse_append >reverse_append >reverse_reverse
731 >associative_append >associative_append %
734 | * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈mv,false〉 ?)
735 [| >Hintape % ] -Hta #Hcneq cut (mv ≠ bit false)
736 [ lapply (\Pf Hcneq) @not_to_not #Heq >Heq % ] -Hcneq #Hcneq #Hta destruct (Hta)
738 [ * #tb * whd in ⊢ (%→?);#Htb cases (Htb 〈mv,false〉 ?)
739 [| >Hintape % ] -Htb #Hceq #Htb lapply (\P Hceq) -Hceq #Hceq destruct (Htb Hceq)
740 * #tc * whd in ⊢ (%→?); #Htc cases (Htc … Hintape) -Htc -Hintape
741 [ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
742 * #_ #Htc lapply (Htc … (refl ??) (refl ??) ?)
743 [ @daemon ] -Htc >append_cons <associative_append #Htc
744 whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc … Ht1') //
745 [ >reverse_append >reverse_append >reverse_reverse @Htable
747 -Houtc -Htc * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal
748 @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) %
751 [ >Houtc >reverse_append >reverse_append >reverse_reverse
752 >associative_append >associative_append %
755 | * #tb * whd in ⊢ (%→?); #Htb cases (Htb 〈mv,false〉 ?)
756 [| >Hintape % ] -Htb #Hcneq' cut (mv ≠ bit true)
757 [ lapply (\Pf Hcneq') @not_to_not #Heq >Heq % ] -Hcneq' #Hcneq' #Htb destruct (Htb)
758 * #tc * whd in ⊢ (%→?); #Htc cases (Htc … Hintape)
759 [ * >(bit_or_null_not_grid … Hmv) #Hfalse destruct (Hfalse) ] -Htc
760 * #_ #Htc lapply (Htc … (refl ??) (refl ??) ?) [@daemon] -Htc #Htc
761 * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd -Htc
762 whd in ⊢ (???%→?); #Htd whd in ⊢ (%→?); #Houtc lapply (Houtc … Htd) -Houtc *
763 [ * cases Htape * * #_ #_ #Hcurc #_
764 >(bit_or_null_not_grid … Hcurc) #Hfalse destruct (Hfalse) ]
765 * #_ #Houtc lapply (Houtc … (refl ??) (refl ??) ?) [@daemon] -Houtc #Houtc
766 @(ex_intro ?? ls) @(ex_intro ?? rs) @(ex_intro ?? curc) %
771 generalize in match Hcneq; generalize in match Hcneq';
772 cases mv in Hmv; normalize //
773 [ * #_ normalize [ #Hfalse @False_ind cases Hfalse /2/ | #_ #Hfalse @False_ind cases Hfalse /2/ ]
774 |*: #Hfalse destruct (Hfalse) ]