From: Andrea Asperti Date: Wed, 27 Jun 2012 09:30:52 +0000 (+0000) Subject: Closed all axioms in turing (but not universal). X-Git-Tag: make_still_working~1630 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fd282412fff8f2529bb1dfb22a684f5c25af37cb;p=helm.git Closed all axioms in turing (but not universal). Revised semantics of basic machines for termination purposes --- diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma index 56a0bf4b1..1c1ce3020 100644 --- a/matita/matita/lib/turing/basic_machines.ma +++ b/matita/matita/lib/turing/basic_machines.ma @@ -50,22 +50,28 @@ definition move_r ≝ move0 (λq.q == move1). definition R_move_r ≝ λalpha,t1,t2. + (current ? t1 = None ? → t1 = t2) ∧ ∀ls,c,rs. - t1 = midtape alpha ls c rs → - t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs). + t1 = midtape alpha ls c rs → + t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs). +(* + (current ? t1 = None ? ∧ t1 = t2) ∨ + ∃ls,c,rs. + t1 = midtape alpha ls c rs ∧ + t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).*) lemma sem_move_r : ∀alpha.Realize ? (move_r alpha) (R_move_r alpha). #alpha #intape @(ex_intro ?? 2) cases intape [ @ex_intro - [| % [ % | #ls #c #rs #Hfalse destruct ] ] + [| % [ % | % // #ls #c #rs #H destruct ] ] |#a #al @ex_intro - [| % [ % | #ls #c #rs #Hfalse destruct ] ] + [| % [ % | % // #ls #c #rs #H destruct ] ] |#a #al @ex_intro - [| % [ % | #ls #c #rs #Hfalse destruct ] ] + [| % [ % | % // #ls #c #rs #H destruct ] ] | #ls #c #rs - @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1) - cases rs0 // ] ] ] + @ex_intro [| % [ % | % [whd in ⊢ ((??%?)→?); #H destruct] + #ls1 #c1 #rs1 #H destruct cases rs1 // ] ] ] qed. (******************** moves the head one step to the left *********************) @@ -79,24 +85,25 @@ definition move_l ≝ [ O ⇒ 〈move1,Some ? 〈a',L〉〉 | S q ⇒ 〈move1,None ?〉 ] ]) move0 (λq.q == move1). - + definition R_move_l ≝ λalpha,t1,t2. + (current ? t1 = None ? → t1 = t2) ∧ ∀ls,c,rs. - t1 = midtape alpha ls c rs → - t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs). + t1 = midtape alpha ls c rs → + t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs). lemma sem_move_l : ∀alpha.Realize ? (move_l alpha) (R_move_l alpha). #alpha #intape @(ex_intro ?? 2) cases intape [ @ex_intro - [| % [ % | #ls #c #rs #Hfalse destruct ] ] + [| % [ % | % // #ls #c #rs #H destruct ] ] |#a #al @ex_intro - [| % [ % | #ls #c #rs #Hfalse destruct ] ] + [| % [ % | % // #ls #c #rs #H destruct ] ] |#a #al @ex_intro - [| % [ % | #ls #c #rs #Hfalse destruct ] ] + [| % [ % | % // #ls #c #rs #H destruct ] ] | #ls #c #rs - @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1) - cases ls0 // ] ] ] + @ex_intro [| % [ % | % [whd in ⊢ ((??%?)→?); #H destruct] + #ls1 #c1 #rs1 #H destruct cases ls1 // ] ] ] qed. (********************************* test char **********************************) @@ -118,7 +125,7 @@ definition test_char ≝ mk_TM alpha tc_states (λp.let 〈q,a〉 ≝ p in match a with - [ None ⇒ 〈tc_true, None ?〉 + [ None ⇒ 〈tc_false, None ?〉 | Some a' ⇒ match test a' with [ true ⇒ 〈tc_true,None ?〉 @@ -127,11 +134,11 @@ definition test_char ≝ definition Rtc_true ≝ λalpha,test,t1,t2. - ∀c. current alpha t1 = Some ? c → test c = true ∧ t2 = t1. + (∃c. current alpha t1 = Some ? c ∧ test c = true) ∧ t2 = t1. definition Rtc_false ≝ λalpha,test,t1,t2. - ∀c. current alpha t1 = Some ? c → test c = false ∧ t2 = t1. + (∀c. current alpha t1 = Some ? c → test c = false) ∧ t2 = t1. lemma tc_q0_q1 : ∀alpha,test,ls,a0,rs. test a0 = true → @@ -159,19 +166,19 @@ lemma sem_test_char : tc_true (Rtc_true alpha test) (Rtc_false alpha test). #alpha #test * [ @(ex_intro ?? 2) - @(ex_intro ?? (mk_config ?? tc_true (niltape ?))) % - [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ] -| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_true (leftof ? a al))) - % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ] -| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_true (rightof ? a al))) - % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ] + @(ex_intro ?? (mk_config ?? tc_false (niltape ?))) % + [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ] +| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_false (leftof ? a al))) + % [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ] +| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_false (rightof ? a al))) + % [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ] | #ls #c #rs @(ex_intro ?? 2) cases (true_or_false (test c)) #Htest [ @(ex_intro ?? (mk_config ?? tc_true ?)) [| % [ % [ whd in ⊢ (??%?); >tc_q0_q1 // - | #_ #c0 #Hc0 % // normalize in Hc0; destruct // ] + | #_ % // @(ex_intro … c) /2/] | * #Hfalse @False_ind @Hfalse % ] ] | @(ex_intro ?? (mk_config ?? tc_false (midtape ? ls c rs))) @@ -179,7 +186,7 @@ lemma sem_test_char : [ % [ whd in ⊢ (??%?); >tc_q0_q2 // | whd in ⊢ ((??%%)→?); #Hfalse destruct (Hfalse) ] - | #_ #c0 #Hc0 % // normalize in Hc0; destruct (Hc0) // + | #_ % // #c0 whd in ⊢ ((??%?)→?); #Hc0 destruct (Hc0) // ] ] ] @@ -215,25 +222,30 @@ definition swap_r ≝ ]]) 〈swap0,foo〉 (λq.\fst q == swap3). - -definition Rswap ≝ + +definition Rswap_r ≝ λalpha,t1,t2. - ∀a,b,ls,rs. - t1 = midtape alpha ls b (a::rs) → - t2 = midtape alpha ls a (b::rs). + (∀b,ls. + t1 = midtape alpha ls b [ ] → + t2 = rightof ? b ls) ∧ + (∀a,b,ls,rs. + t1 = midtape alpha ls b (a::rs) → + t2 = midtape alpha ls a (b::rs)). lemma sem_swap_r : ∀alpha,foo. - swap_r alpha foo ⊨ Rswap alpha. + swap_r alpha foo ⊨ Rswap_r alpha. #alpha #foo * [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?))) - % [% |#a #b #ls #rs #H destruct] + % [% |% [#b #ls | #a #b #ls #rs] #H destruct] |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0))) - % [% |#a #b #ls #rs #H destruct] + % [% | % [#b #ls | #a #b #ls #rs] #H destruct] |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0))) - % [% |#a #b #ls #rs #H destruct] + % [% |% [#b #ls | #a #b #ls #rs] #H destruct] | #lt #c #rt @(ex_intro ?? 4) cases rt - [@ex_intro [|% [ % | #a #b #ls #rs #H destruct]] - |#r0 #rt0 @ex_intro [| % [ % | #a #b #ls #rs #H destruct // + [@ex_intro [|% [ % | % + [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]] + |#r0 #rt0 @ex_intro [| % [ % | % + [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize // ] ] qed. @@ -262,22 +274,27 @@ definition swap_l ≝ definition Rswap_l ≝ λalpha,t1,t2. - ∀a,b,ls,rs. - t1 = midtape alpha (a::ls) b rs → - t2 = midtape alpha (b::ls) a rs. + (∀b,rs. + t1 = midtape alpha [ ] b rs → + t2 = leftof ? b rs) ∧ + (∀a,b,ls,rs. + t1 = midtape alpha (a::ls) b rs → + t2 = midtape alpha (b::ls) a rs). lemma sem_swap_l : ∀alpha,foo. swap_l alpha foo ⊨ Rswap_l alpha. #alpha #foo * [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?))) - % [% |#a #b #ls #rs #H destruct] + % [% |% [#b #rs | #a #b #ls #rs] #H destruct] |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0))) - % [% |#a #b #ls #rs #H destruct] + % [% | % [#b #rs | #a #b #ls #rs] #H destruct] |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0))) - % [% |#a #b #ls #rs #H destruct] + % [% |% [#b #rs | #a #b #ls #rs] #H destruct] | #lt #c #rt @(ex_intro ?? 4) cases lt - [@ex_intro [|% [ % | #a #b #ls #rs #H destruct]] - |#l0 #lt0 @ex_intro [| % [ % | #a #b #ls #rs #H destruct // + [@ex_intro [|% [ % | % + [#b #rs #H destruct normalize // |#a #b #ls #rs #H destruct]]] + |#r0 #rt0 @ex_intro [| % [ % | % + [#b #rs #H destruct | #a #b #ls #rs #H destruct normalize // ] ] -qed. \ No newline at end of file +qed. diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma index e117fc7be..0fcbfbe48 100644 --- a/matita/matita/lib/turing/mono.ma +++ b/matita/matita/lib/turing/mono.ma @@ -47,6 +47,19 @@ definition mk_tape : | cons r0 rs0 ⇒ leftof ? r0 rs0 ] | cons l0 ls0 ⇒ rightof ? l0 ls0 ] ]. +lemma current_to_midtape: ∀sig,t,c. current sig t = Some ? c → + ∃ls,rs. t = midtape ? ls c rs. +#sig * + [#c whd in ⊢ ((??%?)→?); #Hfalse destruct + |#a #l #c whd in ⊢ ((??%?)→?); #Hfalse destruct + |#a #l #c whd in ⊢ ((??%?)→?); #Hfalse destruct + |#ls #a #rs #c whd in ⊢ ((??%?)→?); #H destruct + @(ex_intro … ls) @(ex_intro … rs) // + ] +qed. + +(*********************************** moves ************************************) + inductive move : Type[0] ≝ | L : move | R : move | N : move. diff --git a/matita/matita/lib/turing/move_char.ma b/matita/matita/lib/turing/move_char.ma index a0bf18996..e20591c5f 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,7 +89,7 @@ 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). @@ -96,62 +106,67 @@ lapply (sem_while … (sem_mcr_step alpha sep) inc i outc Hloop) [%] |*:% #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 + 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,7 +249,7 @@ 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). @@ -238,73 +259,72 @@ lapply (sem_while … (sem_mcl_step alpha sep) inc i outc Hloop) [%] [ #tapea 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; + 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. +