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