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_____________________________________________________________*)
13 include "turing/universal/trans_to_tuples.ma".
14 include "turing/universal/uni_step.ma".
16 (* definition zero : ∀n.initN n ≝ λn.mk_Sig ?? 0 (le_O_n n). *)
18 record normalTM : Type[0] ≝
20 pos_no_states : (0 < no_states);
21 ntrans : trans_source no_states → trans_target no_states;
22 nhalt : initN no_states → bool
25 definition normalTM_to_TM ≝ λM:normalTM.
26 mk_TM FinBool (initN (no_states M))
27 (ntrans M) (mk_Sig ?? 0 (pos_no_states M)) (nhalt M).
29 coercion normalTM_to_TM.
31 definition nconfig ≝ λn. config FinBool (initN n).
34 definition normalTM ≝ λn,t,h.
35 λk:0<n.mk_TM FinBool (initN n) t (mk_Sig ?? 0 k) h. *)
37 definition low_config: ∀M:normalTM.nconfig (no_states M) → tape STape ≝
39 let n ≝ no_states M in
43 let q_low ≝ m_bits_of_state n h q in
44 let current_low ≝ match current … (ctape … c) with [ None ⇒ null | Some b ⇒ bit b] in
45 let low_left ≝ map … (λb.〈bit b,false〉) (left … (ctape …c)) in
46 let low_right ≝ map … (λb.〈bit b,false〉) (right … (ctape …c)) in
47 let table ≝ flatten ? (tuples_of_pairs n h (graph_enum ?? t)) in
48 let right ≝ q_low@〈current_low,false〉::〈grid,false〉::table@〈grid,false〉::low_right in
49 mk_tape STape (〈grid,false〉::low_left) (option_hd … right) (tail … right).
51 lemma low_config_eq: ∀t,M,c. t = low_config M c →
52 ∃low_left,low_right,table,q_low_hd,q_low_tl,c_low.
53 low_left = map … (λb.〈bit b,false〉) (left … (ctape …c)) ∧
54 low_right = map … (λb.〈bit b,false〉) (right … (ctape …c)) ∧
55 table = flatten ? (tuples_of_pairs (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) ∧
56 〈q_low_hd,false〉::q_low_tl = m_bits_of_state (no_states M) (nhalt M) (cstate … c) ∧
57 c_low = match current … (ctape … c) with [ None ⇒ null| Some b ⇒ bit b] ∧
58 t = midtape STape (〈grid,false〉::low_left) 〈q_low_hd,false〉 (q_low_tl@〈c_low,false〉::〈grid,false〉::table@〈grid,false〉::low_right).
60 @(ex_intro … (map … (λb.〈bit b,false〉) (left … (ctape …c))))
61 @(ex_intro … (map … (λb.〈bit b,false〉) (right … (ctape …c))))
62 @(ex_intro … (flatten ? (tuples_of_pairs (no_states M) (nhalt M) (graph_enum ?? (ntrans M)))))
63 @(ex_intro … (\fst (hd ? (m_bits_of_state (no_states M) (nhalt M) (cstate … c)) 〈bit true,false〉)))
64 @(ex_intro … (tail ? (m_bits_of_state (no_states M) (nhalt M) (cstate … c))))
65 @(ex_intro … (match current … (ctape … c) with [ None ⇒ null| Some b ⇒ bit b]))
66 % [% [% [% [% // | // ] | // ] | // ] | >eqt //]
69 let rec to_bool_list (l: list (unialpha×bool)) ≝
74 [bit b ⇒ b::to_bool_list tl
79 definition high_c ≝ λc:unialpha×bool.
85 definition high_tape ≝ λls,c,rs.
86 mk_tape FinBool (to_bool_list ls) (high_c c) (to_bool_list rs).
88 lemma high_tape_eq : ∀ls,c,rs. high_tape ls c rs =
89 mk_tape FinBool (to_bool_list ls) (high_c c) (to_bool_list rs).
92 definition high_tape_from_tape ≝ λt:tape STape.
95 |leftof a l ⇒ match \fst a with
96 [bit b ⇒ leftof ? b (to_bool_list l)
99 |rightof a r ⇒ match \fst a with
100 [bit b ⇒ rightof ? b (to_bool_list r)
103 |midtape l c r ⇒ high_tape l c r
106 lemma high_tape_of_lift : ∀ls,c,rs. legal_tape ls c rs →
108 high_tape_from_tape (lift_tape ls c rs).
109 #ls * #c #b #rs * #H cases c //
111 * [ * [#H @False_ind /2/
112 | #Heq >Heq cases rs // * #a #b1 #tl
113 whd in match (lift_tape ???); cases a //
115 |#Heq >Heq cases ls // * #a #b1 #tl
116 whd in match (lift_tape ???); cases a //
120 lemma bool_embedding: ∀l.
121 to_bool_list (map ?? (λb.〈bit b,false〉) l) = l.
122 #l elim l // #a #tl #Hind normalize @eq_f @Hind
125 lemma current_embedding: ∀c.
126 high_c (〈match c with [None ⇒ null | Some b ⇒ bit b],false〉) = c.
129 lemma tape_embedding: ∀ls,c,rs.
131 (map ?? (λb.〈bit b,false〉) ls)
132 (〈match c with [None ⇒ null | Some b ⇒ bit b],false〉)
133 (map ?? (λb.〈bit b,false〉) rs) = mk_tape ? ls c rs.
134 #ls #c #rs >high_tape_eq >bool_embedding >bool_embedding
138 definition high_move ≝ λc,mv.
140 [ bit b ⇒ Some ? 〈b,move_of_unialpha mv〉
144 (* lemma high_of_lift ≝ ∀ls,c,rs.
145 high_tape ls c rs = *)
147 definition map_move ≝
148 λc,mv.match c with [ null ⇒ None ? | _ ⇒ Some ? 〈c,false,move_of_unialpha mv〉 ].
150 (* axiom high_tape_move : ∀t1,ls,c,rs, c1,mv.
152 t1 = lift_tape ls c rs →
153 high_tape_from_tape (tape_move STape t1 (map_move c1 mv)) =
154 tape_move FinBool (high_tape_from_tape t1) (high_move c1 mv). *)
156 definition low_step_R_true ≝ λt1,t2.
158 ∀c: nconfig (no_states M).
159 t1 = low_config M c →
160 halt ? M (cstate … c) = false ∧
161 t2 = low_config M (step ? M c).
163 definition low_tape_aux : ∀M:normalTM.tape FinBool → tape STape ≝
165 let current_low ≝ match current … t with
166 [ None ⇒ None ? | Some b ⇒ Some ? 〈bit b,false〉] in
167 let low_left ≝ map … (λb.〈bit b,false〉) (left … t) in
168 let low_right ≝ map … (λb.〈bit b,false〉) (right … t) in
169 mk_tape STape low_left current_low low_right.
171 lemma left_of_low_tape: ∀M,t.
172 left ? (low_tape_aux M t) = map … (λb.〈bit b,false〉) (left … t).
176 lemma right_of_low_tape: ∀M,t.
177 right ? (low_tape_aux M t) = map … (λb.〈bit b,false〉) (right … t).
181 definition low_move ≝ λaction:option (bool × move).
184 |Some act ⇒ Some ? (〈〈bit (\fst act),false〉,\snd act〉)].
186 (* simulation lemma *)
187 lemma low_tape_move : ∀M,action,t.
188 tape_move STape (low_tape_aux M t) (low_move action) =
189 low_tape_aux M (tape_move FinBool t action).
191 * #b #mv #t cases mv cases t //
192 [#ls #c #rs cases ls //|#ls #c #rs cases rs //]
195 lemma left_of_lift: ∀ls,c,rs. left ? (lift_tape ls c rs) = ls.
196 #ls * #c #b #rs cases c // cases ls // cases rs //
199 lemma right_of_lift: ∀ls,c,rs. legal_tape ls c rs →
200 right ? (lift_tape ls c rs) = rs.
201 #ls * #c #b #rs * #_ cases c // cases ls cases rs // #a #tll #b #tlr
202 #H @False_ind cases H [* [#H1 /2/ |#H1 destruct] |#H1 destruct]
206 lemma current_of_lift: ∀ls,c,b,rs. legal_tape ls 〈c,b〉 rs →
207 current STape (lift_tape ls 〈c,b〉 rs) =
208 match c with [null ⇒ None ? | _ ⇒ Some ? 〈c,b〉].
209 #ls #c #b #rs cases c // whd in ⊢ (%→?); * #_
210 * [* [#Hnull @False_ind /2/ | #Hls >Hls whd in ⊢ (??%%); cases rs //]
211 |#Hrs >Hrs whd in ⊢ (??%%); cases ls //]
214 lemma current_of_lift_None: ∀ls,c,b,rs. legal_tape ls 〈c,b〉 rs →
215 current STape (lift_tape ls 〈c,b〉 rs) = None ? →
217 #ls #c #b #rs #Hlegal >(current_of_lift … Hlegal) cases c normalize
218 [#b #H destruct |// |3,4,5:#H destruct ]
221 lemma current_of_lift_Some: ∀ls,c,c1,rs. legal_tape ls c rs →
222 current STape (lift_tape ls c rs) = Some ? c1 →
224 #ls * #c #cb #b #rs #Hlegal >(current_of_lift … Hlegal) cases c normalize
225 [#b1 #H destruct // |#H destruct |3,4,5:#H destruct //]
228 lemma current_of_low_None: ∀M,t. current FinBool t = None ? →
229 current STape (low_tape_aux M t) = None ?.
230 #M #t cases t // #l #b #r whd in ⊢ ((??%?)→?); #H destruct
233 lemma current_of_low_Some: ∀M,t,b. current FinBool t = Some ? b →
234 current STape (low_tape_aux M t) = Some ? 〈bit b,false〉.
236 [#b whd in ⊢ ((??%?)→?); #H destruct
237 |#b #l #b1 whd in ⊢ ((??%?)→?); #H destruct
238 |#b #l #b1 whd in ⊢ ((??%?)→?); #H destruct
239 |#c #c1 #l #r whd in ⊢ ((??%?)→?); #H destruct %
243 lemma current_of_low:∀M,tape,ls,c,rs. legal_tape ls c rs →
244 lift_tape ls c rs = low_tape_aux M tape →
245 c = 〈match current … tape with
246 [ None ⇒ null | Some b ⇒ bit b], false〉.
247 #M #tape #ls * #c #cb #rs #Hlegal #Hlift
248 cut (current ? (lift_tape ls 〈c,cb〉 rs) = current ? (low_tape_aux M tape))
249 [@eq_f @Hlift] -Hlift #Hlift
250 cut (current … tape = None ? ∨ ∃b.current … tape = Some ? b)
251 [cases (current … tape) [%1 // | #b1 %2 /2/ ]] *
252 [#Hcurrent >Hcurrent normalize
253 >(current_of_low_None …Hcurrent) in Hlift; #Hlift
254 >(current_of_lift_None … Hlegal Hlift)
255 @eq_f cases Hlegal * * #Hmarks #_ #_ #_ @(Hmarks 〈c,cb〉) @memb_hd
256 |* #b #Hcurrent >Hcurrent normalize
257 >(current_of_low_Some …Hcurrent) in Hlift; #Hlift
258 @(current_of_lift_Some … Hlegal Hlift)
263 lemma current_of_low:∀M,tape,ls,c,rs. legal_tape ls c rs →
264 lift_tape ls c rs = low_tape_aux M tape →
265 c = 〈match current … tape with
266 [ None ⇒ null | Some b ⇒ bit b], false〉.
267 #M #tape #ls * #c #cb #rs * * #_ #H cases (orb_true_l … H)
268 [cases c [2,3,4,5: whd in ⊢ ((??%?)→?); #Hfalse destruct]
270 [whd in ⊢ ((??%%)→?); #H destruct
271 |#a #l whd in ⊢ ((??%%)→?); #H destruct
272 |#a #l whd in ⊢ ((??%%)→?); #H destruct
273 |#a #l #r whd in ⊢ ((??%%)→?); #H destruct //
276 [#b whd in ⊢ ((??%?)→?); #Hfalse destruct
277 |3,4,5:whd in ⊢ ((??%?)→?); #Hfalse destruct]
278 #_ * [* [#Habs @False_ind /2/
279 |#Hls >Hls whd in ⊢ ((??%%)→?); *)
282 (* sufficent conditions to have a low_level_config *)
283 lemma is_low_config: ∀ls,c,rs,M,s,tape,qhd,q_tl,table.
285 table = flatten ? (tuples_of_pairs (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) →
286 lift_tape ls c rs = low_tape_aux M tape →
287 〈qhd,false〉::q_tl = m_bits_of_state (no_states M) (nhalt M) s →
288 midtape STape (〈grid,false〉::ls)
290 (q_tl@c::〈grid,false〉::table@〈grid,false〉::rs) =
291 low_config M (mk_config ?? s tape).
292 #ls #c #rs #M #s #tape #qhd #q_tl #table #Hlegal #Htable
293 #Hlift #Hstate whd in match (low_config ??); <Hstate
295 [@eq_f <(left_of_lift ls c rs) >Hlift //
296 | cut (∀A.∀a,b:A.∀l1,l2. a::l1 = b::l2 → a=b)
297 [#A #a #b #l1 #l2 #H destruct (H) %] #Hcut
299 |@eq_f <(current_of_low … Hlegal Hlift) @eq_f @eq_f <Htable @eq_f @eq_f
300 <(right_of_lift ls c rs Hlegal) >Hlift @right_of_low_tape
304 lemma unistep_to_low_step: ∀t1,t2.
305 R_uni_step_true t1 t2 → low_step_R_true t1 t2.
306 #t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step * #n #posn #t #h * #qin #tape #eqt1
307 cases (low_config_eq … eqt1)
308 #low_left * #low_right * #table * #q_low_hd * #q_low_tl * #current_low
309 ***** #Hlow_left #Hlow_right #Htable #Hq_low #Hcurrent_low #Ht1
310 letin trg ≝ (t 〈qin,current ? tape〉)
311 letin qout_low ≝ (m_bits_of_state n h (\fst trg))
312 letin qout_low_hd ≝ (hd ? qout_low 〈bit true,false〉)
313 letin qout_low_tl ≝ (tail ? qout_low)
314 letin low_act ≝ (low_action (\snd (t 〈qin,current ? tape〉)))
315 letin low_cout ≝ (\fst low_act)
316 letin low_m ≝ (\snd low_act)
317 lapply (Huni_step n table q_low_hd (\fst qout_low_hd)
318 current_low low_cout low_left low_right q_low_tl qout_low_tl low_m … Ht1)
321 @(trans_to_match n h t 〈qin,current ? tape〉 … (refl …))
322 >Hq_low >Hcurrent_low whd in match (mk_tuple ?????);
323 >(eq_pair_fst_snd … (t …)) whd in ⊢ (??%?);
324 >(eq_pair_fst_snd … (low_action …)) %
328 -Ht1 #Huni_step lapply (Huni_step ? (refl …)) -Huni_step *
329 #q_low_head_false * #ls1 * #rs1 * #c2 * *
330 #Ht2 #Hlift #Hlegal %
331 [whd in ⊢ (??%?); >q_low_head_false in Hq_low;
332 whd in ⊢ ((???%)→?); generalize in match (h qin);
334 |>Ht2 whd in match (step FinBool ??);
335 whd in match (trans ???);
336 >(eq_pair_fst_snd … (t ?))
337 @is_low_config // >Hlift
338 <low_tape_move @eq_f2
339 [>Hlow_left >Hlow_right >Hcurrent_low whd in ⊢ (??%%);
340 cases (current …tape) [%] #b whd in ⊢ (??%%); %
341 |whd in match low_cout; whd in match low_m; whd in match low_act;
342 generalize in match (\snd (t ?)); * [%] * #b #mv
343 whd in ⊢ (??(?(???%)?)%); cases mv %
348 definition low_step_R_false ≝ λt1,t2.
350 ∀c: nconfig (no_states M).
351 t1 = low_config M c → halt ? M (cstate … c) = true ∧ t1 = t2.
353 definition low_R ≝ λM,qstart,R,t1,t2.
354 ∀tape1. t1 = low_config M (mk_config ?? qstart tape1) →
355 ∃q,tape2.R tape1 tape2 ∧
356 halt ? M q = true ∧ t2 = low_config M (mk_config ?? q tape2).
358 definition R_TM ≝ λsig.λM:TM sig.λq.λt1,t2.
360 loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (mk_config ?? q t1) = Some ? outc ∧
361 t2 = (ctape ?? outc).
364 definition universal_R ≝ λM,R,t1,t2.
368 t1 = low_config M (initc ? M tape1) ∧
369 ∃q.halt ? M q = true → t2 = low_config M (mk_config ?? q tape2).*)
371 axiom uni_step: TM STape.
372 axiom us_acc: states ? uni_step.
374 axiom sem_uni_step: accRealize ? uni_step us_acc low_step_R_true low_step_R_false.
376 definition universalTM ≝ whileTM ? uni_step us_acc.
378 theorem sem_universal: ∀M:normalTM. ∀qstart.
379 WRealize ? universalTM (low_R M qstart (R_TM FinBool M qstart)).
380 #M #q #intape #i #outc #Hloop
381 lapply (sem_while … sem_uni_step intape i outc Hloop)
383 * #ta * #Hstar generalize in match q; -q
384 @(star_ind_l ??????? Hstar)
385 [#tb #q0 whd in ⊢ (%→?); #Htb #tape1 #Htb1
386 cases (Htb … Htb1) -Htb #Hhalt #Htb
390 [ whd @(ex_intro … 1) @(ex_intro … (mk_config … q0 tape1))
391 % [|%] whd in ⊢ (??%?); >Hhalt %
395 |#tb #tc #td whd in ⊢ (%→?); #Htc #Hstar1 #IH
397 lapply (IH (\fst (trans ? M 〈q,current ? tape1〉)) Htd) -IH
398 #IH cases (Htc … Htb); -Htc #Hhaltq
399 whd in match (step FinBool ??); >(eq_pair_fst_snd ?? (trans ???))
400 #Htc change with (mk_config ????) in Htc:(???(??%));
401 cases (IH ? Htc) #q1 * #tape2 * * #HRTM #Hhaltq1 #Houtc
402 @(ex_intro … q1) @(ex_intro … tape2) %
404 [cases HRTM #k * #outc1 * #Hloop #Houtc1
405 @(ex_intro … (S k)) @(ex_intro … outc1) %
406 [>loop_S_false [2://] whd in match (step FinBool ??);
407 >(eq_pair_fst_snd ?? (trans ???)) @Hloop
416 lemma R_TM_to_R: ∀sig,M,R. ∀t1,t2.
417 WRealize sig M R → R_TM ? M (start ? M) t1 t2 → R t1 t2.
418 #sig #M #R #t1 #t2 whd in ⊢ (%→?); #HMR * #i * #outc *
419 #Hloop #Ht2 >Ht2 @(HMR … Hloop)
422 axiom WRealize_to_WRealize: ∀sig,M,R1,R2.
423 (∀t1,t2.R1 t1 t2 → R2 t1 t2) → WRealize sig M R1 → WRealize ? M R2.
425 theorem sem_universal2: ∀M:normalTM. ∀R.
426 WRealize ? M R → WRealize ? universalTM (low_R M (start ? M) R).
427 #M #R #HMR lapply (sem_universal … M (start ? M)) @WRealize_to_WRealize
428 #t1 #t2 whd in ⊢ (%→%); #H #tape1 #Htape1 cases (H ? Htape1)
429 #q * #tape2 * * #HRTM #Hhalt #Ht2 @(ex_intro … q) @(ex_intro … tape2)
430 % [% [@(R_TM_to_R … HRTM) @HMR | //] | //]