matita/matita/lib/turing/move_char.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 (* MOVE_CHAR RIGHT MACHINE
  14
  15 Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra.
  16
  17 Input:
  18 (ls,cs,rs can be empty; # is a parameter)
  19
  20   ls x cs # rs
  21        ^
  22 Output:
  23   ls cs x # rs
  24         ^
  25 Initial state = 〈0,#〉
  26 Final state = 〈4,#〉
  27
  28 *)
  29
  30 include "turing/basic_machines.ma".
  31 include "turing/if_machine.ma".
  32
  33 definition mcc_step ≝ λalpha:FinSet.λsep:alpha.
  34   ifTM alpha (test_char ? (λc.¬c==sep))
  35      (single_finalTM … (seq … (swap_r alpha sep) (move_r ?))) (nop ?) tc_true.
  36
  37 definition Rmcc_step_true ≝
  38   λalpha,sep,t1,t2.
  39    ∀a,b,ls,rs.
  40     t1 = midtape alpha (a::ls) b rs →
  41     b ≠ sep ∧
  42     t2 = mk_tape alpha (a::b::ls) (option_hd ? rs) (tail ? rs).
  43
  44 definition Rmcc_step_false ≝
  45   λalpha,sep,t1,t2.
  46     left ? t1 ≠ [] →  current alpha t1 ≠ None alpha →
  47       current alpha t1 = Some alpha sep ∧ t2 = t1.
  48
  49 lemma sem_mcc_step :
  50   ∀alpha,sep.
  51   mcc_step alpha sep ⊨
  52     [inr … (inl … (inr … start_nop)): Rmcc_step_true alpha sep, Rmcc_step_false alpha sep].
  53 #alpha #sep
  54   @(acc_sem_if_app …
  55      (sem_test_char …) (sem_seq …(sem_swap_r …) (sem_move_r …)) (sem_nop …))
  56   [#intape #outtape #tapea whd in ⊢ (%→%→%);
  57    #Htapea * #tapeb * whd in ⊢ (%→%→?);
  58    #Htapeb #Houttape #a #b #ls #rs #Hintape
  59    >Hintape in Htapea; #Htapea cases (Htapea ? (refl …)) -Htapea
  60    #Hbsep #Htapea % [@(\Pf (injective_notb ? false Hbsep))]
  61    @Houttape @Htapeb //
  62   |#intape #outtape #tapea whd in ⊢ (%→%→%);
  63    cases (current alpha intape)
  64     [#_ #_ #_ * #Hfalse @False_ind @Hfalse %
  65     |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % //
  66      lapply (injective_notb ? true csep) -csep #csep >(\P csep) //
  67     ]
  68   ]
  69 qed.
  70
  71 (* the move_char (variant c) machine *)
  72 definition move_char_r ≝
  73   λalpha,sep.whileTM alpha (mcc_step alpha sep) (inr … (inl … (inr … start_nop))).
  74
  75 definition R_move_char_r ≝
  76   λalpha,sep,t1,t2.
  77     ∀b,a,ls,rs. t1 = midtape alpha (a::ls) b rs →
  78     (b = sep → t2 = t1) ∧
  79     (∀rs1,rs2.rs = rs1@sep::rs2 →
  80      b ≠ sep → memb ? sep rs1 = false →
  81      t2 = midtape alpha (a::reverse ? rs1@b::ls) sep rs2).
  82
  83 lemma sem_move_char_r :
  84   ∀alpha,sep.
  85   WRealize alpha (move_char_r alpha sep) (R_move_char_r alpha sep).
  86 #alpha #sep #inc #i #outc #Hloop
  87 lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%]
  88 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
  89 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
  90   %
  91   [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??)
  92     [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2)]
  93   | #rs1 #rs2 #Hrs #Hb #Hrs1
  94     >Htapea in H1; #H1 cases (H1 ??)
  95     [#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct %
  96     |*:% #H2 normalize in H2; destruct (H2) ]
  97   ]
  98 | #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
  99   lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH
 100   #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea)
 101   #Ha0 #Htapeb %
 102   [ #Hfalse @False_ind @(absurd ?? Ha0) //
 103   | *
 104     [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ (* normalize *)
 105       >Hrs in Htapeb; #Htapeb normalize in Htapeb;
 106       cases (IH … Htapeb) #Houtc #_ >Houtc normalize //
 107     | #r0 #rs0 #rs2 #Hrs #_ #Hrs0
 108       cut (r0 ≠ sep ∧ memb … sep rs0 = false)
 109       [ %
 110          [ % #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct
 111          | whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse
 112            [ destruct
 113            | @Hfalse ]
 114          ]
 115       ] *
 116       #Hr0 -Hrs0 #Hrs0 >Hrs in Htapeb;
 117       normalize in ⊢ (%→?); #Htapeb
 118       cases (IH … Htapeb) -IH #_ #IH
 119       >reverse_cons >associative_append @IH //
 120     ]
 121   ]
 122 qed.
 123
 124 lemma terminate_move_char_r :
 125   ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha (a::ls) b rs →
 126   (b = sep ∨ memb ? sep rs = true) → Terminate alpha (move_char_r alpha sep) t.
 127 #alpha #sep #t #b #a #ls #rs #Ht #Hsep
 128 @(terminate_while … (sem_mcc_step alpha sep))
 129   [%
 130   |generalize in match Hsep; -Hsep
 131    generalize in match Ht; -Ht
 132    generalize in match ls; -ls
 133    generalize in match a; -a
 134    generalize in match b; -b
 135    generalize in match t; -t
 136    elim rs
 137     [#t #b #a #ls #Ht #Hsep % #tinit
 138      whd in ⊢ (%→?); #H @False_ind
 139      cases (H … Ht) #Hb #_ cases Hb #eqb @eqb
 140      cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
 141     |#r0 #rs0 #Hind #t #b #a #ls #Ht #Hsep % #tinit
 142      whd in ⊢ (%→?); #H
 143      cases (H … Ht) #Hbsep #Htinit
 144      @(Hind … Htinit) cases Hsep
 145       [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
 146         [#eqsep %1 >(\P eqsep) // | #H %2 //]
 147   ]
 148 qed.
 149
 150 (* NO GOOD: we must stop if current = None too!!! *)
 151
 152 axiom ssem_move_char_r :
 153   ∀alpha,sep.
 154   Realize alpha (move_char_r alpha sep) (R_move_char_r alpha sep).
 155
 156
 157 (******************************* move_char_l **********************************)
 158 (* MOVE_CHAR (left) MACHINE
 159
 160 Sposta il carattere binario su cui si trova la testina appena prima del primo #
 161 alla sua sinistra.
 162
 163 Input:
 164 (ls,cs,rs can be empty; # is a parameter)
 165
 166   ls # cs x rs
 167         ^
 168 Output:
 169   ls # x cs rs
 170        ^
 171 Initial state = 〈0,#〉
 172 Final state = 〈4,#〉
 173
 174 *)
 175
 176 include "turing/basic_machines.ma".
 177 include "turing/if_machine.ma".
 178
 179 definition mcl_step ≝ λalpha:FinSet.λsep:alpha.
 180   ifTM alpha (test_char ? (λc.¬c==sep))
 181      (single_finalTM … (seq … (swap alpha sep) (move_l ?))) (nop ?) tc_true.
 182
 183 definition Rmcl_step_true ≝
 184   λalpha,sep,t1,t2.
 185    ∀a,b,ls,rs.
 186     t1 = midtape alpha ls b (a::rs) →
 187     b ≠ sep ∧
 188     t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a::b::rs).
 189
 190 definition Rmcl_step_false ≝
 191   λalpha,sep,t1,t2.
 192     right ? t1 ≠ [] →  current alpha t1 ≠ None alpha →
 193       current alpha t1 = Some alpha sep ∧ t2 = t1.
 194
 195 definition mcls_acc: ∀alpha:FinSet.∀sep:alpha.states ? (mcl_step alpha sep)
 196  ≝ λalpha,sep.inr … (inl … (inr … start_nop)).
 197
 198 lemma sem_mcl_step :
 199   ∀alpha,sep.
 200   mcl_step alpha sep ⊨
 201     [mcls_acc alpha sep: Rmcl_step_true alpha sep, Rmcl_step_false alpha sep].
 202 #alpha #sep
 203 @(acc_sem_if_app …
 204   (sem_test_char …) (sem_seq …(sem_swap …) (sem_move_l …)) (sem_nop …))
 205   [#intape #outtape #tapea whd in ⊢ (%→%→%);
 206    #Htapea * #tapeb * whd in ⊢ (%→%→?);
 207    #Htapeb #Houttape #a #b #ls #rs #Hintape
 208    >Hintape in Htapea; #Htapea cases (Htapea ? (refl …)) -Htapea
 209    #Hbsep #Htapea % [@(\Pf (injective_notb ? false Hbsep))]
 210    @Houttape @Htapeb //
 211   |#intape #outtape #tapea whd in ⊢ (%→%→%);
 212    cases (current alpha intape)
 213     [#_ #_ #_ * #Hfalse @False_ind @Hfalse %
 214     |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % //
 215      lapply (injective_notb ? true csep) -csep #csep >(\P csep) //
 216     ]
 217   ]
 218 qed.
 219
 220 (* the move_char (variant left) machine *)
 221 definition move_char_l ≝
 222   λalpha,sep.whileTM alpha (mcl_step alpha sep) (inr … (inl … (inr … start_nop))).
 223
 224 definition R_move_char_l ≝
 225   λalpha,sep,t1,t2.
 226     ∀b,a,ls,rs. t1 = midtape alpha ls b (a::rs) →
 227     (b = sep → t2 = t1) ∧
 228     (∀ls1,ls2.ls = ls1@sep::ls2 →
 229      b ≠ sep → memb ? sep ls1 = false →
 230      t2 = midtape alpha ls2 sep (a::reverse ? ls1@b::rs)).
 231
 232 lemma sem_move_char_l :
 233   ∀alpha,sep.
 234   WRealize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).
 235 #alpha #sep #inc #i #outc #Hloop
 236 lapply (sem_while … (sem_mcl_step alpha sep) inc i outc Hloop) [%]
 237 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 238 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
 239   %
 240   [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??)
 241    [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2) ]
 242   | #rs1 #rs2 #Hrs #Hb #Hrs1
 243     >Htapea in H1; (* normalize in ⊢ (% → ?); *) #H1 cases (H1 ??)
 244     [ #Hfalse normalize in Hfalse; @False_ind @(absurd ?? Hb) destruct %
 245     |*:% normalize #H2 destruct (H2) ]
 246   ]
 247 | #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
 248   lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH
 249   #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea)
 250   #Ha0 #Htapeb %
 251   [ #Hfalse @False_ind @(absurd ?? Ha0) //
 252   | *
 253     [ #ls2 whd in ⊢ (???%→?); #Hls #_ #_
 254       >Hls in Htapeb; #Htapeb normalize in Htapeb;
 255       cases (IH … Htapeb) #Houtc #_ >Houtc normalize //
 256     | #l0 #ls0 #ls2 #Hls #_ #Hls0
 257       cut (l0 ≠ sep ∧ memb … sep ls0 = false)
 258       [ %
 259          [ % #Hl0 >Hl0 in Hls0; >memb_hd #Hfalse destruct
 260          | whd in Hls0:(??%?); cases (sep==l0) in Hls0; normalize #Hfalse
 261            [ destruct
 262            | @Hfalse ]
 263          ]
 264       ] *
 265       #Hl0 -Hls0 #Hls0 >Hls in Htapeb;
 266       normalize in ⊢ (%→?); #Htapeb
 267       cases (IH … Htapeb) -IH #_ #IH
 268       >reverse_cons >associative_append @IH //
 269     ]
 270   ]
 271 qed.
 272
 273 lemma terminate_move_char_l :
 274   ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha ls b (a::rs) →
 275   (b = sep ∨ memb ? sep ls = true) → Terminate alpha (move_char_l alpha sep) t.
 276 #alpha #sep #t #b #a #ls #rs #Ht #Hsep
 277 @(terminate_while … (sem_mcl_step alpha sep))
 278   [%
 279   |generalize in match Hsep; -Hsep
 280    generalize in match Ht; -Ht
 281    generalize in match rs; -rs
 282    generalize in match a; -a
 283    generalize in match b; -b
 284    generalize in match t; -t
 285    elim ls
 286     [#t #b #a #rs #Ht #Hsep % #tinit
 287      whd in ⊢ (%→?); #H @False_ind
 288      cases (H … Ht) #Hb #_ cases Hb #eqb @eqb
 289      cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
 290     |#l0 #ls0 #Hind #t #b #a #rs #Ht #Hsep % #tinit
 291      whd in ⊢ (%→?); #H
 292      cases (H … Ht) #Hbsep #Htinit
 293      @(Hind … Htinit) cases Hsep
 294       [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
 295         [#eqsep %1 >(\P eqsep) // | #H %2 //]
 296   ]
 297 qed.
 298
 299 (* NO GOOD: we must stop if current = None too!!!
 300 lemma ssem_move_char_l :
 301   ∀alpha,sep.
 302   Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).
 303 #alpha #sep *
 304 [ %{5} % [| % [whd in ⊢ (??%?);
 305  @WRealize_to_Realize // @terminate_move_char_l
 306 *)
 307
 308 axiom ssem_move_char_l :
 309   ∀alpha,sep.
 310   Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).