]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/turing/universal/move_tape.ma
match termination completed, still a small case ignored in wsem_match
[helm.git] / matita / matita / lib / turing / universal / move_tape.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 include "turing/move_char.ma".
13 include "turing/universal/marks.ma".
14 include "turing/universal/tuples.ma".
15
16 definition init_cell_states ≝ initN 2.
17
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 …)).
20
21 definition init_cell ≝ 
22  mk_TM STape init_cell_states
23  (λp.let 〈q,a〉 ≝ p in
24   match pi1 … q with
25   [ O ⇒ match a with
26     [ None ⇒ 〈ics1, Some ? 〈〈null,false〉,N〉〉
27     | Some _ ⇒ 〈ics1, None ?〉 ]
28   | S _ ⇒ 〈ics1,None ?〉 ])
29  ics0 (λq.q == ics1).
30  
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)).
34  
35 axiom sem_init_cell : Realize ? init_cell R_init_cell.
36
37 (*
38 MOVE TAPE RIGHT:
39
40   ls # current c # table # d? rs
41                      ^
42   ls # current c # table # d? rs init
43                          ^
44   ls # current c # table # d? rs
45                            ^
46   ls # current c # table # d rs ----------------------
47                            ^     move_l
48   ls # current c # table # d rs
49                          ^       swap
50   ls # current c # table d # rs --------------------
51                          ^
52   ls # current c # table d # rs
53                        ^
54   ls # current c # d table # rs  sub1
55                    ^
56   ls # current c # d table # rs
57                  ^
58   ls # current c d # table # rs -------------------
59                  ^               move_l
60   ls # current c d # table # rs -------------------
61                ^
62   ls # current c d # table # rs
63              ^
64   ls # c current d # table # rs  sub1
65        ^
66   ls # c current d # table # rs
67      ^
68   ls c # current d # table # rs ------------------
69      ^
70
71 (move_to_grid_r;)
72 move_r;
73 init_cell;
74 move_l;
75 swap;
76
77 move_l;
78 move_char_l;
79 ---------move_l;
80 swap;
81
82 move_l;
83
84 move_l;
85 move_char_l;
86 ---------move_l;
87 swap
88 *)
89
90 (* l1 # l2 r  ---> l1 r # l2 
91            ^          ^
92  *)
93 definition move_after_left_bar ≝ 
94   move_l … · move_char_l STape 〈grid,false〉 · swap_r STape 〈grid,false〉.
95   
96 definition R_move_after_left_bar ≝ λ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).
99
100 lemma sem_move_after_left_bar : Realize ? move_after_left_bar R_move_after_left_bar.
101 #intape 
102 cases (sem_seq … (sem_move_l …) (sem_seq … (ssem_move_char_l STape 〈grid,false〉)
103         (sem_swap_r 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 (proj2 ?? 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 (proj2 ?? 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) ]
115       | @Hmemb ]
116     | % #Hc0 lapply (Hnogrids c0 ?)
117       [ @memb_hd | >Hc0 normalize #Hfalse destruct (Hfalse) ]
118     | #Htb whd in ⊢(%→?); >Htb #Houtc lapply (proj2 ?? Houtc … (refl ??)) -Houtc #Houtc
119       >reverse_cons >associative_append @Houtc
120 ]]
121 qed.
122
123 definition move_tape_r ≝ 
124   move_r … · init_cell · move_l … · swap_r STape 〈grid,false〉 ·
125     move_after_left_bar · move_l … · move_after_left_bar · move_r ….
126
127 definition R_move_tape_r ≝ λt1,t2.
128   ∀rs,n,table,c0,bc0,curconfig,ls0.
129   bit_or_null c0 = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) → 
130   t1 = midtape STape (table@〈grid,false〉::〈c0,bc0〉::curconfig@〈grid,false〉::ls0) 
131          〈grid,false〉 rs →
132   (rs = [] ∧
133    t2 = midtape STape (〈c0,bc0〉::ls0) 〈grid,false〉 (reverse STape curconfig@〈null,false〉::
134                              〈grid,false〉::reverse STape table@[〈grid,false〉])) ∨
135   (∃r0,rs0.rs = r0::rs0 ∧
136    t2 = midtape STape (〈c0,bc0〉::ls0) 〈grid,false〉 (reverse STape curconfig@r0::
137                              〈grid,false〉::reverse STape table@〈grid,false〉::rs0)).
138
139 lemma sem_move_tape_r : Realize ? move_tape_r R_move_tape_r.
140 #tapein 
141 cases (sem_seq …(sem_move_r …) (sem_seq … sem_init_cell (sem_seq … (sem_move_l …)
142    (sem_seq … (sem_swap_r STape 〈grid,false〉) (sem_seq … sem_move_after_left_bar
143      (sem_seq … (sem_move_l …) (sem_seq … sem_move_after_left_bar (sem_move_r …))))))) tapein)
144 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
145 #rs #n #table #c0 #bc0 #curconfig #ls0 #Hbitnullc0 #Hbitnullcc #Htable #Htapein
146 cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (proj2 ?? Hta … Htapein) -Hta #Hta
147 * #tb * whd in ⊢ (%→?); *
148 [ * #r0 *
149   generalize in match Hta; generalize in match Htapein; -Htapein -Hta cases rs
150   [ #_ #Hta >Hta normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
151   #r1 #rs1 #Htapein #Hta change with (midtape ?? r1 rs1) in Hta:(???%); >Hta 
152   #Hr0 whd in Hr0:(??%?); #Htb * #tc * whd in ⊢ (%→?); #Htc lapply (proj2 ?? Htc … Htb) -Htc #Htc
153   * #td * whd in ⊢ (%→?); #Htd lapply (proj2 ?? Htd … Htc) -Htd #Htd
154   * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?) [ #x #memx @(no_grids_in_table … Htable) @memb_reverse @memx] 
155   -Hte #Hte
156   * #tf * whd in ⊢ (%→?); #Htf lapply (proj2 ?? 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 (proj2 ?? 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 (proj2 ?? Htc … Htb) -Htc #Htc
164   * #td * whd in ⊢ (%→?); #Htd lapply (proj2 ?? Htd … Htc) -Htd #Htd
165   * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?) [ #x #memx @(no_grids_in_table … Htable) @memb_reverse @memx] -Hte #Hte
166   * #tf * whd in ⊢ (%→?); #Htf lapply (proj2 ?? 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 (proj2 ?? Houtc … Htg) -Houtc #Houtc
169   % % [% | @Houtc ]
170 qed.
171
172 (*
173 MOVE TAPE LEFT:
174
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
180         ^                         move_l
181   ls d? # current c # table # rs
182      ^                            init_cell
183   ls d # current c # table # rs
184      ^                            mtl_aux
185   ls # current c d # table # rs
186                  ^                swap_r
187   ls # current d c # table # rs
188                  ^                mtl_aux
189   ls # current d # table c # rs
190                          ^        swap
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
196      ^
197 *)
198 definition mtl_aux ≝ 
199   swap_r STape 〈grid,false〉 · move_r … · move_r … · 
200     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).
204
205 lemma sem_mtl_aux : Realize ? mtl_aux R_mtl_aux.
206 #intape 
207 cases (sem_seq … (sem_swap_r 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 (proj2 ?? Hta … Hintape) -Hta #Hta
213 * #tb * whd in ⊢(%→?); #Htb lapply (proj2 ?? Htb … Hta) -Htb -Hta whd in ⊢ (???%→?); #Htb
214 * #tc * whd in ⊢(%→?); #Htc lapply (proj2 ?? 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 @(proj2 ?? 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) ]
223     | @Hmemb ]
224   | % #Hc0 lapply (Hnogrids c0 ?)
225     [ @memb_hd | >Hc0 normalize #Hfalse destruct (Hfalse) ]
226   | #Htd whd in ⊢(%→?); >Htd #Houtc lapply (proj2 ?? Houtc … (refl ??)) -Houtc #Houtc
227     >reverse_cons >associative_append @Houtc
228 ]]
229 qed.
230
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).
235
236 lemma sem_ml_atml : 
237   Realize ? ((move_l …) · (adv_to_mark_l … (λc:STape.is_grid (\fst c)))) R_ml_atml.
238 #intape 
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 (proj2 ?? Hta … Hintape) -Hta
243 cases ls1 in Hnogrids;
244 [ #_ #Hta whd in ⊢ (%→?); #Houtc cases (proj2 ?? Houtc … Hta) -Houtc
245  #Houtc #_ >Houtc [@Hta | %]
246 | #c0 #l0 #Hnogrids #Hta whd in ⊢ (%→?); #Houtc cases (proj2 ?? Houtc … Hta) -Houtc
247   #_ #Houtc cases (Houtc ?)
248   [#Houtc #_ >(Houtc … (refl …)(refl …))
249     [>reverse_cons >associative_append %
250     | #x #Hx @Hnogrids @memb_cons //
251     ]
252   |@Hnogrids @memb_hd 
253   ]
254 ]
255 qed.
256
257 definition move_tape_l : TM STape ≝ 
258   (move_l … · adv_to_mark_l … (λc:STape.is_grid (\fst c))) ·
259     (move_l … · adv_to_mark_l … (λc:STape.is_grid (\fst c))) ·
260      move_l … · init_cell · mtl_aux · swap_l STape 〈grid,false〉 ·
261        mtl_aux ·swap_r STape 〈grid,false〉 ·
262          (move_l … · adv_to_mark_l … (λc:STape.is_grid (\fst c))) ·
263            (move_l … · adv_to_mark_l … (λc:STape.is_grid (\fst c))).
264         
265 (*  seq ? (move_r …) (seq ? init_cell (seq ? (move_l …) 
266    (seq ? (swap STape 〈grid,false〉) 
267      (seq ? move_after_left_bar (seq ? (move_l …) move_after_left_bar))))). *)
268
269 axiom daemon: ∀P:Prop.P.
270
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) 
276          〈grid,false〉 rs →
277   (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)).
283    
284 lemma sem_move_tape_l : Realize ? move_tape_l R_move_tape_l.
285 #tapein 
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_l STape 〈grid,false〉)
292        (sem_seq … sem_mtl_aux
293         (sem_seq … (sem_swap_r 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 [#x #memx @(no_grids_in_table … Htable) @memb_reverse @memx] 
299 -Hta #Hta * #tb * whd in ⊢ (%→?); #Htb lapply (Htb (〈c0,bc0〉::curconfig) … Hta)
300 [ @daemon ] -Hta -Htb #Htb
301 * #tc * whd in ⊢ (%→?); #Htc lapply (proj2 ?? Htc … Htb) -Htb -Htc #Htc
302 * #td * whd in ⊢ (%→?); *
303 [ * #c1 * generalize in match Htc; generalize in match Htapein; -Htapein -Htc
304   cases ls0 in Hls0;
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 (proj2 ?? 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 (proj2 ?? 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
322   cases ls0
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 (proj2 ?? 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 (proj2 ?? 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
335     [ >(\P Hx) %
336     | lapply (Hbitnullcc ? Hx) @bit_or_null_not_grid ] ] 
337   -Houtc >reverse_cons >associative_append
338   >reverse_cons >associative_append #Houtc % % [%] @Houtc
339 ]
340 qed.
341
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).
347
348 lemma sem_mtl_aux : Realize ? mtl_aux R_mtl_aux.
349 #intape 
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) ]
362       | @Hmemb ]
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
367 ]]
368 qed.
369
370 check swap*)
371
372
373 (*
374            by cases on current: 
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;
378 *)
379
380 definition lift_tape ≝ λls,c,rs.
381   let 〈c0,b〉 ≝ c in
382   let c' ≝ match c0 with
383   [ null ⇒ None ?
384   | _ ⇒ Some ? c ]
385   in
386   mk_tape STape ls c' rs.
387   
388 definition sim_current_of_tape ≝ λt.
389   match current STape t with
390   [ None ⇒ 〈null,false〉
391   | Some c0 ⇒ c0 ].
392
393
394 definition move_of_unialpha ≝ 
395   λc.match c with
396   [ bit x ⇒ match x with [ true ⇒ R | false ⇒ L ]
397   | _ ⇒ N ].
398
399 definition no_nulls ≝ 
400  λl:list STape.∀x.memb ? x l = true → is_null (\fst x) = false.
401  
402 definition current_of_alpha ≝ λc:STape.
403   match \fst c with [ null ⇒ None ? | _ ⇒ Some ? c ].
404
405 (* 
406    no_marks (c::ls@rs) 
407    only_bits (ls@rs)
408    bit_or_null c
409    
410 *)
411 definition legal_tape ≝ λls,c,rs.
412  no_marks (c::ls@rs) ∧ only_bits (ls@rs) ∧ bit_or_null (\fst c) = true ∧
413  (\fst c ≠ null ∨ ls = [] ∨ rs = []).
414  
415 lemma legal_tape_left :
416   ∀ls,c,rs.legal_tape ls c rs → 
417   left ? (mk_tape STape ls (current_of_alpha c) rs) = ls.
418 #ls * #c #bc #rs * * * #_ #_ #_ *
419 [ *
420   [ cases c
421     [ #c' #_ %
422     | * #Hfalse @False_ind /2/
423     |*: #_ % ]
424   | #Hls >Hls cases c // cases rs //
425   ]
426 | #Hrs >Hrs cases c // cases ls //
427 ]
428 qed.
429
430 axiom legal_tape_current :
431   ∀ls,c,rs.legal_tape ls c rs → 
432   current ? (mk_tape STape ls (current_of_alpha c) rs) = current_of_alpha c.
433
434 axiom legal_tape_right :
435   ∀ls,c,rs.legal_tape ls c rs → 
436   right ? (mk_tape STape ls (current_of_alpha c) rs) = rs.
437
438 (*
439 lemma legal_tape_cases : 
440   ∀ls,c,rs.legal_tape ls c rs → 
441   \fst c ≠ null ∨ (\fst c = null ∧ (ls = [] ∨ rs = [])).
442 #ls #c #rs cases c #c0 #bc0 cases c0
443 [ #c1 normalize #_ % % #Hfalse destruct (Hfalse)
444 | cases ls
445   [ #_ %2 % // % %
446   | #l0 #ls0 cases rs
447     [ #_ %2 % // %2 %
448     | #r0 #rs0 normalize * * #_ #Hrs destruct (Hrs) ]
449   ]
450 |*: #_ % % #Hfalse destruct (Hfalse) ]
451 qed.
452
453 axiom legal_tape_conditions : 
454   ∀ls,c,rs.(\fst c ≠ null ∨ ls = [] ∨ rs = []) → legal_tape ls c rs.
455 (*#ls #c #rs *
456 [ *
457   [ >(eq_pair_fst_snd ?? c) cases (\fst c)
458     [ #c0 #Hc % % %
459     | * #Hfalse @False_ind /2/
460     |*: #Hc % % %
461     ]
462   | cases ls [ * #Hfalse @False_ind /2/ ]
463     #l0 #ls0 
464   
465   #Hc
466 *)
467 *)
468  
469 definition R_move_tape_r_abstract ≝ λt1,t2.
470   ∀rs,n,table,curc,curconfig,ls.
471   is_bit curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) → 
472   t1 = midtape STape (table@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls) 
473          〈grid,false〉 rs →
474   legal_tape ls 〈curc,false〉 rs → 
475   ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs → 
476   ∃ls1,rs1,newc.
477   (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉::
478     〈grid,false〉::reverse ? table@〈grid,false〉::rs1) ∧
479    lift_tape ls1 〈newc,false〉 rs1 = 
480    tape_move_right STape ls 〈curc,false〉 rs ∧ legal_tape ls1 〈newc,false〉 rs1).
481    
482 lemma lift_tape_not_null :
483   ∀ls,c,rs. is_null (\fst c) = false → 
484   lift_tape ls c rs = mk_tape STape ls (Some ? c) rs.
485 #ls * #c0 #bc0 #rs cases c0
486 [|normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
487 //
488 qed.
489
490 axiom bit_not_null :  ∀d.is_bit d = true → is_null d = false.
491  
492 lemma mtr_concrete_to_abstract :
493   ∀t1,t2.R_move_tape_r t1 t2 → R_move_tape_r_abstract t1 t2.
494 #t1 #t2 whd in ⊢(%→?); #Hconcrete
495 #rs #n #table #curc #curconfig #ls #Hbitcurc #Hcurconfig #Htable #Ht1
496 * * * #Hnomarks #Hbits #Hcurc #Hlegal #t1' #Ht1'
497 cases (Hconcrete … Htable Ht1) //
498 [ * #Hrs #Ht2
499   @(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? [])
500   @(ex_intro ?? null) %
501   [ %
502     [ >Ht2 %
503     | >Hrs % ]
504   | % [ % [ %
505     [ >append_nil #x #Hx cases (orb_true_l … Hx) #Hx'
506       [ >(\P Hx') % 
507       | @Hnomarks @(memb_append_l1 … Hx') ]
508     | >append_nil #x #Hx cases (orb_true_l … Hx) #Hx'
509       [ >(\P Hx') //
510       | @Hbits @(memb_append_l1 … Hx') ]]
511     | % ]
512     | %2 % ]
513   ]
514 | * * #r0 #br0 * #rs0 * #Hrs 
515   cut (br0 = false) 
516   [ @(Hnomarks 〈r0,br0〉) @memb_cons @memb_append_l2 >Hrs @memb_hd]
517   #Hbr0 >Hbr0 in Hrs; #Hrs #Ht2
518   @(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? rs0)
519   @(ex_intro ?? r0) %
520   [ %
521     [ >Ht2  //
522     | >Hrs >lift_tape_not_null
523       [ %
524       | @bit_not_null @(Hbits 〈r0,false〉) >Hrs @memb_append_l2 @memb_hd ] ]
525   | % [ % [ %
526     [ #x #Hx cases (orb_true_l … Hx) #Hx'
527       [ >(\P Hx') % 
528       | cases (memb_append … Hx') #Hx'' @Hnomarks 
529         [ @(memb_append_l1 … Hx'') 
530         | >Hrs @memb_cons @memb_append_l2 @(memb_cons … Hx'') ]
531       ]
532     | whd in ⊢ (?%); #x #Hx cases (orb_true_l … Hx) #Hx'
533       [ >(\P Hx') //
534       | cases (memb_append … Hx') #Hx'' @Hbits
535         [ @(memb_append_l1 … Hx'') | >Hrs @memb_append_l2 @(memb_cons … Hx'') ]
536       ]]
537     | whd in ⊢ (??%?); >(Hbits 〈r0,false〉) //
538       @memb_append_l2 >Hrs @memb_hd ]
539     | % % % #Hr0 lapply (Hbits 〈r0,false〉?) 
540       [ @memb_append_l2 >Hrs @memb_hd
541       | >Hr0 normalize #Hfalse destruct (Hfalse)
542       ] ] ] ]
543 qed.
544
545 definition R_move_tape_l_abstract ≝ λt1,t2.
546   ∀rs,n,table,curc,curconfig,ls.
547   is_bit curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) → 
548   t1 = midtape STape (table@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls) 
549          〈grid,false〉 rs →
550   legal_tape ls 〈curc,false〉 rs → 
551   ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs → 
552   ∃ls1,rs1,newc.
553   (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉::
554     〈grid,false〉::reverse ? table@〈grid,false〉::rs1) ∧
555    lift_tape ls1 〈newc,false〉 rs1 = 
556    tape_move_left STape ls 〈curc,false〉 rs ∧ legal_tape ls1 〈newc,false〉 rs1).
557
558 lemma mtl_concrete_to_abstract :
559   ∀t1,t2.R_move_tape_l t1 t2 → R_move_tape_l_abstract t1 t2.
560 #t1 #t2 whd in ⊢(%→?); #Hconcrete
561 #rs #n #table #curc #curconfig #ls #Hcurc #Hcurconfig #Htable #Ht1
562 * * * #Hnomarks #Hbits #Hcurc #Hlegal #t1' #Ht1'
563 cases (Hconcrete … Htable ? Ht1) //
564 [ * #Hls #Ht2
565   @(ex_intro ?? [])
566   @(ex_intro ?? (〈curc,false〉::rs)) 
567   @(ex_intro ?? null) %
568   [ %
569     [ >Ht2 %
570     | >Hls % ]
571   |  % [ % [ %
572     [ #x #Hx cases (orb_true_l … Hx) #Hx'
573       [ >(\P Hx') % 
574       | @Hnomarks >Hls @Hx' ]
575     | #x #Hx cases (orb_true_l … Hx) #Hx'
576       [ >(\P Hx') //
577       | @Hbits >Hls @Hx' ]]
578     | % ]
579     | % %2 % ]
580   ]
581 | * * #l0 #bl0 * #ls0 * #Hls 
582   cut (bl0 = false) 
583   [ @(Hnomarks 〈l0,bl0〉) @memb_cons @memb_append_l1 >Hls @memb_hd]
584   #Hbl0 >Hbl0 in Hls; #Hls #Ht2
585   @(ex_intro ?? ls0) @(ex_intro ?? (〈curc,false〉::rs))
586   @(ex_intro ?? l0) %
587   [ % 
588     [ >Ht2 %
589     | >Hls >lift_tape_not_null
590       [ %
591       | @bit_not_null @(Hbits 〈l0,false〉) >Hls @memb_append_l1 @memb_hd ] ]
592   | % [ % [ %
593     [ #x #Hx cases (orb_true_l … Hx) #Hx'
594       [ >(\P Hx') % 
595       | cases (memb_append … Hx') #Hx'' @Hnomarks 
596         [ >Hls @memb_cons @memb_cons @(memb_append_l1 … Hx'') 
597         | cases (orb_true_l … Hx'') #Hx'''
598           [ >(\P Hx''') @memb_hd
599           | @memb_cons @(memb_append_l2 … Hx''')]
600         ]
601       ]
602     | whd in ⊢ (?%); #x #Hx cases (memb_append … Hx) #Hx'
603       [ @Hbits >Hls @memb_cons @(memb_append_l1 … Hx')
604       | cases (orb_true_l … Hx') #Hx''
605         [ >(\P Hx'') //
606         | @Hbits @(memb_append_l2 … Hx'')
607         ]]]
608     | whd in ⊢ (??%?); >(Hbits 〈l0,false〉) //
609       @memb_append_l1 >Hls @memb_hd ]
610     | % % % #Hl0 lapply (Hbits 〈l0,false〉?) 
611       [ @memb_append_l1 >Hls @memb_hd
612       | >Hl0 normalize #Hfalse destruct (Hfalse)
613       ] ] ] 
614 | #x #Hx @Hbits @memb_append_l1 @Hx ]
615 qed. 
616
617 lemma sem_move_tape_l_abstract : Realize … move_tape_l R_move_tape_l_abstract.
618 @(Realize_to_Realize … mtl_concrete_to_abstract) //
619 qed.
620
621 lemma sem_move_tape_r_abstract : Realize … move_tape_r R_move_tape_r_abstract.
622 @(Realize_to_Realize … mtr_concrete_to_abstract) //
623 qed.
624
625 (*
626  t1 =  ls # cs c # table # rs  
627  
628  let simt ≝ lift_tape ls c rs in
629  let simt' ≝ move_left simt' in
630  
631  t2 = left simt'# cs (sim_current_of_tape simt') # table # right simt'
632 *)
633           
634 (*
635 definition R_move
636
637 definition R_exec_move ≝ λt1,t2.
638   ∀ls,current,table1,newcurrent,table2,rs.
639   t1 = midtape STape (current@〈grid,false〉::ls) 〈grid,false〉
640        (table1@〈comma,true〉::newcurrent@〈comma,false〉::move::table2@
641         〈grid,false〉::rs) → 
642   table_TM (table1@〈comma,false〉::newcurrent@〈comma,false〉::move::table2) →
643   t2 = midtape
644 *)
645
646 (*
647
648 step :
649
650 if is_true(current) (* current state is final *)
651    then nop
652    else 
653    init_match;
654    match_tuple;
655    if is_marked(current) = false (* match ok *)
656       then exec_move; 
657       else sink;
658         
659 *)
660
661
662 definition move_tape ≝ 
663   ifTM ? (test_char ? (λc:STape.c == 〈bit false,false〉)) 
664     (* spostamento a sinistra: verificare se per caso non conviene spostarsi 
665        sulla prima grid invece dell'ultima *)
666     (adv_to_mark_r ? (λc:STape.is_grid (\fst c)) · move_tape_l)
667     (ifTM ? (test_char ? (λc:STape.c == 〈bit true,false〉)) 
668        (adv_to_mark_r ? (λc:STape.is_grid (\fst c)) · move_tape_r)
669        (adv_to_mark_l ? (λc:STape.is_grid (\fst c)) ·
670           move_l … · adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
671        tc_true) tc_true.
672            
673 definition R_move_tape ≝ λt1,t2.
674   ∀rs,n,table1,mv,table2,curc,curconfig,ls.
675   bit_or_null mv = true → only_bits_or_nulls curconfig → 
676   (is_bit mv = true → is_bit curc = true) → 
677   table_TM n (reverse ? table1@〈mv,false〉::table2) → 
678   t1 = midtape STape (table1@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls) 
679          〈mv,false〉 (table2@〈grid,false〉::rs) →
680   legal_tape ls 〈curc,false〉 rs → 
681   ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs → 
682   ∃ls1,rs1,newc.
683   legal_tape ls1 〈newc,false〉 rs1 ∧
684   (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉::
685     〈grid,false〉::reverse ? table1@〈mv,false〉::table2@〈grid,false〉::rs1) ∧
686    ((mv = bit false ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_left STape ls 〈curc,false〉 rs) ∨
687     (mv = bit true ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_right STape ls 〈curc,false〉 rs) ∨
688     (mv = null ∧ ls1 = ls ∧ rs1 = rs ∧ curc = newc))).
689
690 lemma sem_move_tape : Realize ? move_tape R_move_tape.
691 #intape 
692 cases (sem_if ? (test_char ??) … tc_true (sem_test_char ? (λc:STape.c == 〈bit false,false〉))
693         (sem_seq … (sem_adv_to_mark_r ? (λc:STape.is_grid (\fst c))) sem_move_tape_l_abstract)
694         (sem_if ? (test_char ??) … tc_true (sem_test_char ? (λc:STape.c == 〈bit true,false〉))
695         (sem_seq … (sem_adv_to_mark_r ? (λc:STape.is_grid (\fst c))) sem_move_tape_r_abstract)
696         (sem_seq … (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
697           (sem_seq … (sem_move_l …) (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c)))))) intape)
698 #k * #outc * #Hloop #HR
699 @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
700 #rs #n #table1 #mv #table2 #curc #curconfig #ls
701 #Hmv #Hcurconfig #Hmvcurc #Htable #Hintape #Htape #t1' #Ht1'
702 generalize in match HR; -HR *
703 [* #ta * whd in ⊢ (%→?); * * #c * >Hintape normalize in ⊢ (%→?); 
704  #Hdes destruct (Hdes) #eqmv 
705  cut (mv = bit false) [lapply (\P eqmv) #Hdes destruct (Hdes) %] -eqmv #eqmv #Hta 
706  * #tb * whd in ⊢ (%→?); #Htb cases (proj2 ?? Htb … Hta) -Htb -Hta
707   [ * >eqmv normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
708   * * #_ #Htb #_ lapply (Htb ??? (refl ??) (refl …) ?)
709   [ @daemon ] -Htb >append_cons <associative_append #Htb
710   whd in ⊢ (%→?); #Houtc lapply (Houtc … Htb … Ht1') //
711   [ >reverse_append >reverse_append >reverse_reverse @Htable |@Hmvcurc >eqmv % ||]
712   -Houtc -Htb * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal
713   @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) % 
714   [ //
715   | % 
716     [ >Houtc >reverse_append >reverse_append >reverse_reverse
717       >associative_append >associative_append % 
718     | % % % // ]
719   ]
720 | * #ta * whd in ⊢ (%→?); * >Hintape #Hcneq #Hta 
721   cut (mv ≠ bit false) 
722   [lapply (\Pf (Hcneq … (refl …))) @not_to_not #Heq >Heq % ] -Hcneq #Hcneq
723   *
724     [* #tb * * * #ca >Hta -Hta * normalize in ⊢ (%→?); #Hdes destruct (Hdes) #eqmv 
725      cut (mv = bit true) [lapply (\P eqmv) #Hdes destruct (Hdes) %] -eqmv #eqmv 
726      #Htb * #tc * whd in ⊢ (%→?); #Htc cases (proj2 ?? Htc … Htb) -Htc 
727       [ * >(bit_or_null_not_grid … Hmv) #Hfalse destruct (Hfalse) ]
728      * * #_ #Htc lapply (Htc ???(refl ??) (refl ??) ?)
729       [ @daemon ] -Htc >append_cons <associative_append #Htc
730      #_ whd in ⊢ (%→?); #Houtc lapply (Houtc ? n … Htc … Ht1') //
731       [ >reverse_append >reverse_append >reverse_reverse @Htable 
732       | @Hmvcurc @daemon]
733      -Houtc -Htc * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal
734      @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) % 
735       [ //
736       | %
737         [ >Houtc >reverse_append >reverse_append >reverse_reverse
738           >associative_append >associative_append % 
739         | % %2 % // 
740         ]
741       ]
742    |* #tb * whd in ⊢ (%→?); * >Hta #Hcneq' #Htb 
743     cut (mv ≠ bit true) 
744      [lapply (\Pf (Hcneq' … (refl …))) @not_to_not #Heq >Heq % ] -Hcneq' #Hcneq' 
745     * #tc * whd in ⊢ (%→?); #Htc cases (proj2 ?? Htc … Htb) -Htc
746     #_ #Htc cases (Htc (bit_or_null_not_grid … Hmv)) -Htc #Htc #_
747     lapply (Htc … (refl ??) (refl ??) ?) [@daemon] -Htc #Htc
748     * #td * whd in ⊢ (%→?); #Htd lapply (proj2 ?? Htd … Htc) -Htd -Htc
749     whd in ⊢ (???%→?); #Htd whd in ⊢ (%→?); #Houtc cases (proj2 ?? Houtc … Htd) 
750     -Houtc #_ #Houtc cases (Houtc ?) 
751      [2: cases Htape * * #_ #_ #Hcurc #_ >(bit_or_null_not_grid … Hcurc) %]
752     #Houtc #_ lapply (Houtc … (refl ??) (refl ??) ?) [@daemon] -Houtc #Houtc
753     @(ex_intro ?? ls) @(ex_intro ?? rs) @(ex_intro ?? curc) %
754     [ //
755     | %
756       [ @Houtc
757       | %2 % // % // % // 
758         generalize in match Hcneq; generalize in match Hcneq'; 
759         cases mv in Hmv; normalize //
760         [ * #_ normalize [ #Hfalse @False_ind cases Hfalse /2/ | #_ #Hfalse @False_ind cases Hfalse /2/ ] 
761         |*: #Hfalse destruct (Hfalse) ]
762       ]
763     ]
764   ]
765 ]
766 qed.
767