From b31ab31a99065295b91003a0df95dec817cee5de Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 8 Jan 2013 12:03:01 +0000 Subject: [PATCH] more porting to machines that can move without writing --- matita/matita/lib/turing/inject.ma | 21 ++++---- .../lib/turing/multi_universal/compare.ma | 10 ++-- .../lib/turing/multi_universal/match.ma | 48 ++++++++++++++++--- .../lib/turing/multi_universal/moves.ma | 34 +++++-------- .../lib/turing/multi_universal/moves_2.ma | 20 ++++---- .../lib/turing/multi_universal/par_test.ma | 17 +++---- matita/matita/lib/turing/turing.ma | 10 ++-- 7 files changed, 93 insertions(+), 67 deletions(-) diff --git a/matita/matita/lib/turing/inject.ma b/matita/matita/lib/turing/inject.ma index e00f3a36d..0e9ffe090 100644 --- a/matita/matita/lib/turing/inject.ma +++ b/matita/matita/lib/turing/inject.ma @@ -43,15 +43,18 @@ lemma inject_trans_def :∀sig:FinSet.∀n,i:nat.i < S n → whd in ⊢ (??%?); >nth_change_vec // >Htrans // qed. +lemma inj_ter: ∀A,B,C.∀p:A×B×C. + p = 〈\fst (\fst p), \snd (\fst p), \snd p〉. +// qed. -axiom inject_step : ∀sig,n,M,i,q,t,nq,nt,v. i < S n → +lemma inject_step : ∀sig,n,M,i,q,t,nq,nt,v. i < S n → step sig M (mk_config ?? q t) = mk_config ?? nq nt → - cic:/matita/turing/turing/step.def(11) sig n (inject_TM sig M n i) + cic:/matita/turing/turing/step.def(12) sig n (inject_TM sig M n i) (mk_mconfig ?? n q (change_vec ? (S n) v t i)) = mk_mconfig ?? n nq (change_vec ? (S n) v nt i). -(*#sig #n #M #i #q #t #nq #nt #v #lein whd in ⊢ (??%?→?); +#sig #n #M #i #q #t #nq #nt #v #lein whd in ⊢ (??%?→?); whd in match (step ????); >(current_chars_change_vec … lein) ->(eq_pair_fst_snd … (trans sig M ?)) whd in ⊢ (??%?→?); #H +>(inj_ter … (trans sig M ?)) whd in ⊢ (??%?→?); #H >(inject_trans_def sig n i lein M …) [|>(eq_pair_fst_snd ?? (trans sig M 〈q,current sig t〉)) >(eq_pair_fst_snd ?? (\fst (trans sig M 〈q,current sig t〉))) % @@ -59,11 +62,11 @@ whd in match (step ????); >(current_chars_change_vec … lein) whd in ⊢ (??%?); @eq_f2 [destruct (H) // ] @(eq_vec … (niltape ?)) #i0 #lei0n cases (decidable_eq_nat … i i0) #Hii0 -[ >Hii0 >nth_change_vec // >pmap_change >nth_change_vec // destruct (H) // -| >nth_change_vec_neq // >pmap_change >nth_change_vec_neq - >tape_move_null_action // +[ >Hii0 >nth_change_vec // >tape_move_multi_def >pmap_change >nth_change_vec // destruct (H) // +| >nth_change_vec_neq // >tape_move_multi_def >pmap_change >nth_change_vec_neq // + tape_move_null_action // ] -qed. *) +qed. lemma halt_inject: ∀sig,n,M,i,x. cic:/matita/turing/turing/halt.fix(0,2,9) sig n (inject_TM sig M n i) x @@ -76,7 +79,7 @@ qed. lemma loop_inject: ∀sig,n,M,i,k,ins,int,outs,outt,vt.i < S n → loopM sig M k (mk_config ?? ins int) = Some ? (mk_config ?? outs outt) → - cic:/matita/turing/turing/loopM.def(12) sig n (inject_TM sig M n i) k (mk_mconfig ?? n ins (change_vec ?? vt int i)) + cic:/matita/turing/turing/loopM.def(13) sig n (inject_TM sig M n i) k (mk_mconfig ?? n ins (change_vec ?? vt int i)) =Some ? (mk_mconfig sig ? n outs (change_vec ?? vt outt i)). #sig #n #M #i #k elim k -k [#ins #int #outs #outt #vt #Hin normalize in ⊢ (%→?); #H destruct diff --git a/matita/matita/lib/turing/multi_universal/compare.ma b/matita/matita/lib/turing/multi_universal/compare.ma index 930915686..688c88638 100644 --- a/matita/matita/lib/turing/multi_universal/compare.ma +++ b/matita/matita/lib/turing/multi_universal/compare.ma @@ -119,7 +119,7 @@ cases (nth i ?? (None ?)) in ⊢ (???%→?); ] qed. -axiom comp_q0_q1 : +lemma comp_q0_q1 : ∀i,j,sig,n,v,a.i ≠ j → i < S n → j < S n → nth i ? (current_chars ?? v) (None ?) = Some ? a → nth j ? (current_chars ?? v) (None ?) = Some ? a → @@ -129,7 +129,6 @@ axiom comp_q0_q1 : (change_vec ?? v (tape_move_right ? (nth i ? v (niltape ?))) i) (tape_move_right ? (nth j ? v (niltape ?))) j). -(* #i #j #sig #n #v #a #Heq #Hi #Hj #Ha1 #Ha2 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2 [ whd in match (trans ????); @@ -139,11 +138,12 @@ whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2 change with (change_vec ?????) in ⊢ (??(????%)?); <(change_vec_same … v j (niltape ?)) in ⊢ (??%?); <(change_vec_same … v i (niltape ?)) in ⊢ (??%?); - >pmap_change >pmap_change >tape_move_null_action - @eq_f2 // @eq_f2 // >nth_change_vec_neq // + >tape_move_multi_def + >pmap_change >pmap_change tape_move_null_action + @eq_f2 // >nth_change_vec_neq // ] qed. -*) lemma sem_comp_step : ∀i,j,sig,n.i ≠ j → i < S n → j < S n → diff --git a/matita/matita/lib/turing/multi_universal/match.ma b/matita/matita/lib/turing/multi_universal/match.ma index 6e5dad052..ed4142fa3 100644 --- a/matita/matita/lib/turing/multi_universal/match.ma +++ b/matita/matita/lib/turing/multi_universal/match.ma @@ -75,8 +75,42 @@ definition match_test ≝ λsrc,dst.λsig:DeqSet.λn.λv:Vector ? n. match (nth src (option sig) v (None ?)) with [ None ⇒ false | Some x ⇒ notb (nth dst (DeqOption sig) v (None ?) == None ?) ]. + +definition mmove_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 trans_mmove ≝ + λi,sig,n,D. + λp:mmove_states × (Vector (option sig) (S n)). + 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〉 ]. + +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. -definition rewind ≝ λsrc,dst,sig,n.parmove src dst sig n L · parmove_step src dst sig n R. +definition rewind ≝ λsrc,dst,sig,n. + parmove src dst sig n L · mmove src sig n R · mmove dst sig n R. definition R_rewind ≝ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n). (∀x,x0,xs,rs. @@ -101,14 +135,14 @@ lemma sem_rewind : ∀src,dst,sig,n. src ≠ dst → src < S n → dst < S n → rewind src dst sig n ⊨ R_rewind src dst sig n. #src #dst #sig #n #Hneq #Hsrc #Hdst -check acc_sem_seq_app -@(sem_seq_app sig n ????? (sem_parmoveL src dst sig n Hneq Hsrc Hdst) - (accRealize_to_Realize … (sem_parmove_step src dst sig n R Hneq Hsrc Hdst))) -#ta #tb * #tc * * #HR1 #_ #HR2 +@(sem_seq_app sig n ????? (sem_parmoveL src dst sig n Hneq Hsrc Hdst) ?) +[| @(sem_seq_app sig n ????? (sem_move_r_multi …) (sem_move_r_multi …)) // + @le_S_S_to_le // ] +#ta #tb * #tc * * #Htc #_ * #td * whd in ⊢ (%→%→?); #Htd #Htb #x #x0 #xs #rs #Hmidta_src #ls0 #y #y0 #target #rs0 #Hlen #Hmidta_dst ->(HR1 ??? Hmidta_src ls0 y (target@[y0]) rs0 ??) in HR2; +>(Htc ??? Hmidta_src ls0 y (target@[y0]) rs0 ??) in Htd; [|>Hmidta_dst // -|>length_append >length_append >Hlen % ] * +|>length_append >length_append >Hlen % ] * #_ [ whd in ⊢ (%→?); * #x1 * #x2 * * >change_vec_commute in ⊢ (%→?); // >nth_change_vec // cases (reverse sig (xs@[x0])@x::rs) diff --git a/matita/matita/lib/turing/multi_universal/moves.ma b/matita/matita/lib/turing/multi_universal/moves.ma index ca15620c2..df620b352 100644 --- a/matita/matita/lib/turing/multi_universal/moves.ma +++ b/matita/matita/lib/turing/multi_universal/moves.ma @@ -47,8 +47,8 @@ definition trans_parmove_step ≝ [ None ⇒ 〈parmove2,null_action ? n〉 | Some a1 ⇒ 〈parmove1,change_vec ? (S n) (change_vec ?(S n) - (null_action ? n) (〈Some ? a0,D〉) src) - (〈Some ? a1,D〉) dst〉 ] ] + (null_action ? n) (〈None sig,D〉) src) + (〈None ?,D〉) dst〉 ] ] | S q ⇒ match q with [ O ⇒ (* 1 *) 〈parmove1,null_action ? n〉 | S _ ⇒ (* 2 *) 〈parmove2,null_action ? n〉 ] ]. @@ -66,8 +66,8 @@ definition R_parmove_step_true ≝ is_sep x1 = false ∧ outt = change_vec ?? (change_vec ?? int - (tape_move ? (tape_write ? (nth src ? int (niltape ?)) (Some ? x1)) D) src) - (tape_move ? (tape_write ? (nth dst ? int (niltape ?)) (Some ? x2)) D) dst. + (tape_move_mono ? (nth src ? int (niltape ?)) (〈None ?,D〉)) src) + (tape_move_mono ? (nth dst ? int (niltape ?)) (〈None ?,D〉)) dst. definition R_parmove_step_false ≝ λsrc,dst:nat.λsig,n,is_sep.λint,outt: Vector (tape sig) (S n). @@ -120,7 +120,7 @@ whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); whd in ⊢ (??(????(???%))?); >Hsep >Hcurdst @tape_move_null_action ] qed. -axiom parmove_q0_q1 : +lemma parmove_q0_q1 : ∀src,dst,sig,n,D,is_sep,v.src ≠ dst → src < S n → dst < S n → ∀a1,a2. nth src ? (current_chars ?? v) (None ?) = Some ? a1 → @@ -131,9 +131,8 @@ axiom parmove_q0_q1 : mk_mconfig ??? parmove1 (change_vec ? (S n) (change_vec ?? v - (tape_move ? (tape_write ? (nth src ? v (niltape ?)) (Some ? a1)) D) src) - (tape_move ? (tape_write ? (nth dst ? v (niltape ?)) (Some ? a2)) D) dst). -(* + (tape_move_mono ? (nth src ? v (niltape ?)) (〈None ?, D〉)) src) + (tape_move_mono ? (nth dst ? v (niltape ?)) (〈None ?, D〉)) dst). #src #dst #sig #n #D #is_sep #v #Hneq #Hsrc #Hdst #a1 #a2 #Hcursrc #Hcurdst #Hsep whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2 @@ -141,13 +140,13 @@ whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2 >Hcursrc >Hcurdst whd in ⊢ (??(???%)?); >Hsep // | whd in match (trans ????); >Hcursrc >Hcurdst whd in ⊢ (??(????(???%))?); >Hsep whd in ⊢ (??(????(???%))?); - change with (pmap_vec ???????) in ⊢ (??%?); - whd in match (vec_map ?????); - >pmap_change >pmap_change >tape_move_null_action + <(change_vec_same ?? v dst (niltape ?)) in ⊢ (??%?); + >tape_move_multi_def >pmap_change + <(change_vec_same ?? v src (niltape ?)) in ⊢ (??%?); + >pmap_change tape_move_null_action @eq_f2 // @eq_f2 // >nth_change_vec_neq // ] qed. -*) lemma sem_parmove_step : ∀src,dst,sig,n,D,is_sep.src ≠ dst → src < S n → dst < S n → @@ -234,15 +233,9 @@ lapply (sem_while … (sem_parmove_step src dst sig n L is_sep Hneq Hsrc Hdst) #i #Hi cases (decidable_eq_nat i src) #Hisrc [ >Hisrc >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)] >nth_change_vec // - >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)] - >nth_change_vec // | cases (decidable_eq_nat i dst) #Hidst - [ >Hidst >nth_change_vec // >nth_change_vec // - >Hdst_tc in Hc1; >Htargetnil - normalize in ⊢ (%→?); #Hc1 destruct (Hc1) % + [ >Hidst >nth_change_vec // | >nth_change_vec_neq [|@(sym_not_eq … Hidst)] - >nth_change_vec_neq [|@(sym_not_eq … Hisrc)] - >nth_change_vec_neq [|@(sym_not_eq … Hidst)] >nth_change_vec_neq [|@(sym_not_eq … Hisrc)] % ] ] @@ -254,8 +247,7 @@ lapply (sem_while … (sem_parmove_step src dst sig n L is_sep Hneq Hsrc Hdst) >change_vec_change_vec >reverse_cons >associative_append >reverse_cons >associative_append % - | >Hd >nth_change_vec // >Hdst_tc >Htarget >Hdst_tc in Hc1; - normalize in ⊢ (%→?); #H destruct (H) // + | >Hd >nth_change_vec // | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) // | Hd >nth_change_vec_neq [|@sym_not_eq //] diff --git a/matita/matita/lib/turing/multi_universal/moves_2.ma b/matita/matita/lib/turing/multi_universal/moves_2.ma index 2455ec582..072d3a15a 100644 --- a/matita/matita/lib/turing/multi_universal/moves_2.ma +++ b/matita/matita/lib/turing/multi_universal/moves_2.ma @@ -100,7 +100,7 @@ whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); whd in ⊢ (??(????(???%))?); >Hcurdst @tape_move_null_action ] qed. -axiom parmove_q0_q1 : +lemma parmove_q0_q1 : ∀src,dst,sig,n,D,v.src ≠ dst → src < S n → dst < S n → ∀a1,a2. nth src ? (current_chars ?? v) (None ?) = Some ? a1 → @@ -112,21 +112,19 @@ axiom parmove_q0_q1 : (change_vec ?? v (tape_move ? (nth src ? v (niltape ?)) D) src) (tape_move ? (nth dst ? v (niltape ?)) D) dst). -(* -#src #dst #sig #n #D #is_sep #v #Hneq #Hsrc #Hdst -#a1 #a2 #Hcursrc #Hcurdst #Hsep +#src #dst #sig #n #D #v #Hneq #Hsrc #Hdst +#a1 #a2 #Hcursrc #Hcurdst whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2 [ whd in match (trans ????); - >Hcursrc >Hcurdst whd in ⊢ (??(???%)?); >Hsep // + >Hcursrc >Hcurdst % | whd in match (trans ????); - >Hcursrc >Hcurdst whd in ⊢ (??(????(???%))?); >Hsep whd in ⊢ (??(????(???%))?); - change with (pmap_vec ???????) in ⊢ (??%?); - whd in match (vec_map ?????); - >pmap_change >pmap_change >tape_move_null_action - @eq_f2 // @eq_f2 // >nth_change_vec_neq // + >Hcursrc >Hcurdst whd in ⊢ (??(????(???%))?); + >tape_move_multi_def <(change_vec_same ?? v dst (niltape ?)) in ⊢ (??%?); + >pmap_change <(change_vec_same ?? v src (niltape ?)) in ⊢(??%?); + >pmap_change tape_move_null_action + @eq_f2 // >nth_change_vec_neq // ] qed. -*) lemma sem_parmove_step : ∀src,dst,sig,n,D.src ≠ dst → src < S n → dst < S n → diff --git a/matita/matita/lib/turing/multi_universal/par_test.ma b/matita/matita/lib/turing/multi_universal/par_test.ma index 615efdc2e..1ab0e34a4 100644 --- a/matita/matita/lib/turing/multi_universal/par_test.ma +++ b/matita/matita/lib/turing/multi_universal/par_test.ma @@ -39,31 +39,29 @@ definition R_partest_false ≝ λsig,n,test.λint,outt: Vector (tape sig) (S n). test (current_chars ?? int) = false ∧ outt = int. -axiom partest_q0_q1: +lemma partest_q0_q1: ∀sig,n,test,v. test (current_chars ?? v) = true → step sig n (partest sig n test)(mk_mconfig ??? partest0 v) = mk_mconfig ??? partest1 v. -(*#sig #n #test #v #Htest +#sig #n #test #v #Htest whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2 [ whd in ⊢ (??(???%)?); >Htest % -| whd in ⊢ (??(???????(???%))?); >Htest @tape_move_null_action ] -qed.*) +| whd in ⊢ (??(????(???%))?); >Htest @tape_move_null_action ] +qed. -axiom partest_q0_q2: +lemma partest_q0_q2: ∀sig,n,test,v. test (current_chars ?? v) = false → step sig n (partest sig n test)(mk_mconfig ??? partest0 v) = mk_mconfig ??? partest2 v. -(* #sig #n #test #v #Htest whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2 [ whd in ⊢ (??(???%)?); >Htest % -| whd in ⊢ (??(???????(???%))?); >Htest @tape_move_null_action ] +| whd in ⊢ (??(????(???%))?); >Htest @tape_move_null_action ] qed. -*) lemma sem_partest: ∀sig,n,test. @@ -80,5 +78,4 @@ cases (true_or_false (test (current_chars ?? int))) #Htest | whd in ⊢ (??%%→?); #H destruct (H)] | #_ % //] ] -qed. - \ No newline at end of file +qed. \ No newline at end of file diff --git a/matita/matita/lib/turing/turing.ma b/matita/matita/lib/turing/turing.ma index 7e9c708d0..4cf3ebaf1 100644 --- a/matita/matita/lib/turing/turing.ma +++ b/matita/matita/lib/turing/turing.ma @@ -31,12 +31,14 @@ qed. definition current_chars ≝ λsig.λn.λtapes. vec_map ?? (current sig) (S n) tapes. - + definition tape_move_multi ≝ λsig,n,ts,mvs. - pmap_vec ??? (tape_move sig) ? - (pmap_vec ??? (tape_write sig) n ts (vec_map ?? (λx.\fst x) ? mvs)) - (vec_map ?? (λx.\snd x) ? mvs). + pmap_vec ??? (tape_move_mono sig) n ts mvs. + +lemma tape_move_multi_def : ∀sig,n,ts,mvs. + tape_move_multi sig n ts mvs = pmap_vec ??? (tape_move_mono sig) n ts mvs. +// qed. definition step ≝ λsig.λn.λM:mTM sig n.λc:mconfig sig (states ?? M) n. let 〈news,mvs〉 ≝ trans sig n M 〈cstate ??? c,current_chars ?? (ctapes ??? c)〉 in -- 2.39.2