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