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/alphabet.ma".
  20 include "turing/universal/tests.ma".
  21
  22 (* ADVANCE TO MARK (right)
  23
  24    sposta la testina a destra fino a raggiungere il primo carattere marcato
  25
  26 *)
  27
  28 (* 0, a ≠ mark _ ⇒ 0, R
  29 0, a = mark _ ⇒ 1, N *)
  30
  31 definition atm_states ≝ initN 3.
  32
  33 definition atm0 : atm_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
  34 definition atm1 : atm_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
  35 definition atm2 : atm_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
  36
  37 definition atmr_step ≝
  38   λalpha:FinSet.λtest:alpha→bool.
  39   mk_TM alpha atm_states
  40   (λp.let 〈q,a〉 ≝ p in
  41    match a with
  42    [ None ⇒ 〈atm1, None ?〉
  43    | Some a' ⇒
  44      match test a' with
  45      [ true ⇒ 〈atm1,None ?〉
  46      | false ⇒ 〈atm2,Some ? 〈a',R〉〉 ]])
  47   atm0 (λx.notb (x == atm0)).
  48
  49 definition Ratmr_step_true ≝
  50   λalpha,test,t1,t2.
  51    ∃ls,a,rs.
  52    t1 = midtape alpha ls a rs ∧ test a = false ∧
  53    t2 = mk_tape alpha (a::ls) (option_hd ? rs) (tail ? rs).
  54
  55 definition Ratmr_step_false ≝
  56   λalpha,test,t1,t2.
  57     t1 = t2 ∧
  58     (current alpha t1 = None ? ∨
  59      (∃a.current ? t1 = Some ? a ∧ test a = true)).
  60
  61 lemma atmr_q0_q1 :
  62   ∀alpha,test,ls,a0,rs. test a0 = true →
  63   step alpha (atmr_step alpha test)
  64     (mk_config ?? atm0 (midtape … ls a0 rs)) =
  65   mk_config alpha (states ? (atmr_step alpha test)) atm1
  66     (midtape … ls a0 rs).
  67 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
  68 whd in match (trans … 〈?,?〉); >Htest %
  69 qed.
  70
  71 lemma atmr_q0_q2 :
  72   ∀alpha,test,ls,a0,rs. test a0 = false →
  73   step alpha (atmr_step alpha test)
  74     (mk_config ?? atm0 (midtape … ls a0 rs)) =
  75   mk_config alpha (states ? (atmr_step alpha test)) atm2
  76     (mk_tape … (a0::ls) (option_hd ? rs) (tail ? rs)).
  77 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
  78 whd in match (trans … 〈?,?〉); >Htest cases ts //
  79 qed.
  80
  81 lemma sem_atmr_step :
  82   ∀alpha,test.
  83   accRealize alpha (atmr_step alpha test)
  84     atm2 (Ratmr_step_true alpha test) (Ratmr_step_false alpha test).
  85 #alpha #test *
  86 [ @(ex_intro ?? 2)
  87   @(ex_intro ?? (mk_config ?? atm1 (niltape ?))) %
  88   [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
  89 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (leftof ? a al)))
  90   % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
  91 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (rightof ? a al)))
  92   % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
  93 | #ls #c #rs @(ex_intro ?? 2)
  94   cases (true_or_false (test c)) #Htest
  95   [ @(ex_intro ?? (mk_config ?? atm1 ?))
  96     [| %
  97       [ %
  98         [ whd in ⊢ (??%?); >atmr_q0_q1 //
  99         | whd in ⊢ ((??%%)→?); #Hfalse destruct ]
 100       | #_ % // %2 @(ex_intro ?? c) % // ]
 101     ]
 102   | @(ex_intro ?? (mk_config ?? atm2 (mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs))))
 103     %
 104     [ %
 105       [ whd in ⊢ (??%?); >atmr_q0_q2 //
 106       | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
 107         % // % //
 108       ]
 109     | #Hfalse @False_ind @(absurd ?? Hfalse) %
 110     ]
 111   ]
 112 ]
 113 qed.
 114
 115 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
 116   ∀ls,c,rs.
 117   (t1 = midtape alpha ls c rs  →
 118   ((test c = true ∧ t2 = t1) ∨
 119    (test c = false ∧
 120     ∀rs1,b,rs2. rs = rs1@b::rs2 →
 121      test b = true → (∀x.memb ? x rs1 = true → test x = false) →
 122      t2 = midtape ? (reverse ? rs1@c::ls) b rs2))).
 123
 124 definition adv_to_mark_r ≝
 125   λalpha,test.whileTM alpha (atmr_step alpha test) atm2.
 126
 127 lemma wsem_adv_to_mark_r :
 128   ∀alpha,test.
 129   WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
 130 #alpha #test #t #i #outc #Hloop
 131 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
 132 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 133 [ #tapea * #Htapea *
 134   [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
 135     #Hfalse destruct (Hfalse)
 136   | * #a * #Ha #Htest #ls #c #rs #H2 %
 137     >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
 138     <Htapea //
 139   ]
 140 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
 141   lapply (IH HRfalse) -IH #IH
 142   #ls #c #rs #Htapea %2
 143   cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
 144
 145   >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
 146   [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
 147     cases (IH … Htapeb)
 148     [ * #_ #Houtc >Houtc >Htapeb %
 149     | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
 150   | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
 151     cases (IH … Htapeb)
 152     [ * #Hfalse >(Hmemb …) in Hfalse;
 153       [ #Hft destruct (Hft)
 154       | @memb_hd ]
 155     | * #Htestr1 #H1 >reverse_cons >associative_append
 156       @H1 // #x #Hx @Hmemb @memb_cons //
 157     ]
 158   ]
 159 qed.
 160
 161 lemma terminate_adv_to_mark_r :
 162   ∀alpha,test.
 163   ∀t.Terminate alpha (adv_to_mark_r alpha test) t.
 164 #alpha #test #t
 165 @(terminate_while … (sem_atmr_step alpha test))
 166   [ %
 167   | cases t
 168     [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 169     |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 170     | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
 171       elim rs
 172       [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 173        #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 174        % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
 175        normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
 176       | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 177         #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 178         >Ht1 @IH
 179       ]
 180     ]
 181   ]
 182 qed.
 183
 184 lemma sem_adv_to_mark_r :
 185   ∀alpha,test.
 186   Realize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
 187 /2/
 188 qed.
 189
 190 (* MARK machine
 191
 192    marks the current character
 193  *)
 194
 195 definition mark_states ≝ initN 2.
 196
 197 definition ms0 : mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
 198 definition ms1 : mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
 199
 200 definition mark ≝
 201   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
 202   (λp.let 〈q,a〉 ≝ p in
 203     match a with
 204     [ None ⇒ 〈ms1,None ?〉
 205     | Some a' ⇒ match (pi1 … q) with
 206       [ O ⇒ let 〈a'',b〉 ≝ a' in 〈ms1,Some ? 〈〈a'',true〉,N〉〉
 207       | S q ⇒ 〈ms1,None ?〉 ] ])
 208   ms0 (λq.q == ms1).
 209
 210 definition R_mark ≝ λalpha,t1,t2.
 211   ∀ls,c,b,rs.
 212   t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
 213   t2 = midtape ? ls 〈c,true〉 rs.
 214
 215 lemma sem_mark :
 216   ∀alpha.Realize ? (mark alpha) (R_mark alpha).
 217 #alpha #intape @(ex_intro ?? 2) cases intape
 218 [ @ex_intro
 219   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 220 |#a #al @ex_intro
 221   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 222 |#a #al @ex_intro
 223   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 224 | #ls * #c #b #rs
 225   @ex_intro [| % [ % | #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ] ] ]
 226 qed.
 227
 228 (* MOVE RIGHT
 229
 230    moves the head one step to the right
 231
 232 *)
 233
 234 definition move_states ≝ initN 2.
 235 definition move0 : move_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
 236 definition move1 : move_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
 237
 238 definition move_r ≝
 239   λalpha:FinSet.mk_TM alpha move_states
 240   (λp.let 〈q,a〉 ≝ p in
 241     match a with
 242     [ None ⇒ 〈move1,None ?〉
 243     | Some a' ⇒ match (pi1 … q) with
 244       [ O ⇒ 〈move1,Some ? 〈a',R〉〉
 245       | S q ⇒ 〈move1,None ?〉 ] ])
 246   move0 (λq.q == move1).
 247
 248 definition R_move_r ≝ λalpha,t1,t2.
 249   ∀ls,c,rs.
 250   t1 = midtape alpha ls c rs →
 251   t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
 252
 253 lemma sem_move_r :
 254   ∀alpha.Realize ? (move_r alpha) (R_move_r alpha).
 255 #alpha #intape @(ex_intro ?? 2) cases intape
 256 [ @ex_intro
 257   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
 258 |#a #al @ex_intro
 259   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
 260 |#a #al @ex_intro
 261   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
 262 | #ls #c #rs
 263   @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
 264   cases rs0 // ] ] ]
 265 qed.
 266
 267 (* MOVE LEFT
 268
 269    moves the head one step to the right
 270
 271 *)
 272
 273 definition move_l ≝
 274   λalpha:FinSet.mk_TM alpha move_states
 275   (λp.let 〈q,a〉 ≝ p in
 276     match a with
 277     [ None ⇒ 〈move1,None ?〉
 278     | Some a' ⇒ match pi1 … q with
 279       [ O ⇒ 〈move1,Some ? 〈a',L〉〉
 280       | S q ⇒ 〈move1,None ?〉 ] ])
 281   move0 (λq.q == move1).
 282
 283 definition R_move_l ≝ λalpha,t1,t2.
 284   ∀ls,c,rs.
 285   t1 = midtape alpha ls c rs →
 286   t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
 287
 288 lemma sem_move_l :
 289   ∀alpha.Realize ? (move_l alpha) (R_move_l alpha).
 290 #alpha #intape @(ex_intro ?? 2) cases intape
 291 [ @ex_intro
 292   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
 293 |#a #al @ex_intro
 294   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
 295 |#a #al @ex_intro
 296   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
 297 | #ls #c #rs
 298   @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
 299   cases ls0 // ] ] ]
 300 qed.
 301
 302 (* MOVE RIGHT AND MARK machine
 303
 304    marks the first character on the right
 305
 306    (could be rewritten using (mark; move_right))
 307  *)
 308
 309 definition mrm_states ≝ initN 3.
 310
 311 definition mrm0 : mrm_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
 312 definition mrm1 : mrm_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
 313 definition mrm2 : mrm_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
 314
 315 definition move_right_and_mark ≝
 316   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mrm_states
 317   (λp.let 〈q,a〉 ≝ p in
 318     match a with
 319     [ None ⇒ 〈mrm2,None ?〉
 320     | Some a' ⇒ match pi1 … q with
 321       [ O ⇒ 〈mrm1,Some ? 〈a',R〉〉
 322       | S q ⇒ match q with
 323         [ O ⇒ let 〈a'',b〉 ≝ a' in
 324               〈mrm2,Some ? 〈〈a'',true〉,N〉〉
 325         | S _ ⇒ 〈mrm2,None ?〉 ] ] ])
 326   mrm0 (λq.q == mrm2).
 327
 328 definition R_move_right_and_mark ≝ λalpha,t1,t2.
 329   ∀ls,c,d,b,rs.
 330   t1 = midtape (FinProd … alpha FinBool) ls c (〈d,b〉::rs) →
 331   t2 = midtape ? (c::ls) 〈d,true〉 rs.
 332
 333 lemma sem_move_right_and_mark :
 334   ∀alpha.Realize ? (move_right_and_mark alpha) (R_move_right_and_mark alpha).
 335 #alpha #intape @(ex_intro ?? 3) cases intape
 336 [ @ex_intro
 337   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 338 |#a #al @ex_intro
 339   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 340 |#a #al @ex_intro
 341   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 342 | #ls #c *
 343   [ @ex_intro [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #Hfalse destruct ] ]
 344   | * #d #b #rs @ex_intro
 345     [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #H1 destruct (H1) % ] ] ] ]
 346 qed.
 347
 348 (* CLEAR MARK machine
 349
 350    clears the mark in the current character
 351  *)
 352
 353 definition clear_mark_states ≝ initN 3.
 354
 355 definition clear0 : clear_mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
 356 definition clear1 : clear_mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
 357 definition claer2 : clear_mark_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
 358
 359 definition clear_mark ≝
 360   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) clear_mark_states
 361   (λp.let 〈q,a〉 ≝ p in
 362     match a with
 363     [ None ⇒ 〈clear1,None ?〉
 364     | Some a' ⇒ match pi1 … q with
 365       [ O ⇒ let 〈a'',b〉 ≝ a' in 〈clear1,Some ? 〈〈a'',false〉,N〉〉
 366       | S q ⇒ 〈clear1,None ?〉 ] ])
 367   clear0 (λq.q == clear1).
 368
 369 definition R_clear_mark ≝ λalpha,t1,t2.
 370   ∀ls,c,b,rs.
 371   t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
 372   t2 = midtape ? ls 〈c,false〉 rs.
 373
 374 lemma sem_clear_mark :
 375   ∀alpha.Realize ? (clear_mark alpha) (R_clear_mark alpha).
 376 #alpha #intape @(ex_intro ?? 2) cases intape
 377 [ @ex_intro
 378   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 379 |#a #al @ex_intro
 380   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 381 |#a #al @ex_intro
 382   [| % [ % | #ls #c #b #rs #Hfalse destruct ] ]
 383 | #ls * #c #b #rs
 384   @ex_intro [| % [ % | #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ] ] ]
 385 qed.
 386
 387 (* ADVANCE MARK RIGHT machine
 388
 389    clears mark on current char,
 390    moves right, and marks new current char
 391
 392 *)
 393
 394 definition adv_mark_r ≝
 395   λalpha:FinSet.
 396     seq ? (clear_mark alpha)
 397       (seq ? (move_r ?) (mark alpha)).
 398
 399 definition R_adv_mark_r ≝ λalpha,t1,t2.
 400   ∀ls,c,d,b,rs.
 401   t1 = midtape (FinProd … alpha FinBool) ls 〈c,true〉 (〈d,b〉::rs) →
 402   t2 = midtape ? (〈c,false〉::ls) 〈d,true〉 rs.
 403
 404 lemma sem_adv_mark_r :
 405   ∀alpha.Realize ? (adv_mark_r alpha) (R_adv_mark_r alpha).
 406 #alpha #intape
 407 cases (sem_seq ????? (sem_clear_mark …)
 408          (sem_seq ????? (sem_move_r ?) (sem_mark alpha)) intape)
 409 #k * #outc * #Hloop whd in ⊢ (%→?);
 410 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→%→?); #Hs2 #Hs3
 411 @(ex_intro ?? k) @(ex_intro ?? outc) %
 412 [ @Hloop
 413 | -Hloop #ls #c #d #b #rs #Hintape @(Hs3 … b)
 414   @(Hs2 ls 〈c,false〉 (〈d,b〉::rs))
 415   @(Hs1 … Hintape)
 416 ]
 417 qed.
 418
 419 (* ADVANCE TO MARK (left)
 420
 421 axiomatized
 422
 423 *)
 424
 425 definition R_adv_to_mark_l ≝ λalpha,test,t1,t2.
 426   ∀ls,c,rs.
 427   (t1 = midtape alpha ls c rs  →
 428   ((test c = true ∧ t2 = t1) ∨
 429    (test c = false ∧
 430     ∀ls1,b,ls2. ls = ls1@b::ls2 →
 431      test b = true → (∀x.memb ? x ls1 = true → test x = false) →
 432      t2 = midtape ? ls2 b (reverse ? ls1@c::rs)))).
 433
 434 axiom adv_to_mark_l : ∀alpha:FinSet.(alpha → bool) → TM alpha.
 435 (* definition adv_to_mark_l ≝
 436   λalpha,test.whileTM alpha (atml_step alpha test) 2. *)
 437
 438 axiom wsem_adv_to_mark_l :
 439   ∀alpha,test.
 440   WRealize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
 441 (*
 442 #alpha #test #t #i #outc #Hloop
 443 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
 444 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 445 [ #tapea * #Htapea *
 446   [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
 447     #Hfalse destruct (Hfalse)
 448   | * #a * #Ha #Htest #ls #c #rs #H2 %
 449     >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
 450     <Htapea //
 451   ]
 452 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
 453   lapply (IH HRfalse) -IH #IH
 454   #ls #c #rs #Htapea %2
 455   cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
 456
 457   >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
 458   [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
 459     cases (IH … Htapeb)
 460     [ * #_ #Houtc >Houtc >Htapeb %
 461     | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
 462   | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
 463     cases (IH … Htapeb)
 464     [ * #Hfalse >(Hmemb …) in Hfalse;
 465       [ #Hft destruct (Hft)
 466       | @memb_hd ]
 467     | * #Htestr1 #H1 >reverse_cons >associative_append
 468       @H1 // #x #Hx @Hmemb @memb_cons //
 469     ]
 470   ]
 471 qed.
 472 *)
 473
 474 axiom terminate_adv_to_mark_l :
 475   ∀alpha,test.
 476   ∀t.Terminate alpha (adv_to_mark_l alpha test) t.
 477 (*
 478 #alpha #test #t
 479 @(terminate_while … (sem_atmr_step alpha test))
 480   [ %
 481   | cases t
 482     [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 483     |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 484     | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
 485       elim rs
 486       [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 487        #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 488        % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
 489        normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
 490       | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 491         #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 492         >Ht1 @IH
 493       ]
 494     ]
 495   ]
 496 qed.
 497 *)
 498
 499 lemma sem_adv_to_mark_l :
 500   ∀alpha,test.
 501   Realize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
 502 /2/
 503 qed.
 504
 505 (*
 506    ADVANCE BOTH MARKS machine
 507
 508    l1 does not contain marks ⇒
 509
 510
 511    input:
 512    l0 x* a l1 x0* a0 l2
 513               ^
 514
 515    output:
 516    l0 x a* l1 x0 a0* l2
 517         ^
 518 *)
 519
 520 definition is_marked ≝
 521   λalpha.λp:FinProd … alpha FinBool.
 522   let 〈x,b〉 ≝ p in b.
 523
 524 definition adv_both_marks ≝
 525   λalpha.seq ? (adv_mark_r alpha)
 526     (seq ? (move_l ?)
 527      (seq ? (adv_to_mark_l (FinProd alpha FinBool) (is_marked alpha))
 528        (adv_mark_r alpha))).
 529
 530 definition R_adv_both_marks ≝
 531   λalpha,t1,t2.
 532     ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
 533     t1 = midtape (FinProd … alpha FinBool)
 534         (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
 535     t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2).
 536
 537 lemma sem_adv_both_marks :
 538   ∀alpha.Realize ? (adv_both_marks alpha) (R_adv_both_marks alpha).
 539 #alpha #intape
 540 cases (sem_seq ????? (sem_adv_mark_r …)
 541         (sem_seq ????? (sem_move_l …)
 542           (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?))
 543             (sem_adv_mark_r alpha))) intape)
 544 #k * #outc * #Hloop whd in ⊢ (%→?);
 545 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→?); #Hs2
 546 * #tc * whd in ⊢ (%→%→?); #Hs3 #Hs4
 547 @(ex_intro ?? k) @(ex_intro ?? outc) %
 548 [ @Hloop
 549 | -Hloop #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
 550   @(Hs4 … false) -Hs4
 551   lapply (Hs1 … Hintape) #Hta
 552   lapply (Hs2 … Hta) #Htb
 553   cases (Hs3 … Htb)
 554   [ * #Hfalse normalize in Hfalse; destruct (Hfalse)
 555   | * #_ -Hs3 #Hs3
 556     lapply (Hs3 (l1@[〈a,false〉]) 〈x,true〉 l0 ???)
 557     [ #x1 #Hx1 cases (memb_append … Hx1)
 558       [ @Hl1
 559       | #Hx1' >(memb_single … Hx1') % ]
 560     | %
 561     | >associative_append %
 562     | >reverse_append #Htc @Htc ]
 563   ]
 564 qed.
 565
 566 (*
 567    MATCH AND ADVANCE(f)
 568
 569    input:
 570    l0 x* a l1 x0* a0 l2
 571               ^
 572
 573    output:
 574    l0 x a* l1 x0 a0* l2   (f(x0) == true)
 575         ^
 576    l0 x* a l1 x0* a0 l2   (f(x0) == false)
 577               ^
 578 *)
 579
 580 definition match_and_adv ≝
 581   λalpha,f.ifTM ? (test_char ? f)
 582      (adv_both_marks alpha) (clear_mark ?) tc_true.
 583
 584 definition R_match_and_adv ≝
 585   λalpha,f,t1,t2.
 586     ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
 587     t1 = midtape (FinProd … alpha FinBool)
 588         (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
 589     (f 〈x0,true〉 = true ∧ t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2))
 590     ∨ (f 〈x0,true〉 = false ∧
 591     t2 = midtape ? (l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)).
 592
 593 lemma sem_match_and_adv :
 594   ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv alpha f).
 595 #alpha #f #intape
 596 cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape)
 597 #k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
 598 % [ @Hloop ] -Hloop
 599 cases Hif
 600 [ * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
 601   #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
 602   >Hintape in Hta; #Hta cases (Hta … (refl ??)) -Hta #Hf #Hta % %
 603   [ @Hf | @Houtc [ @Hl1 | @Hta ] ]
 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 %2 %
 607   [ @Hf | >(Houtc … Hta) % ]
 608 ]
 609 qed.
 610
 611 (*
 612  if x = c
 613       then move_right; ----
 614            adv_to_mark_r;
 615            if current (* x0 *) = 0
 616               then advance_mark ----
 617                    adv_to_mark_l;
 618                    advance_mark
 619               else STOP
 620       else M
 621 *)
 622
 623 definition comp_step_subcase ≝
 624   λalpha,c,elseM.ifTM ? (test_char ? (λx.x == c))
 625     (seq ? (move_r …)
 626       (seq ? (adv_to_mark_r ? (is_marked alpha))
 627       (match_and_adv ? (λx.x == c))))
 628     elseM tc_true.
 629
 630 definition R_comp_step_subcase ≝
 631   λalpha,c,RelseM,t1,t2.
 632     ∀l0,x,rs.t1 = midtape (FinProd … alpha FinBool) l0 〈x,true〉 rs →
 633     (〈x,true〉 = c ∧
 634      ∀a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
 635      rs = 〈a,false〉::l1@〈x0,true〉::〈a0,false〉::l2 →
 636      ((x = x0 ∧
 637       t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1@〈x0,false〉::〈a0,true〉::l2)) ∨
 638       (x ≠ x0 ∧
 639       t2 = midtape (FinProd … alpha FinBool)
 640         (reverse ? l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)))) ∨
 641     (〈x,true〉 ≠ c ∧ RelseM t1 t2).
 642
 643 lemma sem_comp_step_subcase :
 644   ∀alpha,c,elseM,RelseM.
 645   Realize ? elseM RelseM →
 646   Realize ? (comp_step_subcase alpha c elseM)
 647     (R_comp_step_subcase alpha c RelseM).
 648 #alpha #c #elseM #RelseM #Helse #intape
 649 cases (sem_if ? (test_char ? (λx.x == c)) … tc_true
 650         (sem_test_char ? (λx.x == c))
 651         (sem_seq ????? (sem_move_r …)
 652           (sem_seq ????? (sem_adv_to_mark_r ? (is_marked alpha))
 653              (sem_match_and_adv ? (λx.x == c)))) Helse intape)
 654 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc)
 655 % [ @Hloop ] -Hloop cases HR -HR
 656 [ * #ta * whd in ⊢ (%→?); #Hta * #tb * whd in ⊢ (%→?); #Htb
 657   * #tc * whd in ⊢ (%→?); #Htc whd in ⊢ (%→?); #Houtc
 658   #l0 #x #rs #Hintape cases (true_or_false (〈x,true〉==c)) #Hc
 659   [ % % [ @(\P Hc) ]
 660     #a #l1 #x0 #a0 #l2 #Hl1 #Hrs >Hrs in Hintape; #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 Hx0) in Hx; #Hx lapply (\P Hx) #Hx' destruct (Hx') %
 668         | >Houtc >reverse_reverse % ]
 669     | * #Hx0 #Houtc %2
 670       % [ <(\P Hx) in Hx0; #Hx0 lapply (\Pf Hx0) @not_to_not #Hx' >Hx' %
 671         | >Houtc % ]
 672     | (* members of lists are invariant under reverse *) @daemon ]
 673   | %2 % [ @(\Pf Hc) ]
 674     >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hx #Hta
 675     >Hx in Hc;#Hc destruct (Hc) ]
 676 | * #ta * whd in ⊢ (%→?); #Hta #Helse #ls #c0 #rs #Hintape %2
 677   >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hc #Hta %
 678   [ @(\Pf Hc) | <Hta @Helse ]
 679 ]
 680 qed.
 681
 682 (*
 683 - se marcato, itero
 684 - se non è marcato
 685   + se è un bit, ho fallito il confronto della tupla corrente
 686   + se è un separatore, la tupla fa match
 687
 688
 689 ifTM ? (test_char ? is_marked)
 690   (single_finalTM … (comp_step_subcase unialpha 〈bit false,true〉
 691     (comp_step_subcase unialpha 〈bit true,true〉
 692       (clear_mark …))))
 693   (nop ?)
 694 *)
 695
 696 definition comp_step ≝
 697   ifTM ? (test_char ? (is_marked ?))
 698   (single_finalTM … (comp_step_subcase FSUnialpha 〈bit false,true〉
 699     (comp_step_subcase FSUnialpha 〈bit true,true〉
 700       (comp_step_subcase FSUnialpha 〈null,true〉
 701         (clear_mark …)))))
 702   (nop ?)
 703   tc_true.
 704
 705 definition R_comp_step_true ≝
 706   λt1,t2.
 707     ∀l0,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) l0 c rs →
 708     ∃c'. c = 〈c',true〉 ∧
 709     ((bit_or_null c' = true ∧
 710      ∀a,l1,c0,a0,l2.
 711       rs = 〈a,false〉::l1@〈c0,true〉::〈a0,false〉::l2 →
 712       (∀c.memb ? c l1 = true → is_marked ? c = false) →
 713       (c0 = c' ∧
 714        t2 = midtape ? (〈c',false〉::l0) 〈a,true〉 (l1@〈c0,false〉::〈a0,true〉::l2)) ∨
 715       (c0 ≠ c' ∧
 716        t2 = midtape (FinProd … FSUnialpha FinBool)
 717         (reverse ? l1@〈a,false〉::〈c',true〉::l0) 〈c0,false〉 (〈a0,false〉::l2))) ∨
 718      (bit_or_null c' = false ∧ t2 = midtape ? l0 〈c',false〉 rs)).
 719
 720 definition R_comp_step_false ≝
 721   λt1,t2.
 722    ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
 723    is_marked ? c = false ∧ t2 = t1.
 724
 725 lemma sem_comp_step :
 726   accRealize ? comp_step (inr … (inl … (inr … start_nop)))
 727     R_comp_step_true R_comp_step_false.
 728 #intape
 729 cases (acc_sem_if … (sem_test_char ? (is_marked ?))
 730         (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
 731           (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ??
 732             (sem_comp_step_subcase FSUnialpha 〈null,true〉 ??
 733               (sem_clear_mark …))))
 734         (sem_nop …) intape)
 735 #k * #outc * * #Hloop #H1 #H2
 736 @(ex_intro ?? k) @(ex_intro ?? outc) %
 737 [ % [@Hloop ] ] -Hloop
 738 [ #Hstate lapply (H1 Hstate) -H1 -Hstate -H2 *
 739   #ta * whd in ⊢ (%→?); #Hleft #Hright #ls #c #rs #Hintape
 740   >Hintape in Hleft; #Hleft cases (Hleft ? (refl ??)) -Hleft
 741   cases c in Hintape; #c' #b #Hintape whd in ⊢ (??%?→?);
 742   #Hb >Hb #Hta @(ex_intro ?? c') % //
 743   cases (Hright … Hta)
 744   [ * #Hc' #H1 % % [destruct (Hc') % ]
 745     #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
 746     cases (H1 … Hl1 Hrs)
 747     [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
 748     | * #Hneq #Houtc %2 %
 749       [ @sym_not_eq //
 750       | @Houtc ]
 751     ]
 752   | * #Hc #Helse1 cases (Helse1 … Hta)
 753     [ * #Hc' #H1 % % [destruct (Hc') % ]
 754       #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
 755       cases (H1 … Hl1 Hrs)
 756       [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
 757       | * #Hneq #Houtc %2 %
 758         [ @sym_not_eq //
 759         | @Houtc ]
 760       ]
 761     | * #Hc' #Helse2 cases (Helse2 … Hta)
 762       [ * #Hc'' #H1 % % [destruct (Hc'') % ]
 763         #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
 764         cases (H1 … Hl1 Hrs)
 765         [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
 766         | * #Hneq #Houtc %2 %
 767           [ @sym_not_eq //
 768           | @Houtc ]
 769         ]
 770       | * #Hc'' whd in ⊢ (%→?); #Helse3 %2 %
 771         [ generalize in match Hc''; generalize in match Hc'; generalize in match Hc;
 772           cases c'
 773           [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
 774               | #Hfalse @False_ind @(absurd ?? Hfalse) % ]
 775           | #_ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
 776           |*: #_ #_ #_ % ]
 777         | @(Helse3 … Hta)
 778         ]
 779       ]
 780     ]
 781   ]
 782 | #Hstate lapply (H2 Hstate) -H1 -Hstate -H2 *
 783   #ta * whd in ⊢ (%→%→?); #Hleft #Hright #ls #c #rs #Hintape
 784   >Hintape in Hleft; #Hleft
 785   cases (Hleft ? (refl ??)) -Hleft
 786   #Hc #Hta % // >Hright //
 787 ]
 788 qed.
 789
 790 definition compare ≝
 791   whileTM ? comp_step (inr … (inl … (inr … start_nop))).
 792
 793 (*
 794 definition R_compare :=
 795   λt1,t2.
 796   (t
 797
 798   ∀ls,c,b,rs.t1 = midtape ? ls 〈c,b〉 rs →
 799   (b = true → rs = ....) →
 800   (b = false ∧ ....) ∨
 801   (b = true ∧
 802
 803    rs = cs@l1@〈c0,true〉::cs0@l2
 804    (
 805
 806
 807   ls 〈c,b〉 cs l1 〈c0,b0〉 cs0 l2
 808
 809
 810 ACCETTAZIONE:
 811   ls (hd (Ls@〈grid,false〉))* (tail (Ls@〈grid,false〉)) l1 (hd (Ls@〈comma,false〉))* (tail (Ls@〈comma,false〉)) l2
 812      ^^^^^^^^^^^^^^^^^^^^^^^
 813
 814   ls Ls 〈grid,false〉 l1 Ls 〈comma,true〉 l2
 815         ^^^^^^^^^^^^
 816
 817 RIFIUTO: c ≠ d
 818
 819   ls (hd (Ls@〈c,false〉))* (tail (Ls@〈c,false〉)) l1 (hd (Ls@〈d,false〉))* (tail (Ls@〈d,false〉)) l2
 820      ^^^^^^^^^^^^^^^^^^^^^^^
 821
 822
 823   ls Ls 〈c,true〉 l1 Ls 〈d,false〉 l2
 824                        ^^^^^^^^
 825
 826   ).
 827
 828   |bs| = |b0s| →
 829   (∃la,d.〈b,true〉::bs = la@[〈grid,d〉] ∧ ∀x.memb ? x la → is_bit (\fst x) = true) →
 830   (∃lb,d0.〈b0,true〉::b0s = lb@[〈comma,d0〉] ∧ ∀x.memb ? x lb → is_bit (\fst x) = true) →
 831   t1 = midtape ? l0 〈b,true〉 (bs@l1@〈b0,true〉::b0s@l2 →
 832
 833   mk_tape left (option current) right
 834
 835   (b = grid ∧ b0 = comma ∧ bs = [] ∧ b0s = [] ∧
 836    t2 = midtape ? l0 〈grid,false〉 (l1@〈comma,true〉::l2)) ∨
 837   (b = bit x ∧ b = c ∧ bs = b0s
 838   *)
 839 definition R_compare :=
 840   λt1,t2.
 841   ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
 842   (∀c'.bit_or_null c' = false → c = 〈c',true〉 → t2 = midtape ? ls 〈c',false〉 rs) ∧
 843   (∀c'. c = 〈c',false〉 → t2 = t1) ∧
 844   ∀b,b0,bs,b0s,l1,l2.
 845   |bs| = |b0s| →
 846   (∀c.memb (FinProd … FSUnialpha FinBool) c bs = true → bit_or_null (\fst c) = true) →
 847   (∀c.memb (FinProd … FSUnialpha FinBool) c b0s = true → bit_or_null (\fst c) = true) →
 848   (∀c.memb ? c bs = true → is_marked ? c = false) →
 849   (∀c.memb ? c b0s = true → is_marked ? c = false) →
 850   (∀c.memb ? c l1 = true → is_marked ? c = false) →
 851   c = 〈b,true〉 → bit_or_null b = true →
 852   rs = bs@〈grid,false〉::l1@〈b0,true〉::b0s@〈comma,false〉::l2 →
 853   (〈b,true〉::bs = 〈b0,true〉::b0s ∧
 854    t2 = midtape ? (reverse ? bs@〈b,false〉::ls)
 855           〈grid,false〉 (l1@〈b0,false〉::b0s@〈comma,true〉::l2)) ∨
 856   (∃la,c',d',lb,lc.c' ≠ d' ∧
 857     〈b,false〉::bs = la@〈c',false〉::lb ∧
 858     〈b0,false〉::b0s = la@〈d',false〉::lc ∧
 859     t2 = midtape (FinProd … FSUnialpha FinBool) (reverse ? la@
 860                     reverse ? l1@
 861                     〈grid,false〉::
 862                     reverse ? lb@
 863                     〈c',true〉::
 864                     reverse ? la@ls)
 865                     〈d',false〉 (lc@〈comma,false〉::l2)).
 866
 867 lemma wsem_compare : WRealize ? compare R_compare.
 868 #t #i #outc #Hloop
 869 lapply (sem_while ?????? sem_comp_step t i outc Hloop) [%]
 870 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 871 [ #tapea whd in ⊢ (%→?); #Rfalse #ls #c #rs #Htapea %
 872   [ %
 873     [ #c' #Hc' #Hc lapply (Rfalse … Htapea) -Rfalse * >Hc
 874       whd in ⊢ (??%?→?); #Hfalse destruct (Hfalse)
 875     | #c' #Hc lapply (Rfalse … Htapea) -Rfalse * #_
 876       #Htrue @Htrue ]
 877   | #b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1 #Hc
 878     cases (Rfalse … Htapea) -Rfalse >Hc whd in ⊢ (??%?→?);#Hfalse destruct (Hfalse)
 879   ]
 880 | #tapea #tapeb #tapec #Hleft #Hright #IH #Htapec lapply (IH Htapec) -Htapec -IH #IH
 881   whd in Hleft; #ls #c #rs #Htapea cases (Hleft … Htapea) -Hleft
 882   #c' * #Hc >Hc cases (true_or_false (bit_or_null c')) #Hc'
 883   [2: *
 884     [ * >Hc' #H @False_ind destruct (H)
 885     | * #_ #Htapeb cases (IH … Htapeb) * #_ #H #_ %
 886       [%
 887         [#c1 #Hc1 #Heqc destruct (Heqc) <Htapeb @(H c1) %
 888         |#c1 #Hfalse destruct (Hfalse)
 889         ]
 890       |#b #b0 #bs #b0s #l1 #l2 #_ #_ #_ #_ #_ #_
 891        #Heq destruct (Heq) >Hc' #Hfalse @False_ind destruct (Hfalse)
 892       ]
 893     ]
 894  |#Hleft %
 895     [ %
 896       [ #c'' #Hc'' #Heq destruct (Heq) >Hc'' in Hc'; #H destruct (H)
 897       | #c0 #Hfalse destruct (Hfalse)
 898       ]
 899     |#b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1
 900      #Heq destruct (Heq) #_ #Hrs cases Hleft -Hleft
 901       [2: * >Hc' #Hfalse @False_ind destruct ] * #_
 902        @(list_cases2 … Hlen)
 903        [ #Hbs #Hb0s generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
 904        -Hrs #Hrs normalize in Hrs; #Hleft cases (Hleft ????? Hrs ?) -Hleft
 905          [ * #Heqb #Htapeb cases (IH … Htapeb) -IH * #IH #_ #_
 906           % %
 907             [ >Heqb >Hbs >Hb0s %
 908             | >Hbs >Hb0s @IH %
 909             ]
 910          |* #Hneqb #Htapeb %2
 911           @(ex_intro … [ ]) @(ex_intro … b)
 912           @(ex_intro … b0) @(ex_intro … [ ])
 913           @(ex_intro … [ ]) %
 914             [ % [ % [@sym_not_eq //| >Hbs %] | >Hb0s %]
 915             | cases (IH … Htapeb) -IH * #_ #IH #_ >(IH ? (refl ??))
 916               @Htapeb
 917             ]
 918          | @Hl1 ]
 919       | * #b' #bitb' * #b0' #bitb0' #bs' #b0s' #Hbs #Hb0s
 920         generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
 921         cut (bit_or_null b' = true ∧ bit_or_null b0' = true ∧
 922              bitb' = false ∧ bitb0' = false)
 923         [ % [ % [ % [ >Hbs in Hbs1; #Hbs1 @(Hbs1 〈b',bitb'〉) @memb_hd
 924             | >Hb0s in Hb0s1; #Hb0s1 @(Hb0s1 〈b0',bitb0'〉) @memb_hd ]
 925             | >Hbs in Hbs2; #Hbs2 @(Hbs2 〈b',bitb'〉) @memb_hd ]
 926             | >Hb0s in Hb0s2; #Hb0s2 @(Hb0s2 〈b0',bitb0'〉) @memb_hd ]
 927         | * * * #Ha #Hb #Hc #Hd >Hc >Hd
 928           #Hrs #Hleft
 929           cases (Hleft b' (bs'@〈grid,false〉::l1) b0 b0'
 930                          (b0s'@〈comma,false〉::l2) ??) -Hleft
 931           [ 3: >Hrs normalize @eq_f >associative_append %
 932           | * #Hb0 #Htapeb cases (IH …Htapeb) -IH * #_ #_ #IH
 933             cases (IH b' b0' bs' b0s' (l1@[〈b0,false〉]) l2 ??????? Ha ?) -IH
 934             [ * #Heq #Houtc % %
 935               [ >Hb0 @eq_f >Hbs in Heq; >Hb0s in ⊢ (%→?); #Heq
 936                 destruct (Heq) >Hb0s >Hc >Hd %
 937               | >Houtc >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append
 938                 >associative_append %
 939               ]
 940             | * #la * #c' * #d' * #lb * #lc * * * #H1 #H2 #H3 #H4 %2
 941               @(ex_intro … (〈b,false〉::la)) @(ex_intro … c') @(ex_intro … d')
 942               @(ex_intro … lb) @(ex_intro … lc)
 943               % [ % [ % // >Hbs >Hc >H2 % | >Hb0s >Hd >H3 >Hb0 % ]
 944                 | >H4 >Hbs >Hb0s >Hc >Hd >Hb0 >reverse_append
 945                   >reverse_cons >reverse_cons
 946                   >associative_append >associative_append
 947                   >associative_append >associative_append %
 948                 ]
 949             | generalize in match Hlen; >Hbs >Hb0s
 950               normalize #Hlen destruct (Hlen) @e0
 951             | #c0 #Hc0 @Hbs1 >Hbs @memb_cons //
 952             | #c0 #Hc0 @Hb0s1 >Hb0s @memb_cons //
 953             | #c0 #Hc0 @Hbs2 >Hbs @memb_cons //
 954             | #c0 #Hc0 @Hb0s2 >Hb0s @memb_cons //
 955             | #c0 #Hc0 cases (memb_append … Hc0)
 956               [ @Hl1 | #Hc0' >(memb_single … Hc0') % ]
 957             | %
 958             | >associative_append >associative_append % ]
 959          | * #Hneq #Htapeb %2
 960             @(ex_intro … []) @(ex_intro … b) @(ex_intro … b0)
 961             @(ex_intro … bs) @(ex_intro … b0s) %
 962            [ % // % // @sym_not_eq //
 963            | >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append
 964              >reverse_append in Htapeb; >reverse_cons
 965              >associative_append >associative_append
 966              #Htapeb <Htapeb
 967              cases (IH … Htapeb) -Htapeb -IH * #_ #IH #_ @(IH ? (refl ??))
 968            ]
 969          | #c1 #Hc1 cases (memb_append … Hc1) #Hyp
 970            [ @Hbs2 >Hbs @memb_cons @Hyp
 971            | cases (orb_true_l … Hyp)
 972              [ #Hyp2 >(\P Hyp2) %
 973              | @Hl1
 974              ]
 975            ]
 976          ]
 977 ]]]]]
 978 qed.
 979
 980 axiom sem_compare : Realize ? compare R_compare.