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