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) (clear_mark ?) 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 ∧
 595     t2 = midtape ? (l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)).
 596
 597 lemma sem_match_and_adv :
 598   ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv alpha f).
 599 #alpha #f #intape
 600 cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape)
 601 #k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
 602 % [ @Hloop ] -Hloop
 603 cases Hif
 604 [ * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
 605   #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
 606   >Hintape in Hta; #Hta cases (Hta … (refl ??)) -Hta #Hf #Hta % %
 607   [ @Hf | @Houtc [ @Hl1 | @Hta ] ]
 608 | * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
 609   #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
 610   >Hintape in Hta; #Hta cases (Hta … (refl ??)) -Hta #Hf #Hta %2 %
 611   [ @Hf | >(Houtc … Hta) % ]
 612 ]
 613 qed.
 614
 615 (*
 616  if x = c
 617       then move_right; ----
 618            adv_to_mark_r;
 619            if current (* x0 *) = 0
 620               then advance_mark ----
 621                    adv_to_mark_l;
 622                    advance_mark
 623               else STOP
 624       else M
 625 *)
 626
 627 definition comp_step_subcase ≝
 628   λalpha,c,elseM.ifTM ? (test_char ? (λx.x == c))
 629     (seq ? (move_r …)
 630       (seq ? (adv_to_mark_r ? (is_marked alpha))
 631       (match_and_adv ? (λx.x == c))))
 632     elseM tc_true.
 633
 634 definition R_comp_step_subcase ≝
 635   λalpha,c,RelseM,t1,t2.
 636     ∀l0,x,rs.t1 = midtape (FinProd … alpha FinBool) l0 〈x,true〉 rs →
 637     (〈x,true〉 = c ∧
 638      ∀a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
 639      rs = 〈a,false〉::l1@〈x0,true〉::〈a0,false〉::l2 →
 640      ((x = x0 ∧
 641       t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1@〈x0,false〉::〈a0,true〉::l2)) ∨
 642       (x ≠ x0 ∧
 643       t2 = midtape (FinProd … alpha FinBool)
 644         (reverse ? l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)))) ∨
 645     (〈x,true〉 ≠ c ∧ RelseM t1 t2).
 646
 647 lemma sem_comp_step_subcase :
 648   ∀alpha,c,elseM,RelseM.
 649   Realize ? elseM RelseM →
 650   Realize ? (comp_step_subcase alpha c elseM)
 651     (R_comp_step_subcase alpha c RelseM).
 652 #alpha #c #elseM #RelseM #Helse #intape
 653 cases (sem_if ? (test_char ? (λx.x == c)) … tc_true
 654         (sem_test_char ? (λx.x == c))
 655         (sem_seq ????? (sem_move_r …)
 656           (sem_seq ????? (sem_adv_to_mark_r ? (is_marked alpha))
 657              (sem_match_and_adv ? (λx.x == c)))) Helse intape)
 658 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc)
 659 % [ @Hloop ] -Hloop cases HR -HR
 660 [ * #ta * whd in ⊢ (%→?); #Hta * #tb * whd in ⊢ (%→?); #Htb
 661   * #tc * whd in ⊢ (%→?); #Htc whd in ⊢ (%→?); #Houtc
 662   #l0 #x #rs #Hintape cases (true_or_false (〈x,true〉==c)) #Hc
 663   [ % % [ @(\P Hc) ]
 664     #a #l1 #x0 #a0 #l2 #Hl1 #Hrs >Hrs in Hintape; #Hintape
 665     >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta
 666     #Hx #Hta lapply (Htb … Hta) -Htb #Htb
 667     cases (Htc … Htb) [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
 668     -Htc * #_ #Htc lapply (Htc l1 〈x0,true〉 (〈a0,false〉::l2) (refl ??) (refl ??) Hl1)
 669     -Htc #Htc cases (Houtc ???????? Htc) -Houtc
 670     [ * #Hx0 #Houtc %
 671       % [ <(\P Hx0) in Hx; #Hx lapply (\P Hx) #Hx' destruct (Hx') %
 672         | >Houtc >reverse_reverse % ]
 673     | * #Hx0 #Houtc %2
 674       % [ <(\P Hx) in Hx0; #Hx0 lapply (\Pf Hx0) @not_to_not #Hx' >Hx' %
 675         | >Houtc % ]
 676     | (* members of lists are invariant under reverse *) @daemon ]
 677   | %2 % [ @(\Pf Hc) ]
 678     >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hx #Hta
 679     >Hx in Hc;#Hc destruct (Hc) ]
 680 | * #ta * whd in ⊢ (%→?); #Hta #Helse #ls #c0 #rs #Hintape %2
 681   >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hc #Hta %
 682   [ @(\Pf Hc) | <Hta @Helse ]
 683 ]
 684 qed.
 685
 686 (*
 687 - se marcato, itero
 688 - se non è marcato
 689   + se è un bit, ho fallito il confronto della tupla corrente
 690   + se è un separatore, la tupla fa match
 691
 692
 693 ifTM ? (test_char ? is_marked)
 694   (single_finalTM … (comp_step_subcase unialpha 〈bit false,true〉
 695     (comp_step_subcase unialpha 〈bit true,true〉
 696       (clear_mark …))))
 697   (nop ?)
 698 *)
 699
 700 definition comp_step ≝
 701   ifTM ? (test_char ? (is_marked ?))
 702   (single_finalTM … (comp_step_subcase FSUnialpha 〈bit false,true〉
 703     (comp_step_subcase FSUnialpha 〈bit true,true〉
 704       (clear_mark …))))
 705   (nop ?)
 706   tc_true.
 707
 708 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
 709
 710 definition R_comp_step_true ≝
 711   λt1,t2.
 712     ∀l0,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) l0 c rs →
 713     ∃c'. c = 〈c',true〉 ∧
 714     ((is_bit c' = true ∧
 715      ∀a,l1,c0,a0,l2.
 716       rs = 〈a,false〉::l1@〈c0,true〉::〈a0,false〉::l2 →
 717       (∀c.memb ? c l1 = true → is_marked ? c = false) →
 718       (c0 = c' ∧
 719        t2 = midtape ? (〈c',false〉::l0) 〈a,true〉 (l1@〈c0,false〉::〈a0,true〉::l2)) ∨
 720       (c0 ≠ c' ∧
 721        t2 = midtape (FinProd … FSUnialpha FinBool)
 722         (reverse ? l1@〈a,false〉::〈c',true〉::l0) 〈c0,false〉 (〈a0,false〉::l2))) ∨
 723      (is_bit c' = false ∧ t2 = midtape ? l0 〈c',false〉 rs)).
 724
 725 definition R_comp_step_false ≝
 726   λt1,t2.
 727    ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
 728    is_marked ? c = false ∧ t2 = t1.
 729
 730 lemma sem_comp_step :
 731   accRealize ? comp_step (inr … (inl … (inr … 0)))
 732     R_comp_step_true R_comp_step_false.
 733 #intape
 734 cases (acc_sem_if … (sem_test_char ? (is_marked ?))
 735         (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
 736           (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ??
 737             (sem_clear_mark …)))
 738         (sem_nop …) intape)
 739 #k * #outc * * #Hloop #H1 #H2
 740 @(ex_intro ?? k) @(ex_intro ?? outc) %
 741 [ % [@Hloop ] ] -Hloop
 742 [ #Hstate lapply (H1 Hstate) -H1 -Hstate -H2 *
 743   #ta * whd in ⊢ (%→?); #Hleft #Hright #ls #c #rs #Hintape
 744   >Hintape in Hleft; #Hleft cases (Hleft ? (refl ??)) -Hleft
 745   cases c in Hintape; #c' #b #Hintape whd in ⊢ (??%?→?);
 746   #Hb >Hb #Hta @(ex_intro ?? c') % //
 747   cases (Hright … Hta)
 748   [ * #Hc' #H1 % % [destruct (Hc') % ]
 749     #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
 750     cases (H1 … Hl1 Hrs)
 751     [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
 752     | * #Hneq #Houtc %2 %
 753       [ @sym_not_eq //
 754       | @Houtc ]
 755     ]
 756   | * #Hc #Helse1 cases (Helse1 … Hta)
 757     [ * #Hc' #H1 % % [destruct (Hc') % ]
 758       #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
 759       cases (H1 … Hl1 Hrs)
 760       [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
 761       | * #Hneq #Houtc %2 %
 762         [ @sym_not_eq //
 763         | @Houtc ]
 764       ]
 765     | * #Hc' whd in ⊢ (%→?); #Helse2 %2 %
 766       [ generalize in match Hc'; generalize in match Hc;
 767         cases c'
 768         [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
 769             | #Hfalse @False_ind @(absurd ?? Hfalse) % ]
 770         |*: #_ #_ % ]
 771       | @(Helse2 … Hta)
 772       ]
 773     ]
 774   ]
 775 | #Hstate lapply (H2 Hstate) -H1 -Hstate -H2 *
 776   #ta * whd in ⊢ (%→%→?); #Hleft #Hright #ls #c #rs #Hintape
 777   >Hintape in Hleft; #Hleft
 778   cases (Hleft ? (refl ??)) -Hleft
 779   #Hc #Hta % // >Hright //
 780 ]
 781 qed.
 782
 783 definition compare ≝
 784   whileTM ? comp_step (inr … (inl … (inr … 0))).
 785
 786 (*
 787 definition R_compare :=
 788   λt1,t2.
 789   (t
 790
 791   ∀ls,c,b,rs.t1 = midtape ? ls 〈c,b〉 rs →
 792   (b = true → rs = ....) →
 793   (b = false ∧ ....) ∨
 794   (b = true ∧
 795
 796    rs = cs@l1@〈c0,true〉::cs0@l2
 797    (
 798
 799
 800   ls 〈c,b〉 cs l1 〈c0,b0〉 cs0 l2
 801
 802
 803 ACCETTAZIONE:
 804   ls (hd (Ls@〈grid,false〉))* (tail (Ls@〈grid,false〉)) l1 (hd (Ls@〈comma,false〉))* (tail (Ls@〈comma,false〉)) l2
 805      ^^^^^^^^^^^^^^^^^^^^^^^
 806
 807   ls Ls 〈grid,false〉 l1 Ls 〈comma,true〉 l2
 808         ^^^^^^^^^^^^
 809
 810 RIFIUTO: c ≠ d
 811
 812   ls (hd (Ls@〈c,false〉))* (tail (Ls@〈c,false〉)) l1 (hd (Ls@〈d,false〉))* (tail (Ls@〈d,false〉)) l2
 813      ^^^^^^^^^^^^^^^^^^^^^^^
 814
 815
 816   ls Ls 〈c,true〉 l1 Ls 〈d,false〉 l2
 817                        ^^^^^^^^
 818
 819   ).
 820
 821   |bs| = |b0s| →
 822   (∃la,d.〈b,true〉::bs = la@[〈grid,d〉] ∧ ∀x.memb ? x la → is_bit (\fst x) = true) →
 823   (∃lb,d0.〈b0,true〉::b0s = lb@[〈comma,d0〉] ∧ ∀x.memb ? x lb → is_bit (\fst x) = true) →
 824   t1 = midtape ? l0 〈b,true〉 (bs@l1@〈b0,true〉::b0s@l2 →
 825
 826   mk_tape left (option current) right
 827
 828   (b = grid ∧ b0 = comma ∧ bs = [] ∧ b0s = [] ∧
 829    t2 = midtape ? l0 〈grid,false〉 (l1@〈comma,true〉::l2)) ∨
 830   (b = bit x ∧ b = c ∧ bs = b0s
 831   *)
 832 definition R_compare :=
 833   λt1,t2.
 834   ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
 835   (c = 〈grid,true〉 → t2 = midtape ? ls 〈grid,false〉 rs) ∧
 836   (∀c'. c = 〈c',false〉 → t2 = t1) ∧
 837   ∀b,b0,bs,b0s,l1,l2.
 838   |bs| = |b0s| →
 839   (∀c.memb (FinProd … FSUnialpha FinBool) c bs = true → is_bit (\fst c) = true) →
 840   (∀c.memb (FinProd … FSUnialpha FinBool) c b0s = true → is_bit (\fst c) = true) →
 841   (∀c.memb ? c bs = true → is_marked ? c = false) →
 842   (∀c.memb ? c b0s = true → is_marked ? c = false) →
 843   (∀c.memb ? c l1 = true → is_marked ? c = false) →
 844   c = 〈b,true〉 →
 845   rs = bs@〈grid,false〉::l1@〈b0,true〉::b0s@〈comma,false〉::l2 →
 846   (〈b,true〉::bs = 〈b0,true〉::b0s ∧
 847    ∀l3,c.〈b0,false〉::b0s = l3@[〈c,false〉] →
 848    t2 = midtape ? (reverse ? bs@〈b,false〉::ls)
 849           〈grid,false〉 (l1@l3@〈c,true〉::〈comma,false〉::l2)) ∨
 850   (∃la,c',d',lb,lc.c' ≠ d' ∧
 851     〈b,false〉::bs = la@〈c',false〉::lb ∧
 852     〈b0,false〉::b0s = la@〈d',false〉::lc ∧
 853     t2 = midtape (FinProd … FSUnialpha FinBool) (reverse ? la@
 854                     reverse ? l1@
 855                     〈grid,false〉::
 856                     reverse ? lb@
 857                     〈c',true〉::
 858                     reverse ? la@ls)
 859                     〈d',false〉 (lc@〈comma,false〉::l2)).
 860
 861 lemma list_ind2 :
 862   ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
 863   length ? l1 = length ? l2 →
 864   (P [] []) →
 865   (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) →
 866   P l1 l2.
 867 #T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
 868 generalize in match Hl; generalize in match l2;
 869 elim l1
 870 [#l2 cases l2 // normalize #t2 #tl2 #H destruct
 871 |#t1 #tl1 #IH #l2 cases l2
 872    [normalize #H destruct
 873    |#t2 #tl2 #H @Pcons @IH normalize in H; destruct // ]
 874 ]
 875 qed.
 876
 877 lemma list_cases_2 :
 878   ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:Prop.
 879   length ? l1 = length ? l2 →
 880   (l1 = [] → l2 = [] → P) →
 881   (∀hd1,hd2,tl1,tl2.l1 = hd1::tl1 → l2 = hd2::tl2 → P) → P.
 882 #T1 #T2 #l1 #l2 #P #Hl @(list_ind2 … Hl)
 883 [ #Pnil #Pcons @Pnil //
 884 | #tl1 #tl2 #hd1 #hd2 #IH1 #IH2 #Hp @Hp // ]
 885 qed.
 886
 887 lemma wsem_compare : WRealize ? compare R_compare.
 888 #t #i #outc #Hloop
 889 lapply (sem_while ?????? sem_comp_step t i outc Hloop) [%]
 890 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 891 [ #tapea whd in ⊢ (%→?); #Hsem #ls #c #rs #Htapea %
 892   [ %
 893     [ #Hc lapply (Hsem … Htapea) -Hsem * >Hc
 894       whd in ⊢ (??%?→?); #Hfalse destruct (Hfalse)
 895     | #c' #Hc lapply (Hsem … Htapea) -Hsem * #_
 896       #Htrue @Htrue ]
 897   | #b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1 #Hc
 898     cases (Hsem … Htapea) -Hsem >Hc whd in ⊢ (??%?→?);#Hfalse destruct (Hfalse)
 899   ]
 900 | #tapea #tapeb #tapec #Hleft #Hright #IH #Htapec lapply (IH Htapec) -IH #IH
 901   whd in Hleft; #ls #c #rs #Htapea cases (Hleft … Htapea) -Hleft
 902   #c' * #Hc destruct (Hc) *
 903   [ * #Hc' STOP cases tapeb
 904     [
 905
 906    @(list_cases_2 … Hlen)
 907     [ #Hbs #Hb0s destruct (Hbs Hb0s)
 908       cases (Htapeb grid l1 b0 comma l2 (refl ??) ?) -Htapeb
 909       [ * #Hb0c #Htapeb % %
 910         [ >Hb0c %
 911         | #l3 #c0 #Hl3 whd in Htapec;
 912
 913
 914    %
 915   [ %
 916     [ #Hc destruct (Hc)
 917   #b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1
 918   #Htapea cases (Hleft … Htapea) -Hleft
 919   #c * #Hc destruct (Hc) *
 920   [ * #Hc #Htapeb @(list_cases_2 … Hlen)
 921     [ #Hbs #Hb0s destruct (Hbs Hb0s)
 922       cases (Htapeb grid l1 b0 comma l2 (refl ??) ?) -Htapeb
 923       [ * #Hb0c #Htapeb % %
 924         [ >Hb0c %
 925         | #l3 #c0 #Hl3 whd in Htapec;
 926
 927
 928                 =midtape (FinProd FSUnialpha FinBool) l0 〈b,true〉
 929                  (bs@〈grid,false〉::l1@〈b0,true〉::b0s@〈comma,false〉::l2)
 930           cases (IH … Htapeb)
 931
 932
 933    #Hc
 934   lapply (IH HRfalse) -IH #IH
 935   #ls #c #rs #Htapea %2
 936   cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
 937
 938   >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
 939   [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
 940     cases (IH … Htapeb)
 941     [ * #_ #Houtc >Houtc >Htapeb %
 942     | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
 943   | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
 944     cases (IH … Htapeb)
 945     [ * #Hfalse >(Hmemb …) in Hfalse;
 946       [ #Hft destruct (Hft)
 947       | @memb_hd ]
 948     | * #Htestr1 #H1 >reverse_cons >associative_append
 949       @H1 // #x #Hx @Hmemb @memb_cons //
 950     ]
 951   ]
 952 qed.
 953
 954
 955
 956 (*
 957 l0 x* a l1 x0* a0 l2 ------> l0 x a* l1 x0 a0* l2
 958    ^                               ^
 959
 960 if current (* x *) = #
 961    then
 962    else if x = 0
 963       then move_right; ----
 964            adv_to_mark_r;
 965            if current (* x0 *) = 0
 966               then advance_mark ----
 967                    adv_to_mark_l;
 968                    advance_mark
 969               else STOP
 970       else x = 1 (* analogo *)
 971
 972 *)
 973
 974
 975 (*
 976    MARK NEXT TUPLE machine
 977    (partially axiomatized)
 978
 979    marks the first character after the first bar (rightwards)
 980  *)
 981
 982 axiom myalpha : FinSet.
 983 axiom is_bar : FinProd … myalpha FinBool → bool.
 984 axiom is_grid : FinProd … myalpha FinBool → bool.
 985 definition bar_or_grid ≝ λc.is_bar c ∨ is_grid c.
 986 axiom bar : FinProd … myalpha FinBool.
 987 axiom grid : FinProd … myalpha FinBool.
 988
 989 definition mark_next_tuple ≝
 990   seq ? (adv_to_mark_r ? bar_or_grid)
 991      (ifTM ? (test_char ? is_bar)
 992        (move_r_and_mark ?) (nop ?) 1).
 993
 994 definition R_mark_next_tuple ≝
 995   λt1,t2.
 996     ∀ls,c,rs1,rs2.
 997     (* c non può essere un separatore ... speriamo *)
 998     t1 = midtape ? ls c (rs1@grid::rs2) →
 999     memb ? grid rs1 = false → bar_or_grid c = false →
1000     (∃rs3,rs4,d,b.rs1 = rs3 @ bar :: rs4 ∧
1001       memb ? bar rs3 = false ∧
1002       Some ? 〈d,b〉 = option_hd ? (rs4@grid::rs2) ∧
1003       t2 = midtape ? (bar::reverse ? rs3@c::ls) 〈d,true〉 (tail ? (rs4@grid::rs2)))
1004     ∨
1005     (memb ? bar rs1 = false ∧
1006      t2 = midtape ? (reverse ? rs1@c::ls) grid rs2).
1007
1008 axiom tech_split :
1009   ∀A:DeqSet.∀f,l.
1010    (∀x.memb A x l = true → f x = false) ∨
1011    (∃l1,c,l2.f c = true ∧ l = l1@c::l2 ∧ ∀x.memb ? x l1 = true → f c = false).
1012 (*#A #f #l elim l
1013 [ % #x normalize #Hfalse *)
1014
1015 theorem sem_mark_next_tuple :
1016   Realize ? mark_next_tuple R_mark_next_tuple.
1017 #intape
1018 lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid)
1019          (ifTM ? (test_char ? is_bar) (mark ?) (nop ?) 1) ????)
1020 [@sem_if //
1021 | //
1022 |||#Hif cases (Hif intape) -Hif
1023    #j * #outc * #Hloop * #ta * #Hleft #Hright
1024    @(ex_intro ?? j) @ex_intro [|% [@Hloop] ]
1025    -Hloop
1026    #ls #c #rs1 #rs2 #Hrs #Hrs1 #Hc
1027    cases (Hleft … Hrs)
1028    [ * #Hfalse >Hfalse in Hc; #Htf destruct (Htf)
1029    | * #_ #Hta cases (tech_split ? is_bar rs1)
1030      [ #H1 lapply (Hta rs1 grid rs2 (refl ??) ? ?)
1031        [ (* Hrs1, H1 *) @daemon
1032        | (* bar_or_grid grid = true *) @daemon
1033        | -Hta #Hta cases Hright
1034          [ * #tb * whd in ⊢ (%→?); #Hcurrent
1035            @False_ind cases(Hcurrent grid ?)
1036            [ #Hfalse (* grid is not a bar *) @daemon
1037            | >Hta % ]
1038          | * #tb * whd in ⊢ (%→?); #Hcurrent
1039            cases (Hcurrent grid ?)
1040            [  #_ #Htb whd in ⊢ (%→?); #Houtc
1041              %2 %
1042              [ (* H1 *) @daemon
1043              | >Houtc >Htb >Hta % ]
1044            | >Hta % ]
1045          ]
1046        ]
1047     | * #rs3 * #c0 * #rs4 * * #Hc0 #Hsplit #Hrs3
1048       % @(ex_intro ?? rs3) @(ex_intro ?? rs4)
1049      lapply (Hta rs3 c0 (rs4@grid::rs2) ???)
1050      [ #x #Hrs3' (* Hrs1, Hrs3, Hsplit *) @daemon
1051      | (* bar → bar_or_grid *) @daemon
1052      | >Hsplit >associative_append % ] -Hta #Hta
1053        cases Hright
1054        [ * #tb * whd in ⊢ (%→?); #Hta'
1055          whd in ⊢ (%→?); #Htb
1056          cases (Hta' c0 ?)
1057          [ #_ #Htb' >Htb' in Htb; #Htb
1058            generalize in match Hsplit; -Hsplit
1059            cases rs4 in Hta;
1060            [ >(eq_pair_fst_snd … grid)
1061              #Hta #Hsplit >(Htb … Hta)
1062              >(?:c0 = bar)
1063              [ @(ex_intro ?? (\fst grid)) @(ex_intro ?? (\snd grid))
1064                % [ % [ % [ (* Hsplit *) @daemon |(*Hrs3*) @daemon ] | % ] | % ]
1065                      | (* Hc0 *) @daemon ]
1066            | #r5 #rs5 >(eq_pair_fst_snd … r5)
1067              #Hta #Hsplit >(Htb … Hta)
1068              >(?:c0 = bar)
1069              [ @(ex_intro ?? (\fst r5)) @(ex_intro ?? (\snd r5))
1070                % [ % [ % [ (* Hc0, Hsplit *) @daemon | (*Hrs3*) @daemon ] | % ]
1071                      | % ] | (* Hc0 *) @daemon ] ] | >Hta % ]
1072              | * #tb * whd in ⊢ (%→?); #Hta'
1073                whd in ⊢ (%→?); #Htb
1074                cases (Hta' c0 ?)
1075                [ #Hfalse @False_ind >Hfalse in Hc0;
1076                  #Hc0 destruct (Hc0)
1077                | >Hta % ]
1078 ]]]]
1079 qed.