1 include "turing/basic_machines.ma".
2 include "turing/if_machine.ma".
3 include "turing/multi_to_mono/trace_alphabet.ma".
5 (* a machine that shift the i trace r starting from the bord of the trace *)
7 (* (λc.¬(nth i ? (vec … c) (blank ?))==blank ?)) *)
8 (* vec is a coercion. Why should I insert it? *)
9 definition mti_step ≝ λsig:FinSet.λn,i.
10 ifTM (multi_sig sig n) (test_char ? (not_blank sig n i))
12 (ncombf_r (multi_sig sig n) (shift_i sig n i) (all_blanks sig n)))
15 definition Rmti_step_true ≝
17 ∃b:multi_sig sig n. (nth i ? (vec … b) (blank ?) ≠ blank ?) ∧
19 t1 = midtape (multi_sig sig n) ls b (a::rs) ∧
20 t2 = midtape (multi_sig sig n) ((shift_i sig n i b a)::ls) a rs) ∨
22 t1 = midtape ? ls b [] ∧
23 t2 = rightof ? (shift_i sig n i b (all_blanks sig n)) ls)).
25 (* 〈combf0,all_blank sig n〉 *)
26 definition Rmti_step_false ≝
28 (∀ls,b,rs. t1 = midtape (multi_sig sig n) ls b rs →
29 (nth i ? (vec … b) (blank ?) = blank ?)) ∧ t2 = t1.
34 [inr … (inl … (inr … start_nop)): Rmti_step_true sig n i, Rmti_step_false sig n i].
36 @(acc_sem_if_app (multi_sig sig n) … (sem_test_char …)
37 (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blanks sig n))
38 (sem_nop (multi_sig sig n)))
39 [#intape #outtape #tapea whd in ⊢ (%→%→%); * * #c *
40 #Hcur cases (current_to_midtape … Hcur) #ls * #rs #Hintape
41 #ctest #Htapea * #Hout1 #Hout2 @(ex_intro … c) %
42 [@(\Pf (injective_notb … )) @ctest]
43 generalize in match Hintape; -Hintape cases rs
44 [#Hintape %2 @(ex_intro …ls) % // @Hout1 >Htapea @Hintape
46 @(ex_intro … ls) @(ex_intro … a) @(ex_intro … rs1) % //
47 @Hout2 >Htapea @Hintape
49 |#intape #outtape #tapea whd in ⊢ (%→%→%);
50 * #Htest #tapea #outtape
52 #intape lapply (Htest b ?) [>intape //] -Htest #Htest
53 lapply (injective_notb ? true Htest) -Htest #Htest @(\P Htest)
57 (* move tape i machine *)
59 λsig,n,i.whileTM (multi_sig sig n) (mti_step sig n i) (inr … (inl … (inr … start_nop))).
61 axiom daemon: ∀P:Prop.P.
63 definition R_mti ≝ λsig,n,i,t1,t2.
64 (∀a,rs. t1 = rightof ? a rs → t2 = t1) ∧
66 t1 = midtape (multi_sig sig n) ls a rs →
67 (nth i ? (vec … a) (blank ?) = blank ? ∧ t2 = t1) ∨
70 nth i ? (vec … b) (blank ?) = (blank ?) ∧
71 (∀x. mem ? x (a::rs1) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
72 shift_l sig n i (a::rs1) rss ∧
73 t2 = midtape (multi_sig sig n) ((reverse ? rss)@ls) b rs2) ∨
75 (∀x. mem ? x (a::rs) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
76 shift_l sig n i (a::rs) (rss@[b]) ∧
77 t2 = rightof (multi_sig sig n) (shift_i sig n i b (all_blanks sig n))
78 ((reverse ? rss)@ls)))).
82 WRealize (multi_sig sig n) (mti sig n i) (R_mti sig n i).
83 #sig #n #i #inc #j #outc #Hloop
84 lapply (sem_while … (sem_mti_step sig n i) inc j outc Hloop) [%]
85 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
86 [ whd in ⊢ (% → ?); * #H1 #H2 %
88 |#a #ls #rs #Htapea % % [@(H1 … Htapea) |@H2]
90 | #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
91 lapply (IH HRfalse) -IH -HRfalse whd in ⊢ (%→%);
93 [#b0 #ls #Htapeb cases Hstar1 #b * #_ *
94 [* #ls0 * #a * #rs0 * >Htapeb #H destruct (H)
95 |* #ls0 * >Htapeb #H destruct (H)
97 |#b0 #ls #rs #Htapeb cases Hstar1 #b * #btest *
98 [* #ls1 * #a * #rs1 * >Htapeb #H destruct (H) #Htapec
99 %2 cases (IH2 … Htapec)
102 %{[ ]} %{a} %{rs1} %{[shift_i sig n i b a]} %
103 [%[%[% // |#x #Hb >(mem_single ??? Hb) // ]
105 |>Hout >reverse_single @Htapec
108 [ (* case a \= None and exists b = None *) -IH1 -IH2 #IH
109 %1 cases IH -IH #rs10 * #b0 * #rs2 * #rss * * * *
111 %{(a::rs10)} %{b0} %{rs2} %{(shift_i sig n i b a::rss)}
113 |#x * [#eqxa >eqxa (*?? *) @daemon|@H3]]
115 |>H5 >reverse_cons >associative_append //
117 | (* case a \= None and we reach the end of the (full) tape *) -IH1 -IH2 #IH
118 %2 cases IH -IH #b0 * #rss * * #H1 #H2 #H3
119 %{b0} %{(shift_i sig n i b a::rss)}
120 %[%[#x * [#eqxb >eqxb @btest|@H1]
122 |>H3 >reverse_cons >associative_append //
126 |(* b \= None but the left tape is empty *)
127 * #ls0 * >Htapeb #H destruct (H) #Htapec
129 %[%[#x * [#eqxb >eqxb @btest|@False_ind]
130 |@daemon (*shift of dingle char OK *)]
131 |>(IH1 … Htapec) >Htapec //
136 lemma WF_mti_niltape:
137 ∀sig,n,i. WF ? (inv ? (Rmti_step_true sig n i)) (niltape ?).
138 #sig #n #i @wf #t1 whd in ⊢ (%→?); * #b * #_ *
139 [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
142 lemma WF_mti_rightof:
143 ∀sig,n,i,a,ls. WF ? (inv ? (Rmti_step_true sig n i)) (rightof ? a ls).
144 #sig #n #i #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ *
145 [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
149 ∀sig,n,i,a,ls. WF ? (inv ? (Rmti_step_true sig n i)) (leftof ? a ls).
150 #sig #n #i #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ *
151 [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
155 ∀sig,n,i.∀t. Terminate ? (mti sig n i) t.
156 #sig #n #i #t @(terminate_while … (sem_mti_step sig n i)) [%]
157 cases t // #ls #c #rs lapply c -c lapply ls -ls elim rs
158 [#ls #c @wf #t1 whd in ⊢ (%→?); * #b * #_ *
159 [* #ls1 * #a * #rs1 * #H destruct
160 |* #ls1 * #H destruct #Ht1 >Ht1 //
162 |#a #rs1 #Hind #ls #c @wf #t1 whd in ⊢ (%→?); * #b * #_ *
163 [* #ls1 * #a2 * #rs2 * #H destruct (H) #Ht1 >Ht1 //
164 |* #ls1 * #H destruct
169 lemma ssem_mti: ∀sig,n,i.
170 Realize ? (mti sig n i) (R_mti sig n i).