From 5b28867e30a9cada823ad86ae91d39b94648940a Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 4 Jun 2012 14:16:05 +0000 Subject: [PATCH] semantics of the if-machine. Moved some lemmas to their proper places. --- matita/matita/lib/basics/relations.ma | 14 +- matita/matita/lib/basics/star.ma | 6 - matita/matita/lib/turing/if_machine.ma | 225 ++++++++++++++++++------- matita/matita/lib/turing/mono.ma | 85 ++++++---- 4 files changed, 223 insertions(+), 107 deletions(-) diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma index ff190e5e3..55b26b8ae 100644 --- a/matita/matita/lib/basics/relations.ma +++ b/matita/matita/lib/basics/relations.ma @@ -45,7 +45,19 @@ definition tight_apart: ∀A.∀eq,ap:relation A.Prop definition antisymmetric: ∀A.∀R:relation A.Prop ≝ λA.λR.∀x,y:A. R x y → ¬(R y x). -(********** functions **********) +(********** operations **********) +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). + +definition Rintersection ≝ λA.λR1,R2:relation A.λa,b.R1 a b ∧ R2 a b. +interpretation "interesecion of relations" 'intersects R1 R2 = (Rintersection ? R1 R2). + +definition inv ≝ λA.λR:relation A.λa,b.R b a. + +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 **********) definition compose ≝ λA,B,C:Type[0].λf:B→C.λg:A→B.λx:A.f (g x). diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma index a80ccbea0..c8d2a9473 100644 --- a/matita/matita/lib/basics/star.ma +++ b/matita/matita/lib/basics/star.ma @@ -11,12 +11,6 @@ include "basics/relations.ma". -(********** relations **********) - -definition subR ≝ λA.λR,S:relation A.(∀a,b. R a b → S a b). - -definition inv ≝ λA.λR:relation A.λa,b.R b a. - (* transitive closcure (plus) *) inductive TC (A:Type[0]) (R:relation A) (a:A): A → Prop ≝ diff --git a/matita/matita/lib/turing/if_machine.ma b/matita/matita/lib/turing/if_machine.ma index 3d6675d02..5d52dea55 100644 --- a/matita/matita/lib/turing/if_machine.ma +++ b/matita/matita/lib/turing/if_machine.ma @@ -14,8 +14,8 @@ include "turing/mono.ma". definition single_finalTM ≝ λsig.λM:TM sig.seq ? M (nop ?). -lemma sem_single_final : - ∀sig,M,R.Realize ? M R → Realize ? (single_finalTM sig M) R. +lemma sem_single_final: ∀sig.∀M: TM sig.∀R. + M ⊨ R → single_finalTM sig M ⊨ R. #sig #M #R #HR #intape cases (sem_seq ????? HR (sem_nop …) intape) #k * #outc * #Hloop * #ta * #Hta whd in ⊢ (%→?); #Houtc @@ -55,15 +55,164 @@ definition ifTM ≝ λsig. λcondM,thenM,elseM : TM sig. axiom daemon : ∀X:Prop.X. axiom tdaemon : ∀X:Type[0].X. -axiom sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc. - accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 → - Realize sig (ifTM sig M1 M2 M3 acc) (λt1,t2. (Rtrue ∘ R2) t1 t2 ∨ (Rfalse ∘ R3) t1 t2). - +(****************************** lifting lemmas ********************************) +lemma trans_if_liftM1 : ∀sig,M1,M2,M3,acc,s,a,news,move. + halt ? M1 s = false → + trans sig M1 〈s,a〉 = 〈news,move〉 → + trans sig (ifTM sig M1 M2 M3 acc) 〈inl … s,a〉 = 〈inl … news,move〉. +#sig * #Q1 #T1 #init1 #halt1 #M2 #M3 #acc #s #a #news #move +#Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans % +qed. + +lemma trans_if_liftM2 : ∀sig,M1,M2,M3,acc,s,a,news,move. + halt ? M2 s = false → + trans sig M2 〈s,a〉 = 〈news,move〉 → + trans sig (ifTM sig M1 M2 M3 acc) 〈inr … (inl … s),a〉 = 〈inr… (inl … news),move〉. +#sig #M1 * #Q2 #T2 #init2 #halt2 #M3 #acc #s #a #news #move +#Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans % +qed. + +lemma trans_if_liftM3 : ∀sig,M1,M2,M3,acc,s,a,news,move. + halt ? M3 s = false → + trans sig M3 〈s,a〉 = 〈news,move〉 → + trans sig (ifTM sig M1 M2 M3 acc) 〈inr … (inr … s),a〉 = 〈inr… (inr … news),move〉. +#sig #M1 * #Q2 #T2 #init2 #halt2 #M3 #acc #s #a #news #move +#Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans % +qed. + +lemma step_if_liftM1 : ∀sig,M1,M2,M3,acc,c0. + halt ? M1 (cstate ?? c0) = false → + step sig (ifTM sig M1 M2 M3 acc) (lift_confL sig (states ? M1) ? c0) = + lift_confL sig (states ? M1) ? (step sig M1 c0). +#sig #M1 #M2 #M3 #acc * #s #t + lapply (refl ? (trans ?? 〈s,current sig t〉)) + cases (trans ?? 〈s,current sig t〉) in ⊢ (???% → %); + #s0 #m0 cases t + [ #Heq #Hhalt + | 2,3: #s1 #l1 #Heq #Hhalt + |#ls #s1 #rs #Heq #Hhalt ] + whd in ⊢ (???(????%)); >Heq whd in ⊢ (???%); + whd in ⊢ (??(???%)?); whd in ⊢ (??%?); >(trans_if_liftM1 … Hhalt Heq) // +qed. + +lemma step_if_liftM2 : ∀sig,M1,M2,M3,acc,c0. + halt ? M2 (cstate ?? c0) = false → + step sig (ifTM sig M1 M2 M3 acc) (lift_confR sig ?? (lift_confL sig ?? c0)) = + lift_confR sig ?? (lift_confL sig ?? (step sig M2 c0)). +#sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 #M3 #acc * #s #t + lapply (refl ? (trans ?? 〈s,current sig t〉)) + cases (trans ?? 〈s,current sig t〉) in ⊢ (???% → %); + #s0 #m0 cases t + [ #Heq #Hhalt + | 2,3: #s1 #l1 #Heq #Hhalt + |#ls #s1 #rs #Heq #Hhalt ] + whd in match (step ? M2 ?); >Heq whd in ⊢ (???%); + whd in ⊢ (??(???%)?); whd in ⊢ (??%?); >(trans_if_liftM2 … Hhalt Heq) // +qed. + +lemma step_if_liftM3 : ∀sig,M1,M2,M3,acc,c0. + halt ? M3 (cstate ?? c0) = false → + step sig (ifTM sig M1 M2 M3 acc) (lift_confR sig ?? (lift_confR sig ?? c0)) = + lift_confR sig ?? (lift_confR sig ?? (step sig M3 c0)). +#sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 #M3 #acc * #s #t + lapply (refl ? (trans ?? 〈s,current sig t〉)) + cases (trans ?? 〈s,current sig t〉) in ⊢ (???% → %); + #s0 #m0 cases t + [ #Heq #Hhalt + | 2,3: #s1 #l1 #Heq #Hhalt + |#ls #s1 #rs #Heq #Hhalt ] + whd in match (step ? M3 ?); >Heq whd in ⊢ (???%); + whd in ⊢ (??(???%)?); whd in ⊢ (??%?); >(trans_if_liftM3 … Hhalt Heq) // +qed. + +lemma trans_if_M1true_acc : ∀sig,M1,M2,M3,acc,s,a. + halt ? M1 s = true → s==acc = true → + trans sig (ifTM sig M1 M2 M3 acc) 〈inl … s,a〉 = 〈inr … (inl … (start ? M2)),None ?〉. +#sig #M1 #M2 #M3 #acc #s #a #Hhalt #Hacc whd in ⊢ (??%?); >Hhalt >Hacc % +qed. + +lemma trans_if_M1true_notacc : ∀sig,M1,M2,M3,acc,s,a. + halt ? M1 s = true → s==acc = false → + trans sig (ifTM sig M1 M2 M3 acc) 〈inl … s,a〉 = 〈inr … (inr … (start ? M3)),None ?〉. +#sig #M1 #M2 #M3 #acc #s #a #Hhalt #Hacc whd in ⊢ (??%?); >Hhalt >Hacc % +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 → + 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 +cases (true_or_false (cstate ?? outc1 == acc)) #Hacc + [cases (HR2 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM2 + @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confL … outc2))) % + [@(loop_merge ????????? + (mk_config ? (FinSum (states sig M1) (FinSum (states sig M2) (states sig M3))) + (inr (states sig M1) ? (inl (states sig M2) (states sig M3) (start sig M2))) (ctape ?? outc1) ) + ? + (loop_lift ??? + (lift_confL sig (states ? M1) (FinSum (states ? M2) (states ? M3))) + (step sig M1) (step sig (ifTM sig M1 M2 M3 acc)) + (λc.halt sig M1 (cstate … c)) + (λc.halt_liftL ?? (halt sig M1) (cstate … c)) + … Hloop1)) + [* * + [ #sl #tl whd in ⊢ (??%? → ?); #Hl % + | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ] + |#c0 #Hhalt >(step_if_liftM1 … Hhalt) // + |#x (config_expand ?? outc1); + whd in match (lift_confL ????); + >(trans_if_M1true_acc … Hacc) + [% | @(loop_Some ?????? Hloop1)] + |cases outc1 #s1 #t1 % + |@(loop_lift ??? + (λc.(lift_confR … (lift_confL sig (states ? M2) (states ? M3) c))) + … Hloop2) + [ * #s2 #t2 % + | #c0 #Hhalt >(step_if_liftM2 … Hhalt) // ] + ] + |%1 @(ex_intro … (ctape ?? outc1)) % + [@HMtrue @(\P Hacc) | >(config_expand ?? outc2) @HM2 ] + ] + |cases (HR3 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM3 + @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confR … outc2))) % + [@(loop_merge ????????? + (mk_config ? (FinSum (states sig M1) (FinSum (states sig M2) (states sig M3))) + (inr (states sig M1) ? (inr (states sig M2) (states sig M3) (start sig M3))) (ctape ?? outc1) ) + ? + (loop_lift ??? + (lift_confL sig (states ? M1) (FinSum (states ? M2) (states ? M3))) + (step sig M1) (step sig (ifTM sig M1 M2 M3 acc)) + (λc.halt sig M1 (cstate … c)) + (λc.halt_liftL ?? (halt sig M1) (cstate … c)) + … Hloop1)) + [* * + [ #sl #tl whd in ⊢ (??%? → ?); #Hl % + | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ] + |#c0 #Hhalt >(step_if_liftM1 … Hhalt) // + |#x (config_expand ?? outc1); + whd in match (lift_confL ????); + >(trans_if_M1true_notacc … Hacc) + [% | @(loop_Some ?????? Hloop1)] + |cases outc1 #s1 #t1 % + |@(loop_lift ??? + (λc.(lift_confR … (lift_confR sig (states ? M2) (states ? M3) c))) + … Hloop2) + [ * #s2 #t2 % + | #c0 #Hhalt >(step_if_liftM3 … Hhalt) // ] + ] + |%2 @(ex_intro … (ctape ?? outc1)) % + [@HMfalse @(\Pf Hacc) | >(config_expand ?? outc2) @HM3 ] + ] + ] +qed. + lemma sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,acc. - accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 → - (∀t1,t2,t3. (Rtrue t1 t3 ∧ R2 t3 t2) ∨ (Rfalse t1 t3 ∧ R3 t3 t2) → R4 t1 t2) → - Realize sig - (ifTM sig M1 M2 M3 acc) R4. + accRealize sig M1 acc Rtrue Rfalse → M2 ⊨ R2 → M3 ⊨ R3 → + (∀t1,t2,t3. (Rtrue t1 t3 → R2 t3 t2) ∨ (Rfalse t1 t3 → R3 t3 t2) → R4 t1 t2) → + ifTM sig M1 M2 M3 acc ⊨ R4. #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #R4 #acc #HRacc #HRtrue #HRfalse #Hsub #t cases (sem_if … HRacc HRtrue HRfalse t) @@ -72,9 +221,10 @@ lemma sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,acc. [* #t3 * #Hleft #Hright @(Hsub … t3) %1 /2/ |* #t3 * #Hleft #Hright @(Hsub … t3) %2 /2/ ] qed. - + +(* e ancora usato ??? *) axiom acc_sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc. - accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 → + 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))) @@ -97,54 +247,3 @@ lemma acc_sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,R5,acc. |#H cases (Houtc1 H) #t3 * #Hleft #Hright @Hsub1 // ] |#H cases (Houtc2 H) #t3 * #Hleft #Hright @Hsub2 // ] qed. - -(* -#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 - [cases (HR2 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM2 - @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confL … outc2))) - % - [@(loop_merge ??????????? - (loop_lift ??? - (lift_confL sig (states ? M1) (FinSum (states ? M2) (states ? M3))) - (step sig M1) (step sig (ifTM sig M1 M2 M3 acc)) - (λc.halt sig M1 (cstate … c)) - (λc.halt_liftL ?? (halt sig M1) (cstate … c)) - … Hloop1)) - [* * - [ #sl #tl whd in ⊢ (??%? → ?); #Hl % - | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ] - || #c0 #Hhalt @daemon (* (trans_liftL_true sig M1 M2 ??) - [ whd in ⊢ (??%?); whd in ⊢ (???%); - @daemon -(* @config_eq whd in ⊢ (???%); // *) - | @(loop_Some ?????? Hloop10) - | @tdaemon - | skip ] - ] - | - |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. -*) \ No newline at end of file diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma index 88ec04e1c..a192f608e 100644 --- a/matita/matita/lib/turing/mono.ma +++ b/matita/matita/lib/turing/mono.ma @@ -84,7 +84,18 @@ record config (sig,states:FinSet): Type[0] ≝ { cstate : states; ctape: tape sig }. + +lemma config_expand: ∀sig,Q,c. + c = mk_config sig Q (cstate ?? c) (ctape ?? c). +#sig #Q * // +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. + definition step ≝ λsig.λM:TM sig.λc:config sig (states sig M). let current_char ≝ current ? (ctape ?? c) in let 〈news,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in @@ -172,6 +183,28 @@ lemma loop_eq : ∀sig,f,q,i,j,a,x,y. ] 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 + [#a #b normalize #Hfalse destruct + |#k0 #IH #a #b whd in ⊢ (??%? → ?); cases (true_or_false (p a)) #Hpa + [ >Hpa normalize #H1 destruct // | >Hpa normalize @IH ] + ] +qed. + +lemma loop_lift : ∀A,B,k,lift,f,g,h,hlift,c1,c2. + (∀x.hlift (lift x) = h x) → + (∀x.h x = false → lift (f x) = g (lift x)) → + loop A k f h c1 = Some ? c2 → + loop B k g hlift (lift c1) = Some ? (lift … c2). +#A #B #k #lift #f #g #h #hlift #c1 #c2 #Hfg #Hhlift +generalize in match c1; elim k +[#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse) +|#k0 #IH #c0 whd in ⊢ (??%? → ??%?); + cases (true_or_false (h c0)) #Hc0 >Hfg >Hc0 normalize + [ #Heq destruct (Heq) % | Hhalt >Htrans % qed. -lemma trans_liftR : ∀sig,M1,M2,s,a,news,move. +lemma trans_seq_liftR : ∀sig,M1,M2,s,a,news,move. halt ? M2 s = false → trans sig M2 〈s,a〉 = 〈news,move〉 → trans sig (seq sig M1 M2) 〈inr … s,a〉 = 〈inr … news,move〉. @@ -306,14 +339,7 @@ lemma trans_liftR : ∀sig,M1,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_confR : ∀sig,M1,M2,c0. +lemma step_seq_liftR : ∀sig,M1,M2,c0. halt ? M2 (cstate ?? c0) = false → step sig (seq sig M1 M2) (lift_confR sig (states ? M1) (states ? M2) c0) = lift_confR sig (states ? M1) (states ? M2) (step sig M2 c0). @@ -325,10 +351,10 @@ lemma step_lift_confR : ∀sig,M1,M2,c0. | 2,3: #s1 #l1 #Heq #Hhalt |#ls #s1 #rs #Heq #Hhalt ] whd in ⊢ (???(????%)); >Heq whd in ⊢ (???%); - whd in ⊢ (??(???%)?); whd in ⊢ (??%?); >(trans_liftR … Heq) // + whd in ⊢ (??(???%)?); whd in ⊢ (??%?); >(trans_seq_liftR … Heq) // qed. -lemma step_lift_confL : ∀sig,M1,M2,c0. +lemma step_seq_liftL : ∀sig,M1,M2,c0. halt ? M1 (cstate ?? c0) = false → step sig (seq sig M1 M2) (lift_confL sig (states ? M1) (states ? M2) c0) = lift_confL sig ?? (step sig M1 c0). @@ -340,31 +366,9 @@ lemma step_lift_confL : ∀sig,M1,M2,c0. | 2,3: #s1 #l1 #Heq #Hhalt |#ls #s1 #rs #Heq #Hhalt ] whd in ⊢ (???(????%)); >Heq whd in ⊢ (???%); - whd in ⊢ (??(???%)?); whd in ⊢ (??%?); >(trans_liftL … Heq) // + whd in ⊢ (??(???%)?); whd in ⊢ (??%?); >(trans_seq_liftL … Heq) // qed. -lemma loop_lift : ∀A,B,k,lift,f,g,h,hlift,c1,c2. - (∀x.hlift (lift x) = h x) → - (∀x.h x = false → lift (f x) = g (lift x)) → - loop A k f h c1 = Some ? c2 → - loop B k g hlift (lift c1) = Some ? (lift … c2). -#A #B #k #lift #f #g #h #hlift #c1 #c2 #Hfg #Hhlift -generalize in match c1; elim k -[#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse) -|#k0 #IH #c0 whd in ⊢ (??%? → ??%?); - cases (true_or_false (h c0)) #Hc0 >Hfg >Hc0 normalize - [ #Heq destruct (Heq) % | Hpa normalize #H1 destruct // | >Hpa normalize @IH ] - ] -qed. - lemma trans_liftL_true : ∀sig,M1,M2,s,a. halt ? M1 s = true → trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inr … (start ? M2),None ?〉. @@ -396,12 +400,12 @@ cases (HR2 (ctape sig (states ? M1) outc1)) #k2 * #outc2 * #Hloop2 #HM2 [ * * [ #sl #tl whd in ⊢ (??%? → ?); #Hl % | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ] - || #c0 #Hhalt (trans_liftL_true sig M1 M2 ??) @@ -414,3 +418,10 @@ cases (HR2 (ctape sig (states ? M1) outc1)) #k2 * #outc2 * #Hloop2 #HM2 ] qed. +theorem sem_seq_app: ∀sig.∀M1,M2:TM sig.∀R1,R2,R3. + M1 ⊨ R1 → M2 ⊨ R2 → R1 ∘ R2 ⊆ R3 → M1 · M2 ⊨ R3. +#sig #M1 #M2 #R1 #R2 #R3 #HR1 #HR2 #Hsub +#t cases (sem_seq … HR1 HR2 t) +#k * #outc * #Hloop #Houtc @(ex_intro … k) @(ex_intro … outc) +% [@Hloop |@Hsub @Houtc] +qed. -- 2.39.2