X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Funistep.ma;h=2e4e1e253d2425dd7a237b6930f1f03628d8d773;hb=3026dfea8eae158433ed13df5156a733fa926794;hp=85bf12e8375c6432477a34e6a4cbb803d4955049;hpb=9956360248d4d6cda67fb1363de22097ccaed533;p=helm.git diff --git a/matita/matita/lib/turing/multi_universal/unistep.ma b/matita/matita/lib/turing/multi_universal/unistep.ma index 85bf12e83..2e4e1e253 100644 --- a/matita/matita/lib/turing/multi_universal/unistep.ma +++ b/matita/matita/lib/turing/multi_universal/unistep.ma @@ -12,10 +12,87 @@ include "turing/multi_universal/unistep_aux.ma". +definition exec_move ≝ + cfg_to_obj · tape_move_obj · restart_tape prg 2 · obj_to_cfg. + +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 → + only_bits (list_of_tape ? (nth obj ? t1 (niltape ?))) → + 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_cfg1))) // +#ta #tout * #t1 * #semM1 * #t2 * #semM2 * #t3 * #semM3 #semM4 +#c #m #ls1 #ls2 #rs2 #Hcfg #Hprg #Honlybits #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 *) +whd in semM4; >Ht3 in semM4; +>nth_change_vec_neq [2:@eqb_false_to_not_eq %] +>nth_change_vec [2:@leb_true_to_le %] #semM4 lapply (semM4 … (refl ??)) -semM4 +>nth_change_vec_neq [2:@eqb_false_to_not_eq %] +>nth_change_vec_neq [2:@eqb_false_to_not_eq %] +>nth_change_vec [2:@leb_true_to_le %] #semM4 >(semM4 ?) + [(* tape by tape *) + @(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 %] + >nth_change_vec_neq [2:@eqb_false_to_not_eq %] + >nth_change_vec [2:@leb_true_to_le %] % + |#Hi >Hi (* obj tape *) + >nth_change_vec [2:@leb_true_to_le %] whd in ⊢ (???%); + >reverse_cons >reverse_append >reverse_single + whd in match (option_hd ??); whd in match (tail ??); + whd in ⊢ (??%?); % + ] + |#Hi >Hi (* prg tape *) + >nth_change_vec_neq [2:@eqb_false_to_not_eq %] + >nth_change_vec [2:@leb_true_to_le %] whd in ⊢ (???%); + >Hprg whd in match (list_of_tape ??); >reverse_append + >reverse_single % + ] + |#b #Hcurrent @(list_of_tape_write ? is_bit … (char_to_bit_option c) ? Honlybits) + [#b0 cases c + [#b1 whd in ⊢ (??%?→?); #Hbit destruct (Hbit) % + |whd in ⊢ (??%?→?); #Hbit destruct (Hbit) + |whd in ⊢ (??%?→?); #Hbit destruct (Hbit) + ] + |>(list_of_tape_move … (char_to_move m)) @current_in_list @Hcurrent + ] + ] +qed. + 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. + exec_move. (* definition legal_tape ≝ λn,l,h,t. @@ -25,17 +102,6 @@ definition legal_tape ≝ λn,l,h,t. nth prg ? t1 (niltape ?) = midtape ? [ ] bar table → bar::table = table_TM n l h → *) -definition low_char' ≝ λc. - match c with - [ None ⇒ null - | Some b ⇒ if (is_bit b) then b else null - ]. - -lemma low_char_option : ∀s. - low_char' (option_map FinBool FSUnialpha bit s) = low_char s. -* // -qed. - definition R_unistep ≝ λn,l,h.λt1,t2: Vector ? 3. ∀state,char,table. (* cfg *) @@ -85,15 +151,15 @@ definition R_copy_strict ≝ axiom sem_copy_strict : ∀src,dst,sig,n. src ≠ dst → src < S n → dst < S n → copy src dst sig n ⊨ R_copy_strict src dst sig n. +axiom daemon : ∀P:Prop.P. + lemma sem_unistep : ∀n,l,h.unistep ⊨ R_unistep n l h. #n #l #h @(sem_seq_app ??????? (sem_match_m cfg prg FSUnialpha 2 ???) (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_tape_move_obj - (sem_seq ?????? (sem_restart_tape ???) sem_obj_to_cfg))))))) + (sem_exec_move …))))) /2 by le_n,sym_not_eq/ #ta #tb #HR #state #char #table #Hta_cfg #Hcfg #Hta_prg #Htable #Hbits_obj #Htotaltable @@ -112,7 +178,7 @@ cases HR -HR #tc * whd in ⊢ (%→?); >(?: list_of_tape ? (mk_tape ? (reverse ? (state@[char])@[bar]) (None ?) [ ]) = bar::state@[char]) [|whd in ⊢ (??%?); >left_mk_tape >reverse_append >reverse_reverse - >current_mk_tape >right_mk_tape normalize >append_nil % ] + >current_mk_tape >right_mk_tape [| #_ %2 % ] normalize >append_nil % ] whd in ⊢ (???(???(????%?)??)→?); whd in match (tail ??); #Htd (* move cfg to R *) * #te * whd in ⊢ (%→?); >Htd @@ -120,11 +186,11 @@ whd in ⊢ (???(???(????%?)??)→?); whd in match (tail ??); #Htd >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec // >Htable in Hintable; #Hintable #Hte (* copy *) -cases (cfg_in_table_to_tuple ???? Hcfg ?? Hintable) -#newstate * #m0 * #lr0 * * #Hlr destruct (Hlr) #Hnewcfg #Hm0 -cut (∃fo,so,co.state = fo::so@[co] ∧ |so| = n) -[ @daemon ] * #fo * #so * #co * #Hstate_exp #Hsolen -cut (∃fn,sn,cn.newstate = fn::sn@[cn] ∧ |sn| = n) +lapply (cfg_in_table_to_tuple ???? Hcfg ?? Hintable) +* #newconfig * #m0 * #lr0 * * #Hlr destruct (Hlr) #Hnewcfg #Hm0 +cut (∃fo,so.state = fo::so ∧ |so| = n) +[ @daemon ] * #fo * #so * #Hstate_exp #Hsolen +cut (∃fn,sn,cn.newconfig = fn::sn@[cn] ∧ |sn| = n) [ @daemon ] * #fn * #sn * #cn * #Hnewstate_exp #Hsnlen * #tf * * #_ >Hte >(nth_change_vec ?????? lt_prg) >nth_change_vec_neq [|@sym_not_eq //] >(nth_change_vec ?????? lt_cfg) @@ -132,15 +198,82 @@ cut (∃fn,sn,cn.newstate = fn::sn@[cn] ∧ |sn| = n) whd in match (mk_tape ????); whd in match (tape_move ???); #Htf cases (Htf ?????? (refl ??) (refl ??) ?) -Htf [| whd in match (tail ??); >length_append >length_append - >Hsolen >length_append >length_append >Hsnlen - Hsolen >length_append >Hsnlen //] #rs1 * #rs2 whd in match (tail ??); * * ->append_cons #Hrs1rs2 #Hrs1len +#Hrs1rs2 #Hrs1len >change_vec_change_vec >change_vec_commute [|@sym_not_eq //] ->change_vec_change_vec #Htf -(* cfg to obj *) -* #tg * whd in ⊢ (%→?); >Htf ->nth_change_vec_neq [|@sym_not_eq //] >(nth_change_vec ?????? lt_cfg) +>change_vec_change_vec >append_nil #Htf +(* exec_move *) +cut ((sn@[cn])=rs1) + [@(append_l1_injective ?????? Hrs1rs2) >Hrs1len + >length_append >length_append normalize >Hsolen >Hsnlen % ] #Hrs1 +cut (m0::lr0=rs2) [@(append_l2_injective ?????? Hrs1rs2) >Hrs1 % ] #Hrs2 +cut (∃ll1. ll@[bar] = bar::ll1) + [@daemon (* ll is at the begininng of a table *)] * #ll1 #Hll +whd in ⊢ (%→?); >Htf >nth_change_vec_neq [2:@eqb_false_to_not_eq %] +>nth_change_vec [2:@leb_true_to_le %] +>nth_change_vec [2:@leb_true_to_le %] +>nth_change_vec_neq [2:@eqb_false_to_not_eq %] +>nth_change_vec_neq [2:@eqb_false_to_not_eq %] +>append_cons reverse_append >reverse_single +(append_cons … bar ll) >Hll >reverse_cons +#sem_exec_move +lapply + (sem_exec_move ? m0 ? + (([cn]@reverse FSUnialpha sn) + @fn::reverse FSUnialpha (ll1@(fo::so)@[char])) lr0 … (refl ??) ????) + [@Hm0 + |@daemon (* OK *) + |@Hbits_obj + |whd in ⊢ (??%?); >associative_append >associative_append + >associative_append % + |#Htb >Htb @(eq_vec … (niltape ?)) (* tape by tape *) #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 [2:@leb_true_to_le %] + (* dimostrare che la tabella e' univoca + da cui m = m0 e nchar = cn *) + |(* cfg tape *) #eqi >eqi + >nth_change_vec_neq [2:@eqb_false_to_not_eq %] + >nth_change_vec [2:@leb_true_to_le %] + (* idem *) + ] + |(* prg tape *) #eqi >eqi + >nth_change_vec_neq [2:@eqb_false_to_not_eq %] + >nth_change_vec_neq [2:@eqb_false_to_not_eq %] + >Hta_prg whd in ⊢ (??%?); @eq_f @(cons_injective_r ? bar bar) + >Htable >Hintable >reverse_append >reverse_cons + >reverse_reverse >reverse_cons >reverse_reverse + >associative_append >associative_append >associative_append + >(append_cons ? bar ll) >Hll @eq_f @eq_f Hnewstate_exp % + ] + ] + + +qed. + + + + 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 %]