From e37238b40356ee1b5e7859cf0eb6567918f2ebec Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 5 Jun 2012 11:29:18 +0000 Subject: [PATCH] Some results on relations. Moved things around. --- matita/matita/lib/basics/relations.ma | 27 +- matita/matita/lib/turing/if_machine.ma | 19 +- matita/matita/lib/turing/mono.ma | 13 +- matita/matita/lib/turing/while_machine.ma | 399 +--------------------- 4 files changed, 56 insertions(+), 402 deletions(-) diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma index 55b26b8ae..8b6a79be5 100644 --- a/matita/matita/lib/basics/relations.ma +++ b/matita/matita/lib/basics/relations.ma @@ -46,6 +46,10 @@ definition antisymmetric: ∀A.∀R:relation A.Prop ≝ λA.λR.∀x,y:A. R x y → ¬(R y x). (********** operations **********) +definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2. + ∃am.R1 a1 am ∧ R2 am a2. +interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2). + definition Runion ≝ λA.λR1,R2:relation A.λa,b. R1 a b ∨ R2 a b. interpretation "union of relations" 'union R1 R2 = (Runion ? R1 R2). @@ -54,10 +58,31 @@ interpretation "interesecion of relations" 'intersects R1 R2 = (Rintersection ? definition inv ≝ λA.λR:relation A.λa,b.R b a. +(*********** sub relation ***********) definition subR ≝ λA.λR,S:relation A.(∀a,b. R a b → S a b). interpretation "relation inclusion" 'subseteq R S = (subR ? R S). -(**********P functions **********) +lemma sub_comp_l: ∀A.∀R,R1,R2:relation A. + R1 ⊆ R2 → R1 ∘ R ⊆ R2 ∘ R. +#A #R #R1 #R2 #Hsub #a #b * #c * /4/ +qed. + +lemma sub_comp_r: ∀A.∀R,R1,R2:relation A. + R1 ⊆ R2 → R ∘ R1 ⊆ R ∘ R2. +#A #R #R1 #R2 #Hsub #a #b * #c * /4/ +qed. + +lemma sub_assoc_l: ∀A.∀R1,R2,R3:relation A. + R1 ∘ (R2 ∘ R3) ⊆ (R1 ∘ R2) ∘ R3. +#A #R1 #R2 #R3 #a #b * #c * #Hac * #d * /5/ +qed. + +lemma sub_assoc_r: ∀A.∀R1,R2,R3:relation A. + (R1 ∘ R2) ∘ R3 ⊆ R1 ∘ (R2 ∘ R3). +#A #R1 #R2 #R3 #a #b * #c * * #d * /5 width=5/ +qed. + +(************* functions ************) definition compose ≝ λA,B,C:Type[0].λf:B→C.λg:A→B.λx:A.f (g x). diff --git a/matita/matita/lib/turing/if_machine.ma b/matita/matita/lib/turing/if_machine.ma index 7279ed5cd..2bc83c261 100644 --- a/matita/matita/lib/turing/if_machine.ma +++ b/matita/matita/lib/turing/if_machine.ma @@ -152,7 +152,7 @@ qed. (******************************** semantics ***********************************) lemma sem_if: ∀sig.∀M1,M2,M3:TM sig.∀Rtrue,Rfalse,R2,R3,acc. - accRealize sig M1 acc Rtrue Rfalse → M2 ⊨ R2 → M3 ⊨ R3 → + M1 ⊧ [acc: Rtrue,Rfalse] → M2 ⊨ R2 → M3 ⊨ R3 → ifTM sig M1 M2 M3 acc ⊨ (Rtrue ∘ R2) ∪ (Rfalse ∘ R3). #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HR3 #t cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse @@ -237,12 +237,9 @@ qed. (* we can probably use acc_sem_if to prove sem_if *) lemma acc_sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc. - accRealize sig M1 acc Rtrue Rfalse → M2 ⊨ R2 → M3 ⊨ R3 → - accRealize sig - (ifTM sig M1 (single_finalTM … M2) M3 acc) - (inr … (inl … (inr … start_nop))) - (Rtrue ∘ R2) - (Rfalse ∘ R3). + M1 ⊨ [acc: Rtrue, Rfalse] → M2 ⊨ R2 → M3 ⊨ R3 → + ifTM sig M1 (single_finalTM … M2) M3 acc ⊨ + [inr … (inl … (inr … start_nop)): Rtrue ∘ R2, Rfalse ∘ R3]. #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HR3 #t cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse cases (true_or_false (cstate ?? outc1 == acc)) #Hacc @@ -323,13 +320,11 @@ cases (true_or_false (cstate ?? outc1 == acc)) #Hacc qed. lemma acc_sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,R5,acc. - accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 → + M1 ⊨ [acc: Rtrue, Rfalse] → M2 ⊨ R2 → M3 ⊨ R3 → (∀t1,t2,t3. Rtrue t1 t3 → R2 t3 t2 → R4 t1 t2) → (∀t1,t2,t3. Rfalse t1 t3 → R3 t3 t2 → R5 t1 t2) → - accRealize sig - (ifTM sig M1 (single_finalTM … M2) M3 acc) - (inr … (inl … (inr … start_nop))) - R4 R5. + ifTM sig M1 (single_finalTM … M2) M3 acc ⊨ + [inr … (inl … (inr … start_nop)): R4, R5]. #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #R4 #R5 #acc #HRacc #HRtrue #HRfalse #Hsub1 #Hsub2 #t cases (acc_sem_if … HRacc HRtrue HRfalse t) diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma index 80e3d4aaa..8d772af34 100644 --- a/matita/matita/lib/turing/mono.ma +++ b/matita/matita/lib/turing/mono.ma @@ -183,6 +183,11 @@ lemma loop_eq : ∀sig,f,q,i,j,a,x,y. ] qed. +lemma loop_p_true : + ∀A,k,f,p,a.p a = true → loop A (S k) f p a = Some ? a. +#A #k #f #p #a #Ha normalize >Ha % +qed. + lemma loop_Some : ∀A,k,f,p,a,b.loop A k f p a = Some ? b → p b = true. #A #k #f #p elim k @@ -248,6 +253,9 @@ definition accRealize ≝ λsig.λM:TM sig.λacc:states sig M.λRtrue,Rfalse. loopM sig M i (initc sig M t) = Some ? outc ∧ (cstate ?? outc = acc → Rtrue t (ctape ?? outc)) ∧ (cstate ?? outc ≠ acc → Rfalse t (ctape ?? outc)). + +notation "M ⊨ [q: R1,R2]" non associative with precedence 45 for @{ 'cmodels $M $q $R1 $R2}. +interpretation "conditional realizability" 'cmodels M q R1 R2 = (accRealize ? M q R1 R2). (******************************** NOP Machine *********************************) @@ -298,11 +306,6 @@ definition seq ≝ λsig. λM1,M2 : TM sig. notation "a · b" non associative with precedence 65 for @{ 'middot $a $b}. interpretation "sequential composition" 'middot a b = (seq ? a b). -definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2. - ∃am.R1 a1 am ∧ R2 am a2. - -interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2). - definition lift_confL ≝ λsig,S1,S2,c.match c with [ mk_config s t ⇒ mk_config sig (FinSum S1 S2) (inl … s) t ]. diff --git a/matita/matita/lib/turing/while_machine.ma b/matita/matita/lib/turing/while_machine.ma index d57824644..fff32922e 100644 --- a/matita/matita/lib/turing/while_machine.ma +++ b/matita/matita/lib/turing/while_machine.ma @@ -12,6 +12,10 @@ include "basics/star.ma". include "turing/mono.ma". +(* The following machine implements a while-loop over a body machine $M$. +We just need to extend $M$ adding a single transition leading back from a +distinguished final state $q$ to the initial state. *) + definition while_trans ≝ λsig. λM : TM sig. λq:states sig M. λp. let 〈s,a〉 ≝ p in if s == q then 〈start ? M, None ?〉 @@ -23,8 +27,6 @@ definition whileTM ≝ λsig. λM : TM sig. λqacc: states ? M. (while_trans sig M qacc) (start sig M) (λs.halt sig M s ∧ ¬ s==qacc). - -(* axiom daemon : ∀X:Prop.X. *) lemma while_trans_false : ∀sig,M,q,p. \fst p ≠ q → trans sig (whileTM sig M q) p = trans sig M p. @@ -52,19 +54,20 @@ generalize in match c1; elim k ] qed. -axiom tech1: ∀A.∀R1,R2:relation A. +lemma tech1: ∀A.∀R1,R2:relation A. ∀a,b. (R1 ∘ ((star ? R1) ∘ R2)) a b → ((star ? R1) ∘ R2) a b. - +#A #R1 #R2 #a #b #H lapply (sub_assoc_l ?????? H) @sub_comp_l -a -b +#a #b * #c * /2/ +qed. + lemma halt_while_acc : ∀sig,M,acc.halt sig (whileTM sig M acc) acc = false. -#sig #M #acc normalize >(\b ?) // -cases (halt sig M acc) % +#sig #M #acc normalize >(\b ?) // cases (halt sig M acc) % qed. lemma halt_while_not_acc : ∀sig,M,acc,s.s == acc = false → halt sig (whileTM sig M acc) s = halt sig M s. -#sig #M #acc #s #neqs normalize >neqs -cases (halt sig M s) % +#sig #M #acc #s #neqs normalize >neqs cases (halt sig M s) % qed. lemma step_while_acc : @@ -73,15 +76,10 @@ lemma step_while_acc : #sig #M #acc * #s #t #Hs normalize >(\b Hs) % qed. -lemma loop_p_true : - ∀A,k,f,p,a.p a = true → loop A (S k) f p a = Some ? a. -#A #k #f #p #a #Ha normalize >Ha % -qed. - theorem sem_while: ∀sig,M,acc,Rtrue,Rfalse. halt sig M acc = true → - accRealize sig M acc Rtrue Rfalse → - WRealize sig (whileTM sig M acc) ((star ? Rtrue) ∘ Rfalse). + M ⊨ [acc: Rtrue,Rfalse] → + whileTM sig M acc ⊫ (star ? Rtrue) ∘ Rfalse. #sig #M #acc #Rtrue #Rfalse #Hacctrue #HaccR #t #i generalize in match t; @(nat_elim1 … i) #m #Hind #intape #outc #Hloop @@ -131,8 +129,8 @@ qed. theorem terminate_while: ∀sig,M,acc,Rtrue,Rfalse,t. halt sig M acc = true → - accRealize sig M acc Rtrue Rfalse → - WF ? (inv … Rtrue) t → Terminate sig (whileTM sig M acc) t. + M ⊨ [acc: Rtrue,Rfalse] → + WF ? (inv … Rtrue) t → whileTM sig M acc ↓ t. #sig #M #acc #Rtrue #Rfalse #t #Hacctrue #HM #HWF elim HWF #t1 #H #Hind cases (HM … t1) #i * #outc * * #Hloop #Htrue #Hfalse cases (true_or_false (cstate … outc == acc)) #Hcase @@ -166,370 +164,3 @@ theorem terminate_while: ∀sig,M,acc,Rtrue,Rfalse,t. ] ] qed. - -(* -axiom terminate_while: ∀sig,M,acc,Rtrue,Rfalse,t. - halt sig M acc = true → - accRealize sig M acc Rtrue Rfalse → - ∃t1. Rfalse t t1 → Terminate sig (whileTM sig M acc) t. -*) - -(* (* - -(* We do not distinuish an input tape *) - -record TM (sig:FinSet): Type[1] ≝ -{ states : FinSet; - trans : states × (option sig) → states × (option (sig × move)); - start: states; - halt : states → bool -}. - -record config (sig:FinSet) (M:TM sig): Type[0] ≝ -{ cstate : states sig M; - ctape: tape sig -}. - -definition option_hd ≝ λA.λl:list A. - match l with - [nil ⇒ None ? - |cons a _ ⇒ Some ? a - ]. - -definition tape_move ≝ λsig.λt: tape sig.λm:option (sig × move). - match m with - [ None ⇒ t - | Some m1 ⇒ - match \snd m1 with - [ R ⇒ mk_tape sig ((\fst m1)::(left ? t)) (tail ? (right ? t)) - | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m1)::(right ? t)) - ] - ]. - -definition step ≝ λsig.λM:TM sig.λc:config sig M. - let current_char ≝ option_hd ? (right ? (ctape ?? c)) in - let 〈news,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in - mk_config ?? news (tape_move sig (ctape ?? c) mv). - -let rec loop (A:Type[0]) n (f:A→A) p a on n ≝ - match n with - [ O ⇒ None ? - | S m ⇒ if p a then (Some ? a) else loop A m f p (f a) - ]. - -lemma loop_incr : ∀A,f,p,k1,k2,a1,a2. - loop A k1 f p a1 = Some ? a2 → - loop A (k2+k1) f p a1 = Some ? a2. -#A #f #p #k1 #k2 #a1 #a2 generalize in match a1; elim k1 -[normalize #a0 #Hfalse destruct -|#k1' #IH #a0 Hpa0 whd in ⊢ (??%? → ??%?); // @IH -] -qed. - -lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) → - ∀k1,k2,a1,a2,a3,a4. - loop A k1 f p a1 = Some ? a2 → - f a2 = a3 → q a2 = false → - loop A k2 f q a3 = Some ? a4 → - loop A (k1+k2) f q a1 = Some ? a4. -#Sig #f #p #q #Hpq #k1 elim k1 - [normalize #k2 #a1 #a2 #a3 #a4 #H destruct - |#k1' #Hind #k2 #a1 #a2 #a3 #a4 normalize in ⊢ (%→?); - cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?); - [#eqa1a2 destruct #eqa2a3 #Hqa2 #H - whd in ⊢ (??(??%???)?); >plus_n_Sm @loop_incr - whd in ⊢ (??%?); >Hqa2 >eqa2a3 @H - |normalize >(Hpq … pa1) normalize - #H1 #H2 #H3 @(Hind … H2) // - ] - ] -qed. - -(* -lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) → - ∀k1,k2,a1,a2,a3. - loop A k1 f p a1 = Some ? a2 → - loop A k2 f q a2 = Some ? a3 → - loop A (k1+k2) f q a1 = Some ? a3. -#Sig #f #p #q #Hpq #k1 elim k1 - [normalize #k2 #a1 #a2 #a3 #H destruct - |#k1' #Hind #k2 #a1 #a2 #a3 normalize in ⊢ (%→?→?); - cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?); - [#eqa1a2 destruct #H @loop_incr // - |normalize >(Hpq … pa1) normalize - #H1 #H2 @(Hind … H2) // - ] - ] -qed. -*) - -definition initc ≝ λsig.λM:TM sig.λt. - mk_config sig M (start sig M) t. - -definition Realize ≝ λsig.λM:TM sig.λR:relation (tape sig). -∀t.∃i.∃outc. - loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧ - R t (ctape ?? outc). - -(* Compositions *) - -definition seq_trans ≝ λsig. λM1,M2 : TM sig. -λp. let 〈s,a〉 ≝ p in - match s with - [ inl s1 ⇒ - if halt sig M1 s1 then 〈inr … (start sig M2), None ?〉 - else - let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in - 〈inl … news1,m〉 - | inr s2 ⇒ - let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in - 〈inr … news2,m〉 - ]. - -definition seq ≝ λsig. λM1,M2 : TM sig. - mk_TM sig - (FinSum (states sig M1) (states sig M2)) - (seq_trans sig M1 M2) - (inl … (start sig M1)) - (λs.match s with - [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]). - -definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2. - ∃am.R1 a1 am ∧ R2 am a2. - -(* -definition injectRl ≝ λsig.λM1.λM2.λR. - λc1,c2. ∃c11,c12. - inl … (cstate sig M1 c11) = cstate sig (seq sig M1 M2) c1 ∧ - inl … (cstate sig M1 c12) = cstate sig (seq sig M1 M2) c2 ∧ - ctape sig M1 c11 = ctape sig (seq sig M1 M2) c1 ∧ - ctape sig M1 c12 = ctape sig (seq sig M1 M2) c2 ∧ - R c11 c12. - -definition injectRr ≝ λsig.λM1.λM2.λR. - λc1,c2. ∃c21,c22. - inr … (cstate sig M2 c21) = cstate sig (seq sig M1 M2) c1 ∧ - inr … (cstate sig M2 c22) = cstate sig (seq sig M1 M2) c2 ∧ - ctape sig M2 c21 = ctape sig (seq sig M1 M2) c1 ∧ - ctape sig M2 c22 = ctape sig (seq sig M1 M2) c2 ∧ - R c21 c22. - -definition Rlink ≝ λsig.λM1,M2.λc1,c2. - ctape sig (seq sig M1 M2) c1 = ctape sig (seq sig M1 M2) c2 ∧ - cstate sig (seq sig M1 M2) c1 = inl … (halt sig M1) ∧ - cstate sig (seq sig M1 M2) c2 = inr … (start sig M2). *) - -interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2). - -definition lift_confL ≝ - λsig,M1,M2,c.match c with - [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inl … s) t ]. -definition lift_confR ≝ - λsig,M1,M2,c.match c with - [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inr … s) t ]. - -definition halt_liftL ≝ - λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2). - match s with - [ inl s1 ⇒ halt sig M1 s1 - | inr _ ⇒ true ]. (* should be vacuous in all cases we use halt_liftL *) - -definition halt_liftR ≝ - λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2). - match s with - [ inl _ ⇒ false - | inr s2 ⇒ halt sig M2 s2 ]. - -lemma p_halt_liftL : ∀sig,M1,M2,c. - halt sig M1 (cstate … c) = - halt_liftL sig M1 M2 (cstate … (lift_confL … c)). -#sig #M1 #M2 #c cases c #s #t % -qed. - -lemma trans_liftL : ∀sig,M1,M2,s,a,news,move. - halt ? M1 s = false → - trans sig M1 〈s,a〉 = 〈news,move〉 → - trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inl … news,move〉. -#sig (*#M1*) * #Q1 #T1 #init1 #halt1 #M2 #s #a #news #move -#Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans % -qed. - -lemma config_eq : - ∀sig,M,c1,c2. - cstate sig M c1 = cstate sig M c2 → - ctape sig M c1 = ctape sig M c2 → c1 = c2. -#sig #M1 * #s1 #t1 * #s2 #t2 // -qed. - -lemma step_lift_confL : ∀sig,M1,M2,c0. - halt ? M1 (cstate ?? c0) = false → - step sig (seq sig M1 M2) (lift_confL sig M1 M2 c0) = - lift_confL sig M1 M2 (step sig M1 c0). -#sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s * #lt -#rs #Hhalt -whd in ⊢ (???(????%));whd in ⊢ (???%); -lapply (refl ? (trans ?? 〈s,option_hd sig rs〉)) -cases (trans ?? 〈s,option_hd sig rs〉) in ⊢ (???% → %); -#s0 #m0 #Heq whd in ⊢ (???%); -whd in ⊢ (??(???%)?); whd in ⊢ (??%?); ->(trans_liftL … Heq) -[% | //] -qed. - -lemma loop_liftL : ∀sig,k,M1,M2,c1,c2. - loop ? k (step sig M1) (λc.halt sig M1 (cstate ?? c)) c1 = Some ? c2 → - loop ? k (step sig (seq sig M1 M2)) - (λc.halt_liftL sig M1 M2 (cstate ?? c)) (lift_confL … c1) = - Some ? (lift_confL … c2). -#sig #k #M1 #M2 #c1 #c2 generalize in match c1; -elim k -[#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse) -|#k0 #IH #c0 whd in ⊢ (??%? → ??%?); - lapply (refl ? (halt ?? (cstate sig M1 c0))) - cases (halt ?? (cstate sig M1 c0)) in ⊢ (???% → ?); #Hc0 >Hc0 - [ >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = true) - [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2) % - | // ] - | >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = false) - [whd in ⊢ (??%? → ??%?); #Hc2 <(IH ? Hc2) @eq_f - @step_lift_confL // - | // ] -qed. - -STOP! - -lemma loop_liftR : ∀sig,k,M1,M2,c1,c2. - loop ? k (step sig M2) (λc.halt sig M2 (cstate ?? c)) c1 = Some ? c2 → - loop ? k (step sig (seq sig M1 M2)) - (λc.halt sig (seq sig M1 M2) (cstate ?? c)) (lift_confR … c1) = - Some ? (lift_confR … c2). -#sig #k #M1 #M2 #c1 #c2 -elim k -[normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse) -|#k0 #IH whd in ⊢ (??%? → ??%?); - lapply (refl ? (halt ?? (cstate sig M2 c1))) - cases (halt ?? (cstate sig M2 c1)) in ⊢ (???% → ?); #Hc0 >Hc0 - [ >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = true) - [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2) - | (* ... *) ] - | >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = false) - [whd in ⊢ (??%? → ??%?); #Hc2 Hhalt % -qed. - -lemma eq_ctape_lift_conf_L : ∀sig,M1,M2,outc. - ctape sig (seq sig M1 M2) (lift_confL … outc) = ctape … outc. -#sig #M1 #M2 #outc cases outc #s #t % -qed. - -lemma eq_ctape_lift_conf_R : ∀sig,M1,M2,outc. - ctape sig (seq sig M1 M2) (lift_confR … outc) = ctape … outc. -#sig #M1 #M2 #outc cases outc #s #t % -qed. - -theorem sem_seq: ∀sig,M1,M2,R1,R2. - Realize sig M1 R1 → Realize sig M2 R2 → - Realize sig (seq sig M1 M2) (R1 ∘ R2). -#sig #M1 #M2 #R1 #R2 #HR1 #HR2 #t -cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1 -cases (HR2 (ctape sig M1 outc1)) #k2 * #outc2 * #Hloop2 #HM2 -@(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2)) -% -[@(loop_split ??????????? (loop_liftL … Hloop1)) - [* * - [ #sl #tl whd in ⊢ (??%? → ?); #Hl % - | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ] - ||4:cases outc1 #s1 #t1 % - |5:@(loop_liftR … Hloop2) - |whd in ⊢ (??(???%)?);whd in ⊢ (??%?); - generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10 - >(trans_liftL_true sig M1 M2 ??) - [ whd in ⊢ (??%?); whd in ⊢ (???%); - @config_eq // - | @(loop_Some ?????? Hloop10) ] - ] -| @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1))) - % // -] -qed. - -(* boolean machines: machines with two distinguished halting states *) - - - -(* old stuff *) -definition empty_tapes ≝ λsig.λn. -mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?. -elim n // normalize // -qed. - -definition init ≝ λsig.λM:TM sig.λi:(list sig). - mk_config ?? - (start sig M) - (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M))) - [ ]. - -definition stop ≝ λsig.λM:TM sig.λc:config sig M. - halt sig M (state sig M c). - -let rec loop (A:Type[0]) n (f:A→A) p a on n ≝ - match n with - [ O ⇒ None ? - | S m ⇒ if p a then (Some ? a) else loop A m f p (f a) - ]. - -(* Compute ? M f states that f is computed by M *) -definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig). -∀l.∃i.∃c. - loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧ - out ?? c = f l. - -(* for decision problems, we accept a string if on termination -output is not empty *) - -definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool. -∀l.∃i.∃c. - loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧ - (isnilb ? (out ?? c) = false). - -(* alternative approach. -We define the notion of computation. The notion must be constructive, -since we want to define functions over it, like lenght and size - -Perche' serve Type[2] se sposto a e b a destra? *) - -inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝ - mk_move: p a = false → b = f a → cmove A f p a b. - -inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝ -| empty : ∀a. cstar A M a a -| more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c. - -definition computation ≝ λsig.λM:TM sig. - cstar ? (cmove ? (step sig M) (stop sig M)). - -definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig). - ∀l.∃c.computation sig M (init sig M l) c → - (stop sig M c = true) ∧ out ?? c = f l. - -definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool. - ∀l.∃c.computation sig M (init sig M l) c → - (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false). -*) \ No newline at end of file -- 2.39.2