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/if_machine.ma".
  18 include "turing/basic_machines.ma".
  19 include "turing/universal/alphabet.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 atm0 : atm_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
  33 definition atm1 : atm_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
  34 definition atm2 : atm_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
  35
  36 definition atmr_step ≝
  37   λalpha:FinSet.λtest:alpha→bool.
  38   mk_TM alpha atm_states
  39   (λp.let 〈q,a〉 ≝ p in
  40    match a with
  41    [ None ⇒ 〈atm1, None ?〉
  42    | Some a' ⇒
  43      match test a' with
  44      [ true ⇒ 〈atm1,None ?〉
  45      | false ⇒ 〈atm2,Some ? 〈a',R〉〉 ]])
  46   atm0 (λx.notb (x == atm0)).
  47
  48 definition Ratmr_step_true ≝
  49   λalpha,test,t1,t2.
  50    ∃ls,a,rs.
  51    t1 = midtape alpha ls a rs ∧ test a = false ∧
  52    t2 = mk_tape alpha (a::ls) (option_hd ? rs) (tail ? rs).
  53
  54 definition Ratmr_step_false ≝
  55   λalpha,test,t1,t2.
  56     t1 = t2 ∧
  57     (current alpha t1 = None ? ∨
  58      (∃a.current ? t1 = Some ? a ∧ test a = true)).
  59
  60 lemma atmr_q0_q1 :
  61   ∀alpha,test,ls,a0,rs. test a0 = true →
  62   step alpha (atmr_step alpha test)
  63     (mk_config ?? atm0 (midtape … ls a0 rs)) =
  64   mk_config alpha (states ? (atmr_step alpha test)) atm1
  65     (midtape … ls a0 rs).
  66 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
  67 whd in match (trans … 〈?,?〉); >Htest %
  68 qed.
  69
  70 lemma atmr_q0_q2 :
  71   ∀alpha,test,ls,a0,rs. test a0 = false →
  72   step alpha (atmr_step alpha test)
  73     (mk_config ?? atm0 (midtape … ls a0 rs)) =
  74   mk_config alpha (states ? (atmr_step alpha test)) atm2
  75     (mk_tape … (a0::ls) (option_hd ? rs) (tail ? rs)).
  76 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
  77 whd in match (trans … 〈?,?〉); >Htest cases ts //
  78 qed.
  79
  80 lemma sem_atmr_step :
  81   ∀alpha,test.
  82   accRealize alpha (atmr_step alpha test)
  83     atm2 (Ratmr_step_true alpha test) (Ratmr_step_false alpha test).
  84 #alpha #test *
  85 [ @(ex_intro ?? 2)
  86   @(ex_intro ?? (mk_config ?? atm1 (niltape ?))) %
  87   [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
  88 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (leftof ? a al)))
  89   % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
  90 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (rightof ? a al)))
  91   % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
  92 | #ls #c #rs @(ex_intro ?? 2)
  93   cases (true_or_false (test c)) #Htest
  94   [ @(ex_intro ?? (mk_config ?? atm1 ?))
  95     [| %
  96       [ %
  97         [ whd in ⊢ (??%?); >atmr_q0_q1 //
  98         | whd in ⊢ ((??%%)→?); #Hfalse destruct ]
  99       | #_ % // %2 @(ex_intro ?? c) % // ]
 100     ]
 101   | @(ex_intro ?? (mk_config ?? atm2 (mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs))))
 102     %
 103     [ %
 104       [ whd in ⊢ (??%?); >atmr_q0_q2 //
 105       | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
 106         % // % //
 107       ]
 108     | #Hfalse @False_ind @(absurd ?? Hfalse) %
 109     ]
 110   ]
 111 ]
 112 qed.
 113
 114 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
 115   (current ? t1 = None ? → 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 %
 135     [#_ @Htapea
 136     |#ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
 137      #Hfalse destruct (Hfalse)
 138     ]
 139   | * #a * #Ha #Htest %
 140     [ >Ha #H destruct (H);
 141     | #ls #c #rs #H2 %
 142      >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
 143      <Htapea //
 144     ]
 145   ]
 146 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
 147   lapply (IH HRfalse) -IH #IH %
 148   [cases Hleft #ls * #a * #rs * * #Htapea #_ #_ >Htapea
 149    whd in ⊢((??%?)→?); #H destruct (H);
 150   |#ls #c #rs #Htapea %2
 151    cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
 152    >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
 153     [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
 154      cases (proj2 ?? IH … Htapeb)
 155       [ * #_ #Houtc >Houtc >Htapeb %
 156       | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
 157     | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
 158      cases (proj2 ?? IH … Htapeb)
 159       [ * #Hfalse >(Hmemb …) in Hfalse;
 160         [ #Hft destruct (Hft)
 161         | @memb_hd ]
 162       | * #Htestr1 #H1 >reverse_cons >associative_append
 163        @H1 // #x #Hx @Hmemb @memb_cons //
 164       ]
 165     ]
 166 qed.
 167
 168 lemma terminate_adv_to_mark_r :
 169   ∀alpha,test.
 170   ∀t.Terminate alpha (adv_to_mark_r alpha test) t.
 171 #alpha #test #t
 172 @(terminate_while … (sem_atmr_step alpha test))
 173   [ %
 174   | cases t
 175     [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 176     |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 177     | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
 178       elim rs
 179       [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 180        #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 181        % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
 182        normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
 183       | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 184         #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 185         >Ht1 @IH
 186       ]
 187     ]
 188   ]
 189 qed.
 190
 191 lemma sem_adv_to_mark_r :
 192   ∀alpha,test.
 193   Realize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
 194 /2/
 195 qed.
 196
 197 (* MARK machine
 198
 199    marks the current character
 200  *)
 201
 202 definition mark_states ≝ initN 2.
 203
 204 definition ms0 : mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
 205 definition ms1 : mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
 206
 207 definition mark ≝
 208   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
 209   (λp.let 〈q,a〉 ≝ p in
 210     match a with
 211     [ None ⇒ 〈ms1,None ?〉
 212     | Some a' ⇒ match (pi1 … q) with
 213       [ O ⇒ let 〈a'',b〉 ≝ a' in 〈ms1,Some ? 〈〈a'',true〉,N〉〉
 214       | S q ⇒ 〈ms1,None ?〉 ] ])
 215   ms0 (λq.q == ms1).
 216
 217 definition R_mark ≝ λalpha,t1,t2.
 218   (∀ls,c,b,rs.
 219      t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
 220      t2 = midtape ? ls 〈c,true〉 rs) ∧
 221   (current ? t1 = None ? → t2 = t1).
 222
 223 lemma sem_mark :
 224   ∀alpha.Realize ? (mark alpha) (R_mark alpha).
 225 #alpha #intape @(ex_intro ?? 2) cases intape
 226 [ @ex_intro
 227   [| % [ % | % [#ls #c #b #rs #Hfalse destruct | // ]]]
 228 |#a #al @ex_intro
 229   [| % [ % | % [#ls #c #b #rs #Hfalse destruct | // ]]]
 230 |#a #al @ex_intro
 231   [| % [ % | % [#ls #c #b #rs #Hfalse destruct ] // ]]
 232 | #ls * #c #b #rs
 233   @ex_intro [| % [ % | %
 234   [#ls0 #c0 #b0 #rs0 #H1 destruct (H1) %
 235   | whd in ⊢ ((??%?)→?); #H1 destruct (H1)]]]
 236 qed.
 237
 238
 239 (* MOVE RIGHT AND MARK machine
 240
 241    marks the first character on the right
 242
 243    (could be rewritten using (mark; move_right))
 244  *)
 245
 246 definition mrm_states ≝ initN 3.
 247
 248 definition mrm0 : mrm_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
 249 definition mrm1 : mrm_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
 250 definition mrm2 : mrm_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
 251
 252 definition move_right_and_mark ≝
 253   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mrm_states
 254   (λp.let 〈q,a〉 ≝ p in
 255     match a with
 256     [ None ⇒ 〈mrm2,None ?〉
 257     | Some a' ⇒ match pi1 … q with
 258       [ O ⇒ 〈mrm1,Some ? 〈a',R〉〉
 259       | S q ⇒ match q with
 260         [ O ⇒ let 〈a'',b〉 ≝ a' in
 261               〈mrm2,Some ? 〈〈a'',true〉,N〉〉
 262         | S _ ⇒ 〈mrm2,None ?〉 ] ] ])
 263   mrm0 (λq.q == mrm2).
 264
 265 definition R_move_right_and_mark ≝ λalpha,t1,t2.
 266   ∀ls,c,d,b,rs.
 267   t1 = midtape (FinProd … alpha FinBool) ls c (〈d,b〉::rs) →
 268   t2 = midtape ? (c::ls) 〈d,true〉 rs.
 269
 270 lemma sem_move_right_and_mark :
 271   ∀alpha.Realize ? (move_right_and_mark alpha) (R_move_right_and_mark alpha).
 272 #alpha #intape @(ex_intro ?? 3) cases intape
 273 [ @ex_intro
 274   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 275 |#a #al @ex_intro
 276   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 277 |#a #al @ex_intro
 278   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 279 | #ls #c *
 280   [ @ex_intro [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #Hfalse destruct ] ]
 281   | * #d #b #rs @ex_intro
 282     [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #H1 destruct (H1) % ] ] ] ]
 283 qed.
 284
 285 (* CLEAR MARK machine
 286
 287    clears the mark in the current character
 288  *)
 289
 290 definition clear_mark_states ≝ initN 3.
 291
 292 definition clear0 : clear_mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
 293 definition clear1 : clear_mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
 294 definition claer2 : clear_mark_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
 295
 296 definition clear_mark ≝
 297   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) clear_mark_states
 298   (λp.let 〈q,a〉 ≝ p in
 299     match a with
 300     [ None ⇒ 〈clear1,None ?〉
 301     | Some a' ⇒ match pi1 … q with
 302       [ O ⇒ let 〈a'',b〉 ≝ a' in 〈clear1,Some ? 〈〈a'',false〉,N〉〉
 303       | S q ⇒ 〈clear1,None ?〉 ] ])
 304   clear0 (λq.q == clear1).
 305
 306 definition R_clear_mark ≝ λalpha,t1,t2.
 307   (current ? t1 = None ? → t1 = t2) ∧
 308   ∀ls,c,b,rs.
 309   t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
 310   t2 = midtape ? ls 〈c,false〉 rs.
 311
 312 lemma sem_clear_mark :
 313   ∀alpha.Realize ? (clear_mark alpha) (R_clear_mark alpha).
 314 #alpha #intape @(ex_intro ?? 2) cases intape
 315 [ @ex_intro
 316   [| % [ % | % [#_ %|#ls #c #b #rs #Hfalse destruct ]]]
 317 |#a #al @ex_intro
 318   [| % [ % | % [#_ %|#ls #c #b #rs #Hfalse destruct ]]]
 319 |#a #al @ex_intro
 320   [| % [ % | % [#_ %|#ls #c #b #rs #Hfalse destruct ]]]
 321 | #ls * #c #b #rs
 322   @ex_intro [| % [ % | %
 323   [whd in ⊢ (??%?→?); #H destruct| #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ]]]]
 324 qed.
 325
 326 (* ADVANCE MARK RIGHT machine
 327
 328    clears mark on current char,
 329    moves right, and marks new current char
 330
 331 *)
 332
 333 definition adv_mark_r ≝
 334   λalpha:FinSet.
 335     clear_mark alpha · move_r ? · mark alpha.
 336
 337 definition R_adv_mark_r ≝ λalpha,t1,t2.
 338   (∀ls,c.
 339     (∀d,b,rs.
 340      t1 = midtape (FinProd … alpha FinBool) ls 〈c,true〉 (〈d,b〉::rs) →
 341      t2 = midtape ? (〈c,false〉::ls) 〈d,true〉 rs) ∧
 342     (t1 = midtape (FinProd … alpha FinBool) ls 〈c,true〉 [ ] →
 343      t2 = rightof ? 〈c,false〉 ls)) ∧
 344   (current ? t1 = None ? → t1 = t2).
 345
 346 lemma sem_adv_mark_r :
 347   ∀alpha.Realize ? (adv_mark_r alpha) (R_adv_mark_r alpha).
 348 #alpha
 349 @(sem_seq_app … (sem_clear_mark …)
 350          (sem_seq ????? (sem_move_r ?) (sem_mark alpha)) …)
 351 #intape #outtape whd in ⊢ (%→?); * #ta *
 352 whd in ⊢ (%→?); #Hs1 whd in ⊢ (%→?); * #tb * #Hs2 whd in ⊢ (%→?); #Hs3 %
 353   [#ls #c %
 354     [#d #b #rs #Hintape @(proj1 … Hs3 ?? b ?)
 355      @(proj2 … Hs2 ls 〈c,false〉 (〈d,b〉::rs))
 356      @(proj2 ?? Hs1 … Hintape)
 357     |#Hintape lapply (proj2 ?? Hs1 … Hintape) #Hta lapply (proj2 … Hs2 … Hta)
 358      whd in ⊢ ((???%)→?); #Htb <Htb @(proj2 … Hs3) >Htb //
 359     ]
 360   |#Hcur lapply(proj1 ?? Hs1 … Hcur) #Hta >Hta >Hta in Hcur; #Hcur
 361    lapply (proj1 ?? Hs2 … Hcur) #Htb >Htb >Htb in Hcur; #Hcur
 362    @sym_eq @(proj2 ?? Hs3) @Hcur
 363   ]
 364 qed.
 365
 366 (* ADVANCE TO MARK (left)
 367
 368 axiomatized
 369
 370 *)
 371 definition atml_step ≝
 372   λalpha:FinSet.λtest:alpha→bool.
 373   mk_TM alpha atm_states
 374   (λp.let 〈q,a〉 ≝ p in
 375    match a with
 376    [ None ⇒ 〈atm1, None ?〉
 377    | Some a' ⇒
 378      match test a' with
 379      [ true ⇒ 〈atm1,None ?〉
 380      | false ⇒ 〈atm2,Some ? 〈a',L〉〉 ]])
 381   atm0 (λx.notb (x == atm0)).
 382
 383 definition Ratml_step_true ≝
 384   λalpha,test,t1,t2.
 385    ∃ls,a,rs.
 386    t1 = midtape alpha ls a rs ∧ test a = false ∧
 387    t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a :: rs).
 388
 389 definition Ratml_step_false ≝
 390   λalpha,test,t1,t2.
 391     t1 = t2 ∧
 392     (current alpha t1 = None ? ∨
 393      (∃a.current ? t1 = Some ? a ∧ test a = true)).
 394
 395 lemma atml_q0_q1 :
 396   ∀alpha,test,ls,a0,rs. test a0 = true →
 397   step alpha (atml_step alpha test)
 398     (mk_config ?? atm0 (midtape … ls a0 rs)) =
 399   mk_config alpha (states ? (atml_step alpha test)) atm1
 400     (midtape … ls a0 rs).
 401 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
 402 whd in match (trans … 〈?,?〉); >Htest %
 403 qed.
 404
 405 lemma atml_q0_q2 :
 406   ∀alpha,test,ls,a0,rs. test a0 = false →
 407   step alpha (atml_step alpha test)
 408     (mk_config ?? atm0 (midtape … ls a0 rs)) =
 409   mk_config alpha (states ? (atml_step alpha test)) atm2
 410     (mk_tape … (tail ? ls) (option_hd ? ls) (a0 :: rs)).
 411 #alpha #test #ls #a0 #rs #Htest whd in ⊢ (??%?);
 412 whd in match (trans … 〈?,?〉); >Htest cases ls //
 413 qed.
 414
 415 lemma sem_atml_step :
 416   ∀alpha,test.
 417   accRealize alpha (atml_step alpha test)
 418     atm2 (Ratml_step_true alpha test) (Ratml_step_false alpha test).
 419 #alpha #test *
 420 [ @(ex_intro ?? 2)
 421   @(ex_intro ?? (mk_config ?? atm1 (niltape ?))) %
 422   [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
 423 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (leftof ? a al)))
 424   % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
 425 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (rightof ? a al)))
 426   % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
 427 | #ls #c #rs @(ex_intro ?? 2)
 428   cases (true_or_false (test c)) #Htest
 429   [ @(ex_intro ?? (mk_config ?? atm1 ?))
 430     [| %
 431       [ %
 432         [ whd in ⊢ (??%?); >atml_q0_q1 //
 433         | whd in ⊢ ((??%%)→?); #Hfalse destruct ]
 434       | #_ % // %2 @(ex_intro ?? c) % // ]
 435     ]
 436   | @(ex_intro ?? (mk_config ?? atm2 (mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs))))
 437     %
 438     [ %
 439       [ whd in ⊢ (??%?); >atml_q0_q2 //
 440       | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
 441         % // % //
 442       ]
 443     | #Hfalse @False_ind @(absurd ?? Hfalse) %
 444     ]
 445   ]
 446 ]
 447 qed.
 448
 449 definition R_adv_to_mark_l ≝ λalpha,test,t1,t2.
 450   (current ? t1 = None ? → t1 = t2) ∧
 451   ∀ls,c,rs.
 452   (t1 = midtape alpha ls c rs  →
 453   ((test c = true → t2 = t1) ∧
 454    (test c = false →
 455     (∀ls1,b,ls2. ls = ls1@b::ls2 →
 456      test b = true → (∀x.memb ? x ls1 = true → test x = false) →
 457      t2 = midtape ? ls2 b (reverse ? ls1@c::rs)) ∧
 458     ((∀x.memb ? x ls = true → test x = false) →
 459       ∀a,l. reverse ? (c::ls) = a::l → t2 = leftof ? a (l@rs))
 460      ))).
 461
 462 definition adv_to_mark_l ≝
 463   λalpha,test.whileTM alpha (atml_step alpha test) atm2.
 464
 465 lemma wsem_adv_to_mark_l :
 466   ∀alpha,test.
 467   WRealize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
 468 #alpha #test #t #i #outc #Hloop
 469 lapply (sem_while … (sem_atml_step alpha test) t i outc Hloop) [%]
 470 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 471 [ #tapea * #Htapea *
 472   [ #H1 %
 473     [#_ @Htapea
 474     |#ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
 475      #Hfalse destruct (Hfalse)
 476     ]
 477   | * #a * #Ha #Htest %
 478     [>Ha #H destruct (H);
 479     |#ls #c #rs #H2 %
 480       [#Hc <Htapea //
 481       |#Hc @False_ind >H2 in Ha; whd in ⊢ ((??%?)→?);
 482        #H destruct (H) /2/
 483       ]
 484     ]
 485   ]
 486 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
 487   lapply (IH HRfalse) -IH #IH %
 488   [cases Hleft #ls0 * #a0 * #rs0 * * #Htapea #_ #_ >Htapea
 489    whd in ⊢ ((??%?)→?); #H destruct (H)
 490   |#ls #c #rs #Htapea %
 491     [#Hc cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest @False_ind
 492      >Htapea' in Htapea; #H destruct /2/
 493     |cases Hleft #ls0 * #a * #rs0 *
 494      * #Htapea1 >Htapea in Htapea1; #H destruct (H) #_ #Htapeb
 495      #Hc %
 496       [*
 497         [#b #ls2 #Hls >Hls in Htapeb; #Htapeb #Htestb #_
 498          cases (proj2 ?? IH … Htapeb) #H1 #_ >H1 // >Htapeb %
 499         |#l1 #ls1 #b #ls2 #Hls >Hls in Htapeb; #Htapeb #Htestb #Hmemb
 500          cases (proj2 ?? IH … Htapeb) #_ #H1 >reverse_cons >associative_append
 501          @(proj1 ?? (H1 ?) … (refl …) Htestb …)
 502           [@Hmemb @memb_hd
 503           |#x #memx @Hmemb @memb_cons @memx
 504           ]
 505         ]
 506       |cases ls0 in Htapeb; normalize in ⊢ (%→?);
 507         [#Htapeb #Htest #a0 #l whd in ⊢ ((??%?)→?); #Hrev destruct (Hrev)
 508          >Htapeb in IH; #IH cases (proj1 ?? IH … (refl …)) //
 509         |#l1 #ls1 #Htapeb
 510          cases (proj2 ?? IH … Htapeb) #_ #H1 #Htest #a0 #l
 511          <(reverse_reverse … l) cases (reverse … l)
 512           [#H cut (a::l1::ls1 = [a0])
 513             [<(reverse_reverse  … (a::l1::ls1)) >H //]
 514            #Hrev destruct (Hrev)
 515           |#a1 #l2 >reverse_cons >reverse_cons >reverse_cons
 516            #Hrev cut ([a] = [a1])
 517             [@(append_l2_injective_r ?? (a0::reverse … l2) … Hrev) //]
 518            #Ha <Ha >associative_append @(proj2 ?? (H1 ?))
 519             [@Htest @memb_hd
 520             |#x #membx @Htest @memb_cons @membx
 521             |<(append_l1_injective_r ?? (a0::reverse … l2) … Hrev) //
 522             ]
 523           ]
 524         ]
 525       ]
 526     ]
 527   ]
 528 qed.
 529
 530 lemma terminate_adv_to_mark_l :
 531   ∀alpha,test.
 532   ∀t.Terminate alpha (adv_to_mark_l alpha test) t.
 533 #alpha #test #t
 534 @(terminate_while … (sem_atml_step alpha test))
 535   [ %
 536   | cases t
 537     [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 538     |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 539     | #ls elim ls
 540       [#c #rs % #t1 * #ls0 * #c0 * #rs0 * *
 541        #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 542        % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
 543        normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
 544       | #rs0 #r0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 545         #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 546         >Ht1 @IH
 547       ]
 548     ]
 549   ]
 550 qed.
 551
 552 lemma sem_adv_to_mark_l :
 553   ∀alpha,test.
 554   Realize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
 555 /2/
 556 qed.
 557
 558 (*
 559    ADVANCE BOTH MARKS machine
 560
 561    l1 does not contain marks ⇒
 562
 563
 564    input:
 565    l0 x* a l1 x0* a0 l2
 566               ^
 567
 568    output:
 569    l0 x a* l1 x0 a0* l2
 570         ^
 571 *)
 572
 573 definition adv_both_marks ≝ λalpha.
 574   adv_mark_r alpha · move_l ? ·
 575     adv_to_mark_l (FinProd alpha FinBool) (is_marked alpha) ·
 576       adv_mark_r alpha.
 577
 578 definition R_adv_both_marks ≝
 579   λalpha,t1,t2.
 580     ∀l0,x,a,l1,x0. (∀c.memb ? c l1 = true → is_marked ? c = false) →
 581     (∀l1',a0,l2. t1 = midtape (FinProd … alpha FinBool)
 582         (l1@〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
 583      reverse ? (〈x0,false〉::l1) = 〈a,false〉::l1' →
 584      t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1'@〈a0,true〉::l2)) ∧
 585      (t1 = midtape (FinProd … alpha FinBool)
 586         (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 [ ] →
 587      t2 = rightof ? 〈x0,false〉 (l1@〈a,false〉::〈x,true〉::l0)).
 588
 589 lemma sem_adv_both_marks :
 590   ∀alpha.Realize ? (adv_both_marks alpha) (R_adv_both_marks alpha).
 591 #alpha
 592 @(sem_seq_app … (sem_adv_mark_r …)
 593    (sem_seq ????? (sem_move_l …)
 594       (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?))
 595         (sem_adv_mark_r alpha))) …)
 596 #intape #outtape * #tapea * #Hta * #tb * #Htb * #tc * #Htc #Hout
 597 #l0 #x #a #l1 #x0 #Hmarks %
 598   [#l1' #a0 #l2 #Hintape #Hrev @(proj1 ?? (proj1 ?? Hout … ) ? false) -Hout
 599    lapply (proj1 … (proj1 … Hta …) … Hintape) #Htapea
 600    lapply (proj2 … Htb  … Htapea) -Htb
 601    whd in match (mk_tape ????) ; #Htapeb
 602    lapply (proj1 ?? (proj2 ?? (proj2 ?? Htc … Htapeb) (refl …))) -Htc #Htc
 603    change with ((?::?)@?) in match (cons ???); <Hrev >reverse_cons
 604    >associative_append @Htc [%|%|@Hmarks]
 605   |#Hintape lapply (proj2 ?? (proj1 ?? Hta … ) … Hintape) -Hta #Hta
 606    lapply (proj1 … Htb) >Hta -Htb #Htb lapply (Htb (refl …)) -Htb #Htb
 607    lapply (proj1 ?? Htc) <Htb -Htc #Htc lapply (Htc (refl …)) -Htc #Htc
 608    @sym_eq >Htc @(proj2 ?? Hout …) <Htc %
 609   ]
 610 qed.
 611
 612 (*
 613 definition R_adv_both_marks ≝
 614   λalpha,t1,t2.
 615     ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
 616     (t1 = midtape (FinProd … alpha FinBool)
 617         (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
 618      t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2)) ∧
 619      (t1 = midtape (FinProd … alpha FinBool)
 620         (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 [] →
 621      t2 = rightof ? 〈x0,false〉 (l1@〈a,false〉::〈x,true〉::l0)).
 622
 623 lemma sem_adv_both_marks :
 624   ∀alpha.Realize ? (adv_both_marks alpha) (R_adv_both_marks alpha).
 625 #alpha #intape
 626 cases (sem_seq ????? (sem_adv_mark_r …)
 627         (sem_seq ????? (sem_move_l …)
 628           (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?))
 629             (sem_adv_mark_r alpha))) intape)
 630 #k * #outc * #Hloop whd in ⊢ (%→?);
 631 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→?); #Hs2
 632 * #tc * whd in ⊢ (%→%→?); #Hs3 #Hs4
 633 @(ex_intro ?? k) @(ex_intro ?? outc) %
 634 [ @Hloop
 635 | -Hloop #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
 636   @(Hs4 … false) -Hs4
 637   lapply (Hs1 … Hintape) #Hta
 638   lapply (proj2 … Hs2 … Hta) #Htb
 639   cases (Hs3 … Htb)
 640   [ * #Hfalse normalize in Hfalse; destruct (Hfalse)
 641   | * #_ -Hs3 #Hs3
 642     lapply (Hs3 (l1@[〈a,false〉]) 〈x,true〉 l0 ???)
 643     [ #x1 #Hx1 cases (memb_append … Hx1)
 644       [ @Hl1
 645       | #Hx1' >(memb_single … Hx1') % ]
 646     | %
 647     | >associative_append %
 648     | >reverse_append #Htc @Htc ]
 649   ]
 650 qed. *)
 651
 652 (*
 653    MATCH AND ADVANCE(f)
 654
 655    input:
 656    l0 x* a l1 x0* a0 l2
 657               ^
 658
 659    output:
 660    l0 x a* l1 x0 a0* l2   (f(x0) == true)
 661         ^
 662    l0 x* a l1 x0* a0 l2   (f(x0) == false)
 663               ^
 664 *)
 665
 666 definition match_and_adv ≝
 667   λalpha,f.ifTM ? (test_char ? f)
 668      (adv_both_marks alpha) (clear_mark ?) tc_true.
 669
 670 definition R_match_and_adv ≝
 671   λalpha,f,t1,t2.
 672     ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
 673     t1 = midtape (FinProd … alpha FinBool)
 674         (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
 675     (f 〈x0,true〉 = true ∧ t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2))
 676     ∨ (f 〈x0,true〉 = false ∧
 677     t2 = midtape ? (l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)).
 678
 679 lemma sem_match_and_adv :
 680   ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv alpha f).
 681 #alpha #f #intape
 682 cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape)
 683 #k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
 684 % [ @Hloop ] -Hloop
 685 cases Hif
 686 [ * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
 687   #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape >Hintape in Hta;
 688   * * #x1 * whd in ⊢ ((??%?)→?); #H destruct (H) #Hf #Hta % %
 689   [ @Hf | >append_cons >append_cons in Hta; #Hta @(proj1 ?? (Houtc …) …Hta)
 690     [ #x #memx cases (memb_append …memx)
 691       [@Hl1 | -memx #memx >(memb_single … memx) %]
 692     |>reverse_cons >reverse_append % ] ]
 693 | * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
 694   #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape >Hintape in Hta;
 695   * #Hf #Hta %2 % [ @Hf % | >(proj2 ?? Houtc … Hta) % ]
 696 ]
 697 qed.
 698
 699 (*
 700  if x = c
 701       then move_right; ----
 702            adv_to_mark_r;
 703            if current (* x0 *) = 0
 704               then advance_mark ----
 705                    adv_to_mark_l;
 706                    advance_mark
 707               else STOP
 708       else M
 709 *)
 710
 711 definition comp_step_subcase ≝ λalpha,c,elseM.
 712   ifTM ? (test_char ? (λx.x == c))
 713     (move_r … · adv_to_mark_r ? (is_marked alpha) · match_and_adv ? (λx.x == c))
 714     elseM tc_true.
 715
 716 definition R_comp_step_subcase ≝
 717   λalpha,c,RelseM,t1,t2.
 718     ∀l0,x,rs.t1 = midtape (FinProd … alpha FinBool) l0 〈x,true〉 rs →
 719     (〈x,true〉 = c →
 720      ((∀c.memb ? c rs = true → is_marked ? c = false) →
 721        ∀a,l. (a::l) = reverse ? (〈x,true〉::rs) → t2 = rightof (FinProd alpha FinBool) a (l@l0)) ∧
 722      ∀a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
 723      rs = 〈a,false〉::l1@〈x0,true〉::〈a0,false〉::l2 →
 724      ((x = x0 →
 725       t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1@〈x0,false〉::〈a0,true〉::l2)) ∨
 726       (x ≠ x0 →
 727       t2 = midtape (FinProd … alpha FinBool)
 728         (reverse ? l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)))) ∨
 729     (〈x,true〉 ≠ c → RelseM t1 t2).
 730
 731 lemma dec_marked: ∀alpha,rs.
 732  decidable (∀c.memb ? c rs = true → is_marked alpha c = false).
 733 #alpha #rs elim rs
 734   [%1 #n normalize #H destruct
 735   |#a #tl cases (true_or_false (is_marked ? a)) #Ha
 736     [#_ %2 % #Hall @(absurd ?? not_eq_true_false) <Ha
 737      @Hall @memb_hd
 738     |* [#Hall %1 #c #memc cases (orb_true_l … memc)
 739          [#eqca >(\P eqca) @Ha |@Hall]
 740     |#Hnall %2 @(not_to_not … Hnall) #Hall #c #memc @Hall @memb_cons //
 741     ]
 742   qed.
 743
 744 lemma sem_comp_step_subcase :
 745   ∀alpha,c,elseM,RelseM.
 746   Realize ? elseM RelseM →
 747   Realize ? (comp_step_subcase alpha c elseM)
 748     (R_comp_step_subcase alpha c RelseM).
 749 #alpha #c #elseM #RelseM #Helse #intape
 750 cases (sem_if ? (test_char ? (λx.x == c)) … tc_true
 751         (sem_test_char ? (λx.x == c))
 752         (sem_seq ????? (sem_move_r …)
 753           (sem_seq ????? (sem_adv_to_mark_r ? (is_marked alpha))
 754              (sem_match_and_adv ? (λx.x == c)))) Helse intape)
 755 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc)
 756 % [ @Hloop ] -Hloop cases HR -HR
 757   [* #ta * whd in ⊢ (%→?); #Hta * #tb * whd in ⊢ (%→?); #Htb
 758    * #tc * whd in ⊢ (%→?); #Htc whd in ⊢ (%→?); #Houtc
 759    #l0 #x #rs #Hintape cases (true_or_false (〈x,true〉==c)) #Hc
 760     [%1 #_ cases (dec_marked ? rs) #Hdec
 761       [%
 762         [#_ #a #l1
 763          >Hintape in Hta; * #_(* #x1 * whd in ⊢ ((??%?)→?); #H destruct (H) #Hx *)
 764          #Hta lapply (proj2 … Htb … Hta) -Htb -Hta cases rs
 765            [whd in ⊢ ((???%)→?); #Htb >Htb in Htc; #Htc
 766             lapply (proj1 ?? Htc (refl …)) -Htc #Htc <Htc in Houtc;
 767         |#a #l1 #x0 #a0 #l2 #_ #Hrs @False_ind
 768          @(absurd ?? not_eq_true_false)
 769          change with (is_marked ? 〈x0,true〉) in match true;
 770          @Hdec >Hrs @memb_cons @memb_append_l2 @memb_hd
 771         ]
 772       |% [#H @False_ind @(absurd …H Hdec)]
 773        #a #l1 #x0 #a0 #l2 #Hl1 #Hrs >Hrs in Hintape; #Hintape
 774        >Hintape in Hta; * #_(* #x1 * whd in ⊢ ((??%?)→?); #H destruct (H) #Hx *)
 775        #Hta lapply (proj2 … Htb … Hta) -Htb -Hta
 776        whd in match (mk_tape ????); #Htb cases Htc -Htc #_ #Htc
 777        cases (Htc … Htb) [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
 778        -Htc * #_ #Htc lapply (Htc l1 〈x0,true〉 (〈a0,false〉::l2) (refl ??) (refl ??) Hl1)
 779        -Htc #Htc cases (Houtc ???????? Htc) -Houtc
 780         [* #Hx0 #Houtc %1 #Hx >Houtc >reverse_reverse %
 781         |* #Hx0 #Houtc %2 #_ >Houtc %
 782         |#x #membx @Hl1 <(reverse_reverse …l1) @memb_reverse @membx
 783         ]
 784       ]
 785     |%2 >Hintape in Hta; * * #x1 * whd in ⊢ ((??%?)→?); #H destruct (H)
 786      >Hc #H destruct (H)
 787     ]
 788   |* #ta * whd in ⊢ (%→?); * #Hc #Hta #Helse #ls #c0 #rs #Hintape %2
 789    #_ >Hintape in Hta; #Hta <Hta @Helse
 790   ]
 791 qed.
 792
 793 (*
 794 - se marcato, itero
 795 - se non è marcato
 796   + se è un bit, ho fallito il confronto della tupla corrente
 797   + se è un separatore, la tupla fa match
 798
 799
 800 ifTM ? (test_char ? is_marked)
 801   (single_finalTM … (comp_step_subcase unialpha 〈bit false,true〉
 802     (comp_step_subcase unialpha 〈bit true,true〉
 803       (clear_mark …))))
 804   (nop ?)
 805 *)
 806
 807 definition comp_step ≝
 808   ifTM ? (test_char ? (is_marked ?))
 809   (single_finalTM … (comp_step_subcase FSUnialpha 〈bit false,true〉
 810     (comp_step_subcase FSUnialpha 〈bit true,true〉
 811       (comp_step_subcase FSUnialpha 〈null,true〉
 812         (clear_mark …)))))
 813   (nop ?)
 814   tc_true.
 815
 816 (* da spostare *)
 817
 818 lemma mem_append : ∀A,x,l1,l2. mem A x (l1@l2) →
 819   mem A x l1 ∨ mem A x l2.
 820 #A #x #l1 elim l1 normalize [/2/]
 821 #a #tl #Hind #l2 * [#eqxa %1 /2/ |#memx cases (Hind … memx) /3/]
 822 qed.
 823
 824 let rec split_on A (l:list A) f acc on l ≝
 825   match l with
 826   [ nil ⇒ 〈acc,nil ?〉
 827   | cons a tl ⇒
 828     if f a then 〈acc,a::tl〉 else split_on A tl f (a::acc)
 829   ].
 830
 831 lemma split_on_spec: ∀A,l,f,acc,res1,res2.
 832   split_on A l f acc = 〈res1,res2〉 →
 833     (∃l1. res1 = l1@acc ∧
 834     reverse ? l1@res2 = l ∧
 835     ∀x. mem ? x l1 → f x = false) ∧
 836     ∀a,tl. res2 = a::tl → f a = true.
 837 #A #l #f elim l
 838   [#acc #res1 #res2 normalize in ⊢ (%→?); #H destruct %
 839     [@(ex_intro … []) % normalize [% % | #x @False_ind]
 840     |#a #tl #H destruct
 841     ]
 842   |#a #tl #Hind #acc #res1 #res2 normalize in ⊢ (%→?);
 843    cases (true_or_false (f a)) #Hfa >Hfa normalize in ⊢ (%→?);
 844    #H destruct
 845    [% [@(ex_intro … []) % normalize [% % | #x @False_ind]
 846       |#a1 #tl1 #H destruct (H) //]
 847    |cases (Hind (a::acc) res1 res2 H) * #l1 * *
 848     #Hres1 #Htl #Hfalse #Htrue % [2:@Htrue] @(ex_intro … (l1@[a])) %
 849      [% [>associative_append @Hres1 | >reverse_append <Htl % ]
 850      |#x #Hmemx cases (mem_append ???? Hmemx)
 851         [@Hfalse | normalize * [#H >H //| @False_ind]
 852      ]
 853    ]
 854   ]
 855 qed.
 856
 857 axiom mem_reverse: ∀A,l,x. mem A x (reverse ? l) → mem A x l.
 858
 859 lemma split_on_spec_ex: ∀A,l,f.∃l1,l2.
 860     l1@l2 = l ∧ (∀x:A. mem ? x l1 → f x = false) ∧
 861     ∀a,tl. l2 = a::tl → f a = true.
 862 #A #l #f @(ex_intro … (reverse … (\fst (split_on A l f []))))
 863 @(ex_intro … (\snd (split_on A l f [])))
 864 cases (split_on_spec A l f [ ] ?? (eq_pair_fst_snd …)) * #l1 * *
 865 >append_nil #Hl1 >Hl1 #Hl #Hfalse #Htrue %
 866   [% [@Hl|#x #memx @Hfalse @mem_reverse //] | @Htrue]
 867 qed.
 868
 869 definition R_comp_step_true ≝ λt1,t2.
 870   ∃l0,c,a,l1,c0,l1',a0,l2.
 871     t1 = midtape (FinProd … FSUnialpha FinBool)
 872       l0 〈c,true〉 (l1@〈c0,true〉::〈a0,false〉::l2) ∧
 873        l1@[〈c0,false〉] = 〈a,false〉::l1' ∧
 874       (∀c.memb ? c l1 = true → is_marked ? c = false) ∧
 875       (bit_or_null c = true → c0 = c →
 876         t2 = midtape ? (〈c,false〉::l0) 〈a,true〉 (l1'@〈c0,false〉::〈a0,true〉::l2)) ∧
 877       (bit_or_null c = true → c0 ≠ c →
 878         t2 = midtape (FinProd … FSUnialpha FinBool)
 879          (reverse ? l1@〈a,false〉::〈c,true〉::l0) 〈c0,false〉 (〈a0,false〉::l2)) ∧
 880       (bit_or_null c = false →
 881         t2 = midtape ? l0 〈c,false〉 (〈a,false〉::l1@〈c0,true〉::〈a0,false〉::l2)).
 882
 883 definition R_comp_step_false ≝
 884   λt1,t2.
 885    ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
 886    is_marked ? c = false ∧ t2 = t1.
 887
 888 (*
 889 lemma is_marked_to_exists: ∀alpha,c. is_marked alpha c = true →
 890  ∃c'. c = 〈c',true〉.
 891 #alpha * c *)
 892
 893 lemma sem_comp_step :
 894   accRealize ? comp_step (inr … (inl … (inr … start_nop)))
 895     R_comp_step_true R_comp_step_false.
 896 @(acc_sem_if_app … (sem_test_char ? (is_marked ?))
 897         (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
 898           (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ??
 899             (sem_comp_step_subcase FSUnialpha 〈null,true〉 ??
 900               (sem_clear_mark …))))
 901         (sem_nop …) …)
 902 [#intape #outtape #midtape * * * #c #b * #Hcurrent
 903 whd in ⊢ ((??%?)→?); #Hb #Hmidtape >Hmidtape -Hmidtape
 904  cases (current_to_midtape … Hcurrent) #ls * #rs >Hb #Hintape >Hintape -Hb
 905  whd in ⊢ (%→?); #Htapea lapply (Htapea … (refl …)) -Htapea
 906  cases (split_on_spec_ex ? rs (is_marked ?)) #l1 * #l2 * * #Hrs #Hl1 #Hl2
 907  cases (true_or_false (c == bit false))
 908   [(* c = bit false *) #Hc * [2: * >(\P Hc) * #H @False_ind @H //]
 909    * #_ #Hout whd
 910    cases (split_on_spec
 911
 912
 913 [ #Hstate lapply (H1 Hstate) -H1 -Hstate -H2 *
 914   #ta * whd in ⊢ (%→?); #Hleft #Hright #ls #c #rs #Hintape
 915   >Hintape in Hleft; * *
 916   cases c in Hintape; #c' #b #Hintape #x * whd in ⊢ (??%?→?); #H destruct (H)
 917   whd in ⊢ (??%?→?); #Hb >Hb #Hta @(ex_intro ?? c') % //
 918   cases (Hright … Hta)
 919   [ * #Hc' #H1 % % [destruct (Hc') % ]
 920     #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
 921     cases (H1 … Hl1 Hrs)
 922     [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
 923     | * #Hneq #Houtc %2 %
 924       [ @sym_not_eq //
 925       | @Houtc ]
 926     ]
 927   | * #Hc #Helse1 cases (Helse1 … Hta)
 928     [ * #Hc' #H1 % % [destruct (Hc') % ]
 929       #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
 930       cases (H1 … Hl1 Hrs)
 931       [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
 932       | * #Hneq #Houtc %2 %
 933         [ @sym_not_eq //
 934         | @Houtc ]
 935       ]
 936     | * #Hc' #Helse2 cases (Helse2 … Hta)
 937       [ * #Hc'' #H1 % % [destruct (Hc'') % ]
 938         #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
 939         cases (H1 … Hl1 Hrs)
 940         [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
 941         | * #Hneq #Houtc %2 %
 942           [ @sym_not_eq //
 943           | @Houtc ]
 944         ]
 945       | * #Hc'' whd in ⊢ (%→?); #Helse3 %2 %
 946         [ generalize in match Hc''; generalize in match Hc'; generalize in match Hc;
 947           cases c'
 948           [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
 949               | #Hfalse @False_ind @(absurd ?? Hfalse) % ]
 950           | #_ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
 951           |*: #_ #_ #_ % ]
 952         | @(Helse3 … Hta)
 953         ]
 954       ]
 955     ]
 956   ]
 957 | #Hstate lapply (H2 Hstate) -H1 -Hstate -H2 *
 958   #ta * whd in ⊢ (%→%→?); #Hleft #Hright #ls #c #rs #Hintape
 959   >Hintape in Hleft; * #Hc #Hta % [@Hc % | >Hright //]
 960 ]
 961 qed.
 962 definition R_comp_step_true ≝
 963   λt1,t2.
 964     ∀l0,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) l0 c rs →
 965     ∃c'. c = 〈c',true〉 ∧
 966     ((bit_or_null c' = true ∧
 967      ∀a,l1,c0,a0,l2.
 968       rs = 〈a,false〉::l1@〈c0,true〉::〈a0,false〉::l2 →
 969       (∀c.memb ? c l1 = true → is_marked ? c = false) →
 970       (c0 = c' ∧
 971        t2 = midtape ? (〈c',false〉::l0) 〈a,true〉 (l1@〈c0,false〉::〈a0,true〉::l2)) ∨
 972       (c0 ≠ c' ∧
 973        t2 = midtape (FinProd … FSUnialpha FinBool)
 974         (reverse ? l1@〈a,false〉::〈c',true〉::l0) 〈c0,false〉 (〈a0,false〉::l2))) ∨
 975      (bit_or_null c' = false ∧ t2 = midtape ? l0 〈c',false〉 rs)).
 976
 977 definition R_comp_step_false ≝
 978   λt1,t2.
 979    ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
 980    is_marked ? c = false ∧ t2 = t1.
 981
 982 lemma sem_comp_step :
 983   accRealize ? comp_step (inr … (inl … (inr … start_nop)))
 984     R_comp_step_true R_comp_step_false.
 985 #intape
 986 cases (acc_sem_if … (sem_test_char ? (is_marked ?))
 987         (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
 988           (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ??
 989             (sem_comp_step_subcase FSUnialpha 〈null,true〉 ??
 990               (sem_clear_mark …))))
 991         (sem_nop …) intape)
 992 #k * #outc * * #Hloop #H1 #H2
 993 @(ex_intro ?? k) @(ex_intro ?? outc) %
 994 [ % [@Hloop ] ] -Hloop
 995 [ #Hstate lapply (H1 Hstate) -H1 -Hstate -H2 *
 996   #ta * whd in ⊢ (%→?); #Hleft #Hright #ls #c #rs #Hintape
 997   >Hintape in Hleft; * *
 998   cases c in Hintape; #c' #b #Hintape #x * whd in ⊢ (??%?→?); #H destruct (H)
 999   whd in ⊢ (??%?→?); #Hb >Hb #Hta @(ex_intro ?? c') % //
1000   cases (Hright … Hta)
1001   [ * #Hc' #H1 % % [destruct (Hc') % ]
1002     #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
1003     cases (H1 … Hl1 Hrs)
1004     [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
1005     | * #Hneq #Houtc %2 %
1006       [ @sym_not_eq //
1007       | @Houtc ]
1008     ]
1009   | * #Hc #Helse1 cases (Helse1 … Hta)
1010     [ * #Hc' #H1 % % [destruct (Hc') % ]
1011       #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
1012       cases (H1 … Hl1 Hrs)
1013       [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
1014       | * #Hneq #Houtc %2 %
1015         [ @sym_not_eq //
1016         | @Houtc ]
1017       ]
1018     | * #Hc' #Helse2 cases (Helse2 … Hta)
1019       [ * #Hc'' #H1 % % [destruct (Hc'') % ]
1020         #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
1021         cases (H1 … Hl1 Hrs)
1022         [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
1023         | * #Hneq #Houtc %2 %
1024           [ @sym_not_eq //
1025           | @Houtc ]
1026         ]
1027       | * #Hc'' whd in ⊢ (%→?); #Helse3 %2 %
1028         [ generalize in match Hc''; generalize in match Hc'; generalize in match Hc;
1029           cases c'
1030           [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
1031               | #Hfalse @False_ind @(absurd ?? Hfalse) % ]
1032           | #_ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
1033           |*: #_ #_ #_ % ]
1034         | @(Helse3 … Hta)
1035         ]
1036       ]
1037     ]
1038   ]
1039 | #Hstate lapply (H2 Hstate) -H1 -Hstate -H2 *
1040   #ta * whd in ⊢ (%→%→?); #Hleft #Hright #ls #c #rs #Hintape
1041   >Hintape in Hleft; * #Hc #Hta % [@Hc % | >Hright //]
1042 ]
1043 qed.
1044
1045 definition compare ≝
1046   whileTM ? comp_step (inr … (inl … (inr … start_nop))).
1047
1048 (*
1049 definition R_compare :=
1050   λt1,t2.
1051   (t
1052
1053   ∀ls,c,b,rs.t1 = midtape ? ls 〈c,b〉 rs →
1054   (b = true → rs = ....) →
1055   (b = false ∧ ....) ∨
1056   (b = true ∧
1057
1058    rs = cs@l1@〈c0,true〉::cs0@l2
1059    (
1060
1061
1062   ls 〈c,b〉 cs l1 〈c0,b0〉 cs0 l2
1063
1064
1065 ACCETTAZIONE:
1066   ls (hd (Ls@〈grid,false〉))* (tail (Ls@〈grid,false〉)) l1 (hd (Ls@〈comma,false〉))* (tail (Ls@〈comma,false〉)) l2
1067      ^^^^^^^^^^^^^^^^^^^^^^^
1068
1069   ls Ls 〈grid,false〉 l1 Ls 〈comma,true〉 l2
1070         ^^^^^^^^^^^^
1071
1072 RIFIUTO: c ≠ d
1073
1074   ls (hd (Ls@〈c,false〉))* (tail (Ls@〈c,false〉)) l1 (hd (Ls@〈d,false〉))* (tail (Ls@〈d,false〉)) l2
1075      ^^^^^^^^^^^^^^^^^^^^^^^
1076
1077
1078   ls Ls 〈c,true〉 l1 Ls 〈d,false〉 l2
1079                        ^^^^^^^^
1080
1081   ).
1082
1083   |bs| = |b0s| →
1084   (∃la,d.〈b,true〉::bs = la@[〈grid,d〉] ∧ ∀x.memb ? x la → is_bit (\fst x) = true) →
1085   (∃lb,d0.〈b0,true〉::b0s = lb@[〈comma,d0〉] ∧ ∀x.memb ? x lb → is_bit (\fst x) = true) →
1086   t1 = midtape ? l0 〈b,true〉 (bs@l1@〈b0,true〉::b0s@l2 →
1087
1088   mk_tape left (option current) right
1089
1090   (b = grid ∧ b0 = comma ∧ bs = [] ∧ b0s = [] ∧
1091    t2 = midtape ? l0 〈grid,false〉 (l1@〈comma,true〉::l2)) ∨
1092   (b = bit x ∧ b = c ∧ bs = b0s
1093   *)
1094 definition R_compare :=
1095   λt1,t2.
1096   ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
1097   (∀c'.bit_or_null c' = false → c = 〈c',true〉 → t2 = midtape ? ls 〈c',false〉 rs) ∧
1098   (∀c'. c = 〈c',false〉 → t2 = t1) ∧
1099   ∀b,b0,bs,b0s,l1,l2.
1100   |bs| = |b0s| →
1101   (∀c.memb (FinProd … FSUnialpha FinBool) c bs = true → bit_or_null (\fst c) = true) →
1102   (∀c.memb (FinProd … FSUnialpha FinBool) c b0s = true → bit_or_null (\fst c) = true) →
1103   (∀c.memb ? c bs = true → is_marked ? c = false) →
1104   (∀c.memb ? c b0s = true → is_marked ? c = false) →
1105   (∀c.memb ? c l1 = true → is_marked ? c = false) →
1106   c = 〈b,true〉 → bit_or_null b = true →
1107   rs = bs@〈grid,false〉::l1@〈b0,true〉::b0s@〈comma,false〉::l2 →
1108   (〈b,true〉::bs = 〈b0,true〉::b0s ∧
1109    t2 = midtape ? (reverse ? bs@〈b,false〉::ls)
1110           〈grid,false〉 (l1@〈b0,false〉::b0s@〈comma,true〉::l2)) ∨
1111   (∃la,c',d',lb,lc.c' ≠ d' ∧
1112     〈b,false〉::bs = la@〈c',false〉::lb ∧
1113     〈b0,false〉::b0s = la@〈d',false〉::lc ∧
1114     t2 = midtape (FinProd … FSUnialpha FinBool) (reverse ? la@
1115                     reverse ? l1@
1116                     〈grid,false〉::
1117                     reverse ? lb@
1118                     〈c',true〉::
1119                     reverse ? la@ls)
1120                     〈d',false〉 (lc@〈comma,false〉::l2)).
1121
1122 lemma wsem_compare : WRealize ? compare R_compare.
1123 #t #i #outc #Hloop
1124 lapply (sem_while ?????? sem_comp_step t i outc Hloop) [%]
1125 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
1126 [ #tapea whd in ⊢ (%→?); #Rfalse #ls #c #rs #Htapea %
1127   [ %
1128     [ #c' #Hc' #Hc lapply (Rfalse … Htapea) -Rfalse * >Hc
1129       whd in ⊢ (??%?→?); #Hfalse destruct (Hfalse)
1130     | #c' #Hc lapply (Rfalse … Htapea) -Rfalse * #_
1131       #Htrue @Htrue ]
1132   | #b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1 #Hc
1133     cases (Rfalse … Htapea) -Rfalse >Hc whd in ⊢ (??%?→?);#Hfalse destruct (Hfalse)
1134   ]
1135 | #tapea #tapeb #tapec #Hleft #Hright #IH #Htapec lapply (IH Htapec) -Htapec -IH #IH
1136   whd in Hleft; #ls #c #rs #Htapea cases (Hleft … Htapea) -Hleft
1137   #c' * #Hc >Hc cases (true_or_false (bit_or_null c')) #Hc'
1138   [2: *
1139     [ * >Hc' #H @False_ind destruct (H)
1140     | * #_ #Htapeb cases (IH … Htapeb) * #_ #H #_ %
1141       [%
1142         [#c1 #Hc1 #Heqc destruct (Heqc) <Htapeb @(H c1) %
1143         |#c1 #Hfalse destruct (Hfalse)
1144         ]
1145       |#b #b0 #bs #b0s #l1 #l2 #_ #_ #_ #_ #_ #_
1146        #Heq destruct (Heq) >Hc' #Hfalse @False_ind destruct (Hfalse)
1147       ]
1148     ]
1149  |#Hleft %
1150     [ %
1151       [ #c'' #Hc'' #Heq destruct (Heq) >Hc'' in Hc'; #H destruct (H)
1152       | #c0 #Hfalse destruct (Hfalse)
1153       ]
1154     |#b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1
1155      #Heq destruct (Heq) #_ #Hrs cases Hleft -Hleft
1156       [2: * >Hc' #Hfalse @False_ind destruct ] * #_
1157        @(list_cases2 … Hlen)
1158        [ #Hbs #Hb0s generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
1159        -Hrs #Hrs normalize in Hrs; #Hleft cases (Hleft ????? Hrs ?) -Hleft
1160          [ * #Heqb #Htapeb cases (IH … Htapeb) -IH * #IH #_ #_
1161           % %
1162             [ >Heqb >Hbs >Hb0s %
1163             | >Hbs >Hb0s @IH %
1164             ]
1165          |* #Hneqb #Htapeb %2
1166           @(ex_intro … [ ]) @(ex_intro … b)
1167           @(ex_intro … b0) @(ex_intro … [ ])
1168           @(ex_intro … [ ]) %
1169             [ % [ % [@sym_not_eq //| >Hbs %] | >Hb0s %]
1170             | cases (IH … Htapeb) -IH * #_ #IH #_ >(IH ? (refl ??))
1171               @Htapeb
1172             ]
1173          | @Hl1 ]
1174       | * #b' #bitb' * #b0' #bitb0' #bs' #b0s' #Hbs #Hb0s
1175         generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
1176         cut (bit_or_null b' = true ∧ bit_or_null b0' = true ∧
1177              bitb' = false ∧ bitb0' = false)
1178         [ % [ % [ % [ >Hbs in Hbs1; #Hbs1 @(Hbs1 〈b',bitb'〉) @memb_hd
1179             | >Hb0s in Hb0s1; #Hb0s1 @(Hb0s1 〈b0',bitb0'〉) @memb_hd ]
1180             | >Hbs in Hbs2; #Hbs2 @(Hbs2 〈b',bitb'〉) @memb_hd ]
1181             | >Hb0s in Hb0s2; #Hb0s2 @(Hb0s2 〈b0',bitb0'〉) @memb_hd ]
1182         | * * * #Ha #Hb #Hc #Hd >Hc >Hd
1183           #Hrs #Hleft
1184           cases (Hleft b' (bs'@〈grid,false〉::l1) b0 b0'
1185                          (b0s'@〈comma,false〉::l2) ??) -Hleft
1186           [ 3: >Hrs normalize @eq_f >associative_append %
1187           | * #Hb0 #Htapeb cases (IH …Htapeb) -IH * #_ #_ #IH
1188             cases (IH b' b0' bs' b0s' (l1@[〈b0,false〉]) l2 ??????? Ha ?) -IH
1189             [ * #Heq #Houtc % %
1190               [ >Hb0 @eq_f >Hbs in Heq; >Hb0s in ⊢ (%→?); #Heq
1191                 destruct (Heq) >Hb0s >Hc >Hd %
1192               | >Houtc >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append
1193                 >associative_append %
1194               ]
1195             | * #la * #c' * #d' * #lb * #lc * * * #H1 #H2 #H3 #H4 %2
1196               @(ex_intro … (〈b,false〉::la)) @(ex_intro … c') @(ex_intro … d')
1197               @(ex_intro … lb) @(ex_intro … lc)
1198               % [ % [ % // >Hbs >Hc >H2 % | >Hb0s >Hd >H3 >Hb0 % ]
1199                 | >H4 >Hbs >Hb0s >Hc >Hd >Hb0 >reverse_append
1200                   >reverse_cons >reverse_cons
1201                   >associative_append >associative_append
1202                   >associative_append >associative_append %
1203                 ]
1204             | generalize in match Hlen; >Hbs >Hb0s
1205               normalize #Hlen destruct (Hlen) @e0
1206             | #c0 #Hc0 @Hbs1 >Hbs @memb_cons //
1207             | #c0 #Hc0 @Hb0s1 >Hb0s @memb_cons //
1208             | #c0 #Hc0 @Hbs2 >Hbs @memb_cons //
1209             | #c0 #Hc0 @Hb0s2 >Hb0s @memb_cons //
1210             | #c0 #Hc0 cases (memb_append … Hc0)
1211               [ @Hl1 | #Hc0' >(memb_single … Hc0') % ]
1212             | %
1213             | >associative_append >associative_append % ]
1214          | * #Hneq #Htapeb %2
1215             @(ex_intro … []) @(ex_intro … b) @(ex_intro … b0)
1216             @(ex_intro … bs) @(ex_intro … b0s) %
1217            [ % // % // @sym_not_eq //
1218            | >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append
1219              >reverse_append in Htapeb; >reverse_cons
1220              >associative_append >associative_append
1221              #Htapeb <Htapeb
1222              cases (IH … Htapeb) -Htapeb -IH * #_ #IH #_ @(IH ? (refl ??))
1223            ]
1224          | #c1 #Hc1 cases (memb_append … Hc1) #Hyp
1225            [ @Hbs2 >Hbs @memb_cons @Hyp
1226            | cases (orb_true_l … Hyp)
1227              [ #Hyp2 >(\P Hyp2) %
1228              | @Hl1
1229              ]
1230            ]
1231          ]
1232 ]]]]]
1233 qed.
1234
1235 axiom sem_compare : Realize ? compare R_compare.