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 lemma dec_test: ∀alpha,rs,test.
 115  decidable (∀c.memb alpha c rs = true → test c = false).
 116 #alpha #rs #test elim rs
 117   [%1 #n normalize #H destruct
 118   |#a #tl cases (true_or_false (test a)) #Ha
 119     [#_ %2 % #Hall @(absurd ?? not_eq_true_false) <Ha
 120      @Hall @memb_hd
 121     |* [#Hall %1 #c #memc cases (orb_true_l … memc)
 122          [#eqca >(\P eqca) @Ha |@Hall]
 123     |#Hnall %2 @(not_to_not … Hnall) #Hall #c #memc @Hall @memb_cons //
 124     ]
 125   qed.
 126
 127 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
 128   (current ? t1 = None ? → t1 = t2) ∧
 129   ∀ls,c,rs.
 130   (t1 = midtape alpha ls c rs  →
 131   ((test c = true ∧ t2 = t1) ∨
 132    (test c = false ∧
 133     (∀rs1,b,rs2. rs = rs1@b::rs2 →
 134      test b = true → (∀x.memb ? x rs1 = true → test x = false) →
 135      t2 = midtape ? (reverse ? rs1@c::ls) b rs2) ∧
 136      ((∀x.memb ? x rs = true → test x = false) →
 137       ∀a,l.reverse ? (c::rs) = a::l →
 138       t2 = rightof alpha a (l@ls))))).
 139
 140 definition adv_to_mark_r ≝
 141   λalpha,test.whileTM alpha (atmr_step alpha test) atm2.
 142
 143 lemma wsem_adv_to_mark_r :
 144   ∀alpha,test.
 145   WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
 146 #alpha #test #t #i #outc #Hloop
 147 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
 148 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 149 [ #tapea * #Htapea *
 150   [ #H1 %
 151     [#_ @Htapea
 152     |#ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
 153      #Hfalse destruct (Hfalse)
 154     ]
 155   | * #a * #Ha #Htest %
 156     [ >Ha #H destruct (H);
 157     | #ls #c #rs #H2 %
 158      >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
 159      <Htapea //
 160     ]
 161   ]
 162 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
 163   lapply (IH HRfalse) -IH #IH %
 164   [cases Hleft #ls * #a * #rs * * #Htapea #_ #_ >Htapea
 165    whd in ⊢((??%?)→?); #H destruct (H);
 166   |#ls #c #rs #Htapea %2
 167    cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
 168    >Htapea' in Htapea; #Htapea destruct (Htapea) % [ % // ]
 169    [*
 170     [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
 171      cases (proj2 ?? IH … Htapeb)
 172       [ * #_ #Houtc >Houtc >Htapeb %
 173       | * * >Htestb #Hfalse destruct (Hfalse) ]
 174     | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
 175      cases (proj2 ?? IH … Htapeb)
 176       [ * #Hfalse >(Hmemb …) in Hfalse;
 177         [ #Hft destruct (Hft)
 178         | @memb_hd ]
 179       | * * #Htestr1 #H1 #_ >reverse_cons >associative_append
 180        @H1 // #x #Hx @Hmemb @memb_cons //
 181       ]
 182     ]
 183    |cases rs in Htapeb; normalize in ⊢ (%→?);
 184     [#Htapeb #_ #a0 #l whd in ⊢ ((??%?)→?); #Hrev destruct (Hrev)
 185      >Htapeb in IH; #IH cases (proj1 ?? IH … (refl …)) //
 186     |#r1 #rs1 #Htapeb #Hmemb
 187      cases (proj2 ?? IH … Htapeb) [ * >Hmemb [ #Hfalse destruct(Hfalse) ] @memb_hd ]
 188      * #_ #H1 #a #l <(reverse_reverse … l) cases (reverse … l)
 189       [#H cut (c::r1::rs1 = [a])
 190         [<(reverse_reverse  … (c::r1::rs1)) >H //]
 191        #Hrev destruct (Hrev)
 192       |#a1 #l2 >reverse_cons >reverse_cons >reverse_cons
 193        #Hrev cut ([c] = [a1])
 194         [@(append_l2_injective_r ?? (a::reverse … l2) … Hrev) //]
 195        #Ha <Ha >associative_append @H1
 196         [#x #membx @Hmemb @memb_cons @membx
 197         |<(append_l1_injective_r ?? (a::reverse … l2) … Hrev) //
 198         ]
 199 qed.
 200
 201 lemma terminate_adv_to_mark_r :
 202   ∀alpha,test.
 203   ∀t.Terminate alpha (adv_to_mark_r alpha test) t.
 204 #alpha #test #t
 205 @(terminate_while … (sem_atmr_step alpha test))
 206   [ %
 207   | cases t
 208     [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 209     |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 210     | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
 211       elim rs
 212       [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 213        #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 214        % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
 215        normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
 216       | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 217         #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 218         >Ht1 @IH
 219       ]
 220     ]
 221   ]
 222 qed.
 223
 224 lemma sem_adv_to_mark_r :
 225   ∀alpha,test.
 226   Realize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
 227 /2/
 228 qed.
 229
 230 (* MARK machine
 231
 232    marks the current character
 233  *)
 234
 235 definition mark_states ≝ initN 2.
 236
 237 definition ms0 : mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
 238 definition ms1 : mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
 239
 240 definition mark ≝
 241   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
 242   (λp.let 〈q,a〉 ≝ p in
 243     match a with
 244     [ None ⇒ 〈ms1,None ?〉
 245     | Some a' ⇒ match (pi1 … q) with
 246       [ O ⇒ let 〈a'',b〉 ≝ a' in 〈ms1,Some ? 〈〈a'',true〉,N〉〉
 247       | S q ⇒ 〈ms1,None ?〉 ] ])
 248   ms0 (λq.q == ms1).
 249
 250 definition R_mark ≝ λalpha,t1,t2.
 251   (∀ls,c,b,rs.
 252      t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
 253      t2 = midtape ? ls 〈c,true〉 rs) ∧
 254   (current ? t1 = None ? → t2 = t1).
 255
 256 lemma sem_mark :
 257   ∀alpha.Realize ? (mark alpha) (R_mark alpha).
 258 #alpha #intape @(ex_intro ?? 2) cases intape
 259 [ @ex_intro
 260   [| % [ % | % [#ls #c #b #rs #Hfalse destruct | // ]]]
 261 |#a #al @ex_intro
 262   [| % [ % | % [#ls #c #b #rs #Hfalse destruct | // ]]]
 263 |#a #al @ex_intro
 264   [| % [ % | % [#ls #c #b #rs #Hfalse destruct ] // ]]
 265 | #ls * #c #b #rs
 266   @ex_intro [| % [ % | %
 267   [#ls0 #c0 #b0 #rs0 #H1 destruct (H1) %
 268   | whd in ⊢ ((??%?)→?); #H1 destruct (H1)]]]
 269 qed.
 270
 271
 272 (* MOVE RIGHT AND MARK machine
 273
 274    marks the first character on the right
 275
 276    (could be rewritten using (mark; move_right))
 277  *)
 278
 279 definition mrm_states ≝ initN 3.
 280
 281 definition mrm0 : mrm_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
 282 definition mrm1 : mrm_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
 283 definition mrm2 : mrm_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
 284
 285 definition move_right_and_mark ≝
 286   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mrm_states
 287   (λp.let 〈q,a〉 ≝ p in
 288     match a with
 289     [ None ⇒ 〈mrm2,None ?〉
 290     | Some a' ⇒ match pi1 … q with
 291       [ O ⇒ 〈mrm1,Some ? 〈a',R〉〉
 292       | S q ⇒ match q with
 293         [ O ⇒ let 〈a'',b〉 ≝ a' in
 294               〈mrm2,Some ? 〈〈a'',true〉,N〉〉
 295         | S _ ⇒ 〈mrm2,None ?〉 ] ] ])
 296   mrm0 (λq.q == mrm2).
 297
 298 definition R_move_right_and_mark ≝ λalpha,t1,t2.
 299   ∀ls,c,d,b,rs.
 300   t1 = midtape (FinProd … alpha FinBool) ls c (〈d,b〉::rs) →
 301   t2 = midtape ? (c::ls) 〈d,true〉 rs.
 302
 303 lemma sem_move_right_and_mark :
 304   ∀alpha.Realize ? (move_right_and_mark alpha) (R_move_right_and_mark alpha).
 305 #alpha #intape @(ex_intro ?? 3) cases intape
 306 [ @ex_intro
 307   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 308 |#a #al @ex_intro
 309   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 310 |#a #al @ex_intro
 311   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 312 | #ls #c *
 313   [ @ex_intro [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #Hfalse destruct ] ]
 314   | * #d #b #rs @ex_intro
 315     [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #H1 destruct (H1) % ] ] ] ]
 316 qed.
 317
 318 (* CLEAR MARK machine
 319
 320    clears the mark in the current character
 321  *)
 322
 323 definition clear_mark_states ≝ initN 3.
 324
 325 definition clear0 : clear_mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
 326 definition clear1 : clear_mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
 327 definition claer2 : clear_mark_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
 328
 329 definition clear_mark ≝
 330   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) clear_mark_states
 331   (λp.let 〈q,a〉 ≝ p in
 332     match a with
 333     [ None ⇒ 〈clear1,None ?〉
 334     | Some a' ⇒ match pi1 … q with
 335       [ O ⇒ let 〈a'',b〉 ≝ a' in 〈clear1,Some ? 〈〈a'',false〉,N〉〉
 336       | S q ⇒ 〈clear1,None ?〉 ] ])
 337   clear0 (λq.q == clear1).
 338
 339 definition R_clear_mark ≝ λalpha,t1,t2.
 340   (current ? t1 = None ? → t1 = t2) ∧
 341   ∀ls,c,b,rs.
 342   t1 = midtape (FinProd … alpha FinBool) ls 〈c,b〉 rs →
 343   t2 = midtape ? ls 〈c,false〉 rs.
 344
 345 lemma sem_clear_mark :
 346   ∀alpha.Realize ? (clear_mark alpha) (R_clear_mark alpha).
 347 #alpha #intape @(ex_intro ?? 2) cases intape
 348 [ @ex_intro
 349   [| % [ % | % [#_ %|#ls #c #b #rs #Hfalse destruct ]]]
 350 |#a #al @ex_intro
 351   [| % [ % | % [#_ %|#ls #c #b #rs #Hfalse destruct ]]]
 352 |#a #al @ex_intro
 353   [| % [ % | % [#_ %|#ls #c #b #rs #Hfalse destruct ]]]
 354 | #ls * #c #b #rs
 355   @ex_intro [| % [ % | %
 356   [whd in ⊢ (??%?→?); #H destruct| #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ]]]]
 357 qed.
 358
 359 (* ADVANCE MARK RIGHT machine
 360
 361    clears mark on current char,
 362    moves right, and marks new current char
 363
 364 *)
 365
 366 definition adv_mark_r ≝
 367   λalpha:FinSet.
 368     clear_mark alpha · move_r ? · mark alpha.
 369
 370 definition R_adv_mark_r ≝ λalpha,t1,t2.
 371   (∀ls,c.
 372     (∀d,b,rs.
 373      t1 = midtape (FinProd … alpha FinBool) ls 〈c,true〉 (〈d,b〉::rs) →
 374      t2 = midtape ? (〈c,false〉::ls) 〈d,true〉 rs) ∧
 375     (t1 = midtape (FinProd … alpha FinBool) ls 〈c,true〉 [ ] →
 376      t2 = rightof ? 〈c,false〉 ls)) ∧
 377   (current ? t1 = None ? → t1 = t2).
 378
 379 lemma sem_adv_mark_r :
 380   ∀alpha.Realize ? (adv_mark_r alpha) (R_adv_mark_r alpha).
 381 #alpha
 382 @(sem_seq_app … (sem_clear_mark …)
 383          (sem_seq ????? (sem_move_r ?) (sem_mark alpha)) …)
 384 #intape #outtape whd in ⊢ (%→?); * #ta *
 385 whd in ⊢ (%→?); #Hs1 whd in ⊢ (%→?); * #tb * #Hs2 whd in ⊢ (%→?); #Hs3 %
 386   [#ls #c %
 387     [#d #b #rs #Hintape @(proj1 … Hs3 ?? b ?)
 388      @(proj2 … Hs2 ls 〈c,false〉 (〈d,b〉::rs))
 389      @(proj2 ?? Hs1 … Hintape)
 390     |#Hintape lapply (proj2 ?? Hs1 … Hintape) #Hta lapply (proj2 … Hs2 … Hta)
 391      whd in ⊢ ((???%)→?); #Htb <Htb @(proj2 … Hs3) >Htb //
 392     ]
 393   |#Hcur lapply(proj1 ?? Hs1 … Hcur) #Hta >Hta >Hta in Hcur; #Hcur
 394    lapply (proj1 ?? Hs2 … Hcur) #Htb >Htb >Htb in Hcur; #Hcur
 395    @sym_eq @(proj2 ?? Hs3) @Hcur
 396   ]
 397 qed.
 398
 399 (* ADVANCE TO MARK (left)
 400
 401 axiomatized
 402
 403 *)
 404 definition atml_step ≝
 405   λalpha:FinSet.λtest:alpha→bool.
 406   mk_TM alpha atm_states
 407   (λp.let 〈q,a〉 ≝ p in
 408    match a with
 409    [ None ⇒ 〈atm1, None ?〉
 410    | Some a' ⇒
 411      match test a' with
 412      [ true ⇒ 〈atm1,None ?〉
 413      | false ⇒ 〈atm2,Some ? 〈a',L〉〉 ]])
 414   atm0 (λx.notb (x == atm0)).
 415
 416 definition Ratml_step_true ≝
 417   λalpha,test,t1,t2.
 418    ∃ls,a,rs.
 419    t1 = midtape alpha ls a rs ∧ test a = false ∧
 420    t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a :: rs).
 421
 422 definition Ratml_step_false ≝
 423   λalpha,test,t1,t2.
 424     t1 = t2 ∧
 425     (current alpha t1 = None ? ∨
 426      (∃a.current ? t1 = Some ? a ∧ test a = true)).
 427
 428 lemma atml_q0_q1 :
 429   ∀alpha,test,ls,a0,rs. test a0 = true →
 430   step alpha (atml_step alpha test)
 431     (mk_config ?? atm0 (midtape … ls a0 rs)) =
 432   mk_config alpha (states ? (atml_step alpha test)) atm1
 433     (midtape … ls a0 rs).
 434 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
 435 whd in match (trans … 〈?,?〉); >Htest %
 436 qed.
 437
 438 lemma atml_q0_q2 :
 439   ∀alpha,test,ls,a0,rs. test a0 = false →
 440   step alpha (atml_step alpha test)
 441     (mk_config ?? atm0 (midtape … ls a0 rs)) =
 442   mk_config alpha (states ? (atml_step alpha test)) atm2
 443     (mk_tape … (tail ? ls) (option_hd ? ls) (a0 :: rs)).
 444 #alpha #test #ls #a0 #rs #Htest whd in ⊢ (??%?);
 445 whd in match (trans … 〈?,?〉); >Htest cases ls //
 446 qed.
 447
 448 lemma sem_atml_step :
 449   ∀alpha,test.
 450   accRealize alpha (atml_step alpha test)
 451     atm2 (Ratml_step_true alpha test) (Ratml_step_false alpha test).
 452 #alpha #test *
 453 [ @(ex_intro ?? 2)
 454   @(ex_intro ?? (mk_config ?? atm1 (niltape ?))) %
 455   [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
 456 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (leftof ? a al)))
 457   % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
 458 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (rightof ? a al)))
 459   % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
 460 | #ls #c #rs @(ex_intro ?? 2)
 461   cases (true_or_false (test c)) #Htest
 462   [ @(ex_intro ?? (mk_config ?? atm1 ?))
 463     [| %
 464       [ %
 465         [ whd in ⊢ (??%?); >atml_q0_q1 //
 466         | whd in ⊢ ((??%%)→?); #Hfalse destruct ]
 467       | #_ % // %2 @(ex_intro ?? c) % // ]
 468     ]
 469   | @(ex_intro ?? (mk_config ?? atm2 (mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs))))
 470     %
 471     [ %
 472       [ whd in ⊢ (??%?); >atml_q0_q2 //
 473       | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
 474         % // % //
 475       ]
 476     | #Hfalse @False_ind @(absurd ?? Hfalse) %
 477     ]
 478   ]
 479 ]
 480 qed.
 481
 482 definition R_adv_to_mark_l ≝ λalpha,test,t1,t2.
 483   (current ? t1 = None ? → t1 = t2) ∧
 484   ∀ls,c,rs.
 485   (t1 = midtape alpha ls c rs  →
 486   ((test c = true → t2 = t1) ∧
 487    (test c = false →
 488     (∀ls1,b,ls2. ls = ls1@b::ls2 →
 489      test b = true → (∀x.memb ? x ls1 = true → test x = false) →
 490      t2 = midtape ? ls2 b (reverse ? ls1@c::rs)) ∧
 491     ((∀x.memb ? x ls = true → test x = false) →
 492       ∀a,l. reverse ? (c::ls) = a::l → t2 = leftof ? a (l@rs))
 493      ))).
 494
 495 definition adv_to_mark_l ≝
 496   λalpha,test.whileTM alpha (atml_step alpha test) atm2.
 497
 498 lemma wsem_adv_to_mark_l :
 499   ∀alpha,test.
 500   WRealize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
 501 #alpha #test #t #i #outc #Hloop
 502 lapply (sem_while … (sem_atml_step alpha test) t i outc Hloop) [%]
 503 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 504 [ #tapea * #Htapea *
 505   [ #H1 %
 506     [#_ @Htapea
 507     |#ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
 508      #Hfalse destruct (Hfalse)
 509     ]
 510   | * #a * #Ha #Htest %
 511     [>Ha #H destruct (H);
 512     |#ls #c #rs #H2 %
 513       [#Hc <Htapea //
 514       |#Hc @False_ind >H2 in Ha; whd in ⊢ ((??%?)→?);
 515        #H destruct (H) /2/
 516       ]
 517     ]
 518   ]
 519 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
 520   lapply (IH HRfalse) -IH #IH %
 521   [cases Hleft #ls0 * #a0 * #rs0 * * #Htapea #_ #_ >Htapea
 522    whd in ⊢ ((??%?)→?); #H destruct (H)
 523   |#ls #c #rs #Htapea %
 524     [#Hc cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest @False_ind
 525      >Htapea' in Htapea; #H destruct /2/
 526     |cases Hleft #ls0 * #a * #rs0 *
 527      * #Htapea1 >Htapea in Htapea1; #H destruct (H) #_ #Htapeb
 528      #Hc %
 529       [*
 530         [#b #ls2 #Hls >Hls in Htapeb; #Htapeb #Htestb #_
 531          cases (proj2 ?? IH … Htapeb) #H1 #_ >H1 // >Htapeb %
 532         |#l1 #ls1 #b #ls2 #Hls >Hls in Htapeb; #Htapeb #Htestb #Hmemb
 533          cases (proj2 ?? IH … Htapeb) #_ #H1 >reverse_cons >associative_append
 534          @(proj1 ?? (H1 ?) … (refl …) Htestb …)
 535           [@Hmemb @memb_hd
 536           |#x #memx @Hmemb @memb_cons @memx
 537           ]
 538         ]
 539       |cases ls0 in Htapeb; normalize in ⊢ (%→?);
 540         [#Htapeb #Htest #a0 #l whd in ⊢ ((??%?)→?); #Hrev destruct (Hrev)
 541          >Htapeb in IH; #IH cases (proj1 ?? IH … (refl …)) //
 542         |#l1 #ls1 #Htapeb
 543          cases (proj2 ?? IH … Htapeb) #_ #H1 #Htest #a0 #l
 544          <(reverse_reverse … l) cases (reverse … l)
 545           [#H cut (a::l1::ls1 = [a0])
 546             [<(reverse_reverse  … (a::l1::ls1)) >H //]
 547            #Hrev destruct (Hrev)
 548           |#a1 #l2 >reverse_cons >reverse_cons >reverse_cons
 549            #Hrev cut ([a] = [a1])
 550             [@(append_l2_injective_r ?? (a0::reverse … l2) … Hrev) //]
 551            #Ha <Ha >associative_append @(proj2 ?? (H1 ?))
 552             [@Htest @memb_hd
 553             |#x #membx @Htest @memb_cons @membx
 554             |<(append_l1_injective_r ?? (a0::reverse … l2) … Hrev) //
 555             ]
 556           ]
 557         ]
 558       ]
 559     ]
 560   ]
 561 qed.
 562
 563 lemma terminate_adv_to_mark_l :
 564   ∀alpha,test.
 565   ∀t.Terminate alpha (adv_to_mark_l alpha test) t.
 566 #alpha #test #t
 567 @(terminate_while … (sem_atml_step alpha test))
 568   [ %
 569   | cases t
 570     [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 571     |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 572     | #ls elim ls
 573       [#c #rs % #t1 * #ls0 * #c0 * #rs0 * *
 574        #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 575        % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
 576        normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
 577       | #rs0 #r0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 578         #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 579         >Ht1 @IH
 580       ]
 581     ]
 582   ]
 583 qed.
 584
 585 lemma sem_adv_to_mark_l :
 586   ∀alpha,test.
 587   Realize alpha (adv_to_mark_l alpha test) (R_adv_to_mark_l alpha test).
 588 /2/
 589 qed.
 590
 591 (*
 592    ADVANCE BOTH MARKS machine
 593
 594    l1 does not contain marks ⇒
 595
 596
 597    input:
 598    l0 x* a l1 x0* a0 l2
 599               ^
 600
 601    output:
 602    l0 x a* l1 x0 a0* l2
 603         ^
 604 *)
 605
 606 definition adv_both_marks ≝ λalpha.
 607   adv_mark_r alpha · move_l ? ·
 608     adv_to_mark_l (FinProd alpha FinBool) (is_marked alpha) ·
 609       adv_mark_r alpha.
 610
 611 definition R_adv_both_marks ≝ λalpha,t1,t2.
 612   ∀ls,x0,rs.
 613     t1 = midtape (FinProd … alpha FinBool) ls 〈x0,true〉 rs →
 614      (rs = [ ] → (* first case: rs empty *)
 615        t2 = rightof (FinProd … alpha FinBool) 〈x0,false〉 ls) ∧
 616      (∀l0,x,a,a0,b,l1,l1',l2.
 617        ls = (l1@〈x,true〉::l0) →
 618        (∀c.memb ? c l1 = true → is_marked ? c = false) →
 619        rs = (〈a0,b〉::l2) →
 620        reverse ? (〈x0,false〉::l1) = 〈a,false〉::l1' →
 621        t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1'@〈a0,true〉::l2)).
 622
 623 lemma sem_adv_both_marks :
 624   ∀alpha.Realize ? (adv_both_marks alpha) (R_adv_both_marks alpha).
 625 #alpha
 626 @(sem_seq_app … (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))) …)
 630 #intape #outtape * #tapea * #Hta * #tb * #Htb * #tc * #Htc #Hout
 631 #ls #c #rs #Hintape %
 632   [#Hrs >Hrs in Hintape; #Hintape lapply (proj2 ?? (proj1 ?? Hta … ) … Hintape) -Hta #Hta
 633    lapply (proj1 … Htb) >Hta -Htb #Htb lapply (Htb (refl …)) -Htb #Htb
 634    lapply (proj1 ?? Htc) <Htb -Htc #Htc lapply (Htc (refl …)) -Htc #Htc
 635    @sym_eq >Htc @(proj2 ?? Hout …) <Htc %
 636   |#l0 #x #a #a0 #b #l1 #l1' #l2 #Hls #Hmarks #Hrs #Hrev
 637    >Hrs in Hintape; >Hls #Hintape
 638    @(proj1 ?? (proj1 ?? Hout … ) ? false) -Hout
 639    lapply (proj1 … (proj1 … Hta …) … Hintape) #Htapea
 640    lapply (proj2 … Htb  … Htapea) -Htb
 641    whd in match (mk_tape ????) ; #Htapeb
 642    lapply (proj1 ?? (proj2 ?? (proj2 ?? Htc … Htapeb) (refl …))) -Htc #Htc
 643    change with ((?::?)@?) in match (cons ???); <Hrev >reverse_cons
 644    >associative_append @Htc [%|%|@Hmarks]
 645   ]
 646 qed.
 647
 648 (*
 649 definition R_adv_both_marks ≝
 650   λalpha,t1,t2.
 651     ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) →
 652     (t1 = midtape (FinProd … alpha FinBool)
 653         (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) →
 654      t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2)) ∧
 655      (t1 = midtape (FinProd … alpha FinBool)
 656         (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 [] →
 657      t2 = rightof ? 〈x0,false〉 (l1@〈a,false〉::〈x,true〉::l0)).
 658
 659 lemma sem_adv_both_marks :
 660   ∀alpha.Realize ? (adv_both_marks alpha) (R_adv_both_marks alpha).
 661 #alpha #intape
 662 cases (sem_seq ????? (sem_adv_mark_r …)
 663         (sem_seq ????? (sem_move_l …)
 664           (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?))
 665             (sem_adv_mark_r alpha))) intape)
 666 #k * #outc * #Hloop whd in ⊢ (%→?);
 667 * #ta * whd in ⊢ (%→?); #Hs1 * #tb * whd in ⊢ (%→?); #Hs2
 668 * #tc * whd in ⊢ (%→%→?); #Hs3 #Hs4
 669 @(ex_intro ?? k) @(ex_intro ?? outc) %
 670 [ @Hloop
 671 | -Hloop #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape
 672   @(Hs4 … false) -Hs4
 673   lapply (Hs1 … Hintape) #Hta
 674   lapply (proj2 … Hs2 … Hta) #Htb
 675   cases (Hs3 … Htb)
 676   [ * #Hfalse normalize in Hfalse; destruct (Hfalse)
 677   | * #_ -Hs3 #Hs3
 678     lapply (Hs3 (l1@[〈a,false〉]) 〈x,true〉 l0 ???)
 679     [ #x1 #Hx1 cases (memb_append … Hx1)
 680       [ @Hl1
 681       | #Hx1' >(memb_single … Hx1') % ]
 682     | %
 683     | >associative_append %
 684     | >reverse_append #Htc @Htc ]
 685   ]
 686 qed. *)
 687
 688 (*
 689    MATCH AND ADVANCE(f)
 690
 691    input:
 692    l0 x* a l1 x0* a0 l2
 693               ^
 694
 695    output:
 696    l0 x a* l1 x0 a0* l2   (f(x0) == true)
 697         ^
 698    l0 x* a l1 x0* a0 l2   (f(x0) == false)
 699               ^
 700 *)
 701
 702 definition match_and_adv ≝
 703   λalpha,f.ifTM ? (test_char ? f)
 704      (adv_both_marks alpha) (clear_mark ?) tc_true.
 705
 706 definition R_match_and_adv ≝
 707   λalpha,f,t1,t2.
 708     ∀ls,x0,rs.
 709      t1 = midtape (FinProd … alpha FinBool) ls 〈x0,true〉 rs →
 710     ((* first case: (f 〈x0,true〉 = false) *)
 711      (f 〈x0,true〉 = false) →
 712        t2 = midtape (FinProd … alpha FinBool) ls 〈x0,false〉 rs) ∧
 713     ((f 〈x0,true〉 = true) →  rs = [ ] → (* second case: rs empty *)
 714        t2 = rightof (FinProd … alpha FinBool) 〈x0,false〉 ls) ∧
 715     ((f 〈x0,true〉 = true) →
 716      ∀l0,x,a,a0,b,l1,l1',l2.
 717      (* third case: we expect to have a mark on the left! *)
 718      ls = (l1@〈x,true〉::l0) →
 719      (∀c.memb ? c l1 = true → is_marked ? c = false) →
 720      rs = 〈a0,b〉::l2 →
 721      reverse ? (〈x0,false〉::l1) = 〈a,false〉::l1' →
 722        t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1'@〈a0,true〉::l2)).
 723
 724 lemma sem_match_and_adv :
 725   ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv alpha f).
 726 #alpha #f #intape
 727 cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape)
 728 #k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
 729 % [ @Hloop ] -Hloop
 730 (*
 731 @(sem_if_app … (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?))
 732 #intape #outape #Htb * #H *)
 733 cases Hif -Hif
 734 [ * #ta * whd in ⊢ (%→%→?); * * #c * #Hcurrent #fc #Hta #Houtc
 735   #ls #x #rs #Hintape >Hintape in Hcurrent; whd in ⊢ ((??%?)→?); #H destruct (H) %
 736   [%[>fc #H destruct (H)
 737     |#_ #Hrs >Hrs in Hintape; #Hintape >Hintape in Hta; #Hta
 738      cases (Houtc … Hta) #Houtc #_ @Houtc //
 739     ]
 740   |#l0 #x0 #a #a0 #b #l1 #l1' #l2 #Hls #Hmarks #Hrs #Hrev >Hintape in Hta; #Hta
 741    @(proj2 ?? (Houtc … Hta) … Hls Hmarks Hrs Hrev)
 742   ]
 743 | * #ta * * #H #Hta * #_ #Houtc #ls #c #rs #Hintape
 744    >Hintape in H; #H lapply(H … (refl …)) #fc %
 745   [%[#_ >Hintape in Hta; #Hta @(Houtc … Hta)
 746     |>fc #H destruct (H)
 747     ]
 748   |>fc #H destruct (H)
 749   ]
 750 ]
 751 qed.
 752
 753 (*
 754 lemma sem_match_and_adv :
 755   ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv alpha f).
 756 #alpha #f #intape
 757 cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape)
 758 #k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
 759 % [ @Hloop ] -Hloop
 760 cases Hif
 761 [ * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
 762   #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape >Hintape in Hta;
 763   * * #x1 * whd in ⊢ ((??%?)→?); #H destruct (H) #Hf #Hta % %
 764   [ @Hf | >append_cons >append_cons in Hta; #Hta @(proj1 ?? (Houtc …) …Hta)
 765     [ #x #memx cases (memb_append …memx)
 766       [@Hl1 | -memx #memx >(memb_single … memx) %]
 767     |>reverse_cons >reverse_append % ] ]
 768 | * #ta * whd in ⊢ (%→%→?); #Hta #Houtc
 769   #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape >Hintape in Hta;
 770   * #Hf #Hta %2 % [ @Hf % | >(proj2 ?? Houtc … Hta) % ]
 771 ]
 772 qed.
 773 *)
 774
 775 definition R_match_and_adv_of ≝
 776   λalpha,t1,t2.current (FinProd … alpha FinBool) t1 = None ? → t2 = t1.
 777
 778 lemma sem_match_and_adv_of :
 779   ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv_of alpha).
 780 #alpha #f #intape
 781 cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape)
 782 #k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
 783 % [ @Hloop ] -Hloop
 784 cases Hif
 785 [ * #ta * whd in ⊢ (%→%→?); #Hta #Houtc #Hcur
 786   cases Hta * #x >Hcur * #Hfalse destruct (Hfalse)
 787 | * #ta * whd in ⊢ (%→%→?); * #_ #Hta * #Houtc #_ <Hta #Hcur >(Houtc Hcur) % ]
 788 qed.
 789
 790 lemma sem_match_and_adv_full :
 791   ∀alpha,f.Realize ? (match_and_adv alpha f)
 792     (R_match_and_adv alpha f ∩ R_match_and_adv_of alpha).
 793 #alpha #f #intape cases (sem_match_and_adv ? f intape)
 794 #i * #outc * #Hloop #HR1 %{i} %{outc} % // % //
 795 cases (sem_match_and_adv_of ? f intape) #i0 * #outc0 * #Hloop0 #HR2
 796 >(loop_eq … Hloop Hloop0) //
 797 qed.
 798
 799 (*
 800  if x = c
 801       then move_right; ----
 802            adv_to_mark_r;
 803            if current (* x0 *) = 0
 804               then advance_mark ----
 805                    adv_to_mark_l;
 806                    advance_mark
 807               else STOP
 808       else M
 809 *)
 810
 811 definition comp_step_subcase ≝ λalpha,c,elseM.
 812   ifTM ? (test_char ? (λx.x == c))
 813     (move_r … · adv_to_mark_r ? (is_marked alpha) · match_and_adv ? (λx.x == c))
 814     elseM tc_true.
 815
 816 definition R_comp_step_subcase ≝
 817   λalpha,c,RelseM,t1,t2.
 818     ∀ls,x,rs.t1 = midtape (FinProd … alpha FinBool) ls 〈x,true〉 rs →
 819     (〈x,true〉 = c →
 820      ((* test true but no marks in rs *)
 821       (∀c.memb ? c rs = true → is_marked ? c = false) →
 822        ∀a,l. (a::l) = reverse ? (〈x,true〉::rs) →
 823        t2 = rightof (FinProd alpha FinBool) a (l@ls)) ∧
 824     ∀l1,x0,l2.
 825      (∀c.memb ? c l1 = true → is_marked ? c = false) →
 826       rs = l1@〈x0,true〉::l2 →
 827       (x = x0 →
 828        l2 = [ ] → (* test true but l2 is empty *)
 829        t2 = rightof ? 〈x0,false〉 ((reverse ? l1)@〈x,true〉::ls))  ∧
 830       (x = x0 →
 831        ∀a,a0,b,l1',l2'. (* test true and l2 is not empty *)
 832        〈a,false〉::l1' = l1@[〈x0,false〉] →
 833        l2 = 〈a0,b〉::l2' →
 834        t2 = midtape ? (〈x,false〉::ls) 〈a,true〉 (l1'@〈a0,true〉::l2')) ∧
 835       (x ≠ x0 →(* test false *)
 836       t2 = midtape (FinProd … alpha FinBool) ((reverse ? l1)@〈x,true〉::ls) 〈x0,false〉 l2)) ∧
 837     (〈x,true〉 ≠ c → RelseM t1 t2).
 838
 839 lemma dec_marked: ∀alpha,rs.
 840  decidable (∀c.memb ? c rs = true → is_marked alpha c = false).
 841 #alpha #rs elim rs
 842   [%1 #n normalize #H destruct
 843   |#a #tl cases (true_or_false (is_marked ? a)) #Ha
 844     [#_ %2 % #Hall @(absurd ?? not_eq_true_false) <Ha
 845      @Hall @memb_hd
 846     |* [#Hall %1 #c #memc cases (orb_true_l … memc)
 847          [#eqca >(\P eqca) @Ha |@Hall]
 848     |#Hnall %2 @(not_to_not … Hnall) #Hall #c #memc @Hall @memb_cons //
 849     ]
 850   qed.
 851
 852 (* axiom daemon:∀P:Prop.P. *)
 853
 854 lemma sem_comp_step_subcase :
 855   ∀alpha,c,elseM,RelseM.
 856   Realize ? elseM RelseM →
 857   Realize ? (comp_step_subcase alpha c elseM)
 858     (R_comp_step_subcase alpha c RelseM).
 859 #alpha #c #elseM #RelseM #Helse #intape
 860 cases (sem_if ? (test_char ? (λx.x == c)) … tc_true
 861         (sem_test_char ? (λx.x == c))
 862         (sem_seq ????? (sem_move_r …)
 863           (sem_seq ????? (sem_adv_to_mark_r ? (is_marked alpha))
 864              (sem_match_and_adv_full ? (λx.x == c)))) Helse intape)
 865 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc)
 866 % [ @Hloop ] -Hloop cases HR -HR
 867   [* #ta * whd in ⊢ (%→?); * * #cin * #Hcin #Hcintrue #Hta * #tb * whd in ⊢ (%→?); #Htb
 868    * #tc * whd in ⊢ (%→?); #Htc * whd in ⊢ (%→%→?); #Houtc #Houtc1
 869    #ls #x #rs #Hintape >Hintape in Hcin; whd in ⊢ ((??%?)→?); #H destruct (H) %
 870     [#_ cases (dec_marked ? rs) #Hdec
 871       [%
 872         [#_ #a #l1
 873          >Hintape in Hta; #Hta
 874          lapply (proj2 ?? Htb … Hta) -Htb -Hta cases rs in Hdec;
 875            (* by cases on rs *)
 876            [#_ whd in ⊢ ((???%)→?); #Htb >Htb in Htc; #Htc
 877             lapply (proj1 ?? Htc (refl …)) -Htc #Htc <Htc in Houtc1; #Houtc1
 878             normalize in ⊢ (???%→?); #Hl1 destruct(Hl1) @(Houtc1 (refl …))
 879            |#r0 #rs0 #Hdec whd in ⊢ ((???%)→?); #Htb >Htb in Htc; #Htc
 880             >reverse_cons >reverse_cons #Hl1
 881             cases (proj2 ?? Htc … (refl …))
 882             [* >(Hdec …) [ #Hfalse destruct(Hfalse) ] @memb_hd
 883             |* #_ -Htc #Htc cut (∃l2.l1 = l2@[〈x,true〉])
 884              [generalize in match Hl1; -Hl1 <(reverse_reverse … l1)
 885               cases (reverse ? l1)
 886               [#Hl1 cut ([a]=〈x,true〉::r0::rs0)
 887                [ <(reverse_reverse … (〈x,true〉::r0::rs0))
 888                  >reverse_cons >reverse_cons <Hl1 %
 889                | #Hfalse destruct(Hfalse)]
 890               |#a0 #l10 >reverse_cons #Heq
 891                lapply (append_l2_injective_r ? (a::reverse ? l10) ???? Heq) //
 892                #Ha0 destruct(Ha0) /2/ ]
 893              |* #l2 #Hl2 >Hl2 in Hl1; #Hl1
 894               lapply (append_l1_injective_r ? (a::l2) … Hl1) // -Hl1 #Hl1
 895               >reverse_cons in Htc; #Htc lapply (Htc … (sym_eq … Hl1))
 896               [ #x0 #Hmemb @Hdec @memb_cons @Hmemb ]
 897               -Htc #Htc >Htc in Houtc1; #Houtc1 >associative_append @Houtc1 %
 898              ]
 899             ]
 900            ]
 901         |#l1 #x0 #l2 #_ #Hrs @False_ind
 902          @(absurd ?? not_eq_true_false)
 903          change with (is_marked ? 〈x0,true〉) in match true;
 904          @Hdec >Hrs @memb_append_l2 @memb_hd
 905         ]
 906       |% [#H @False_ind @(absurd …H Hdec)]
 907        (* by cases on l1 *) *
 908         [#x0 #l2 #Hdec normalize in ⊢ (%→?); #Hrs >Hrs in Hintape; #Hintape
 909          >Hintape in Hta; (* * * #x1 * whd in ⊢ ((??%?)→?); #H destruct (H) #Hx *)
 910          #Hta lapply (proj2 … Htb … Hta) -Htb -Hta
 911          whd in match (mk_tape ????); whd in match (tail ??); #Htb cases Htc -Htc
 912          #_ #Htc cases (Htc … Htb) -Htc
 913           [2: * * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
 914          * * #Htc >Htb in Htc; -Htb #Htc cases (Houtc … Htc) -Houtc *
 915          #H1 #H2 #H3 cases (true_or_false (x==x0)) #eqxx0
 916           [>(\P eqxx0) % [2: #H @False_ind /2/] %
 917             [#_ #Hl2 >(H2 … Hl2) <(\P eqxx0) [% | @Hcintrue]
 918             |#_ #a #a0 #b #l1' #l2' normalize in ⊢ (%→?); #Hdes destruct (Hdes)
 919              #Hl2 @(H3 … Hdec … Hl2) <(\P eqxx0) [@Hcintrue | % | @reverse_single]
 920             ]
 921           |% [% #eqx @False_ind lapply (\Pf eqxx0) #Habs @(absurd … eqx Habs)]
 922            #_ @H1 @(\bf ?) @(not_to_not ??? (\Pf eqxx0)) <(\P Hcintrue)
 923            #Hdes destruct (Hdes) %
 924           ]
 925         |#l1hd #l1tl #x0 #l2 #Hdec normalize in ⊢ (%→?); #Hrs >Hrs in Hintape; #Hintape
 926          >Hintape in Hta; (* * * #x1 * whd in ⊢ ((??%?)→?); #H destruct (H) #Hx *)
 927          #Hta lapply (proj2 … Htb … Hta) -Htb -Hta
 928          whd in match (mk_tape ????); whd in match (tail ??); #Htb cases Htc -Htc
 929          #_ #Htc cases (Htc … Htb) -Htc
 930           [* #Hfalse @False_ind >(Hdec … (memb_hd …)) in Hfalse; #H destruct]
 931          * * #_ #Htc lapply (Htc … (refl …) (refl …) ?) -Htc
 932           [#x1 #membx1 @Hdec @memb_cons @membx1] #Htc
 933          cases (Houtc … Htc) -Houtc *
 934          #H1 #H2 #H3 #_ cases (true_or_false (x==x0)) #eqxx0
 935           [>(\P eqxx0) % [2: #H @False_ind /2/] %
 936             [#_ #Hl2 >(H2 … Hl2) <(\P eqxx0)
 937               [>reverse_cons >associative_append % | @Hcintrue]
 938             |#_ #a #a0 #b #l1' #l2' normalize in ⊢ (%→?); #Hdes (* destruct (Hdes) *)
 939              #Hl2 @(H3 ?????? (reverse … (l1hd::l1tl)) … Hl2) <(\P eqxx0)
 940               [@Hcintrue
 941               |>reverse_cons >associative_append %
 942               |#c0 #memc @Hdec <(reverse_reverse ? (l1hd::l1tl)) @memb_reverse @memc
 943               |>Hdes >reverse_cons >reverse_reverse >(\P eqxx0) %
 944               ]
 945             ]
 946           |% [% #eqx @False_ind lapply (\Pf eqxx0) #Habs @(absurd … eqx Habs)]
 947            #_ >reverse_cons >associative_append @H1 @(\bf ?)
 948            @(not_to_not ??? (\Pf eqxx0)) <(\P Hcintrue) #Hdes
 949            destruct (Hdes) %
 950           ]
 951         ]
 952       ]
 953     |>(\P Hcintrue) * #Hfalse @False_ind @Hfalse %
 954     ]
 955   | * #ta * * #Hcur #Hta #Houtc
 956     #l0 #x #rs #Hintape >Hintape in Hcur; #Hcur lapply (Hcur ? (refl …)) -Hcur #Hc %
 957     [ #Hfalse >Hfalse in Hc; #Hc cases (\Pf Hc) #Hc @False_ind @Hc %
 958     | -Hc #Hc <Hintape <Hta @Houtc ] ]
 959 qed.
 960
 961 (*
 962 - se marcato, itero
 963 - se non è marcato
 964   + se è un bit, ho fallito il confronto della tupla corrente
 965   + se è un separatore, la tupla fa match
 966
 967
 968 ifTM ? (test_char ? is_marked)
 969   (single_finalTM … (comp_step_subcase unialpha 〈bit false,true〉
 970     (comp_step_subcase unialpha 〈bit true,true〉
 971       (clear_mark …))))
 972   (nop ?)
 973 *)
 974
 975 definition comp_step ≝
 976   ifTM ? (test_char ? (is_marked ?))
 977   (single_finalTM … (comp_step_subcase FSUnialpha 〈bit false,true〉
 978     (comp_step_subcase FSUnialpha 〈bit true,true〉
 979       (comp_step_subcase FSUnialpha 〈null,true〉
 980         (clear_mark …)))))
 981   (nop ?)
 982   tc_true.
 983
 984 (* da spostare *)
 985
 986 lemma mem_append : ∀A,x,l1,l2. mem A x (l1@l2) →
 987   mem A x l1 ∨ mem A x l2.
 988 #A #x #l1 elim l1 normalize [/2/]
 989 #a #tl #Hind #l2 * [#eqxa %1 /2/ |#memx cases (Hind … memx) /3/]
 990 qed.
 991
 992 let rec split_on A (l:list A) f acc on l ≝
 993   match l with
 994   [ nil ⇒ 〈acc,nil ?〉
 995   | cons a tl ⇒
 996     if f a then 〈acc,a::tl〉 else split_on A tl f (a::acc)
 997   ].
 998
 999 lemma split_on_spec: ∀A,l,f,acc,res1,res2.
1000   split_on A l f acc = 〈res1,res2〉 →
1001     (∃l1. res1 = l1@acc ∧
1002     reverse ? l1@res2 = l ∧
1003     ∀x. mem ? x l1 → f x = false) ∧
1004     ∀a,tl. res2 = a::tl → f a = true.
1005 #A #l #f elim l
1006   [#acc #res1 #res2 normalize in ⊢ (%→?); #H destruct %
1007     [@(ex_intro … []) % normalize [% % | #x @False_ind]
1008     |#a #tl #H destruct
1009     ]
1010   |#a #tl #Hind #acc #res1 #res2 normalize in ⊢ (%→?);
1011    cases (true_or_false (f a)) #Hfa >Hfa normalize in ⊢ (%→?);
1012    #H destruct
1013    [% [@(ex_intro … []) % normalize [% % | #x @False_ind]
1014       |#a1 #tl1 #H destruct (H) //]
1015    |cases (Hind (a::acc) res1 res2 H) * #l1 * *
1016     #Hres1 #Htl #Hfalse #Htrue % [2:@Htrue] @(ex_intro … (l1@[a])) %
1017      [% [>associative_append @Hres1 | >reverse_append <Htl % ]
1018      |#x #Hmemx cases (mem_append ???? Hmemx)
1019         [@Hfalse | normalize * [#H >H //| @False_ind]
1020      ]
1021    ]
1022   ]
1023 qed.
1024
1025 axiom mem_reverse: ∀A,l,x. mem A x (reverse ? l) → mem A x l.
1026
1027 lemma split_on_spec_ex: ∀A,l,f.∃l1,l2.
1028     l1@l2 = l ∧ (∀x:A. mem ? x l1 → f x = false) ∧
1029     ∀a,tl. l2 = a::tl → f a = true.
1030 #A #l #f @(ex_intro … (reverse … (\fst (split_on A l f []))))
1031 @(ex_intro … (\snd (split_on A l f [])))
1032 cases (split_on_spec A l f [ ] ?? (eq_pair_fst_snd …)) * #l1 * *
1033 >append_nil #Hl1 >Hl1 #Hl #Hfalse #Htrue %
1034   [% [@Hl|#x #memx @Hfalse @mem_reverse //] | @Htrue]
1035 qed.
1036
1037 (* versione esistenziale *)
1038
1039 definition R_comp_step_true ≝ λt1,t2.
1040   ∃ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls 〈c,true〉 rs ∧
1041     ((* bit_or_null c = false *)
1042     (bit_or_null c = false → t2 = midtape ? ls 〈c,false〉 rs) ∧
1043     (* no marks in rs *)
1044     (bit_or_null c = true →
1045       (∀c.memb ? c rs = true → is_marked ? c = false) →
1046        ∀a,l. (a::l) = reverse ? (〈c,true〉::rs) →
1047        t2 = rightof (FinProd FSUnialpha FinBool) a (l@ls)) ∧
1048     (∀l1,c0,l2.
1049       bit_or_null c = true →
1050       (∀c.memb ? c l1 = true → is_marked ? c = false) →
1051       rs = l1@〈c0,true〉::l2 →
1052       (c = c0 →
1053        l2 = [ ] → (* test true but l2 is empty *)
1054        t2 = rightof ? 〈c0,false〉 ((reverse ? l1)@〈c,true〉::ls))  ∧
1055       (c = c0 →
1056        ∀a,a0,b,l1',l2'. (* test true and l2 is not empty *)
1057        〈a,false〉::l1' = l1@[〈c0,false〉] →
1058        l2 = 〈a0,b〉::l2' →
1059        t2 = midtape ? (〈c,false〉::ls) 〈a,true〉 (l1'@〈a0,true〉::l2')) ∧
1060       (c ≠ c0 →(* test false *)
1061        t2 = midtape (FinProd … FSUnialpha FinBool)
1062          ((reverse ? l1)@〈c,true〉::ls) 〈c0,false〉 l2))).
1063
1064 definition R_comp_step_false ≝
1065   λt1,t2.
1066    ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
1067    is_marked ? c = false ∧ t2 = t1.
1068
1069 lemma is_marked_to_exists: ∀alpha,c. is_marked alpha c = true →
1070  ∃c'. c = 〈c',true〉.
1071 #alpha * #c * [#_ @(ex_intro … c) //| normalize #H destruct]
1072 qed.
1073
1074 lemma exists_current: ∀alpha,c,t.
1075   current alpha t = Some alpha c → ∃ls,rs. t= midtape ? ls c rs.
1076 #alpha #c *
1077   [whd in ⊢ (??%?→?); #H destruct
1078   |#a #l whd in ⊢ (??%?→?); #H destruct
1079   |#a #l whd in ⊢ (??%?→?); #H destruct
1080   |#ls #c1 #rs whd in ⊢ (??%?→?); #H destruct
1081    @(ex_intro … ls) @(ex_intro … rs) //
1082   ]
1083 qed.
1084
1085 lemma sem_comp_step :
1086   accRealize ? comp_step (inr … (inl … (inr … start_nop)))
1087     R_comp_step_true R_comp_step_false.
1088 @(acc_sem_if_app … (sem_test_char ? (is_marked ?))
1089         (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
1090           (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ??
1091             (sem_comp_step_subcase FSUnialpha 〈null,true〉 ??
1092               (sem_clear_mark …))))
1093         (sem_nop …) …)
1094 [#intape #outape #ta #Hta #Htb cases Hta * #cm * #Hcur
1095  cases (exists_current … Hcur) #ls * #rs #Hintape #cmark
1096  cases (is_marked_to_exists … cmark) #c #Hcm
1097  >Hintape >Hcm -Hintape -Hcm #Hta
1098  @(ex_intro … ls) @(ex_intro … c) @(ex_intro …rs) % [//] lapply Hta -Hta
1099  (* #ls #c #rs #Hintape whd in Hta;
1100  >Hintape in Hta; * #_ -Hintape  forse non serve *)
1101  cases (true_or_false (c==bit false)) #Hc
1102   [>(\P Hc) #Hta %
1103     [%[whd in ⊢ ((??%?)→?); #Hdes destruct
1104       |#Hc @(proj1 ?? (proj1 ?? (Htb … Hta) (refl …)))
1105       ]
1106     |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (Htb … Hta) (refl …)))
1107     ]
1108   |cases (true_or_false (c==bit true)) #Hc1
1109     [>(\P Hc1) #Hta
1110       cut (〈bit true, true〉 ≠ 〈bit false, true〉) [% #Hdes destruct] #Hneq %
1111       [%[whd in ⊢ ((??%?)→?); #Hdes destruct
1112         |#Hc @(proj1 … (proj1 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) (refl …)))
1113         ]
1114       |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (proj2 ?? (Htb … Hta) Hneq … Hta)(refl …)))
1115       ]
1116     |cases (true_or_false (c==null)) #Hc2
1117       [>(\P Hc2) #Hta
1118         cut (〈null, true〉 ≠ 〈bit false, true〉) [% #Hdes destruct] #Hneq
1119         cut (〈null, true〉 ≠ 〈bit true, true〉) [% #Hdes destruct] #Hneq1 %
1120         [%[whd in ⊢ ((??%?)→?); #Hdes destruct
1121           |#Hc @(proj1 … (proj1 ?? (proj2 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) Hneq1 … Hta) (refl …)))
1122           ]
1123         |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (proj2 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) Hneq1 … Hta) (refl …)))
1124         ]
1125       |#Hta cut (bit_or_null c = false)
1126         [lapply Hc; lapply Hc1; lapply Hc2 -Hc -Hc1 -Hc2
1127          cases c normalize [* normalize /2/] /2/] #Hcut %
1128         [%[cases (Htb … Hta) #_ -Htb #Htb
1129            cases (Htb … Hta) [2: % #H destruct (H) normalize in Hc; destruct] #_ -Htb #Htb
1130            cases (Htb … Hta) [2: % #H destruct (H) normalize in Hc1; destruct] #_ -Htb #Htb
1131            lapply (Htb ?) [% #H destruct (H) normalize in Hc2; destruct]
1132            * #_ #Houttape #_ @(Houttape … Hta)
1133           |>Hcut #H destruct
1134           ]
1135         |#l1 #c0 #l2 >Hcut #H destruct
1136         ]
1137       ]
1138     ]
1139   ]
1140 |#intape #outape #ta #Hta #Htb #ls #c #rs #Hintape
1141  >Hintape in Hta; whd in ⊢ (%→?); * #Hmark #Hta % [@Hmark //]
1142  whd in Htb; >Htb //
1143 ]
1144 qed.
1145
1146 (* old universal version
1147
1148 definition R_comp_step_true ≝ λt1,t2.
1149   ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls 〈c,true〉 rs →
1150     (* bit_or_null c = false *)
1151     (bit_or_null c = false → t2 = midtape ? ls 〈c,false〉 rs) ∧
1152     (* no marks in rs *)
1153     (bit_or_null c = true →
1154       (∀c.memb ? c rs = true → is_marked ? c = false) →
1155        ∀a,l. (a::l) = reverse ? (〈c,true〉::rs) →
1156        t2 = rightof (FinProd FSUnialpha FinBool) a (l@ls)) ∧
1157     (∀l1,c0,l2.
1158       bit_or_null c = true →
1159       (∀c.memb ? c l1 = true → is_marked ? c = false) →
1160       rs = l1@〈c0,true〉::l2 →
1161       (c = c0 →
1162        l2 = [ ] → (* test true but l2 is empty *)
1163        t2 = rightof ? 〈c0,false〉 ((reverse ? l1)@〈c,true〉::ls))  ∧
1164       (c = c0 →
1165        ∀a,a0,b,l1',l2'. (* test true and l2 is not empty *)
1166        〈a,false〉::l1' = l1@[〈c0,false〉] →
1167        l2 = 〈a0,b〉::l2' →
1168        t2 = midtape ? (〈c,false〉::ls) 〈a,true〉 (l1'@〈a0,true〉::l2')) ∧
1169       (c ≠ c0 →(* test false *)
1170        t2 = midtape (FinProd … FSUnialpha FinBool)
1171          ((reverse ? l1)@〈c,true〉::ls) 〈c0,false〉 l2)).
1172
1173 definition R_comp_step_false ≝
1174   λt1,t2.
1175    ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
1176    is_marked ? c = false ∧ t2 = t1.
1177
1178 (*
1179 lemma is_marked_to_exists: ∀alpha,c. is_marked alpha c = true →
1180  ∃c'. c = 〈c',true〉.
1181 #alpha * c *)
1182
1183 lemma sem_comp_step :
1184   accRealize ? comp_step (inr … (inl … (inr … start_nop)))
1185     R_comp_step_true R_comp_step_false.
1186 @(acc_sem_if_app … (sem_test_char ? (is_marked ?))
1187         (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
1188           (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ??
1189             (sem_comp_step_subcase FSUnialpha 〈null,true〉 ??
1190               (sem_clear_mark …))))
1191         (sem_nop …) …)
1192 [#intape #outape #ta #Hta #Htb #ls #c #rs #Hintape whd in Hta;
1193  >Hintape in Hta; * #_ -Hintape (* forse non serve *)
1194  cases (true_or_false (c==bit false)) #Hc
1195   [>(\P Hc) #Hta %
1196     [%[whd in ⊢ ((??%?)→?); #Hdes destruct
1197       |#Hc @(proj1 ?? (proj1 ?? (Htb … Hta) (refl …)))
1198       ]
1199     |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (Htb … Hta) (refl …)))
1200     ]
1201   |cases (true_or_false (c==bit true)) #Hc1
1202     [>(\P Hc1) #Hta
1203       cut (〈bit true, true〉 ≠ 〈bit false, true〉) [% #Hdes destruct] #Hneq %
1204       [%[whd in ⊢ ((??%?)→?); #Hdes destruct
1205         |#Hc @(proj1 … (proj1 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) (refl …)))
1206         ]
1207       |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (proj2 ?? (Htb … Hta) Hneq … Hta)(refl …)))
1208       ]
1209     |cases (true_or_false (c==null)) #Hc2
1210       [>(\P Hc2) #Hta
1211         cut (〈null, true〉 ≠ 〈bit false, true〉) [% #Hdes destruct] #Hneq
1212         cut (〈null, true〉 ≠ 〈bit true, true〉) [% #Hdes destruct] #Hneq1 %
1213         [%[whd in ⊢ ((??%?)→?); #Hdes destruct
1214           |#Hc @(proj1 … (proj1 ?? (proj2 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) Hneq1 … Hta) (refl …)))
1215           ]
1216         |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (proj2 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) Hneq1 … Hta) (refl …)))
1217         ]
1218       |#Hta cut (bit_or_null c = false)
1219         [lapply Hc; lapply Hc1; lapply Hc2 -Hc -Hc1 -Hc2
1220          cases c normalize [* normalize /2/] /2/] #Hcut %
1221         [%[cases (Htb … Hta) #_ -Htb #Htb
1222            cases (Htb … Hta) [2: % #H destruct (H) normalize in Hc; destruct] #_ -Htb #Htb
1223            cases (Htb … Hta) [2: % #H destruct (H) normalize in Hc1; destruct] #_ -Htb #Htb
1224            lapply (Htb ?) [% #H destruct (H) normalize in Hc2; destruct]
1225            * #_ #Houttape #_ @(Houttape … Hta)
1226           |>Hcut #H destruct
1227           ]
1228         |#l1 #c0 #l2 >Hcut #H destruct
1229         ]
1230       ]
1231     ]
1232   ]
1233 |#intape #outape #ta #Hta #Htb #ls #c #rs #Hintape
1234  >Hintape in Hta; whd in ⊢ (%→?); * #Hmark #Hta % [@Hmark //]
1235  whd in Htb; >Htb //
1236 ]
1237 qed. *)
1238
1239 (*
1240 definition R_comp_step_true ≝
1241   λt1,t2.
1242     ∀l0,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) l0 c rs →
1243     ∃c'. c = 〈c',true〉 ∧
1244     ((bit_or_null c' = true ∧
1245      ∀a,l1,c0,a0,l2.
1246       rs = 〈a,false〉::l1@〈c0,true〉::〈a0,false〉::l2 →
1247       (∀c.memb ? c l1 = true → is_marked ? c = false) →
1248       (c0 = c' ∧
1249        t2 = midtape ? (〈c',false〉::l0) 〈a,true〉 (l1@〈c0,false〉::〈a0,true〉::l2)) ∨
1250       (c0 ≠ c' ∧
1251        t2 = midtape (FinProd … FSUnialpha FinBool)
1252         (reverse ? l1@〈a,false〉::〈c',true〉::l0) 〈c0,false〉 (〈a0,false〉::l2))) ∨
1253      (bit_or_null c' = false ∧ t2 = midtape ? l0 〈c',false〉 rs)).
1254
1255 definition R_comp_step_false ≝
1256   λt1,t2.
1257    ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
1258    is_marked ? c = false ∧ t2 = t1.
1259
1260 lemma sem_comp_step :
1261   accRealize ? comp_step (inr … (inl … (inr … start_nop)))
1262     R_comp_step_true R_comp_step_false.
1263 #intape
1264 cases (acc_sem_if … (sem_test_char ? (is_marked ?))
1265         (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
1266           (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ??
1267             (sem_comp_step_subcase FSUnialpha 〈null,true〉 ??
1268               (sem_clear_mark …))))
1269         (sem_nop …) intape)
1270 #k * #outc * * #Hloop #H1 #H2
1271 @(ex_intro ?? k) @(ex_intro ?? outc) %
1272 [ % [@Hloop ] ] -Hloop
1273 [ #Hstate lapply (H1 Hstate) -H1 -Hstate -H2 *
1274   #ta * whd in ⊢ (%→?); #Hleft #Hright #ls #c #rs #Hintape
1275   >Hintape in Hleft; * *
1276   cases c in Hintape; #c' #b #Hintape #x * whd in ⊢ (??%?→?); #H destruct (H)
1277   whd in ⊢ (??%?→?); #Hb >Hb #Hta @(ex_intro ?? c') % //
1278   cases (Hright … Hta)
1279   [ * #Hc' #H1 % % [destruct (Hc') % ]
1280     #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
1281     cases (H1 … Hl1 Hrs)
1282     [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
1283     | * #Hneq #Houtc %2 %
1284       [ @sym_not_eq //
1285       | @Houtc ]
1286     ]
1287   | * #Hc #Helse1 cases (Helse1 … Hta)
1288     [ * #Hc' #H1 % % [destruct (Hc') % ]
1289       #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
1290       cases (H1 … Hl1 Hrs)
1291       [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
1292       | * #Hneq #Houtc %2 %
1293         [ @sym_not_eq //
1294         | @Houtc ]
1295       ]
1296     | * #Hc' #Helse2 cases (Helse2 … Hta)
1297       [ * #Hc'' #H1 % % [destruct (Hc'') % ]
1298         #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
1299         cases (H1 … Hl1 Hrs)
1300         [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
1301         | * #Hneq #Houtc %2 %
1302           [ @sym_not_eq //
1303           | @Houtc ]
1304         ]
1305       | * #Hc'' whd in ⊢ (%→?); #Helse3 %2 %
1306         [ generalize in match Hc''; generalize in match Hc'; generalize in match Hc;
1307           cases c'
1308           [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
1309               | #Hfalse @False_ind @(absurd ?? Hfalse) % ]
1310           | #_ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
1311           |*: #_ #_ #_ % ]
1312         | @(Helse3 … Hta)
1313         ]
1314       ]
1315     ]
1316   ]
1317 | #Hstate lapply (H2 Hstate) -H1 -Hstate -H2 *
1318   #ta * whd in ⊢ (%→%→?); #Hleft #Hright #ls #c #rs #Hintape
1319   >Hintape in Hleft; * #Hc #Hta % [@Hc % | >Hright //]
1320 ]
1321 qed.*)
1322
1323 definition compare ≝
1324   whileTM ? comp_step (inr … (inl … (inr … start_nop))).
1325
1326 (*
1327 definition R_compare :=
1328   λt1,t2.
1329   (t
1330
1331   ∀ls,c,b,rs.t1 = midtape ? ls 〈c,b〉 rs →
1332   (b = true → rs = ....) →
1333   (b = false ∧ ....) ∨
1334   (b = true ∧
1335
1336    rs = cs@l1@〈c0,true〉::cs0@l2
1337    (
1338
1339
1340   ls 〈c,b〉 cs l1 〈c0,b0〉 cs0 l2
1341
1342
1343 ACCETTAZIONE:
1344   ls (hd (Ls@〈grid,false〉))* (tail (Ls@〈grid,false〉)) l1 (hd (Ls@〈comma,false〉))* (tail (Ls@〈comma,false〉)) l2
1345      ^^^^^^^^^^^^^^^^^^^^^^^
1346
1347   ls Ls 〈grid,false〉 l1 Ls 〈comma,true〉 l2
1348         ^^^^^^^^^^^^
1349
1350 RIFIUTO: c ≠ d
1351
1352   ls (hd (Ls@〈c,false〉))* (tail (Ls@〈c,false〉)) l1 (hd (Ls@〈d,false〉))* (tail (Ls@〈d,false〉)) l2
1353      ^^^^^^^^^^^^^^^^^^^^^^^
1354
1355
1356   ls Ls 〈c,true〉 l1 Ls 〈d,false〉 l2
1357                        ^^^^^^^^
1358
1359   ).
1360
1361   |bs| = |b0s| →
1362   (∃la,d.〈b,true〉::bs = la@[〈grid,d〉] ∧ ∀x.memb ? x la → is_bit (\fst x) = true) →
1363   (∃lb,d0.〈b0,true〉::b0s = lb@[〈comma,d0〉] ∧ ∀x.memb ? x lb → is_bit (\fst x) = true) →
1364   t1 = midtape ? l0 〈b,true〉 (bs@l1@〈b0,true〉::b0s@l2 →
1365
1366   mk_tape left (option current) right
1367
1368   (b = grid ∧ b0 = comma ∧ bs = [] ∧ b0s = [] ∧
1369    t2 = midtape ? l0 〈grid,false〉 (l1@〈comma,true〉::l2)) ∨
1370   (b = bit x ∧ b = c ∧ bs = b0s
1371   *)
1372
1373 definition list_cases2: ∀A.∀P:list A →list A →Prop.∀l1,l2. |l1| = |l2| →
1374 P [ ] [ ] → (∀a1,a2:A.∀tl1,tl2. |tl1| = |tl2| → P (a1::tl1) (a2::tl2)) → P l1 l2.
1375 #A #P #l1 #l2 #Hlen lapply Hlen @(list_ind2 … Hlen) //
1376 #tl1 #tl2 #hd1 #hd2 #Hind normalize #HlenS #H1 #H2 @H2 //
1377 qed.
1378
1379 definition R_compare :=
1380   λt1,t2.
1381   ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
1382   (∀c'.bit_or_null c' = false → c = 〈c',true〉 → t2 = midtape ? ls 〈c',false〉 rs) ∧
1383   (∀c'. c = 〈c',false〉 → t2 = t1) ∧
1384 (* forse manca il caso no marks in rs *)
1385   ∀b,b0,bs,b0s,l1,l2.
1386   |bs| = |b0s| →
1387   (∀c.memb (FinProd … FSUnialpha FinBool) c bs = true → bit_or_null (\fst c) = true) →
1388   (∀c.memb (FinProd … FSUnialpha FinBool) c b0s = true → bit_or_null (\fst c) = true) →
1389   (∀c.memb ? c bs = true → is_marked ? c = false) →
1390   (∀c.memb ? c b0s = true → is_marked ? c = false) →
1391   (∀c.memb ? c l1 = true → is_marked ? c = false) →
1392   c = 〈b,true〉 → bit_or_null b = true →
1393   rs = bs@〈grid,false〉::l1@〈b0,true〉::b0s@〈comma,false〉::l2 →
1394   (〈b,true〉::bs = 〈b0,true〉::b0s ∧
1395    t2 = midtape ? (reverse ? bs@〈b,false〉::ls)
1396           〈grid,false〉 (l1@〈b0,false〉::b0s@〈comma,true〉::l2)) ∨
1397   (∃la,c',d',lb,lc.c' ≠ d' ∧
1398     〈b,false〉::bs = la@〈c',false〉::lb ∧
1399     〈b0,false〉::b0s = la@〈d',false〉::lc ∧
1400     t2 = midtape (FinProd … FSUnialpha FinBool) (reverse ? la@
1401                     reverse ? l1@
1402                     〈grid,false〉::
1403                     reverse ? lb@
1404                     〈c',true〉::
1405                     reverse ? la@ls)
1406                     〈d',false〉 (lc@〈comma,false〉::l2)).
1407
1408 lemma wsem_compare : WRealize ? compare R_compare.
1409 #t #i #outc #Hloop
1410 lapply (sem_while ?????? sem_comp_step t i outc Hloop) [%]
1411 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
1412 [ #tapea whd in ⊢ (%→?); #Rfalse #ls #c #rs #Htapea %
1413   [ %
1414     [ #c' #Hc' #Hc lapply (Rfalse … Htapea) -Rfalse * >Hc
1415       whd in ⊢ (??%?→?); #Hfalse destruct (Hfalse)
1416     | #c' #Hc lapply (Rfalse … Htapea) -Rfalse * #_
1417       #Htrue @Htrue ]
1418   | #b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1 #Hc
1419     cases (Rfalse … Htapea) -Rfalse >Hc whd in ⊢ (??%?→?);#Hfalse destruct (Hfalse)
1420   ]
1421 | #tapea #tapeb #tapec #Hleft #Hright #IH #Htapec lapply (IH Htapec) -Htapec -IH #IH
1422   whd in Hleft; #ls #c #rs #Htapea cases Hleft -Hleft
1423   #ls0 * #c' * #rs0 * >Htapea #Hdes destruct (Hdes) * *
1424   cases (true_or_false (bit_or_null c')) #Hc'
1425   [2: #Htapeb lapply (Htapeb Hc') -Htapeb #Htapeb #_ #_ %
1426     [%[#c1 #Hc1 #Heqc destruct (Heqc)
1427        cases (IH … Htapeb) * #_ #H #_ <Htapeb @(H … (refl…))
1428       |#c1 #Heqc destruct (Heqc)
1429       ]
1430     |#b #b0 #bs #b0s #l1 #l2 #_ #_ #_ #_ #_ #_
1431      #Heq destruct (Heq) >Hc' #Hfalse @False_ind destruct (Hfalse)
1432     ]
1433   |#_ (* no marks in rs ??? *) #_ #Hleft %
1434     [ %
1435       [ #c'' #Hc'' #Heq destruct (Heq) >Hc'' in Hc'; #H destruct (H)
1436       | #c0 #Hfalse destruct (Hfalse)
1437       ]
1438     |#b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1
1439      #Heq destruct (Heq) #_ >append_cons; <associative_append #Hrs
1440      cases (Hleft …  Hc' … Hrs) -Hleft
1441       [2: #c1 #memc1 cases (memb_append … memc1) -memc1 #memc1
1442         [cases (memb_append … memc1) -memc1 #memc1
1443           [@Hbs2 @memc1 |>(memb_single … memc1) %]
1444         |@Hl1 @memc1
1445         ]
1446       |* (* manca il caso in cui dopo una parte uguale il
1447             secondo nastro finisca ... ???? *)
1448        #_ cases (true_or_false (b==b0)) #eqbb0
1449         [2: #_ #Htapeb %2 lapply (Htapeb … (\Pf eqbb0)) -Htapeb #Htapeb
1450          cases (IH … Htapeb) * #_ #Hout #_
1451          @(ex_intro … []) @(ex_intro … b) @(ex_intro … b0)
1452          @(ex_intro … bs) @(ex_intro … b0s) %
1453           [%[%[@(\Pf eqbb0) | %] | %]
1454           |>(Hout … (refl …)) -Hout >Htapeb @eq_f3 [2,3:%]
1455            >reverse_append >reverse_append >associative_append
1456            >associative_append %
1457           ]
1458         |lapply Hbs1 lapply Hbs2 lapply Hrs -Hbs1 -Hbs2 -Hrs
1459          @(list_cases2 … Hlen)
1460           [#Hrs #_ #_ >associative_append >associative_append #Htapeb #_
1461            lapply (Htapeb … (\P eqbb0) … (refl …) (refl …)) -Htapeb #Htapeb
1462            cases (IH … Htapeb) -IH * #Hout #_ #_ %1 %
1463             [>(\P eqbb0) %
1464             |>(Hout grid (refl …) (refl …)) @eq_f
1465              normalize >associative_append %
1466             ]
1467           |* #a1 #ba1 * #a2 #ba2 #tl1 #tl2 #HlenS #Hrs #Hbs1 #Hbs2
1468            cut (ba1 = false) [@(Hbs1 〈a1,ba1〉) @memb_hd] #Hba1 >Hba1
1469            >associative_append >associative_append #Htapeb #_
1470            lapply (Htapeb … (\P eqbb0) … (refl …) (refl …)) -Htapeb #Htapeb
1471            cases (IH … Htapeb) -IH * #_ #_
1472            #IH cases(IH a1 a2 ?? (l1@[〈b0,false〉]) l2 HlenS ????? (refl …) ??)
1473             [
1474
1475
1476 (*
1477          cut (∃a,l1'.〈a,false〉::l1'=((bs@[〈grid,false〉])@l1)@[〈b0,false〉])
1478           [generalize in match Hbs2; cases bs
1479             [#_ @(ex_intro … grid) @(ex_intro … (l1@[〈b0,false〉]))
1480              >associative_append %
1481             |* #bsc #bsb #bstl #Hbs2 @(ex_intro … bsc)
1482              @(ex_intro … (((bstl@[〈grid,false〉])@l1)@[〈b0,false〉]))
1483              normalize @eq_f2 [2:%] @eq_f @sym_eq @(Hbs2 〈bsc,bsb〉) @memb_hd
1484             ]
1485           ]
1486          * #a * #l1' #H2
1487          cut (∃a0,b1,l2'.b0s@〈comma,false〉::l2=〈a0,b1〉::l2')
1488           [cases b0s
1489             [@(ex_intro … comma) @(ex_intro … false) @(ex_intro … l2) %
1490             |* #bsc #bsb #bstl @(ex_intro … bsc) @(ex_intro … bsb)
1491              @(ex_intro … (bstl@〈comma,false〉::l2)) %
1492             ]
1493           ] *)
1494          * #a0 * #b1 * #l2' #H3
1495          lapply (Htapeb … (\P eqbb0) a a0 b1 l1' l2' H2 H3) -Htapeb #Htapeb
1496          cases (IH … Htapeb) -IH *
1497
1498
1499       [2: * >Hc' #Hfalse @False_ind destruct ] * #_
1500        @(list_cases2 … Hlen)
1501        [ #Hbs #Hb0s generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
1502        -Hrs #Hrs normalize in Hrs; #Hleft cases (Hleft ????? Hrs ?) -Hleft
1503          [ * #Heqb #Htapeb cases (IH … Htapeb) -IH * #IH #_ #_
1504           % %
1505             [ >Heqb >Hbs >Hb0s %
1506             | >Hbs >Hb0s @IH %
1507             ]
1508          |* #Hneqb #Htapeb %2
1509           @(ex_intro … [ ]) @(ex_intro … b)
1510           @(ex_intro … b0) @(ex_intro … [ ])
1511           @(ex_intro … [ ]) %
1512             [ % [ % [@sym_not_eq //| >Hbs %] | >Hb0s %]
1513             | cases (IH … Htapeb) -IH * #_ #IH #_ >(IH ? (refl ??))
1514               @Htapeb
1515             ]
1516          | @Hl1 ]
1517       | * #b' #bitb' * #b0' #bitb0' #bs' #b0s' #Hbs #Hb0s
1518         generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
1519         cut (bit_or_null b' = true ∧ bit_or_null b0' = true ∧
1520              bitb' = false ∧ bitb0' = false)
1521         [ % [ % [ % [ >Hbs in Hbs1; #Hbs1 @(Hbs1 〈b',bitb'〉) @memb_hd
1522             | >Hb0s in Hb0s1; #Hb0s1 @(Hb0s1 〈b0',bitb0'〉) @memb_hd ]
1523             | >Hbs in Hbs2; #Hbs2 @(Hbs2 〈b',bitb'〉) @memb_hd ]
1524             | >Hb0s in Hb0s2; #Hb0s2 @(Hb0s2 〈b0',bitb0'〉) @memb_hd ]
1525         | * * * #Ha #Hb #Hc #Hd >Hc >Hd
1526           #Hrs #Hleft
1527           cases (Hleft b' (bs'@〈grid,false〉::l1) b0 b0'
1528                          (b0s'@〈comma,false〉::l2) ??) -Hleft
1529           [ 3: >Hrs normalize @eq_f >associative_append %
1530           | * #Hb0 #Htapeb cases (IH …Htapeb) -IH * #_ #_ #IH
1531             cases (IH b' b0' bs' b0s' (l1@[〈b0,false〉]) l2 ??????? Ha ?) -IH
1532             [ * #Heq #Houtc % %
1533               [ >Hb0 @eq_f >Hbs in Heq; >Hb0s in ⊢ (%→?); #Heq
1534                 destruct (Heq) >Hb0s >Hc >Hd %
1535               | >Houtc >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append
1536                 >associative_append %
1537               ]
1538             | * #la * #c' * #d' * #lb * #lc * * * #H1 #H2 #H3 #H4 %2
1539               @(ex_intro … (〈b,false〉::la)) @(ex_intro … c') @(ex_intro … d')
1540               @(ex_intro … lb) @(ex_intro … lc)
1541               % [ % [ % // >Hbs >Hc >H2 % | >Hb0s >Hd >H3 >Hb0 % ]
1542                 | >H4 >Hbs >Hb0s >Hc >Hd >Hb0 >reverse_append
1543                   >reverse_cons >reverse_cons
1544                   >associative_append >associative_append
1545                   >associative_append >associative_append %
1546                 ]
1547             | generalize in match Hlen; >Hbs >Hb0s
1548               normalize #Hlen destruct (Hlen) @e0
1549             | #c0 #Hc0 @Hbs1 >Hbs @memb_cons //
1550             | #c0 #Hc0 @Hb0s1 >Hb0s @memb_cons //
1551             | #c0 #Hc0 @Hbs2 >Hbs @memb_cons //
1552             | #c0 #Hc0 @Hb0s2 >Hb0s @memb_cons //
1553             | #c0 #Hc0 cases (memb_append … Hc0)
1554               [ @Hl1 | #Hc0' >(memb_single … Hc0') % ]
1555             | %
1556             | >associative_append >associative_append % ]
1557          | * #Hneq #Htapeb %2
1558             @(ex_intro … []) @(ex_intro … b) @(ex_intro … b0)
1559             @(ex_intro … bs) @(ex_intro … b0s) %
1560            [ % // % // @sym_not_eq //
1561            | >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append
1562              >reverse_append in Htapeb; >reverse_cons
1563              >associative_append >associative_append
1564              #Htapeb <Htapeb
1565              cases (IH … Htapeb) -Htapeb -IH * #_ #IH #_ @(IH ? (refl ??))
1566            ]
1567          | #c1 #Hc1 cases (memb_append … Hc1) #Hyp
1568            [ @Hbs2 >Hbs @memb_cons @Hyp
1569            | cases (orb_true_l … Hyp)
1570              [ #Hyp2 >(\P Hyp2) %
1571              | @Hl1
1572              ]
1573            ]
1574          ]
1575 ]]]]]
1576 qed.
1577
1578 axiom sem_compare : Realize ? compare R_compare.