From 1e797237a245f38a9674117b9d31ab76d8efe7cb Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Mon, 4 Feb 2013 15:46:19 +0000 Subject: [PATCH] converting certain basic machines to composed machines --- .../lib/turing/multi_universal/moves_2.ma | 48 ++++++++--------- matita/matita/lib/turing/simple_machines.ma | 51 +++++++++++-------- 2 files changed, 50 insertions(+), 49 deletions(-) diff --git a/matita/matita/lib/turing/multi_universal/moves_2.ma b/matita/matita/lib/turing/multi_universal/moves_2.ma index e56a0f183..a904414fa 100644 --- a/matita/matita/lib/turing/multi_universal/moves_2.ma +++ b/matita/matita/lib/turing/multi_universal/moves_2.ma @@ -13,6 +13,8 @@ include "turing/turing.ma". include "turing/inject.ma". include "turing/while_multi.ma". include "turing/while_machine.ma". +include "turing/simple_machines.ma". +include "turing/if_machine.ma". definition parmove_states ≝ initN 3. @@ -311,22 +313,10 @@ qed. else nop } *) - -definition mte_states ≝ initN 3. -definition mte0 : mte_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)). -definition mte1 : mte_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)). -definition mte2 : mte_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)). -definition mte_step ≝ - λalpha:FinSet.λD.mk_TM alpha mte_states - (λp.let 〈q,a〉 ≝ p in - match a with - [ None ⇒ 〈mte1,None ?,N〉 - | Some a' ⇒ match (pi1 … q) with - [ O ⇒ 〈mte2,Some ? a',D〉 - | S q ⇒ 〈mte2,None ?,N〉 ] ]) - mte0 (λq.q == mte1 ∨ q == mte2). - +definition mte_step ≝ λalpha,D. +ifTM ? (test_null alpha) (single_finalTM ? (move alpha D)) (nop ?) tc_true. + definition R_mte_step_true ≝ λalpha,D,t1,t2. ∃ls,c,rs. t1 = midtape alpha ls c rs ∧ t2 = tape_move ? t1 D. @@ -334,21 +324,25 @@ definition R_mte_step_true ≝ λalpha,D,t1,t2. definition R_mte_step_false ≝ λalpha.λt1,t2:tape alpha. current ? t1 = None ? ∧ t1 = t2. +definition mte2 : ∀alpha,D.states ? (mte_step alpha D) ≝ +λalpha,D.(inr … (inl … (inr … start_nop))). + lemma sem_mte_step : - ∀alpha,D.mte_step alpha D ⊨ [ mte2 : R_mte_step_true alpha D, R_mte_step_false alpha ] . -#alpha #D #intape @(ex_intro ?? 2) cases intape -[ @ex_intro - [| % [ % [ % | normalize #H destruct ] | #_ % // ] ] -|#a #al @ex_intro - [| % [ % [ % | normalize #H destruct ] | #_ % // ] ] -|#a #al @ex_intro - [| % [ % [ % | normalize #H destruct ] | #_ % // ] ] -| #ls #c #rs - @ex_intro [| % [ % [ % | #_ %{ls} %{c} %{rs} % // ] - | normalize in ⊢ (?(??%?)→?); * #H @False_ind /2/ ] ] ] + ∀alpha,D.mte_step alpha D ⊨ + [ mte2 … : R_mte_step_true alpha D, R_mte_step_false alpha ] . +#alpha #D #ta +@(acc_sem_if_app ??????????? (sem_test_null …) + (sem_move_single …) (sem_nop alpha) ??) +[ #tb #tc #td * #Hcurtb + lapply (refl ? (current ? tb)) cases (current ? tb) in ⊢ (???%→?); + [ #H @False_ind >H in Hcurtb; * /2/ ] + -Hcurtb #c #Hcurtb #Htb whd in ⊢ (%→?); #Htc whd + cases (current_to_midtape … Hcurtb) #ls * #rs #Hmidtb + %{ls} %{c} %{rs} % // +| #tb #tc #td * #Hcurtb #Htb whd in ⊢ (%→?); #Htc whd % // ] qed. -definition move_to_end ≝ λsig,D.whileTM sig (mte_step sig D) mte2. +definition move_to_end ≝ λsig,D.whileTM sig (mte_step sig D) (mte2 …). definition R_move_to_end_r ≝ λsig,int,outt. diff --git a/matita/matita/lib/turing/simple_machines.ma b/matita/matita/lib/turing/simple_machines.ma index 4b5198900..2cfaf7c7a 100644 --- a/matita/matita/lib/turing/simple_machines.ma +++ b/matita/matita/lib/turing/simple_machines.ma @@ -67,39 +67,46 @@ cases (acc_sem_inject … Hin (sem_test_null alpha) int) | @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) // #Hi0i @sym_eq @Hnth_j @sym_not_eq // ] ] qed. + (* move a single tape *) -definition mmove_states ≝ initN 2. +definition smove_states ≝ initN 2. -definition mmove0 : mmove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)). -definition mmove1 : mmove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)). +definition smove0 : smove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)). +definition smove1 : smove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)). -definition trans_mmove ≝ - λi,sig,n,D. - λp:mmove_states × (Vector (option sig) (S n)). +definition trans_smove ≝ + λsig,D. + λp:smove_states × (option sig). let 〈q,a〉 ≝ p in match (pi1 … q) with - [ O ⇒ 〈mmove1,change_vec ? (S n) (null_action ? n) (〈None ?,D〉) i〉 - | S _ ⇒ 〈mmove1,null_action sig n〉 ]. + [ O ⇒ 〈smove1,None sig, D〉 + | S _ ⇒ 〈smove1,None sig, N〉 ]. + +definition move ≝ + λsig,D.mk_TM sig smove_states (trans_smove sig D) smove0 (λq.q == smove1). + +definition mmove ≝ λi,sig,n,D.inject_TM sig (move sig D) n i. + +definition Rmove ≝ + λalpha,D,t1,t2. t2 = tape_move alpha t1 D. + +lemma sem_move_single : + ∀alpha,D.move alpha D ⊨ Rmove alpha D. +#alpha #D #int %{2} %{(mk_config ? smove_states smove1 ?)} [| % % ] +qed. -definition mmove ≝ - λi,sig,n,D. - mk_mTM sig n mmove_states (trans_mmove i sig n D) - mmove0 (λq.q == mmove1). - definition Rm_multi ≝ λalpha,n,i,D.λt1,t2:Vector ? (S n). t2 = change_vec ? (S n) t1 (tape_move alpha (nth i ? t1 (niltape ?)) D) i. - + lemma sem_move_multi : ∀alpha,n,i,D.i ≤ n → mmove i alpha n D ⊨ Rm_multi alpha n i D. -#alpha #n #i #D #Hin #int %{2} -%{(mk_mconfig ? mmove_states n mmove1 ?)} -[| % - [ whd in ⊢ (??%?); @eq_f whd in ⊢ (??%?); @eq_f % - | whd >tape_move_multi_def - <(change_vec_same … (ctapes …) i (niltape ?)) - >pmap_change tape_move_null_action % ] ] - qed. +#alpha #n #i #D #Hin #ta cases (sem_inject … Hin (sem_move_single alpha D) ta) +#k * #outc * #Hloop * whd in ⊢ (%→?); #Htb1 #Htb2 %{k} %{outc} % [ @Hloop ] +whd @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) #Hi0i +[ >Hi0i >Htb1 >nth_change_vec // +| >nth_change_vec_neq [|@sym_not_eq //]