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 (* vec is a coercion. Why should I insert it? *)
8 definition mti_step ≝ λsig:FinSet.λn,i.
9 ifTM (multi_sig sig n) (test_char ? (λc:multi_sig sig n.¬(nth i ? (vec … c) (blank ?))==blank ?))
10 (single_finalTM … (ncombf_r (multi_sig sig n) (shift_i sig n i) (all_blank sig n)))
13 definition Rmti_step_true ≝
15 ∃b:multi_sig sig n. (nth i ? (vec … b) (blank ?) ≠ blank ?) ∧
17 t1 = midtape (multi_sig sig n) ls b (a::rs) ∧
18 t2 = midtape (multi_sig sig n) ((shift_i sig n i b a)::ls) a rs) ∨
20 t1 = midtape ? ls b [] ∧
21 t2 = rightof ? (shift_i sig n i b (all_blank sig n)) ls)).
23 (* 〈combf0,all_blank sig n〉 *)
24 definition Rmti_step_false ≝
26 (∀ls,b,rs. t1 = midtape (multi_sig sig n) ls b rs →
27 (nth i ? (vec … b) (blank ?) = blank ?)) ∧ t2 = t1.
32 [inr … (inl … (inr … start_nop)): Rmti_step_true sig n i, Rmti_step_false sig n i].
34 @(acc_sem_if_app (multi_sig sig n) ??????????
35 (sem_test_char …) (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
36 (sem_nop (multi_sig sig n)))
37 [#intape #outtape #tapea whd in ⊢ (%→%→%); * * #c *
38 #Hcur cases (current_to_midtape … Hcur) #ls * #rs #Hintape
39 #ctest #Htapea * #Hout1 #Hout2 @(ex_intro … c) %
40 [@(\Pf (injective_notb … )) @ctest]
41 generalize in match Hintape; -Hintape cases rs
42 [#Hintape %2 @(ex_intro …ls) % // @Hout1 >Htapea @Hintape
44 @(ex_intro … ls) @(ex_intro … a) @(ex_intro … rs1) % //
45 @Hout2 >Htapea @Hintape
47 |#intape #outtape #tapea whd in ⊢ (%→%→%);
48 * #Htest #tapea #outtape
50 #intape lapply (Htest b ?) [>intape //] -Htest #Htest
51 lapply (injective_notb ? true Htest) -Htest #Htest @(\P Htest)
55 (* move tape i machine *)
57 λsig,n,i.whileTM (multi_sig sig n) (mti_step sig n i) (inr … (inl … (inr … start_nop))).
59 axiom daemon: ∀P:Prop.P.
63 (∀a,rs. t1 = rightof ? a rs → t2 = t1) ∧
65 t1 = midtape (multi_sig sig n) ls a rs →
66 (nth i ? (vec … a) (blank ?) = blank ? ∧ t2 = t1) ∨
69 nth i ? (vec … b) (blank ?) = (blank ?) ∧
70 (∀x. mem ? x (a::rs1) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
71 shift_l sig n i (a::rs1) rss ∧
72 t2 = midtape (multi_sig sig n) ((reverse ? rss)@ls) b rs2) ∨
74 (∀x. mem ? x (a::rs) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
75 shift_l sig n i (a::rs) (rss@[b]) ∧
76 t2 = rightof (multi_sig sig n) (shift_i sig n i b (all_blank sig n))
77 ((reverse ? rss)@ls)))).
81 WRealize (multi_sig sig n) (mti sig n i) (R_mti sig n i).
82 #sig #n #i #inc #j #outc #Hloop
83 lapply (sem_while … (sem_mti_step sig n i) inc j outc Hloop) [%]
84 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
85 [ whd in ⊢ (% → ?); * #H1 #H2 %
87 |#a #ls #rs #Htapea % % [@(H1 … Htapea) |@H2]
89 | #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
90 lapply (IH HRfalse) -IH -HRfalse whd in ⊢ (%→%);
92 [#b0 #ls #Htapeb cases Hstar1 #b * #_ *
93 [* #ls0 * #a * #rs0 * >Htapeb #H destruct (H)
94 |* #ls0 * >Htapeb #H destruct (H)
96 |#b0 #ls #rs #Htapeb cases Hstar1 #b * #btest *
97 [* #ls1 * #a * #rs1 * >Htapeb #H destruct (H) #Htapec
98 %2 cases (IH2 … Htapec)
101 %{[ ]} %{a} %{rs1} %{[shift_i sig n i b a]} %
102 [%[%[% // |#x #Hb >(mem_single ??? Hb) // ]
104 |>Hout >reverse_single @Htapec
107 [ (* case a \= None and exists b = None *) -IH1 -IH2 #IH
108 %1 cases IH -IH #rs10 * #b0 * #rs2 * #rss * * * *
110 %{(a::rs10)} %{b0} %{rs2} %{(shift_i sig n i b a::rss)}
112 |#x * [#eqxa >eqxa (*?? *) @daemon|@H3]]
114 |>H5 >reverse_cons >associative_append //
116 | (* case a \= None and we reach the end of the (full) tape *) -IH1 -IH2 #IH
117 %2 cases IH -IH #b0 * #rss * * #H1 #H2 #H3
118 %{b0} %{(shift_i sig n i b a::rss)}
119 %[%[#x * [#eqxb >eqxb @btest|@H1]
121 |>H3 >reverse_cons >associative_append //
125 |(* b \= None but the left tape is empty *)
126 * #ls0 * >Htapeb #H destruct (H) #Htapec
128 %[%[#x * [#eqxb >eqxb @btest|@False_ind]
129 |@daemon (*shift of dingle char OK *)]
130 |>(IH1 … Htapec) >Htapec //
135 lemma WF_mti_niltape:
136 ∀sig,n,i. WF ? (inv ? (Rmti_step_true sig n i)) (niltape ?).
137 #sig #n #i @wf #t1 whd in ⊢ (%→?); * #b * #_ *
138 [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
141 lemma WF_mti_rightof:
142 ∀sig,n,i,a,ls. WF ? (inv ? (Rmti_step_true sig n i)) (rightof ? a ls).
143 #sig #n #i #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ *
144 [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
148 ∀sig,n,i,a,ls. WF ? (inv ? (Rmti_step_true sig n i)) (leftof ? a ls).
149 #sig #n #i #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ *
150 [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
154 ∀sig,n,i.∀t. Terminate ? (mti sig n i) t.
155 #sig #n #i #t @(terminate_while … (sem_mti_step sig n i)) [%]
156 cases t // #ls #c #rs lapply c -c lapply ls -ls elim rs
157 [#ls #c @wf #t1 whd in ⊢ (%→?); * #b * #_ *
158 [* #ls1 * #a * #rs1 * #H destruct
159 |* #ls1 * #H destruct #Ht1 >Ht1 //
161 |#a #rs1 #Hind #ls #c @wf #t1 whd in ⊢ (%→?); * #b * #_ *
162 [* #ls1 * #a2 * #rs2 * #H destruct (H) #Ht1 >Ht1 //
163 |* #ls1 * #H destruct
168 lemma ssem_mti: ∀sig,n,i.
169 Realize ? (mti sig n i) (R_mti sig n i).