1 (* include "turing/auxiliary_machines.ma". *)
3 include "turing/multi_to_mono/shift_trace.ma".
4 include "turing/multi_universal/normalTM.ma". (* for DeqMove *)
6 (******************************************************************************)
8 (* exec_move_R : before shifting the trace left - to simulate a right move of
9 the head - we must be sure we are not in rightoverflow, that is that the symbol
10 at the right of the head, if any, is not blank *)
12 (* a simple look-ahead machine *)
13 definition mtestR ≝ λsig,test.
15 (ifTM ? (test_char ? test)
16 (single_finalTM ? (move sig L))
17 (move sig L) tc_true).
20 definition RmtestR_true ≝ λsig,test.λt1,t2.
22 t1 = midtape sig ls c rs →
23 ∃c1,rs1. rs = c1::rs1 ∧ t1 = t2 ∧ (test c1 = true).
25 definition RmtestR_false ≝ λsig,test.λt1,t2.
27 t1 = midtape sig ls c (c1::rs) →
28 t1 = t2 ∧ (test c1 = false)) ∧
30 t1 = midtape sig ls c [] → t1 = t2).
32 definition mtestR_acc: ∀sig,test.states ? (mtestR sig test).
33 #sig #test @inr @inr @inl @inr @start_nop
36 lemma sem_mtestR: ∀sig,test.
39 RmtestR_true sig test, RmtestR_false sig test].
41 @(acc_sem_seq_app sig … (sem_move_single … )
43 (sem_test_char sig test)
45 (sem_move_single … )))
46 [#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in ⊢ (%→?); * *
47 #cx * #Hcx #H1cx #Htx #Ht2 #ls #c #rs #Ht1
48 >Ht1 in Hmove; cases rs
49 [#H >H in Hcx; whd in ⊢ (??%?→?); #H1 destruct (H1)
50 |#c1 #rs1 #Ht3 %{c1} %{rs1} %
51 [% [//|>Htx in Ht2; >Ht3 whd in ⊢ (%→?); #H @sym_eq @H ]
52 |>Ht3 in Hcx; whd in ⊢ (??%?→?); #H1 destruct (H1) //
55 |#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in ⊢ (%→?); *
58 >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
59 >Ht3 in Hcx; #Hcx lapply (Hcx ? (refl ??))
60 #Htest % // >Heqtx in Htx; >Ht3 whd in ⊢ (%→?); #H @sym_eq @H
61 |#ls0 #c0 #Ht1 >Ht1 in Hmove; whd in match (tape_move ???);
62 <Heqtx #H1tx >H1tx in Htx; #H @sym_eq @H
67 definition guarded_M ≝ λsig,n,i,M.
68 (ifTM ? (test_char ? (no_blank sig n i))
70 (ifTM ? (mtestR ? (no_blank sig n i))
72 (nop ?) (mtestR_acc …)) tc_true).
74 definition R_guarded_M ≝ λsig,n,i,RM,t1,t2.
75 ∀ls,a,rs. t1 = midtape ? ls a rs →
76 (no_blank sig n i a = false →
77 no_blank sig n i (hd ? rs (all_blank …)) = false → t1=t2) ∧
78 (no_blank sig n i a = true ∨
79 no_blank sig n i (hd ? rs (all_blank …)) = true → RM t1 t2).
81 lemma sem_R_guarded: ∀sig,n,i,M,RM. M ⊨ RM →
82 guarded_M sig n i M ⊨ R_guarded_M sig n i RM.
84 @(sem_if_app … (sem_test_char … ) HM
85 (sem_if … (sem_mtestR … ) HM (sem_nop ?)))
87 [* * * #c * #Hc #H1c #Ht1 #Htout #ls #a #rs #Htin
88 >Htin in Hc; normalize in ⊢ (%→?); #H1 destruct (H1) %
89 [>H1c #H2 @False_ind destruct (H2)
90 |#H1 <Htin <Ht1 @Htout
92 |* * #Hc #Ht1 #H #ls #a #rs lapply (Hc a) <Ht1 -Ht1 #Ha #Ht1
94 [* #t2 * #Ht2 lapply (Ht2 … Ht1)
95 * #c1 * #rs1 * * #H1 #H2 #H3 #H4 % [2: //]
96 #Ha >H1 whd in match (hd ???); >H3 #H destruct (H)
97 |lapply Ht1 -Ht1 cases rs
98 [#Ht1 * #t2 * * #_ #Ht2 lapply (Ht2 … Ht1) -Ht2 #Ht2
99 whd in ⊢ (%→?); #Htout % [//] *
100 [>Ha [#H destruct (H)| >Ht1 %]
101 |whd in ⊢ (??%?→?); >blank_all_blank whd in ⊢ (??%?→?);
104 |#c #rs1 #Ht1 * #t2 * * #Ht2 #_ lapply (Ht2 … Ht1) -Ht2 *
105 #Ht2 whd in ⊢ (??%?→?); #Hnb whd in ⊢ (%→?); #Htout % [//] *
106 [>Ha [#H destruct (H)| >Ht1 %]
107 |whd in ⊢ (??%?→?); whd in match (hd ???); >Hnb whd in ⊢ (??%?→?);
115 definition move_R_i ≝ λsig,n,i. guarded_M sig n i (mtiL sig n i).
117 definition Rmove_R_i ≝ λsig,n,i. R_guarded_M sig n i (Rmtil sig n i).
120 (*************************** readback of the tape *****************************)
122 definition opt_cur ≝ λsig,a.
123 if a == blank sig then None ? else Some ? a.
125 definition rb_trace ≝ λsig,ls,a,rs.
126 mk_tape ? (to_blank ? ls) (opt_cur sig a) (to_blank ? rs).
128 lemma rb_trace_def: ∀sig,ls,a,rs.
129 rb_trace sig ls a rs =
130 mk_tape ? (to_blank ? ls) (opt_cur sig a) (to_blank ? rs).
133 definition rb_trace_i ≝ λsig,n,ls,a,rs,i.
134 rb_trace sig (trace ? n i ls) (nth i ? a (blank ?)) (trace ? n i rs).
136 lemma rb_trace_i_def: ∀sig,n,ls,a,rs,i.
137 rb_trace_i sig n ls a rs i =
138 rb_trace sig (trace ? n i ls) (nth i ? a (blank ?)) (trace ? n i rs).
141 let rec readback sig n ls a rs i on i : Vector (tape (sig_ext sig)) i ≝
143 [ O ⇒ mk_Vector ? 0 (nil ?) (refl ??)
144 | S j ⇒ vec_cons ? (rb_trace_i sig n ls a rs j) j (readback sig n ls a rs j)
147 lemma orb_false_l: ∀b1,b2:bool.
148 (b1 ∨ b2) = false → (b1 = false) ∧ (b2 = false).
149 * * normalize /2/ qed.
151 lemma no_blank_true_to_not_blank: ∀sig,n,a,i.
152 (no_blank sig n i a = true) → nth i ? (vec … n a) (blank sig) ≠ blank ?.
153 #sig #n #a #i #H @(not_to_not … (eqnot_to_noteq … false H))
157 lemma rb_move_R : ∀sig,n,ls,a,rs,outt,i.
158 (∀i.regular_trace sig n a ls rs i) →
159 nth n ? (vec … a) (blank ?) = head ? →
162 Rmove_R_i … i (midtape ? ls a rs) outt →
164 outt = midtape ? ls1 a1 rs1 ∧
165 (∀i.regular_trace sig n a1 ls1 rs1 i) ∧
166 rb_trace_i sig n ls1 (vec … a1) rs1 i =
167 tape_move ? (rb_trace_i sig n ls (vec … a) rs i) R ∧
169 rb_trace_i sig n ls1 (vec … a1) rs1 j =
170 rb_trace_i sig n ls (vec … a) rs j.
171 #sig #n #ls #a #rs #outt #i #Hreg #Hha #Hhls #Hhrs #Hmove
172 lapply (Hmove … (refl …)) -Hmove * #HMove1 #HMove2
173 cases (true_or_false (no_blank sig n i a ∨
174 no_blank sig n i (hd (multi_sig sig n) rs (all_blank sig n))))
175 [2: #Hcase cases (orb_false_l … Hcase) -Hcase #Hb1 #Hb2
176 lapply (HMove1 … Hb1 Hb2) #Hout %{ls} %{a} %{rs}
177 %[%[%[@sym_eq @Hout |@Hreg]
179 cut (nth i ? (vec … a) (blank ?) = blank sig)
180 [@(\P ?) @injective_notb @Hb1] #Ha >Ha
181 >rb_trace_def whd in match (opt_cur ??);
182 cut (to_blank sig (trace sig n i rs) = [])
184 cases (to_blank sig (trace sig n i ls)) //
188 lapply(HMove2 (orb_true_l … Hb) … (refl …) Hha Hreg ? Hhls Hhrs) -HMove2
189 [#Hb1 lapply Hb -Hb whd in match (no_blank sig n i a);
190 >Hb1 #H @no_blank_true_to_not_blank @H]
191 * #ls1 * #a1 * #rs1 * * * * * #H1 #H2 #H3 #H4 #H5 #H6
194 |(* either a is blank or not *)
195 cases (true_or_false (no_blank sig n i a)) #Hba
197 >rb_trace_i_def >rb_trace_def <to_blank_i_def >H5 >to_blank_cons_nb
198 [2: @no_blank_true_to_not_blank //]
199 lapply H6 -H6 #Hrs >(rb_trace_i_def … rs i) >rb_trace_def
200 <(to_blank_i_def … rs) <Hrs
201 cut (opt_cur sig (nth i ? (vec … a) (blank sig)) =
202 Some ? (nth i ? (vec … a) (blank sig))) [@daemon] #Ha >Ha
203 (* either a1 is blank or not *)
204 cases (true_or_false (no_blank sig n i a1)) #Hba1
205 [cut (opt_cur sig (nth i ? (vec … a1) (blank sig)) =
206 Some ? (nth i ? (vec … a1) (blank sig))) [@daemon] #Ha1 >Ha1
207 >to_blank_cons_nb [%|@(\Pf ?) @injective_notb @Hba1]
208 |cut (opt_cur sig (nth i ? (vec … a1) (blank sig)) = None ?) [@daemon]
210 cut (to_blank_i … i (a1::rs1) = [ ]) [@daemon] #Ha1rs1 >Ha1rs1
211 cut (to_blank_i … i rs1 = [ ]) [@daemon] #Hrs1 <to_blank_i_def >Hrs1 %
213 |>rb_trace_i_def >rb_trace_def <to_blank_i_def (* >H5 >to_blank_cons_nb *)
214 >rb_trace_i_def >rb_trace_def <(to_blank_i_def … rs) <H6 >H5
215 cut (to_blank_i … i (a::ls) = [ ]) [@daemon] #Hals >Hals
216 cut (to_blank_i … i ls = [ ]) [@daemon] #Hls <(to_blank_i_def … ls) >Hls
217 cut (opt_cur sig (nth i ? (vec … a) (blank sig)) = None ?) [@daemon] #Ha >Ha
218 cut (nth i ? (vec … a1) (blank ?) ≠ blank ?) [@daemon] #Ha1
219 >(to_blank_cons_nb … Ha1)
220 cut (opt_cur sig (nth i ? (vec … a1) (blank sig)) =
221 Some ? (nth i ? (vec … a1) (blank sig))) [@daemon] -Ha1 #Ha1 >Ha1 %
225 #j #Hle #Hneq >rb_trace_i_def >rb_trace_i_def >rb_trace_def >rb_trace_def
226 <(to_blank_i_def … rs) <(to_blank_i_def … rs1) >(H4 j Hle Hneq)
227 cut ((to_blank_i sig n j ls1 = to_blank_i sig n j ls) ∧
228 (opt_cur sig (nth j (sig_ext sig) (vec … a1) (blank sig)) =
229 opt_cur sig (nth j (sig_ext sig) (vec … a) (blank sig))))
230 [@daemon] * #H7 #H8 >H7 >H8 //
235 definition Rmove_R_i_rb ≝ λsig,n,i,t1,t2.
237 t1 = midtape ? ls a rs →
238 (∀i.regular_trace sig n a ls rs i) →
239 nth n ? (vec … a) (blank ?) = head ? →
243 t2 = midtape (multi_sig sig n) ls1 a1 rs1 ∧
244 (∀i.regular_trace sig n a1 ls1 rs1 i) ∧
245 rb_trace_i sig n ls1 (vec … a1) rs1 i =
246 tape_move ? (rb_trace_i sig n ls (vec … a) rs i) R ∧
248 rb_trace_i sig n ls1 (vec … a1) rs1 j =
249 rb_trace_i sig n ls (vec … a) rs j.
251 lemma sem_move_R_i : ∀sig,n,i.i < n →
252 move_R_i sig n i ⊨ Rmove_R_i_rb sig n i.
253 #sig #n #i #ltin @(Realize_to_Realize … (Rmove_R_i sig n i))
254 [#t1 #t2 #H #ls #a #rs #H1 #H2 #H3 #H4 #H5 @rb_move_R // <H1 //
255 |@sem_R_guarded @sem_Rmtil //
259 (* move_L_i axiomatized *)
261 axiom move_L_i : ∀sig.∀n,i:nat.TM (multi_sig sig n).
263 definition Rmove_L_i_rb ≝ λsig,n,i,t1,t2.
265 t1 = midtape ? ls a rs →
266 (∀i.regular_trace sig n a ls rs i) →
267 nth n ? (vec … a) (blank ?) = head ? →
271 t2 = midtape (multi_sig sig n) ls1 a1 rs1 ∧
272 (∀i.regular_trace sig n a1 ls1 rs1 i) ∧
273 rb_trace_i sig n ls1 (vec … a1) rs1 i =
274 tape_move ? (rb_trace_i sig n ls (vec … a) rs i) L ∧
276 rb_trace_i sig n ls1 (vec … a1) rs1 j =
277 rb_trace_i sig n ls (vec … a) rs j.
279 axiom sem_move_L_i : ∀sig,n,i.i < n →
280 move_L_i sig n i ⊨ Rmove_L_i_rb sig n i.
283 lemma rb_move_L : ∀sig,n,ls,a,rs,outt,i.
284 (∀i.regular_trace sig n a ls rs i) →
285 nth n ? (vec … a) (blank ?) = head ? →
288 Rmove_L_i … i (midtape ? ls a rs) outt →
290 outt = midtape ? ls1 a1 rs1 ∧
291 rb_trace_i sig n ls1 (vec … a1) rs1 i =
292 tape_move ? (rb_trace_i sig n ls (vec … a) rs i) L ∧
294 rb_trace_i sig n ls1 (vec … a1) rs1 j =
295 rb_trace_i sig n ls (vec … a) rs j. *)
297 (* The following function read a move from a vector of moves and executes it *)
299 axiom get_move : ∀sig.∀n.∀a:multi_sig sig n.nat → DeqMove.
301 definition exec_move_i ≝ λsig,n,i.
302 (ifTM ? (test_char ? (λa. (get_move sig n a i == R)))
304 (ifTM ? (test_char ? (λa. (get_move sig n a i == L)))
306 (nop ?) tc_true) tc_true).
308 definition R_exec_move_i ≝ λsig,n,i,t1,t2.
310 t1 = midtape ? ls a rs →
311 (∀i.regular_trace sig n a ls rs i) →
312 nth n ? (vec … a) (blank ?) = head ? →
316 t2 = midtape (multi_sig sig n) ls1 a1 rs1 ∧
317 (∀i.regular_trace sig n a1 ls1 rs1 i) ∧
318 rb_trace_i sig n ls1 (vec … a1) rs1 i =
319 tape_move ? (rb_trace_i sig n ls (vec … a) rs i) (get_move sig n a i) ∧
321 rb_trace_i sig n ls1 (vec … a1) rs1 j =
322 rb_trace_i sig n ls (vec … a) rs j.
324 lemma tape_move_N: ∀A,t. tape_move A t N = t.
327 lemma sem_exec_move_i: ∀sig,n,i. i < n →
328 exec_move_i sig n i ⊨ R_exec_move_i sig n i.
330 @(sem_if_app … (sem_test_char …)
331 (sem_move_R_i … ltin)
332 (sem_if … (sem_test_char …)
333 (sem_move_L_i … ltin) (sem_nop ?)))
335 [* * * #c * #Hc #HR #Ht1 #HMR
336 #a #ls #rs #Htin >Htin in Hc; whd in ⊢ (??%?→?); #H destruct (H)
337 >(\P HR) @HMR >Ht1 @Htin
339 [* #t2 * * * #c * #Hc #HL #Ht2 #HML
340 #a #ls #rs #Htin >Htin in Hc; whd in ⊢ (??%?→?); #H destruct (H)
341 >(\P HL) @HML >Ht2 @Htin
342 |* #t2 * * #HL #Ht2 >Ht2 whd in ⊢ (%→?); #Htout >Htout
343 #a #ls #rs #Htin >Htin in HR; #HR >Htin in HL; #HL
344 cut (get_move sig n a i = N)
345 [lapply (HR a (refl … )) lapply (HL a (refl … ))
346 cases (get_move sig n a i) normalize
347 [#H destruct (H) |#_ #H destruct (H) | //]]
348 #HN >HN >tape_move_N #Hreg #_ #_ #_
350 %[%[%[%|@Hreg] |%] | //]
355 axiom reg_inv : ∀sig,n,a,ls,rs,a1,ls1,rs1.
356 regular_trace sig n a1 ls1 rs1 n →
357 (rb_trace_i sig n ls1 (vec … a1) rs1 n =
358 rb_trace_i sig n ls (vec … n a) rs n) →
359 nth n ? (vec … a) (blank ?) = head ? →
362 nth n ? (vec … a1) (blank ?) = head ? ∧
363 no_head_in … ls1 ∧ no_head_in … rs1.