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