matita/matita/lib/turing/universal/move_tape.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_____________________________________________________________*)
  11
  12 include "turing/universal/move_char_c.ma".
  13 include "turing/universal/move_char_l.ma".
  14 include "turing/universal/tuples.ma".
  15
  16 definition init_cell_states ≝ initN 2.
  17
  18 definition ics0 : init_cell_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
  19 definition ics1 : init_cell_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
  20
  21 d
  22 definition init_cell ≝
  23  mk_TM STape init_cell_states
  24  (λp.let 〈q,a〉 ≝ p in
  25   match pi1 … q with
  26   [ O ⇒ match a with
  27     [ None ⇒ 〈ics1, Some ? 〈〈null,false〉,N〉〉
  28     | Some _ ⇒ 〈1, None ?〉 ]
  29   | S _ ⇒ 〈ics1,None ?〉 ])
  30  ics0 (λq.q == ics1).
  31
  32 definition R_init_cell ≝ λt1,t2.
  33  (∃c.current STape t1 = Some ? c ∧ t2 = t1) ∨
  34  (current STape t1 = None ? ∧ t2 = midtape ? (left ? t1) 〈null,false〉 (right ? t1)).
  35
  36 axiom sem_init_cell : Realize ? init_cell R_init_cell.
  37
  38 definition swap_states : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 4) alpha.
  39
  40 definition swap ≝
  41  λalpha:FinSet.λd:alpha.
  42  mk_TM alpha (mcl_states alpha)
  43  (λp.let 〈q,a〉 ≝ p in
  44   let 〈q',b〉 ≝ q in
  45   match a with
  46   [ None ⇒ 〈〈3,d〉,None ?〉
  47   | Some a' ⇒
  48   match q' with
  49   [ O ⇒ (* qinit *)
  50      〈〈1,a'〉,Some ? 〈a',R〉〉
  51   | S q' ⇒ match q' with
  52     [ O ⇒ (* q1 *)
  53       〈〈2,a'〉,Some ? 〈b,L〉〉
  54     | S q' ⇒ match q' with
  55       [ O ⇒ (* q2 *)
  56         〈〈3,d〉,Some ? 〈b,N〉〉
  57       | S _⇒ (* qacc *)
  58           〈〈3,d〉,None ?〉 ] ] ] ])
  59   〈0,d〉
  60   (λq.let 〈q',a〉 ≝ q in q' == 3).
  61
  62 definition R_swap ≝
  63   λalpha,t1,t2.
  64    ∀a,b,ls,rs.
  65     t1 = midtape alpha ls b (a::rs) →
  66     t2 = midtape alpha ls a (b::rs).
  67
  68 (*
  69 lemma swap_q0_q1 :
  70   ∀alpha:FinSet.∀d,a,ls,a0,rs.
  71   step alpha (swap alpha d)
  72     (mk_config ?? 〈0,a〉 (mk_tape … ls (Some ? a0) rs)) =
  73   mk_config alpha (states ? (swap alpha d)) 〈1,a0〉
  74     (tape_move_right alpha ls a0 rs).
  75 #alpha #d #a *
  76 [ #a0 #rs %
  77 | #a1 #ls #a0 #rs %
  78 ]
  79 qed.
  80
  81 lemma swap_q1_q2 :
  82   ∀alpha:FinSet.∀d,a,ls,a0,rs.
  83   step alpha (swap alpha d)
  84     (mk_config ?? 〈1,a〉 (mk_tape … ls (Some ? a0) rs)) =
  85   mk_config alpha (states ? (swap alpha d)) 〈2,a0〉
  86     (tape_move_left alpha ls a rs).
  87 #alpha #sep #a #ls #a0 * //
  88 qed.
  89
  90 lemma swap_q2_q3 :
  91   ∀alpha:FinSet.∀d,a,ls,a0,rs.
  92   step alpha (swap alpha d)
  93     (mk_config ?? 〈2,a〉 (mk_tape … ls (Some ? a0) rs)) =
  94   mk_config alpha (states ? (swap alpha d)) 〈3,d〉
  95     (tape_move_left alpha ls a rs).
  96 #alpha #sep #a #ls #a0 * //
  97 qed.
  98 *)
  99
 100 lemma sem_swap :
 101   ∀alpha,d.
 102   Realize alpha (swap alpha d) (R_swap alpha).
 103 #alpha #d #tapein @(ex_intro ?? 4) cases tapein
 104 [ @ex_intro [| % [ % | #a #b #ls #rs #Hfalse destruct (Hfalse) ] ]
 105 | #a #al @ex_intro [| % [ % | #a #b #ls #rs #Hfalse destruct (Hfalse) ] ]
 106 | #a #al @ex_intro [| % [ % | #a #b #ls #rs #Hfalse destruct (Hfalse) ] ]
 107 | #ls #c #rs cases rs
 108   [ @ex_intro [| % [ % | #a #b #ls0 #rs0 #Hfalse destruct (Hfalse) ] ]
 109   | -rs #r #rs @ex_intro
 110     [|%
 111      [%
 112      | #r0 #c0 #ls0 #rs0 #Htape destruct (Htape) normalize cases ls0
 113        [% | #l1 #ls1 %] ] ] ] ]
 114 qed.
 115
 116 axiom ssem_move_char_l :
 117   ∀alpha,sep.
 118   Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).
 119
 120 (*
 121 MOVE TAPE RIGHT:
 122
 123   ls # current c # table # d? rs
 124                      ^
 125   ls # current c # table # d? rs init
 126                          ^
 127   ls # current c # table # d? rs
 128                            ^
 129   ls # current c # table # d rs ----------------------
 130                            ^     move_l
 131   ls # current c # table # d rs
 132                          ^       swap
 133   ls # current c # table d # rs --------------------
 134                          ^
 135   ls # current c # table d # rs
 136                        ^
 137   ls # current c # d table # rs  sub1
 138                    ^
 139   ls # current c # d table # rs
 140                  ^
 141   ls # current c d # table # rs -------------------
 142                  ^               move_l
 143   ls # current c d # table # rs -------------------
 144                ^
 145   ls # current c d # table # rs
 146              ^
 147   ls # c current d # table # rs  sub1
 148        ^
 149   ls # c current d # table # rs
 150      ^
 151   ls c # current d # table # rs ------------------
 152      ^
 153
 154 (move_to_grid_r;)
 155 move_r;
 156 init_cell;
 157 move_l;
 158 swap;
 159
 160 move_l;
 161 move_char_l;
 162 ---------move_l;
 163 swap;
 164
 165 move_l;
 166
 167 move_l;
 168 move_char_l;
 169 ---------move_l;
 170 swap
 171 *)
 172
 173 (* l1 # l2 r  ---> l1 r # l2
 174            ^          ^
 175  *)
 176 definition mtr_aux ≝
 177   seq ? (move_l …) (seq ? (move_char_l STape 〈grid,false〉)
 178    (swap STape 〈grid,false〉)).
 179 definition R_mtr_aux ≝ λt1,t2.
 180   ∀l1,l2,l3,r. t1 = midtape STape (l2@〈grid,false〉::l1) r l3 → no_grids l2 →
 181   t2 = midtape STape l1 r (〈grid,false〉::reverse ? l2@l3).
 182
 183 lemma sem_mtr_aux : Realize ? mtr_aux R_mtr_aux.
 184 #intape
 185 cases (sem_seq … (sem_move_l …) (sem_seq … (ssem_move_char_l STape 〈grid,false〉)
 186         (sem_swap STape 〈grid,false〉)) intape)
 187 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc)  % [@Hloop] -Hloop
 188 #l1 #l2 #l3  #r #Hintape #Hl2
 189 cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta #Hta
 190 * #tb * whd in ⊢(%→?); generalize in match Hta; -Hta cases l2 in Hl2;
 191 [ #_ #Hta #Htb lapply (Htb … Hta) -Htb * #Htb lapply (Htb (refl ??)) -Htb #Htb #_
 192   whd in ⊢(%→?); >Htb #Houtc lapply (Houtc … Hta) -Houtc #Houtc @Houtc
 193 | #c0 #l0 #Hnogrids #Hta #Htb lapply (Htb … Hta) -Htb * #_ #Htb
 194     lapply (Htb … (refl ??) ??)
 195     [ cases (true_or_false (memb STape 〈grid,false〉 l0)) #Hmemb
 196       [ @False_ind lapply (Hnogrids 〈grid,false〉 ?)
 197         [ @memb_cons // | normalize #Hfalse destruct (Hfalse) ]
 198       | @Hmemb ]
 199     | % #Hc0 lapply (Hnogrids c0 ?)
 200       [ @memb_hd | >Hc0 normalize #Hfalse destruct (Hfalse) ]
 201     | #Htb whd in ⊢(%→?); >Htb #Houtc lapply (Houtc … (refl ??)) -Houtc #Houtc
 202       >reverse_cons >associative_append @Houtc
 203 ]]
 204 qed.
 205
 206 definition move_tape_r ≝
 207   seq ? (move_r …) (seq ? init_cell (seq ? (move_l …)
 208    (seq ? (swap STape 〈grid,false〉)
 209      (seq ? mtr_aux (seq ? (move_l …) (seq ? mtr_aux (move_r …))))))).
 210
 211 definition R_move_tape_r ≝ λt1,t2.
 212   ∀rs,n,table,c0,bc0,curconfig,ls0.
 213   bit_or_null c0 = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) →
 214   t1 = midtape STape (table@〈grid,false〉::〈c0,bc0〉::curconfig@〈grid,false〉::ls0)
 215          〈grid,false〉 rs →
 216   (rs = [] ∧
 217    t2 = midtape STape (〈c0,bc0〉::ls0) 〈grid,false〉 (reverse STape curconfig@〈null,false〉::
 218                              〈grid,false〉::reverse STape table@[〈grid,false〉])) ∨
 219   (∃r0,rs0.rs = r0::rs0 ∧
 220    t2 = midtape STape (〈c0,bc0〉::ls0) 〈grid,false〉 (reverse STape curconfig@r0::
 221                              〈grid,false〉::reverse STape table@〈grid,false〉::rs0)).
 222
 223 lemma sem_move_tape_r : Realize ? move_tape_r R_move_tape_r.
 224 #tapein
 225 cases (sem_seq …(sem_move_r …) (sem_seq … sem_init_cell (sem_seq … (sem_move_l …)
 226    (sem_seq … (sem_swap STape 〈grid,false〉) (sem_seq … sem_mtr_aux
 227      (sem_seq … (sem_move_l …) (sem_seq … sem_mtr_aux (sem_move_r …))))))) tapein)
 228 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
 229 #rs #n #table #c0 #bc0 #curconfig #ls0 #Hbitnullc0 #Hbitnullcc #Htable #Htapein
 230 cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Htapein) -Hta #Hta
 231 * #tb * whd in ⊢ (%→?); *
 232 [ * #r0 *
 233   generalize in match Hta; generalize in match Htapein; -Htapein -Hta cases rs
 234   [ #_ #Hta >Hta normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
 235   #r1 #rs1 #Htapein #Hta change with (midtape ?? r1 rs1) in Hta:(???%); >Hta
 236   #Hr0 whd in Hr0:(??%?); #Htb * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc #Htc
 237   * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd #Htd
 238   * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?) [ (*memb_reverse @(no_grids_in_table … Htable)*) @daemon ] -Hte #Hte
 239   * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf #Htf
 240   * #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?) [ #x #Hx @bit_or_null_not_grid @Hbitnullcc // ] -Htg #Htg
 241   whd in ⊢ (%→?); #Houtc lapply (Houtc … Htg) -Houtc #Houtc
 242   %2 @(ex_intro ?? r1) @(ex_intro ?? rs1) % [%] @Houtc
 243 | * generalize in match Hta; generalize in match Htapein; -Htapein -Hta cases rs
 244   [|#r1 #rs1 #_ #Hta >Hta normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
 245   #Htapein #Hta change with (rightof ???) in Hta:(???%); >Hta
 246   #Hr0 whd in Hr0:(??%?); #Htb * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc #Htc
 247   * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd #Htd
 248   * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?) [(*same as above @(no_grids_in_table … Htable) *) @daemon ] -Hte #Hte
 249   * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf #Htf
 250   * #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?) [ #x #Hx @bit_or_null_not_grid @Hbitnullcc // ] -Htg #Htg
 251   whd in ⊢ (%→?); #Houtc lapply (Houtc … Htg) -Houtc #Houtc
 252   % % [% | @Houtc ]
 253 qed.
 254
 255 (*
 256 MOVE TAPE LEFT:
 257
 258   ls # current c # table # d rs
 259                      ^
 260   ls # current c # table # d rs
 261                          ^
 262   ls # current c # table d # rs
 263                        ^
 264   ls # current c # d table # rs
 265                    ^
 266   ls # current c # d table # rs
 267                  ^
 268   ls # current c d # table # rs
 269                ^
 270   ls # current c d # table # rs
 271              ^
 272   ls # c current c # table # rs
 273        ^
 274   ls # c current c # table # rs
 275      ^
 276   ls c # current c # table # rs
 277      ^
 278
 279 move_to_grid_r;
 280 swap;
 281 move_char_l;
 282 move_l;
 283 swap;
 284 move_l;
 285 move_char_l;
 286 move_l;
 287 swap
 288 *)
 289 axiom move_tape_l : TM STape.
 290 (*  seq ? (move_r …) (seq ? init_cell (seq ? (move_l …)
 291    (seq ? (swap STape 〈grid,false〉)
 292      (seq ? mtr_aux (seq ? (move_l …) mtr_aux))))). *)
 293
 294 definition R_move_tape_l ≝ λt1,t2.
 295   ∀rs,n,table,c0,bc0,curconfig,ls0.
 296   bit_or_null c0 = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) →
 297   t1 = midtape STape (table@〈grid,false〉::〈c0,bc0〉::curconfig@〈grid,false〉::ls0)
 298          〈grid,false〉 rs →
 299   (ls0 = [] ∧
 300    t2 = midtape STape [] 〈grid,false〉
 301          (reverse ? curconfig@〈null,false〉::〈grid,false〉::reverse ? table@〈grid,false〉::〈c0,bc0〉::rs)) ∨
 302   (∃l1,ls1. ls0 = l1::ls1 ∧
 303    t2 = midtape STape ls1 〈grid,false〉
 304          (reverse ? curconfig@l1::〈grid,false〉::reverse ? table@〈grid,false〉::〈c0,bc0〉::rs)).
 305
 306 axiom sem_move_tape_l : Realize ? move_tape_l R_move_tape_l.
 307
 308 (*
 309            by cases on current:
 310              case bit false: move_tape_l
 311              case bit true: move_tape_r
 312              case null: adv_to_grid_l; move_l; adv_to_grid_l;
 313 *)
 314
 315 definition lift_tape ≝ λls,c,rs.
 316   let 〈c0,b〉 ≝ c in
 317   let c' ≝ match c0 with
 318   [ null ⇒ None ?
 319   | _ ⇒ Some ? c ]
 320   in
 321   mk_tape STape ls c' rs.
 322
 323 definition sim_current_of_tape ≝ λt.
 324   match current STape t with
 325   [ None ⇒ 〈null,false〉
 326   | Some c0 ⇒ c0 ].
 327
 328
 329 definition move_of_unialpha ≝
 330   λc.match c with
 331   [ bit x ⇒ match x with [ true ⇒ R | false ⇒ L ]
 332   | _ ⇒ N ].
 333
 334 definition R_uni_step ≝ λt1,t2.
 335   ∀n,table,c,c1,ls,rs,curs,curc,news,newc,mv.
 336   table_TM n table →
 337   match_in_table n (〈c,false〉::curs) 〈curc,false〉
 338     (〈c1,false〉::news) 〈newc,false〉 〈mv,false〉 table →
 339   t1 = midtape STape (〈grid,false〉::ls) 〈c,false〉
 340     (curs@〈curc,false〉::〈grid,false〉::table@〈grid,false〉::rs) →
 341   ∀t1',ls1,rs1.t1' = lift_tape ls 〈curc,false〉 rs →
 342   (t2 = midtape STape (〈grid,false〉::ls1) 〈c1,false〉
 343     (news@〈newc,false〉::〈grid,false〉::table@〈grid,false〉::rs1) ∧
 344    lift_tape ls1 〈newc,false〉 rs1 =
 345    tape_move STape t1' (Some ? 〈〈newc,false〉,move_of_unialpha mv〉)).
 346
 347 definition no_nulls ≝
 348  λl:list STape.∀x.memb ? x l = true → is_null (\fst x) = false.
 349
 350 definition current_of_alpha ≝ λc:STape.
 351   match \fst c with [ null ⇒ None ? | _ ⇒ Some ? c ].
 352
 353 (*
 354    no_marks (c::ls@rs)
 355    only_bits (ls@rs)
 356    bit_or_null c
 357
 358 *)
 359 definition legal_tape ≝ λls,c,rs.
 360  no_marks (c::ls@rs) ∧ only_bits (ls@rs) ∧ bit_or_null (\fst c) = true ∧
 361  (\fst c ≠ null ∨ ls = [] ∨ rs = []).
 362
 363 lemma legal_tape_left :
 364   ∀ls,c,rs.legal_tape ls c rs →
 365   left ? (mk_tape STape ls (current_of_alpha c) rs) = ls.
 366 #ls * #c #bc #rs * * * #_ #_ #_ *
 367 [ *
 368   [ cases c
 369     [ #c' #_ %
 370     | * #Hfalse @False_ind /2/
 371     |*: #_ % ]
 372   | #Hls >Hls cases c // cases rs //
 373   ]
 374 | #Hrs >Hrs cases c // cases ls //
 375 ]
 376 qed.
 377
 378 axiom legal_tape_current :
 379   ∀ls,c,rs.legal_tape ls c rs →
 380   current ? (mk_tape STape ls (current_of_alpha c) rs) = current_of_alpha c.
 381
 382 axiom legal_tape_right :
 383   ∀ls,c,rs.legal_tape ls c rs →
 384   right ? (mk_tape STape ls (current_of_alpha c) rs) = rs.
 385
 386 (*
 387 lemma legal_tape_cases :
 388   ∀ls,c,rs.legal_tape ls c rs →
 389   \fst c ≠ null ∨ (\fst c = null ∧ (ls = [] ∨ rs = [])).
 390 #ls #c #rs cases c #c0 #bc0 cases c0
 391 [ #c1 normalize #_ % % #Hfalse destruct (Hfalse)
 392 | cases ls
 393   [ #_ %2 % // % %
 394   | #l0 #ls0 cases rs
 395     [ #_ %2 % // %2 %
 396     | #r0 #rs0 normalize * * #_ #Hrs destruct (Hrs) ]
 397   ]
 398 |*: #_ % % #Hfalse destruct (Hfalse) ]
 399 qed.
 400
 401 axiom legal_tape_conditions :
 402   ∀ls,c,rs.(\fst c ≠ null ∨ ls = [] ∨ rs = []) → legal_tape ls c rs.
 403 (*#ls #c #rs *
 404 [ *
 405   [ >(eq_pair_fst_snd ?? c) cases (\fst c)
 406     [ #c0 #Hc % % %
 407     | * #Hfalse @False_ind /2/
 408     |*: #Hc % % %
 409     ]
 410   | cases ls [ * #Hfalse @False_ind /2/ ]
 411     #l0 #ls0
 412
 413   #Hc
 414 *)
 415 *)
 416
 417 definition R_move_tape_r_abstract ≝ λt1,t2.
 418   ∀rs,n,table,curc,curconfig,ls.
 419   is_bit curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) →
 420   t1 = midtape STape (table@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls)
 421          〈grid,false〉 rs →
 422   legal_tape ls 〈curc,false〉 rs →
 423   ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs →
 424   ∃ls1,rs1,newc.
 425   (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉::
 426     〈grid,false〉::reverse ? table@〈grid,false〉::rs1) ∧
 427    lift_tape ls1 〈newc,false〉 rs1 =
 428    tape_move_right STape ls 〈curc,false〉 rs ∧ legal_tape ls1 〈newc,false〉 rs1).
 429
 430 lemma lift_tape_not_null :
 431   ∀ls,c,rs. is_null (\fst c) = false →
 432   lift_tape ls c rs = mk_tape STape ls (Some ? c) rs.
 433 #ls * #c0 #bc0 #rs cases c0
 434 [|normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
 435 //
 436 qed.
 437
 438 axiom bit_not_null :  ∀d.is_bit d = true → is_null d = false.
 439
 440 lemma mtr_concrete_to_abstract :
 441   ∀t1,t2.R_move_tape_r t1 t2 → R_move_tape_r_abstract t1 t2.
 442 #t1 #t2 whd in ⊢(%→?); #Hconcrete
 443 #rs #n #table #curc #curconfig #ls #Hbitcurc #Hcurconfig #Htable #Ht1
 444 * * * #Hnomarks #Hbits #Hcurc #Hlegal #t1' #Ht1'
 445 cases (Hconcrete … Htable Ht1) //
 446 [ * #Hrs #Ht2
 447   @(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? [])
 448   @(ex_intro ?? null) %
 449   [ %
 450     [ >Ht2 %
 451     | >Hrs % ]
 452   | % [ % [ %
 453     [ >append_nil #x #Hx cases (orb_true_l … Hx) #Hx'
 454       [ >(\P Hx') %
 455       | @Hnomarks @(memb_append_l1 … Hx') ]
 456     | >append_nil #x #Hx cases (orb_true_l … Hx) #Hx'
 457       [ >(\P Hx') //
 458       | @Hbits @(memb_append_l1 … Hx') ]]
 459     | % ]
 460     | %2 % ]
 461   ]
 462 | * * #r0 #br0 * #rs0 * #Hrs
 463   cut (br0 = false)
 464   [ @(Hnomarks 〈r0,br0〉) @memb_cons @memb_append_l2 >Hrs @memb_hd]
 465   #Hbr0 >Hbr0 in Hrs; #Hrs #Ht2
 466   @(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? rs0)
 467   @(ex_intro ?? r0) %
 468   [ %
 469     [ >Ht2  //
 470     | >Hrs >lift_tape_not_null
 471       [ %
 472       | @bit_not_null @(Hbits 〈r0,false〉) >Hrs @memb_append_l2 @memb_hd ] ]
 473   | % [ % [ %
 474     [ #x #Hx cases (orb_true_l … Hx) #Hx'
 475       [ >(\P Hx') %
 476       | cases (memb_append … Hx') #Hx'' @Hnomarks
 477         [ @(memb_append_l1 … Hx'')
 478         | >Hrs @memb_cons @memb_append_l2 @(memb_cons … Hx'') ]
 479       ]
 480     | whd in ⊢ (?%); #x #Hx cases (orb_true_l … Hx) #Hx'
 481       [ >(\P Hx') //
 482       | cases (memb_append … Hx') #Hx'' @Hbits
 483         [ @(memb_append_l1 … Hx'') | >Hrs @memb_append_l2 @(memb_cons … Hx'') ]
 484       ]]
 485     | whd in ⊢ (??%?); >(Hbits 〈r0,false〉) //
 486       @memb_append_l2 >Hrs @memb_hd ]
 487     | % % % #Hr0 lapply (Hbits 〈r0,false〉?)
 488       [ @memb_append_l2 >Hrs @memb_hd
 489       | >Hr0 normalize #Hfalse destruct (Hfalse)
 490       ] ] ] ]
 491 qed.
 492
 493 definition R_move_tape_l_abstract ≝ λt1,t2.
 494   ∀rs,n,table,curc,curconfig,ls.
 495   is_bit curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) →
 496   t1 = midtape STape (table@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls)
 497          〈grid,false〉 rs →
 498   legal_tape ls 〈curc,false〉 rs →
 499   ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs →
 500   ∃ls1,rs1,newc.
 501   (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉::
 502     〈grid,false〉::reverse ? table@〈grid,false〉::rs1) ∧
 503    lift_tape ls1 〈newc,false〉 rs1 =
 504    tape_move_left STape ls 〈curc,false〉 rs ∧ legal_tape ls1 〈newc,false〉 rs1).
 505
 506 lemma mtl_concrete_to_abstract :
 507   ∀t1,t2.R_move_tape_l t1 t2 → R_move_tape_l_abstract t1 t2.
 508 #t1 #t2 whd in ⊢(%→?); #Hconcrete
 509 #rs #n #table #curc #curconfig #ls #Hcurc #Hcurconfig #Htable #Ht1
 510 * * * #Hnomarks #Hbits #Hcurc #Hlegal #t1' #Ht1'
 511 cases (Hconcrete … Htable Ht1) //
 512 [ * #Hls #Ht2
 513   @(ex_intro ?? [])
 514   @(ex_intro ?? (〈curc,false〉::rs))
 515   @(ex_intro ?? null) %
 516   [ %
 517     [ >Ht2 %
 518     | >Hls % ]
 519   |  % [ % [ %
 520     [ #x #Hx cases (orb_true_l … Hx) #Hx'
 521       [ >(\P Hx') %
 522       | @Hnomarks >Hls @Hx' ]
 523     | #x #Hx cases (orb_true_l … Hx) #Hx'
 524       [ >(\P Hx') //
 525       | @Hbits >Hls @Hx' ]]
 526     | % ]
 527     | % %2 % ]
 528   ]
 529 | * * #l0 #bl0 * #ls0 * #Hls
 530   cut (bl0 = false)
 531   [ @(Hnomarks 〈l0,bl0〉) @memb_cons @memb_append_l1 >Hls @memb_hd]
 532   #Hbl0 >Hbl0 in Hls; #Hls #Ht2
 533   @(ex_intro ?? ls0) @(ex_intro ?? (〈curc,false〉::rs))
 534   @(ex_intro ?? l0) %
 535   [ %
 536     [ >Ht2 %
 537     | >Hls >lift_tape_not_null
 538       [ %
 539       | @bit_not_null @(Hbits 〈l0,false〉) >Hls @memb_append_l1 @memb_hd ] ]
 540   | % [ % [ %
 541     [ #x #Hx cases (orb_true_l … Hx) #Hx'
 542       [ >(\P Hx') %
 543       | cases (memb_append … Hx') #Hx'' @Hnomarks
 544         [ >Hls @memb_cons @memb_cons @(memb_append_l1 … Hx'')
 545         | cases (orb_true_l … Hx'') #Hx'''
 546           [ >(\P Hx''') @memb_hd
 547           | @memb_cons @(memb_append_l2 … Hx''')]
 548         ]
 549       ]
 550     | whd in ⊢ (?%); #x #Hx cases (memb_append … Hx) #Hx'
 551       [ @Hbits >Hls @memb_cons @(memb_append_l1 … Hx')
 552       | cases (orb_true_l … Hx') #Hx''
 553         [ >(\P Hx'') //
 554         | @Hbits @(memb_append_l2 … Hx'')
 555         ]]]
 556     | whd in ⊢ (??%?); >(Hbits 〈l0,false〉) //
 557       @memb_append_l1 >Hls @memb_hd ]
 558     | % % % #Hl0 lapply (Hbits 〈l0,false〉?)
 559       [ @memb_append_l1 >Hls @memb_hd
 560       | >Hl0 normalize #Hfalse destruct (Hfalse)
 561       ] ] ] ]
 562 qed.
 563
 564 lemma Realize_to_Realize :
 565   ∀alpha,M,R1,R2.(∀t1,t2.R1 t1 t2 → R2 t1 t2) → Realize alpha M R1 → Realize alpha M R2.
 566 #alpha #M #R1 #R2 #Himpl #HR1 #intape
 567 cases (HR1 intape) -HR1 #k * #outc * #Hloop #HR1
 568 @(ex_intro ?? k) @(ex_intro ?? outc) % /2/
 569 qed.
 570
 571 lemma sem_move_tape_l_abstract : Realize … move_tape_l R_move_tape_l_abstract.
 572 @(Realize_to_Realize … mtl_concrete_to_abstract) //
 573 qed.
 574
 575 lemma sem_move_tape_r_abstract : Realize … move_tape_r R_move_tape_r_abstract.
 576 @(Realize_to_Realize … mtr_concrete_to_abstract) //
 577 qed.
 578
 579 (*
 580  t1 =  ls # cs c # table # rs
 581
 582  let simt ≝ lift_tape ls c rs in
 583  let simt' ≝ move_left simt' in
 584
 585  t2 = left simt'# cs (sim_current_of_tape simt') # table # right simt'
 586 *)
 587
 588 (*
 589 definition R_move
 590
 591 definition R_exec_move ≝ λt1,t2.
 592   ∀ls,current,table1,newcurrent,table2,rs.
 593   t1 = midtape STape (current@〈grid,false〉::ls) 〈grid,false〉
 594        (table1@〈comma,true〉::newcurrent@〈comma,false〉::move::table2@
 595         〈grid,false〉::rs) →
 596   table_TM (table1@〈comma,false〉::newcurrent@〈comma,false〉::move::table2) →
 597   t2 = midtape
 598 *)
 599
 600 (*
 601
 602 step :
 603
 604 if is_true(current) (* current state is final *)
 605    then nop
 606    else
 607    init_match;
 608    match_tuple;
 609    if is_marked(current) = false (* match ok *)
 610       then exec_move;
 611       else sink;
 612
 613 *)
 614
 615
 616 definition move_tape ≝
 617   ifTM ? (test_char ? (λc:STape.c == 〈bit false,false〉))
 618     (* spostamento a sinistra: verificare se per caso non conviene spostarsi
 619        sulla prima grid invece dell'ultima *)
 620     (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c))) move_tape_l)
 621     (ifTM ? (test_char ? (λc:STape.c == 〈bit true,false〉))
 622        (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c))) move_tape_r)
 623        (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
 624           (seq ? (move_l …) (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))))
 625        tc_true) tc_true.
 626
 627 definition R_move_tape ≝ λt1,t2.
 628   ∀rs,n,table1,mv,table2,curc,curconfig,ls.
 629   bit_or_null mv = true → only_bits_or_nulls curconfig →
 630   (is_bit mv = true → is_bit curc = true) →
 631   table_TM n (reverse ? table1@〈mv,false〉::table2) →
 632   t1 = midtape STape (table1@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls)
 633          〈mv,false〉 (table2@〈grid,false〉::rs) →
 634   legal_tape ls 〈curc,false〉 rs →
 635   ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs →
 636   ∃ls1,rs1,newc.
 637   legal_tape ls1 〈newc,false〉 rs1 ∧
 638   (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉::
 639     〈grid,false〉::reverse ? table1@〈mv,false〉::table2@〈grid,false〉::rs1) ∧
 640    ((mv = bit false ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_left STape ls 〈curc,false〉 rs) ∨
 641     (mv = bit true ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_right STape ls 〈curc,false〉 rs) ∨
 642     (mv = null ∧ ls1 = ls ∧ rs1 = rs ∧ curc = newc))).
 643
 644 lemma sem_move_tape : Realize ? move_tape R_move_tape.
 645 #intape
 646 cases (sem_if ? (test_char ??) … tc_true (sem_test_char ? (λc:STape.c == 〈bit false,false〉))
 647         (sem_seq … (sem_adv_to_mark_r ? (λc:STape.is_grid (\fst c))) sem_move_tape_l_abstract)
 648         (sem_if ? (test_char ??) … tc_true (sem_test_char ? (λc:STape.c == 〈bit true,false〉))
 649         (sem_seq … (sem_adv_to_mark_r ? (λc:STape.is_grid (\fst c))) sem_move_tape_r_abstract)
 650         (sem_seq … (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
 651           (sem_seq … (sem_move_l …) (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c)))))) intape)
 652 #k * #outc * #Hloop #HR
 653 @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
 654 #rs #n #table1 #mv #table2 #curc #curconfig #ls
 655 #Hmv #Hcurconfig #Hmvcurc #Htable #Hintape #Htape #t1' #Ht1'
 656 generalize in match HR; -HR *
 657 [ * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈mv,false〉 ?)
 658   [| >Hintape % ] -Hta #Hceq #Hta lapply (\P Hceq) -Hceq #Hceq destruct (Hta Hceq)
 659   * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hintape) -Htb -Hintape
 660   [ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
 661   * #_ #Htb lapply (Htb … (refl ??) (refl ??) ?)
 662   [ @daemon ] -Htb >append_cons <associative_append #Htb
 663   whd in ⊢ (%→?); #Houtc lapply (Houtc … Htb … Ht1') //
 664   [ >reverse_append >reverse_append >reverse_reverse @Htable
 665   | /2/
 666   ||]
 667   -Houtc -Htb * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal
 668   @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) %
 669   [ //
 670   | %
 671     [ >Houtc >reverse_append >reverse_append >reverse_reverse
 672       >associative_append >associative_append %
 673     | % % % // ]
 674   ]
 675 | * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈mv,false〉 ?)
 676   [| >Hintape % ] -Hta #Hcneq cut (mv ≠ bit false)
 677   [ lapply (\Pf Hcneq) @not_to_not #Heq >Heq % ] -Hcneq #Hcneq #Hta destruct (Hta)
 678     *
 679     [ * #tb * whd in ⊢ (%→?);#Htb cases (Htb 〈mv,false〉 ?)
 680       [| >Hintape % ] -Htb #Hceq #Htb lapply (\P Hceq) -Hceq #Hceq destruct (Htb Hceq)
 681       * #tc * whd in ⊢ (%→?); #Htc cases (Htc … Hintape) -Htc -Hintape
 682       [ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
 683     * #_ #Htc lapply (Htc … (refl ??) (refl ??) ?)
 684     [ @daemon ] -Htc >append_cons <associative_append #Htc
 685     whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc … Ht1') //
 686     [ >reverse_append >reverse_append >reverse_reverse @Htable
 687     | /2/ |]
 688     -Houtc -Htc * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal
 689     @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) %
 690     [ //
 691     | %
 692       [ >Houtc >reverse_append >reverse_append >reverse_reverse
 693         >associative_append >associative_append %
 694       | % %2 % // ]
 695     ]
 696   | * #tb * whd in ⊢ (%→?); #Htb cases (Htb 〈mv,false〉 ?)
 697     [| >Hintape % ] -Htb #Hcneq' cut (mv ≠ bit true)
 698     [ lapply (\Pf Hcneq') @not_to_not #Heq >Heq % ] -Hcneq' #Hcneq' #Htb destruct (Htb)
 699     * #tc * whd in ⊢ (%→?); #Htc cases (Htc … Hintape)
 700     [ *  >(bit_or_null_not_grid … Hmv) #Hfalse destruct (Hfalse) ] -Htc
 701     * #_ #Htc lapply (Htc … (refl ??) (refl ??) ?) [@daemon] -Htc #Htc
 702     * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd -Htc
 703     whd in ⊢ (???%→?); #Htd whd in ⊢ (%→?); #Houtc lapply (Houtc … Htd) -Houtc *
 704     [ * cases Htape * * #_ #_ #Hcurc #_
 705       >(bit_or_null_not_grid … Hcurc) #Hfalse destruct (Hfalse) ]
 706     * #_ #Houtc lapply (Houtc … (refl ??) (refl ??) ?) [@daemon] -Houtc #Houtc
 707     @(ex_intro ?? ls) @(ex_intro ?? rs) @(ex_intro ?? curc) %
 708     [ //
 709     | %
 710       [ @Houtc
 711       | %2 % // % // % //
 712         generalize in match Hcneq; generalize in match Hcneq';
 713         cases mv in Hmv; normalize //
 714         [ * #_ normalize [ #Hfalse @False_ind cases Hfalse /2/ | #_ #Hfalse @False_ind cases Hfalse /2/ ]
 715         |*: #Hfalse destruct (Hfalse) ]
 716       ]
 717     ]
 718   ]
 719 ]
 720 qed.