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