From 53656d48b302c50e775159dc62e56cd7b1550676 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Fri, 16 Nov 2012 17:03:13 +0000 Subject: [PATCH] Match machine (multi) --- matita/matita/lib/turing/basic_machines.ma | 2 +- matita/matita/lib/turing/inject.ma | 18 ++++ .../lib/turing/multi_universal/match.ma | 101 +++++++++++++++++- matita/matita/lib/turing/turing.ma | 54 ++++++++++ 4 files changed, 172 insertions(+), 3 deletions(-) diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma index 9790cb43c..82d4758c2 100644 --- a/matita/matita/lib/turing/basic_machines.ma +++ b/matita/matita/lib/turing/basic_machines.ma @@ -302,4 +302,4 @@ lemma sem_swap_l : ∀alpha,foo. [#b #rs #H destruct | #a #b #ls #rs #H destruct normalize // ] ] -qed. +qed. \ No newline at end of file diff --git a/matita/matita/lib/turing/inject.ma b/matita/matita/lib/turing/inject.ma index be40c5638..d7851d85f 100644 --- a/matita/matita/lib/turing/inject.ma +++ b/matita/matita/lib/turing/inject.ma @@ -132,4 +132,22 @@ theorem sem_inject: ∀sig.∀M:TM sig.∀R.∀n,i. |#j #i >nth_change_vec_neq // ] ] +qed. + +theorem acc_sem_inject: ∀sig.∀M:TM sig.∀Rtrue,Rfalse,acc.∀n,i. + i≤n → M ⊨ [ acc : Rtrue, Rfalse ] → + inject_TM sig M n i ⊨ [ acc : inject_R sig Rtrue n i, inject_R sig Rfalse n i ]. +#sig #M #Rtrue #Rfalse #acc #n #i #lein #HR #vt cases (HR (nth i ? vt (niltape ?))) +#k * * #outs #outt * * #Hloop #HRtrue #HRfalse @(ex_intro ?? k) +@(ex_intro ?? (mk_mconfig ?? n outs (change_vec ? (S n) vt outt i))) % [ % + [whd in ⊢ (??(?????%)?); <(change_vec_same ?? vt i (niltape ?)) in ⊢ (??%?); + @loop_inject /2 by refl, trans_eq, le_S_S/ + |#Hqtrue % + [>nth_change_vec /2 by le_S_S/ + |#j #Hneq >nth_change_vec_neq // + ] ] + |#Hqfalse % + [>nth_change_vec /2 by le_S_S/ @HRfalse @Hqfalse + |#j #Hneq >nth_change_vec_neq // + ] ] qed. \ No newline at end of file diff --git a/matita/matita/lib/turing/multi_universal/match.ma b/matita/matita/lib/turing/multi_universal/match.ma index b153ef8c7..d69540193 100644 --- a/matita/matita/lib/turing/multi_universal/match.ma +++ b/matita/matita/lib/turing/multi_universal/match.ma @@ -12,9 +12,10 @@ (* *) (**************************************************************************) -include "turing/turing.ma". +include "turing/multi_universal/moves.ma". +include "turing/if_multi.ma". include "turing/inject.ma". -include "turing/while_multi.ma". +include "turing/basic_machines.ma". definition compare_states ≝ initN 3. @@ -266,3 +267,99 @@ lemma sem_compare : ∀i,j,sig,n. #i #j #sig #n #Hneq #Hi #Hj @WRealize_to_Realize /2/ qed. +(* + |conf1 $ + |confin 0/1 confout move + + match machine step ≝ + compare; + if (cur(src) != $) + then + parmoveL; + moveR(dst); + else nop + *) + +definition match_step ≝ λsrc,dst,sig,n,is_startc,is_endc. + compare src dst sig n · + (ifTM ?? (inject_TM ? (test_char ? is_endc) n src) + (single_finalTM ?? + (parmove src dst sig n L is_startc · (inject_TM ? (move_r ?) n dst))) + (nop ? n) + tc_false). + +definition R_match_step_false ≝ + λsrc,dst,sig,n,is_endc.λint,outt: Vector (tape sig) (S n). + ∃ls,ls0,rs,rs0,x,xs,end,c. + is_endc end = true ∧ + nth src ? int (niltape ?) = midtape sig ls x (xs@end::rs) ∧ + nth dst ? int (niltape ?) = midtape sig ls0 x (xs@c::rs0) ∧ + outt = change_vec ?? + (change_vec ?? int (midtape sig (reverse ? xs@x::ls) end rs) src) + (midtape sig (reverse ? xs@x::ls0) c rs0) dst. + +(* + src : | +*) + +definition R_match_step_true ≝ + λsrc,dst,sig,n,is_startc,is_endc.λint,outt: Vector (tape sig) (S n). + ∀s.current sig (nth src (tape sig) int (niltape sig)) = Some ? s → + is_startc s = true → + (∀s1.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s1 → + s ≠ s1 → + outt = change_vec ?? int + (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈s1,R〉)) dst ∧ is_endc s = false) ∧ + (∀ls,x,xs,ci,rs,ls0,cj,rs0. + nth src ? int (niltape ?) = midtape sig ls x (xs@ci::rs) → + nth dst ? int (niltape ?) = midtape sig ls0 x (xs@cj::rs0) → ci ≠ cj → + outt = change_vec ?? int + (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈x,R〉)) dst ∧ is_endc ci = false). + +definition Rtc_multi_true ≝ + λalpha,test,n,i.λt1,t2:Vector ? (S n). + (∃c. current alpha (nth i ? t1 (niltape ?)) = Some ? c ∧ test c = true) ∧ t2 = t1. + +definition Rtc_multi_false ≝ + λalpha,test,n,i.λt1,t2:Vector ? (S n). + (∀c. current alpha (nth i ? t1 (niltape ?)) = Some ? c → test c = false) ∧ t2 = t1. + +lemma sem_test_char_multi : + ∀alpha,test,n,i.i ≤ n → + inject_TM ? (test_char ? test) n i ⊨ + [ tc_true : Rtc_multi_true alpha test n i, Rtc_multi_false alpha test n i ]. +#alpha #test #n #i #Hin #int +cases (acc_sem_inject … Hin (sem_test_char alpha test) int) +#k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ % +[ @Hloop +| #Hqtrue lapply (Htrue Hqtrue) * * * #c * + #Hcur #Htestc #Hnth_i #Hnth_j % + [ %{c} % // + | @(eq_vec … (niltape ?)) #i0 #Hi0 + cases (decidable_eq_nat i0 i) #Hi0i + [ >Hi0i @Hnth_i + | @sym_eq @Hnth_j @sym_not_eq // ] ] ] +| #Hqfalse lapply (Hfalse Hqfalse) * * #Htestc #Hnth_i #Hnth_j % + [ @Htestc + | @(eq_vec … (niltape ?)) #i0 #Hi0 + cases (decidable_eq_nat i0 i) #Hi0i + [ >Hi0i @Hnth_i + | @sym_eq @Hnth_j @sym_not_eq // ] ] ] +qed. + +lemma sem_match_step : + ∀src,dst,sig,n,is_startc,is_endc.src ≠ dst → src < S n → dst < S n → + match_step src dst sig n is_startc is_endc ⊨ + [ inr … (inr … (inr … start_nop)) : + R_match_step_true src dst sig n is_startc is_endc, + R_match_step_false src dst sig n is_endc ]. +#src #dst #sig #n #is_startc #is_endc #Hneq #Hsrc #Hdst +@(acc_sem_seq_app … (sem_compare … Hneq Hsrc Hdst) + (acc_sem_if … (sem_test_char_multi ? () + (sem_nop …) + (sem_seq … sem_mark_next_tuple + (sem_if … (sem_test_char ? (λc:STape.is_grid (\fst c))) + (sem_mark ?) (sem_seq … (sem_move_l …) (sem_init_current …)))))) + (sem_nop ?) …) + + #int diff --git a/matita/matita/lib/turing/turing.ma b/matita/matita/lib/turing/turing.ma index c9412adb0..a8290de51 100644 --- a/matita/matita/lib/turing/turing.ma +++ b/matita/matita/lib/turing/turing.ma @@ -412,3 +412,57 @@ theorem sem_seq_app_guarded: ∀sig,n.∀M1,M2:mTM sig n.∀Pre1,Pre2,R1,R2,R3. % [@Hloop |@Hsub @Houtc] qed. +theorem acc_sem_seq : ∀sig,n.∀M1,M2:mTM sig n.∀R1,Rtrue,Rfalse,acc. + M1 ⊨ R1 → M2 ⊨ [ acc: Rtrue, Rfalse ] → + M1 · M2 ⊨ [ inr … acc: R1 ∘ Rtrue, R1 ∘ Rfalse ]. +#sig #n #M1 #M2 #R1 #Rtrue #Rfalse #acc #HR1 #HR2 #t +cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1 +cases (HR2 (ctapes sig (states ?? M1) n outc1)) #k2 * #outc2 * * #Hloop2 +#HMtrue #HMfalse +@(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2)) +% [ % +[@(loop_merge ??????????? + (loop_lift ??? (lift_confL sig n (states sig n M1) (states sig n M2)) + (step sig n M1) (step sig n (seq sig n M1 M2)) + (λc.halt sig n M1 (cstate … c)) + (λc.halt_liftL ?? (halt sig n M1) (cstate … c)) … Hloop1)) + [ * * + [ #sl #tl whd in ⊢ (??%? → ?); #Hl % + | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ] + || #c0 #Hhalt (trans_liftL_true sig n M1 M2 ??) + [ whd in ⊢ (??%?); whd in ⊢ (???%); + @mconfig_eq whd in ⊢ (???%); // + | @(loop_Some ?????? Hloop10) ] + ] +| >(mconfig_expand … outc2) in ⊢ (%→?); whd in ⊢ (??%?→?); + #Hqtrue destruct (Hqtrue) + @(ex_intro … (ctapes ? (FinSum (states ?? M1) (states ?? M2)) ? (lift_confL … outc1))) + % // >eq_ctape_lift_conf_L >eq_ctape_lift_conf_R /2/ ] +| >(mconfig_expand … outc2) in ⊢ (%→?); whd in ⊢ (?(??%?)→?); #Hqfalse + @(ex_intro … (ctapes ? (FinSum (states ?? M1) (states ?? M2)) ? (lift_confL … outc1))) + % // >eq_ctape_lift_conf_L >eq_ctape_lift_conf_R @HMfalse + @(not_to_not … Hqfalse) // +] +qed. + +lemma acc_sem_seq_app : ∀sig,n.∀M1,M2:mTM sig n.∀R1,Rtrue,Rfalse,R2,R3,acc. + M1 ⊨ R1 → M2 ⊨ [acc: Rtrue, Rfalse] → + (∀t1,t2,t3. R1 t1 t3 → Rtrue t3 t2 → R2 t1 t2) → + (∀t1,t2,t3. R1 t1 t3 → Rfalse t3 t2 → R3 t1 t2) → + M1 · M2 ⊨ [inr … acc : R2, R3]. +#sig #n #M1 #M2 #R1 #Rtrue #Rfalse #R2 #R3 #acc +#HR1 #HRacc #Hsub1 #Hsub2 +#t cases (acc_sem_seq … HR1 HRacc t) +#k * #outc * * #Hloop #Houtc1 #Houtc2 @(ex_intro … k) @(ex_intro … outc) +% [% [@Hloop + |#H cases (Houtc1 H) #t3 * #Hleft #Hright @Hsub1 // ] + |#H cases (Houtc2 H) #t3 * #Hleft #Hright @Hsub2 // ] +qed. -- 2.39.2