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.