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_____________________________________________________________*)
12 include "turing/while_machine.ma".
14 (******************* write a given symbol under the head **********************)
15 definition write_states ≝ initN 2.
17 definition wr0 : write_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
18 definition wr1 : write_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
20 definition write ≝ λalpha,c.
21 mk_TM alpha write_states
24 [ O ⇒ 〈wr1,Some ? c,N〉
25 | S _ ⇒ 〈wr1,None ?,N〉 ])
28 definition R_write ≝ λalpha,c,t1,t2.
29 ∀ls,x,rs.t1 = midtape alpha ls x rs → t2 = midtape alpha ls c rs.
31 lemma sem_write : ∀alpha,c.Realize ? (write alpha c) (R_write alpha c).
32 #alpha #c #t @(ex_intro … 2) @ex_intro
33 [|% [% |#ls #c #rs #Ht >Ht % ] ]
36 (******************** moves the head one step to the right ********************)
38 definition move_states ≝ initN 2.
39 definition move0 : move_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
40 definition move1 : move_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
43 λalpha:FinSet.mk_TM alpha move_states
46 [ None ⇒ 〈move1,None ?,N〉
47 | Some a' ⇒ match (pi1 … q) with
48 [ O ⇒ 〈move1,Some ? a',R〉
49 | S q ⇒ 〈move1,None ?,N〉 ] ])
50 move0 (λq.q == move1).
52 definition R_move_r ≝ λalpha,t1,t2.
53 (current ? t1 = None ? → t1 = t2) ∧
55 t1 = midtape alpha ls c rs →
56 t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
58 (current ? t1 = None ? ∧ t1 = t2) ∨
60 t1 = midtape alpha ls c rs ∧
61 t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).*)
64 ∀alpha.Realize ? (move_r alpha) (R_move_r alpha).
65 #alpha #intape @(ex_intro ?? 2) cases intape
67 [| % [ % | % // #ls #c #rs #H destruct ] ]
69 [| % [ % | % // #ls #c #rs #H destruct ] ]
71 [| % [ % | % // #ls #c #rs #H destruct ] ]
73 @ex_intro [| % [ % | % [whd in ⊢ ((??%?)→?); #H destruct]
74 #ls1 #c1 #rs1 #H destruct cases rs1 // ] ] ]
77 (******************** moves the head one step to the left *********************)
80 λalpha:FinSet.mk_TM alpha move_states
83 [ None ⇒ 〈move1,None ?,N〉
84 | Some a' ⇒ match pi1 … q with
85 [ O ⇒ 〈move1,Some ? a',L〉
86 | S q ⇒ 〈move1,None ?,N〉 ] ])
87 move0 (λq.q == move1).
89 definition R_move_l ≝ λalpha,t1,t2.
90 (current ? t1 = None ? → t1 = t2) ∧
92 t1 = midtape alpha ls c rs →
93 t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
96 ∀alpha.Realize ? (move_l alpha) (R_move_l alpha).
97 #alpha #intape @(ex_intro ?? 2) cases intape
99 [| % [ % | % // #ls #c #rs #H destruct ] ]
101 [| % [ % | % // #ls #c #rs #H destruct ] ]
103 [| % [ % | % // #ls #c #rs #H destruct ] ]
105 @ex_intro [| % [ % | % [whd in ⊢ ((??%?)→?); #H destruct]
106 #ls1 #c1 #rs1 #H destruct cases ls1 // ] ] ]
109 (* a slightly different move machine. *)
110 definition smove_states ≝ initN 2.
112 definition smove0 : smove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
113 definition smove1 : smove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
115 definition trans_smove ≝
117 λp:smove_states × (option sig).
118 let 〈q,a〉 ≝ p in match (pi1 … q) with
119 [ O ⇒ 〈smove1,None sig, D〉
120 | S _ ⇒ 〈smove1,None sig, N〉 ].
123 λsig,D.mk_TM sig smove_states (trans_smove sig D) smove0 (λq.q == smove1).
126 λalpha,D,t1,t2. t2 = tape_move alpha t1 D.
128 lemma sem_move_single :
129 ∀alpha,D.move alpha D ⊨ Rmove alpha D.
130 #alpha #D #int %{2} %{(mk_config ? smove_states smove1 ?)} [| % % ]
133 (********************************* test char **********************************)
135 (* the test_char machine ends up in two different states q1 and q2 wether or not
136 the current character satisfies a boolean test function passed as a parameter to
138 The machine ends up in q1 also in case there is no current character.
141 definition tc_states ≝ initN 3.
143 definition tc_start : tc_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
144 definition tc_true : tc_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
145 definition tc_false : tc_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
147 definition test_char ≝
148 λalpha:FinSet.λtest:alpha→bool.
149 mk_TM alpha tc_states
152 [ None ⇒ 〈tc_false, None ?,N〉
155 [ true ⇒ 〈tc_true,None ?,N〉
156 | false ⇒ 〈tc_false,None ?,N〉 ]])
157 tc_start (λx.notb (x == tc_start)).
159 definition Rtc_true ≝
161 (∃c. current alpha t1 = Some ? c ∧ test c = true) ∧ t2 = t1.
163 definition Rtc_false ≝
165 (∀c. current alpha t1 = Some ? c → test c = false) ∧ t2 = t1.
168 ∀alpha,test,ls,a0,rs. test a0 = true →
169 step alpha (test_char alpha test)
170 (mk_config ?? tc_start (midtape … ls a0 rs)) =
171 mk_config alpha (states ? (test_char alpha test)) tc_true
172 (midtape … ls a0 rs).
173 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
174 whd in match (trans … 〈?,?〉); >Htest %
178 ∀alpha,test,ls,a0,rs. test a0 = false →
179 step alpha (test_char alpha test)
180 (mk_config ?? tc_start (midtape … ls a0 rs)) =
181 mk_config alpha (states ? (test_char alpha test)) tc_false
182 (midtape … ls a0 rs).
183 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
184 whd in match (trans … 〈?,?〉); >Htest %
187 lemma sem_test_char :
189 accRealize alpha (test_char alpha test)
190 tc_true (Rtc_true alpha test) (Rtc_false alpha test).
193 @(ex_intro ?? (mk_config ?? tc_false (niltape ?))) %
194 [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
195 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_false (leftof ? a al)))
196 % [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
197 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_false (rightof ? a al)))
198 % [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
199 | #ls #c #rs @(ex_intro ?? 2)
200 cases (true_or_false (test c)) #Htest
201 [ @(ex_intro ?? (mk_config ?? tc_true ?))
204 [ whd in ⊢ (??%?); >tc_q0_q1 //
205 | #_ % // @(ex_intro … c) /2/]
206 | * #Hfalse @False_ind @Hfalse % ]
208 | @(ex_intro ?? (mk_config ?? tc_false (midtape ? ls c rs)))
211 [ whd in ⊢ (??%?); >tc_q0_q2 //
212 | whd in ⊢ ((??%%)→?); #Hfalse destruct (Hfalse) ]
213 | #_ % // #c0 whd in ⊢ ((??%?)→?); #Hc0 destruct (Hc0) //
219 lemma test_char_inv :
220 ∀sig.∀P:tape sig → Prop.∀f,t,t0.P t → Rtc_true sig f t t0 → P t0.
221 #sig #P #f #t #t0 #HPt * #_ //
224 definition test_null ≝ λalpha.test_char alpha (λ_.true).
226 definition R_test_null_true ≝ λalpha,t1,t2.
227 current alpha t1 ≠ None ? ∧ t1 = t2.
229 definition R_test_null_false ≝ λalpha,t1,t2.
230 current alpha t1 = None ? ∧ t1 = t2.
232 lemma sem_test_null : ∀alpha.
233 test_null alpha ⊨ [ tc_true : R_test_null_true alpha, R_test_null_false alpha].
234 #alpha #t1 cases (sem_test_char alpha (λ_.true) t1) #k * #outc * * #Hloop #Htrue
235 #Hfalse %{k} %{outc} % [ %
237 | #Houtc cases (Htrue ?) [| @Houtc] * #c * #Hcurt1 #_ #Houtc1 %
238 [ >Hcurt1 % #H destruct (H) | <Houtc1 % ] ]
239 | #Houtc cases (Hfalse ?) [| @Houtc] #Habsurd #Houtc %
240 [ cases (current alpha t1) in Habsurd; // #c1 #Habsurd
241 lapply (Habsurd ? (refl ??)) #H destruct (H)
245 (************************************* swap ***********************************)
246 definition swap_states : FinSet → FinSet ≝
247 λalpha:FinSet.FinProd (initN 4) alpha.
249 definition swap0 : initN 4 ≝ mk_Sig ?? 0 (leb_true_to_le 1 4 (refl …)).
250 definition swap1 : initN 4 ≝ mk_Sig ?? 1 (leb_true_to_le 2 4 (refl …)).
251 definition swap2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)).
252 definition swap3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)).
255 λalpha:FinSet.λfoo:alpha.
256 mk_TM alpha (swap_states alpha)
259 let q' ≝ pi1 nat (λi.i<4) q' in
261 [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
264 [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? a',R〉 (* save in register and move R *)
265 | S q' ⇒ match q' with
266 [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? b,L〉 (* swap with register and move L *)
267 | S q' ⇒ match q' with
268 [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
269 | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
274 (λq.\fst q == swap3).
279 t1 = midtape alpha ls b [ ] →
280 t2 = rightof ? b ls) ∧
282 t1 = midtape alpha ls b (a::rs) →
283 t2 = midtape alpha ls a (b::rs)).
285 lemma sem_swap_r : ∀alpha,foo.
286 swap_r alpha foo ⊨ Rswap_r alpha.
288 [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
289 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
290 |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
291 % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
292 |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
293 % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
294 | #lt #c #rt @(ex_intro ?? 4) cases rt
295 [@ex_intro [|% [ % | %
296 [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
297 |#r0 #rt0 @ex_intro [| % [ % | %
298 [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
304 λalpha:FinSet.λfoo:alpha.
305 mk_TM alpha (swap_states alpha)
308 let q' ≝ pi1 nat (λi.i<4) q' in
310 [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
313 [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? a',L〉 (* save in register and move L *)
314 | S q' ⇒ match q' with
315 [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? b,R〉 (* swap with register and move R *)
316 | S q' ⇒ match q' with
317 [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
318 | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
323 (λq.\fst q == swap3).
328 t1 = midtape alpha [ ] b rs →
329 t2 = leftof ? b rs) ∧
331 t1 = midtape alpha (a::ls) b rs →
332 t2 = midtape alpha (b::ls) a rs).
334 lemma sem_swap_l : ∀alpha,foo.
335 swap_l alpha foo ⊨ Rswap_l alpha.
337 [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
338 % [% |% [#b #rs | #a #b #ls #rs] #H destruct]
339 |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
340 % [% | % [#b #rs | #a #b #ls #rs] #H destruct]
341 |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
342 % [% |% [#b #rs | #a #b #ls #rs] #H destruct]
343 | #lt #c #rt @(ex_intro ?? 4) cases lt
344 [@ex_intro [|% [ % | %
345 [#b #rs #H destruct normalize // |#a #b #ls #rs #H destruct]]]
346 |#r0 #rt0 @ex_intro [| % [ % | %
347 [#b #rs #H destruct | #a #b #ls #rs #H destruct normalize //