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 // ] ]
70 (* move a single tape *)
71 definition mmove_states ≝ initN 2.
73 definition mmove0 : mmove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
74 definition mmove1 : mmove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
76 definition trans_mmove ≝
78 λp:mmove_states × (Vector (option sig) (S n)).
79 let 〈q,a〉 ≝ p in match (pi1 … q) with
80 [ O ⇒ 〈mmove1,change_vec ? (S n) (null_action ? n) (〈None ?,D〉) i〉
81 | S _ ⇒ 〈mmove1,null_action sig n〉 ].
85 mk_mTM sig n mmove_states (trans_mmove i sig n D)
86 mmove0 (λq.q == mmove1).
89 λalpha,n,i,D.λt1,t2:Vector ? (S n).
90 t2 = change_vec ? (S n) t1 (tape_move alpha (nth i ? t1 (niltape ?)) D) i.
92 lemma sem_move_multi :
94 mmove i alpha n D ⊨ Rm_multi alpha n i D.
95 #alpha #n #i #D #Hin #int %{2}
96 %{(mk_mconfig ? mmove_states n mmove1 ?)}
98 [ whd in ⊢ (??%?); @eq_f whd in ⊢ (??%?); @eq_f %
99 | whd >tape_move_multi_def
100 <(change_vec_same … (ctapes …) i (niltape ?))
101 >pmap_change <tape_move_multi_def >tape_move_null_action % ] ]
104 (* simple copy with no move *)
105 definition copy_states ≝ initN 3.
107 definition cc0 : copy_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
108 definition cc1 : copy_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
110 definition trans_copy_char_N ≝
111 λsrc,dst.λsig:FinSet.λn.
112 λp:copy_states × (Vector (option sig) (S n)).
115 [ O ⇒ 〈cc1,change_vec ? (S n)
116 (change_vec ? (S n) (null_action ? n) (〈None ?,N〉) src)
117 (〈nth src ? a (None ?),N〉) dst〉
118 | S _ ⇒ 〈cc1,null_action ? n〉 ].
120 definition copy_char_N ≝
122 mk_mTM sig n copy_states (trans_copy_char_N src dst sig n)
125 definition R_copy_char_N ≝
126 λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
127 outt = change_vec ?? int
128 (tape_write ? (nth dst ? int (niltape ?))
129 (current ? (nth src ? int (niltape ?)))) dst.
131 lemma copy_char_N_q0_q1 :
132 ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n →
133 step sig n (copy_char_N src dst sig n) (mk_mconfig ??? cc0 v) =
136 (tape_write ? (nth dst ? v (niltape ?))
137 (current ? (nth src ? v (niltape ?)))) dst).
138 #src #dst #sig #n #v #Heq #Hsrc #Hdst
139 whd in ⊢ (??%?); @eq_f
140 <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
141 <(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
143 >pmap_change >pmap_change <tape_move_multi_def
144 >tape_move_null_action @eq_f3 //
146 | >change_vec_same >change_vec_same >nth_current_chars // ]
149 lemma sem_copy_char_N:
150 ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
151 copy_char_N src dst sig n ⊨ R_copy_char_N src dst sig n.
152 #src #dst #sig #n #Hneq #Hsrc #Hdst #int
153 %{2} % [| % [ % | whd >copy_char_N_q0_q1 // ]]
156 (**************** copy and advance ***********************)
157 definition copy_char_states ≝ initN 3.
159 definition trans_copy_char ≝
160 λsrc,dst.λsig:FinSet.λn.
161 λp:copy_char_states × (Vector (option sig) (S n)).
164 [ O ⇒ 〈cc1,change_vec ? (S n)
165 (change_vec ? (S n) (null_action ? n) (〈None ?,R〉) src)
166 (〈nth src ? a (None ?),R〉) dst〉
167 | S _ ⇒ 〈cc1,null_action ? n〉 ].
169 definition copy_char ≝
171 mk_mTM sig n copy_char_states (trans_copy_char src dst sig n)
174 definition R_copy_char ≝
175 λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
178 (tape_move_mono ? (nth src ? int (niltape ?)) 〈None ?, R〉) src)
179 (tape_move_mono ? (nth dst ? int (niltape ?))
180 〈current ? (nth src ? int (niltape ?)), R〉) dst.
182 lemma copy_char_q0_q1 :
183 ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n →
184 step sig n (copy_char src dst sig n) (mk_mconfig ??? cc0 v) =
188 (tape_move_mono ? (nth src ? v (niltape ?)) 〈None ?, R〉) src)
189 (tape_move_mono ? (nth dst ? v (niltape ?)) 〈current ? (nth src ? v (niltape ?)), R〉) dst).
190 #src #dst #sig #n #v #Heq #Hsrc #Hdst
192 <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
193 <(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
194 >tape_move_multi_def @eq_f2 //
195 >pmap_change >pmap_change <tape_move_multi_def
196 >tape_move_null_action @eq_f2 // @eq_f2
198 | >change_vec_same >change_vec_same // ]
202 ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
203 copy_char src dst sig n ⊨ R_copy_char src dst sig n.
204 #src #dst #sig #n #Hneq #Hsrc #Hdst #int
205 %{2} % [| % [ % | whd >copy_char_q0_q1 // ]]
210 (********************** look_ahead test *************************)
212 definition mtestR ≝ λsig,i,n,test.
214 (ifTM ?? (inject_TM ? (test_char ? test) n i)
215 (single_finalTM ?? (mmove i sig n L))
216 (mmove i sig n L) tc_true).
220 definition RmtestR_true ≝ λsig,i,n,test.λt1,t2:Vector ? n.
222 nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
223 t1 = t2 ∧ (test c1 = true).
225 definition RmtestR_false ≝ λsig,i,n,test.λt1,t2:Vector ? n.
227 nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
228 t1 = t2 ∧ (test c1 = false).
230 definition mtestR_acc: ∀sig,i,n,test.states ?? (mtestR sig i n test).
231 #sig #i #n #test @inr @inr @inl @inr @start_nop
234 lemma sem_mtestR: ∀sig,i,n,test. i ≤ n →
235 mtestR sig i n test ⊨
236 [mtestR_acc sig i n test:
237 RmtestR_true sig i (S n) test, RmtestR_false sig i (S n) test].
238 #sig #i #n #test #Hlein
239 @(acc_sem_seq_app sig n … (sem_move_multi … R Hlein)
240 (acc_sem_if sig n ????????
241 (sem_test_char_multi sig test n i Hlein)
242 (sem_move_multi … L Hlein)
243 (sem_move_multi … L Hlein)))
244 [#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in ⊢ (%→?); * *
245 #cx #Hcx #Htx #Ht2 #ls #c #c1 #rs #Ht1
246 >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
247 >Ht3 in Hcx; >nth_change_vec [|@le_S_S //] * whd in ⊢ (??%?→?);
248 #Hsome destruct (Hsome) #Htest % [2:@Htest]
249 >Htx in Ht2; whd in ⊢ (%→?); #Ht2 @(eq_vec … (niltape ?))
250 #j #lejn cases (true_or_false (eqb i j)) #Hij
251 [lapply lejn <(eqb_true_to_eq … Hij) #lein >Ht2 >nth_change_vec [2://]
252 >Ht3 >nth_change_vec >Ht1 //
253 |lapply (eqb_false_to_not_eq … Hij) #Hneq >Ht2 >nth_change_vec_neq [2://]
254 >Ht3 >nth_change_vec_neq //
256 |#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in ⊢ (%→?); *
257 #Hcx #Heqtx #Htx #ls #c #c1 #rs #Ht1
258 >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
259 >Ht3 in Hcx; >nth_change_vec [2:@le_S_S //] #Hcx lapply (Hcx ? (refl ??))
260 #Htest % // @(eq_vec … (niltape ?))
261 #j #lejn cases (true_or_false (eqb i j)) #Hij
262 [lapply lejn <(eqb_true_to_eq … Hij) #lein >Htx >nth_change_vec [2://]
263 >Heqtx >Ht3 >nth_change_vec >Ht1 //
264 |lapply (eqb_false_to_not_eq … Hij) #Hneq >Htx >nth_change_vec_neq [2://]
265 >Heqtx >Ht3 >nth_change_vec_neq //