X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Funi_step.ma;h=eabab3e838c66dbac33a0da3b8e42eae2f708d5b;hb=39aab7babf51252cecb81a66af82fe797e8dcbe7;hp=5286a33401914cc2a8e1e5c3f1077f182df12a0d;hpb=fb0cac5935fe56077893f6f02390c40dd1188953;p=helm.git diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma index 5286a3340..eabab3e83 100644 --- a/matita/matita/lib/turing/universal/uni_step.ma +++ b/matita/matita/lib/turing/universal/uni_step.ma @@ -15,6 +15,8 @@ *) include "turing/universal/copy.ma". +include "turing/universal/move_tape.ma". +include "turing/universal/match_machines.ma". (* @@ -55,46 +57,44 @@ if is_true(current) (* current state is final *) *) definition init_match ≝ - seq ? (mark ?) - (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c))) - (seq ? (move_r ?) - (seq ? (mark ?) - (seq ? (move_l ?) - (adv_to_mark_l ? (is_marked ?)))))). - + mark ? · adv_to_mark_r ? (λc:STape.is_grid (\fst c)) · move_r ? · + move_r ? · mark ? · move_l ? · adv_to_mark_l ? (is_marked ?). + definition R_init_match ≝ λt1,t2. ∀ls,l,rs,c,d. no_grids (〈c,false〉::l) → no_marks l → - t1 = midtape STape ls 〈c,false〉 (l@〈grid,false〉::〈d,false〉::rs) → - t2 = midtape STape ls 〈c,true〉 (l@〈grid,false〉::〈d,true〉::rs). + t1 = midtape STape ls 〈c,false〉 (l@〈grid,false〉::〈bar,false〉::〈d,false〉::rs) → + t2 = midtape STape ls 〈c,true〉 (l@〈grid,false〉::〈bar,false〉::〈d,true〉::rs). lemma sem_init_match : Realize ? init_match R_init_match. #intape cases (sem_seq ????? (sem_mark ?) (sem_seq ????? (sem_adv_to_mark_r ? (λc:STape.is_grid (\fst c))) (sem_seq ????? (sem_move_r ?) - (sem_seq ????? (sem_mark ?) - (sem_seq ????? (sem_move_l ?) - (sem_adv_to_mark_l ? (is_marked ?)))))) intape) + (sem_seq ????? (sem_move_r ?) + (sem_seq ????? (sem_mark ?) + (sem_seq ????? (sem_move_l ?) + (sem_adv_to_mark_l ? (is_marked ?))))))) intape) #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop #ls #l #rs #c #d #Hnogrids #Hnomarks #Hintape cases HR -HR -#ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta -Hintape #Hta -* #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Htb -Hta +#ta * whd in ⊢ (%→?); * #Hta #_ lapply (Hta … Hintape) -Hta -Hintape #Hta +* #tb * whd in ⊢ (%→?); * #_ #Htb cases (Htb … Hta) -Htb -Hta [* #Hgridc @False_ind @(absurd … Hgridc) @eqnot_to_noteq @(Hnogrids 〈c,false〉) @memb_hd ] -* #Hgrdic #Htb lapply (Htb l 〈grid,false〉 (〈d,false〉::rs) (refl …) (refl …) ?) +* * #Hgrdic #Htb #_ lapply (Htb l 〈grid,false〉 (〈bar,false〉::〈d,false〉::rs) (refl …) (refl …) ?) [#x #membl @Hnogrids @memb_cons @membl] -Htb #Htb -* #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc -Htb #Htc -* #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd -Htc #Htd -* #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Hte -Htd #Hte -whd in ⊢ (%→?); #Htf cases (Htf … Hte) -Htf -Hte - [* whd in ⊢ ((??%?)→?); #Habs destruct (Habs)] -* #_ #Htf lapply (Htf (reverse ? l) 〈c,true〉 ls (refl …) (refl …) ?) - [#x #membl @Hnomarks @daemon] -Htf #Htf >Htf >reverse_reverse % +* #tc * whd in ⊢ (%→?); * #_ #Htc lapply (Htc … Htb) -Htc -Htb #Htc +* #td * whd in ⊢ (%→?); * #_ #Htd lapply (Htd … Htc) -Htd -Htc #Htd +* #te * whd in ⊢ (%→?); * #Hte #_ lapply (Hte … Htd) -Hte -Htd #Hte +* #tf * whd in ⊢ (%→?); * #_ #Htf lapply (Htf … Hte) -Htf -Hte #Htf +whd in ⊢ (%→?); * #_ #Htg cases (Htg … Htf) -Htg -Htf +#_ #Htg cases (Htg (refl …)) -Htg #Htg #_ +lapply (Htg (〈grid,false〉::reverse ? l) 〈c,true〉 ls (refl …) (refl …) ?) + [#x #membl @Hnomarks @daemon] -Htg #Htg >Htg >reverse_cons >reverse_reverse + >associative_append % qed. - (* init_copy init_current_on_match; (* no marks in current *) @@ -105,10 +105,8 @@ qed. *) definition init_copy ≝ - seq ? init_current_on_match - (seq ? (move_r ?) - (seq ? (adv_to_mark_r ? (is_marked ?)) - (adv_mark_r ?))). + init_current_on_match · move_r ? · + adv_to_mark_r ? (is_marked ?) · adv_mark_r ?. definition R_init_copy ≝ λt1,t2. ∀l1,l2,c,ls,d,rs. @@ -136,21 +134,22 @@ cases (sem_seq ????? sem_init_current_on_match #l1 #l2 #c #ls #d #rs #Hl1marks #Hl1grids #Hl2marks #Hc #Hintape cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hl1grids Hc Hintape) -Hta -Hintape #Hta -* #tb * whd in ⊢ (%→?); #Htb lapply (Htb … Hta) -Htb -Hta +* #tb * whd in ⊢ (%→?); * #_ #Htb lapply (Htb … Hta) -Htb -Hta generalize in match Hl1marks; -Hl1marks cases (list_last ? l1) [#eql1 >eql1 #Hl1marks whd in ⊢ ((???%)→?); whd in ⊢ ((???(????%))→?); #Htb - * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc -Htb * + * #tc * whd in ⊢ (%→?); * #_ #Htc lapply (Htc … Htb) -Htc -Htb * [* whd in ⊢ ((??%?)→?); #Htemp destruct (Htemp)] - * #_ #Htc lapply (Htc … (refl …) (refl …) ?) + * * #_ #Htc #_ lapply (Htc … (refl …) (refl …) ?) [#x #membx @Hl2marks @membx] - #Htc whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc) -Houtc -Htc #Houtc + #Htc whd in ⊢ (%→?); * #Houtc #_ cases (Houtc (reverse ? l2@〈grid,false〉::〈c,true〉::〈grid,false〉::ls) comma) + -Houtc #Houtc lapply (Houtc … Htc) -Houtc -Htc #Houtc #_ >Houtc % |* #c1 * #tl #eql1 >eql1 #Hl1marks >reverse_append >reverse_single whd in ⊢ ((???%)→?); whd in ⊢ ((???(????%))→?); >associative_append whd in ⊢ ((???(????%))→?); #Htb - * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc -Htb * + * #tc * whd in ⊢ (%→?); * #_ #Htc lapply (Htc … Htb) -Htc -Htb * [* >Hl1marks [#Htemp destruct (Htemp)] @memb_append_l2 @memb_hd] - * #_ >append_cons append_cons Houtc >reverse_append >reverse_append >reverse_single >reverse_reverse >associative_append >associative_append >associative_append % @@ -234,12 +235,8 @@ cases HR -HR ] qed. *) -include "turing/universal/move_tape.ma". - -definition exec_move ≝ - seq ? init_copy - (seq ? copy - (seq ? (move_r …) move_tape)). +definition exec_action ≝ + init_copy · copy · move_r … · move_tape. definition map_move ≝ λc,mv.match c with [ null ⇒ None ? | _ ⇒ Some ? 〈c,false,move_of_unialpha mv〉 ]. @@ -251,7 +248,18 @@ definition map_move ≝ mv ≠ null → c1 ≠ null dal fatto che c1 e mv sono contenuti nella table *) -definition R_exec_move ≝ λt1,t2. + +definition Pre_exec_action ≝ λt1. + ∃n,curconfig,ls,rs,c0,c1,s0,s1,table1,newconfig,mv,table2. + table_TM n (table1@〈comma,false〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2) ∧ + no_marks curconfig ∧ only_bits (curconfig@[〈s0,false〉]) ∧ + only_bits (〈s1,false〉::newconfig) ∧ bit_or_null c1 = true ∧ + |curconfig| = |newconfig| ∧ + legal_tape ls 〈c0,false〉 rs ∧ + t1 = midtape STape (〈c0,false〉::curconfig@〈s0,false〉::〈grid,false〉::ls) 〈grid,false〉 + (table1@〈comma,true〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs). + +definition R_exec_action ≝ λt1,t2. ∀n,curconfig,ls,rs,c0,c1,s0,s1,table1,newconfig,mv,table2. table_TM n (table1@〈comma,false〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2) → no_marks curconfig → only_bits (curconfig@[〈s0,false〉]) → @@ -325,96 +333,114 @@ qed. *) -lemma sem_exec_move : Realize ? exec_move R_exec_move. -#intape -cases (sem_seq … sem_init_copy - (sem_seq … sem_copy - (sem_seq … (sem_move_r …) sem_move_tape )) intape) -#k * #outc * #Hloop #HR -@(ex_intro ?? k) @(ex_intro ?? outc) % [ @Hloop ] -Hloop -#n #curconfig #ls #rs #c0 #c1 #s0 #s1 #table1 #newconfig #mv #table2 -#Htable #Hcurconfig1 #Hcurconfig2 #Hnewconfig #Hc1 #Hlen #Htape #Hintape #t1' #Ht1' -cases HR -HR #ta * whd in ⊢ (%→?); #Hta -lapply (Hta (〈c0,false〉::curconfig) table1 s0 ls s1 - (newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs) … Hintape) -Hta +(*lemma GRealize_to_Realize : + ∀sig,M,R.GRealize sig M (λx.True) R → Realize sig M R. +#sig #M #R #HR #t @HR // +qed.*) + +lemma sem_exec_action : GRealize ? exec_action Pre_exec_action R_exec_action. +@(sem_seq_app_guarded … (Realize_to_GRealize … sem_init_copy) ???) +[3:@(sem_seq_app_guarded … sem_copy) + [3:@(sem_seq_app_guarded … (Realize_to_GRealize … (sem_move_r STape))) + [3:@(Realize_to_GRealize … (sem_move_tape …)) + |@(λt.True) + |4:// + |5:@sub_reflexive] + |@(λt.True) + |4:// + |5:@sub_reflexive] +|4:#t1 #t2 + * #n * #curconfig * #ls * #rs * #c0 * #c1 * #s0 * #s1 * #table1 * #newconfig + * #mv * #table2 * * * * * * * + #Htable #Hcurconfig1 #Hcurconfig2 #Hnewconfig #Hc1 #Hlen #Htape #Ht1 + whd in ⊢ (%→?); >Ht1 #HR + lapply (HR (〈c0,false〉::curconfig) table1 s0 ls s1 + (newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs) ???? (refl ??)) + [(*Hcurconfig2*) @daemon + |(*by Htable *) @daemon + |(*Hcurconfig2*) @daemon + |(*Hcurconfig1*) @daemon ] + -HR #Ht2 whd + %{(〈grid,false〉::ls)} %{s0} %{s1} %{c0} %{c1} %{(〈mv,false〉::table2@〈grid,false〉::rs)} + %{newconfig} %{(〈comma,false〉::reverse ? table1)} %{curconfig} >Ht2 + % [ % [ % [ % [ % [ % [ % [ % + [ % + |(*by Htabel*) @daemon ] + |(*by Htable*) @daemon ] + |// ] + |>Hlen % ] + |@Hcurconfig2 ] + |@Hnewconfig ] + |cases Htape * * // ] + | // ] + |1,2:skip] +#ta #outtape #HR #n #curconfig #ls #rs #c0 #c1 #s0 #s1 #table1 #newconfig #mv +#table2 #Htable #Hcurconfig1 #Hcurconfig2 #Hnewconfig #Hbitnullc1 #Hlen #Htape +#Hta #ta' #Hta' +cases HR -HR #tb * whd in ⊢ (%→?); #Htb +lapply (Htb (〈c0,false〉::curconfig) table1 s0 ls s1 + (newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs) + ???? Hta) -Htb [ (*Hcurconfig2*) @daemon | (*Htable*) @daemon -| (*bit_or_null c0 = true *) @daemon -| (*Hcurconfig1*) @daemon -| #Hta * #tb * whd in ⊢ (%→?); #Htb - lapply (Htb (〈grid,false〉::ls) s0 s1 c0 c1 (〈mv,false〉::table2@〈grid,false〉::rs) newconfig (〈comma,false〉::reverse ? table1) curconfig Hta ????????) -Htb - [9:|*:(* bit_or_null c0,c1; |curconfig| = |newconfig|*) @daemon ] - #Htb * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc whd in ⊢(???(??%%%)→?);#Htc - whd in ⊢ (%→?); #Houtc whd in Htc:(???%); whd in Htc:(???(??%%%)); - lapply (Houtc rs n - (〈comma,false〉::〈c1,false〉::reverse ? newconfig@〈s1,false〉::〈comma,false〉::reverse ? table1) - mv table2 (merge_char c0 c1) (reverse ? newconfig@[〈s1,false〉]) ls ????????) - [3: cases Htape -Htape * * #Hnomarks #Hbits #Hc0 #Hlsrs % [ % [ % - [ #x #Hx cases (orb_true_l … Hx) #Hx' - [ >(\P Hx') % - | @Hnomarks @memb_cons // ] - | @Hbits ] - | cases (merge_char_cases c0 c1) #Hmerge >Hmerge // ] - | cases (true_or_false (c0 == null)) #Hc0' - [ cases Hlsrs -Hlsrs - [ * - [ >(\P Hc0') * #Hfalse @False_ind /2/ - | #Hlsnil % %2 // ] - | #Hrsnil %2 // ] - | % % @merge_char_not_null @(\Pf Hc0') ] ] - |4:>Htc @(eq_f3 … (midtape ?)) - [ @eq_f @eq_f >associative_append >associative_append % - | % - | % ] +| (* by Htape bit_or_null c0 = true, moreover Hcurconfig2 *) @daemon +| (*Hcurconfig1*) @daemon ] +#Htb * #tc * whd in ⊢ (%→?); #Htc +lapply (Htc (〈grid,false〉::ls) s0 s1 c0 c1 (〈mv,false〉::table2@〈grid,false〉::rs) newconfig (〈comma,false〉::reverse ? table1) curconfig Htb ????????) -Htc +[9:|*:(* bit_or_null c0,c1; |curconfig| = |newconfig|*) @daemon ] +#Htc * #td * whd in ⊢ (%→?); * #_ #Htd lapply (Htd … Htc) -Htd whd in ⊢(???(??%%%)→?);#Htd +whd in ⊢ (%→?); #Houtc whd in Htd:(???%); whd in Htd:(???(??%%%)); +lapply (Houtc rs n + (〈comma,false〉::〈c1,false〉::reverse ? newconfig@〈s1,false〉::〈comma,false〉::reverse ? table1) + mv table2 (merge_char c0 c1) (reverse ? newconfig@[〈s1,false〉]) ls ????????) +[3: cases Htape -Htape * * #Hnomarks #Hbits #Hc0 #Hlsrs % [ % [ % + [ #x #Hx cases (orb_true_l … Hx) #Hx' + [ >(\P Hx') % + | @Hnomarks @memb_cons // ] + | @Hbits ] + | cases (merge_char_cases c0 c1) #Hmerge >Hmerge // ] + | cases (true_or_false (c0 == null)) #Hc0' + [ cases Hlsrs -Hlsrs + [ * + [ >(\P Hc0') * #Hfalse @False_ind /2/ + | #Hlsnil % %2 // ] + | #Hrsnil %2 // ] + | % % @merge_char_not_null @(\Pf Hc0') ] ] +|4:>Htd @(eq_f3 … (midtape ?)) + [ @eq_f @eq_f >associative_append >associative_append % | % - || >reverse_cons >reverse_cons >reverse_append >reverse_reverse - >reverse_cons >reverse_cons >reverse_reverse - >associative_append >associative_append >associative_append - >associative_append >associative_append - @Htable - | (* well formedness of table *) @daemon - | (* Hnewconfig *) @daemon - | (* bit_or_null mv = true (well formedness of table) *) @daemon - | -Houtc * #ls1 * #rs1 * #newc * #Hnewtapelegal * #Houtc * - [ * - [ * #Hmv #Htapemove - @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) - % - [ % - [ >Houtc -Houtc >reverse_append - >reverse_reverse >reverse_single @eq_f - >reverse_cons >reverse_cons >reverse_append >reverse_cons - >reverse_cons >reverse_reverse >reverse_reverse - >associative_append >associative_append - >associative_append >associative_append - >associative_append >associative_append % - | >Hmv >Ht1' >Htapemove - (* mv = bit false -→ c1 = bit ? *) - cut (∃c1'.c1 = bit c1') [ @daemon ] * #c1' #Hc1 - >Hc1 >tape_move_left_eq >(legal_tape_left … Htape) - >(legal_tape_right … Htape) % - ] - | // - ] - | * #Hmv #Htapemove - @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) % - [ % - [ >Houtc -Houtc >reverse_append - >reverse_reverse >reverse_single @eq_f - >reverse_cons >reverse_cons >reverse_append >reverse_cons - >reverse_cons >reverse_reverse >reverse_reverse - >associative_append >associative_append - >associative_append >associative_append - >associative_append >associative_append % - |>Hmv >Ht1' >Htapemove - cut (∃c1'.c1 = bit c1') [ @daemon ] * #c1' #Hc1 - >Hc1 >tape_move_right_eq >(legal_tape_left … Htape) - >(legal_tape_right … Htape) % - ] - | // + | % ] +| % +|| >reverse_cons >reverse_cons >reverse_append >reverse_reverse + >reverse_cons >reverse_cons >reverse_reverse + >associative_append >associative_append >associative_append + >associative_append >associative_append + @Htable +| (* well formedness of table *) @daemon +| (* Hnewconfig *) @daemon +| (* bit_or_null mv = true (well formedness of table) *) @daemon +| -Houtc * #ls1 * #rs1 * #newc * #Hnewtapelegal * #Houtc * + [ * + [ * #Hmv #Htapemove + @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) + % + [ % + [ >Houtc -Houtc >reverse_append + >reverse_reverse >reverse_single @eq_f + >reverse_cons >reverse_cons >reverse_append >reverse_cons + >reverse_cons >reverse_reverse >reverse_reverse + >associative_append >associative_append + >associative_append >associative_append + >associative_append >associative_append % + | >Hmv >Hta' >Htapemove + (* mv = bit false -→ c1 = bit ? *) + cut (∃c1'.c1 = bit c1') [ @daemon ] * #c1' #Hc1 + >Hc1 >tape_move_left_eq >(legal_tape_left … Htape) + >(legal_tape_right … Htape) % ] + | // ] - | * * * #Hmv #Hlseq #Hrseq #Hnewc + | * #Hmv #Htapemove @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) % [ % [ >Houtc -Houtc >reverse_append @@ -424,19 +450,36 @@ lapply (Hta (〈c0,false〉::curconfig) table1 s0 ls s1 >associative_append >associative_append >associative_append >associative_append >associative_append >associative_append % - |>Hmv >Ht1' cases c1 in Hnewc; - [ #c1' whd in ⊢ (??%?→?);#Hnewc Hlseq >Hrseq whd in ⊢ (??%%); - >(legal_tape_left … Htape) >(legal_tape_right … Htape) % - | whd in ⊢ (??%?→?); #Hnewc >Hnewc >Hlseq >Hrseq % - |*: whd in ⊢ (??%?→?);#Hnewc Hlseq >Hrseq whd in ⊢ (??%%); - >(legal_tape_left … Htape) >(legal_tape_right … Htape) % - ] + |>Hmv >Hta' >Htapemove + cut (∃c1'.c1 = bit c1') [ @daemon ] * #c1' #Hc1 + >Hc1 >tape_move_right_eq >(legal_tape_left … Htape) + >(legal_tape_right … Htape) % ] | // ] ] + | * * * #Hmv #Hlseq #Hrseq #Hnewc + @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) % + [ % + [ >Houtc -Houtc >reverse_append + >reverse_reverse >reverse_single @eq_f + >reverse_cons >reverse_cons >reverse_append >reverse_cons + >reverse_cons >reverse_reverse >reverse_reverse + >associative_append >associative_append + >associative_append >associative_append + >associative_append >associative_append % + |>Hmv >Hta' cases c1 in Hnewc; + [ #c1' whd in ⊢ (??%?→?);#Hnewc Hlseq >Hrseq whd in ⊢ (??%%); + >(legal_tape_left … Htape) >(legal_tape_right … Htape) % + | whd in ⊢ (??%?→?); #Hnewc >Hnewc >Hlseq >Hrseq % + |*: whd in ⊢ (??%?→?);#Hnewc Hlseq >Hrseq whd in ⊢ (??%%); + >(legal_tape_left … Htape) >(legal_tape_right … Htape) % + ] + ] + | // + ] ] ] qed. @@ -447,7 +490,7 @@ if is_false(current) (* current state is not final *) match_tuple; if is_marked(current) = false (* match ok *) then - exec_move + exec_action move_r; else sink; else nop; @@ -455,14 +498,12 @@ if is_false(current) (* current state is not final *) definition uni_step ≝ ifTM ? (test_char STape (λc.\fst c == bit false)) - (single_finalTM ? (seq ? init_match - (seq ? match_tuple + (single_finalTM ? + (init_match · match_tuple · (ifTM ? (test_char ? (λc.¬is_marked ? c)) - (seq ? exec_move (move_r …)) - (nop ?) (* sink *) - tc_true)))) - (nop ?) - tc_true. + (exec_action · move_r …) + (nop ?) tc_true))) + (nop ?) tc_true. definition R_uni_step_true ≝ λt1,t2. ∀n,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv. @@ -483,16 +524,171 @@ definition R_uni_step_true ≝ λt1,t2. definition R_uni_step_false ≝ λt1,t2. ∀b. current STape t1 = Some ? 〈bit b,false〉 → b = true ∧ t2 = t1. -axiom sem_match_tuple : Realize ? match_tuple R_match_tuple. +(*axiom sem_match_tuple : Realize ? match_tuple R_match_tuple.*) +definition us_acc : states ? uni_step ≝ (inr … (inl … (inr … start_nop))). + +definition Pre_uni_step ≝ λt1. + ∃n,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv. + 0 < |table| ∧ table_TM (S n) table ∧ + match_in_table (S n) (〈s0,false〉::curconfig) 〈c0,false〉 + (〈s1,false〉::newconfig) 〈c1,false〉 〈mv,false〉 table ∧ + legal_tape ls 〈c0,false〉 rs ∧ + t1 = midtape STape (〈grid,false〉::ls) 〈s0,false〉 + (curconfig@〈c0,false〉::〈grid,false〉::table@〈grid,false〉::rs). + lemma sem_uni_step : - accRealize ? uni_step (inr … (inl … (inr … start_nop))) + accGRealize ? uni_step us_acc Pre_uni_step R_uni_step_true R_uni_step_false. +@daemon (* this no longer works: TODO *) (* +@(acc_sem_if_app_guarded STape … (sem_test_char ? (λc:STape.\fst c == bit false)) + ? (test_char_inv …) (sem_nop …) …) +[| @(sem_seq_app_guarded … (Realize_to_GRealize … sem_init_match) ???) + [ 5: @sub_reflexive + | 3: @(sem_seq_app_guarded … sem_match_tuple + (Realize_to_GRealize … (sem_if ????????? (sem_test_char … (λc.¬is_marked FSUnialpha c)) + (sem_seq … sem_exec_action (sem_move_r …)) + (sem_nop …)))) + [@(λx.True) + |// + |@sub_reflexive] + ||| #t1 #t2 * #n * #table * #s0 * #s1 * #c0 * #c1 * #ls * #rs * #curconfig + * #newconfig * #mv * * * * + #Hlen1 #Htable #Hmatch #Hlegal #Ht1 + whd in ⊢ (%→?); + cut (∃tup,table0.table = tup@table0 ∧ tuple_TM (S n) tup) + [@daemon] + * #tup * #table0 * #Htableeq * #qin * #cin * #qout * #cout * #mv0 + * * * * * * * * * * + #Hqinnomarks #_ #Hqinbits #_ #_ #_ #_ #_ #Hqinlen #_ #Htupeq + cut (∃d,qin0.qin = 〈d,false〉::qin0) + [ lapply Hqinlen lapply Hqinnomarks -Hqinlen -Hqinnomarks cases qin + [ #_ normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) + | * #d #bd #qin0 #Hqinnomarks #_ %{d} %{qin0} + >(?:bd=false) [%] + @(Hqinnomarks 〈d,bd〉) @memb_hd ] ] + * #d * #qin0 #Hqineq + #Ht2 + lapply (Ht2 (〈grid,false〉::ls) (curconfig@[〈c0,false〉]) + (qin0@〈cin,false〉::〈comma,false〉::qout@〈cout,false〉::〈comma,false〉::〈mv0,false〉::table0@〈grid,false〉::rs) s0 d ???) + [ >Ht1 @eq_f >associative_append @eq_f @eq_f @eq_f + >Htableeq >Htupeq >associative_append whd in ⊢ (??%?); + @eq_f >Hqineq >associative_append @eq_f whd in ⊢ (??%?); + @eq_f whd in ⊢ (??%?); @eq_f + >associative_append % + | @daemon + | @daemon + ] + #Ht2 % [| % [| % [| % [ @Ht2 ] + %2 + (* ls0 = ls + c = s0 + l1 = curconfig@[〈c0,false〉] + l2 = [〈bar,false〉] + c10 = d + l3 = qin0@[〈cin,false〉] + l4 = qout@〈cout,false〉::〈comma,false〉::〈mv0,false〉::table0 + rs00 = rs + n0 = S n ? + *) + %{ls} %{s0} %{(curconfig@[〈c0,false〉])} + %{([〈bar,false〉])} %{d} %{(qin0@[〈cin,false〉])} + %{(qout@〈cout,false〉::〈comma,false〉::〈mv0,false〉::table0)} + %{rs} %{n} @daemon (* TODO *) + ] + ] + ] + ] + | #intape #outtape + #ta whd in ⊢ (%→?); #Hta #HR + #n #fulltable #s0 #s1 #c0 #c1 #ls #rs #curconfig #newconfig #mv + #Htable_len cut (∃t0,table. fulltable =〈bar,false〉::〈t0,false〉::table) [(* 0 < |table| *) @daemon] + * #t0 * #table #Hfulltable >Hfulltable -fulltable + #Htable #Hmatch #Htape #Hintape #t1' #Ht1' + >Hintape in Hta; * * * #c #bc * + whd in ⊢ (??%?→?); #HSome destruct (HSome) #Hc #Hta % [@(\P Hc)] + cases HR -HR + #tb * whd in ⊢ (%→?); #Htb + lapply (Htb (〈grid,false〉::ls) (curconfig@[〈c0,false〉]) (table@〈grid,false〉::rs) c t0 ???) + [ >Hta >associative_append % + | @daemon + | @daemon + | -Hta -Htb #Htb * + #tc * whd in ⊢ (%→?); #Htc cases (Htc … Htable … Htb) -Htb -Htc + [| * #Hcurrent #Hfalse @False_ind + (* absurd by Hmatch *) @daemon + | >(\P Hc) % + | (* Htable (con lemma) *) @daemon + | (* Hmatch *) @daemon + | (* Htable *) @daemon + | (* Htable, Hmatch → |config| = n + necessaria modifica in R_match_tuple, le dimensioni non corrispondono + *) @daemon + ] + * #table1 * #newc * #mv1 * #table2 * #Htableeq #Htc * + [ * #td * whd in ⊢ (%→?); >Htc -Htc * * #c2 * whd in ⊢ (??%?→?); #Hc2 destruct (Hc2) + #_ #Htd + cut (newc = 〈s1,false〉::newconfig@[〈c1,false〉]) [@daemon] #Hnewc + >Hnewc cut (mv1 = 〈mv,false〉) + [@daemon] #Hmv1 + * #te * whd in ⊢ (%→?); #Hte + cut (td = midtape STape (〈c0,false〉::reverse STape curconfig@〈c,false〉::〈grid,false〉::ls) + 〈grid,false〉 + ((table1@〈bar,false〉::〈c,false〉::curconfig@[〈c0,false〉])@〈comma,true〉::〈s1,false〉:: + newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs)) + [ >Htd @eq_f3 // + [ >reverse_append >reverse_single % + | >associative_append >associative_append normalize + >associative_append >Hmv1 >Hnewc @eq_f @eq_f @eq_f @eq_f @eq_f @eq_f + whd in ⊢ (??%?); >associative_append % + ] + ] + -Htd #Htd lapply (Hte … (S n) … Htd … Ht1') -Htd -Hte + [ // + | (*|curconfig| = |newconfig|*) @daemon + | (* Htable → bit_or_null c1 = true *) @daemon + | (* only_bits (〈s1,false〉::newconfig) *) @daemon + | (* only_bits (curconfig@[〈s0,false〉]) *) @daemon + | (* no_marks (reverse ? curconfig) *) @daemon + | >Hmv1 in Htableeq; >Hnewc + >associative_append >associative_append normalize + >associative_append >associative_append + #Htableeq Houttape @eq_f @eq_f @eq_f @eq_f + change with ((〈bar,false〉::〈t0,false〉::table)@?) in ⊢ (???%); + >Htableeq >associative_append >associative_append + >associative_append normalize >associative_append + >associative_append normalize >Hnewc associative_append normalize >associative_append + >Hmv1 % + | @Hliftte + ] + | // + ] + ] + ] + | * #td * whd in ⊢ (%→%→?); >Htc * #Htd + lapply (Htd ? (refl ??)) normalize in ⊢ (%→?); + #Hfalse destruct (Hfalse) + ] + ] +| #t1 #t2 #t3 whd in ⊢ (%→%→?); #Ht1 #Ht2 + #b #Hb >Hb in Ht1; * #Hc #Ht1 lapply (Hc ? (refl ??)) -Hc #Hb' % + // cases b in Hb'; normalize #H1 // +] +*) +qed. + +(* @(acc_sem_if_app STape … (sem_test_char ? (λc:STape.\fst c == bit false)) (sem_seq … sem_init_match (sem_seq … sem_match_tuple (sem_if … (* ????????? (sem_test_char … (λc.¬is_marked FSUnialpha c)) *) - (sem_seq … sem_exec_move (sem_move_r …)) + (sem_seq … sem_exec_action (sem_move_r …)) (sem_nop …)))) (sem_nop …) …) @@ -500,14 +696,14 @@ lemma sem_uni_step : [ #intape #outtape #ta whd in ⊢ (%→?); #Hta #HR #n #fulltable #s0 #s1 #c0 #c1 #ls #rs #curconfig #newconfig #mv - #Htable_len cut (∃t0,table. fulltable =〈t0,false〉::table) [(* 0 < |table| *) @daemon] + #Htable_len cut (∃t0,table. fulltable =〈bar,false〉::〈t0,false〉::table) [(* 0 < |table| *) @daemon] * #t0 * #table #Hfulltable >Hfulltable -fulltable #Htable #Hmatch #Htape #Hintape #t1' #Ht1' - >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta - #Hs0 lapply (\P Hs0) -Hs0 #Hs0 #Hta % // + >Hintape in Hta; * * * #c #bc * + whd in ⊢ (??%?→?); #HSome destruct (HSome) #Hc #Hta % [@(\P Hc)] cases HR -HR #tb * whd in ⊢ (%→?); #Htb - lapply (Htb (〈grid,false〉::ls) (curconfig@[〈c0,false〉]) (table@〈grid,false〉::rs) s0 t0 ???) + lapply (Htb (〈grid,false〉::ls) (curconfig@[〈c0,false〉]) (table@〈grid,false〉::rs) c t0 ???) [ >Hta >associative_append % | @daemon | @daemon @@ -515,28 +711,30 @@ lemma sem_uni_step : #tc * whd in ⊢ (%→?); #Htc cases (Htc … Htable … Htb) -Htb -Htc [| * #Hcurrent #Hfalse @False_ind (* absurd by Hmatch *) @daemon - | >Hs0 % - | (* da decidere se aggiungere un'assunzione o utilizzare Hmatch *) @daemon + | >(\P Hc) % + | (* Htable (con lemma) *) @daemon + | (* Hmatch *) @daemon | (* Htable *) @daemon | (* Htable, Hmatch → |config| = n necessaria modifica in R_match_tuple, le dimensioni non corrispondono - *) @daemon ] + *) @daemon + ] * #table1 * #newc * #mv1 * #table2 * #Htableeq #Htc * - [ * #td * whd in ⊢ (%→?); >Htc -Htc #Htd - cases (Htd ? (refl ??)) #_ -Htd + [ * #td * whd in ⊢ (%→?); >Htc -Htc * * #c2 * whd in ⊢ (??%?→?); #Hc2 destruct (Hc2) + #_ #Htd cut (newc = 〈s1,false〉::newconfig@[〈c1,false〉]) [@daemon] #Hnewc - >Hnewc #Htd - cut (∃mv2. mv1 = [〈mv2,false〉]) - [@daemon] * #mv2 #Hmv1 + >Hnewc cut (mv1 = 〈mv,false〉) + [@daemon] #Hmv1 * #te * whd in ⊢ (%→?); #Hte - cut (td = midtape STape (〈c0,false〉::reverse STape curconfig@〈s0,false〉::〈grid,false〉::ls) + cut (td = midtape STape (〈c0,false〉::reverse STape curconfig@〈c,false〉::〈grid,false〉::ls) 〈grid,false〉 - ((table1@〈s0,false〉::curconfig@[〈c0,false〉])@〈comma,true〉::〈s1,false〉:: - newconfig@〈c1,false〉::〈comma,false〉::〈mv2,false〉::table2@〈grid,false〉::rs)) + ((table1@〈bar,false〉::〈c,false〉::curconfig@[〈c0,false〉])@〈comma,true〉::〈s1,false〉:: + newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs)) [ >Htd @eq_f3 // [ >reverse_append >reverse_single % | >associative_append >associative_append normalize - >associative_append >associative_append >Hmv1 % + >associative_append >Hmv1 >Hnewc @eq_f @eq_f @eq_f @eq_f @eq_f @eq_f + whd in ⊢ (??%?); >associative_append % ] ] -Htd #Htd lapply (Hte … (S n) … Htd … Ht1') -Htd -Hte @@ -551,31 +749,30 @@ lemma sem_uni_step : >associative_append >associative_append #Htableeq Houttape @eq_f @eq_f @eq_f @eq_f - change with ((〈t0,false〉::table)@?) in ⊢ (???%); + change with ((〈bar,false〉::〈t0,false〉::table)@?) in ⊢ (???%); >Htableeq >associative_append >associative_append >associative_append normalize >associative_append >associative_append normalize >Hnewc associative_append normalize >associative_append >Hmv1 % - | >(?: mv = mv2) [| (*Hmatch, Htableeq*) @daemon ] - @Hliftte + | @Hliftte ] | // ] ] ] - | * #td * whd in ⊢ (%→%→?); >Htc #Htd - cases (Htd ? (refl ??)) normalize in ⊢ (%→?); + | * #td * whd in ⊢ (%→%→?); >Htc * #Htd + lapply (Htd ? (refl ??)) normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ] ] | #t1 #t2 #t3 whd in ⊢ (%→%→?); #Ht1 #Ht2 - #b #Hb cases (Ht1 ? Hb) #Hb' #Ht3 >Ht2 % // - cases b in Hb'; normalize #H1 // + #b #Hb >Hb in Ht1; * #Hc #Ht1 lapply (Hc ? (refl ??)) -Hc #Hb' % + // cases b in Hb'; normalize #H1 // ] qed. - +*) \ No newline at end of file