From d17dfeccb51f1dd6f94645018c15078ef4d329a4 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 6 Jun 2012 09:07:48 +0000 Subject: [PATCH] swap machine; move_char revisited --- matita/matita/lib/turing/basic_machines.ma | 52 +++++++++++++++++++ .../lib/turing/universal/move_char_l.ma | 37 +++++++++++-- .../matita/lib/turing/universal/move_tape.ma | 2 +- 3 files changed, 87 insertions(+), 4 deletions(-) diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma index 5612353a8..1d873ee86 100644 --- a/matita/matita/lib/turing/basic_machines.ma +++ b/matita/matita/lib/turing/basic_machines.ma @@ -185,3 +185,55 @@ lemma sem_test_char : ] qed. +(************************************* swap ***********************************) +definition swap_states : FinSet → FinSet ≝ + λalpha:FinSet.FinProd (initN 4) alpha. + +definition swap0 : initN 4 ≝ mk_Sig ?? 0 (leb_true_to_le 1 4 (refl …)). +definition swap1 : initN 4 ≝ mk_Sig ?? 1 (leb_true_to_le 2 4 (refl …)). +definition swap2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)). +definition swap3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)). + +definition swap ≝ + λalpha:FinSet.λfoo:alpha. + mk_TM alpha (swap_states alpha) + (λp.let 〈q,a〉 ≝ p in + let 〈q',b〉 ≝ q in + let q' ≝ pi1 nat (λi.i<4) q' in (* perche' devo passare il predicato ??? *) + match a with + [ None ⇒ 〈〈swap3,foo〉,None ?〉 (* if tape is empty then stop *) + | Some a' ⇒ + match q' with + [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? 〈a',R〉〉 (* save in register and move R *) + | S q' ⇒ match q' with + [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? 〈b,L〉〉 (* swap with register and move L *) + | S q' ⇒ match q' with + [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? 〈b,N〉〉 (* copy from register and stay *) + | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?〉 (* final state *) + ] + ] + ]]) + 〈swap0,foo〉 + (λq.\fst q == swap3). + +definition Rswap ≝ + λalpha,t1,t2. + ∀a,b,ls,rs. + t1 = midtape alpha ls b (a::rs) → + t2 = midtape alpha ls a (b::rs). + +lemma sem_swap : ∀alpha,foo. + swap alpha foo ⊨ Rswap alpha. +#alpha #foo * + [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?))) + % [% |#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] + |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0))) + % [% |#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 // + ] + ] +qed. diff --git a/matita/matita/lib/turing/universal/move_char_l.ma b/matita/matita/lib/turing/universal/move_char_l.ma index 2fa78ec6a..b85385705 100644 --- a/matita/matita/lib/turing/universal/move_char_l.ma +++ b/matita/matita/lib/turing/universal/move_char_l.ma @@ -12,7 +12,8 @@ (* MOVE_CHAR (left) MACHINE -Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra. +Sposta il carattere binario su cui si trova la testina appena prima del primo # +alla sua sinistra. Input: (ls,cs,rs can be empty; # is a parameter) @@ -31,7 +32,8 @@ Final state = 〈4,#〉 *) -include "turing/while_machine.ma". +include "turing/basic_machines.ma". +include "turing/if_machine.ma". definition mcl_states : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 5) alpha. @@ -41,6 +43,12 @@ definition mcl2 : initN 5 ≝ mk_Sig ?? 2 (leb_true_to_le 3 5 (refl …)). definition mcl3 : initN 5 ≝ mk_Sig ?? 3 (leb_true_to_le 4 5 (refl …)). definition mcl4 : initN 5 ≝ mk_Sig ?? 4 (leb_true_to_le 5 5 (refl …)). +definition mcl_step ≝ λalpha:FinSet.λsep:alpha. + ifTM alpha (test_char ? (λc.¬c==sep)) + (single_finalTM … (seq … (swap alpha sep) (move_l ?))) (nop ?) tc_true. + + +(* definition mcl_step ≝ λalpha:FinSet.λsep:alpha. mk_TM alpha (mcl_states alpha) @@ -101,6 +109,7 @@ lemma mcl_q2_q3 : (tape_move_left alpha ls a rs). #alpha #sep #a #ls #a0 * // qed. +*) definition Rmcl_step_true ≝ λalpha,sep,t1,t2. @@ -113,7 +122,7 @@ definition Rmcl_step_false ≝ λalpha,sep,t1,t2. right ? t1 ≠ [] → current alpha t1 ≠ None alpha → current alpha t1 = Some alpha sep ∧ t2 = t1. - +(* lemma mcl_trans_init_sep: ∀alpha,sep,x. trans ? (mcl_step alpha sep) 〈〈mcl0,x〉,Some ? sep〉 = 〈〈mcl4,sep〉,None ?〉. @@ -125,7 +134,29 @@ lemma mcl_trans_init_not_sep: trans ? (mcl_step alpha sep) 〈〈mcl0,x〉,Some ? y〉 = 〈〈mcl1,y〉,Some ? 〈y,R〉〉. #alpha #sep #x #y #H1 normalize >H1 // qed. +*) +lemma sem_mcl_step : + ∀alpha,sep. + mcl_step alpha sep ⊨ + [inr … (inl … (inr … start_nop)): Rmcl_step_true alpha sep, Rmcl_step_false alpha sep]. +#alpha #sep + @(acc_sem_if_app … + (sem_test_char …) (sem_seq …(sem_swap …) (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 + |#intape #outtape #tapea whd in ⊢ (%→%→%); + cases (current alpha intape) + [#_ #_ #_ * #Hfalse @False_ind @Hfalse % + |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % // + lapply (injective_notb ? true csep) -csep #csep >(\P csep) + ] + + lemma sem_mcl_step : ∀alpha,sep. accRealize alpha (mcl_step alpha sep) diff --git a/matita/matita/lib/turing/universal/move_tape.ma b/matita/matita/lib/turing/universal/move_tape.ma index dad01b719..cd8a87c5f 100644 --- a/matita/matita/lib/turing/universal/move_tape.ma +++ b/matita/matita/lib/turing/universal/move_tape.ma @@ -9,7 +9,7 @@ \ / GNU General Public License Version 2 V_____________________________________________________________*) -(* include "turing/universal/move_char_c.ma". *) +include "turing/universal/move_char_c.ma". include "turing/universal/move_char_l.ma". include "turing/universal/tuples.ma". -- 2.39.2