From: Wilmer Ricciotti Date: Tue, 8 Jan 2013 09:16:34 +0000 (+0000) Subject: porting to machine that can move without writing X-Git-Tag: make_still_working~1360 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3f37ee83ce3c43f34d38729d192e72510f998a53;p=helm.git porting to machine that can move without writing --- diff --git a/matita/matita/lib/turing/inject.ma b/matita/matita/lib/turing/inject.ma index d7851d85f..e00f3a36d 100644 --- a/matita/matita/lib/turing/inject.ma +++ b/matita/matita/lib/turing/inject.ma @@ -13,7 +13,7 @@ include "turing/turing.ma". (******************* inject a mono machine into a multi tape one **********************) definition inject_trans ≝ λsig,states:FinSet.λn,i:nat. - λtrans:states × (option sig) → states × (option (sig × move)). + λtrans:states × (option sig) → states × (option sig × move). λp:states × (Vector (option sig) (S n)). let 〈q,a〉 ≝ p in let 〈nq,na〉 ≝ trans 〈q,nth i ? a (None ?)〉 in @@ -22,32 +22,40 @@ definition inject_trans ≝ λsig,states:FinSet.λn,i:nat. definition inject_TM ≝ λsig.λM:TM sig.λn,i. mk_mTM sig n (states ? M) - (inject_trans ?? n i (trans ? M)) + (inject_trans sig (states ? M) n i ?) (* (trans sig M))*) (start ? M) (halt ? M). +(* ????? *) +lapply (trans sig M) #trans #x lapply (trans x) * * +#s #a #m % [ @s | % [ @a | @m ] ] +qed. axiom current_chars_change_vec: ∀sig,n,v,a,i. i < S n → current_chars sig ? (change_vec ? (S n) v a i) = change_vec ? (S n)(current_chars ?? v) (current ? a) i. - + lemma inject_trans_def :∀sig:FinSet.∀n,i:nat.i < S n → - ∀M,v,s,a,sn,an. - trans sig M 〈s,a〉 = 〈sn,an〉 → + ∀M,v,s,a,sn,an,mn. + trans sig M 〈s,a〉 = 〈sn,an,mn〉 → cic:/matita/turing/turing/trans.fix(0,2,9) sig n (inject_TM sig M n i) 〈s,change_vec ? (S n) v a i〉 = - 〈sn,change_vec ? (S n) (null_action ? n) an i〉. -#sig #n #i #Hlt #trans #v #s #a #sn #an #Htrans + 〈sn,change_vec ? (S n) (null_action ? n) 〈an,mn〉 i〉. +#sig #n #i #Hlt #M #v #s #a #sn #an #mn #Htrans whd in ⊢ (??%?); >nth_change_vec // >Htrans // qed. -lemma inject_step : ∀sig,n,M,i,q,t,nq,nt,v. i < S n → + +axiom 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(10) sig n (inject_TM sig M n i) + cic:/matita/turing/turing/step.def(11) 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 ->(inject_trans_def sig n i lein M … (eq_pair_fst_snd … )) +>(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〉))) % +| *: skip ] whd in ⊢ (??%?); @eq_f2 [destruct (H) // ] @(eq_vec … (niltape ?)) #i0 #lei0n cases (decidable_eq_nat … i i0) #Hii0 @@ -55,7 +63,7 @@ cases (decidable_eq_nat … i i0) #Hii0 | >nth_change_vec_neq // >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 @@ -68,7 +76,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(11) sig n (inject_TM sig M n i) k (mk_mconfig ?? n ins (change_vec ?? vt int i)) + 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)) =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/mono.ma b/matita/matita/lib/turing/mono.ma index 39ecff800..bab3ab1ba 100644 --- a/matita/matita/lib/turing/mono.ma +++ b/matita/matita/lib/turing/mono.ma @@ -109,6 +109,10 @@ definition tape_move ≝ λsig.λt: tape sig.λm:move. | N ⇒ t ]. +definition tape_move_mono ≝ + λsig,t,mv. + tape_move sig (tape_write sig t (\fst mv)) (\snd mv). + record config (sig,states:FinSet): Type[0] ≝ { cstate : states; ctape: tape sig diff --git a/matita/matita/lib/turing/multi_universal/compare.ma b/matita/matita/lib/turing/multi_universal/compare.ma index 2a26abb3e..930915686 100644 --- a/matita/matita/lib/turing/multi_universal/compare.ma +++ b/matita/matita/lib/turing/multi_universal/compare.ma @@ -33,18 +33,18 @@ definition comp2 : compare_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …) *) definition trans_compare_step ≝ - λi,j.λsig:FinSet.λn.λis_endc. + λi,j.λsig:FinSet.λn. λp:compare_states × (Vector (option sig) (S n)). let 〈q,a〉 ≝ p in match pi1 … q with [ O ⇒ match nth i ? a (None ?) with - [ None ⇒ 〈comp2,null_action ? n〉 + [ None ⇒ 〈comp2,null_action sig n〉 | Some ai ⇒ match nth j ? a (None ?) with [ None ⇒ 〈comp2,null_action ? n〉 - | Some aj ⇒ if notb (is_endc ai) ∧ ai == aj + | Some aj ⇒ if ai == aj then 〈comp1,change_vec ? (S n) - (change_vec ? (S n) (null_action ? n) (Some ? 〈ai,R〉) i) - (Some ? 〈aj,R〉) j〉 + (change_vec ? (S n) (null_action ? n) (〈None ?,R〉) i) + (〈None ?,R〉) j〉 else 〈comp2,null_action ? n〉 ] ] | S q ⇒ match q with @@ -52,112 +52,105 @@ definition trans_compare_step ≝ | S _ ⇒ (* 2 *) 〈comp2,null_action ? n〉 ] ]. definition compare_step ≝ - λi,j,sig,n,is_endc. - mk_mTM sig n compare_states (trans_compare_step i j sig n is_endc) + λi,j,sig,n. + mk_mTM sig n compare_states (trans_compare_step i j sig n) comp0 (λq.q == comp1 ∨ q == comp2). definition R_comp_step_true ≝ - λi,j,sig,n,is_endc.λint,outt: Vector (tape sig) (S n). + λi,j,sig,n.λint,outt: Vector (tape sig) (S n). ∃x. - is_endc x = false ∧ current ? (nth i ? int (niltape ?)) = Some ? x ∧ current ? (nth j ? int (niltape ?)) = Some ? x ∧ outt = change_vec ?? (change_vec ?? int - (tape_move ? (nth i ? int (niltape ?)) (Some ? 〈x,R〉)) i) - (tape_move ? (nth j ? int (niltape ?)) (Some ? 〈x,R〉)) j. + (tape_move_right ? (nth i ? int (niltape ?))) i) + (tape_move_right ? (nth j ? int (niltape ?))) j. definition R_comp_step_false ≝ - λi,j:nat.λsig,n,is_endc.λint,outt: Vector (tape sig) (S n). - ((∃x.current ? (nth i ? int (niltape ?)) = Some ? x ∧ is_endc x = true) ∨ - current ? (nth i ? int (niltape ?)) ≠ current ? (nth j ? int (niltape ?)) ∨ - current ? (nth i ? int (niltape ?)) = None ? ∨ - current ? (nth j ? int (niltape ?)) = None ?) ∧ outt = int. + λi,j:nat.λsig,n.λint,outt: Vector (tape sig) (S n). + (current ? (nth i ? int (niltape ?)) ≠ current ? (nth j ? int (niltape ?)) ∨ + current ? (nth i ? int (niltape ?)) = None ? ∨ + current ? (nth j ? int (niltape ?)) = None ?) ∧ outt = int. lemma comp_q0_q2_null : - ∀i,j,sig,n,is_endc,v.i < S n → j < S n → + ∀i,j,sig,n,v.i < S n → j < S n → (nth i ? (current_chars ?? v) (None ?) = None ? ∨ nth j ? (current_chars ?? v) (None ?) = None ?) → - step sig n (compare_step i j sig n is_endc) (mk_mconfig ??? comp0 v) + step sig n (compare_step i j sig n) (mk_mconfig ??? comp0 v) = mk_mconfig ??? comp2 v. -#i #j #sig #n #is_endc #v #Hi #Hj +#i #j #sig #n #v #Hi #Hj whd in ⊢ (? → ??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (?→??%?); * #Hcurrent [ @eq_f2 [ whd in ⊢ (??(???%)?); >Hcurrent % - | whd in ⊢ (??(???????(???%))?); >Hcurrent @tape_move_null_action ] + | whd in ⊢ (??(????(???%))?); >Hcurrent @tape_move_null_action ] | @eq_f2 [ whd in ⊢ (??(???%)?); >Hcurrent cases (nth i ?? (None sig)) // - | whd in ⊢ (??(???????(???%))?); >Hcurrent + | whd in ⊢ (??(????(???%))?); >Hcurrent cases (nth i ?? (None sig)) [|#x] @tape_move_null_action ] ] qed. lemma comp_q0_q2_neq : - ∀i,j,sig,n,is_endc,v.i < S n → j < S n → - ((∃x.nth i ? (current_chars ?? v) (None ?) = Some ? x ∧ is_endc x = true) ∨ - nth i ? (current_chars ?? v) (None ?) ≠ nth j ? (current_chars ?? v) (None ?)) → - step sig n (compare_step i j sig n is_endc) (mk_mconfig ??? comp0 v) + ∀i,j,sig,n,v.i < S n → j < S n → + (nth i ? (current_chars ?? v) (None ?) ≠ nth j ? (current_chars ?? v) (None ?)) → + step sig n (compare_step i j sig n) (mk_mconfig ??? comp0 v) = mk_mconfig ??? comp2 v. -#i #j #sig #n #is_endc #v #Hi #Hj lapply (refl ? (nth i ?(current_chars ?? v)(None ?))) +#i #j #sig #n #v #Hi #Hj lapply (refl ? (nth i ?(current_chars ?? v)(None ?))) cases (nth i ?? (None ?)) in ⊢ (???%→?); [ #Hnth #_ @comp_q0_q2_null // % // | #ai #Hai lapply (refl ? (nth j ?(current_chars ?? v)(None ?))) cases (nth j ?? (None ?)) in ⊢ (???%→?); [ #Hnth #_ @comp_q0_q2_null // %2 // - | #aj #Haj * - [ * #c * >Hai #Heq #Hendc whd in ⊢ (??%?); - >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2 - [ whd in match (trans ????); >Hai >Haj destruct (Heq) - whd in ⊢ (??(???%)?); >Hendc // - | whd in match (trans ????); >Hai >Haj destruct (Heq) - whd in ⊢ (??(???????(???%))?); >Hendc @tape_move_null_action - ] - | #Hneq - whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2 - [ whd in match (trans ????); >Hai >Haj - whd in ⊢ (??(???%)?); cut ((¬is_endc ai∧ai==aj)=false) - [>(\bf ?) /2 by not_to_not/ cases (is_endc ai) // |#Hcut >Hcut //] - | whd in match (trans ????); >Hai >Haj - whd in ⊢ (??(???????(???%))?); cut ((¬is_endc ai∧ai==aj)=false) - [>(\bf ?) /2 by not_to_not/ cases (is_endc ai) // - |#Hcut >Hcut @tape_move_null_action - ] - ] + | #aj #Haj * #Hneq + whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2 + [ whd in match (trans ????); >Hai >Haj + whd in ⊢ (??(???%)?); cut ((ai==aj)=false) + [>(\bf ?) /2 by not_to_not/ % #Haiaj @Hneq + >Hai >Haj // + | #Haiaj >Haiaj % ] + | whd in match (trans ????); >Hai >Haj + whd in ⊢ (??(????(???%))?); cut ((ai==aj)=false) + [>(\bf ?) /2 by not_to_not/ % #Haiaj @Hneq + >Hai >Haj // + |#Hcut >Hcut @tape_move_null_action ] ] + ] ] qed. -lemma comp_q0_q1 : - ∀i,j,sig,n,is_endc,v,a.i ≠ j → i < S n → j < S n → - nth i ? (current_chars ?? v) (None ?) = Some ? a → is_endc a = false → +axiom 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 → - step sig n (compare_step i j sig n is_endc) (mk_mconfig ??? comp0 v) = + step sig n (compare_step i j sig n) (mk_mconfig ??? comp0 v) = mk_mconfig ??? comp1 (change_vec ? (S n) (change_vec ?? v - (tape_move ? (nth i ? v (niltape ?)) (Some ? 〈a,R〉)) i) - (tape_move ? (nth j ? v (niltape ?)) (Some ? 〈a,R〉)) j). -#i #j #sig #n #is_endc #v #a #Heq #Hi #Hj #Ha1 #Hnotendc #Ha2 + (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 ????); - >Ha1 >Ha2 whd in ⊢ (??(???%)?); >Hnotendc >(\b ?) // + >Ha1 >Ha2 whd in ⊢ (??(???%)?); >(\b ?) // | whd in match (trans ????); - >Ha1 >Ha2 whd in ⊢ (??(???????(???%))?); >Hnotendc >(\b ?) // - change with (change_vec ?????) in ⊢ (??(???????%)?); + >Ha1 >Ha2 whd in ⊢ (??(????(???%))?); >(\b ?) // + 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 // ] qed. +*) lemma sem_comp_step : - ∀i,j,sig,n,is_endc.i ≠ j → i < S n → j < S n → - compare_step i j sig n is_endc ⊨ - [ comp1: R_comp_step_true i j sig n is_endc, - R_comp_step_false i j sig n is_endc ]. -#i #j #sig #n #is_endc #Hneq #Hi #Hj #int + ∀i,j,sig,n.i ≠ j → i < S n → j < S n → + compare_step i j sig n ⊨ + [ comp1: R_comp_step_true i j sig n, + R_comp_step_false i j sig n ]. +#i #j #sig #n #Hneq #Hi #Hj #int lapply (refl ? (current ? (nth i ? int (niltape ?)))) cases (current ? (nth i ? int (niltape ?))) in ⊢ (???%→?); [ #Hcuri %{2} % @@ -173,163 +166,127 @@ cases (current ? (nth i ? int (niltape ?))) in ⊢ (???%→?); [ whd in ⊢ (??%?); >comp_q0_q2_null /2/ %2 Ha >Hcurj % % %2 % #H destruct (H) ] ] - | #b #Hb %{2} - cases (true_or_false (is_endc a)) #Haendc + | #_ % // >Ha >Hcurj % % % #H destruct (H) ] ] + | #b #Hb %{2} cases (true_or_false (a == b)) #Hab [ % + [| % [ % + [whd in ⊢ (??%?); >(comp_q0_q1 … a Hneq Hi Hj) // + [>(\P Hab) (\P Hab) %{b} % // % // <(\P Hab) // ] + | * #H @False_ind @H % + ] ] + | % [| % [ % [whd in ⊢ (??%?); >comp_q0_q2_neq // - % %{a} % // Ha >Hb + @(not_to_not ??? (\Pf Hab)) #H destruct (H) % | normalize in ⊢ (%→?); #H destruct (H) ] - | #_ % // % % % >Ha %{a} % // ] - ] - |cases (true_or_false (a == b)) #Hab - [ % - [| % [ % - [whd in ⊢ (??%?); >(comp_q0_q1 … a Hneq Hi Hj) // - [>(\P Hab) (\P Hab) %{b} % // % // <(\P Hab) % // ] - | * #H @False_ind @H % - ] ] - | % - [| % [ % - [whd in ⊢ (??%?); >comp_q0_q2_neq // - <(nth_vec_map ?? (current …) i ? int (niltape ?)) - <(nth_vec_map ?? (current …) j ? int (niltape ?)) %2 >Ha >Hb - @(not_to_not ??? (\Pf Hab)) #H destruct (H) % - | normalize in ⊢ (%→?); #H destruct (H) ] - | #_ % // % % %2 >Ha >Hb @(not_to_not ??? (\Pf Hab)) #H destruct (H) % ] ] - ] + | #_ % // % % >Ha >Hb @(not_to_not ??? (\Pf Hab)) #H destruct (H) % ] ] ] ] ] qed. -definition compare ≝ λi,j,sig,n,is_endc. - whileTM … (compare_step i j sig n is_endc) comp1. +definition compare ≝ λi,j,sig,n. + whileTM … (compare_step i j sig n) comp1. definition R_compare ≝ - λi,j,sig,n,is_endc.λint,outt: Vector (tape sig) (S n). - ((∃x.current ? (nth i ? int (niltape ?)) = Some ? x ∧ is_endc x = true) ∨ - (current ? (nth i ? int (niltape ?)) ≠ current ? (nth j ? int (niltape ?)) ∨ + λi,j,sig,n.λint,outt: Vector (tape sig) (S n). + ((current ? (nth i ? int (niltape ?)) ≠ current ? (nth j ? int (niltape ?)) ∨ current ? (nth i ? int (niltape ?)) = None ? ∨ current ? (nth j ? int (niltape ?)) = None ?) → outt = int) ∧ (∀ls,x,xs,ci,rs,ls0,rs0. nth i ? int (niltape ?) = midtape sig ls x (xs@ci::rs) → nth j ? int (niltape ?) = midtape sig ls0 x (xs@rs0) → - (∀c0. memb ? c0 (x::xs) = true → is_endc c0 = false) → (rs0 = [ ] ∧ outt = change_vec ?? (change_vec ?? int (midtape sig (reverse ? xs@x::ls) ci rs) i) (mk_tape sig (reverse ? xs@x::ls0) (None ?) []) j) ∨ ∃cj,rs1.rs0 = cj::rs1 ∧ - ((is_endc ci = true ∨ ci ≠ cj) → + (ci ≠ cj → outt = change_vec ?? (change_vec ?? int (midtape sig (reverse ? xs@x::ls) ci rs) i) (midtape sig (reverse ? xs@x::ls0) cj rs1) j)). -lemma wsem_compare : ∀i,j,sig,n,is_endc.i ≠ j → i < S n → j < S n → - compare i j sig n is_endc ⊫ R_compare i j sig n is_endc. -#i #j #sig #n #is_endc #Hneq #Hi #Hj #ta #k #outc #Hloop -lapply (sem_while … (sem_comp_step i j sig n is_endc Hneq Hi Hj) … Hloop) // +lemma wsem_compare : ∀i,j,sig,n.i ≠ j → i < S n → j < S n → + compare i j sig n ⊫ R_compare i j sig n. +#i #j #sig #n #Hneq #Hi #Hj #ta #k #outc #Hloop +lapply (sem_while … (sem_comp_step i j sig n Hneq Hi Hj) … Hloop) // -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar -[ whd in ⊢ (%→?); * * [ * [ * - [* #curi * #Hcuri #Hendi #Houtc % - [ #_ @Houtc - | #ls #x #xs #ci #rs #ls0 #rs0 #Hnthi #Hnthj #Hnotendc - @False_ind - >Hnthi in Hcuri; normalize in ⊢ (%→?); #H destruct (H) - >(Hnotendc ? (memb_hd … )) in Hendi; #H destruct (H) - ] - |#Hcicj #Houtc % - [ #_ @Houtc - | #ls #x #xs #ci #rs #ls0 #rs0 #Hnthi #Hnthj - >Hnthi in Hcicj; >Hnthj normalize in ⊢ (%→?); * #H @False_ind @H % - ]] - | #Hci #Houtc % - [ #_ @Houtc - | #ls #x #xs #ci #rs #ls0 #rs0 #Hnthi >Hnthi in Hci; - normalize in ⊢ (%→?); #H destruct (H) ] ] - | #Hcj #Houtc % - [ #_ @Houtc - | #ls #x #xs #ci #rs #ls0 #rs0 #_ #Hnthj >Hnthj in Hcj; - normalize in ⊢ (%→?); #H destruct (H) ] ] - | #td #te * #x * * * #Hendcx #Hci #Hcj #Hd #Hstar #IH #He lapply (IH He) -IH * - #IH1 #IH2 % - [ >Hci >Hcj * [* #x0 * #H destruct (H) >Hendcx #H destruct (H) - |* [* #H @False_ind [cases H -H #H @H % | destruct (H)] | #H destruct (H)]] - | #ls #c0 #xs #ci #rs #ls0 #rs0 cases xs - [ #Hnthi #Hnthj #Hnotendc cases rs0 in Hnthj; - [ #Hnthj % % // >IH1 - [ >Hd @eq_f3 // - [ @eq_f3 // >(?:c0=x) [ >Hnthi % ] - >Hnthi in Hci;normalize #H destruct (H) % - | >(?:c0=x) [ >Hnthj % ] - >Hnthi in Hci;normalize #H destruct (H) % ] - | >Hd %2 %2 >nth_change_vec // >Hnthj % ] - | #r1 #rs1 #Hnthj %2 %{r1} %{rs1} % // * - [ #Hendci >IH1 - [ >Hd @eq_f3 // - [ @eq_f3 // >(?:c0=x) [ >Hnthi % ] - >Hnthi in Hci;normalize #H destruct (H) % - | >(?:c0=x) [ >Hnthj % ] - >Hnthi in Hci;normalize #H destruct (H) % ] +[ whd in ⊢ (%→?); * * [ * + [ #Hcicj #Houtc % + [ #_ @Houtc + | #ls #x #xs #ci #rs #ls0 #rs0 #Hnthi #Hnthj + >Hnthi in Hcicj; >Hnthj normalize in ⊢ (%→?); * #H @False_ind @H % + ] + | #Hci #Houtc % + [ #_ @Houtc + | #ls #x #xs #ci #rs #ls0 #rs0 #Hnthi >Hnthi in Hci; + normalize in ⊢ (%→?); #H destruct (H) ] ] + | #Hcj #Houtc % + [ #_ @Houtc + | #ls #x #xs #ci #rs #ls0 #rs0 #_ #Hnthj >Hnthj in Hcj; + normalize in ⊢ (%→?); #H destruct (H) ] ] +| #td #te * #x * * #Hci #Hcj #Hd #Hstar #IH #He lapply (IH He) -IH * + #IH1 #IH2 % + [ >Hci >Hcj * [ * + [ * #H @False_ind @H % | #H destruct (H)] | #H destruct (H)] + | #ls #c0 #xs #ci #rs #ls0 #rs0 cases xs + [ #Hnthi #Hnthj cases rs0 in Hnthj; + [ #Hnthj % % // >IH1 + [ >Hd @eq_f3 // + [ @eq_f3 // >Hnthi % + | >Hnthj % ] + | >Hd %2 >nth_change_vec // >Hnthj % ] + | #r1 #rs1 #Hnthj %2 %{r1} %{rs1} % // #Hcir1 >IH1 + [ >Hd @eq_f3 // + [ @eq_f3 // >Hnthi % + | >Hnthj % ] | >Hd >nth_change_vec // >nth_change_vec_neq [|@sym_not_eq //] - >nth_change_vec // >Hnthi >Hnthj normalize % %{ci} % // + >nth_change_vec // >Hnthi >Hnthj normalize % % + @(not_to_not … Hcir1) #H destruct (H) % ] - |#Hcir1 >IH1 - [>Hd @eq_f3 // - [ @eq_f3 // >(?:c0=x) [ >Hnthi % ] - >Hnthi in Hci;normalize #H destruct (H) % - | >(?:c0=x) [ >Hnthj % ] - >Hnthi in Hci;normalize #H destruct (H) % ] - | >Hd %2 % % >nth_change_vec // - >nth_change_vec_neq [|@sym_not_eq //] - >nth_change_vec // >Hnthi >Hnthj normalize @(not_to_not … Hcir1) - #H destruct (H) % ] ] - ] - |#x0 #xs0 #Hnthi #Hnthj #Hnotendc - cut (c0 = x) [ >Hnthi in Hci; normalize #H destruct (H) // ] - #Hcut destruct (Hcut) cases rs0 in Hnthj; - [ #Hnthj % % // - cases (IH2 (x::ls) x0 xs0 ci rs (x::ls0) [ ] ???) -IH2 - [ * #_ #IH2 >IH2 >Hd >change_vec_commute in ⊢ (??%?); // - >change_vec_change_vec >change_vec_commute in ⊢ (??%?); // - @sym_not_eq // - | * #cj * #rs1 * #H destruct (H) - | >Hd >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec // - >Hnthi % - | >Hd >nth_change_vec // >Hnthj % - | #c0 #Hc0 @Hnotendc @memb_cons @Hc0 ] - | #r1 #rs1 #Hnthj %2 %{r1} %{rs1} % // #Hcir1 - cases(IH2 (x::ls) x0 xs0 ci rs (x::ls0) (r1::rs1) ???) - [ * #H destruct (H) - | * #r1' * #rs1' * #H destruct (H) #Hc1r1 >Hc1r1 // - >Hd >change_vec_commute in ⊢ (??%?); // - >change_vec_change_vec >change_vec_commute in ⊢ (??%?); // + | #x0 #xs0 #Hnthi #Hnthj + cut (c0 = x) [ >Hnthi in Hci; normalize #H destruct (H) // ] + #Hcut destruct (Hcut) cases rs0 in Hnthj; + [ #Hnthj % % // + cases (IH2 (x::ls) x0 xs0 ci rs (x::ls0) [ ] ??) -IH2 + [ * #_ #IH2 >IH2 >Hd >change_vec_commute in ⊢ (??%?); // + >change_vec_change_vec >change_vec_commute in ⊢ (??%?); // @sym_not_eq // - | >Hd >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec // - >Hnthi // - | >Hd >nth_change_vec // >Hnthi >Hnthj % - | #c0 #Hc0 @Hnotendc @memb_cons @Hc0 + | * #cj * #rs1 * #H destruct (H) + | >Hd >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec // + >Hnthi % + | >Hd >nth_change_vec // >Hnthj % ] + | #r1 #rs1 #Hnthj %2 %{r1} %{rs1} % // #Hcir1 + cases(IH2 (x::ls) x0 xs0 ci rs (x::ls0) (r1::rs1) ??) + [ * #H destruct (H) + | * #r1' * #rs1' * #H destruct (H) #Hc1r1 >Hc1r1 // + >Hd >change_vec_commute in ⊢ (??%?); // + >change_vec_change_vec >change_vec_commute in ⊢ (??%?); // + @sym_not_eq // + | >Hd >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec // + >Hnthi // + | >Hd >nth_change_vec // >Hnthi >Hnthj % ]]]]] -qed. +qed. -lemma terminate_compare : ∀i,j,sig,n,is_endc,t. +lemma terminate_compare : ∀i,j,sig,n,t. i ≠ j → i < S n → j < S n → - compare i j sig n is_endc ↓ t. -#i #j #sig #n #is_endc #t #Hneq #Hi #Hj + compare i j sig n ↓ t. +#i #j #sig #n #t #Hneq #Hi #Hj @(terminate_while … (sem_comp_step …)) // <(change_vec_same … t i (niltape ?)) cases (nth i (tape sig) t (niltape ?)) -[ % #t1 * #x * * * #_ >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct -|2,3: #a0 #al0 % #t1 * #x * * * #_ >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct +[ % #t1 * #x * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct +|2,3: #a0 #al0 % #t1 * #x * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct | #ls #c #rs lapply c -c lapply ls -ls lapply t -t elim rs - [#t #ls #c % #t1 * #x * * * #Hendcx >nth_change_vec // normalize in ⊢ (%→?); - #H1 destruct (H1) #Hxsep >change_vec_change_vec #Ht1 % - #t2 * #x0 * * * #Hendcx0 >Ht1 >nth_change_vec_neq [|@sym_not_eq //] + [#t #ls #c % #t1 * #x * * >nth_change_vec // normalize in ⊢ (%→?); + #H1 destruct (H1) #_ >change_vec_change_vec #Ht1 % + #t2 * #x0 * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H) |#r0 #rs0 #IH #t #ls #c % #t1 * #x * * >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H) #Hcur @@ -338,8 +295,8 @@ cases (nth i (tape sig) t (niltape ?)) ] qed. -lemma sem_compare : ∀i,j,sig,n,is_endc. +lemma sem_compare : ∀i,j,sig,n. i ≠ j → i < S n → j < S n → - compare i j sig n is_endc ⊨ R_compare i j sig n is_endc. -#i #j #sig #n #is_endc #Hneq #Hi #Hj @WRealize_to_Realize /2/ + compare i j sig n ⊨ R_compare i j sig n. +#i #j #sig #n #Hneq #Hi #Hj @WRealize_to_Realize /2/ qed. diff --git a/matita/matita/lib/turing/multi_universal/copy.ma b/matita/matita/lib/turing/multi_universal/copy.ma index 1fef8d0b0..284349ec5 100644 --- a/matita/matita/lib/turing/multi_universal/copy.ma +++ b/matita/matita/lib/turing/multi_universal/copy.ma @@ -47,8 +47,8 @@ definition trans_copy_step ≝ | Some a0 ⇒ if is_sep a0 then 〈copy2,null_action ? n〉 else 〈copy1,change_vec ? (S n) (change_vec ?(S n) - (null_action ? n) (Some ? 〈a0,R〉) src) - (Some ? 〈a0,R〉) dst〉 ] + (null_action ? n) (〈Some ? a0,R〉) src) + (〈Some ? a0,R〉) dst〉 ] | S q ⇒ match q with [ O ⇒ (* 1 *) 〈copy1,null_action ? n〉 | S _ ⇒ (* 2 *) 〈copy2,null_action ? n〉 ] ]. @@ -65,8 +65,8 @@ definition R_copy_step_true ≝ is_sep x1 = false ∧ outt = change_vec ?? (change_vec ?? int - (tape_move ? (nth src ? int (niltape ?)) (Some ? 〈x1,R〉)) src) - (tape_move ? (nth dst ? int (niltape ?)) (Some ? 〈x1,R〉)) dst. + (tape_move_mono ? (nth src ? int (niltape ?)) (〈Some ? x1,R〉)) src) + (tape_move_mono ? (nth dst ? int (niltape ?)) (〈Some ? x1,R〉)) dst. definition R_copy_step_false ≝ λsrc,dst:nat.λsig,n,is_sep.λint,outt: Vector (tape sig) (S n). @@ -102,12 +102,12 @@ whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2 [ >current_chars_change_vec // whd in match (trans ????); >nth_change_vec // >Hcurrent whd in ⊢ (??(???%)?); >Hsep % | >current_chars_change_vec // whd in match (trans ????); - >nth_change_vec // >Hcurrent whd in ⊢ (??(???????(???%))?); + >nth_change_vec // >Hcurrent whd in ⊢ (??(????(???%))?); >Hsep @tape_move_null_action ] qed. -lemma copy_q0_q1 : +axiom copy_q0_q1 : ∀src,dst,sig,n,is_sep,v,t.src ≠ dst → src < S n → dst < S n → ∀s.current ? t = Some ? s → is_sep s = false → step sig n (copy_step src dst sig n is_sep) @@ -115,20 +115,21 @@ lemma copy_q0_q1 : mk_mconfig ??? copy1 (change_vec ? (S n) (change_vec ?? v - (tape_move ? t (Some ? 〈s,R〉)) src) - (tape_move ? (nth dst ? v (niltape ?)) (Some ? 〈s,R〉)) dst). + (tape_move_mono ? t (〈Some ? s,R〉)) src) + (tape_move_mono ? (nth dst ? v (niltape ?)) (〈Some ? s,R〉)) dst). +(* #src #dst #sig #n #is_sep #v #t #Hneq #Hsrc #Hdst #s #Hcurrent #Hsep whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2 [ >current_chars_change_vec // whd in match (trans ????); >nth_change_vec // >Hcurrent whd in ⊢ (??(???%)?); >Hsep % | >current_chars_change_vec // whd in match (trans ????); - >nth_change_vec // >Hcurrent whd in ⊢ (??(???????(???%))?); - >Hsep whd in ⊢ (??(???????(???%))?); >change_vec_commute // >pmap_change + >nth_change_vec // >Hcurrent whd in ⊢ (??(????(???%))?); + >Hsep whd in ⊢ (??(????(???%))?); >change_vec_commute // >pmap_change >change_vec_commute // @eq_f3 // <(change_vec_same ?? v dst (niltape ?)) in ⊢(??%?); >pmap_change @eq_f3 // ] -qed. +qed.*) lemma sem_copy_step : ∀src,dst,sig,n,is_sep.src ≠ dst → src < S n → dst < S n → diff --git a/matita/matita/lib/turing/multi_universal/match.ma b/matita/matita/lib/turing/multi_universal/match.ma index d05a8c35a..6e5dad052 100644 --- a/matita/matita/lib/turing/multi_universal/match.ma +++ b/matita/matita/lib/turing/multi_universal/match.ma @@ -14,7 +14,7 @@ include "turing/multi_universal/compare.ma". include "turing/multi_universal/par_test.ma". - +include "turing/multi_universal/moves_2.ma". definition Rtc_multi_true ≝ λalpha,test,n,i.λt1,t2:Vector ? (S n). @@ -71,111 +71,189 @@ cases (acc_sem_inject … Hin (sem_test_null alpha) int) #Hi0i @sym_eq @Hnth_j @sym_not_eq // ] ] qed. -lemma comp_list: ∀S:DeqSet. ∀l1,l2:list S.∀is_endc. ∃l,tl1,tl2. - l1 = l@tl1 ∧ l2 = l@tl2 ∧ (∀c.c ∈ l = true → is_endc c = false) ∧ - ∀a,tla. tl1 = a::tla → - is_endc a = true ∨ (is_endc a = false ∧∀b,tlb.tl2 = b::tlb → a≠b). -#S #l1 #l2 #is_endc elim l1 in l2; -[ #l2 %{[ ]} %{[ ]} %{l2} normalize % - [ % [ % // | #c #H destruct (H) ] | #a #tla #H destruct (H) ] -| #x #l3 #IH cases (true_or_false (is_endc x)) #Hendcx - [ #l %{[ ]} %{(x::l3)} %{l} normalize - % [ % [ % // | #c #H destruct (H) ] | #a #tla #H destruct (H) >Hendcx % % ] - | * - [ %{[ ]} %{(x::l3)} %{[ ]} normalize % - [ % [ % // | #c #H destruct (H) ] - | #a #tla #H destruct (H) cases (is_endc a) - [ % % | %2 % // #b #tlb #H destruct (H) ] - ] - | #y #l4 cases (true_or_false (x==y)) #Hxy - [ lapply (\P Hxy) -Hxy #Hxy destruct (Hxy) - cases (IH l4) -IH #l * #tl1 * #tl2 * * * #Hl3 #Hl4 #Hl #IH - %{(y::l)} %{tl1} %{tl2} normalize - % [ % [ % // - | #c cases (true_or_false (c==y)) #Hcy >Hcy normalize - [ >(\P Hcy) // - | @Hl ] - ] - | #a #tla #Htl1 @(IH … Htl1) ] - | %{[ ]} %{(x::l3)} %{(y::l4)} normalize % - [ % [ % // | #c #H destruct (H) ] - | #a #tla #H destruct (H) cases (is_endc a) - [ % % | %2 % // #b #tlb #H destruct (H) @(\Pf Hxy) ] - ] - ] - ] - ] -] -qed. - -definition match_test ≝ λsrc,dst.λsig:DeqSet.λn,is_endc.λv:Vector ? n. +definition match_test ≝ λsrc,dst.λsig:DeqSet.λn.λv:Vector ? n. match (nth src (option sig) v (None ?)) with [ None ⇒ false - | Some x ⇒ notb ((is_endc x) ∨ (nth dst (DeqOption sig) v (None ?) == None ?))]. + | Some x ⇒ notb (nth dst (DeqOption sig) v (None ?) == None ?) ]. + +definition rewind ≝ λsrc,dst,sig,n.parmove src dst sig n L · parmove_step src dst sig n R. + +definition R_rewind ≝ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n). + (∀x,x0,xs,rs. + nth src ? int (niltape ?) = midtape sig (xs@[x0]) x rs → + ∀ls0,y,y0,target,rs0.|xs| = |target| → + nth dst ? int (niltape ?) = midtape sig (target@y0::ls0) y rs0 → + outt = change_vec ?? + (change_vec ?? int (midtape sig [] x0 (reverse ? xs@x::rs)) src) + (midtape sig ls0 y0 (reverse ? target@y::rs0)) dst). + +theorem accRealize_to_Realize : + ∀sig,n.∀M:mTM sig n.∀Rtrue,Rfalse,acc. + M ⊨ [ acc: Rtrue, Rfalse ] → M ⊨ Rtrue ∪ Rfalse. +#sig #n #M #Rtrue #Rfalse #acc #HR #t +cases (HR t) #k * #outc * * #Hloop +#Htrue #Hfalse %{k} %{outc} % // +cases (true_or_false (cstate sig (states sig n M) n outc == acc)) #Hcase +[ % @Htrue @(\P Hcase) | %2 @Hfalse @(\Pf Hcase) ] +qed. + +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 +#x #x0 #xs #rs #Hmidta_src #ls0 #y #y0 #target #rs0 #Hlen #Hmidta_dst +>(HR1 ??? Hmidta_src ls0 y (target@[y0]) rs0 ??) in HR2; +[|>Hmidta_dst // +|>length_append >length_append >Hlen % ] * +[ whd in ⊢ (%→?); * #x1 * #x2 * * + >change_vec_commute in ⊢ (%→?); // >nth_change_vec // + cases (reverse sig (xs@[x0])@x::rs) + [|#z #zs] normalize in ⊢ (%→?); #H destruct (H) +| whd in ⊢ (%→?); * #_ #Htb >Htb -Htb FAIL + + normalize in ⊢ (%→?); + (sem_parmove_step src dst sig n R Hneq Hsrc Hdst)) + (acc_sem_if ? n … (sem_partest sig n (match_test src dst sig ?)) + (sem_seq … + (sem_parmoveL ???? Hneq Hsrc Hdst) + (sem_inject … dst (le_S_S_to_le … Hdst) (sem_move_r ? ))) + (sem_nop …))) + -definition match_step ≝ λsrc,dst,sig,n,is_startc,is_endc. - compare src dst sig n is_endc · - (ifTM ?? (partest sig n (match_test src dst sig ? is_endc)) +definition match_step ≝ λsrc,dst,sig,n. + compare src dst sig n · + (ifTM ?? (partest sig n (match_test src dst sig ?)) (single_finalTM ?? - (parmove src dst sig n L is_startc · (inject_TM ? (move_r ?) n dst))) + (rewind src dst sig n · (inject_TM ? (move_r ?) n dst))) (nop …) partest1). definition R_match_step_false ≝ - λsrc,dst,sig,n,is_endc.λint,outt: Vector (tape sig) (S n). - ∀ls,x,xs,end,rs. - nth src ? int (niltape ?) = midtape sig ls x (xs@end::rs) → - (∀c0. memb ? c0 (x::xs) = true → is_endc c0 = false) → is_endc end = true → - ((current sig (nth dst (tape sig) int (niltape sig)) = None ?) ∧ outt = int) ∨ + λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n). + ∀ls,x,xs. + nth src ? int (niltape ?) = midtape sig ls x xs → + ((current sig (nth dst (tape sig) int (niltape sig)) = None ?) ∧ outt = int) ∨ (∃ls0,rs0,xs0. nth dst ? int (niltape ?) = midtape sig ls0 x rs0 ∧ xs = rs0@xs0 ∧ current sig (nth dst (tape sig) outt (niltape sig)) = None ?) ∨ (∃ls0,rs0. nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) ∧ - ∀rsj,c. - rs0 = c::rsj → + (* ∀rsj,c. + rs0 = c::rsj → *) outt = change_vec ?? - (change_vec ?? int (midtape sig (reverse ? xs@x::ls) end rs) src) - (midtape sig (reverse ? xs@x::ls0) c rsj) dst). + (change_vec ?? int (mk_tape sig (reverse ? xs@x::ls) (None ?) [ ]) src) + (mk_tape sig (reverse ? xs@x::ls0) (option_hd ? rs0) (tail ? rs0)) dst). +(*definition R_match_step_true ≝ + λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n). + ∀s,rs.current sig (nth src (tape sig) int (niltape sig)) = Some ? s → + current sig (nth dst (tape sig) int (niltape sig)) ≠ None ? ∧ + (∀s1.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s1 → s ≠ s1 → + outt = change_vec ?? int + (tape_move_mono … (nth dst ? int (niltape ?)) (〈Some ? s1,R〉)) dst) ∧ + (∀ls,x,xs,ci,rs,ls0,rs0. + nth src ? int (niltape ?) = midtape sig ls x (xs@ci::rs) → + nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) → + rs0 ≠ [] ∧ + ∀cj,rs1.rs0 = cj::rs1 → + ci ≠ cj → + (outt = change_vec ?? int + (tape_move_mono … (nth dst ? int (niltape ?)) (〈None ?,R〉)) dst)). +*) definition R_match_step_true ≝ - λsrc,dst,sig,n,is_startc,is_endc.λint,outt: Vector (tape sig) (S n). + λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n). ∀s.current sig (nth src (tape sig) int (niltape sig)) = Some ? s → - current sig (nth dst (tape sig) int (niltape sig)) ≠ None ? ∧ - (is_startc s = true → - (∀c.c ∈ right ? (nth src (tape sig) int (niltape sig)) = true → is_startc c = false) → - (∀s1.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s1 → s ≠ s1 → + ∃s1.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s1 ∧ + (left ? (nth src ? int (niltape ?)) = [ ] → + (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,rs0. - nth src ? int (niltape ?) = midtape sig ls x (xs@ci::rs) → - nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) → - (∀c0. memb ? c0 (x::xs) = true → is_endc c0 = false) → - is_endc ci = false ∧ rs0 ≠ [] ∧ - ∀cj,rs1.rs0 = cj::rs1 → - ci ≠ cj → - (outt = change_vec ?? int - (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈x,R〉)) dst ∧ is_endc ci = false))). - + (tape_move_mono … (nth dst ? int (niltape ?)) (〈None ?,R〉)) dst) ∧ + (∀xs,ci,rs,ls0,rs0. + nth src ? int (niltape ?) = midtape sig [] s (xs@ci::rs) → + nth dst ? int (niltape ?) = midtape sig ls0 s (xs@rs0) → + rs0 ≠ [] ∧ + ∀cj,rs1.rs0 = cj::rs1 → + ci ≠ cj → + (outt = change_vec ?? int + (tape_move_mono … (nth dst ? int (niltape ?)) (〈None ?,R〉)) dst))). + 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 ⊨ + ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n → + match_step src dst sig n ⊨ [ inr ?? (inr ?? (inl … (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 sig n … (sem_compare src dst sig n is_endc Hneq Hsrc Hdst) - (acc_sem_if ? n … (sem_partest sig n (match_test src dst sig ? is_endc)) + R_match_step_true src dst sig n, + R_match_step_false src dst sig n ]. +#src #dst #sig #n #Hneq #Hsrc #Hdst +@(acc_sem_seq_app sig n … (sem_compare src dst sig n Hneq Hsrc Hdst) + (acc_sem_if ? n … (sem_partest sig n (match_test src dst sig ?)) (sem_seq … - (sem_parmoveL ???? is_startc Hneq Hsrc Hdst) + (sem_parmoveL ???? Hneq Hsrc Hdst) (sem_inject … dst (le_S_S_to_le … Hdst) (sem_move_r ? ))) (sem_nop …))) -[#ta #tb #tc * #Hcomp1 #Hcomp2 * #td * * #Htest #Htd >Htd -Htd - * #te * #Hte #Htb whd - #s #Hcurta_src % - [ lapply (refl ? (current ? (nth dst ? ta (niltape ?)))) +[#ta #tb #tc * #Hcomp1 #Hcomp2 * #td * #Htest + * #te * #Hte #Htb #s #Hcurta_src whd + cut (∃s1.current sig (nth dst (tape sig) ta (niltape sig))=Some sig s1) + [ lapply Hcomp1 -Hcomp1 + lapply (refl ? (current ? (nth dst ? ta (niltape ?)))) cases (current ? (nth dst ? ta (niltape ?))) in ⊢ (???%→%); - [| #c #_ % #Hfalse destruct (Hfalse) ] + [ #Hcurta_dst #Hcomp1 >Hcomp1 in Htest; // * + change with (vec_map ?????) in match (current_chars ???); whd in ⊢ (??%?→?); + <(nth_vec_map ?? (current ?) src ? ta (niltape ?)) + <(nth_vec_map ?? (current ?) dst ? ta (niltape ?)) + >Hcurta_src >Hcurta_dst whd in ⊢ (??%?→?); #H destruct (H) + | #s1 #_ #_ %{s1} % ] ] + * #s1 #Hcurta_dst %{s1} % // #Hleftta % + [ #Hneqss1 -Hcomp2 cut (tc = ta) + [@Hcomp1 %1 %1 >Hcurta_src >Hcurta_dst @(not_to_not … Hneqss1) #H destruct (H) //] + #H destruct (H) -Hcomp1 cut (td = ta) + [ cases Htest -Htest // ] #Htdta destruct (Htdta) + cases Hte -Hte #Hte #_ + cases (current_to_midtape … Hcurta_src) #ls * #rs #Hmidta_src + cases (current_to_midtape … Hcurta_dst) #ls0 * #rs0 #Hmidta_dst + >Hmidta_src in Hleftta; normalize in ⊢ (%→?); #Hls destruct (Hls) + >(Hte s [ ] rs Hmidta_src ls0 s1 [ ] rs0 (refl ??) Hmidta_dst) in Htb; + * whd in ⊢ (%→?); + mid + + in Htb; + cut (te = ta) + [ cases Htest -Htest #Htest #Htdta Htdta @Hcurta_src %{s} % //] + -Hte #H destruct (H) % + [cases Htb * #_ #Hmove #Hmove1 @(eq_vec … (niltape … )) + #i #Hi cases (decidable_eq_nat i dst) #Hidst + [ >Hidst >nth_change_vec // cases (current_to_midtape … Hcurta_dst) + #ls * #rs #Hta_mid >(Hmove … Hta_mid) >Hta_mid cases rs // + | >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @Hmove1 @sym_not_eq // ] + | whd in Htest:(??%?); >(nth_vec_map ?? (current sig)) in Hcurta_src; #Hcurta_src + >Hcurta_src in Htest; whd in ⊢ (??%?→?); + cases (is_endc s) // whd in ⊢ (??%?→?); #H @sym_eq // + ] + <(nth_vec_map ?? (current ?) dst ? tc (niltape ?)) + >Hcurta_src normalize + lapply (refl ? (current ? (nth dst ? ta (niltape ?)))) + cases (current ? (nth dst ? ta (niltape ?))) in ⊢ (???%→%); + [| #s1 #Hcurta_dst % + [ % #Hfalse destruct (Hfalse) + | #s1' #Hs1 destruct (Hs1) #Hneqss1 -Hcomp2 + cut (tc = ta) + [@Hcomp1 %1 %1 >Hcurta_src >Hcurta_dst @(not_to_not … Hneqss1) #H destruct (H) //] + #H destruct (H) -Hcomp1 cases Hte -Hte #_ #Hte + cut (te = ta) [ cases Htest -Htest #Htest #Htdta Hidst >nth_change_vec // cases (current_to_midtape … Hcurta_dst) + #ls * #rs #Hta_mid >(Hmove … Hta_mid) >Hta_mid cases rs // + | >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @Hmove1 @sym_not_eq // ] + | whd in Htest:(??%?); >(nth_vec_map ?? (current sig)) in Hcurta_src; #Hcurta_src + >Hcurta_src in Htest; whd in ⊢ (??%?→?); + cases (is_endc s) // whd in ⊢ (??%?→?); #H @sym_eq // + ] + + ] #Hcurta_dst >Hcomp1 in Htest; [| %2 %2 //] whd in ⊢ (??%?→?); change with (current ? (niltape ?)) in match (None ?); Hcurta_src whd in ⊢ (??%?→?); (eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2 [ whd in ⊢ (??(???%)?); >Hcurrent % -| whd in ⊢ (??(???????(???%))?); >Hcurrent @tape_move_null_action ] +| whd in ⊢ (??(????(???%))?); >Hcurrent @tape_move_null_action ] qed. lemma parmove_q0_q2_sep : @@ -101,8 +101,8 @@ lemma parmove_q0_q2_sep : whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2 [ whd in ⊢ (??(???%)?); >Hcurrent whd in ⊢ (??(???%)?); >Hsep % -| whd in ⊢ (??(???????(???%))?); >Hcurrent - whd in ⊢ (??(???????(???%))?); >Hsep @tape_move_null_action ] +| whd in ⊢ (??(????(???%))?); >Hcurrent + whd in ⊢ (??(????(???%))?); >Hsep @tape_move_null_action ] qed. lemma parmove_q0_q2_null_dst : @@ -116,11 +116,11 @@ lemma parmove_q0_q2_null_dst : whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2 [ whd in ⊢ (??(???%)?); >Hcursrc whd in ⊢ (??(???%)?); >Hsep >Hcurdst % -| whd in ⊢ (??(???????(???%))?); >Hcursrc - whd in ⊢ (??(???????(???%))?); >Hsep >Hcurdst @tape_move_null_action ] +| whd in ⊢ (??(????(???%))?); >Hcursrc + whd in ⊢ (??(????(???%))?); >Hsep >Hcurdst @tape_move_null_action ] qed. -lemma parmove_q0_q1 : +axiom 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,22 +131,23 @@ lemma parmove_q0_q1 : mk_mconfig ??? parmove1 (change_vec ? (S n) (change_vec ?? v - (tape_move ? (nth src ? v (niltape ?)) (Some ? 〈a1,D〉)) src) - (tape_move ? (nth dst ? v (niltape ?)) (Some ? 〈a2,D〉)) dst). + (tape_move ? (tape_write ? (nth src ? v (niltape ?)) (Some ? a1)) D) src) + (tape_move ? (tape_write ? (nth dst ? v (niltape ?)) (Some ? a2)) 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 [ whd in match (trans ????); >Hcursrc >Hcurdst whd in ⊢ (??(???%)?); >Hsep // | whd in match (trans ????); - >Hcursrc >Hcurdst whd in ⊢ (??(???????(???%))?); >Hsep - change with (change_vec ?????) in ⊢ (??(???????%)?); - <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?); - <(change_vec_same … v src (niltape ?)) in ⊢ (??%?); + >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 // ] qed. +*) lemma sem_parmove_step : ∀src,dst,sig,n,D,is_sep.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 04c4fe79d..615efdc2e 100644 --- a/matita/matita/lib/turing/multi_universal/par_test.ma +++ b/matita/matita/lib/turing/multi_universal/par_test.ma @@ -39,29 +39,31 @@ definition R_partest_false ≝ λsig,n,test.λint,outt: Vector (tape sig) (S n). test (current_chars ?? int) = false ∧ outt = int. -lemma partest_q0_q1: +axiom 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. +qed.*) -lemma partest_q0_q2: +axiom 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 ] qed. +*) lemma sem_partest: ∀sig,n,test. diff --git a/matita/matita/lib/turing/turing.ma b/matita/matita/lib/turing/turing.ma index a8290de51..7e9c708d0 100644 --- a/matita/matita/lib/turing/turing.ma +++ b/matita/matita/lib/turing/turing.ma @@ -8,7 +8,7 @@ include "basics/vectors.ma". record mTM (sig:FinSet) (tapes_no:nat) : Type[1] ≝ { states : FinSet; trans : states × (Vector (option sig) (S tapes_no)) → - states × (Vector (option (sig × move))(S tapes_no)); + states × (Vector ((option sig) × move) (S tapes_no)); start: states; halt : states → bool }. @@ -32,11 +32,15 @@ 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). + 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 - mk_mconfig ??? - news - (pmap_vec ??? (tape_move sig) ? (ctapes ??? c) mvs). + mk_mconfig ??? news (tape_move_multi sig ? (ctapes ??? c) mvs). definition empty_tapes ≝ λsig.λn. mk_Vector ? n (make_list (tape sig) (niltape sig) n) ?. @@ -189,7 +193,7 @@ definition start_nop : initN 1 ≝ mk_Sig ?? 0 (le_n … 1). *) definition nop ≝ λalpha:FinSet.λn.mk_mTM alpha n nop_states - (λp.let 〈q,a〉 ≝ p in 〈q,mk_Vector ? (S n) (make_list ? (None ?) (S n)) ?〉) + (λp.let 〈q,a〉 ≝ p in 〈q,mk_Vector ? (S n) (make_list ? (〈None ?,N〉) (S n)) ?〉) start_nop (λ_.true). elim n normalize // qed. @@ -210,12 +214,12 @@ generalize in match ltn1; generalize in match ltm1; (************************** Sequential Composition ****************************) definition null_action ≝ λsig.λn. -mk_Vector ? (S n) (make_list (option (sig × move)) (None ?) (S n)) ?. +mk_Vector ? (S n) (make_list (option sig × move) (〈None ?,N〉) (S n)) ?. elim (S n) // normalize // qed. lemma tape_move_null_action: ∀sig,n,tapes. - pmap_vec ??? (tape_move sig) (S n) tapes (null_action sig n) = tapes. + tape_move_multi sig (S n) tapes (null_action sig n) = tapes. #sig #n #tapes cases tapes -tapes #tapes whd in match (null_action ??); #Heq @Vector_eq