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