From: Andrea Asperti Date: Sat, 26 Jan 2013 21:24:19 +0000 (+0000) Subject: A lot of changes X-Git-Tag: make_still_working~1307 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7e96e893e0ebea2589f619fab861bf9984cff989;p=helm.git A lot of changes --- diff --git a/matita/matita/lib/turing/multi_universal/match.ma b/matita/matita/lib/turing/multi_universal/match.ma index 0ef1213ea..181a35235 100644 --- a/matita/matita/lib/turing/multi_universal/match.ma +++ b/matita/matita/lib/turing/multi_universal/match.ma @@ -12,102 +12,15 @@ (* *) (**************************************************************************) +include "turing/simple_machines.ma". 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). - (∃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. - -definition Rm_test_null_true ≝ - λalpha,n,i.λt1,t2:Vector ? (S n). - current alpha (nth i ? t1 (niltape ?)) ≠ None ? ∧ t2 = t1. - -definition Rm_test_null_false ≝ - λalpha,n,i.λt1,t2:Vector ? (S n). - current alpha (nth i ? t1 (niltape ?)) = None ? ∧ t2 = t1. - -lemma sem_test_null_multi : ∀alpha,n,i.i ≤ n → - inject_TM ? (test_null ?) n i ⊨ - [ tc_true : Rm_test_null_true alpha n i, Rm_test_null_false alpha n i ]. -#alpha #n #i #Hin #int -cases (acc_sem_inject … Hin (sem_test_null alpha) int) -#k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ % -[ @Hloop -| #Hqtrue lapply (Htrue Hqtrue) * * #Hcur #Hnth_i #Hnth_j % // - @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) #Hi0i - [ >Hi0i @sym_eq @Hnth_i | @sym_eq @Hnth_j @sym_not_eq // ] ] -| #Hqfalse lapply (Hfalse Hqfalse) * * #Hcur #Hnth_i #Hnth_j % - [ @Hcur - | @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) // - #Hi0i @sym_eq @Hnth_j @sym_not_eq // ] ] -qed. - 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 · mmove src sig n R · mmove dst sig n R. @@ -224,7 +137,7 @@ 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 @(Realize_to_Realize … (sem_rewind_strong …)) // -#ta #tb * * * #H1 #H2 #H3 #H4 % /2/ +#ta #tb * * * #H1 #H2 #H3 #H4 % /2 by / qed. definition match_step ≝ λsrc,dst,sig,n. diff --git a/matita/matita/lib/turing/multi_universal/unistep.ma b/matita/matita/lib/turing/multi_universal/unistep.ma index 85bf12e83..a4a038184 100644 --- a/matita/matita/lib/turing/multi_universal/unistep.ma +++ b/matita/matita/lib/turing/multi_universal/unistep.ma @@ -12,19 +12,9 @@ include "turing/multi_universal/unistep_aux.ma". -definition unistep ≝ - match_m cfg prg FSUnialpha 2 · - restart_tape cfg 2 · mmove cfg ? 2 R · copy prg cfg FSUnialpha 2 · +definition exec_move ≝ cfg_to_obj · tape_move_obj · restart_tape prg 2 · obj_to_cfg. -(* -definition legal_tape ≝ λn,l,h,t. - ∃state,char,table. - nth cfg ? t1 (niltape ?) = midtape ? [ ] bar (state@[char]) → - is_config n (bar::state@[char]) → - nth prg ? t1 (niltape ?) = midtape ? [ ] bar table → - bar::table = table_TM n l h → *) - definition low_char' ≝ λc. match c with [ None ⇒ null @@ -36,6 +26,56 @@ lemma low_char_option : ∀s. * // qed. +definition R_exec_move ≝ λt1,t2:Vector (tape FSUnialpha) 3. +∀c,m,ls1,ls2,rs2. + nth cfg ? t1 (niltape ?) = mk_tape FSUnialpha (c::ls1@[bar]) (None ?) [ ] → + nth prg ? t1 (niltape ?) = midtape FSUnialpha (ls2@[bar]) m rs2 → + c ≠ bar → m ≠ bar → + let new_obj ≝ + tape_move_mono ? (nth obj ? t1 (niltape ?)) + 〈char_to_bit_option c, char_to_move m〉 in + let next_c ≝ low_char' (current ? new_obj) in + let new_cfg ≝ midtape ? [ ] bar ((reverse ? ls1)@[next_c]) in + let new_prg ≝ midtape FSUnialpha [ ] bar ((reverse ? ls2)@m::rs2) in + t2 = Vector_of_list ? [new_obj;new_cfg;new_prg]. + + +lemma sem_exec_move: exec_move ⊨ R_exec_move. +@(sem_seq_app ??????? sem_cfg_to_obj1 + (sem_seq ?????? sem_tape_move_obj + (sem_seq ?????? (sem_restart_tape ???) sem_obj_to_cfg))) // +#ta #tout * #t1 * #semM1 * #t2 * #semM2 * #t3 * #semM3 #semM4 +#c #m #ls1 #ls2 #rs2 #Hcfg #Hprg #Hc #Hm +(* M1 = cfg_to_obj *) +lapply (semM1 … Hcfg Hc) #Ht1 +(* M2 = tape_move *) +whd in semM2; >Ht1 in semM2; -Ht1 +>nth_change_vec_neq [2:@eqb_false_to_not_eq %] +>nth_change_vec_neq [2:@eqb_false_to_not_eq %] +>Hprg #Ht2 lapply (Ht2 … (refl ??)) -Ht2 +>nth_change_vec_neq [2:@eqb_false_to_not_eq %] +>nth_change_vec // >change_vec_commute [2:@eqb_false_to_not_eq %] +>change_vec_change_vec #Ht2 +(* M3 = restart prg *) +whd in semM3; >Ht2 in semM3; #semM3 lapply (semM3 … (refl ??)); -semM3 +>nth_change_vec_neq [2:@eqb_false_to_not_eq %] +>nth_change_vec_neq [2:@eqb_false_to_not_eq %] #Ht3 +(* M4 = obj_to_cfg *) + + +definition unistep ≝ + match_m cfg prg FSUnialpha 2 · + restart_tape cfg 2 · mmove cfg ? 2 R · copy prg cfg FSUnialpha 2 · + cfg_to_obj · tape_move_obj · restart_tape prg 2 · obj_to_cfg. + +(* +definition legal_tape ≝ λn,l,h,t. + ∃state,char,table. + nth cfg ? t1 (niltape ?) = midtape ? [ ] bar (state@[char]) → + is_config n (bar::state@[char]) → + nth prg ? t1 (niltape ?) = midtape ? [ ] bar table → + bar::table = table_TM n l h → *) + definition R_unistep ≝ λn,l,h.λt1,t2: Vector ? 3. ∀state,char,table. (* cfg *) @@ -91,7 +131,7 @@ lemma sem_unistep : ∀n,l,h.unistep ⊨ R_unistep n l h. (sem_seq ?????? (sem_restart_tape ???) (sem_seq ?????? (sem_move_multi ? 2 cfg R ?) (sem_seq ?????? (sem_copy_strict prg cfg FSUnialpha 2 ???) - (sem_seq ?????? sem_cfg_to_obj + (sem_seq ?????? sem_cfg_to_obj1 (sem_seq ?????? sem_tape_move_obj (sem_seq ?????? (sem_restart_tape ???) sem_obj_to_cfg))))))) /2 by le_n,sym_not_eq/ @@ -141,6 +181,35 @@ whd in match (mk_tape ????); whd in match (tape_move ???); (* cfg to obj *) * #tg * whd in ⊢ (%→?); >Htf >nth_change_vec_neq [|@sym_not_eq //] >(nth_change_vec ?????? lt_cfg) +lapply (append_l1_injective ?????? Hrs1rs2) +[ >Hsnlen >Hrs1len >length_append >length_append >length_append >length_append + normalize >Hsolen >Hsnlen % ] #Hrs1 reverse_append >reverse_single + >associative_append #Htg lapply (Htg … (refl ??) Hm0) -Htg + (* simplifying tg *) + >nth_change_vec_neq [2:@eqb_false_to_not_eq %] + >nth_change_vec_neq [2:@eqb_false_to_not_eq %] + + + + + + cut ((mk_tape FSUnialpha [] + (option_hd FSUnialpha + (reverse FSUnialpha (m0::[]@reverse FSUnialpha (sn@[cn])@[fn; bar]))) + (tail FSUnialpha + (reverse FSUnialpha (m0::[]@reverse FSUnialpha (sn@[cn])@[fn; bar])))) = + midtape ? [ ] bar (fn::sn@[cn;m0])) + [cut (reverse FSUnialpha (m0::[]@reverse FSUnialpha (sn@[cn])@[fn; bar]) = + bar::fn::sn@[cn;m0]) + [>reverse_cons whd in ⊢ (??(??(??%)?)?); >reverse_append >reverse_reverse + >append_cons in ⊢ (???%); % ] #Hrev >Hrev % ] #Hmk_tape >Hmk_tape -Hmk_tape + >change_vec_commute + + >reverse_append >reverse_append + check reverse_cons + reverse_cons + -Htg #Htg + >(change_vec_commute ????? cfg prg) [2:@eqb_false_to_not_eq %] >nth_change_vec_neq [2:@eqb_false_to_not_eq %] >nth_change_vec_neq [2:@eqb_false_to_not_eq %] diff --git a/matita/matita/lib/turing/multi_universal/unistep_aux.ma b/matita/matita/lib/turing/multi_universal/unistep_aux.ma index 972b48930..bb730a558 100644 --- a/matita/matita/lib/turing/multi_universal/unistep_aux.ma +++ b/matita/matita/lib/turing/multi_universal/unistep_aux.ma @@ -52,70 +52,13 @@ include "turing/multi_universal/tuples.ma". cfg_to_obj *) -definition copy_char_states ≝ initN 3. - -definition cc0 : copy_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)). -definition cc1 : copy_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)). - -definition trans_copy_char ≝ - λsrc,dst.λsig:FinSet.λn. - λp:copy_char_states × (Vector (option sig) (S n)). - let 〈q,a〉 ≝ p in - match pi1 … q with - [ O ⇒ 〈cc1,change_vec ? (S n) - (change_vec ? (S n) (null_action ? n) (〈None ?,R〉) src) - (〈nth src ? a (None ?),R〉) dst〉 - | S _ ⇒ 〈cc1,null_action ? n〉 ]. - -definition copy_char ≝ - λsrc,dst,sig,n. - mk_mTM sig n copy_char_states (trans_copy_char src dst sig n) - cc0 (λq.q == cc1). - -definition R_copy_char ≝ - λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n). - outt = change_vec ?? - (change_vec ?? int - (tape_move_mono ? (nth src ? int (niltape ?)) 〈None ?, R〉) src) - (tape_move_mono ? (nth dst ? int (niltape ?)) - 〈current ? (nth src ? int (niltape ?)), R〉) dst. - -lemma copy_char_q0_q1 : - ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n → - step sig n (copy_char src dst sig n) (mk_mconfig ??? cc0 v) = - mk_mconfig ??? cc1 - (change_vec ? (S n) - (change_vec ?? v - (tape_move_mono ? (nth src ? v (niltape ?)) 〈None ?, R〉) src) - (tape_move_mono ? (nth dst ? v (niltape ?)) 〈current ? (nth src ? v (niltape ?)), R〉) dst). -#src #dst #sig #n #v #Heq #Hsrc #Hdst -whd in ⊢ (??%?); -<(change_vec_same … v dst (niltape ?)) in ⊢ (??%?); -<(change_vec_same … v src (niltape ?)) in ⊢ (??%?); ->tape_move_multi_def @eq_f2 // ->pmap_change >pmap_change tape_move_null_action @eq_f2 // @eq_f2 -[ >change_vec_same % -| >change_vec_same >change_vec_same // ] -qed. - -lemma sem_copy_char: - ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n → - copy_char src dst sig n ⊨ R_copy_char src dst sig n. -#src #dst #sig #n #Hneq #Hsrc #Hdst #int -%{2} % [| % [ % | whd >copy_char_q0_q1 // ]] -qed. - definition obj ≝ (0:DeqNat). definition cfg ≝ (1:DeqNat). definition prg ≝ (2:DeqNat). definition obj_to_cfg ≝ - mmove cfg FSUnialpha 2 L · (ifTM ?? (inject_TM ? (test_null ?) 2 obj) - (copy_char obj cfg FSUnialpha 2 · - mmove cfg FSUnialpha 2 L · - mmove obj FSUnialpha 2 L) + (copy_char_N obj cfg FSUnialpha 2) (inject_TM ? (write FSUnialpha null) 2 cfg) tc_true) · inject_TM ? (move_to_end FSUnialpha L) 2 cfg · @@ -123,7 +66,7 @@ definition obj_to_cfg ≝ definition R_obj_to_cfg ≝ λt1,t2:Vector (tape FSUnialpha) 3. ∀c,ls. - nth cfg ? t1 (niltape ?) = mk_tape FSUnialpha (c::ls) (None ?) [ ] → + nth cfg ? t1 (niltape ?) = midtape ? ls c [ ] → (∀lso,x,rso.nth obj ? t1 (niltape ?) = midtape FSUnialpha lso x rso → t2 = change_vec ?? t1 (mk_tape ? [ ] (option_hd ? (reverse ? (x::ls))) (tail ? (reverse ? (x::ls)))) cfg) ∧ @@ -131,7 +74,7 @@ definition R_obj_to_cfg ≝ λt1,t2:Vector (tape FSUnialpha) 3. t2 = change_vec ?? t1 (mk_tape ? [ ] (option_hd FSUnialpha (reverse ? (null::ls))) (tail ? (reverse ? (null::ls)))) cfg). - + axiom accRealize_to_Realize : ∀sig,n.∀M:mTM sig n.∀Rtrue,Rfalse,acc. M ⊨ [ acc: Rtrue, Rfalse ] → M ⊨ Rtrue ∪ Rfalse. @@ -161,69 +104,69 @@ lemma eq_vec_change_vec : ∀sig,n.∀v1,v2:Vector sig n.∀i,t,d. | >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @H2 @sym_not_eq // ] qed. +lemma not_None_to_Some: ∀A.∀a. a ≠ None A → ∃b. a = Some ? b. +#A * /2/ * #H @False_ind @H % +qed. + lemma sem_obj_to_cfg : obj_to_cfg ⊨ R_obj_to_cfg. -@(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?) - (sem_seq ?????? - (sem_if ?????????? - (sem_test_null_multi ?? obj ?) - (sem_seq ?????? (sem_copy_char …) - (sem_seq ?????? (sem_move_multi ? 2 cfg L ?) - (sem_move_multi ? 2 obj L ?))) - (sem_inject ???? cfg ? (sem_write FSUnialpha null))) - (sem_seq ?????? (sem_inject ???? cfg ? (sem_move_to_end_l ?)) - (sem_move_multi ? 2 cfg R ?)))) // -#ta #tb * -#tc * whd in ⊢ (%→?); #Htc * -#td * * -[ * #te * * #Hcurtc #Hte - * destruct (Hte) #te * whd in ⊢ (%→?); #Hte - cut (∃x.current ? (nth obj ? tc (niltape ?)) = Some ? x) - [ cases (current ? (nth obj ? tc (niltape ?))) in Hcurtc; - [ * #H @False_ind /2/ | #x #_ %{x} % ] ] * #x #Hcurtc' -(* [ whd in ⊢ (%→%→?); * #x * #y * * -Hcurtc #Hcurtc1 #Hcurtc2 #Hte *) - * #tf * whd in ⊢ (%→%→?); #Htf #Htd - * #tg * * * whd in ⊢ (%→%→%→%→?); #Htg1 #Htg2 #Htg3 #Htb - #c #ls #Hta1 % - [ #lso #x0 #rso #Hta2 >Hta1 in Htc; >eq_mk_tape_rightof - whd in match (tape_move ???); #Htc - cut (tg = change_vec ?? td (mk_tape ? [ ] (None ?) (reverse ? ls@[x])) cfg) - [ lapply (eq_vec_change_vec ??????? (Htg2 ls x [ ] ?) Htg3) // - >Htd >nth_change_vec_neq // >Htf >nth_change_vec // - >Hte >Hcurtc' >nth_change_vec // >Htc >nth_change_vec // ] - -Htg1 -Htg2 -Htg3 #Htg destruct - >change_vec_change_vec >change_vec_change_vec - >change_vec_commute // >change_vec_change_vec - >change_vec_commute [|@sym_not_eq //] >change_vec_change_vec - >change_vec_commute // >change_vec_change_vec - >nth_change_vec // >nth_change_vec_neq [|@sym_not_eq //] - >nth_change_vec // >nth_change_vec_neq [|@sym_not_eq //] - >change_vec_commute [|@sym_not_eq //] @eq_f3 // - [ >Hta2 cases rso in Hta2; whd in match (tape_move_mono ???); - [ #Hta2 whd in match (tape_move ???); tape_move_mk_tape_R [| #_ % %] >reverse_cons - >nth_change_vec_neq in Hcurtc'; [|@sym_not_eq //] >Hta2 - normalize in ⊢ (%→?); #H destruct (H) % - ] - | #Hta2 >Htc in Hcurtc'; >nth_change_vec_neq [| @sym_not_eq //] - >Hta2 #H destruct (H) +@(sem_seq_app FSUnialpha 2 ????? + (sem_if ?????????? + (sem_test_null_multi ?? obj ?) + (sem_copy_char_N …) + (sem_inject ???? cfg ? (sem_write FSUnialpha null))) + (sem_seq ?????? (sem_inject ???? cfg ? (sem_move_to_end_l ?)) + (sem_move_multi ? 2 cfg R ?))) // +#ta #tout * +#tb * #Hif * #tc * #HM2 #HM3 #c #ls #Hcfg +(* Hif *) +cases Hif -Hif +[ * #t1 * * #Hcurta #Ht1 destruct (Ht1) + lapply (not_None_to_Some … Hcurta) * #curta #Hcurtaeq + whd in ⊢ (%→?); #Htb % [2: #Hcur @False_ind /2/] + #lso #xo #rso #Hobjta cases HM2 whd in ⊢ (%→?); * #_ + #HM2 #Heq >Htb in HM2; >nth_change_vec [2: @leb_true_to_le %] + >Hcfg >Hcurtaeq #HM2 lapply (HM2 … (refl ??)) -HM2 + whd in match (left ??); whd in match (right ??); + >reverse_cons #Htc >HM3 @(eq_vec … (niltape ?)) #i #lei2 + cases (le_to_or_lt_eq … (le_S_S_to_le …lei2)) + [#lei1 cases (le_to_or_lt_eq … (le_S_S_to_le …lei1)) + [#lei0 lapply(le_n_O_to_eq … (le_S_S_to_le …lei0)) #eqi nth_change_vec_neq [2:@eqb_false_to_not_eq %] + <(Heq 0) [2:@eqb_false_to_not_eq %] >Htb + >nth_change_vec_neq [2:@eqb_false_to_not_eq %] + >nth_change_vec_neq [%|2:@eqb_false_to_not_eq %] + |#Hi >Hi >nth_change_vec // >nth_change_vec // >Htc + >Hobjta in Hcurtaeq; whd in ⊢ (??%?→?); #Htmp destruct(Htmp) + >tape_move_mk_tape_R [2: #_ %1 %] % + ] + |#Hi >Hi >nth_change_vec_neq [2:@eqb_false_to_not_eq %] + >nth_change_vec_neq [2:@eqb_false_to_not_eq %] + <(Heq 2) [2:@eqb_false_to_not_eq %] >Htb + >nth_change_vec_neq [%|2:@eqb_false_to_not_eq %] + ] +| * #t1 * * #Hcurta #Ht1 destruct (Ht1) + * whd in ⊢ (%→?); #Htb lapply (Htb … Hcfg) -Htb #Htb + #Htbeq % + [#lso #xo #rso #Hmid @False_ind >Hmid in Hcurta; + whd in ⊢ (??%?→?); #Htmp destruct (Htmp)] + #_ cases HM2 whd in ⊢ (%→?); * #_ + #HM2 #Heq >Htb in HM2; #HM2 lapply (HM2 … (refl ??)) -HM2 + #Htc >HM3 @(eq_vec … (niltape ?)) #i #lei2 + cases (le_to_or_lt_eq … (le_S_S_to_le …lei2)) + [#lei1 cases (le_to_or_lt_eq … (le_S_S_to_le …lei1)) + [#lei0 lapply(le_n_O_to_eq … (le_S_S_to_le …lei0)) #eqi nth_change_vec_neq [2:@eqb_false_to_not_eq %] + >nth_change_vec_neq [2:@eqb_false_to_not_eq %] + <(Heq 0) [2:@eqb_false_to_not_eq %] >Htb + <(Htbeq 0) [2:@eqb_false_to_not_eq %] % + |#Hi >Hi >nth_change_vec // >nth_change_vec // >Htc + >tape_move_mk_tape_R [2: #_ %1 %] >reverse_cons % ] -| * #te * * #Hcurtc #Hte - * whd in ⊢ (%→%→?); #Htd1 #Htd2 - * #tf * * * #Htf1 #Htf2 #Htf3 whd in ⊢ (%→?); #Htb - #c #ls #Hta1 % - [ #lso #x #rso #Hta2 >Htc in Hcurtc; >nth_change_vec_neq [|@sym_not_eq //] - >Hta2 normalize in ⊢ (%→?); #H destruct (H) - | #_ >Hta1 in Htc; >eq_mk_tape_rightof whd in match (tape_move ???); #Htc - destruct (Hte) cut (td = change_vec ?? tc (midtape ? ls null []) cfg) - [ lapply (eq_vec_change_vec ??????? (Htd1 ls c [ ] ?) Htd2) // - >Htc >nth_change_vec // ] -Htd1 -Htd2 #Htd - -Htf1 cut (tf = change_vec ?? td (mk_tape ? [ ] (None ?) (reverse ? ls@[null])) cfg) - [ lapply (eq_vec_change_vec ??????? (Htf2 ls null [ ] ?) Htf3) // - >Htd >nth_change_vec // ] -Htf2 -Htf3 #Htf destruct (Htf Htd Htc Htb) - >change_vec_change_vec >change_vec_change_vec >change_vec_change_vec - >change_vec_change_vec >change_vec_change_vec >nth_change_vec // - >reverse_cons >tape_move_mk_tape_R /2/ ] + |#Hi >Hi >nth_change_vec_neq [2:@eqb_false_to_not_eq %] + >nth_change_vec_neq [2:@eqb_false_to_not_eq %] + <(Heq 2) [2:@eqb_false_to_not_eq %] + <(Htbeq 2) [%|@eqb_false_to_not_eq %] + ] ] qed. @@ -254,25 +197,21 @@ definition cfg_to_obj ≝ mmove cfg FSUnialpha 2 L · (ifTM ?? (inject_TM ? test_null_char 2 cfg) (nop ? 2) - (copy_char cfg obj FSUnialpha 2 · - mmove cfg FSUnialpha 2 L · - mmove obj FSUnialpha 2 L) - tc_true) · + (copy_char_N cfg obj FSUnialpha 2) + tc_true). +(* · inject_TM ? (move_to_end FSUnialpha L) 2 cfg · - mmove cfg FSUnialpha 2 R. + mmove cfg FSUnialpha 2 R. *) definition R_cfg_to_obj ≝ λt1,t2:Vector (tape FSUnialpha) 3. ∀c,ls. nth cfg ? t1 (niltape ?) = mk_tape FSUnialpha (c::ls) (None ?) [ ] → - (c = null → - t2 = change_vec ?? t1 - (mk_tape ? [ ] (option_hd FSUnialpha (reverse ? (c::ls))) - (tail ? (reverse ? (c::ls)))) cfg) ∧ + (c = null → t2 = change_vec ?? t1 (midtape ? ls c [ ]) cfg) ∧ (c ≠ null → t2 = change_vec ?? (change_vec ?? t1 (midtape ? (left ? (nth obj ? t1 (niltape ?))) c (right ? (nth obj ? t1 (niltape ?)))) obj) - (mk_tape ? [ ] (option_hd ? (reverse ? (c::ls))) (tail ? (reverse ? (c::ls)))) cfg). + (midtape ? ls c [ ]) cfg). lemma tape_move_mk_tape_L : ∀sig,ls,c,rs. @@ -286,68 +225,35 @@ qed. lemma sem_cfg_to_obj : cfg_to_obj ⊨ R_cfg_to_obj. @(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?) - (sem_seq ?????? - (sem_if ?????????? - (acc_sem_inject ?????? cfg ? sem_test_null_char) - (sem_nop …) - (sem_seq ?????? (sem_copy_char …) - (sem_seq ?????? (sem_move_multi ? 2 cfg L ?) (sem_move_multi ? 2 obj L ?)))) - (sem_seq ?????? (sem_inject ???? cfg ? (sem_move_to_end_l ?)) - (sem_move_multi ? 2 cfg R ?)))) // [@sym_not_eq //] + (sem_if ?????????? + (acc_sem_inject ?????? cfg ? sem_test_null_char) + (sem_nop …) + (sem_copy_char_N …))) +// [@sym_not_eq //] #ta #tb * #tc * whd in ⊢ (%→?); #Htc * -#td * * -[ * #te * * * #Hcurtc #Hte1 #Hte2 whd in ⊢ (%→?); #Htd destruct (Htd) - * #tf * * * #Htf1 #Htf2 #Htf3 - whd in ⊢ (%→?); #Htb +[ * #te * * * #Hcurtc #Hte1 #Hte2 whd in ⊢ (%→?); #Htb destruct (Htb) #c #ls #Hta % [ #Hc >Hta in Htc; >eq_mk_tape_rightof whd in match (tape_move ???); #Htc cut (te = tc) [ lapply (eq_vec_change_vec ??????? (sym_eq … Hte1) Hte2) >change_vec_same // ] - -Hte1 -Hte2 #Hte - cut (tf = change_vec ? 3 te (mk_tape ? [ ] (None ?) (reverse ? ls@[c])) cfg) - [ lapply (eq_vec_change_vec ??????? (Htf2 ls c [ ] ?) Htf3) // - >Hte >Htc >nth_change_vec // ] -Htf1 -Htf2 -Htf3 #Htf - destruct (Htf Hte Htc Htb) - >change_vec_change_vec >change_vec_change_vec >change_vec_change_vec - >nth_change_vec // >tape_move_mk_tape_R [| #_ % % ] - >reverse_cons % - | #Hc >Hta in Htc; >eq_mk_tape_rightof whd in match (tape_move ???); #Htc - >Htc in Hcurtc; >nth_change_vec // normalize in ⊢ (%→?); - #H destruct (H) @False_ind cases Hc /2/ ] - * #tf * * + -Hte1 -Hte2 #Hte // + | #Hc >Hta in Htc; >eq_mk_tape_rightof whd in match (tape_move ???); #Htc + >Htc in Hcurtc; >nth_change_vec // normalize in ⊢ (%→?); + #H destruct (H) @False_ind cases Hc /2/ ] | * #te * * * #Hcurtc #Hte1 #Hte2 - * #tf * whd in ⊢ (%→?); #Htf - * #tg * whd in ⊢ (%→%→?); #Htg #Htd - * #th * * * #Hth1 #Hth2 #Hth3 - whd in ⊢ (%→?); #Htb + whd in ⊢ (%→?); #Htb #c #ls #Hta % #Hc - [ >Htc in Hcurtc; >Hta >nth_change_vec // >tape_move_mk_tape_L // - >Hc normalize in ⊢ (%→?); * #H @False_ind /2/ + [ >Htc in Hcurtc; >Hta >nth_change_vec // + normalize in ⊢ (%→?); * #H @False_ind /2/ | cut (te = tc) [ lapply (eq_vec_change_vec ??????? (sym_eq … Hte1) Hte2) - >change_vec_same // ] -Hte1 -Hte2 #Hte - cut (th = change_vec ?? td (mk_tape ? [ ] (None ?) (reverse ? ls@[c])) cfg) - [ lapply (eq_vec_change_vec ??????? (Hth2 ls c [ ] ?) Hth3) // - >Htd >nth_change_vec_neq // >Htg >nth_change_vec // - >Htf >nth_change_vec_neq // >nth_change_vec // - >Hte >Htc >nth_change_vec // >Hta // ] -Hth1 -Hth2 -Hth3 #Hth - destruct (Hth Hte Hta Htb Htd Htg Htc Htf) - >change_vec_change_vec >change_vec_change_vec - >change_vec_commute // >change_vec_change_vec - >change_vec_commute [|@sym_not_eq //] >change_vec_change_vec - >change_vec_commute // >change_vec_change_vec - >nth_change_vec // >nth_change_vec_neq [|@sym_not_eq //] - >nth_change_vec // >nth_change_vec_neq [|@sym_not_eq //] - >change_vec_commute [|@sym_not_eq //] - @eq_f3 // - [ >Hta >tape_move_mk_tape_L // >nth_change_vec // whd in match (current ??); - @eq_f2 // cases (nth obj ? ta (niltape ?)) - [| #r0 #rs0 | #l0 #ls0 | #ls0 #c0 #rs0 ] try % - cases rs0 // - | >reverse_cons >tape_move_mk_tape_R // #_ % % ] + >change_vec_same // ] -Hte1 -Hte2 #Hte destruct (Hte) + >Hta in Htc; whd in match (tape_move ???); #Htc + >Htc in Htb; >nth_change_vec // + >nth_change_vec_neq [2:@eqb_false_to_not_eq //] >Hta + #Htb @Htb ] -] qed. definition char_to_move ≝ λc.match c with @@ -363,10 +269,11 @@ definition R_cfg_to_obj1 ≝ λt1,t2:Vector (tape FSUnialpha) 3. nth cfg ? t1 (niltape ?) = mk_tape FSUnialpha (c::ls) (None ?) [ ] → c ≠ bar → let new_obj ≝ - tape_write ? (nth obj ? t1 (niltape ?)) (char_to_bit_option c) in - t2 = change_vec ?? - (change_vec ?? t1 new_obj obj) - (mk_tape ? [ ] (option_hd ? (reverse ? (c::ls))) (tail ? (reverse ? (c::ls)))) cfg. + tape_write ? (nth obj ? t1 (niltape ?)) (char_to_bit_option c) in + t2 = change_vec ?? + (change_vec ?? t1 + (tape_write ? (nth obj ? t1 (niltape ?)) (char_to_bit_option c)) obj) + (midtape ? ls c [ ]) cfg. lemma sem_cfg_to_obj1: cfg_to_obj ⊨ R_cfg_to_obj1. @(Realize_to_Realize … sem_cfg_to_obj) #t1 #t2 #H #c #ls #Hcfg #Hbar diff --git a/matita/matita/lib/turing/simple_machines.ma b/matita/matita/lib/turing/simple_machines.ma index 66ca59a06..4b5198900 100644 --- a/matita/matita/lib/turing/simple_machines.ma +++ b/matita/matita/lib/turing/simple_machines.ma @@ -9,7 +9,203 @@ \ / GNU General Public License Version 2 V_____________________________________________________________*) -include "turing/multi_universal/match.ma". +include "turing/if_multi.ma". +include "turing/inject.ma". +include "turing/basic_machines.ma". + +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. + +definition Rm_test_null_true ≝ + λalpha,n,i.λt1,t2:Vector ? (S n). + current alpha (nth i ? t1 (niltape ?)) ≠ None ? ∧ t2 = t1. + +definition Rm_test_null_false ≝ + λalpha,n,i.λt1,t2:Vector ? (S n). + current alpha (nth i ? t1 (niltape ?)) = None ? ∧ t2 = t1. + +lemma sem_test_null_multi : ∀alpha,n,i.i ≤ n → + inject_TM ? (test_null ?) n i ⊨ + [ tc_true : Rm_test_null_true alpha n i, Rm_test_null_false alpha n i ]. +#alpha #n #i #Hin #int +cases (acc_sem_inject … Hin (sem_test_null alpha) int) +#k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ % +[ @Hloop +| #Hqtrue lapply (Htrue Hqtrue) * * #Hcur #Hnth_i #Hnth_j % // + @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) #Hi0i + [ >Hi0i @sym_eq @Hnth_i | @sym_eq @Hnth_j @sym_not_eq // ] ] +| #Hqfalse lapply (Hfalse Hqfalse) * * #Hcur #Hnth_i #Hnth_j % + [ @Hcur + | @(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 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. + +(* simple copy with no move *) +definition copy_states ≝ initN 3. + +definition cc0 : copy_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)). +definition cc1 : copy_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)). + +definition trans_copy_char_N ≝ + λsrc,dst.λsig:FinSet.λn. + λp:copy_states × (Vector (option sig) (S n)). + let 〈q,a〉 ≝ p in + match pi1 … q with + [ O ⇒ 〈cc1,change_vec ? (S n) + (change_vec ? (S n) (null_action ? n) (〈None ?,N〉) src) + (〈nth src ? a (None ?),N〉) dst〉 + | S _ ⇒ 〈cc1,null_action ? n〉 ]. + +definition copy_char_N ≝ + λsrc,dst,sig,n. + mk_mTM sig n copy_states (trans_copy_char_N src dst sig n) + cc0 (λq.q == cc1). + +definition R_copy_char_N ≝ + λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n). + outt = change_vec ?? int + (tape_write ? (nth dst ? int (niltape ?)) + (current ? (nth src ? int (niltape ?)))) dst. + +lemma copy_char_N_q0_q1 : + ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n → + step sig n (copy_char_N src dst sig n) (mk_mconfig ??? cc0 v) = + mk_mconfig ??? cc1 + (change_vec ?? v + (tape_write ? (nth dst ? v (niltape ?)) + (current ? (nth src ? v (niltape ?)))) dst). +#src #dst #sig #n #v #Heq #Hsrc #Hdst +whd in ⊢ (??%?); @eq_f +<(change_vec_same … v dst (niltape ?)) in ⊢ (??%?); +<(change_vec_same … v src (niltape ?)) in ⊢ (??%?); +>tape_move_multi_def +>pmap_change >pmap_change tape_move_null_action @eq_f3 // +[ >change_vec_same % +| >change_vec_same >change_vec_same >nth_current_chars // ] +qed. + +lemma sem_copy_char_N: + ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n → + copy_char_N src dst sig n ⊨ R_copy_char_N src dst sig n. +#src #dst #sig #n #Hneq #Hsrc #Hdst #int +%{2} % [| % [ % | whd >copy_char_N_q0_q1 // ]] +qed. + +(**************** copy and advance ***********************) +definition copy_char_states ≝ initN 3. + +definition trans_copy_char ≝ + λsrc,dst.λsig:FinSet.λn. + λp:copy_char_states × (Vector (option sig) (S n)). + let 〈q,a〉 ≝ p in + match pi1 … q with + [ O ⇒ 〈cc1,change_vec ? (S n) + (change_vec ? (S n) (null_action ? n) (〈None ?,R〉) src) + (〈nth src ? a (None ?),R〉) dst〉 + | S _ ⇒ 〈cc1,null_action ? n〉 ]. + +definition copy_char ≝ + λsrc,dst,sig,n. + mk_mTM sig n copy_char_states (trans_copy_char src dst sig n) + cc0 (λq.q == cc1). + +definition R_copy_char ≝ + λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n). + outt = change_vec ?? + (change_vec ?? int + (tape_move_mono ? (nth src ? int (niltape ?)) 〈None ?, R〉) src) + (tape_move_mono ? (nth dst ? int (niltape ?)) + 〈current ? (nth src ? int (niltape ?)), R〉) dst. + +lemma copy_char_q0_q1 : + ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n → + step sig n (copy_char src dst sig n) (mk_mconfig ??? cc0 v) = + mk_mconfig ??? cc1 + (change_vec ? (S n) + (change_vec ?? v + (tape_move_mono ? (nth src ? v (niltape ?)) 〈None ?, R〉) src) + (tape_move_mono ? (nth dst ? v (niltape ?)) 〈current ? (nth src ? v (niltape ?)), R〉) dst). +#src #dst #sig #n #v #Heq #Hsrc #Hdst +whd in ⊢ (??%?); +<(change_vec_same … v dst (niltape ?)) in ⊢ (??%?); +<(change_vec_same … v src (niltape ?)) in ⊢ (??%?); +>tape_move_multi_def @eq_f2 // +>pmap_change >pmap_change tape_move_null_action @eq_f2 // @eq_f2 +[ >change_vec_same % +| >change_vec_same >change_vec_same // ] +qed. + +lemma sem_copy_char: + ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n → + copy_char src dst sig n ⊨ R_copy_char src dst sig n. +#src #dst #sig #n #Hneq #Hsrc #Hdst #int +%{2} % [| % [ % | whd >copy_char_q0_q1 // ]] +qed. + + (********************** look_ahead test *************************)