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 (variant c) 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)
34 include "turing/while_machine.ma".
36 definition mcc_states : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 5) alpha.
38 definition mcc0 : initN 5 ≝ mk_Sig ?? 0 (leb_true_to_le 1 5 (refl …)).
39 definition mcc1 : initN 5 ≝ mk_Sig ?? 1 (leb_true_to_le 2 5 (refl …)).
40 definition mcc2 : initN 5 ≝ mk_Sig ?? 2 (leb_true_to_le 3 5 (refl …)).
41 definition mcc3 : initN 5 ≝ mk_Sig ?? 3 (leb_true_to_le 4 5 (refl …)).
42 definition mcc4 : initN 5 ≝ mk_Sig ?? 4 (leb_true_to_le 5 5 (refl …)).
45 λalpha:FinSet.λsep:alpha.
46 mk_TM alpha (mcc_states alpha)
49 let q' ≝ pi1 nat (λi.i<5) q' in (* perche' devo passare il predicato ??? *)
51 [ None ⇒ 〈〈mcc4,sep〉,None ?〉
56 [ true ⇒ 〈〈mcc4,sep〉,None ?〉
57 | false ⇒ 〈〈mcc1,a'〉,Some ? 〈a',L〉〉 ]
58 | S q' ⇒ match q' with
60 〈〈mcc2,a'〉,Some ? 〈b,R〉〉
61 | S q' ⇒ match q' with
63 〈〈mcc3,sep〉,Some ? 〈b,R〉〉
64 | S q' ⇒ match q' with
68 〈〈mcc4,sep〉,None ?〉 ] ] ] ] ])
70 (λq.let 〈q',a〉 ≝ q in q' == mcc3 ∨ q' == mcc4).
73 ∀alpha:FinSet.∀sep,a,ls,a0,rs.
75 step alpha (mcc_step alpha sep)
76 (mk_config ?? 〈mcc0,a〉 (mk_tape … ls (Some ? a0) rs)) =
77 mk_config alpha (states ? (mcc_step alpha sep)) 〈mcc1,a0〉
78 (tape_move_left alpha ls a0 rs).
80 [ #a0 #rs #Ha0 whd in ⊢ (??%?);
81 normalize in match (trans ???); >Ha0 %
82 | #a1 #ls #a0 #rs #Ha0 whd in ⊢ (??%?);
83 normalize in match (trans ???); >Ha0 %
88 ∀alpha:FinSet.∀sep,a,ls,a0,rs.
89 step alpha (mcc_step alpha sep)
90 (mk_config ?? 〈mcc1,a〉 (mk_tape … ls (Some ? a0) rs)) =
91 mk_config alpha (states ? (mcc_step alpha sep)) 〈mcc2,a0〉
92 (tape_move_right alpha ls a rs).
93 #alpha #sep #a #ls #a0 * //
97 ∀alpha:FinSet.∀sep,a,ls,a0,rs.
98 step alpha (mcc_step alpha sep)
99 (mk_config ?? 〈mcc2,a〉 (mk_tape … ls (Some ? a0) rs)) =
100 mk_config alpha (states ? (mcc_step alpha sep)) 〈mcc3,sep〉
101 (tape_move_right alpha ls a rs).
102 #alpha #sep #a #ls #a0 * //
105 definition Rmcc_step_true ≝
108 t1 = midtape alpha (a::ls) b rs →
110 t2 = mk_tape alpha (a::b::ls) (option_hd ? rs) (tail ? rs).
112 definition Rmcc_step_false ≝
114 left ? t1 ≠ [] → current alpha t1 ≠ None alpha →
115 current alpha t1 = Some alpha sep ∧ t2 = t1.
117 lemma mcc_trans_init_sep:
119 trans ? (mcc_step alpha sep) 〈〈mcc0,x〉,Some ? sep〉 = 〈〈mcc4,sep〉,None ?〉.
120 #alpha #sep #x normalize >(\b ?) //
123 lemma mcc_trans_init_not_sep:
124 ∀alpha,sep,x,y.y == sep = false →
125 trans ? (mcc_step alpha sep) 〈〈mcc0,x〉,Some ? y〉 = 〈〈mcc1,y〉,Some ? 〈y,L〉〉.
126 #alpha #sep #x #y #H1 normalize >H1 //
131 accRealize alpha (mcc_step alpha sep)
132 〈mcc3,sep〉 (Rmcc_step_true alpha sep) (Rmcc_step_false alpha sep).
134 cut (∀P:Prop.〈mcc4,sep〉=〈mcc3,sep〉→P)
135 [#P whd in ⊢ ((??(???%?)(???%?))→?); #Hfalse destruct] #Hfalse
138 @(ex_intro … (mk_config ?? 〈mcc4,sep〉 (niltape ?))) %
139 [% [whd in ⊢ (??%?); % | @Hfalse]
140 |#H1 #H2 @False_ind @(absurd ?? H2) %]
141 |#l0 #lt0 @(ex_intro ?? 2)
142 @(ex_intro … (mk_config ?? 〈mcc4,sep〉 (leftof ? l0 lt0)))%
143 [% [whd in ⊢ (??%?);% |@Hfalse]
144 |#H1 #H2 @False_ind @(absurd ?? H2) %]
145 |#r0 #rt0 @(ex_intro ?? 2)
146 @(ex_intro … (mk_config ?? 〈mcc4,sep〉 (rightof ? r0 rt0))) %
147 [% [whd in ⊢ (??%?);% |@Hfalse]
148 |#H1 #H2 #H3 @False_ind @(absurd ?? H3) %]
149 | #lt #c #rt cases (true_or_false (c == sep)) #Hc
151 @(ex_intro ?? (mk_config ?? 〈mcc4,sep〉 (midtape ? lt c rt)))
153 [ >(\P Hc) >loop_S_false // >loop_S_true
154 [ @eq_f whd in ⊢ (??%?); >mcc_trans_init_sep %
155 |>(\P Hc) whd in ⊢(??(???(???%))?); >mcc_trans_init_sep % ]
157 |#_ #H1 #H2 % // normalize >(\P Hc) % ]
158 | @(ex_intro ?? 4) cases lt
161 [ >loop_S_false // >mcc_q0_q1 //
162 | normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
163 | normalize in ⊢ (%→?); #_ #H1 @False_ind @(absurd ?? H1) % ] ]
166 [ >loop_S_false // >mcc_q0_q1 //
167 | #_ #a #b #ls #rs #Hb destruct %
169 | >mcc_q1_q2 >mcc_q2_q3 cases rs normalize // ] ]
170 | normalize in ⊢ (% → ?); * #Hfalse
178 (* the move_char (variant c) machine *)
179 definition move_char_c ≝
180 λalpha,sep.whileTM alpha (mcc_step alpha sep) 〈mcc3,sep〉.
182 definition R_move_char_c ≝
184 ∀b,a,ls,rs. t1 = midtape alpha (a::ls) b rs →
185 (b = sep → t2 = t1) ∧
186 (∀rs1,rs2.rs = rs1@sep::rs2 →
187 b ≠ sep → memb ? sep rs1 = false →
188 t2 = midtape alpha (a::reverse ? rs1@b::ls) sep rs2).
190 lemma sem_move_char_c :
192 WRealize alpha (move_char_c alpha sep) (R_move_char_c alpha sep).
193 #alpha #sep #inc #i #outc #Hloop
194 lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%]
195 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
196 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
198 [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??)
199 [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2)]
200 | #rs1 #rs2 #Hrs #Hb #Hrs1
201 >Htapea in H1; #H1 cases (H1 ??)
202 [#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct %
203 |*:% #H2 normalize in H2; destruct (H2) ]
205 | #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
206 lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH
207 #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea)
209 [ #Hfalse @False_ind @(absurd ?? Ha0) //
211 [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ (* normalize *)
212 >Hrs in Htapeb; #Htapeb normalize in Htapeb;
213 cases (IH … Htapeb) #Houtc #_ >Houtc normalize //
214 | #r0 #rs0 #rs2 #Hrs #_ #Hrs0
215 cut (r0 ≠ sep ∧ memb … sep rs0 = false)
217 [ % #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct
218 | whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse
223 #Hr0 -Hrs0 #Hrs0 >Hrs in Htapeb;
224 normalize in ⊢ (%→?); #Htapeb
225 cases (IH … Htapeb) -IH #_ #IH
226 >reverse_cons >associative_append @IH //
231 lemma terminate_move_char_c :
232 ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha (a::ls) b rs →
233 (b = sep ∨ memb ? sep rs = true) → Terminate alpha (move_char_c alpha sep) t.
234 #alpha #sep #t #b #a #ls #rs #Ht #Hsep
235 @(terminate_while … (sem_mcc_step alpha sep))
237 |generalize in match Hsep; -Hsep
238 generalize in match Ht; -Ht
239 generalize in match ls; -ls
240 generalize in match a; -a
241 generalize in match b; -b
242 generalize in match t; -t
244 [#t #b #a #ls #Ht #Hsep % #tinit
245 whd in ⊢ (%→?); #H @False_ind
246 cases (H … Ht) #Hb #_ cases Hb #eqb @eqb
247 cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
248 |#r0 #rs0 #Hind #t #b #a #ls #Ht #Hsep % #tinit
250 cases (H … Ht) #Hbsep #Htinit
251 @(Hind … Htinit) cases Hsep
252 [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
253 [#eqsep %1 >(\P eqsep) // | #H %2 //]