X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmove_char.ma;h=297344d54140f180dc75d28f99d719ed073cf197;hb=45f2accd093c8d10eb692266f4c3c0c59cb22d8b;hp=a0bf18996055e573c3f4e08c46b4f101eefe6fe7;hpb=0716716134a7820a822561cd6c55d5e71412acfd;p=helm.git diff --git a/matita/matita/lib/turing/move_char.ma b/matita/matita/lib/turing/move_char.ma index a0bf18996..297344d54 100644 --- a/matita/matita/lib/turing/move_char.ma +++ b/matita/matita/lib/turing/move_char.ma @@ -35,17 +35,20 @@ definition mcr_step ≝ λalpha:FinSet.λsep:alpha. (single_finalTM … (swap_l alpha sep · move_r ?)) (nop ?) tc_true. definition Rmcr_step_true ≝ - λalpha,sep,t1,t2. - ∀a,b,ls,rs. - t1 = midtape alpha (a::ls) b rs → - b ≠ sep ∧ - t2 = mk_tape alpha (a::b::ls) (option_hd ? rs) (tail ? rs). + λalpha,sep,t1,t2. + ∃b. b ≠ sep ∧ + ((∃a,ls,rs. + t1 = midtape alpha (a::ls) b rs ∧ + t2 = mk_tape alpha (a::b::ls) (option_hd ? rs) (tail ? rs)) ∨ + (∃rs. + t1 = midtape alpha [ ] b rs ∧ + t2 = leftof alpha b rs)). definition Rmcr_step_false ≝ λalpha,sep,t1,t2. left ? t1 ≠ [] → current alpha t1 ≠ None alpha → current alpha t1 = Some alpha sep ∧ t2 = t1. - + lemma sem_mcr_step : ∀alpha,sep. mcr_step alpha sep ⊨ @@ -53,18 +56,25 @@ lemma sem_mcr_step : #alpha #sep @(acc_sem_if_app … (sem_test_char …) (sem_seq …(sem_swap_l …) (sem_move_r …)) (sem_nop …)) - [#intape #outtape #tapea whd in ⊢ (%→%→%); - #Htapea * #tapeb * whd in ⊢ (%→%→?); - #Htapeb #Houttape #a #b #ls #rs #Hintape - >Hintape in Htapea; #Htapea cases (Htapea ? (refl …)) -Htapea - #Hbsep #Htapea % [@(\Pf (injective_notb ? false Hbsep))] - @Houttape @Htapeb // + [#intape #outtape #tapea whd in ⊢ (%→%→%); * * #c * + #Hcur cases (current_to_midtape … Hcur) #ls * #rs #Hintape + #csep #Htapea * #tapeb * #Hswap #Hmove @(ex_intro … c) % + [@(\Pf (injective_notb ? false csep))] + generalize in match Hintape; -Hintape cases ls + [#Hintape %2 @(ex_intro …rs) % // + >Htapea in Hswap; >Hintape + whd in ⊢ (%→?); * #Hswap #_ >(Hswap … (refl …)) in Hmove; + whd in ⊢ (%→?); * #Hmove #_ >Hmove // + |#a #ls1 #Hintape %1 + @(ex_intro … a) @(ex_intro … ls1) @(ex_intro … rs) % // + @(proj2 … Hmove) @(proj2 … Hswap) >Htapea // + ] |#intape #outtape #tapea whd in ⊢ (%→%→%); cases (current alpha intape) [#_ #_ #_ * #Hfalse @False_ind @Hfalse % - |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % // + |#c * #H1 #H2 #Htapea #_ #_ % // lapply (H1 c (refl …)) #csep lapply (injective_notb ? true csep) -csep #csep >(\P csep) // - ] + ] ] qed. @@ -79,14 +89,14 @@ definition R_move_char_r ≝ (∀rs1,rs2.rs = rs1@sep::rs2 → b ≠ sep → memb ? sep rs1 = false → t2 = midtape alpha (a::reverse ? rs1@b::ls) sep rs2). - + lemma sem_move_char_r : ∀alpha,sep. WRealize alpha (move_char_r alpha sep) (R_move_char_r alpha sep). #alpha #sep #inc #i #outc #Hloop lapply (sem_while … (sem_mcr_step alpha sep) inc i outc Hloop) [%] -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar) -[ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea +[ whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea % [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??) [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2)] @@ -95,63 +105,68 @@ lapply (sem_while … (sem_mcr_step alpha sep) inc i outc Hloop) [%] [#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct % |*:% #H2 normalize in H2; destruct (H2) ] ] -| #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse - lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH - #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea) - #Ha0 #Htapeb % - [ #Hfalse @False_ind @(absurd ?? Ha0) // - | * - [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ (* normalize *) - >Hrs in Htapeb; #Htapeb normalize in Htapeb; - cases (IH … Htapeb) #Houtc #_ >Houtc normalize // - | #r0 #rs0 #rs2 #Hrs #_ #Hrs0 +| #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse + lapply (IH HRfalse) -IH -HRfalse whd in ⊢ (%→%); #IH + #b0 #a0 #ls #rs #Htapea cases Hstar1 #b * #bsep * + [* #a * #ls1 * #rs1 * >Htapea #H destruct (H) #Htapeb % + [#Hb @False_ind /2/ + |* (* by cases on rs1 *) + [#rs2 whd in ⊢ (???%→?); #Hrs #_ #_ (* normalize *) + >Hrs in Htapeb; #Htapeb normalize in Htapeb; + cases (IH … Htapeb) #Houtc #_ >Houtc normalize // + |#r0 #rs0 #rs2 #Hrs #_ #Hrs0 cut (r0 ≠ sep ∧ memb … sep rs0 = false) - [ % - [ % #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct - | whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse - [ destruct - | @Hfalse ] - ] - ] * + [% + [% #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct + |whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse + [ destruct | @Hfalse ]] + ] * #Hr0 -Hrs0 #Hrs0 >Hrs in Htapeb; normalize in ⊢ (%→?); #Htapeb cases (IH … Htapeb) -IH #_ #IH >reverse_cons >associative_append @IH // - ] - ] + ] + ] + |* #rs1 * >Htapea #H destruct (H) + ] qed. -lemma terminate_move_char_r : - ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha (a::ls) b rs → - (b = sep ∨ memb ? sep rs = true) → Terminate alpha (move_char_r alpha sep) t. -#alpha #sep #t #b #a #ls #rs #Ht #Hsep -@(terminate_while … (sem_mcr_step alpha sep)) - [% - |generalize in match Hsep; -Hsep - generalize in match Ht; -Ht - generalize in match ls; -ls - generalize in match a; -a - generalize in match b; -b - generalize in match t; -t - elim rs - [#t #b #a #ls #Ht #Hsep % #tinit - whd in ⊢ (%→?); #H @False_ind - cases (H … Ht) #Hb #_ cases Hb #eqb @eqb - cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct - |#r0 #rs0 #Hind #t #b #a #ls #Ht #Hsep % #tinit - whd in ⊢ (%→?); #H - cases (H … Ht) #Hbsep #Htinit - @(Hind … Htinit) cases Hsep - [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb) - [#eqsep %1 >(\P eqsep) // | #H %2 //] - ] +lemma WF_mcr_niltape: + ∀alpha,sep. WF ? (inv ? (Rmcr_step_true alpha sep)) (niltape alpha). +#alpha #sep @wf #t1 whd in ⊢ (%→?); * #b * #_ * + [* #a * #ls * #rs * #H destruct | * #rs * #H destruct ] +qed. + +lemma WF_mcr_rightof: + ∀alpha,sep,a,ls. WF ? (inv ? (Rmcr_step_true alpha sep)) (rightof alpha a ls). +#alpha #sep #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ * + [* #a * #ls * #rs * #H destruct | * #rs * #H destruct ] qed. -(* NO GOOD: we must stop if current = None too!!! *) +lemma WF_mcr_leftof: + ∀alpha,sep,a,rs. WF ? (inv ? (Rmcr_step_true alpha sep)) (leftof alpha a rs). +#alpha #sep #a #rs @wf #t1 whd in ⊢ (%→?); * #b * #_ * + [* #a * #ls * #rs * #H destruct | * #rs * #H destruct ] +qed. -axiom ssem_move_char_r : +lemma terminate_move_char_r : + ∀alpha,sep.∀t. Terminate alpha (move_char_r alpha sep) t. +#alpha #sep #t @(terminate_while … (sem_mcr_step alpha sep)) [%] +cases t // #ls #c #rs generalize in match ls; generalize in match c; elim rs + [#c1 #l1 @wf #t1 whd in ⊢ (%→?); * #b * #bsep * + [* #a * #ls1 * #rs1 * #H destruct #Ht1 >Ht1 // + |* #rs1 * #_ #Ht1 >Ht1 // + ] + |#a #ls1 #Hind #c1 #l1 @wf #t1 whd in ⊢ (%→?); * #b * #bsep * + [* #a * #ls1 * #rs1 * #H destruct whd in ⊢ ((???%)→?); #Ht1 >Ht1 @Hind + |* #rs1 * #_ #Ht1 >Ht1 // + ] +qed. + +lemma ssem_move_char_r : ∀alpha,sep. Realize alpha (move_char_r alpha sep) (R_move_char_r alpha sep). +/2/ qed. (******************************* move_char_l **********************************) @@ -173,51 +188,57 @@ Final state = 〈4,#〉 *) -include "turing/basic_machines.ma". -include "turing/if_machine.ma". - definition mcl_step ≝ λalpha:FinSet.λsep:alpha. ifTM alpha (test_char ? (λc.¬c==sep)) (single_finalTM … (swap_r alpha sep · move_l ?)) (nop ?) tc_true. - -definition Rmcl_step_true ≝ - λalpha,sep,t1,t2. - ∀a,b,ls,rs. - t1 = midtape alpha ls b (a::rs) → - b ≠ sep ∧ - t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a::b::rs). +definition Rmcl_step_true ≝ + λalpha,sep,t1,t2. + ∃b. b ≠ sep ∧ + ((∃a,ls,rs. + t1 = midtape alpha ls b (a::rs) ∧ + t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a::b::rs)) ∨ + (∃ls. + t1 = midtape alpha ls b [ ] ∧ + t2 = rightof alpha b ls)). + definition Rmcl_step_false ≝ λalpha,sep,t1,t2. right ? t1 ≠ [] → current alpha t1 ≠ None alpha → current alpha t1 = Some alpha sep ∧ t2 = t1. - + definition mcls_acc: ∀alpha:FinSet.∀sep:alpha.states ? (mcl_step alpha sep) ≝ λalpha,sep.inr … (inl … (inr … start_nop)). lemma sem_mcl_step : ∀alpha,sep. mcl_step alpha sep ⊨ - [mcls_acc alpha sep: Rmcl_step_true alpha sep, Rmcl_step_false alpha sep]. + [mcls_acc ??: Rmcl_step_true alpha sep, Rmcl_step_false alpha sep]. #alpha #sep -@(acc_sem_if_app … - (sem_test_char …) (sem_seq …(sem_swap_r …) (sem_move_l …)) (sem_nop …)) - [#intape #outtape #tapea whd in ⊢ (%→%→%); - #Htapea * #tapeb * whd in ⊢ (%→%→?); - #Htapeb #Houttape #a #b #ls #rs #Hintape - >Hintape in Htapea; #Htapea cases (Htapea ? (refl …)) -Htapea - #Hbsep #Htapea % [@(\Pf (injective_notb ? false Hbsep))] - @Houttape @Htapeb // + @(acc_sem_if_app … + (sem_test_char …) (sem_seq …(sem_swap_r …) (sem_move_l …)) (sem_nop …)) + [#intape #outtape #tapea whd in ⊢ (%→%→%); * * #c * + #Hcur cases (current_to_midtape … Hcur) #ls * #rs #Hintape + #csep #Htapea * #tapeb * #Hswap #Hmove @(ex_intro … c) % + [@(\Pf (injective_notb ? false csep))] + generalize in match Hintape; -Hintape cases rs + [#Hintape %2 @(ex_intro …ls) % // + >Htapea in Hswap; >Hintape + whd in ⊢ (%→?); * #Hswap #_ >(Hswap … (refl …)) in Hmove; + whd in ⊢ (%→?); * #Hmove #_ >Hmove // + |#a #rs1 #Hintape %1 + @(ex_intro … a) @(ex_intro … ls) @(ex_intro … rs1) % // + @(proj2 … Hmove) @(proj2 … Hswap) >Htapea // + ] |#intape #outtape #tapea whd in ⊢ (%→%→%); cases (current alpha intape) [#_ #_ #_ * #Hfalse @False_ind @Hfalse % - |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % // + |#c * #H1 #H2 #Htapea #_ #_ % // lapply (H1 c (refl …)) #csep lapply (injective_notb ? true csep) -csep #csep >(\P csep) // - ] + ] ] qed. - -(* the move_char (variant left) machine *) + definition move_char_l ≝ λalpha,sep.whileTM alpha (mcl_step alpha sep) (inr … (inl … (inr … start_nop))). @@ -228,83 +249,82 @@ definition R_move_char_l ≝ (∀ls1,ls2.ls = ls1@sep::ls2 → b ≠ sep → memb ? sep ls1 = false → t2 = midtape alpha ls2 sep (a::reverse ? ls1@b::rs)). - + lemma sem_move_char_l : ∀alpha,sep. WRealize alpha (move_char_l alpha sep) (R_move_char_l alpha sep). #alpha #sep #inc #i #outc #Hloop lapply (sem_while … (sem_mcl_step alpha sep) inc i outc Hloop) [%] -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar) -[ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea +[ whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea % [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??) - [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2) ] + [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2)] | #rs1 #rs2 #Hrs #Hb #Hrs1 - >Htapea in H1; (* normalize in ⊢ (% → ?); *) #H1 cases (H1 ??) - [ #Hfalse normalize in Hfalse; @False_ind @(absurd ?? Hb) destruct % - |*:% normalize #H2 destruct (H2) ] + >Htapea in H1; #H1 cases (H1 ??) + [#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct % + |*:% #H2 normalize in H2; destruct (H2) ] ] -| #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse - lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH - #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea) - #Ha0 #Htapeb % - [ #Hfalse @False_ind @(absurd ?? Ha0) // - | * - [ #ls2 whd in ⊢ (???%→?); #Hls #_ #_ - >Hls in Htapeb; #Htapeb normalize in Htapeb; - cases (IH … Htapeb) #Houtc #_ >Houtc normalize // - | #l0 #ls0 #ls2 #Hls #_ #Hls0 - cut (l0 ≠ sep ∧ memb … sep ls0 = false) - [ % - [ % #Hl0 >Hl0 in Hls0; >memb_hd #Hfalse destruct - | whd in Hls0:(??%?); cases (sep==l0) in Hls0; normalize #Hfalse - [ destruct - | @Hfalse ] - ] - ] * - #Hl0 -Hls0 #Hls0 >Hls in Htapeb; +| #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse + lapply (IH HRfalse) -IH -HRfalse whd in ⊢ (%→%); #IH + #b0 #a0 #ls #rs #Htapea cases Hstar1 #b * #bsep * + [* #a * #ls1 * #rs1 * >Htapea #H destruct (H) #Htapeb % + [#Hb @False_ind /2/ + |* (* by cases on ls1 *) + [#rs2 whd in ⊢ (???%→?); #Hrs #_ #_ (* normalize *) + >Hrs in Htapeb; #Htapeb normalize in Htapeb; + cases (IH … Htapeb) #Houtc #_ >Houtc normalize // + |#r0 #rs0 #rs2 #Hrs #_ #Hrs0 + cut (r0 ≠ sep ∧ memb … sep rs0 = false) + [% + [% #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct + |whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse + [ destruct | @Hfalse ]] + ] * + #Hr0 -Hrs0 #Hrs0 >Hrs in Htapeb; normalize in ⊢ (%→?); #Htapeb cases (IH … Htapeb) -IH #_ #IH >reverse_cons >associative_append @IH // - ] - ] + ] + ] + |* #rs1 * >Htapea #H destruct (H) + ] qed. -lemma terminate_move_char_l : - ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha ls b (a::rs) → - (b = sep ∨ memb ? sep ls = true) → Terminate alpha (move_char_l alpha sep) t. -#alpha #sep #t #b #a #ls #rs #Ht #Hsep -@(terminate_while … (sem_mcl_step alpha sep)) - [% - |generalize in match Hsep; -Hsep - generalize in match Ht; -Ht - generalize in match rs; -rs - generalize in match a; -a - generalize in match b; -b - generalize in match t; -t - elim ls - [#t #b #a #rs #Ht #Hsep % #tinit - whd in ⊢ (%→?); #H @False_ind - cases (H … Ht) #Hb #_ cases Hb #eqb @eqb - cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct - |#l0 #ls0 #Hind #t #b #a #rs #Ht #Hsep % #tinit - whd in ⊢ (%→?); #H - cases (H … Ht) #Hbsep #Htinit - @(Hind … Htinit) cases Hsep - [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb) - [#eqsep %1 >(\P eqsep) // | #H %2 //] - ] +lemma WF_mcl_niltape: + ∀alpha,sep. WF ? (inv ? (Rmcl_step_true alpha sep)) (niltape alpha). +#alpha #sep @wf #t1 whd in ⊢ (%→?); * #b * #_ * + [* #a * #ls * #rs * #H destruct | * #rs * #H destruct ] qed. -(* NO GOOD: we must stop if current = None too!!! -lemma ssem_move_char_l : - ∀alpha,sep. - Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep). -#alpha #sep * -[ %{5} % [| % [whd in ⊢ (??%?); - @WRealize_to_Realize // @terminate_move_char_l -*) +lemma WF_mcl_rightof: + ∀alpha,sep,a,ls. WF ? (inv ? (Rmcl_step_true alpha sep)) (rightof alpha a ls). +#alpha #sep #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ * + [* #a * #ls * #rs * #H destruct | * #rs * #H destruct ] +qed. + +lemma WF_mcl_leftof: + ∀alpha,sep,a,rs. WF ? (inv ? (Rmcl_step_true alpha sep)) (leftof alpha a rs). +#alpha #sep #a #rs @wf #t1 whd in ⊢ (%→?); * #b * #_ * + [* #a * #ls * #rs * #H destruct | * #rs * #H destruct ] +qed. + +lemma terminate_move_char_l : + ∀alpha,sep.∀t. Terminate alpha (move_char_l alpha sep) t. +#alpha #sep #t @(terminate_while … (sem_mcl_step alpha sep)) [%] +cases t // #ls elim ls + [#c1 #l1 @wf #t1 whd in ⊢ (%→?); * #b * #bsep * + [* #a * #ls1 * #rs1 * #H destruct #Ht1 >Ht1 // + |* #rs1 * #_ #Ht1 >Ht1 // + ] + |#a #ls1 #Hind #c1 #l1 @wf #t1 whd in ⊢ (%→?); * #b * #bsep * + [* #a * #ls1 * #rs1 * #H destruct whd in ⊢ ((???%)→?); #Ht1 >Ht1 @Hind + |* #rs1 * #_ #Ht1 >Ht1 // + ] +qed. -axiom ssem_move_char_l : +lemma ssem_move_char_l: ∀alpha,sep. Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep). +/2/ qed. +