matita/matita/lib/turing/basic_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/while_machine.ma".
  13
  14 (******************* write a given symbol under the head **********************)
  15 definition write_states ≝ initN 2.
  16
  17 definition wr0 : write_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
  18 definition wr1 : write_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
  19
  20 definition write ≝ λalpha,c.
  21   mk_TM alpha write_states
  22   (λp.let 〈q,a〉 ≝ p in
  23     match pi1 … q with
  24     [ O ⇒ 〈wr1,Some ? c,N〉
  25     | S _ ⇒ 〈wr1,None ?,N〉 ])
  26   wr0 (λx.x == wr1).
  27
  28 definition R_write ≝ λalpha,c,t1,t2.
  29   ∀ls,x,rs.t1 = midtape alpha ls x rs → t2 = midtape alpha ls c rs.
  30
  31 lemma sem_write : ∀alpha,c.Realize ? (write alpha c) (R_write alpha c).
  32 #alpha #c #t @(ex_intro … 2) @ex_intro
  33   [|% [% |#ls #c #rs #Ht >Ht % ] ]
  34 qed.
  35
  36 definition R_write_strong ≝ λalpha,c,t1,t2.
  37   t2 = midtape alpha (left ? t1) c (right ? t1).
  38
  39 lemma sem_write_strong : ∀alpha,c.Realize ? (write alpha c) (R_write_strong alpha c).
  40 #alpha #c #t @(ex_intro … 2) @ex_intro
  41   [|% [% |cases t normalize // ] ]
  42 qed.
  43
  44 (******************** moves the head one step to the right ********************)
  45
  46 definition move_states ≝ initN 2.
  47 definition move0 : move_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
  48 definition move1 : move_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
  49
  50 definition move_r ≝
  51   λalpha:FinSet.mk_TM alpha move_states
  52   (λp.let 〈q,a〉 ≝ p in
  53     match a with
  54     [ None ⇒ 〈move1,None ?,N〉
  55     | Some a' ⇒ match (pi1 … q) with
  56       [ O ⇒ 〈move1,Some ? a',R〉
  57       | S q ⇒ 〈move1,None ?,N〉 ] ])
  58   move0 (λq.q == move1).
  59
  60 definition R_move_r ≝ λalpha,t1,t2.
  61   (current ? t1 = None ? → t1 = t2) ∧
  62   ∀ls,c,rs.
  63     t1 = midtape alpha ls c rs →
  64     t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
  65 (*
  66   (current ? t1 = None ? ∧ t1 = t2) ∨
  67   ∃ls,c,rs.
  68   t1 = midtape alpha ls c rs ∧
  69   t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).*)
  70
  71 lemma sem_move_r :
  72   ∀alpha.Realize ? (move_r alpha) (R_move_r alpha).
  73 #alpha #intape @(ex_intro ?? 2) cases intape
  74 [ @ex_intro
  75   [| % [ % | % // #ls #c #rs #H destruct ] ]
  76 |#a #al @ex_intro
  77   [| % [ % | % // #ls #c #rs #H destruct ] ]
  78 |#a #al @ex_intro
  79   [| % [ % | % // #ls #c #rs #H destruct ] ]
  80 | #ls #c #rs
  81   @ex_intro [| % [ % | % [whd in ⊢ ((??%?)→?); #H destruct]
  82   #ls1 #c1 #rs1 #H destruct cases rs1 // ] ] ]
  83 qed.
  84
  85 (******************** moves the head one step to the left *********************)
  86
  87 definition move_l ≝
  88   λalpha:FinSet.mk_TM alpha move_states
  89   (λp.let 〈q,a〉 ≝ p in
  90     match a with
  91     [ None ⇒ 〈move1,None ?,N〉
  92     | Some a' ⇒ match pi1 … q with
  93       [ O ⇒ 〈move1,Some ? a',L〉
  94       | S q ⇒ 〈move1,None ?,N〉 ] ])
  95   move0 (λq.q == move1).
  96
  97 definition R_move_l ≝ λalpha,t1,t2.
  98   (current ? t1 = None ? → t1 = t2) ∧
  99   ∀ls,c,rs.
 100     t1 = midtape alpha ls c rs →
 101     t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
 102
 103 lemma sem_move_l :
 104   ∀alpha.Realize ? (move_l alpha) (R_move_l alpha).
 105 #alpha #intape @(ex_intro ?? 2) cases intape
 106 [ @ex_intro
 107   [| % [ % | % // #ls #c #rs #H destruct ] ]
 108 |#a #al @ex_intro
 109   [| % [ % | % // #ls #c #rs #H destruct ] ]
 110 |#a #al @ex_intro
 111   [| % [ % | % // #ls #c #rs #H destruct ] ]
 112 | #ls #c #rs
 113   @ex_intro [| % [ % | % [whd in ⊢ ((??%?)→?); #H destruct]
 114   #ls1 #c1 #rs1 #H destruct cases ls1 // ] ] ]
 115 qed.
 116
 117 (* a slightly different move machine. *)
 118 definition smove_states ≝ initN 2.
 119
 120 definition smove0 : smove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
 121 definition smove1 : smove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
 122
 123 definition trans_smove ≝
 124  λsig,D.
 125  λp:smove_states × (option sig).
 126  let 〈q,a〉 ≝ p in match (pi1 … q) with
 127  [ O ⇒ 〈smove1,None sig, D〉
 128  | S _ ⇒ 〈smove1,None sig, N〉 ].
 129
 130 definition move ≝
 131   λsig,D.mk_TM sig smove_states (trans_smove sig D) smove0 (λq.q == smove1).
 132
 133 definition Rmove ≝
 134   λalpha,D,t1,t2. t2 = tape_move alpha t1 D.
 135
 136 lemma sem_move_single :
 137   ∀alpha,D.move alpha D ⊨ Rmove alpha D.
 138 #alpha #D #int %{2} %{(mk_config ? smove_states smove1 ?)} [| % % ]
 139 qed.
 140
 141 (********************************* test char **********************************)
 142
 143 (* the test_char machine ends up in two different states q1 and q2 wether or not
 144 the current character satisfies a boolean test function passed as a parameter to
 145 the machine.
 146 The machine ends up in q1 also in case there is no current character.
 147 *)
 148
 149 definition tc_states ≝ initN 3.
 150
 151 definition tc_start : tc_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
 152 definition tc_true : tc_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
 153 definition tc_false : tc_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
 154
 155 definition test_char ≝
 156   λalpha:FinSet.λtest:alpha→bool.
 157   mk_TM alpha tc_states
 158   (λp.let 〈q,a〉 ≝ p in
 159    match a with
 160    [ None ⇒ 〈tc_false, None ?,N〉
 161    | Some a' ⇒
 162      match test a' with
 163      [ true ⇒ 〈tc_true,None ?,N〉
 164      | false ⇒ 〈tc_false,None ?,N〉 ]])
 165   tc_start (λx.notb (x == tc_start)).
 166
 167 definition Rtc_true ≝
 168   λalpha,test,t1,t2.
 169    (∃c. current alpha t1 = Some ? c ∧ test c = true) ∧ t2 = t1.
 170
 171 definition Rtc_false ≝
 172   λalpha,test,t1,t2.
 173     (∀c. current alpha t1 = Some ? c → test c = false) ∧ t2 = t1.
 174
 175 lemma tc_q0_q1 :
 176   ∀alpha,test,ls,a0,rs. test a0 = true →
 177   step alpha (test_char alpha test)
 178     (mk_config ?? tc_start (midtape … ls a0 rs)) =
 179   mk_config alpha (states ? (test_char alpha test)) tc_true
 180     (midtape … ls a0 rs).
 181 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
 182 whd in match (trans … 〈?,?〉); >Htest %
 183 qed.
 184
 185 lemma tc_q0_q2 :
 186   ∀alpha,test,ls,a0,rs. test a0 = false →
 187   step alpha (test_char alpha test)
 188     (mk_config ?? tc_start (midtape … ls a0 rs)) =
 189   mk_config alpha (states ? (test_char alpha test)) tc_false
 190     (midtape … ls a0 rs).
 191 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
 192 whd in match (trans … 〈?,?〉); >Htest %
 193 qed.
 194
 195 lemma sem_test_char :
 196   ∀alpha,test.
 197   accRealize alpha (test_char alpha test)
 198     tc_true (Rtc_true alpha test) (Rtc_false alpha test).
 199 #alpha #test *
 200 [ @(ex_intro ?? 2)
 201   @(ex_intro ?? (mk_config ?? tc_false (niltape ?))) %
 202   [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
 203 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_false (leftof ? a al)))
 204   % [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
 205 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_false (rightof ? a al)))
 206   % [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
 207 | #ls #c #rs @(ex_intro ?? 2)
 208   cases (true_or_false (test c)) #Htest
 209   [ @(ex_intro ?? (mk_config ?? tc_true ?))
 210     [| %
 211       [ %
 212         [ whd in ⊢ (??%?); >tc_q0_q1 //
 213         | #_ % // @(ex_intro … c) /2/]
 214       | * #Hfalse @False_ind @Hfalse % ]
 215     ]
 216   | @(ex_intro ?? (mk_config ?? tc_false (midtape ? ls c rs)))
 217     %
 218     [ %
 219       [ whd in ⊢ (??%?); >tc_q0_q2 //
 220       | whd in ⊢ ((??%%)→?); #Hfalse destruct (Hfalse) ]
 221     | #_ % // #c0 whd in ⊢ ((??%?)→?); #Hc0 destruct (Hc0) //
 222     ]
 223   ]
 224 ]
 225 qed.
 226
 227 lemma test_char_inv :
 228   ∀sig.∀P:tape sig → Prop.∀f,t,t0.P t → Rtc_true sig f t t0 → P t0.
 229 #sig #P #f #t #t0 #HPt * #_ //
 230 qed.
 231
 232 definition test_null ≝ λalpha.test_char alpha (λ_.true).
 233
 234 definition R_test_null_true ≝ λalpha,t1,t2.
 235   current alpha t1 ≠ None ? ∧ t1 = t2.
 236
 237 definition R_test_null_false ≝ λalpha,t1,t2.
 238   current alpha t1 = None ? ∧ t1 = t2.
 239
 240 lemma sem_test_null : ∀alpha.
 241   test_null alpha ⊨ [ tc_true : R_test_null_true alpha, R_test_null_false alpha].
 242 #alpha #t1 cases (sem_test_char alpha (λ_.true) t1) #k * #outc * * #Hloop #Htrue
 243 #Hfalse %{k} %{outc} % [ %
 244 [ @Hloop
 245 | #Houtc cases (Htrue ?) [| @Houtc] * #c * #Hcurt1 #_ #Houtc1 %
 246   [ >Hcurt1 % #H destruct (H) | <Houtc1 % ] ]
 247 | #Houtc cases (Hfalse ?) [| @Houtc] #Habsurd #Houtc %
 248   [ cases (current alpha t1) in Habsurd; // #c1 #Habsurd
 249     lapply (Habsurd ? (refl ??)) #H destruct (H)
 250   | <Houtc % ] ]
 251 qed.
 252
 253 (************************************* swap ***********************************)
 254 definition swap_states : FinSet → FinSet ≝
 255   λalpha:FinSet.FinProd (initN 4) alpha.
 256
 257 definition swap0 : initN 4 ≝ mk_Sig ?? 0 (leb_true_to_le 1 4 (refl …)).
 258 definition swap1 : initN 4 ≝ mk_Sig ?? 1 (leb_true_to_le 2 4 (refl …)).
 259 definition swap2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)).
 260 definition swap3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)).
 261
 262 definition swap_r ≝
 263  λalpha:FinSet.λfoo:alpha.
 264  mk_TM alpha (swap_states alpha)
 265  (λp.let 〈q,a〉 ≝ p in
 266   let 〈q',b〉 ≝ q in
 267   let q' ≝ pi1 nat (λi.i<4) q' in
 268   match a with
 269   [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
 270   | Some a' ⇒
 271   match q' with
 272   [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? a',R〉  (* save in register and move R *)
 273   | S q' ⇒ match q' with
 274     [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? b,L〉 (* swap with register and move L *)
 275     | S q' ⇒ match q' with
 276       [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
 277       | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
 278       ]
 279     ]
 280   ]])
 281   〈swap0,foo〉
 282   (λq.\fst q == swap3).
 283
 284 definition Rswap_r ≝
 285   λalpha,t1,t2.
 286     (∀b,ls.
 287       t1 = midtape alpha ls b [ ] →
 288       t2 = rightof ? b ls) ∧
 289     (∀a,b,ls,rs.
 290       t1 = midtape alpha ls b (a::rs) →
 291       t2 = midtape alpha ls a (b::rs)).
 292
 293 lemma sem_swap_r : ∀alpha,foo.
 294   swap_r alpha foo ⊨ Rswap_r alpha.
 295 #alpha #foo *
 296   [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
 297    % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
 298   |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
 299    % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
 300   |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
 301    % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
 302   | #lt #c #rt @(ex_intro ?? 4) cases rt
 303     [@ex_intro [|% [ % | %
 304       [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
 305     |#r0 #rt0 @ex_intro [| % [ % | %
 306       [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
 307     ]
 308   ]
 309 qed.
 310
 311 definition swap_l ≝
 312  λalpha:FinSet.λfoo:alpha.
 313  mk_TM alpha (swap_states alpha)
 314  (λp.let 〈q,a〉 ≝ p in
 315   let 〈q',b〉 ≝ q in
 316   let q' ≝ pi1 nat (λi.i<4) q' in
 317   match a with
 318   [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
 319   | Some a' ⇒
 320   match q' with
 321   [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? a',L〉  (* save in register and move L *)
 322   | S q' ⇒ match q' with
 323     [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? b,R〉 (* swap with register and move R *)
 324     | S q' ⇒ match q' with
 325       [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
 326       | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
 327       ]
 328     ]
 329   ]])
 330   〈swap0,foo〉
 331   (λq.\fst q == swap3).
 332
 333 definition Rswap_l ≝
 334   λalpha,t1,t2.
 335    (∀b,rs.
 336      t1 = midtape alpha [ ] b rs →
 337      t2 = leftof ? b rs) ∧
 338    (∀a,b,ls,rs.
 339       t1 = midtape alpha (a::ls) b rs →
 340       t2 = midtape alpha (b::ls) a rs).
 341
 342 lemma sem_swap_l : ∀alpha,foo.
 343   swap_l alpha foo ⊨ Rswap_l alpha.
 344 #alpha #foo *
 345   [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
 346    % [% |% [#b #rs | #a #b #ls #rs] #H destruct]
 347   |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
 348    % [% | % [#b #rs | #a #b #ls #rs] #H destruct]
 349   |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
 350    % [% |% [#b #rs | #a #b #ls #rs] #H destruct]
 351   | #lt #c #rt @(ex_intro ?? 4) cases lt
 352     [@ex_intro [|% [ % | %
 353       [#b #rs #H destruct normalize // |#a #b #ls #rs #H destruct]]]
 354     |#r0 #rt0 @ex_intro [| % [ % | %
 355       [#b #rs #H destruct | #a #b #ls #rs #H destruct normalize //
 356     ]
 357   ]
 358 qed.
 359
 360 (********************************** combine ***********************************)
 361 (* replace the content x of a cell with a combiation f(x,y) of x and the content
 362 y of the adiacent cell *)
 363
 364 definition combf_states : FinSet → FinSet ≝
 365   λalpha:FinSet.FinProd (initN 4) alpha.
 366
 367 definition combf0 : initN 4 ≝ mk_Sig ?? 0 (leb_true_to_le 1 4 (refl …)).
 368 definition combf1 : initN 4 ≝ mk_Sig ?? 1 (leb_true_to_le 2 4 (refl …)).
 369 definition combf2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)).
 370 definition combf3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)).
 371
 372 definition combf_r ≝
 373  λalpha:FinSet.λf.λfoo:alpha.
 374  mk_TM alpha (combf_states alpha)
 375  (λp.let 〈q,a〉 ≝ p in
 376   let 〈q',b〉 ≝ q in
 377   let q' ≝ pi1 nat (λi.i<4) q' in
 378   match a with
 379   [ None ⇒ 〈〈combf3,foo〉,None ?,N〉 (* if tape is empty then stop *)
 380   | Some a' ⇒
 381   match q' with
 382   [ O ⇒ (* q0 *) 〈〈combf1,a'〉,Some ? a',R〉  (* save in register and move R *)
 383   | S q' ⇒ match q' with
 384     [ O ⇒ (* q1 *) 〈〈combf2,f b a'〉,Some ? a',L〉
 385       (* combine in register and move L *)
 386     | S q' ⇒ match q' with
 387       [ O ⇒ (* q2 *) 〈〈combf3,foo〉,Some ? b,R〉
 388         (* copy from register and move R *)
 389       | S q' ⇒ (* q3 *) 〈〈combf3,foo〉,None ?,N〉 (* final state *)
 390       ]
 391     ]
 392   ]])
 393   〈combf0,foo〉
 394   (λq.\fst q == combf3).
 395
 396 definition Rcombf_r ≝
 397   λalpha,f,t1,t2.
 398     (∀b,ls.
 399       t1 = midtape alpha ls b [ ] →
 400       t2 = rightof ? b ls) ∧
 401     (∀a,b,ls,rs.
 402       t1 = midtape alpha ls b (a::rs) →
 403       t2 = midtape alpha ((f b a)::ls) a rs).
 404
 405 lemma sem_combf_r : ∀alpha,f,foo.
 406   combf_r alpha f foo ⊨ Rcombf_r alpha f.
 407 #alpha #f #foo *
 408   [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (niltape ?)))
 409    % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
 410   |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (leftof ? l0 lt0)))
 411    % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
 412   |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (rightof ? r0 rt0)))
 413    % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
 414   | #lt #c #rt @(ex_intro ?? 4) cases rt
 415     [@ex_intro [|% [ % | %
 416       [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
 417     |#r0 #rt0 @ex_intro [| % [ % | %
 418       [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
 419     ]
 420   ]
 421 qed.
 422
 423 definition combf_l ≝
 424  λalpha:FinSet.λf.λfoo:alpha.
 425  mk_TM alpha (combf_states alpha)
 426  (λp.let 〈q,a〉 ≝ p in
 427   let 〈q',b〉 ≝ q in
 428   let q' ≝ pi1 nat (λi.i<4) q' in
 429   match a with
 430   [ None ⇒ 〈〈combf3,foo〉,None ?,N〉 (* if tape is empty then stop *)
 431   | Some a' ⇒
 432   match q' with
 433   [ O ⇒ (* q0 *) 〈〈combf1,a'〉,Some ? a',L〉  (* save in register and move R *)
 434   | S q' ⇒ match q' with
 435     [ O ⇒ (* q1 *) 〈〈combf2,f b a'〉,Some ? a',R〉
 436       (* combine in register and move L *)
 437     | S q' ⇒ match q' with
 438       [ O ⇒ (* q2 *) 〈〈combf3,foo〉,Some ? b,L〉
 439         (* copy from register and move R *)
 440       | S q' ⇒ (* q3 *) 〈〈combf3,foo〉,None ?,N〉 (* final state *)
 441       ]
 442     ]
 443   ]])
 444   〈combf0,foo〉
 445   (λq.\fst q == combf3).
 446
 447 definition Rcombf_l ≝
 448   λalpha,f,t1,t2.
 449     (∀b,rs.
 450       t1 = midtape alpha [ ] b rs →
 451       t2 = leftof ? b rs) ∧
 452     (∀a,b,ls,rs.
 453       t1 = midtape alpha (a::ls) b rs →
 454       t2 = midtape alpha ls a ((f b a)::rs)).
 455
 456 lemma sem_combf_l : ∀alpha,f,foo.
 457   combf_l alpha f foo ⊨ Rcombf_l alpha f.
 458 #alpha #f #foo *
 459   [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (niltape ?)))
 460    % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
 461   |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (leftof ? l0 lt0)))
 462    % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
 463   |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (rightof ? r0 rt0)))
 464    % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
 465   | #lt #c #rt @(ex_intro ?? 4) cases lt
 466     [@ex_intro [|% [ % | %
 467       [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
 468     |#r0 #rt0 @ex_intro [| % [ % | %
 469       [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
 470     ]
 471   ]
 472 qed.
 473
 474 (********************************* new_combine ********************************)
 475 (* replace the content x of a cell with a combiation f(x,y) of x and the content
 476 y of the adiacent cell; if there is no adjacent cell, combines with a default
 477 value foo *)
 478
 479 definition ncombf_r ≝
 480  λalpha:FinSet.λf.λfoo:alpha.
 481  mk_TM alpha (combf_states alpha)
 482  (λp.let 〈q,a〉 ≝ p in
 483   let 〈q',b〉 ≝ q in
 484   let q' ≝ pi1 nat (λi.i<4) q' in
 485   match a with
 486   [ None ⇒ if (eqb q' 1)then (* if on right cell, combine in register and move L *)
 487            〈〈combf2,f b foo〉,None ?,L〉
 488            else 〈〈combf3,foo〉,None ?,N〉 (* else stop *)
 489   | Some a' ⇒
 490   match q' with
 491   [ O ⇒ (* q0 *) 〈〈combf1,a'〉,Some ? a',R〉  (* save in register and move R *)
 492   | S q' ⇒ match q' with
 493     [ O ⇒ (* q1 *) 〈〈combf2,f b a'〉,Some ? a',L〉
 494       (* combine in register and move L *)
 495     | S q' ⇒ match q' with
 496       [ O ⇒ (* q2 *) 〈〈combf3,foo〉,Some ? b,R〉
 497         (* copy from register and move R *)
 498       | S q' ⇒ (* q3 *) 〈〈combf3,foo〉,None ?,N〉 (* final state *)
 499       ]
 500     ]
 501   ]])
 502   〈combf0,foo〉
 503   (λq.\fst q == combf3).
 504
 505 definition Rncombf_r ≝
 506   λalpha,f,foo,t1,t2.
 507     (∀b,ls.
 508       t1 = midtape alpha ls b [ ] →
 509       t2 = rightof ? (f b foo) ls) ∧
 510     (∀a,b,ls,rs.
 511       t1 = midtape alpha ls b (a::rs) →
 512       t2 = midtape alpha ((f b a)::ls) a rs).
 513
 514 lemma sem_ncombf_r : ∀alpha,f,foo.
 515   ncombf_r alpha f foo ⊨ Rncombf_r alpha f foo.
 516 #alpha #f #foo *
 517   [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (niltape ?)))
 518    % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
 519   |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (leftof ? l0 lt0)))
 520    % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
 521   |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (rightof ? r0 rt0)))
 522    % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
 523   | #lt #c #rt @(ex_intro ?? 4) cases rt
 524     [@ex_intro [|% [ % | %
 525       [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
 526     |#r0 #rt0 @ex_intro [| % [ % | %
 527       [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
 528     ]
 529   ]
 530 qed.
 531
 532 definition ncombf_l ≝
 533  λalpha:FinSet.λf.λfoo:alpha.
 534  mk_TM alpha (combf_states alpha)
 535  (λp.let 〈q,a〉 ≝ p in
 536   let 〈q',b〉 ≝ q in
 537   let q' ≝ pi1 nat (λi.i<4) q' in
 538   match a with
 539   [ None ⇒ if (eqb q' 1)then
 540            (* if on left cell, combine in register and move R *)
 541            〈〈combf2,f b foo〉,None ?,R〉
 542            else 〈〈combf3,foo〉,None ?,N〉 (* else stop *)
 543   | Some a' ⇒
 544   match q' with
 545   [ O ⇒ (* q0 *) 〈〈combf1,a'〉,Some ? a',L〉  (* save in register and move R *)
 546   | S q' ⇒ match q' with
 547     [ O ⇒ (* q1 *) 〈〈combf2,f b a'〉,Some ? a',R〉
 548       (* combine in register and move L *)
 549     | S q' ⇒ match q' with
 550       [ O ⇒ (* q2 *) 〈〈combf3,foo〉,Some ? b,L〉
 551         (* copy from register and move R *)
 552       | S q' ⇒ (* q3 *) 〈〈combf3,foo〉,None ?,N〉 (* final state *)
 553       ]
 554     ]
 555   ]])
 556   〈combf0,foo〉
 557   (λq.\fst q == combf3).
 558
 559 definition Rncombf_l ≝
 560   λalpha,f,foo,t1,t2.
 561     (∀b,rs.
 562       t1 = midtape alpha [ ] b rs →
 563       t2 = leftof ? (f b foo) rs) ∧
 564     (∀a,b,ls,rs.
 565       t1 = midtape alpha (a::ls) b rs →
 566       t2 = midtape alpha ls a ((f b a)::rs)).
 567
 568 lemma sem_ncombf_l : ∀alpha,f,foo.
 569   ncombf_l alpha f foo ⊨ Rncombf_l alpha f foo.
 570 #alpha #f #foo *
 571   [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (niltape ?)))
 572    % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
 573   |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (leftof ? l0 lt0)))
 574    % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
 575   |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (rightof ? r0 rt0)))
 576    % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
 577   | #lt #c #rt @(ex_intro ?? 4) cases lt
 578     [@ex_intro [|% [ % | %
 579       [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
 580     |#r0 #rt0 @ex_intro [| % [ % | %
 581       [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
 582     ]
 583   ]
 584 qed.