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 "basics/star.ma".
13 include "turing/mono.ma".
15 definition while_trans ≝ λsig. λM : TM sig. λq:states sig M. λp.
17 if s == q then 〈start ? M, None ?〉
20 definition whileTM ≝ λsig. λM : TM sig. λqacc: states ? M.
23 (while_trans sig M qacc)
25 (λs.halt sig M s ∧ ¬ s==qacc).
27 (* axiom daemon : ∀X:Prop.X. *)
29 lemma while_trans_false : ∀sig,M,q,p.
30 \fst p ≠ q → trans sig (whileTM sig M q) p = trans sig M p.
31 #sig #M #q * #q1 #a #Hq normalize >(\bf Hq) normalize //
34 lemma loop_lift_acc : ∀A,B,k,lift,f,g,h,hlift,c1,c2,subh.
35 (∀x.subh x = true → h x = true) →
36 (∀x.subh x = false → hlift (lift x) = h x) →
37 (∀x.h x = false → lift (f x) = g (lift x)) →
39 loop A k f h c1 = Some ? c2 →
40 loop B k g hlift (lift c1) = Some ? (lift … c2).
41 #A #B #k #lift #f #g #h #hlift #c1 #c2 #subh #Hsubh #Hlift #Hfg #Hc2
42 generalize in match c1; elim k
43 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
44 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
45 cases (true_or_false (h c0)) #Hc0 >Hc0
46 [ normalize #Heq destruct (Heq) >(Hlift … Hc2) >Hc0 //
47 | normalize >(Hlift c0)
48 [>Hc0 normalize <(Hfg … Hc0) @IH
49 |cases (true_or_false (subh c0)) //
50 #H <Hc0 @sym_eq >H @Hsubh //
55 axiom tech1: ∀A.∀R1,R2:relation A.
56 ∀a,b. (R1 ∘ ((star ? R1) ∘ R2)) a b → ((star ? R1) ∘ R2) a b.
58 lemma halt_while_acc :
59 ∀sig,M,acc.halt sig (whileTM sig M acc) acc = false.
60 #sig #M #acc normalize >(\b ?) //
61 cases (halt sig M acc) %
64 lemma step_while_acc :
65 ∀sig,M,acc,c.cstate ?? c = acc →
66 step sig (whileTM sig M acc) c = initc … (ctape ?? c).
67 #sig #M #acc * #s #t #Hs normalize >(\b Hs) %
71 ∀A,k,f,p,a.p a = true → loop A (S k) f p a = Some ? a.
72 #A #k #f #p #a #Ha normalize >Ha %
75 theorem sem_while: ∀sig,M,acc,Rtrue,Rfalse.
76 halt sig M acc = true →
77 accRealize sig M acc Rtrue Rfalse →
78 WRealize sig (whileTM sig M acc) ((star ? Rtrue) ∘ Rfalse).
79 #sig #M #acc #Rtrue #Rfalse #Hacctrue #HaccR #t #i
80 generalize in match t;
81 @(nat_elim1 … i) #m #Hind #intape #outc #Hloop
82 cases (loop_split ?? (λc. halt sig M (cstate ?? c)) ????? Hloop)
83 [#k1 * #outc1 * #Hloop1 #Hloop2
84 cases (HaccR intape) #k * #outcM * * #HloopM #HMtrue #HMfalse
86 [ @(loop_eq … k … Hloop1)
87 @(loop_lift ?? k (λc.c) ?
88 (step ? (whileTM ? M acc)) ?
89 (λc.halt sig M (cstate ?? c)) ??
92 | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
94 |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
96 | #HoutcM1 cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
97 [@tech1 @(ex_intro … (ctape ?? outc1)) %
98 [ <HoutcM1 @HMtrue >HoutcM1 @(\P Hacc)
101 [normalize #H destruct (H) ]
102 #m' #_ cases k1 in Hloop1;
103 [normalize #H destruct (H) ]
104 #k1' #_ normalize /2/
105 | <Hloop2 whd in ⊢ (???%);
106 >(\P Hacc) >halt_while_acc whd in ⊢ (???%);
107 normalize in match (halt ?? acc);
108 >step_while_acc // @(\P Hacc)
111 |@(ex_intro … intape) % //
112 cut (Some ? outc1 = Some ? outc)
113 [ <Hloop1 <Hloop2 >loop_p_true in ⊢ (???%); //
114 normalize >(loop_Some ?????? Hloop1) >Hacc %
115 | #Houtc1c destruct @HMfalse @(\Pf Hacc)
119 | * #s0 #t0 normalize cases (s0 == acc) normalize
120 [ cases (halt sig M s0) normalize #Hfalse destruct
121 | cases (halt sig M s0) normalize //
126 (* inductive move_states : Type[0] ≝
127 | start : move_states
132 | qfail : move_states.
137 definition mystates : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 5) alpha.
139 definition move_char ≝
140 λalpha:FinSet.λsep:alpha.
141 mk_TM alpha (mystates alpha)
145 [ None ⇒ 〈〈4,sep〉,None ?〉
150 [ true ⇒ 〈〈4,sep〉,None ?〉
151 | false ⇒ 〈〈1,a'〉,Some ? 〈a',L〉〉 ]
152 | S q' ⇒ match q' with
154 〈〈2,a'〉,Some ? 〈b,R〉〉
155 | S q' ⇒ match q' with
157 〈〈3,sep〉,Some ? 〈b,R〉〉
158 | S q' ⇒ match q' with
162 〈〈4,sep〉,None ?〉 ] ] ] ] ])
164 (λq.let 〈q',a〉 ≝ q in q' == 3 ∨ q' == 4).
167 ∀sig:FinSet.list sig → option sig → list sig → tape sig ≝
168 λsig,lt,c,rt.match c with
169 [ Some c' ⇒ midtape sig lt c' rt
170 | None ⇒ match lt with
171 [ nil ⇒ match rt with
173 | cons r0 rs0 ⇒ leftof ? r0 rs0 ]
174 | cons l0 ls0 ⇒ rightof ? l0 ls0 ] ].
177 ∀alpha:FinSet.∀sep,a,ls,a0,rs.
179 step alpha (move_char alpha sep)
180 (mk_config ?? 〈0,a〉 (mk_tape … ls (Some ? a0) rs)) =
181 mk_config alpha (states ? (move_char alpha sep)) 〈1,a0〉
182 (tape_move_left alpha ls a0 rs).
184 [ #a0 #rs #Ha0 whd in ⊢ (??%?);
185 normalize in match (trans ???); >Ha0 %
186 | #a1 #ls #a0 #rs #Ha0 whd in ⊢ (??%?);
187 normalize in match (trans ???); >Ha0 %
192 ∀alpha:FinSet.∀sep,a,ls,a0,rs.
193 step alpha (move_char alpha sep)
194 (mk_config ?? 〈1,a〉 (mk_tape … ls (Some ? a0) rs)) =
195 mk_config alpha (states ? (move_char alpha sep)) 〈2,a0〉
196 (tape_move_right alpha ls a rs).
197 #alpha #sep #a #ls #a0 * //
201 ∀alpha:FinSet.∀sep,a,ls,a0,rs.
202 step alpha (move_char alpha sep)
203 (mk_config ?? 〈2,a〉 (mk_tape … ls (Some ? a0) rs)) =
204 mk_config alpha (states ? (move_char alpha sep)) 〈3,sep〉
205 (tape_move_right alpha ls a rs).
206 #alpha #sep #a #ls #a0 * //
209 definition option_hd ≝
210 λA.λl:list A. match l with
212 | cons a _ ⇒ Some ? a ].
214 definition Rmove_char_true ≝
216 ∀a,b,ls,rs. b ≠ sep →
217 t1 = midtape alpha (a::ls) b rs →
218 t2 = mk_tape alpha (a::b::ls) (option_hd ? rs) (tail ? rs).
220 definition Rmove_char_false ≝
222 (current alpha t1 = None alpha → t2 = t1) ∧
223 (current alpha t1 = Some alpha sep → t2 = t1).
226 ∀A,n,f,p,a. p a = true →
227 loop A (S n) f p a = Some ? a. /2/
231 ∀A,n,f,p,a. p a = false →
232 loop A (S n) f p a = loop A n f p (f a).
233 normalize #A #n #f #p #a #Hpa >Hpa %
236 notation < "𝐅" non associative with precedence 90
238 notation < "𝐃" non associative with precedence 90
241 interpretation "FinSet" 'bigF = (mk_FinSet ???).
242 interpretation "DeqSet" 'bigD = (mk_DeqSet ???).
244 lemma trans_init_sep:
246 trans ? (move_char alpha sep) 〈〈0,x〉,Some ? sep〉 = 〈〈4,sep〉,None ?〉.
247 #alpha #sep #x normalize >(\b ?) //
250 lemma trans_init_not_sep:
251 ∀alpha,sep,x,y.y == sep = false →
252 trans ? (move_char alpha sep) 〈〈0,x〉,Some ? y〉 = 〈〈1,y〉,Some ? 〈y,L〉〉.
253 #alpha #sep #x #y #H1 normalize >H1 //
256 lemma sem_move_char :
258 accRealize alpha (move_char alpha sep)
259 〈3,sep〉 (Rmove_char_true alpha sep) (Rmove_char_false alpha sep).
262 @(ex_intro … (mk_config ?? 〈4,sep〉 (niltape ?)))
263 % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 whd % #_ % ]
264 |#l0 #lt0 @(ex_intro ?? 2)
265 @(ex_intro … (mk_config ?? 〈4,sep〉 (leftof ? l0 lt0)))
266 % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 whd % #_ % ]
267 |#r0 #rt0 @(ex_intro ?? 2)
268 @(ex_intro … (mk_config ?? 〈4,sep〉 (rightof ? r0 rt0)))
269 % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 whd % #_ % ]
270 | #lt #c #rt cases (true_or_false (c == sep)) #Hc
272 @(ex_intro ?? (mk_config ?? 〈4,sep〉 (midtape ? lt c rt)))
275 [ >(\P Hc) >loop_S_false //
277 [ @eq_f whd in ⊢ (??%?); >trans_init_sep %
278 |>(\P Hc) whd in ⊢(??(???(???%))?);
290 | normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
292 | normalize in ⊢ (%→?); #_ %
293 [ normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
294 | normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
295 @False_ind @(absurd ?? (\Pf Hc)) %
304 | #_ #a #b #ls #rs #Hb #Htape
308 cases rs normalize //
310 | normalize in ⊢ (% → ?); * #Hfalse
319 definition R_while_cmove :
321 ∀a,b,ls,rs. b ≠ sep → memb ? sep rs = false →
322 t1 = midtape alpha (a::ls) b (rs@sep::rs') →
323 t2 = midtape alpha (a::rev ? rs@b::ls) sep rs'.
327 (* We do not distinuish an input tape *)
329 record TM (sig:FinSet): Type[1] ≝
331 trans : states × (option sig) → states × (option (sig × move));
336 record config (sig:FinSet) (M:TM sig): Type[0] ≝
337 { cstate : states sig M;
341 definition option_hd ≝ λA.λl:list A.
347 definition tape_move ≝ λsig.λt: tape sig.λm:option (sig × move).
352 [ R ⇒ mk_tape sig ((\fst m1)::(left ? t)) (tail ? (right ? t))
353 | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m1)::(right ? t))
357 definition step ≝ λsig.λM:TM sig.λc:config sig M.
358 let current_char ≝ option_hd ? (right ? (ctape ?? c)) in
359 let 〈news,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
360 mk_config ?? news (tape_move sig (ctape ?? c) mv).
362 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
365 | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
368 lemma loop_incr : ∀A,f,p,k1,k2,a1,a2.
369 loop A k1 f p a1 = Some ? a2 →
370 loop A (k2+k1) f p a1 = Some ? a2.
371 #A #f #p #k1 #k2 #a1 #a2 generalize in match a1; elim k1
372 [normalize #a0 #Hfalse destruct
373 |#k1' #IH #a0 <plus_n_Sm whd in ⊢ (??%? → ??%?);
374 cases (true_or_false (p a0)) #Hpa0 >Hpa0 whd in ⊢ (??%? → ??%?); // @IH
378 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
380 loop A k1 f p a1 = Some ? a2 →
381 f a2 = a3 → q a2 = false →
382 loop A k2 f q a3 = Some ? a4 →
383 loop A (k1+k2) f q a1 = Some ? a4.
384 #Sig #f #p #q #Hpq #k1 elim k1
385 [normalize #k2 #a1 #a2 #a3 #a4 #H destruct
386 |#k1' #Hind #k2 #a1 #a2 #a3 #a4 normalize in ⊢ (%→?);
387 cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
388 [#eqa1a2 destruct #eqa2a3 #Hqa2 #H
389 whd in ⊢ (??(??%???)?); >plus_n_Sm @loop_incr
390 whd in ⊢ (??%?); >Hqa2 >eqa2a3 @H
391 |normalize >(Hpq … pa1) normalize
392 #H1 #H2 #H3 @(Hind … H2) //
398 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
400 loop A k1 f p a1 = Some ? a2 →
401 loop A k2 f q a2 = Some ? a3 →
402 loop A (k1+k2) f q a1 = Some ? a3.
403 #Sig #f #p #q #Hpq #k1 elim k1
404 [normalize #k2 #a1 #a2 #a3 #H destruct
405 |#k1' #Hind #k2 #a1 #a2 #a3 normalize in ⊢ (%→?→?);
406 cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
407 [#eqa1a2 destruct #H @loop_incr //
408 |normalize >(Hpq … pa1) normalize
409 #H1 #H2 @(Hind … H2) //
415 definition initc ≝ λsig.λM:TM sig.λt.
416 mk_config sig M (start sig M) t.
418 definition Realize ≝ λsig.λM:TM sig.λR:relation (tape sig).
420 loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧
425 definition seq_trans ≝ λsig. λM1,M2 : TM sig.
429 if halt sig M1 s1 then 〈inr … (start sig M2), None ?〉
431 let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in
434 let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
438 definition seq ≝ λsig. λM1,M2 : TM sig.
440 (FinSum (states sig M1) (states sig M2))
441 (seq_trans sig M1 M2)
442 (inl … (start sig M1))
444 [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]).
446 definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
447 ∃am.R1 a1 am ∧ R2 am a2.
450 definition injectRl ≝ λsig.λM1.λM2.λR.
452 inl … (cstate sig M1 c11) = cstate sig (seq sig M1 M2) c1 ∧
453 inl … (cstate sig M1 c12) = cstate sig (seq sig M1 M2) c2 ∧
454 ctape sig M1 c11 = ctape sig (seq sig M1 M2) c1 ∧
455 ctape sig M1 c12 = ctape sig (seq sig M1 M2) c2 ∧
458 definition injectRr ≝ λsig.λM1.λM2.λR.
460 inr … (cstate sig M2 c21) = cstate sig (seq sig M1 M2) c1 ∧
461 inr … (cstate sig M2 c22) = cstate sig (seq sig M1 M2) c2 ∧
462 ctape sig M2 c21 = ctape sig (seq sig M1 M2) c1 ∧
463 ctape sig M2 c22 = ctape sig (seq sig M1 M2) c2 ∧
466 definition Rlink ≝ λsig.λM1,M2.λc1,c2.
467 ctape sig (seq sig M1 M2) c1 = ctape sig (seq sig M1 M2) c2 ∧
468 cstate sig (seq sig M1 M2) c1 = inl … (halt sig M1) ∧
469 cstate sig (seq sig M1 M2) c2 = inr … (start sig M2). *)
471 interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
473 definition lift_confL ≝
474 λsig,M1,M2,c.match c with
475 [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inl … s) t ].
476 definition lift_confR ≝
477 λsig,M1,M2,c.match c with
478 [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inr … s) t ].
480 definition halt_liftL ≝
481 λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
483 [ inl s1 ⇒ halt sig M1 s1
484 | inr _ ⇒ true ]. (* should be vacuous in all cases we use halt_liftL *)
486 definition halt_liftR ≝
487 λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
490 | inr s2 ⇒ halt sig M2 s2 ].
492 lemma p_halt_liftL : ∀sig,M1,M2,c.
493 halt sig M1 (cstate … c) =
494 halt_liftL sig M1 M2 (cstate … (lift_confL … c)).
495 #sig #M1 #M2 #c cases c #s #t %
498 lemma trans_liftL : ∀sig,M1,M2,s,a,news,move.
499 halt ? M1 s = false →
500 trans sig M1 〈s,a〉 = 〈news,move〉 →
501 trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inl … news,move〉.
502 #sig (*#M1*) * #Q1 #T1 #init1 #halt1 #M2 #s #a #news #move
503 #Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
508 cstate sig M c1 = cstate sig M c2 →
509 ctape sig M c1 = ctape sig M c2 → c1 = c2.
510 #sig #M1 * #s1 #t1 * #s2 #t2 //
513 lemma step_lift_confL : ∀sig,M1,M2,c0.
514 halt ? M1 (cstate ?? c0) = false →
515 step sig (seq sig M1 M2) (lift_confL sig M1 M2 c0) =
516 lift_confL sig M1 M2 (step sig M1 c0).
517 #sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s * #lt
519 whd in ⊢ (???(????%));whd in ⊢ (???%);
520 lapply (refl ? (trans ?? 〈s,option_hd sig rs〉))
521 cases (trans ?? 〈s,option_hd sig rs〉) in ⊢ (???% → %);
522 #s0 #m0 #Heq whd in ⊢ (???%);
523 whd in ⊢ (??(???%)?); whd in ⊢ (??%?);
528 lemma loop_liftL : ∀sig,k,M1,M2,c1,c2.
529 loop ? k (step sig M1) (λc.halt sig M1 (cstate ?? c)) c1 = Some ? c2 →
530 loop ? k (step sig (seq sig M1 M2))
531 (λc.halt_liftL sig M1 M2 (cstate ?? c)) (lift_confL … c1) =
532 Some ? (lift_confL … c2).
533 #sig #k #M1 #M2 #c1 #c2 generalize in match c1;
535 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
536 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
537 lapply (refl ? (halt ?? (cstate sig M1 c0)))
538 cases (halt ?? (cstate sig M1 c0)) in ⊢ (???% → ?); #Hc0 >Hc0
539 [ >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = true)
540 [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2) %
542 | >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = false)
543 [whd in ⊢ (??%? → ??%?); #Hc2 <(IH ? Hc2) @eq_f
550 lemma loop_liftR : ∀sig,k,M1,M2,c1,c2.
551 loop ? k (step sig M2) (λc.halt sig M2 (cstate ?? c)) c1 = Some ? c2 →
552 loop ? k (step sig (seq sig M1 M2))
553 (λc.halt sig (seq sig M1 M2) (cstate ?? c)) (lift_confR … c1) =
554 Some ? (lift_confR … c2).
555 #sig #k #M1 #M2 #c1 #c2
557 [normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
558 |#k0 #IH whd in ⊢ (??%? → ??%?);
559 lapply (refl ? (halt ?? (cstate sig M2 c1)))
560 cases (halt ?? (cstate sig M2 c1)) in ⊢ (???% → ?); #Hc0 >Hc0
561 [ >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = true)
562 [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2)
564 | >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = false)
565 [whd in ⊢ (??%? → ??%?); #Hc2 <IH
566 [@eq_f (* @step_lift_confR // *)
572 ∀A,k,f,p,a,b.loop A k f p a = Some ? b → p b = true.
573 #A #k #f #p #a #b elim k
574 [normalize #Hfalse destruct
575 |#k0 #IH whd in ⊢ (??%? → ?); cases (p a)
576 [ normalize #H1 destruct
578 lemma trans_liftL_true : ∀sig,M1,M2,s,a.
580 trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inr … (start ? M2),None ?〉.
582 #Hhalt whd in ⊢ (??%?); >Hhalt %
585 lemma eq_ctape_lift_conf_L : ∀sig,M1,M2,outc.
586 ctape sig (seq sig M1 M2) (lift_confL … outc) = ctape … outc.
587 #sig #M1 #M2 #outc cases outc #s #t %
590 lemma eq_ctape_lift_conf_R : ∀sig,M1,M2,outc.
591 ctape sig (seq sig M1 M2) (lift_confR … outc) = ctape … outc.
592 #sig #M1 #M2 #outc cases outc #s #t %
595 theorem sem_seq: ∀sig,M1,M2,R1,R2.
596 Realize sig M1 R1 → Realize sig M2 R2 →
597 Realize sig (seq sig M1 M2) (R1 ∘ R2).
598 #sig #M1 #M2 #R1 #R2 #HR1 #HR2 #t
599 cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
600 cases (HR2 (ctape sig M1 outc1)) #k2 * #outc2 * #Hloop2 #HM2
601 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
603 [@(loop_split ??????????? (loop_liftL … Hloop1))
605 [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
606 | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
607 ||4:cases outc1 #s1 #t1 %
608 |5:@(loop_liftR … Hloop2)
609 |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
610 generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
611 >(trans_liftL_true sig M1 M2 ??)
612 [ whd in ⊢ (??%?); whd in ⊢ (???%);
614 | @(loop_Some ?????? Hloop10) ]
616 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))
621 (* boolean machines: machines with two distinguished halting states *)
626 definition empty_tapes ≝ λsig.λn.
627 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
628 elim n // normalize //
631 definition init ≝ λsig.λM:TM sig.λi:(list sig).
634 (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
637 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
638 halt sig M (state sig M c).
640 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
643 | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
646 (* Compute ? M f states that f is computed by M *)
647 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
649 loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
652 (* for decision problems, we accept a string if on termination
653 output is not empty *)
655 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
657 loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
658 (isnilb ? (out ?? c) = false).
660 (* alternative approach.
661 We define the notion of computation. The notion must be constructive,
662 since we want to define functions over it, like lenght and size
664 Perche' serve Type[2] se sposto a e b a destra? *)
666 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
667 mk_move: p a = false → b = f a → cmove A f p a b.
669 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
670 | empty : ∀a. cstar A M a a
671 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
673 definition computation ≝ λsig.λM:TM sig.
674 cstar ? (cmove ? (step sig M) (stop sig M)).
676 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
677 ∀l.∃c.computation sig M (init sig M l) c →
678 (stop sig M c = true) ∧ out ?? c = f l.
680 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
681 ∀l.∃c.computation sig M (init sig M l) c →
682 (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).