matita/matita/lib/turing/universal/marks.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
  13 (* COMPARE BIT
  14
  15 *)
  16
  17 include "turing/while_machine.ma".
  18 include "turing/if_machine.ma".
  19
  20 (* ADVANCE TO MARK (right)
  21
  22    sposta la testina a destra fino a raggiungere il primo carattere marcato
  23
  24 *)
  25
  26 (* 0, a ≠ mark _ ⇒ 0, R
  27 0, a = mark _ ⇒ 1, N *)
  28
  29 definition atm_states ≝ initN 3.
  30
  31 definition atmr_step ≝
  32   λalpha:FinSet.λtest:alpha→bool.
  33   mk_TM alpha atm_states
  34   (λp.let 〈q,a〉 ≝ p in
  35    match a with
  36    [ None ⇒ 〈1, None ?〉
  37    | Some a' ⇒
  38      match test a' with
  39      [ true ⇒ 〈1,None ?〉
  40      | false ⇒ 〈2,Some ? 〈a',R〉〉 ]])
  41   O (λx.notb (x == 0)).
  42
  43 definition Ratmr_step_true ≝
  44   λalpha,test,t1,t2.
  45    ∃ls,a,rs.
  46    t1 = midtape alpha ls a rs ∧ test a = false ∧
  47    t2 = mk_tape alpha (a::ls) (option_hd ? rs) (tail ? rs).
  48
  49 definition Ratmr_step_false ≝
  50   λalpha,test,t1,t2.
  51     t1 = t2 ∧
  52     (current alpha t1 = None ? ∨
  53      (∃a.current ? t1 = Some ? a ∧ test a = true)).
  54
  55 lemma atmr_q0_q1 :
  56   ∀alpha,test,ls,a0,rs. test a0 = true →
  57   step alpha (atmr_step alpha test)
  58     (mk_config ?? 0 (midtape … ls a0 rs)) =
  59   mk_config alpha (states ? (atmr_step alpha test)) 1
  60     (midtape … ls a0 rs).
  61 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
  62 qed.
  63
  64 lemma atmr_q0_q2 :
  65   ∀alpha,test,ls,a0,rs. test a0 = false →
  66   step alpha (atmr_step alpha test)
  67     (mk_config ?? 0 (midtape … ls a0 rs)) =
  68   mk_config alpha (states ? (atmr_step alpha test)) 2
  69     (mk_tape … (a0::ls) (option_hd ? rs) (tail ? rs)).
  70 #alpha #test #ls #a0 #ts #Htest normalize >Htest cases ts //
  71 qed.
  72
  73 lemma sem_atmr_step :
  74   ∀alpha,test.
  75   accRealize alpha (atmr_step alpha test)
  76     2 (Ratmr_step_true alpha test) (Ratmr_step_false alpha test).
  77 #alpha #test *
  78 [ @(ex_intro ?? 2)
  79   @(ex_intro ?? (mk_config ?? 1 (niltape ?))) %
  80   [ % // #Hfalse destruct | #_ % // % % ]
  81 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (leftof ? a al)))
  82   % [ % // #Hfalse destruct | #_ % // % % ]
  83 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (rightof ? a al)))
  84   % [ % // #Hfalse destruct | #_ % // % % ]
  85 | #ls #c #rs @(ex_intro ?? 2)
  86   cases (true_or_false (test c)) #Htest
  87   [ @(ex_intro ?? (mk_config ?? 1 ?))
  88     [| %
  89       [ %
  90         [ whd in ⊢ (??%?); >atmr_q0_q1 //
  91         | #Hfalse destruct ]
  92       | #_ % // %2 @(ex_intro ?? c) % // ]
  93     ]
  94   | @(ex_intro ?? (mk_config ?? 2 (mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs))))
  95     %
  96     [ %
  97       [ whd in ⊢ (??%?); >atmr_q0_q2 //
  98       | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
  99         % // % //
 100       ]
 101     | #Hfalse @False_ind @(absurd ?? Hfalse) %
 102     ]
 103   ]
 104 ]
 105 qed.
 106
 107 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
 108   ∀ls,c,rs.
 109   (t1 = midtape alpha ls c rs  →
 110   ((test c = true ∧ t2 = t1) ∨
 111    (test c = false ∧
 112     ∀rs1,b,rs2. rs = rs1@b::rs2 →
 113      test b = true → (∀x.memb ? x rs1 = true → test x = false) →
 114      t2 = midtape ? (reverse ? rs1@c::ls) b rs2))).
 115
 116 definition adv_to_mark_r ≝
 117   λalpha,test.whileTM alpha (atmr_step alpha test) 2.
 118
 119 lemma wsem_adv_to_mark_r :
 120   ∀alpha,test.
 121   WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
 122 #alpha #test #t #i #outc #Hloop
 123 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
 124 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 125 [ #tapea * #Htapea *
 126   [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
 127     #Hfalse destruct (Hfalse)
 128   | * #a * #Ha #Htest #ls #c #rs #H2 %
 129     >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
 130     <Htapea //
 131   ]
 132 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
 133   lapply (IH HRfalse) -IH #IH
 134   #ls #c #rs #Htapea %2
 135   cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
 136
 137   >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
 138   [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
 139     cases (IH … Htapeb)
 140     [ * #_ #Houtc >Houtc >Htapeb %
 141     | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
 142   | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
 143     cases (IH … Htapeb)
 144     [ * #Hfalse >(Hmemb …) in Hfalse;
 145       [ #Hft destruct (Hft)
 146       | @memb_hd ]
 147     | * #Htestr1 #H1 >reverse_cons >associative_append
 148       @H1 // #x #Hx @Hmemb @memb_cons //
 149     ]
 150   ]
 151 qed.
 152
 153 lemma terminate_adv_to_mark_r :
 154   ∀alpha,test.
 155   ∀t.Terminate alpha (adv_to_mark_r alpha test) t.
 156 #alpha #test #t
 157 @(terminate_while … (sem_atmr_step alpha test))
 158   [ %
 159   | cases t
 160     [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 161     |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 162     | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
 163       elim rs
 164       [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 165        #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 166        % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
 167        normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
 168       | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 169         #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 170         >Ht1 @IH
 171       ]
 172     ]
 173   ]
 174 qed.
 175
 176 lemma sem_adv_to_mark_r :
 177   ∀alpha,test.
 178   Realize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
 179 /2/
 180 qed.
 181
 182 (* MARK machine
 183
 184    marks the current character
 185  *)
 186
 187 definition mark_states ≝ initN 2.
 188
 189 definition mark ≝
 190   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
 191   (λp.let 〈q,a〉 ≝ p in
 192     match a with
 193     [ None ⇒ 〈1,None ?〉
 194     | Some a' ⇒ match q with
 195       [ O ⇒ let 〈a'',b〉 ≝ a' in 〈1,Some ? 〈〈a'',true〉,N〉〉
 196       | S q ⇒ 〈1,None ?〉 ] ])
 197   O (λq.q == 1).
 198
 199 definition R_mark ≝ λalpha,t1,t2.
 200   ∀ls,c,b,rs.
 201   t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
 202   t2 = midtape ? ls 〈c,true〉 rs.
 203
 204 lemma sem_mark :
 205   ∀alpha.Realize ? (mark alpha) (R_mark alpha).
 206 #alpha #intape @(ex_intro ?? 2) cases intape
 207 [ @ex_intro
 208   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 209 |#a #al @ex_intro
 210   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 211 |#a #al @ex_intro
 212   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 213 | #ls * #c #b #rs
 214   @ex_intro [| % [ % | #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ] ] ]
 215 qed.
 216
 217 (* MOVE RIGHT
 218
 219    moves the head one step to the right
 220
 221 *)
 222
 223 definition move_states ≝ initN 2.
 224
 225 definition move_r ≝
 226   λalpha:FinSet.mk_TM alpha move_states
 227   (λp.let 〈q,a〉 ≝ p in
 228     match a with
 229     [ None ⇒ 〈1,None ?〉
 230     | Some a' ⇒ match q with
 231       [ O ⇒ 〈1,Some ? 〈a',R〉〉
 232       | S q ⇒ 〈1,None ?〉 ] ])
 233   O (λq.q == 1).
 234
 235 definition R_move_r ≝ λalpha,t1,t2.
 236   ∀ls,c,rs.
 237   t1 = midtape alpha ls c rs →
 238   t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
 239
 240 lemma sem_move_r :
 241   ∀alpha.Realize ? (move_r alpha) (R_move_r alpha).
 242 #alpha #intape @(ex_intro ?? 2) cases intape
 243 [ @ex_intro
 244   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
 245 |#a #al @ex_intro
 246   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
 247 |#a #al @ex_intro
 248   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
 249 | #ls #c #rs
 250   @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
 251   cases rs0 // ] ] ]
 252 qed.
 253
 254 (* MOVE LEFT
 255
 256    moves the head one step to the right
 257
 258 *)
 259
 260 definition move_l ≝
 261   λalpha:FinSet.mk_TM alpha move_states
 262   (λp.let 〈q,a〉 ≝ p in
 263     match a with
 264     [ None ⇒ 〈1,None ?〉
 265     | Some a' ⇒ match q with
 266       [ O ⇒ 〈1,Some ? 〈a',L〉〉
 267       | S q ⇒ 〈1,None ?〉 ] ])
 268   O (λq.q == 1).
 269
 270 definition R_move_l ≝ λalpha,t1,t2.
 271   ∀ls,c,rs.
 272   t1 = midtape alpha ls c rs →
 273   t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
 274
 275 lemma sem_move_l :
 276   ∀alpha.Realize ? (move_l alpha) (R_move_l alpha).
 277 #alpha #intape @(ex_intro ?? 2) cases intape
 278 [ @ex_intro
 279   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
 280 |#a #al @ex_intro
 281   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
 282 |#a #al @ex_intro
 283   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
 284 | #ls #c #rs
 285   @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
 286   cases ls0 // ] ] ]
 287 qed.
 288
 289 (* MOVE RIGHT AND MARK machine
 290
 291    marks the first character on the right
 292
 293    (could be rewritten using (mark; move_right))
 294  *)
 295
 296 definition mrm_states ≝ initN 3.
 297
 298 definition move_right_and_mark ≝
 299   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mrm_states
 300   (λp.let 〈q,a〉 ≝ p in
 301     match a with
 302     [ None ⇒ 〈2,None ?〉
 303     | Some a' ⇒ match q with
 304       [ O ⇒ 〈1,Some ? 〈a',R〉〉
 305       | S q ⇒ match q with
 306         [ O ⇒ let 〈a'',b〉 ≝ a' in
 307               〈2,Some ? 〈〈a'',true〉,N〉〉
 308         | S _ ⇒ 〈2,None ?〉 ] ] ])
 309   O (λq.q == 2).
 310
 311 definition R_move_right_and_mark ≝ λalpha,t1,t2.
 312   ∀ls,c,d,b,rs.
 313   t1 = midtape (FinProd … alpha FinBool) ls c (〈d,b〉::rs) →
 314   t2 = midtape ? (c::ls) 〈d,true〉 rs.
 315
 316 lemma sem_move_right_and_mark :
 317   ∀alpha.Realize ? (move_right_and_mark alpha) (R_move_right_and_mark alpha).
 318 #alpha #intape @(ex_intro ?? 3) cases intape
 319 [ @ex_intro
 320   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 321 |#a #al @ex_intro
 322   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 323 |#a #al @ex_intro
 324   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 325 | #ls #c *
 326   [ @ex_intro [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #Hfalse destruct ] ]
 327   | * #d #b #rs @ex_intro
 328     [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #H1 destruct (H1) % ] ] ] ]
 329 qed.
 330
 331 (* CLEAR MARK machine
 332
 333    clears the mark in the current character
 334  *)
 335
 336 definition clear_mark_states ≝ initN 3.
 337
 338 definition clear_mark ≝
 339   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) clear_mark_states
 340   (λp.let 〈q,a〉 ≝ p in
 341     match a with
 342     [ None ⇒ 〈1,None ?〉
 343     | Some a' ⇒ match q with
 344       [ O ⇒ let 〈a'',b〉 ≝ a' in 〈1,Some ? 〈〈a'',false〉,N〉〉
 345       | S q ⇒ 〈1,None ?〉 ] ])
 346   O (λq.q == 1).
 347
 348 definition R_clear_mark ≝ λalpha,t1,t2.
 349   ∀ls,c,b,rs.
 350   t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
 351   t2 = midtape ? ls 〈c,false〉 rs.
 352
 353 lemma sem_clear_mark :
 354   ∀alpha.Realize ? (clear_mark alpha) (R_clear_mark alpha).
 355 #alpha #intape @(ex_intro ?? 2) cases intape
 356 [ @ex_intro
 357   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 358 |#a #al @ex_intro
 359   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 360 |#a #al @ex_intro
 361   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 362 | #ls * #c #b #rs
 363   @ex_intro [| % [ % | #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ] ] ]
 364 qed.
 365
 366 (* ADVANCE MARK RIGHT machine
 367
 368    clears mark on current char,
 369    moves right, and marks new current char
 370
 371 *)
 372
 373 definition adv_mark_r ≝
 374   λalpha:FinSet.
 375     seq ? (clear_mark alpha)
 376       (seq ? (move_r ?) (mark alpha)).
 377
 378 definition R_adv_mark_r ≝ λalpha,t1,t2.
 379   ∀ls,c,d,b,rs.
 380   t1 = midtape (FinProd … alpha FinBool) ls 〈c,true〉 (〈d,b〉::rs) →
 381   t2 = midtape ? (〈c,false〉::ls) 〈d,true〉 rs.
 382
 383 lemma sem_adv_mark_r :
 384   ∀alpha.Realize ? (adv_mark_r alpha) (R_adv_mark_r alpha).
 385 #alpha #intape
 386 cases (sem_seq ????? (sem_clear_mark …)
 387          (sem_seq ????? (sem_move_r ?) (sem_mark alpha)) intape)
 388 #k * #outc * #Hloop whd in ⊢ (%→?);
 389 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→%→?); #Hs2 #Hs3
 390 @(ex_intro ?? k) @(ex_intro ?? outc) %
 391 [ @Hloop
 392 | -Hloop #ls #c #d #b #rs #Hintape @(Hs3 … b)
 393   @(Hs2 ls 〈c,false〉 (〈d,b〉::rs))
 394   @(Hs1 … Hintape)
 395 ]
 396 qed.
 397
 398 (* ADVANCE TO MARK (left)
 399
 400 axiomatized
 401
 402 *)
 403
 404 definition R_adv_to_mark_l ≝ λalpha,test,t1,t2.
 405   ∀ls,c,rs.
 406   (t1 = midtape alpha ls c rs  →
 407   ((test c = true ∧ t2 = t1) ∨
 408    (test c = false ∧
 409     ∀ls1,b,ls2. ls = ls1@b::ls2 →
 410      test b = true → (∀x.memb ? x ls1 = true → test x = false) →
 411      t2 = midtape ? ls2 b (reverse ? ls1@c::rs)))).
 412
 413 axiom adv_to_mark_l : ∀alpha:FinSet.(alpha → bool) → TM alpha.
 414 (* definition adv_to_mark_l ≝
 415   λalpha,test.whileTM alpha (atml_step alpha test) 2. *)
 416
 417 axiom wsem_adv_to_mark_l :
 418   ∀alpha,test.
 419   WRealize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
 420 (*
 421 #alpha #test #t #i #outc #Hloop
 422 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
 423 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 424 [ #tapea * #Htapea *
 425   [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
 426     #Hfalse destruct (Hfalse)
 427   | * #a * #Ha #Htest #ls #c #rs #H2 %
 428     >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
 429     <Htapea //
 430   ]
 431 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
 432   lapply (IH HRfalse) -IH #IH
 433   #ls #c #rs #Htapea %2
 434   cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
 435
 436   >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
 437   [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
 438     cases (IH … Htapeb)
 439     [ * #_ #Houtc >Houtc >Htapeb %
 440     | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
 441   | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
 442     cases (IH … Htapeb)
 443     [ * #Hfalse >(Hmemb …) in Hfalse;
 444       [ #Hft destruct (Hft)
 445       | @memb_hd ]
 446     | * #Htestr1 #H1 >reverse_cons >associative_append
 447       @H1 // #x #Hx @Hmemb @memb_cons //
 448     ]
 449   ]
 450 qed.
 451 *)
 452
 453 axiom terminate_adv_to_mark_l :
 454   ∀alpha,test.
 455   ∀t.Terminate alpha (adv_to_mark_l alpha test) t.
 456 (*
 457 #alpha #test #t
 458 @(terminate_while … (sem_atmr_step alpha test))
 459   [ %
 460   | cases t
 461     [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 462     |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 463     | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
 464       elim rs
 465       [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 466        #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 467        % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
 468        normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
 469       | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 470         #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 471         >Ht1 @IH
 472       ]
 473     ]
 474   ]
 475 qed.
 476 *)
 477
 478 lemma sem_adv_to_mark_l :
 479   ∀alpha,test.
 480   Realize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
 481 /2/
 482 qed.
 483
 484 (*
 485    ADVANCE BOTH MARKS machine
 486
 487    l1 does not contain marks ⇒
 488
 489
 490    input:
 491    l0 x* a l1 x0* a0 l2
 492               ^
 493
 494    output:
 495    l0 x a* l1 x0 a0* l2
 496         ^
 497 *)
 498
 499 definition is_marked ≝
 500   λalpha.λp:FinProd … alpha FinBool.
 501   let 〈x,b〉 ≝ p in b.
 502
 503 definition adv_both_marks ≝
 504   λalpha.seq ? (adv_mark_r alpha)
 505     (seq ? (move_l ?)
 506      (seq ? (adv_to_mark_l (FinProd alpha FinBool) (is_marked alpha))
 507        (adv_mark_r alpha))).
 508
 509 definition R_adv_both_marks ≝
 510   λalpha,t1,t2.
 511     ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
 512     t1 = midtape (FinProd … alpha FinBool)
 513         (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
 514     t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2).
 515
 516 lemma sem_adv_both_marks :
 517   ∀alpha.Realize ? (adv_both_marks alpha) (R_adv_both_marks alpha).
 518 #alpha #intape
 519 cases (sem_seq ????? (sem_adv_mark_r …)
 520         (sem_seq ????? (sem_move_l …)
 521           (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?))
 522             (sem_adv_mark_r alpha))) intape)
 523 #k * #outc * #Hloop whd in ⊢ (%→?);
 524 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→?); #Hs2
 525 * #tc * whd in ⊢ (%→%→?); #Hs3 #Hs4
 526 @(ex_intro ?? k) @(ex_intro ?? outc) %
 527 [ @Hloop
 528 | -Hloop #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
 529   @(Hs4 … false) -Hs4
 530   lapply (Hs1 … Hintape) #Hta
 531   lapply (Hs2 … Hta) #Htb
 532   cases (Hs3 … Htb)
 533   [ * #Hfalse normalize in Hfalse; destruct (Hfalse)
 534   | * #_ -Hs3 #Hs3
 535     lapply (Hs3 (l1@[〈a,false〉]) 〈x,true〉 l0 ???)
 536     [ #x1 #Hx1 cases (memb_append … Hx1)
 537       [ @Hl1
 538       | #Hx1' >(memb_single … Hx1') % ]
 539     | %
 540     | >associative_append %
 541     | >reverse_append #Htc @Htc ]
 542   ]
 543 qed.
 544
 545 inductive unialpha : Type[0] ≝
 546 | bit : bool → unialpha
 547 | comma : unialpha
 548 | bar : unialpha
 549 | grid : unialpha.
 550
 551 definition unialpha_eq ≝
 552   λa1,a2.match a1 with
 553   [ bit x ⇒ match a2 with [ bit y ⇒ ¬ xorb x y | _ ⇒ false ]
 554   | comma ⇒ match a2 with [ comma ⇒ true | _ ⇒ false ]
 555   | bar ⇒ match a2 with [ bar ⇒ true | _ ⇒ false ]
 556   | grid ⇒ match a2 with [ grid ⇒ true | _ ⇒ false ] ].
 557
 558 definition DeqUnialpha ≝ mk_DeqSet unialpha unialpha_eq ?.
 559 * [ #x * [ #y cases x cases y normalize % // #Hfalse destruct
 560          | *: normalize % #Hfalse destruct ]
 561   |*: * [1,5,9,13: #y ] normalize % #H1 destruct % ]
 562 qed.
 563
 564 definition FSUnialpha ≝
 565   mk_FinSet DeqUnialpha [bit true;bit false;comma;bar;grid] ?.
 566 @daemon
 567 qed.
 568
 569 (*
 570    MATCH AND ADVANCE(f)
 571
 572    input:
 573    l0 x* a l1 x0* a0 l2
 574               ^
 575
 576    output:
 577    l0 x a* l1 x0 a0* l2   (f(x0) == true)
 578         ^
 579    l0 x* a l1 x0* a0 l2   (f(x0) == false)
 580               ^
 581 *)
 582
 583 include "turing/universal/tests.ma".
 584
 585 (* NO OPERATION
 586
 587   t1 = t2
 588   *)
 589
 590 definition nop_states ≝ initN 1.
 591
 592 definition nop ≝
 593   λalpha:FinSet.mk_TM alpha nop_states
 594   (λp.let 〈q,a〉 ≝ p in 〈q,None ?〉)
 595   O (λ_.true).
 596
 597 definition R_nop ≝ λalpha.λt1,t2:tape alpha.t2 = t1.
 598
 599 lemma sem_nop :
 600   ∀alpha.Realize alpha (nop alpha) (R_nop alpha).
 601 #alpha #intape @(ex_intro ?? 1) @ex_intro [| % normalize % ]
 602 qed.
 603
 604 definition match_and_adv ≝
 605   λalpha,f.ifTM ? (test_char ? f)
 606      (adv_both_marks alpha) (nop ?) tc_true.
 607
 608 definition R_match_and_adv ≝
 609   λalpha,f,t1,t2.
 610     ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
 611     t1 = midtape (FinProd … alpha FinBool)
 612         (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
 613     (f 〈x0,true〉 = true ∧ t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2))
 614     ∨ (f 〈x0,true〉 = false ∧ t2 = t1).
 615
 616 lemma sem_match_and_adv :
 617   ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv alpha f).
 618 #alpha #f #intape
 619 cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_nop ?) intape)
 620 #k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
 621 % [ @Hloop ] -Hloop
 622 cases Hif
 623 [ * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
 624   #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
 625   >Hintape in Hta; #Hta cases (Hta … (refl ??)) -Hta #Hf #Hta % %
 626   [ @Hf | @Houtc [ @Hl1 | @Hta ] ]
 627 | * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
 628   #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
 629   >Hintape in Hta; #Hta cases (Hta … (refl ??)) -Hta #Hf #Hta %2 %
 630   [ @Hf | >Houtc @Hta ]
 631 ]
 632 qed.
 633
 634 (*
 635  if x = c
 636       then move_right; ----
 637            adv_to_mark_r;
 638            if current (* x0 *) = 0
 639               then advance_mark ----
 640                    adv_to_mark_l;
 641                    advance_mark
 642               else STOP
 643       else M
 644 *)
 645
 646 definition comp_step_subcase ≝
 647   λalpha,c,elseM.ifTM ? (test_char ? (λx.x == c))
 648     (seq ? (move_r …)
 649       (seq ? (adv_to_mark_r ? (is_marked alpha))
 650       (match_and_adv ? (λx.x == c))))
 651     elseM tc_true.
 652
 653 definition R_comp_step_subcase ≝
 654   λalpha,c,RelseM,t1,t2.
 655     ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
 656     t1 = midtape (FinProd … alpha FinBool)
 657            l0 〈x,true〉 (〈a,false〉::l1@〈x0,true〉::〈a0,false〉::l2) →
 658     (〈x,true〉 = c ∧ x = x0 ∧
 659      t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1@〈x0,false〉::〈a0,true〉::l2))
 660     ∨ (〈x,true〉 = c ∧ x ≠ x0 ∧
 661      t2 = midtape (FinProd … alpha FinBool)
 662         (reverse ? l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2))
 663     ∨ (〈x,true〉 ≠ c ∧ RelseM t1 t2).
 664
 665 lemma sem_comp_step_subcase :
 666   ∀alpha,c,elseM,RelseM.
 667   Realize ? elseM RelseM →
 668   Realize ? (comp_step_subcase alpha c elseM)
 669     (R_comp_step_subcase alpha c RelseM).
 670 #alpha #c #elseM #RelseM #Helse #intape
 671 cases (sem_if ? (test_char ? (λx.x == c)) … tc_true
 672         (sem_test_char ? (λx.x == c))
 673         (sem_seq ????? (sem_move_r …)
 674           (sem_seq ????? (sem_adv_to_mark_r ? (is_marked alpha))
 675              (sem_match_and_adv ? (λx.x == c)))) Helse intape)
 676 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc)
 677 % [ @Hloop ] -Hloop cases HR -HR
 678 [ * #ta * whd in ⊢ (%→?); #Hta * #tb * whd in ⊢ (%→?); #Htb
 679   * #tc * whd in ⊢ (%→?); #Htc whd in ⊢ (%→?); #Houtc
 680   #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape %
 681   >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta
 682   #Hx #Hta lapply (Htb … Hta) -Htb #Htb
 683   cases (Htc … Htb) [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
 684   -Htc * #_ #Htc lapply (Htc l1 〈x0,true〉 (〈a0,false〉::l2) (refl ??) (refl ??) Hl1)
 685   -Htc #Htc cases (Houtc ???????? Htc) -Houtc
 686   [ * #Hx0 #Houtc % %
 687     [ % [ @(\P Hx) | <(\P Hx0) in Hx; #Hx lapply (\P Hx) #Hx' destruct (Hx') % ]
 688     | >Houtc >reverse_reverse % ]
 689   | * #Hx0 #Houtc %2 %
 690     [ % [ @(\P Hx) | <(\P Hx) in Hx0; #Hx0 lapply (\Pf Hx0) @not_to_not #Hx' >Hx' %]
 691     | >Houtc @Htc ]
 692   | (* members of lists are invariant under reverse *) @daemon ]
 693 | * #ta * whd in ⊢ (%→?); #Hta #Houtc
 694   #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape %2
 695   >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hx #Hta %
 696   [ @(\Pf Hx)
 697   | <Hta @Houtc ]
 698 ]
 699 qed.
 700
 701
 702
 703 (*
 704    MARK NEXT TUPLE machine
 705    (partially axiomatized)
 706
 707    marks the first character after the first bar (rightwards)
 708  *)
 709
 710 axiom myalpha : FinSet.
 711 axiom is_bar : FinProd … myalpha FinBool → bool.
 712 axiom is_grid : FinProd … myalpha FinBool → bool.
 713 definition bar_or_grid ≝ λc.is_bar c ∨ is_grid c.
 714 axiom bar : FinProd … myalpha FinBool.
 715 axiom grid : FinProd … myalpha FinBool.
 716
 717 definition mark_next_tuple ≝
 718   seq ? (adv_to_mark_r ? bar_or_grid)
 719      (ifTM ? (test_char ? is_bar)
 720        (move_r_and_mark ?) (nop ?) 1).
 721
 722 definition R_mark_next_tuple ≝
 723   λt1,t2.
 724     ∀ls,c,rs1,rs2.
 725     (* c non può essere un separatore ... speriamo *)
 726     t1 = midtape ? ls c (rs1@grid::rs2) →
 727     memb ? grid rs1 = false → bar_or_grid c = false →
 728     (∃rs3,rs4,d,b.rs1 = rs3 @ bar :: rs4 ∧
 729       memb ? bar rs3 = false ∧
 730       Some ? 〈d,b〉 = option_hd ? (rs4@grid::rs2) ∧
 731       t2 = midtape ? (bar::reverse ? rs3@c::ls) 〈d,true〉 (tail ? (rs4@grid::rs2)))
 732     ∨
 733     (memb ? bar rs1 = false ∧
 734      t2 = midtape ? (reverse ? rs1@c::ls) grid rs2).
 735
 736 axiom tech_split :
 737   ∀A:DeqSet.∀f,l.
 738    (∀x.memb A x l = true → f x = false) ∨
 739    (∃l1,c,l2.f c = true ∧ l = l1@c::l2 ∧ ∀x.memb ? x l1 = true → f c = false).
 740 (*#A #f #l elim l
 741 [ % #x normalize #Hfalse *)
 742
 743 theorem sem_mark_next_tuple :
 744   Realize ? mark_next_tuple R_mark_next_tuple.
 745 #intape
 746 lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid)
 747          (ifTM ? (test_char ? is_bar) (mark ?) (nop ?) 1) ????)
 748 [@sem_if //
 749 | //
 750 |||#Hif cases (Hif intape) -Hif
 751    #j * #outc * #Hloop * #ta * #Hleft #Hright
 752    @(ex_intro ?? j) @ex_intro [|% [@Hloop] ]
 753    -Hloop
 754    #ls #c #rs1 #rs2 #Hrs #Hrs1 #Hc
 755    cases (Hleft … Hrs)
 756    [ * #Hfalse >Hfalse in Hc; #Htf destruct (Htf)
 757    | * #_ #Hta cases (tech_split ? is_bar rs1)
 758      [ #H1 lapply (Hta rs1 grid rs2 (refl ??) ? ?)
 759        [ (* Hrs1, H1 *) @daemon
 760        | (* bar_or_grid grid = true *) @daemon
 761        | -Hta #Hta cases Hright
 762          [ * #tb * whd in ⊢ (%→?); #Hcurrent
 763            @False_ind cases(Hcurrent grid ?)
 764            [ #Hfalse (* grid is not a bar *) @daemon
 765            | >Hta % ]
 766          | * #tb * whd in ⊢ (%→?); #Hcurrent
 767            cases (Hcurrent grid ?)
 768            [  #_ #Htb whd in ⊢ (%→?); #Houtc
 769              %2 %
 770              [ (* H1 *) @daemon
 771              | >Houtc >Htb >Hta % ]
 772            | >Hta % ]
 773          ]
 774        ]
 775     | * #rs3 * #c0 * #rs4 * * #Hc0 #Hsplit #Hrs3
 776       % @(ex_intro ?? rs3) @(ex_intro ?? rs4)
 777      lapply (Hta rs3 c0 (rs4@grid::rs2) ???)
 778      [ #x #Hrs3' (* Hrs1, Hrs3, Hsplit *) @daemon
 779      | (* bar → bar_or_grid *) @daemon
 780      | >Hsplit >associative_append % ] -Hta #Hta
 781        cases Hright
 782        [ * #tb * whd in ⊢ (%→?); #Hta'
 783          whd in ⊢ (%→?); #Htb
 784          cases (Hta' c0 ?)
 785          [ #_ #Htb' >Htb' in Htb; #Htb
 786            generalize in match Hsplit; -Hsplit
 787            cases rs4 in Hta;
 788            [ >(eq_pair_fst_snd … grid)
 789              #Hta #Hsplit >(Htb … Hta)
 790              >(?:c0 = bar)
 791              [ @(ex_intro ?? (\fst grid)) @(ex_intro ?? (\snd grid))
 792                % [ % [ % [ (* Hsplit *) @daemon |(*Hrs3*) @daemon ] | % ] | % ]
 793                      | (* Hc0 *) @daemon ]
 794            | #r5 #rs5 >(eq_pair_fst_snd … r5)
 795              #Hta #Hsplit >(Htb … Hta)
 796              >(?:c0 = bar)
 797              [ @(ex_intro ?? (\fst r5)) @(ex_intro ?? (\snd r5))
 798                % [ % [ % [ (* Hc0, Hsplit *) @daemon | (*Hrs3*) @daemon ] | % ]
 799                      | % ] | (* Hc0 *) @daemon ] ] | >Hta % ]
 800              | * #tb * whd in ⊢ (%→?); #Hta'
 801                whd in ⊢ (%→?); #Htb
 802                cases (Hta' c0 ?)
 803                [ #Hfalse @False_ind >Hfalse in Hc0;
 804                  #Hc0 destruct (Hc0)
 805                | >Hta % ]
 806 ]]]]
 807 qed.