X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Funistep_aux.ma;h=bb730a558bfa4ac58c8c0827f0033c6f901259ee;hb=7e96e893e0ebea2589f619fab861bf9984cff989;hp=aa4dbc7ab6a86387ee0a98c85b495f4441f7a9af;hpb=2a438f72ba71acd29acaae155d8ef60536140ea5;p=helm.git diff --git a/matita/matita/lib/turing/multi_universal/unistep_aux.ma b/matita/matita/lib/turing/multi_universal/unistep_aux.ma index aa4dbc7ab..bb730a558 100644 --- a/matita/matita/lib/turing/multi_universal/unistep_aux.ma +++ b/matita/matita/lib/turing/multi_universal/unistep_aux.ma @@ -57,11 +57,8 @@ 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_step 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 · @@ -69,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) ∧ @@ -77,8 +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 sem_move_to_end_l : ∀sig. move_to_end sig L ⊨ R_move_to_end_l sig. + axiom accRealize_to_Realize : ∀sig,n.∀M:mTM sig n.∀Rtrue,Rfalse,acc. M ⊨ [ acc: Rtrue, Rfalse ] → M ⊨ Rtrue ∪ Rfalse. @@ -88,11 +84,6 @@ lemma eq_mk_tape_rightof : #alpha #a #al % qed. -axiom daemon : ∀P:Prop.P. - -definition option_cons ≝ λsig.λc:option sig.λl. - match c with [ None ⇒ l | Some c0 ⇒ c0::l ]. - lemma tape_move_mk_tape_R : ∀sig,ls,c,rs. (c = None ? → ls = [ ] ∨ rs = [ ]) → @@ -103,67 +94,79 @@ lemma tape_move_mk_tape_R : normalize // qed. +lemma eq_vec_change_vec : ∀sig,n.∀v1,v2:Vector sig n.∀i,t,d. + nth i ? v2 d = t → + (∀j.i ≠ j → nth j ? v1 d = nth j ? v2 d) → + v2 = change_vec ?? v1 t i. +#sig #n #v1 #v2 #i #t #d #H1 #H2 @(eq_vec … d) +#i0 #Hlt cases (decidable_eq_nat i0 i) #Hii0 +[ >Hii0 >nth_change_vec // +| >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 ?????? (accRealize_to_Realize … (sem_copy_step …)) - (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 ⊢ (%→%→?); * #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) - [@daemon] -Htg1 -Htg2 -Htg3 #Htg destruct (Htg Htf Hte Htd Htc Htb) - >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 Hcurtc1; [|@sym_not_eq //] >Hta2 - normalize in ⊢ (%→?); #H destruct (H) % - ] - | #Hta2 >Htc in Hcurtc1; >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 %] % ] - | * #Hcurtc0 #Hte #_ #_ #c #ls #Hta1 >Hta1 in Htc; >eq_mk_tape_rightof - whd in match (tape_move ???); #Htc >Htc in Hcurtc0; * - [ >Htc in Hcurtc; >nth_change_vec_neq [|@sym_not_eq //] - #Hcurtc #Hcurtc0 >Hcurtc0 in Hcurtc; * #H @False_ind @H % - | >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H) ] + |#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 % + ] + |#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 %] ] -| * #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) - [@daemon] -Htd1 -Htd2 #Htd - -Htf1 cut (tf = change_vec ?? td (mk_tape ? [ ] (None ?) (reverse ? ls@[null])) cfg) - [@daemon] -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/ ] ] qed. @@ -194,85 +197,124 @@ definition cfg_to_obj ≝ mmove cfg FSUnialpha 2 L · (ifTM ?? (inject_TM ? test_null_char 2 cfg) (nop ? 2) - (copy_step 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. + (c = None ? → ls = [ ] ∨ rs = [ ]) → + tape_move ? (mk_tape sig ls c rs) L = + mk_tape ? (tail ? ls) (option_hd ? ls) (option_cons ? c rs). +#sig * [ * [ * | #c * ] | #l0 #ls0 * [ * +[| #r0 #rs0 #H @False_ind cases (H (refl ??)) #H1 destruct (H1) ] | #c * ] ] +normalize // +qed. -axiom 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 ?????????? - (sem_test_null_multi ?? obj ?) - (sem_seq ?????? (accRealize_to_Realize … (sem_copy_step …)) - (sem_move_multi ? 2 cfg L ?)) - (sem_inject ???? cfg ? (sem_write FSUnialpha null))) - (sem_seq ?????? (sem_inject ???? cfg ? (sem_move_to_end_l ?)) - (sem_move_multi ? 2 cfg R ?)))) // +lemma sem_cfg_to_obj : cfg_to_obj ⊨ R_cfg_to_obj. +@(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?) + (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 #Hte - * destruct (Hte) #te * * - [ whd in ⊢ (%→%→?); * #x * #y * * -Hcurtc #Hcurtc1 #Hcurtc2 #Hte #Htd - * #tf * * * whd in ⊢ (%→%→%→%→?); #Htf1 #Htf2 #Htf3 #Htb - #c #ls #Hta1 % - [ #lso #x0 #rso #Hta2 >Hta1 in Htc; >eq_mk_tape_rightof - whd in match (tape_move ???); #Htc - cut (tf = change_vec ?? tc (mk_tape ? [ ] (None ?) (reverse ? ls@[x])) cfg) - [@daemon] -Htf1 -Htf2 -Htf3 #Htf destruct (Htf Hte Htd Htc Htb) - >change_vec_change_vec >change_vec_change_vec >change_vec_change_vec - >nth_change_vec // >tape_move_mk_tape_R - @daemon - | #Hta2 >Htc in Hcurtc1; >nth_change_vec_neq [| @sym_not_eq //] - >Hta2 #H destruct (H) - ] - | * #Hcurtc0 #Hte #_ #_ #c #ls #Hta1 >Hta1 in Htc; >eq_mk_tape_rightof - whd in match (tape_move ???); #Htc >Htc in Hcurtc0; * - [ >Htc in Hcurtc; >nth_change_vec_neq [|@sym_not_eq //] - #Hcurtc #Hcurtc0 >Hcurtc0 in Hcurtc; * #H @False_ind @H % - | >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H) ] +[ * #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 // + | #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 + whd in ⊢ (%→?); #Htb + #c #ls #Hta % #Hc + [ >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 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 ] -| * #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) - [@daemon] -Htd1 -Htd2 #Htd - -Htf1 cut (tf = change_vec ?? td (mk_tape ? [ ] (None ?) (reverse ? ls@[null])) cfg) - [@daemon] -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/ ] -] qed. -*) - -(* macchina che muove il nastro obj a destra o sinistra a seconda del valore - del current di prg, che codifica la direzione in cui ci muoviamo *) definition char_to_move ≝ λc.match c with [ bit b ⇒ if b then R else L | _ ⇒ N]. - + +definition char_to_bit_option ≝ λc.match c with + [ bit b ⇒ Some ? (bit b) + | _ ⇒ None ?]. + +definition R_cfg_to_obj1 ≝ λt1,t2:Vector (tape FSUnialpha) 3. + ∀c,ls. + 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 + (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 +cases (H c ls Hcfg) cases (true_or_false (c==null)) #Hc + [#Ht2 #_ >(Ht2 (\P Hc)) -Ht2 @(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 in ⊢ (???%); [2:@eqb_false_to_not_eq %] + >nth_change_vec // >(\P Hc) % + |#Hi >Hi >nth_change_vec // + ] + |#Hi >Hi >nth_change_vec_neq [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 %] % + ] + |#_ #Ht2 >(Ht2 (\Pf Hc)) -Ht2 @(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 in ⊢ (???%); [2:@eqb_false_to_not_eq %] + >nth_change_vec // >nth_change_vec // + lapply (\bf Hbar) lapply Hc elim c // + [whd in ⊢ (??%?→?); #H destruct (H) + |#_ whd in ⊢ (??%?→?); #H destruct (H) + ] + |#Hi >Hi >nth_change_vec // + ] + |#Hi >Hi >nth_change_vec_neq [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 %] % + ] + ] +qed. + + +(* macchina che muove il nastro obj a destra o sinistra a seconda del valore + del current di prg, che codifica la direzione in cui ci muoviamo *) + definition tape_move_obj : mTM FSUnialpha 2 ≝ ifTM ?? (inject_TM ? (test_char ? (λc:FSUnialpha.c == bit false)) 2 prg) @@ -284,64 +326,133 @@ definition tape_move_obj : mTM FSUnialpha 2 ≝ tc_true) tc_true. -definition restart_tape ≝ λi. - inject_TM ? (move_to_end FSUnialpha L) 2 i · - mmove i FSUnialpha 2 R. +definition R_tape_move_obj' ≝ λt1,t2:Vector (tape FSUnialpha) 3. + (current ? (nth prg ? t1 (niltape ?)) = Some ? (bit false) → + t2 = change_vec ?? t1 (tape_move ? (nth obj ? t1 (niltape ?)) L) obj) ∧ + (current ? (nth prg ? t1 (niltape ?)) = Some ? (bit true) → + t2 = change_vec ?? t1 (tape_move ? (nth obj ? t1 (niltape ?)) R) obj) ∧ + (current ? (nth prg ? t1 (niltape ?)) ≠ Some ? (bit false) → + current ? (nth prg ? t1 (niltape ?)) ≠ Some ? (bit true) → + t2 = t1). + +lemma sem_tape_move_obj' : tape_move_obj ⊨ R_tape_move_obj'. +#ta cases (sem_if ?????????? + (acc_sem_inject ?????? prg ? (sem_test_char ? (λc:FSUnialpha.c == bit false))) + (sem_move_multi ? 2 obj L ?) + (sem_if ?????????? + (acc_sem_inject ?????? prg ? (sem_test_char ? (λc:FSUnialpha.c == bit true))) + (sem_move_multi ? 2 obj R ?) + (sem_nop …)) ta) // +#i * #outc * #Hloop #HR %{i} %{outc} % [@Hloop] -i +cases HR -HR +[ * #tb * * * * #c * #Hcurta_prg #Hc lapply (\P Hc) -Hc #Hc #Htb1 #Htb2 + whd in ⊢ (%→%); #Houtc >Houtc -Houtc % [ % + [ >Hcurta_prg #H destruct (H) >(?:tb = ta) + [| lapply (eq_vec_change_vec ??????? Htb1 Htb2) + >change_vec_same // ] % + | >Hcurta_prg #H destruct (H) destruct (Hc) ] + | >Hcurta_prg >Hc * #H @False_ind /2/ ] +| * #tb * * * #Hnotfalse #Htb1 #Htb2 cut (tb = ta) + [ lapply (eq_vec_change_vec ??????? Htb1 Htb2) + >change_vec_same // ] -Htb1 -Htb2 #Htb destruct (Htb) * + [ * #tc * * * * #c * #Hcurta_prg #Hc lapply (\P Hc) -Hc #Hc #Htc1 #Htc2 + whd in ⊢ (%→%); #Houtc >Houtc -Houtc % [ % + [ >Hcurta_prg #H destruct (H) destruct (Hc) + | >Hcurta_prg #H destruct (H) >(?:tc = ta) + [| lapply (eq_vec_change_vec ??????? Htc1 Htc2) + >change_vec_same // ] % ] + | >Hcurta_prg >Hc #_ * #H @False_ind /2/ ] + | * #tc * * * #Hnottrue #Htc1 #Htc2 cut (tc = ta) + [ lapply (eq_vec_change_vec ??????? Htc1 Htc2) + >change_vec_same // ] -Htc1 -Htc2 + #Htc destruct (Htc) whd in ⊢ (%→?); #Houtc % [ % + [ #Hcurta_prg lapply (\Pf (Hnotfalse ? Hcurta_prg)) * #H @False_ind /2/ + | #Hcurta_prg lapply (\Pf (Hnottrue ? Hcurta_prg)) * #H @False_ind /2/ ] + | #_ #_ @Houtc ] + ] +] +qed. -definition unistep ≝ - obj_to_cfg · match_m cfg prg FSUnialpha 2 · - restart_tape cfg · copy prg cfg FSUnialpha 2 · - cfg_to_obj · tape_move_obj · restart_tape prg. +definition R_tape_move_obj ≝ λt1,t2:Vector (tape FSUnialpha) 3. + ∀c. current ? (nth prg ? t1 (niltape ?)) = Some ? c → + t2 = change_vec ?? t1 (tape_move ? (nth obj ? t1 (niltape ?)) (char_to_move c)) obj. -(* -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 → *) +lemma sem_tape_move_obj : tape_move_obj ⊨ R_tape_move_obj. +@(Realize_to_Realize … sem_tape_move_obj') +#ta #tb * * #Htb1 #Htb2 #Htb3 * [ * +[ @Htb2 | @Htb1 ] +| #Hcurta_prg change with (nth obj ? ta (niltape ?)) in match (tape_move ???); + >change_vec_same @Htb3 >Hcurta_prg % #H destruct (H) +| #Hcurta_prg change with (nth obj ? ta (niltape ?)) in match (tape_move ???); + >change_vec_same @Htb3 >Hcurta_prg % #H destruct (H) +] +qed. -definition list_of_tape ≝ λsig,t. - left sig t@option_cons ? (current ? t) (right ? t). +definition list_of_tape ≝ λsig.λt:tape sig. + reverse ? (left ? t)@option_cons ? (current ? t) (right ? t). -definition low_char' ≝ λc. - match c with - [ None ⇒ null - | Some b ⇒ if (is_bit b) then b else null - ]. +definition restart_tape ≝ λi,n. + mmove i FSUnialpha n L · + inject_TM ? (move_to_end FSUnialpha L) n i · + mmove i FSUnialpha n R. -definition R_unistep ≝ λn,l,h.λt1,t2: Vector ? 3. - ∀state,oldc,table. - (* cfg *) - nth cfg ? t1 (niltape ?) = midtape ? [ ] bar (state@[oldc]) → - is_config n (bar::state@[oldc]) → - (* prg *) - nth prg ? t1 (niltape ?) = midtape ? [ ] bar table → - bar::table = table_TM n l h → - (* obj *) - only_bits (list_of_tape ? (nth obj ? t1 (niltape ?))) → - let char ≝ low_char' (current ? (nth obj ? t1 (niltape ?))) in - let conf ≝ (bar::state@[char]) in - (∃ll,lr.bar::table = ll@conf@lr) → - ∃nstate,nchar,m,t. tuple_encoding n h t = (conf@nstate@[nchar;m]) ∧ - mem ? t l ∧ - t2 = - change_vec ?? - (change_vec ?? t1 (midtape ? [ ] bar (nstate@[nchar])) cfg) - (tape_move_mono ? (nth obj ? t1 (niltape ?)) 〈Some ? nchar,char_to_move m〉) obj. +definition R_restart_tape ≝ λi,n.λint,outt:Vector (tape FSUnialpha) (S n). + ∀t.t = nth i ? int (niltape ?) → + outt = change_vec ?? int + (mk_tape ? [ ] (option_hd ? (list_of_tape ? t)) (tail ? (list_of_tape ? t))) i. -definition tape_map ≝ λA,B:FinSet.λf:A→B.λt. - mk_tape B (map ?? f (left ? t)) - (option_map ?? f (current ? t)) - (map ?? f (right ? t)). - -definition low ≝ λM:normalTM.λc:nconfig (no_states M).Vector_of_list ? - [tape_map ?? bit (ctape ?? c); - midtape ? [ ] bar (bits_of_state ? (nhalt M) (cstate ?? c)); - midtape ? [ ] bar (table_TM ? (graph_enum ?? (ntrans M)) (nhalt M)) - ]. +lemma sem_restart_tape : ∀i,n.i < S n → restart_tape i n ⊨ R_restart_tape i n. +#i #n #Hleq +@(sem_seq_app ??????? (sem_move_multi ? n i L ?) + (sem_seq ?????? (sem_inject ???? i ? (sem_move_to_end_l ?)) + (sem_move_multi ? n i R ?))) [1,2,3:@le_S_S_to_le //] +#ta #tb * #tc * whd in ⊢ (%→?); #Htc +* #td * * * #Htd1 #Htd2 #Htd3 +whd in ⊢ (%→?); #Htb * +[ #Hta_i Htc in Htd1; >nth_change_vec // *) -Htd1 -Htd2 -Htd3 + #Htd >Htd in Htb; >Htc >change_vec_change_vec >nth_change_vec // + #Htb >Htb % +| #r0 #rs0 #Hta_i Htc in Htd1; >nth_change_vec // *) -Htd1 -Htd2 -Htd3 + #Htd >Htd in Htb; >Htc >change_vec_change_vec >nth_change_vec // + #Htb >Htb % +| #l0 #ls0 #Hta_i Htd in Htb; >Htc >change_vec_change_vec >change_vec_change_vec + >nth_change_vec // #Htb >Htb <(reverse_reverse ? ls0) in ⊢ (???%); + cases (reverse ? ls0) + [ % + | #l1 #ls1 >reverse_cons + >(?: list_of_tape ? (rightof ? l0 (reverse ? ls1@[l1])) = + l1::ls1@[l0]) + [|change with (reverse ??@?) in ⊢ (??%?); + whd in match (left ??); >reverse_cons >reverse_append + whd in ⊢ (??%?); @eq_f >reverse_reverse normalize >append_nil % ] % ] +| * + [ #c #rs #Hta_i Htc in Htd1; >nth_change_vec // *) -Htd1 -Htd2 -Htd3 + #Htd >Htd in Htb; >Htc >change_vec_change_vec >nth_change_vec // + #Htb >Htb % + | #l0 #ls0 #c #rs #Hta_i Htd in Htb; >Htc >change_vec_change_vec >change_vec_change_vec + >nth_change_vec // #Htb >Htb <(reverse_reverse ? ls0) in ⊢ (???%); + cases (reverse ? ls0) + [ % + | #l1 #ls1 >reverse_cons + >(?: list_of_tape ? (midtape ? (l0::reverse ? ls1@[l1]) c rs) = + l1::ls1@l0::c::rs) + [|change with (reverse ??@?) in ⊢ (??%?); + whd in match (left ??); >reverse_cons >reverse_append + whd in ⊢ (??%?); @eq_f >reverse_reverse normalize + >associative_append % ] % ] + ] +] +qed. - - - - \ No newline at end of file