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.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_____________________________________________________________*)
13 (* MOVE_CHAR RIGHT MACHINE
15 Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra.
18 (ls,cs,rs can be empty; # is a parameter)
30 include "turing/basic_machines.ma".
31 include "turing/if_machine.ma".
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.
37 definition Rmcr_step_true ≝
41 t1 = midtape alpha (a::ls) b rs ∧
42 t2 = mk_tape alpha (a::b::ls) (option_hd ? rs) (tail ? rs)) ∨
44 t1 = midtape alpha [ ] b rs ∧
45 t2 = leftof alpha b rs)).
47 definition Rmcr_step_false ≝
49 left ? t1 ≠ [] → current alpha t1 ≠ None alpha →
50 current alpha t1 = Some alpha sep ∧ t2 = t1.
55 [inr … (inl … (inr … start_nop)): Rmcr_step_true alpha sep, Rmcr_step_false alpha sep].
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 //
69 @(ex_intro … a) @(ex_intro … ls1) @(ex_intro … rs) % //
70 @(proj2 … Hmove) @(proj2 … Hswap) >Htapea //
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) //
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))).
85 definition R_move_char_r ≝
87 ∀b,a,ls,rs. t1 = midtape alpha (a::ls) b rs →
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).
93 lemma sem_move_char_r :
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 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
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) ]
108 | #tapea #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 %
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)
120 [% #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct
121 |whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse
122 [ destruct | @Hfalse ]]
124 #Hr0 -Hrs0 #Hrs0 >Hrs in Htapeb;
125 normalize in ⊢ (%→?); #Htapeb
126 cases (IH … Htapeb) -IH #_ #IH
127 >reverse_cons >associative_append @IH //
130 |* #rs1 * >Htapea #H destruct (H)
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 ]
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 ]
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 ]
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 //
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 //
166 lemma ssem_move_char_r :
168 Realize alpha (move_char_r alpha sep) (R_move_char_r alpha sep).
172 (******************************* move_char_l **********************************)
173 (* MOVE_CHAR (left) MACHINE
175 Sposta il carattere binario su cui si trova la testina appena prima del primo #
179 (ls,cs,rs can be empty; # is a parameter)
186 Initial state = 〈0,#〉
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.
195 definition Rmcl_step_true ≝
199 t1 = midtape alpha ls b (a::rs) ∧
200 t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a::b::rs)) ∨
202 t1 = midtape alpha ls b [ ] ∧
203 t2 = rightof alpha b ls)).
205 definition Rmcl_step_false ≝
207 right ? t1 ≠ [] → current alpha t1 ≠ None alpha →
208 current alpha t1 = Some alpha sep ∧ t2 = t1.
210 definition mcls_acc: ∀alpha:FinSet.∀sep:alpha.states ? (mcl_step alpha sep)
211 ≝ λalpha,sep.inr … (inl … (inr … start_nop)).
216 [mcls_acc ??: Rmcl_step_true alpha sep, Rmcl_step_false alpha sep].
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 //
230 @(ex_intro … a) @(ex_intro … ls) @(ex_intro … rs1) % //
231 @(proj2 … Hmove) @(proj2 … Hswap) >Htapea //
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) //
242 definition move_char_l ≝
243 λalpha,sep.whileTM alpha (mcl_step alpha sep) (inr … (inl … (inr … start_nop))).
245 definition R_move_char_l ≝
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)).
253 lemma sem_move_char_l :
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 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
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) ]
268 | #tapea #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 %
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)
280 [% #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct
281 |whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse
282 [ destruct | @Hfalse ]]
284 #Hr0 -Hrs0 #Hrs0 >Hrs in Htapeb;
285 normalize in ⊢ (%→?); #Htapeb
286 cases (IH … Htapeb) -IH #_ #IH
287 >reverse_cons >associative_append @IH //
290 |* #rs1 * >Htapea #H destruct (H)
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 ]
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 ]
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 ]
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 //
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 //
326 lemma ssem_move_char_l:
328 Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).