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/if_multi.ma".
13 include "turing/inject.ma".
14 include "turing/basic_machines.ma".
16 definition Rtc_multi_true ≝
17 λalpha,test,n,i.λt1,t2:Vector ? (S n).
18 (∃c. current alpha (nth i ? t1 (niltape ?)) = Some ? c ∧ test c = true) ∧ t2 = t1.
20 definition Rtc_multi_false ≝
21 λalpha,test,n,i.λt1,t2:Vector ? (S n).
22 (∀c. current alpha (nth i ? t1 (niltape ?)) = Some ? c → test c = false) ∧ t2 = t1.
24 lemma sem_test_char_multi :
25 ∀alpha,test,n,i.i ≤ n →
26 inject_TM ? (test_char ? test) n i ⊨
27 [ tc_true : Rtc_multi_true alpha test n i, Rtc_multi_false alpha test n i ].
28 #alpha #test #n #i #Hin #int
29 cases (acc_sem_inject … Hin (sem_test_char alpha test) int)
30 #k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ %
32 | #Hqtrue lapply (Htrue Hqtrue) * * * #c *
33 #Hcur #Htestc #Hnth_i #Hnth_j %
35 | @(eq_vec … (niltape ?)) #i0 #Hi0
36 cases (decidable_eq_nat i0 i) #Hi0i
38 | @sym_eq @Hnth_j @sym_not_eq // ] ] ]
39 | #Hqfalse lapply (Hfalse Hqfalse) * * #Htestc #Hnth_i #Hnth_j %
41 | @(eq_vec … (niltape ?)) #i0 #Hi0
42 cases (decidable_eq_nat i0 i) #Hi0i
44 | @sym_eq @Hnth_j @sym_not_eq // ] ] ]
47 definition Rm_test_null_true ≝
48 λalpha,n,i.λt1,t2:Vector ? (S n).
49 current alpha (nth i ? t1 (niltape ?)) ≠ None ? ∧ t2 = t1.
51 definition Rm_test_null_false ≝
52 λalpha,n,i.λt1,t2:Vector ? (S n).
53 current alpha (nth i ? t1 (niltape ?)) = None ? ∧ t2 = t1.
55 lemma sem_test_null_multi : ∀alpha,n,i.i ≤ n →
56 inject_TM ? (test_null ?) n i ⊨
57 [ tc_true : Rm_test_null_true alpha n i, Rm_test_null_false alpha n i ].
58 #alpha #n #i #Hin #int
59 cases (acc_sem_inject … Hin (sem_test_null alpha) int)
60 #k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ %
62 | #Hqtrue lapply (Htrue Hqtrue) * * #Hcur #Hnth_i #Hnth_j % //
63 @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) #Hi0i
64 [ >Hi0i @sym_eq @Hnth_i | @sym_eq @Hnth_j @sym_not_eq // ] ]
65 | #Hqfalse lapply (Hfalse Hqfalse) * * #Hcur #Hnth_i #Hnth_j %
67 | @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) //
68 #Hi0i @sym_eq @Hnth_j @sym_not_eq // ] ]
71 (* move a single tape *)
72 definition smove_states ≝ initN 2.
74 definition smove0 : smove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
75 definition smove1 : smove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
77 definition trans_smove ≝
79 λp:smove_states × (option sig).
80 let 〈q,a〉 ≝ p in match (pi1 … q) with
81 [ O ⇒ 〈smove1,None sig, D〉
82 | S _ ⇒ 〈smove1,None sig, N〉 ].
85 λsig,D.mk_TM sig smove_states (trans_smove sig D) smove0 (λq.q == smove1).
87 definition mmove ≝ λi,sig,n,D.inject_TM sig (move sig D) n i.
90 λalpha,D,t1,t2. t2 = tape_move alpha t1 D.
92 lemma sem_move_single :
93 ∀alpha,D.move alpha D ⊨ Rmove alpha D.
94 #alpha #D #int %{2} %{(mk_config ? smove_states smove1 ?)} [| % % ]
98 λalpha,n,i,D.λt1,t2:Vector ? (S n).
99 t2 = change_vec ? (S n) t1 (tape_move alpha (nth i ? t1 (niltape ?)) D) i.
101 lemma sem_move_multi :
103 mmove i alpha n D ⊨ Rm_multi alpha n i D.
104 #alpha #n #i #D #Hin #ta cases (sem_inject … Hin (sem_move_single alpha D) ta)
105 #k * #outc * #Hloop * whd in ⊢ (%→?); #Htb1 #Htb2 %{k} %{outc} % [ @Hloop ]
106 whd @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) #Hi0i
107 [ >Hi0i >Htb1 >nth_change_vec //
108 | >nth_change_vec_neq [|@sym_not_eq //] <Htb2 // @sym_not_eq // ]
111 (* simple copy with no move *)
112 definition copy_states ≝ initN 3.
114 definition cc0 : copy_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
115 definition cc1 : copy_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
117 definition trans_copy_char_N ≝
118 λsrc,dst.λsig:FinSet.λn.
119 λp:copy_states × (Vector (option sig) (S n)).
122 [ O ⇒ 〈cc1,change_vec ? (S n)
123 (change_vec ? (S n) (null_action ? n) (〈None ?,N〉) src)
124 (〈nth src ? a (None ?),N〉) dst〉
125 | S _ ⇒ 〈cc1,null_action ? n〉 ].
127 definition copy_char_N ≝
129 mk_mTM sig n copy_states (trans_copy_char_N src dst sig n)
132 definition R_copy_char_N ≝
133 λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
134 outt = change_vec ?? int
135 (tape_write ? (nth dst ? int (niltape ?))
136 (current ? (nth src ? int (niltape ?)))) dst.
138 lemma copy_char_N_q0_q1 :
139 ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n →
140 step sig n (copy_char_N src dst sig n) (mk_mconfig ??? cc0 v) =
143 (tape_write ? (nth dst ? v (niltape ?))
144 (current ? (nth src ? v (niltape ?)))) dst).
145 #src #dst #sig #n #v #Heq #Hsrc #Hdst
146 whd in ⊢ (??%?); @eq_f
147 <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
148 <(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
150 >pmap_change >pmap_change <tape_move_multi_def
151 >tape_move_null_action @eq_f3 //
153 | >change_vec_same >change_vec_same >nth_current_chars // ]
156 lemma sem_copy_char_N:
157 ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
158 copy_char_N src dst sig n ⊨ R_copy_char_N src dst sig n.
159 #src #dst #sig #n #Hneq #Hsrc #Hdst #int
160 %{2} % [| % [ % | whd >copy_char_N_q0_q1 // ]]
163 (**************** copy and advance ***********************)
164 definition copy_char_states ≝ initN 3.
166 definition trans_copy_char ≝
167 λsrc,dst.λsig:FinSet.λn.
168 λp:copy_char_states × (Vector (option sig) (S n)).
171 [ O ⇒ 〈cc1,change_vec ? (S n)
172 (change_vec ? (S n) (null_action ? n) (〈None ?,R〉) src)
173 (〈nth src ? a (None ?),R〉) dst〉
174 | S _ ⇒ 〈cc1,null_action ? n〉 ].
176 definition copy_char ≝
178 mk_mTM sig n copy_char_states (trans_copy_char src dst sig n)
181 definition R_copy_char ≝
182 λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
185 (tape_move_mono ? (nth src ? int (niltape ?)) 〈None ?, R〉) src)
186 (tape_move_mono ? (nth dst ? int (niltape ?))
187 〈current ? (nth src ? int (niltape ?)), R〉) dst.
189 lemma copy_char_q0_q1 :
190 ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n →
191 step sig n (copy_char src dst sig n) (mk_mconfig ??? cc0 v) =
195 (tape_move_mono ? (nth src ? v (niltape ?)) 〈None ?, R〉) src)
196 (tape_move_mono ? (nth dst ? v (niltape ?)) 〈current ? (nth src ? v (niltape ?)), R〉) dst).
197 #src #dst #sig #n #v #Heq #Hsrc #Hdst
199 <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
200 <(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
201 >tape_move_multi_def @eq_f2 //
202 >pmap_change >pmap_change <tape_move_multi_def
203 >tape_move_null_action @eq_f2 // @eq_f2
205 | >change_vec_same >change_vec_same // ]
209 ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
210 copy_char src dst sig n ⊨ R_copy_char src dst sig n.
211 #src #dst #sig #n #Hneq #Hsrc #Hdst #int
212 %{2} % [| % [ % | whd >copy_char_q0_q1 // ]]
217 (********************** look_ahead test *************************)
219 definition mtestR ≝ λsig,i,n,test.
221 (ifTM ?? (inject_TM ? (test_char ? test) n i)
222 (single_finalTM ?? (mmove i sig n L))
223 (mmove i sig n L) tc_true).
227 definition RmtestR_true ≝ λsig,i,n,test.λt1,t2:Vector ? n.
229 nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
230 t1 = t2 ∧ (test c1 = true).
232 definition RmtestR_false ≝ λsig,i,n,test.λt1,t2:Vector ? n.
234 nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
235 t1 = t2 ∧ (test c1 = false).
237 definition mtestR_acc: ∀sig,i,n,test.states ?? (mtestR sig i n test).
238 #sig #i #n #test @inr @inr @inl @inr @start_nop
241 lemma sem_mtestR: ∀sig,i,n,test. i ≤ n →
242 mtestR sig i n test ⊨
243 [mtestR_acc sig i n test:
244 RmtestR_true sig i (S n) test, RmtestR_false sig i (S n) test].
245 #sig #i #n #test #Hlein
246 @(acc_sem_seq_app sig n … (sem_move_multi … R Hlein)
247 (acc_sem_if sig n ????????
248 (sem_test_char_multi sig test n i Hlein)
249 (sem_move_multi … L Hlein)
250 (sem_move_multi … L Hlein)))
251 [#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in ⊢ (%→?); * *
252 #cx #Hcx #Htx #Ht2 #ls #c #c1 #rs #Ht1
253 >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
254 >Ht3 in Hcx; >nth_change_vec [|@le_S_S //] * whd in ⊢ (??%?→?);
255 #Hsome destruct (Hsome) #Htest % [2:@Htest]
256 >Htx in Ht2; whd in ⊢ (%→?); #Ht2 @(eq_vec … (niltape ?))
257 #j #lejn cases (true_or_false (eqb i j)) #Hij
258 [lapply lejn <(eqb_true_to_eq … Hij) #lein >Ht2 >nth_change_vec [2://]
259 >Ht3 >nth_change_vec >Ht1 //
260 |lapply (eqb_false_to_not_eq … Hij) #Hneq >Ht2 >nth_change_vec_neq [2://]
261 >Ht3 >nth_change_vec_neq //
263 |#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in ⊢ (%→?); *
264 #Hcx #Heqtx #Htx #ls #c #c1 #rs #Ht1
265 >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
266 >Ht3 in Hcx; >nth_change_vec [2:@le_S_S //] #Hcx lapply (Hcx ? (refl ??))
267 #Htest % // @(eq_vec … (niltape ?))
268 #j #lejn cases (true_or_false (eqb i j)) #Hij
269 [lapply lejn <(eqb_true_to_eq … Hij) #lein >Htx >nth_change_vec [2://]
270 >Heqtx >Ht3 >nth_change_vec >Ht1 //
271 |lapply (eqb_false_to_not_eq … Hij) #Hneq >Htx >nth_change_vec_neq [2://]
272 >Heqtx >Ht3 >nth_change_vec_neq //