matita/matita/lib/turing/universal/compare.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_____________________________________________________________*)
  11
  12
  13 (* COMPARE BIT
  14
  15 *)
  16
  17 include "turing/while_machine.ma".
  18
  19 (* ADVANCE TO MARK (right)
  20
  21    sposta la testina a destra fino a raggiungere il primo carattere marcato
  22
  23 *)
  24
  25 (* 0, a ≠ mark _ ⇒ 0, R
  26 0, a = mark _ ⇒ 1, N *)
  27
  28 definition atm_states ≝ initN 3.
  29
  30 definition atmr_step ≝
  31   λalpha:FinSet.λtest:alpha→bool.
  32   mk_TM alpha atm_states
  33   (λp.let 〈q,a〉 ≝ p in
  34    match a with
  35    [ None ⇒ 〈1, None ?〉
  36    | Some a' ⇒
  37      match test a' with
  38      [ true ⇒ 〈1,None ?〉
  39      | false ⇒ 〈2,Some ? 〈a',R〉〉 ]])
  40   O (λx.notb (x == 0)).
  41
  42 definition Ratmr_step_true ≝
  43   λalpha,test,t1,t2.
  44    ∃ls,a,rs.
  45    t1 = midtape alpha ls a rs ∧ test a = false ∧
  46    t2 = mk_tape alpha (a::ls) (option_hd ? rs) (tail ? rs).
  47
  48 definition Ratmr_step_false ≝
  49   λalpha,test,t1,t2.
  50     t1 = t2 ∧
  51     (current alpha t1 = None ? ∨
  52      (∃a.current ? t1 = Some ? a ∧ test a = true)).
  53
  54 lemma atmr_q0_q1 :
  55   ∀alpha,test,ls,a0,rs. test a0 = true →
  56   step alpha (atmr_step alpha test)
  57     (mk_config ?? 0 (midtape … ls a0 rs)) =
  58   mk_config alpha (states ? (atmr_step alpha test)) 1
  59     (midtape … ls a0 rs).
  60 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
  61 qed.
  62
  63 lemma atmr_q0_q2 :
  64   ∀alpha,test,ls,a0,rs. test a0 = false →
  65   step alpha (atmr_step alpha test)
  66     (mk_config ?? 0 (midtape … ls a0 rs)) =
  67   mk_config alpha (states ? (atmr_step alpha test)) 2
  68     (mk_tape … (a0::ls) (option_hd ? rs) (tail ? rs)).
  69 #alpha #test #ls #a0 #ts #Htest normalize >Htest cases ts //
  70 qed.
  71
  72 lemma sem_atmr_step :
  73   ∀alpha,test.
  74   accRealize alpha (atmr_step alpha test)
  75     2 (Ratmr_step_true alpha test) (Ratmr_step_false alpha test).
  76 #alpha #test *
  77 [ @(ex_intro ?? 2)
  78   @(ex_intro ?? (mk_config ?? 1 (niltape ?))) %
  79   [ % // #Hfalse destruct | #_ % // % % ]
  80 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (leftof ? a al)))
  81   % [ % // #Hfalse destruct | #_ % // % % ]
  82 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (rightof ? a al)))
  83   % [ % // #Hfalse destruct | #_ % // % % ]
  84 | #ls #c #rs @(ex_intro ?? 2)
  85   cases (true_or_false (test c)) #Htest
  86   [ @(ex_intro ?? (mk_config ?? 1 ?))
  87     [| %
  88       [ %
  89         [ whd in ⊢ (??%?); >atmr_q0_q1 //
  90         | #Hfalse destruct ]
  91       | #_ % // %2 @(ex_intro ?? c) % // ]
  92     ]
  93   | @(ex_intro ?? (mk_config ?? 2 (mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs))))
  94     %
  95     [ %
  96       [ whd in ⊢ (??%?); >atmr_q0_q2 //
  97       | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
  98         % // % //
  99       ]
 100     | #Hfalse @False_ind @(absurd ?? Hfalse) %
 101     ]
 102   ]
 103 ]
 104 qed.
 105
 106 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
 107   ∀ls,c,rs.
 108   (t1 = midtape alpha ls c rs  →
 109   ((test c = true ∧ t2 = t1) ∨
 110    (test c = false ∧
 111     ∀rs1,b,rs2. rs = rs1@b::rs2 →
 112      test b = true → (∀x.memb ? x rs1 = true → test x = false) →
 113      t2 = midtape ? (reverse ? rs1@c::ls) b rs2))).
 114
 115 definition adv_to_mark_r ≝
 116   λalpha,test.whileTM alpha (atmr_step alpha test) 2.
 117
 118 lemma sem_adv_to_mark_r :
 119   ∀alpha,test.
 120   WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
 121 #alpha #test #t #i #outc #Hloop
 122 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
 123 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 124 [ #tapea * #Htapea *
 125   [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
 126     #Hfalse destruct (Hfalse)
 127   | * #a * #Ha #Htest #ls #c #rs #H2 %
 128     >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
 129     <Htapea //
 130   ]
 131 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
 132   lapply (IH HRfalse) -IH #IH
 133   #ls #c #rs #Htapea %2
 134   cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
 135
 136   >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
 137   [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
 138     cases (IH … Htapeb)
 139     [ * #_ #Houtc >Houtc >Htapeb %
 140     | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
 141   | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
 142     cases (IH … Htapeb)
 143     [ * #Hfalse >(Hmemb …) in Hfalse;
 144       [ #Hft destruct (Hft)
 145       | @memb_hd ]
 146     | * #Htestr1 #H1 >reverse_cons >associative_append
 147       @H1 // #x #Hx @Hmemb @memb_cons //
 148     ]
 149   ]
 150 qed.
 151
 152 lemma terminate_adv_to_mark_r :
 153   ∀alpha,test.
 154   ∀t. (* ∀b,a,ls,rs. t = midtape alpha (a::ls) b rs →
 155     (b = sep ∨ memb ? sep rs = true) →  *)
 156   Terminate alpha (adv_to_mark_r alpha test) t.
 157 #alpha #test #t
 158 @(terminate_while … (sem_atmr_step alpha test))
 159   [ %
 160   | % #t1 whd in ⊢ (% → ?); * #ls * #c * #rs
 161     * * generalize in match c; generalize in match ls;
 162     -ls -c elim rs
 163     [ #ls #c #Ht #Hc #Ht1
 164       % >Ht1 #t2 * #ls0 * #c0 * #rs0 * *
 165       normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
 166
 167
 168      #Ht #Hc #t1
 169     elim t
 170     [ % #a whd in ⊢ (% → ?);
 171
 172  #sep #t #b #a #ls #rs #Ht #Hsep
 173 @(terminate_while … (sem_mcc_step alpha sep))
 174   [%
 175   |generalize in match Hsep; -Hsep
 176    generalize in match Ht; -Ht
 177    generalize in match ls; -ls
 178    generalize in match a; -a
 179    generalize in match b; -b
 180    generalize in match t; -t
 181    elim rs
 182     [#t #b #a #ls #Ht #Hsep % #tinit
 183      whd in ⊢ (%→?); #H @False_ind
 184      cases (H … Ht) #Hb #_ cases Hb #eqb @eqb
 185      cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
 186     |#r0 #rs0 #Hind #t #b #a #ls #Ht #Hsep % #tinit
 187      whd in ⊢ (%→?); #H
 188      cases (H … Ht) #Hbsep #Htinit
 189      @(Hind … Htinit) cases Hsep
 190       [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
 191         [#eqsep %1 >(\P eqsep) // | #H %2 //]
 192   ]
 193 qed.