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/basic_machines.ma".
13 include "turing/if_multi.ma".
14 include "turing/while_multi.ma".
15 include "turing/inject.ma".
16 include "turing/basic_multi_machines.ma".
18 (**************************** injected machines *******************************)
20 definition Rtc_multi_true ≝
21 λalpha,test,n,i.λt1,t2:Vector ? (S n).
22 (∃c. current alpha (nth i ? t1 (niltape ?)) = Some ? c ∧ test c = true) ∧ t2 = t1.
24 definition Rtc_multi_false ≝
25 λalpha,test,n,i.λt1,t2:Vector ? (S n).
26 (∀c. current alpha (nth i ? t1 (niltape ?)) = Some ? c → test c = false) ∧ t2 = t1.
28 lemma sem_test_char_multi :
29 ∀alpha,test,n,i.i ≤ n →
30 inject_TM ? (test_char ? test) n i ⊨
31 [ tc_true : Rtc_multi_true alpha test n i, Rtc_multi_false alpha test n i ].
32 #alpha #test #n #i #Hin #int
33 cases (acc_sem_inject … Hin (sem_test_char alpha test) int)
34 #k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ %
36 | #Hqtrue lapply (Htrue Hqtrue) * * * #c *
37 #Hcur #Htestc #Hnth_i #Hnth_j %
39 | @(eq_vec … (niltape ?)) #i0 #Hi0
40 cases (decidable_eq_nat i0 i) #Hi0i
42 | @sym_eq @Hnth_j @sym_not_eq // ] ] ]
43 | #Hqfalse lapply (Hfalse Hqfalse) * * #Htestc #Hnth_i #Hnth_j %
45 | @(eq_vec … (niltape ?)) #i0 #Hi0
46 cases (decidable_eq_nat i0 i) #Hi0i
48 | @sym_eq @Hnth_j @sym_not_eq // ] ] ]
51 definition Rm_test_null_true ≝
52 λalpha,n,i.λt1,t2:Vector ? (S n).
53 current alpha (nth i ? t1 (niltape ?)) ≠ None ? ∧ t2 = t1.
55 definition Rm_test_null_false ≝
56 λalpha,n,i.λt1,t2:Vector ? (S n).
57 current alpha (nth i ? t1 (niltape ?)) = None ? ∧ t2 = t1.
59 lemma sem_test_null_multi : ∀alpha,n,i.i ≤ n →
60 inject_TM ? (test_null ?) n i ⊨
61 [ tc_true : Rm_test_null_true alpha n i, Rm_test_null_false alpha n i ].
62 #alpha #n #i #Hin #int
63 cases (acc_sem_inject … Hin (sem_test_null alpha) int)
64 #k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ %
66 | #Hqtrue lapply (Htrue Hqtrue) * * #Hcur #Hnth_i #Hnth_j % //
67 @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) #Hi0i
68 [ >Hi0i @sym_eq @Hnth_i | @sym_eq @Hnth_j @sym_not_eq // ] ]
69 | #Hqfalse lapply (Hfalse Hqfalse) * * #Hcur #Hnth_i #Hnth_j %
71 | @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) //
72 #Hi0i @sym_eq @Hnth_j @sym_not_eq // ] ]
75 (* move a single tape *)
76 definition mmove ≝ λi,sig,n,D.inject_TM sig (move sig D) n i.
79 λalpha,n,i,D.λt1,t2:Vector ? (S n).
80 t2 = change_vec ? (S n) t1 (tape_move alpha (nth i ? t1 (niltape ?)) D) i.
82 lemma sem_move_multi :
84 mmove i alpha n D ⊨ Rm_multi alpha n i D.
85 #alpha #n #i #D #Hin #ta cases (sem_inject … Hin (sem_move_single alpha D) ta)
86 #k * #outc * #Hloop * whd in ⊢ (%→?); #Htb1 #Htb2 %{k} %{outc} % [ @Hloop ]
87 whd @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) #Hi0i
88 [ >Hi0i >Htb1 >nth_change_vec //
89 | >nth_change_vec_neq [|@sym_not_eq //] <Htb2 // @sym_not_eq // ]
92 (********************** look_ahead test *************************)
94 definition mtestR ≝ λsig,i,n,test.
96 (ifTM ?? (inject_TM ? (test_char ? test) n i)
97 (single_finalTM ?? (mmove i sig n L))
98 (mmove i sig n L) tc_true).
102 definition RmtestR_true ≝ λsig,i,n,test.λt1,t2:Vector ? n.
104 nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
105 t1 = t2 ∧ (test c1 = true).
107 definition RmtestR_false ≝ λsig,i,n,test.λt1,t2:Vector ? n.
109 nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
110 t1 = t2 ∧ (test c1 = false).
112 definition mtestR_acc: ∀sig,i,n,test.states ?? (mtestR sig i n test).
113 #sig #i #n #test @inr @inr @inl @inr @start_nop
116 lemma sem_mtestR: ∀sig,i,n,test. i ≤ n →
117 mtestR sig i n test ⊨
118 [mtestR_acc sig i n test:
119 RmtestR_true sig i (S n) test, RmtestR_false sig i (S n) test].
120 #sig #i #n #test #Hlein
121 @(acc_sem_seq_app sig n … (sem_move_multi … R Hlein)
122 (acc_sem_if sig n ????????
123 (sem_test_char_multi sig test n i Hlein)
124 (sem_move_multi … L Hlein)
125 (sem_move_multi … L Hlein)))
126 [#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in ⊢ (%→?); * *
127 #cx #Hcx #Htx #Ht2 #ls #c #c1 #rs #Ht1
128 >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
129 >Ht3 in Hcx; >nth_change_vec [|@le_S_S //] * whd in ⊢ (??%?→?);
130 #Hsome destruct (Hsome) #Htest % [2:@Htest]
131 >Htx in Ht2; whd in ⊢ (%→?); #Ht2 @(eq_vec … (niltape ?))
132 #j #lejn cases (true_or_false (eqb i j)) #Hij
133 [lapply lejn <(eqb_true_to_eq … Hij) #lein >Ht2 >nth_change_vec [2://]
134 >Ht3 >nth_change_vec >Ht1 //
135 |lapply (eqb_false_to_not_eq … Hij) #Hneq >Ht2 >nth_change_vec_neq [2://]
136 >Ht3 >nth_change_vec_neq //
138 |#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in ⊢ (%→?); *
139 #Hcx #Heqtx #Htx #ls #c #c1 #rs #Ht1
140 >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
141 >Ht3 in Hcx; >nth_change_vec [2:@le_S_S //] #Hcx lapply (Hcx ? (refl ??))
142 #Htest % // @(eq_vec … (niltape ?))
143 #j #lejn cases (true_or_false (eqb i j)) #Hij
144 [lapply lejn <(eqb_true_to_eq … Hij) #lein >Htx >nth_change_vec [2://]
145 >Heqtx >Ht3 >nth_change_vec >Ht1 //
146 |lapply (eqb_false_to_not_eq … Hij) #Hneq >Htx >nth_change_vec_neq [2://]
147 >Heqtx >Ht3 >nth_change_vec_neq //
151 (* advance in parallel along two tapes src and dst until we reach the end
154 definition parmove ≝ λsrc,dst,sig,n,D.
155 whileTM … (parmove_step src dst sig n D) parmove1.
157 definition R_parmoveL ≝
158 λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
160 nth src ? int (niltape ?) = midtape sig xs x rs →
161 ∀ls0,x0,target,rs0.|xs| = |target| →
162 nth dst ? int (niltape ?) = midtape sig (target@ls0) x0 rs0 →
164 (change_vec ?? int (mk_tape sig [] (None ?) (reverse ? xs@x::rs)) src)
165 (mk_tape sig (tail ? ls0) (option_hd ? ls0) (reverse ? target@x0::rs0)) dst) ∧
167 nth dst ? int (niltape ?) = midtape sig xs x rs →
168 ∀ls0,x0,target,rs0.|xs| = |target| →
169 nth src ? int (niltape ?) = midtape sig (target@ls0) x0 rs0 →
171 (change_vec ?? int (mk_tape sig [] (None ?) (reverse ? xs@x::rs)) dst)
172 (mk_tape sig (tail ? ls0) (option_hd ? ls0) (reverse ? target@x0::rs0)) src) ∧
173 ((current ? (nth src ? int (niltape ?)) = None ? ∨
174 current ? (nth dst ? int (niltape ?)) = None ?) →
177 lemma wsem_parmoveL : ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
178 parmove src dst sig n L ⊫ R_parmoveL src dst sig n.
179 #src #dst #sig #n #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
180 lapply (sem_while … (sem_parmove_step src dst sig n L Hneq Hsrc Hdst) … Hloop) //
181 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
182 [ whd in ⊢ (%→?); * #H #Houtc % [2: #_ @Houtc ] cases H #Hcurtb
184 [ #x #xs #rs #Hsrctb >Hsrctb in Hcurtb; normalize in ⊢ (%→?);
185 #Hfalse destruct (Hfalse)
186 | #x #xs #rs #Hdsttb #ls0 #x0 #target #rs0 #Hlen #Hsrctb >Hsrctb in Hcurtb;
187 normalize in ⊢ (%→?); #H destruct (H)
190 [ #x #xs #rs #Hsrctb #ls0 #x0 #target
191 #rs0 #Hlen #Hdsttb >Hdsttb in Hcurtb; normalize in ⊢ (%→?); #H destruct (H)
192 | #x #xs #rs #Hdsttb >Hdsttb in Hcurtb; normalize in ⊢ (%→?);
193 #Hfalse destruct (Hfalse)
196 | #td #te * #c0 * #c1 * * #Hc0 #Hc1 #Hd #Hstar #IH #He
197 lapply (IH He) -IH * * #IH1a #IH1b #IH2 % [ %
198 [ #x #xs #rs #Hsrc_td #ls0 #x0 #target
200 >Hsrc_td in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
201 >Hdst_td in Hd; >Hsrc_td @(list_cases2 … Hlen)
202 [ #Hxsnil #Htargetnil >Hxsnil >Htargetnil #Hd >IH2
203 [2: %1 >Hd >nth_change_vec_neq [|@(sym_not_eq … Hneq)]
205 >Hd -Hd @(eq_vec … (niltape ?))
206 #i #Hi cases (decidable_eq_nat i src) #Hisrc
207 [ >Hisrc >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
209 >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
211 | cases (decidable_eq_nat i dst) #Hidst
212 [ >Hidst >nth_change_vec // >nth_change_vec //
213 >Hdst_td in Hc1; >Htargetnil
214 normalize in ⊢ (%→?); #Hc1 destruct (Hc1) cases ls0 //
215 | >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
216 >nth_change_vec_neq [|@(sym_not_eq … Hisrc)]
217 >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
218 >nth_change_vec_neq [|@(sym_not_eq … Hisrc)] %
221 | #hd1 #hd2 #tl1 #tl2 #Hxs #Htarget >Hxs >Htarget #Hd
222 >(IH1a hd1 tl1 (c0::rs) ? ls0 hd2 tl2 (x0::rs0))
223 [ >Hd >(change_vec_commute … ?? td ?? src dst) //
224 >change_vec_change_vec
225 >(change_vec_commute … ?? td ?? dst src) [|@sym_not_eq //]
226 >change_vec_change_vec
227 >reverse_cons >associative_append
228 >reverse_cons >associative_append %
229 | >Hd >nth_change_vec //
230 | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
231 | >Hd >nth_change_vec_neq [|@sym_not_eq //]
234 | #x #xs #rs #Hdst_td #ls0 #x0 #target
236 >Hdst_td in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
237 >Hsrc_td in Hd; >Hdst_td @(list_cases2 … Hlen)
238 [ #Hxsnil #Htargetnil >Hxsnil >Htargetnil #Hd >IH2
239 [2: %2 >Hd >nth_change_vec //]
240 >Hd -Hd @(eq_vec … (niltape ?))
241 #i #Hi cases (decidable_eq_nat i dst) #Hidst
242 [ >Hidst >(nth_change_vec_neq … dst src) //
243 >nth_change_vec // >nth_change_vec //
244 | cases (decidable_eq_nat i src) #Hisrc
245 [ >Hisrc >nth_change_vec // >(nth_change_vec_neq …) [|@sym_not_eq //]
246 >Hsrc_td in Hc1; >Htargetnil
247 normalize in ⊢ (%→?); #Hc1 destruct (Hc1) >nth_change_vec //
249 | >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
250 >nth_change_vec_neq [|@(sym_not_eq … Hisrc)]
251 >nth_change_vec_neq [|@(sym_not_eq … Hisrc)]
252 >nth_change_vec_neq [|@(sym_not_eq … Hidst)] %
255 | #hd1 #hd2 #tl1 #tl2 #Hxs #Htarget >Hxs >Htarget #Hd
256 >(IH1b hd1 tl1 (x::rs) ? ls0 hd2 tl2 (x0::rs0))
257 [ >Hd >(change_vec_commute … ?? td ?? dst src) [|@sym_not_eq //]
258 >change_vec_change_vec
259 >(change_vec_commute … ?? td ?? src dst) //
260 >change_vec_change_vec
261 >reverse_cons >associative_append
262 >reverse_cons >associative_append
263 >change_vec_commute [|@sym_not_eq //] %
264 | >Hd >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
265 | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
266 | >Hd >nth_change_vec // ]
269 | >Hc0 >Hc1 * [ #Hc0 destruct (Hc0) | #Hc1 destruct (Hc1) ]
273 lemma terminate_parmoveL : ∀src,dst,sig,n,t.
274 src ≠ dst → src < S n → dst < S n →
275 parmove src dst sig n L ↓ t.
276 #src #dst #sig #n #t #Hneq #Hsrc #Hdst
277 @(terminate_while … (sem_parmove_step …)) //
278 <(change_vec_same … t src (niltape ?))
279 cases (nth src (tape sig) t (niltape ?))
280 [ % #t1 * #x1 * #x2 * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
281 |2,3: #a0 #al0 % #t1 * #x1 * #x2 * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
282 | #ls lapply t -t elim ls
283 [#t #c #rs % #t1 * #x1 * #x2 * * >nth_change_vec // normalize in ⊢ (%→?);
284 #H1 destruct (H1) #Hcurdst >change_vec_change_vec #Ht1 %
285 #t2 * #y1 * #y2 * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
286 >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H)
287 |#l0 #ls0 #IH #t #c #rs % #t1 * #x1 * #x2 * * >nth_change_vec //
288 normalize in ⊢ (%→?); #H destruct (H) #Hcurdst
289 >change_vec_change_vec >change_vec_commute // #Ht1 >Ht1 @IH
294 lemma sem_parmoveL : ∀src,dst,sig,n.
295 src ≠ dst → src < S n → dst < S n →
296 parmove src dst sig n L ⊨ R_parmoveL src dst sig n.
297 #src #dst #sig #n #Hneq #Hsrc #Hdst @WRealize_to_Realize
298 [/2/ | @wsem_parmoveL //]
302 definition compare ≝ λi,j,sig,n.
303 whileTM … (compare_step i j sig n) comp1.
305 (* (∃rs'.rs = rs0@rs' ∧ current ? (nth j ? outt (niltape ?)) = None ?) ∨
306 (∃rs0'.rs0 = rs@rs0' ∧
309 (mk_tape sig (reverse sig rs@x::ls) (None sig) []) i)
310 (mk_tape sig (reverse sig rs@x::ls0) (option_hd sig rs0')
311 (tail sig rs0')) j) ∨
312 (∃xs,ci,cj,rs',rs0'.ci ≠ cj ∧ rs = xs@ci::rs' ∧ rs0 = xs@cj::rs0' ∧
314 (change_vec ?? int (midtape sig (reverse ? xs@x::ls) ci rs') i)
315 (midtape sig (reverse ? xs@x::ls0) cj rs0') j)).*)
316 definition R_compare ≝
317 λi,j,sig,n.λint,outt: Vector (tape sig) (S n).
318 ((current ? (nth i ? int (niltape ?)) ≠ current ? (nth j ? int (niltape ?)) ∨
319 current ? (nth i ? int (niltape ?)) = None ? ∨
320 current ? (nth j ? int (niltape ?)) = None ?) → outt = int) ∧
322 (* nth i ? int (niltape ?) = midtape sig ls x (xs@ci::rs) → *)
323 nth i ? int (niltape ?) = midtape sig ls x rs →
324 nth j ? int (niltape ?) = midtape sig ls0 x rs0 →
328 (mk_tape sig (reverse sig rs0@x::ls) (option_hd sig rs') (tail ? rs')) i)
329 (mk_tape sig (reverse sig rs0@x::ls0) (None ?) [ ]) j) ∨
330 (∃rs0'.rs0 = rs@rs0' ∧
333 (mk_tape sig (reverse sig rs@x::ls) (None sig) []) i)
334 (mk_tape sig (reverse sig rs@x::ls0) (option_hd sig rs0')
335 (tail sig rs0')) j) ∨
336 (∃xs,ci,cj,rs',rs0'.ci ≠ cj ∧ rs = xs@ci::rs' ∧ rs0 = xs@cj::rs0' ∧
338 (change_vec ?? int (midtape sig (reverse ? xs@x::ls) ci rs') i)
339 (midtape sig (reverse ? xs@x::ls0) cj rs0') j)).
341 lemma wsem_compare : ∀i,j,sig,n.i ≠ j → i < S n → j < S n →
342 compare i j sig n ⊫ R_compare i j sig n.
343 #i #j #sig #n #Hneq #Hi #Hj #ta #k #outc #Hloop
344 lapply (sem_while … (sem_comp_step i j sig n Hneq Hi Hj) … Hloop) //
345 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
346 [ whd in ⊢ (%→?); * * [ *
349 | #ls #x #rs #ls0 #rs0 #Hnthi #Hnthj
350 >Hnthi in Hcicj; >Hnthj normalize in ⊢ (%→?); * #H @False_ind @H %
354 | #ls #x #rs #ls0 #rs0 #Hnthi >Hnthi in Hci;
355 normalize in ⊢ (%→?); #H destruct (H) ] ]
358 | #ls #x #rs #ls0 #rs0 #_ #Hnthj >Hnthj in Hcj;
359 normalize in ⊢ (%→?); #H destruct (H) ] ]
360 | #td #te * #x * * #Hci #Hcj #Hd #Hstar #IH #He lapply (IH He) -IH *
363 [ * #H @False_ind @H % | #H destruct (H)] | #H destruct (H)]
364 | #ls #c0 #rs #ls0 #rs0 cases rs
365 [ -IH2 #Hnthi #Hnthj % %2 %{rs0} % [%]
366 >Hnthi in Hd; #Hd >Hd in IH1; #IH1 >IH1
367 [| % %2 >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec // % ]
368 >Hnthj cases rs0 [| #r1 #rs1 ] %
369 | #r1 #rs1 #Hnthi cases rs0
370 [ -IH2 #Hnthj % % %{(r1::rs1)} % [%]
371 >Hnthj in Hd; #Hd >Hd in IH1; #IH1 >IH1
372 [| %2 >nth_change_vec // ]
374 | #r2 #rs2 #Hnthj lapply IH2; >Hd in IH1; >Hnthi >Hnthj
376 >nth_change_vec_neq [| @sym_not_eq // ] >nth_change_vec //
377 cases (true_or_false (r1 == r2)) #Hr1r2
378 [ >(\P Hr1r2) #_ #IH2 cases (IH2 … (refl ??) (refl ??)) [ *
379 [ * #rs' * #Hrs1 #Hcurout_j % % %{rs'}
382 | >Hcurout_j >change_vec_commute // >change_vec_change_vec
383 >change_vec_commute // @sym_not_eq // ]
384 | * #rs0' * #Hrs2 #Hcurout_i % %2 %{rs0'}
385 >Hrs2 >Hcurout_i % //
386 >change_vec_commute // >change_vec_change_vec
387 >change_vec_commute [|@sym_not_eq//] >change_vec_change_vec
388 >reverse_cons >associative_append >associative_append % ]
389 | * #xs * #ci * #cj * #rs' * #rs0' * * * #Hcicj #Hrs1 #Hrs2
390 >change_vec_commute // >change_vec_change_vec
391 >change_vec_commute [| @sym_not_eq ] // >change_vec_change_vec
392 #Houtc %2 %{(r2::xs)} %{ci} %{cj} %{rs'} %{rs0'}
393 % [ % [ % [ // | >Hrs1 // ] | >Hrs2 // ]
394 | >reverse_cons >associative_append >associative_append >Houtc % ] ]
395 | lapply (\Pf Hr1r2) -Hr1r2 #Hr1r2 #IH1 #_ %2
396 >IH1 [| % % normalize @(not_to_not … Hr1r2) #H destruct (H) % ]
397 %{[]} %{r1} %{r2} %{rs1} %{rs2} % [ % [ % /2/ | % ] | % ] ]]]]]
400 lemma terminate_compare : ∀i,j,sig,n,t.
401 i ≠ j → i < S n → j < S n →
402 compare i j sig n ↓ t.
403 #i #j #sig #n #t #Hneq #Hi #Hj
404 @(terminate_while … (sem_comp_step …)) //
405 <(change_vec_same … t i (niltape ?))
406 cases (nth i (tape sig) t (niltape ?))
407 [ % #t1 * #x * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
408 |2,3: #a0 #al0 % #t1 * #x * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
409 | #ls #c #rs lapply c -c lapply ls -ls lapply t -t elim rs
410 [#t #ls #c % #t1 * #x * * >nth_change_vec // normalize in ⊢ (%→?);
411 #H1 destruct (H1) #_ >change_vec_change_vec #Ht1 %
412 #t2 * #x0 * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
413 >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H)
414 |#r0 #rs0 #IH #t #ls #c % #t1 * #x * * >nth_change_vec //
415 normalize in ⊢ (%→?); #H destruct (H) #Hcur
416 >change_vec_change_vec >change_vec_commute // #Ht1 >Ht1 @IH
421 lemma sem_compare : ∀i,j,sig,n.
422 i ≠ j → i < S n → j < S n →
423 compare i j sig n ⊨ R_compare i j sig n.
424 #i #j #sig #n #Hneq #Hi #Hj @WRealize_to_Realize
425 [/2/| @wsem_compare // ]
430 definition copy ≝ λsrc,dst,sig,n.
431 whileTM … (copy_step src dst sig n) copy1.
434 λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
435 ((current ? (nth src ? int (niltape ?)) = None ? ∨
436 current ? (nth dst ? int (niltape ?)) = None ?) → outt = int) ∧
437 (∀ls,x,x0,rs,ls0,rs0.
438 nth src ? int (niltape ?) = midtape sig ls x rs →
439 nth dst ? int (niltape ?) = midtape sig ls0 x0 rs0 →
440 (∃rs01,rs02.rs0 = rs01@rs02 ∧ |rs01| = |rs| ∧
443 (mk_tape sig (reverse sig rs@x::ls) (None sig) []) src)
444 (mk_tape sig (reverse sig rs@x::ls0) (option_hd sig rs02)
445 (tail sig rs02)) dst) ∨
446 (∃rs1,rs2.rs = rs1@rs2 ∧ |rs1| = |rs0| ∧
449 (mk_tape sig (reverse sig rs1@x::ls) (option_hd sig rs2)
451 (mk_tape sig (reverse sig rs1@x::ls0) (None sig) []) dst)).
453 lemma wsem_copy : ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
454 copy src dst sig n ⊫ R_copy src dst sig n.
455 #src #dst #sig #n #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
456 lapply (sem_while … (sem_copy_step src dst sig n Hneq Hsrc Hdst) … Hloop) //
457 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
458 [ whd in ⊢ (%→?); * #Hnone #Hout %
460 |#ls #x #x0 #rs #ls0 #rs0 #Hsrc1 #Hdst1 @False_ind cases Hnone
461 [>Hsrc1 normalize #H destruct (H) | >Hdst1 normalize #H destruct (H)]
463 |#tc #td * #x * #y * * #Hcx #Hcy #Htd #Hstar #IH #He lapply (IH He) -IH *
465 [* [>Hcx #H destruct (H) | >Hcy #H destruct (H)]
466 |#ls #x' #y' #rs #ls0 #rs0 #Hnth_src #Hnth_dst
467 >Hnth_src in Hcx; whd in ⊢ (??%?→?); #H destruct (H)
468 >Hnth_dst in Hcy; whd in ⊢ (??%?→?); #H destruct (H)
469 >Hnth_src in Htd; >Hnth_dst -Hnth_src -Hnth_dst
471 [(* the source tape is empty after the move *)
473 [%1 >Htd >nth_change_vec_neq [2:@(not_to_not … Hneq) //] >nth_change_vec //]
474 #Hout (* whd in match (tape_move ???); *) %1 %{([])} %{rs0} %
476 |whd in match (reverse ??); whd in match (reverse ??);
477 >Hout >Htd @eq_f2 // cases rs0 //
480 [(* the dst tape is empty after the move *)
481 #Htd lapply (IH1 ?) [%2 >Htd >nth_change_vec //]
482 #Hout (* whd in match (tape_move ???); *) %2 %{[ ]} %{(c1::tl1)} %
484 |whd in match (reverse ??); whd in match (reverse ??);
487 |#c2 #tl2 whd in match (tape_move_mono ???); whd in match (tape_move_mono ???);
489 cut (nth src (tape sig) td (niltape sig)=midtape sig (x::ls) c1 tl1)
490 [>Htd >nth_change_vec_neq [2:@(not_to_not … Hneq) //] @nth_change_vec //]
492 cut (nth dst (tape sig) td (niltape sig)=midtape sig (x::ls0) c2 tl2)
493 [>Htd @nth_change_vec //]
494 #Hdst_td cases (IH2 … Hsrc_td Hdst_td) -Hsrc_td -Hdst_td
495 [* #rs01 * #rs02 * * #H1 #H2 #H3 %1
496 %{(c2::rs01)} %{rs02} % [% [@eq_f //|normalize @eq_f @H2]]
497 >Htd in H3; >change_vec_commute // >change_vec_change_vec
498 >change_vec_commute [2:@(not_to_not … Hneq) //] >change_vec_change_vec
499 #H >reverse_cons >associative_append >associative_append @H
500 |* #rs11 * #rs12 * * #H1 #H2 #H3 %2
501 %{(c1::rs11)} %{rs12} % [% [@eq_f //|normalize @eq_f @H2]]
502 >Htd in H3; >change_vec_commute // >change_vec_change_vec
503 >change_vec_commute [2:@(not_to_not … Hneq) //] >change_vec_change_vec
504 #H >reverse_cons >associative_append >associative_append @H
512 lemma terminate_copy : ∀src,dst,sig,n,t.
513 src ≠ dst → src < S n → dst < S n → copy src dst sig n ↓ t.
514 #src #dst #sig #n #t #Hneq #Hsrc #Hdts
515 @(terminate_while … (sem_copy_step …)) //
516 <(change_vec_same … t src (niltape ?))
517 cases (nth src (tape sig) t (niltape ?))
518 [ % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
519 |2,3: #a0 #al0 % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
520 | #ls #c #rs lapply c -c lapply ls -ls lapply t -t elim rs
521 [#t #ls #c % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?);
522 #H1 destruct (H1) #_ >change_vec_change_vec #Ht1 %
523 #t2 * #x0 * #y0 * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
524 >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H)
525 |#r0 #rs0 #IH #t #ls #c % #t1 * #x * #y * * >nth_change_vec //
526 normalize in ⊢ (%→?); #H destruct (H) #Hcur
527 >change_vec_change_vec >change_vec_commute // #Ht1 >Ht1 @IH
532 lemma sem_copy : ∀src,dst,sig,n.
533 src ≠ dst → src < S n → dst < S n →
534 copy src dst sig n ⊨ R_copy src dst sig n.
535 #i #j #sig #n #Hneq #Hi #Hj @WRealize_to_Realize [/2/| @wsem_copy // ]