]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/turing/basic_multi_machines.ma
made executable again
[helm.git] / matita / matita / lib / turing / basic_multi_machines.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/turing.ma".
13
14 definition compare_states ≝ initN 3.
15
16 definition comp0 : compare_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
17 definition comp1 : compare_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
18 definition comp2 : compare_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
19
20 definition trans_compare_step ≝ 
21  λi,j.λsig:FinSet.λn.
22  λp:compare_states × (Vector (option sig) (S n)).
23  let 〈q,a〉 ≝ p in
24  match pi1 … q with
25  [ O ⇒ match nth i ? a (None ?) with
26    [ None ⇒ 〈comp2,null_action sig n〉
27    | Some ai ⇒ match nth j ? a (None ?) with 
28      [ None ⇒ 〈comp2,null_action ? n〉
29      | Some aj ⇒ if ai == aj 
30          then 〈comp1,change_vec ? (S n) 
31                       (change_vec ? (S n) (null_action ? n) (〈None ?,R〉) i)
32                         (〈None ?,R〉) j〉
33          else 〈comp2,null_action ? n〉 ]
34    ]
35  | S q ⇒ match q with 
36    [ O ⇒ (* 1 *) 〈comp1,null_action ? n〉
37    | S _ ⇒ (* 2 *) 〈comp2,null_action ? n〉 ] ].
38
39 definition compare_step ≝ 
40   λi,j,sig,n.
41   mk_mTM sig n compare_states (trans_compare_step i j sig n) 
42     comp0 (λq.q == comp1 ∨ q == comp2).
43
44 definition R_comp_step_true ≝ 
45   λi,j,sig,n.λint,outt: Vector (tape sig) (S n).
46   ∃x.
47    current ? (nth i ? int (niltape ?)) = Some ? x ∧
48    current ? (nth j ? int (niltape ?)) = Some ? x ∧
49    outt = change_vec ?? 
50             (change_vec ?? int
51               (tape_move_right ? (nth i ? int (niltape ?))) i)
52             (tape_move_right ? (nth j ? int (niltape ?))) j.
53
54 definition R_comp_step_false ≝ 
55   λi,j:nat.λsig,n.λint,outt: Vector (tape sig) (S n).
56    (current ? (nth i ? int (niltape ?)) ≠ current ? (nth j ? int (niltape ?)) ∨
57     current ? (nth i ? int (niltape ?)) = None ? ∨
58     current ? (nth j ? int (niltape ?)) = None ?) ∧ outt = int.
59
60 lemma comp_q0_q2_null :
61   ∀i,j,sig,n,v.i < S n → j < S n → 
62   (nth i ? (current_chars ?? v) (None ?) = None ? ∨
63    nth j ? (current_chars ?? v) (None ?) = None ?) → 
64   step sig n (compare_step i j sig n) (mk_mconfig ??? comp0 v) 
65   = mk_mconfig ??? comp2 v.
66 #i #j #sig #n #v #Hi #Hj
67 whd in ⊢ (? → ??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (?→??%?);
68 * #Hcurrent
69 [ @eq_f2
70   [ whd in ⊢ (??(???%)?); >Hcurrent %
71   | whd in ⊢ (??(????(???%))?); >Hcurrent @tape_move_null_action ]
72 | @eq_f2
73   [ whd in ⊢ (??(???%)?); >Hcurrent cases (nth i ?? (None sig)) //
74   | whd in ⊢ (??(????(???%))?); >Hcurrent
75     cases (nth i ?? (None sig)) [|#x] @tape_move_null_action ] ]
76 qed.
77
78 lemma comp_q0_q2_neq :
79   ∀i,j,sig,n,v.i < S n → j < S n → 
80   (nth i ? (current_chars ?? v) (None ?) ≠ nth j ? (current_chars ?? v) (None ?)) → 
81   step sig n (compare_step i j sig n) (mk_mconfig ??? comp0 v) 
82   = mk_mconfig ??? comp2 v.
83 #i #j #sig #n #v #Hi #Hj lapply (refl ? (nth i ?(current_chars ?? v)(None ?)))
84 cases (nth i ?? (None ?)) in ⊢ (???%→?);
85 [ #Hnth #_ @comp_q0_q2_null // % //
86 | #ai #Hai lapply (refl ? (nth j ?(current_chars ?? v)(None ?)))
87   cases (nth j ?? (None ?)) in ⊢ (???%→?);
88   [ #Hnth #_ @comp_q0_q2_null // %2 //
89   | #aj #Haj * #Hneq
90     whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
91     [ whd in match (trans ????); >Hai >Haj
92       whd in ⊢ (??(???%)?); cut ((ai==aj)=false)
93       [>(\bf ?) /2 by not_to_not/ % #Haiaj @Hneq
94        >Hai >Haj //
95       | #Haiaj >Haiaj % ]
96     | whd in match (trans ????); >Hai >Haj
97       whd in ⊢ (??(????(???%))?); cut ((ai==aj)=false)
98       [>(\bf ?) /2 by not_to_not/ % #Haiaj @Hneq
99        >Hai >Haj //
100       |#Hcut >Hcut @tape_move_null_action
101       ]
102     ]
103   ]
104 ]
105 qed.
106
107 lemma comp_q0_q1 :
108   ∀i,j,sig,n,v,a.i ≠ j → i < S n → j < S n → 
109   nth i ? (current_chars ?? v) (None ?) = Some ? a →
110   nth j ? (current_chars ?? v) (None ?) = Some ? a → 
111   step sig n (compare_step i j sig n) (mk_mconfig ??? comp0 v) =
112     mk_mconfig ??? comp1 
113      (change_vec ? (S n) 
114        (change_vec ?? v
115          (tape_move_right ? (nth i ? v (niltape ?))) i)
116        (tape_move_right ? (nth j ? v (niltape ?))) j).
117 #i #j #sig #n #v #a #Heq #Hi #Hj #Ha1 #Ha2
118 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
119 [ whd in match (trans ????);
120   >Ha1 >Ha2 whd in ⊢ (??(???%)?); >(\b ?) //
121 | whd in match (trans ????);
122   >Ha1 >Ha2 whd in ⊢ (??(????(???%))?); >(\b ?) //
123   change with (change_vec ?????) in ⊢ (??(????%)?);
124   <(change_vec_same … v j (niltape ?)) in ⊢ (??%?);
125   <(change_vec_same … v i (niltape ?)) in ⊢ (??%?);
126   >tape_move_multi_def 
127   >pmap_change >pmap_change <tape_move_multi_def
128   >tape_move_null_action
129   @eq_f2 // >nth_change_vec_neq //
130 ]
131 qed.
132
133 lemma sem_comp_step :
134   ∀i,j,sig,n.i ≠ j → i < S n → j < S n → 
135   compare_step i j sig n ⊨ 
136     [ comp1: R_comp_step_true i j sig n, 
137              R_comp_step_false i j sig n ].
138 #i #j #sig #n #Hneq #Hi #Hj #int
139 lapply (refl ? (current ? (nth i ? int (niltape ?))))
140 cases (current ? (nth i ? int (niltape ?))) in ⊢ (???%→?);
141 [ #Hcuri %{2} %
142   [| % [ %
143     [ whd in ⊢ (??%?); >comp_q0_q2_null /2/ 
144     | normalize in ⊢ (%→?); #H destruct (H) ]
145   | #_ % // % %2 // ] ]
146 | #a #Ha lapply (refl ? (current ? (nth j ? int (niltape ?))))
147   cases (current ? (nth j ? int (niltape ?))) in ⊢ (???%→?);
148   [ #Hcurj %{2} %
149     [| % [ %
150        [ whd in ⊢ (??%?); >comp_q0_q2_null /2/ %2
151        | normalize in ⊢ (%→?); #H destruct (H) ]
152        | #_ % // >Ha >Hcurj % % % #H destruct (H) ] ]
153   | #b #Hb %{2} cases (true_or_false (a == b)) #Hab
154     [ %
155       [| % [ % 
156         [whd in ⊢  (??%?);  >(comp_q0_q1 … a Hneq Hi Hj) //
157          >(\P Hab) <Hb @sym_eq @nth_vec_map
158         | #_ whd >(\P Hab) %{b} % // % // <(\P Hab) // ]
159         | * #H @False_ind @H %
160       ] ]
161     | %
162       [| % [ % 
163         [whd in ⊢  (??%?);  >comp_q0_q2_neq //
164          <(nth_vec_map ?? (current …) i ? int (niltape ?))
165          <(nth_vec_map ?? (current …) j ? int (niltape ?)) >Ha >Hb
166          @(not_to_not ??? (\Pf Hab)) #H destruct (H) %
167         | normalize in ⊢ (%→?); #H destruct (H) ]
168       | #_ % // % % >Ha >Hb @(not_to_not ??? (\Pf Hab)) #H destruct (H) % ] ]
169     ]
170   ]
171 ]
172 qed.
173 (* copy a character from src tape to dst tape without moving them *)
174
175 definition copy_states ≝ initN 3.
176
177 definition cc0 : copy_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
178 definition cc1 : copy_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
179
180 definition trans_copy_char_N ≝ 
181  λsrc,dst.λsig:FinSet.λn.
182  λp:copy_states × (Vector (option sig) (S n)).
183  let 〈q,a〉 ≝ p in
184  match pi1 … q with
185  [ O ⇒ 〈cc1,change_vec ? (S n) 
186            (change_vec ? (S n) (null_action ? n) (〈None ?,N〉) src)
187            (〈nth src ? a (None ?),N〉) dst〉
188  | S _ ⇒ 〈cc1,null_action ? n〉 ].
189
190 definition copy_char_N ≝ 
191   λsrc,dst,sig,n.
192   mk_mTM sig n copy_states (trans_copy_char_N src dst sig n) 
193     cc0 (λq.q == cc1).
194
195 definition R_copy_char_N ≝ 
196   λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
197   outt = change_vec ?? int
198           (tape_write  ? (nth dst ? int (niltape ?))
199             (current ? (nth src ? int (niltape ?)))) dst.
200
201 lemma copy_char_N_q0_q1 :
202   ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n → 
203   step sig n (copy_char_N src dst sig n) (mk_mconfig ??? cc0 v) =
204     mk_mconfig ??? cc1 
205      (change_vec ?? v
206        (tape_write  ? (nth dst ? v (niltape ?))
207           (current ? (nth src ? v (niltape ?)))) dst).
208 #src #dst #sig #n #v #Heq #Hsrc #Hdst
209 whd in ⊢ (??%?); @eq_f
210 <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
211 <(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
212 >tape_move_multi_def
213 >pmap_change >pmap_change <tape_move_multi_def
214 >tape_move_null_action @eq_f3 //
215 [ >change_vec_same %
216 | >change_vec_same >change_vec_same >nth_current_chars // ]
217 qed.
218
219 lemma sem_copy_char_N:
220   ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n → 
221   copy_char_N src dst sig n ⊨ R_copy_char_N src dst sig n.
222 #src #dst #sig #n #Hneq #Hsrc #Hdst #int
223 %{2} % [| % [ % | whd >copy_char_N_q0_q1 // ]]
224 qed.
225
226 (* copy a character from src tape to dst tape and advance both tape to
227    the right - useful for copying stings 
228
229 definition copy_char_states ≝ initN 3.
230
231 definition trans_copy_char ≝ 
232  λsrc,dst.λsig:FinSet.λn.
233  λp:copy_char_states × (Vector (option sig) (S n)).
234  let 〈q,a〉 ≝ p in
235  match pi1 … q with
236  [ O ⇒ 〈cc1,change_vec ? (S n) 
237            (change_vec ? (S n) (null_action ? n) (〈None ?,R〉) src)
238            (〈nth src ? a (None ?),R〉) dst〉
239  | S _ ⇒ 〈cc1,null_action ? n〉 ].
240
241 definition copy_char ≝ 
242   λsrc,dst,sig,n.
243   mk_mTM sig n copy_char_states (trans_copy_char src dst sig n) 
244     cc0 (λq.q == cc1).
245
246 definition R_copy_char ≝ 
247   λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
248   outt = change_vec ?? 
249          (change_vec ?? int
250           (tape_move_mono ? (nth src ? int (niltape ?)) 〈None ?, R〉) src)
251           (tape_move_mono ? (nth dst ? int (niltape ?)) 
252            〈current ? (nth src ? int (niltape ?)), R〉) dst.
253
254 lemma copy_char_q0_q1 :
255   ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n → 
256   step sig n (copy_char src dst sig n) (mk_mconfig ??? cc0 v) =
257     mk_mconfig ??? cc1 
258      (change_vec ? (S n) 
259        (change_vec ?? v
260          (tape_move_mono ? (nth src ? v (niltape ?)) 〈None ?, R〉) src)
261             (tape_move_mono ? (nth dst ? v (niltape ?)) 〈current ? (nth src ? v (niltape ?)), R〉) dst).
262 #src #dst #sig #n #v #Heq #Hsrc #Hdst
263 whd in ⊢ (??%?);
264 <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
265 <(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
266 >tape_move_multi_def @eq_f2 //
267 >pmap_change >pmap_change <tape_move_multi_def
268 >tape_move_null_action @eq_f2 // @eq_f2
269 [ >change_vec_same %
270 | >change_vec_same >change_vec_same // ]
271 qed.
272
273 lemma sem_copy_char:
274   ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n → 
275   copy_char src dst sig n ⊨ R_copy_char src dst sig n.
276 #src #dst #sig #n #Hneq #Hsrc #Hdst #int
277 %{2} % [| % [ % | whd >copy_char_q0_q1 // ]]
278 qed.*)
279
280 definition copy0 : copy_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
281 definition copy1 : copy_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
282 definition copy2 : copy_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
283
284 definition trans_copy_step ≝ 
285  λsrc,dst.λsig:FinSet.λn.
286  λp:copy_states × (Vector (option sig) (S n)).
287  let 〈q,a〉 ≝ p in
288  match pi1 … q with
289  [ O ⇒ match nth src ? a (None ?) with
290    [ None ⇒ 〈copy2,null_action sig n〉
291    | Some ai ⇒ match nth dst ? a (None ?) with 
292      [ None ⇒ 〈copy2,null_action ? n〉
293      | Some aj ⇒ 
294          〈copy1,change_vec ? (S n) 
295            (change_vec ? (S n) (null_action ? n) (〈None ?,R〉) src)
296            (〈Some ? ai,R〉) dst〉
297      ]
298    ]
299  | S q ⇒ match q with 
300    [ O ⇒ (* 1 *) 〈copy1,null_action ? n〉
301    | S _ ⇒ (* 2 *) 〈copy2,null_action ? n〉 ] ].
302
303 definition copy_step ≝ 
304   λsrc,dst,sig,n.
305   mk_mTM sig n copy_states (trans_copy_step src dst sig n) 
306     copy0 (λq.q == copy1 ∨ q == copy2).
307
308 definition R_copy_step_true ≝ 
309   λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
310   ∃x,y.
311    current ? (nth src ? int (niltape ?)) = Some ? x ∧
312    current ? (nth dst ? int (niltape ?)) = Some ? y ∧
313    outt = change_vec ?? 
314             (change_vec ?? int
315               (tape_move_mono ? (nth src ? int (niltape ?)) 〈None ?, R〉) src)
316             (tape_move_mono ? (nth dst ? int (niltape ?)) 〈Some ? x, R〉) dst.
317
318 definition R_copy_step_false ≝ 
319   λsrc,dst:nat.λsig,n.λint,outt: Vector (tape sig) (S n).
320     (current ? (nth src ? int (niltape ?)) = None ? ∨
321      current ? (nth dst ? int (niltape ?)) = None ?) ∧ outt = int.
322
323 lemma copy_q0_q2_null :
324   ∀src,dst,sig,n,v.src < S n → dst < S n → 
325   (nth src ? (current_chars ?? v) (None ?) = None ? ∨
326    nth dst ? (current_chars ?? v) (None ?) = None ?) → 
327   step sig n (copy_step src dst sig n) (mk_mconfig ??? copy0 v) 
328   = mk_mconfig ??? copy2 v.
329 #src #dst #sig #n #v #Hi #Hj
330 whd in ⊢ (? → ??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (?→??%?);
331 * #Hcurrent
332 [ @eq_f2
333   [ whd in ⊢ (??(???%)?); >Hcurrent %
334   | whd in ⊢ (??(????(???%))?); >Hcurrent @tape_move_null_action ]
335 | @eq_f2
336   [ whd in ⊢ (??(???%)?); >Hcurrent cases (nth src ?? (None sig)) //
337   | whd in ⊢ (??(????(???%))?); >Hcurrent
338     cases (nth src ?? (None sig)) [|#x] @tape_move_null_action ] ]
339 qed.
340
341 lemma copy_q0_q1 :
342   ∀src,dst,sig,n,v,a,b.src ≠ dst → src < S n → dst < S n → 
343   nth src ? (current_chars ?? v) (None ?) = Some ? a →
344   nth dst ? (current_chars ?? v) (None ?) = Some ? b → 
345   step sig n (copy_step src dst sig n) (mk_mconfig ??? copy0 v) =
346     mk_mconfig ??? copy1 
347      (change_vec ? (S n) 
348        (change_vec ?? v
349          (tape_move_mono ? (nth src ? v (niltape ?)) 〈None ?, R〉) src)
350             (tape_move_mono ? (nth dst ? v (niltape ?)) 〈Some ? a, R〉) dst).
351 #src #dst #sig #n #v #a #b #Heq #Hsrc #Hdst #Ha1 #Ha2
352 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
353 [ whd in match (trans ????);
354   >Ha1 >Ha2 whd in ⊢ (??(???%)?); >(\b ?) //
355 | whd in match (trans ????);
356   >Ha1 >Ha2 whd in ⊢ (??(????(???%))?); >(\b ?) //
357   change with (change_vec ?????) in ⊢ (??(????%)?);
358   <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
359   <(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
360   >tape_move_multi_def 
361   >pmap_change >pmap_change <tape_move_multi_def
362   >tape_move_null_action
363   @eq_f2 // >nth_change_vec_neq //
364 ]
365 qed.
366
367 lemma sem_copy_step :
368   ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n → 
369   copy_step src dst sig n ⊨ 
370     [ copy1: R_copy_step_true src dst sig n, 
371             R_copy_step_false src dst sig n ].
372 #src #dst #sig #n #Hneq #Hsrc #Hdst #int
373 lapply (refl ? (current ? (nth src ? int (niltape ?))))
374 cases (current ? (nth src ? int (niltape ?))) in ⊢ (???%→?);
375 [ #Hcur_src %{2} %
376   [| % [ %
377     [ whd in ⊢ (??%?); >copy_q0_q2_null /2/ 
378     | normalize in ⊢ (%→?); #H destruct (H) ]
379   | #_ % // % // ] ]
380 | #a #Ha lapply (refl ? (current ? (nth dst ? int (niltape ?))))
381   cases (current ? (nth dst ? int (niltape ?))) in ⊢ (???%→?);
382   [ #Hcur_dst %{2} %
383     [| % [ %
384        [ whd in ⊢ (??%?); >copy_q0_q2_null /2/ 
385        | normalize in ⊢ (%→?); #H destruct (H) ]
386        | #_ % // %2 >Hcur_dst % ] ]
387   | #b #Hb %{2} %
388     [| % [ % 
389       [whd in ⊢  (??%?);  >(copy_q0_q1 … a b Hneq Hsrc Hdst) //
390       | #_ %{a} %{b} % // % //]
391       | * #H @False_ind @H %
392       ]
393     ]
394   ]
395 ]
396 qed.
397
398
399 (* advance in parallel on tapes src and dst; stops if one of the
400    two tapes is in oveflow *)
401
402 definition parmove_states ≝ initN 3.
403
404 definition parmove0 : parmove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
405 definition parmove1 : parmove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
406 definition parmove2 : parmove_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
407
408 (*
409    src: a b c ... z ---→ a b c ... z 
410         ^                            ^
411    dst: _ _ _ ... _ ---→ a b c ... z 
412         ^                            ^
413
414    0) (x,_) → (x,_)(R,R) → 1
415       (None,_) → None 2
416    1) (_,_) → None 1
417    2) (_,_) → None 2
418 *)
419
420 definition trans_parmove_step ≝ 
421  λsrc,dst,sig,n,D.
422  λp:parmove_states × (Vector (option sig) (S n)).
423  let 〈q,a〉 ≝ p in
424  match pi1 … q with
425  [ O ⇒ match nth src ? a (None ?) with
426    [ None ⇒ 〈parmove2,null_action sig n〉
427    | Some a0 ⇒ match nth dst ? a (None ?) with
428      [ None ⇒ 〈parmove2,null_action ? n〉
429      | Some a1 ⇒ 〈parmove1,change_vec ? (S n)
430                           (change_vec ?(S n)
431                            (null_action ? n) (〈None ?,D〉) src)
432                           (〈None ?,D〉) dst〉 ] ]
433  | S q ⇒ match q with 
434    [ O ⇒ (* 1 *) 〈parmove1,null_action ? n〉
435    | S _ ⇒ (* 2 *) 〈parmove2,null_action ? n〉 ] ].
436
437 definition parmove_step ≝ 
438   λsrc,dst,sig,n,D.
439   mk_mTM sig n parmove_states (trans_parmove_step src dst sig n D) 
440     parmove0 (λq.q == parmove1 ∨ q == parmove2).
441
442 definition R_parmove_step_true ≝ 
443   λsrc,dst,sig,n,D.λint,outt: Vector (tape sig) (S n).
444   ∃x1,x2.
445    current ? (nth src ? int (niltape ?)) = Some ? x1 ∧
446    current ? (nth dst ? int (niltape ?)) = Some ? x2 ∧
447    outt = change_vec ?? 
448             (change_vec ?? int
449               (tape_move ? (nth src ? int (niltape ?)) D) src)
450             (tape_move ? (nth dst ? int (niltape ?)) D) dst.
451
452 definition R_parmove_step_false ≝ 
453   λsrc,dst:nat.λsig,n.λint,outt: Vector (tape sig) (S n).
454   (current ? (nth src ? int (niltape ?)) = None ?  ∨
455    current ? (nth dst ? int (niltape ?)) = None ?) ∧
456    outt = int.
457
458 lemma parmove_q0_q2_null_src :
459   ∀src,dst,sig,n,D,v.src < S n → dst < S n → 
460   nth src ? (current_chars ?? v) (None ?) = None ? → 
461   step sig n (parmove_step src dst sig n D)
462     (mk_mconfig ??? parmove0 v) =
463     mk_mconfig ??? parmove2 v.
464 #src #dst #sig #n #D #v #Hsrc #Hdst #Hcurrent
465 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
466 @eq_f2
467 [ whd in ⊢ (??(???%)?); >Hcurrent %
468 | whd in ⊢ (??(????(???%))?); >Hcurrent @tape_move_null_action ]
469 qed.
470
471 lemma parmove_q0_q2_null_dst :
472   ∀src,dst,sig,n,D,v,s.src < S n → dst < S n → 
473   nth src ? (current_chars ?? v) (None ?) = Some ? s → 
474   nth dst ? (current_chars ?? v) (None ?) = None ? → 
475   step sig n (parmove_step src dst sig n D)
476     (mk_mconfig ??? parmove0 v) =
477     mk_mconfig ??? parmove2 v.
478 #src #dst #sig #n #D #v #s #Hsrc #Hdst #Hcursrc #Hcurdst
479 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
480 @eq_f2
481 [ whd in ⊢ (??(???%)?); >Hcursrc whd in ⊢ (??(???%)?); >Hcurdst %
482 | whd in ⊢ (??(????(???%))?); >Hcursrc
483   whd in ⊢ (??(????(???%))?); >Hcurdst @tape_move_null_action ]
484 qed.
485
486 lemma parmove_q0_q1 :
487   ∀src,dst,sig,n,D,v.src ≠ dst → src < S n → dst < S n → 
488   ∀a1,a2.
489   nth src ? (current_chars ?? v) (None ?) = Some ? a1 →
490   nth dst ? (current_chars ?? v) (None ?) = Some ? a2 → 
491   step sig n (parmove_step src dst sig n D)
492     (mk_mconfig ??? parmove0 v) =
493     mk_mconfig ??? parmove1 
494      (change_vec ? (S n) 
495        (change_vec ?? v
496          (tape_move ? (nth src ? v (niltape ?)) D) src)
497        (tape_move ? (nth dst ? v (niltape ?)) D) dst).
498 #src #dst #sig #n #D #v #Hneq #Hsrc #Hdst
499 #a1 #a2 #Hcursrc #Hcurdst
500 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
501 [ whd in match (trans ????);
502   >Hcursrc >Hcurdst %
503 | whd in match (trans ????);
504   >Hcursrc >Hcurdst whd in ⊢ (??(????(???%))?); 
505   >tape_move_multi_def <(change_vec_same ?? v dst (niltape ?)) in ⊢ (??%?);
506   >pmap_change <(change_vec_same ?? v src (niltape ?)) in ⊢(??%?);
507   >pmap_change <tape_move_multi_def >tape_move_null_action
508   @eq_f2 // >nth_change_vec_neq //
509 ]
510 qed.
511
512 lemma sem_parmove_step :
513   ∀src,dst,sig,n,D.src ≠ dst → src < S n → dst < S n → 
514   parmove_step src dst sig n D ⊨ 
515     [ parmove1: R_parmove_step_true src dst sig n D, 
516              R_parmove_step_false src dst sig n ].
517 #src #dst #sig #n #D #Hneq #Hsrc #Hdst #int
518 lapply (refl ? (current ? (nth src ? int (niltape ?))))
519 cases (current ? (nth src ? int (niltape ?))) in ⊢ (???%→?);
520 [ #Hcursrc %{2} %
521   [| % [ %
522     [ whd in ⊢ (??%?); >parmove_q0_q2_null_src /2/
523     | normalize in ⊢ (%→?); #H destruct (H) ]
524     | #_ % // % // ] ]
525 | #a #Ha lapply (refl ? (current ? (nth dst ? int (niltape ?))))
526   cases (current ? (nth dst ? int (niltape ?))) in ⊢ (???%→?);
527   [ #Hcurdst %{2} %
528     [| % [ %
529       [ whd in ⊢ (??%?); >(parmove_q0_q2_null_dst …) /2/ 
530       | normalize in ⊢ (%→?); #H destruct (H) ]
531       | #_ % // %2 // ] ]
532   | #b #Hb %{2} %
533     [| % [ % 
534       [whd in ⊢  (??%?); >(parmove_q0_q1 … Hneq Hsrc Hdst ? b ??)
535         [2: <(nth_vec_map ?? (current …) dst ? int (niltape ?)) //
536         |3: <(nth_vec_map ?? (current …) src ? int (niltape ?)) //
537         | // ]
538       | #_ %{a} %{b} % // % // ]
539       | * #H @False_ind @H % ]
540 ]]]
541 qed.
542
543 (* perform a symultaneous test on all tapes; ends up in state partest1 if
544    the test is succesfull and partest2 otherwise *)
545
546 definition partest_states ≝ initN 3.
547
548 definition partest0 : partest_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
549 definition partest1 : partest_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
550 definition partest2 : partest_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
551
552 definition trans_partest ≝ 
553  λsig,n,test.
554  λp:partest_states × (Vector (option sig) (S n)).
555  let 〈q,a〉 ≝ p in
556  if test a then 〈partest1,null_action sig n〉 
557  else 〈partest2,null_action ? n〉.
558
559 definition partest ≝ 
560   λsig,n,test.
561   mk_mTM sig n partest_states (trans_partest sig n test) 
562     partest0 (λq.q == partest1 ∨ q == partest2).
563
564 definition R_partest_true ≝ 
565   λsig,n,test.λint,outt: Vector (tape sig) (S n).
566   test (current_chars ?? int) = true ∧ outt = int.
567   
568 definition R_partest_false ≝ 
569   λsig,n,test.λint,outt: Vector (tape sig) (S n).
570   test (current_chars ?? int) = false ∧ outt = int.
571
572 lemma partest_q0_q1:
573   ∀sig,n,test,v.
574   test (current_chars ?? v) = true → 
575   step sig n (partest sig n test)(mk_mconfig ??? partest0 v) 
576     = mk_mconfig ??? partest1 v.
577 #sig #n #test #v #Htest
578 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
579 @eq_f2
580 [ whd in ⊢ (??(???%)?); >Htest %
581 | whd in ⊢ (??(????(???%))?); >Htest @tape_move_null_action ]
582 qed.
583
584 lemma partest_q0_q2:
585   ∀sig,n,test,v.
586   test (current_chars ?? v) = false → 
587   step sig n (partest sig n test)(mk_mconfig ??? partest0 v) 
588     = mk_mconfig ??? partest2 v.
589 #sig #n #test #v #Htest
590 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
591 @eq_f2
592 [ whd in ⊢ (??(???%)?); >Htest %
593 | whd in ⊢ (??(????(???%))?); >Htest @tape_move_null_action ]
594 qed.
595
596 lemma sem_partest:
597   ∀sig,n,test.
598   partest sig n test ⊨ 
599     [ partest1: R_partest_true sig n test, R_partest_false sig n test ].
600 #sig #n #test #int
601 cases (true_or_false (test (current_chars ?? int))) #Htest
602 [ %{2} %{(mk_mconfig ? partest_states n partest1 int)} %
603   [ % [ whd in ⊢ (??%?); >partest_q0_q1 /2/ | #_ % // ] 
604   | * #H @False_ind @H %
605   ]
606 | %{2} %{(mk_mconfig ? partest_states n partest2 int)} %
607   [ % [ whd in ⊢ (??%?); >partest_q0_q2 /2/ 
608       | whd in ⊢ (??%%→?); #H destruct (H)]
609   | #_ % //]
610 ]
611 qed.