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 ?〉 ])
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 ?〉
47 | Some a' ⇒ match (pi1 … q) with
48 [ O ⇒ 〈move1,Some ? 〈a',R〉〉
49 | S q ⇒ 〈move1,None ?〉 ] ])
50 move0 (λq.q == move1).
52 definition R_move_r ≝ λalpha,t1,t2.
54 t1 = midtape alpha ls c rs →
55 t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
58 ∀alpha.Realize ? (move_r alpha) (R_move_r alpha).
59 #alpha #intape @(ex_intro ?? 2) cases intape
61 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
63 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
65 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
67 @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
71 (******************** moves the head one step to the left *********************)
74 λalpha:FinSet.mk_TM alpha move_states
77 [ None ⇒ 〈move1,None ?〉
78 | Some a' ⇒ match pi1 … q with
79 [ O ⇒ 〈move1,Some ? 〈a',L〉〉
80 | S q ⇒ 〈move1,None ?〉 ] ])
81 move0 (λq.q == move1).
83 definition R_move_l ≝ λalpha,t1,t2.
85 t1 = midtape alpha ls c rs →
86 t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
89 ∀alpha.Realize ? (move_l alpha) (R_move_l alpha).
90 #alpha #intape @(ex_intro ?? 2) cases intape
92 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
94 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
96 [| % [ % | #ls #c #rs #Hfalse destruct ] ]
98 @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
102 (********************************* test char **********************************)
104 (* the test_char machine ends up in two different states q1 and q2 wether or not
105 the current character satisfies a boolean test function passed as a parameter to
107 The machine ends up in q1 also in case there is no current character.
110 definition tc_states ≝ initN 3.
112 definition tc_start : tc_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
113 definition tc_true : tc_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
114 definition tc_false : tc_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
116 definition test_char ≝
117 λalpha:FinSet.λtest:alpha→bool.
118 mk_TM alpha tc_states
121 [ None ⇒ 〈tc_true, None ?〉
124 [ true ⇒ 〈tc_true,None ?〉
125 | false ⇒ 〈tc_false,None ?〉 ]])
126 tc_start (λx.notb (x == tc_start)).
128 definition Rtc_true ≝
130 ∀c. current alpha t1 = Some ? c → test c = true ∧ t2 = t1.
132 definition Rtc_false ≝
134 ∀c. current alpha t1 = Some ? c → test c = false ∧ t2 = t1.
137 ∀alpha,test,ls,a0,rs. test a0 = true →
138 step alpha (test_char alpha test)
139 (mk_config ?? tc_start (midtape … ls a0 rs)) =
140 mk_config alpha (states ? (test_char alpha test)) tc_true
141 (midtape … ls a0 rs).
142 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
143 whd in match (trans … 〈?,?〉); >Htest %
147 ∀alpha,test,ls,a0,rs. test a0 = false →
148 step alpha (test_char alpha test)
149 (mk_config ?? tc_start (midtape … ls a0 rs)) =
150 mk_config alpha (states ? (test_char alpha test)) tc_false
151 (midtape … ls a0 rs).
152 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
153 whd in match (trans … 〈?,?〉); >Htest %
156 lemma sem_test_char :
158 accRealize alpha (test_char alpha test)
159 tc_true (Rtc_true alpha test) (Rtc_false alpha test).
162 @(ex_intro ?? (mk_config ?? tc_true (niltape ?))) %
163 [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
164 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_true (leftof ? a al)))
165 % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
166 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_true (rightof ? a al)))
167 % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
168 | #ls #c #rs @(ex_intro ?? 2)
169 cases (true_or_false (test c)) #Htest
170 [ @(ex_intro ?? (mk_config ?? tc_true ?))
173 [ whd in ⊢ (??%?); >tc_q0_q1 //
174 | #_ #c0 #Hc0 % // normalize in Hc0; destruct // ]
175 | * #Hfalse @False_ind @Hfalse % ]
177 | @(ex_intro ?? (mk_config ?? tc_false (midtape ? ls c rs)))
180 [ whd in ⊢ (??%?); >tc_q0_q2 //
181 | whd in ⊢ ((??%%)→?); #Hfalse destruct (Hfalse) ]
182 | #_ #c0 #Hc0 % // normalize in Hc0; destruct (Hc0) //
188 (************************************* swap ***********************************)
189 definition swap_states : FinSet → FinSet ≝
190 λalpha:FinSet.FinProd (initN 4) alpha.
192 definition swap0 : initN 4 ≝ mk_Sig ?? 0 (leb_true_to_le 1 4 (refl …)).
193 definition swap1 : initN 4 ≝ mk_Sig ?? 1 (leb_true_to_le 2 4 (refl …)).
194 definition swap2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)).
195 definition swap3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)).
198 λalpha:FinSet.λfoo:alpha.
199 mk_TM alpha (swap_states alpha)
202 let q' ≝ pi1 nat (λi.i<4) q' in
204 [ None ⇒ 〈〈swap3,foo〉,None ?〉 (* if tape is empty then stop *)
207 [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? 〈a',R〉〉 (* save in register and move R *)
208 | S q' ⇒ match q' with
209 [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? 〈b,L〉〉 (* swap with register and move L *)
210 | S q' ⇒ match q' with
211 [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? 〈b,N〉〉 (* copy from register and stay *)
212 | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?〉 (* final state *)
217 (λq.\fst q == swap3).
222 t1 = midtape alpha ls b (a::rs) →
223 t2 = midtape alpha ls a (b::rs).
225 lemma sem_swap_r : ∀alpha,foo.
226 swap_r alpha foo ⊨ Rswap alpha.
228 [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
229 % [% |#a #b #ls #rs #H destruct]
230 |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
231 % [% |#a #b #ls #rs #H destruct]
232 |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
233 % [% |#a #b #ls #rs #H destruct]
234 | #lt #c #rt @(ex_intro ?? 4) cases rt
235 [@ex_intro [|% [ % | #a #b #ls #rs #H destruct]]
236 |#r0 #rt0 @ex_intro [| % [ % | #a #b #ls #rs #H destruct //
242 λalpha:FinSet.λfoo:alpha.
243 mk_TM alpha (swap_states alpha)
246 let q' ≝ pi1 nat (λi.i<4) q' in
248 [ None ⇒ 〈〈swap3,foo〉,None ?〉 (* if tape is empty then stop *)
251 [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? 〈a',L〉〉 (* save in register and move L *)
252 | S q' ⇒ match q' with
253 [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? 〈b,R〉〉 (* swap with register and move R *)
254 | S q' ⇒ match q' with
255 [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? 〈b,N〉〉 (* copy from register and stay *)
256 | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?〉 (* final state *)
261 (λq.\fst q == swap3).
266 t1 = midtape alpha (a::ls) b rs →
267 t2 = midtape alpha (b::ls) a rs.
269 lemma sem_swap_l : ∀alpha,foo.
270 swap_l alpha foo ⊨ Rswap_l alpha.
272 [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
273 % [% |#a #b #ls #rs #H destruct]
274 |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
275 % [% |#a #b #ls #rs #H destruct]
276 |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
277 % [% |#a #b #ls #rs #H destruct]
278 | #lt #c #rt @(ex_intro ?? 4) cases lt
279 [@ex_intro [|% [ % | #a #b #ls #rs #H destruct]]
280 |#l0 #lt0 @ex_intro [| % [ % | #a #b #ls #rs #H destruct //