X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Funi_step.ma;h=eabab3e838c66dbac33a0da3b8e42eae2f708d5b;hb=df4cfc76ab059f6b3d5daf324712ad27ec281088;hp=0cc8f71c49140c35a2d2ef564c3302f34c3a9057;hpb=f0d422b660e11886ec4f9a823da795050f07e07f;p=helm.git diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma index 0cc8f71c4..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,12 +248,23 @@ 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〉]) → only_bits (〈s1,false〉::newconfig) → + no_marks curconfig → only_bits (curconfig@[〈s0,false〉]) → + only_bits (〈s1,false〉::newconfig) → bit_or_null c1 = true → |curconfig| = |newconfig| → - no_nulls ls → no_nulls rs → no_marks ls → no_marks rs → 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) → @@ -298,100 +306,154 @@ lemma merge_char_not_null : ] 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 #Hlen #Hls #Hrs #Hls1 #Hrs1 #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 merge_char_null : ∀c.merge_char null c = c. +* // +qed. + +lemma merge_char_cases : ∀c1,c2.merge_char c1 c2 = c1 ∨ merge_char c1 c2 = c2. +#c1 * +[ #c1' %2 % +| % % +| *: %2 % ] +qed. + +(* lemma merge_char_c_bit : + ∀c1,c2.is_bit c2 = true → merge_char c1 c2 = c2. +#c1 * +[ #c2' #_ % +|*: normalize #Hfalse destruct (Hfalse) ] +qed. + +lemma merge_char_c_bit : + ∀c1,c2.is_null c2 = true → merge_char c1 c2 = c1. +#c1 * +[ #c2' #_ % +|*: normalize #Hfalse destruct (Hfalse) ] +qed. + +*) + +(*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 ????? - Hls Hrs Hls1 Hrs1 ???) - [3: cases (true_or_false (c0 == null)) #Hc0 - [ >(\P Hc0) in Htape; #Htape cases (legal_tape_cases … Htape) - [ * #Hfalse @False_ind /2/ - | * #_ * - [ #Hlsnil @legal_tape_conditions % %2 // - | #Hrsnil @legal_tape_conditions %2 // - ] - ] - | @legal_tape_conditions % % @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 - | (* Hnewconfig *) @daemon - | (* bit_or_null mv = true *) @daemon - | (* bit_or_null c1,c2 → bit_or_null (merge_char c1 c2) *) @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 cases (legal_tape_cases … Htape) - [ #Hc0 >lift_tape_not_null /2/ - | * #Hc0 * - [ #Hls >Hc0 >Hls whd in ⊢ (??%%); cases rs; - [%| #r0 #rs0 %] - | #Hrs >Hc0 >Hrs cases ls; [%| #l0 #ls0 %] - ] - ] - ] - | // + | % ] +| % +|| >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 #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 cases (legal_tape_cases … Htape) - [ #Hc0 >lift_tape_not_null /2/ - | * #Hc0 * - [ #Hls >Hc0 >Hls whd in ⊢ (??%%); cases rs; - [%| #r0 #rs0 %] - | #Hrs >Hc0 >Hrs cases ls; [%| #l0 #ls0 %] - ] - ] + | // + ] + | * #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 + cut (∃c1'.c1 = bit c1') [ @daemon ] * #c1' #Hc1 + >Hc1 >tape_move_right_eq >(legal_tape_left … Htape) + >(legal_tape_right … Htape) % ] | // ] @@ -406,14 +468,15 @@ 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; + |>Hmv >Hta' cases c1 in Hnewc; [ #c1' whd in ⊢ (??%?→?);#Hnewc Hlseq >Hrseq cases Htape * #Hleft #Hright #_ - whd in ⊢ (??%%); >Hleft >Hright % + >Hlseq >Hrseq whd in ⊢ (??%%); + >(legal_tape_left … Htape) >(legal_tape_right … Htape) % | whd in ⊢ (??%?→?); #Hnewc >Hnewc >Hlseq >Hrseq % |*: whd in ⊢ (??%?→?);#Hnewc Hlseq >Hrseq cases Htape * #Hleft #Hright #_ - whd in ⊢ (??%%); >Hleft >Hright % ] + >Hlseq >Hrseq whd in ⊢ (??%%); + >(legal_tape_left … Htape) >(legal_tape_right … Htape) % + ] ] | // ] @@ -421,19 +484,295 @@ lapply (Hta (〈c0,false〉::curconfig) table1 s0 ls s1 ] qed. -definition R_uni_step ≝ λt1,t2. - ∀n,table,c,c1,ls,rs,curs,curc,news,newc,mv. - table_TM n table → - match_in_table (〈c,false〉::curs@[〈curc,false〉]) - (〈c1,false〉::news@[〈newc,false〉]) mv table → - t1 = midtape STape (〈grid,false〉::ls) 〈c,false〉 - (curs@〈curc,false〉::〈grid,false〉::table@〈grid,false〉::rs) → - ∀t1',ls1,rs1.t1' = lift_tape ls 〈curc,false〉 rs → - (t2 = midtape STape (〈grid,false〉::ls1) 〈c1,false〉 - (news@〈newc,false〉::〈grid,false〉::table@〈grid,false〉::rs1) ∧ - lift_tape ls1 〈newc,false〉 rs1 = - tape_move STape t1' (Some ? 〈〈newc,false〉,move_of_unialpha mv〉)). - -definition no_nulls ≝ - λl:list STape.∀x.memb ? x l = true → is_null (\fst x) = false. - +(* +if is_false(current) (* current state is not final *) + then init_match; + match_tuple; + if is_marked(current) = false (* match ok *) + then + exec_action + move_r; + else sink; + else nop; +*) + +definition uni_step ≝ + ifTM ? (test_char STape (λc.\fst c == bit false)) + (single_finalTM ? + (init_match · match_tuple · + (ifTM ? (test_char ? (λc.¬is_marked ? c)) + (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. + 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) → + ∀t1'.t1' = lift_tape ls 〈c0,false〉 rs → + s0 = bit false ∧ + ∃ls1,rs1,c2. + (t2 = midtape STape (〈grid,false〉::ls1) 〈s1,false〉 + (newconfig@〈c2,false〉::〈grid,false〉::table@〈grid,false〉::rs1) ∧ + lift_tape ls1 〈c2,false〉 rs1 = + tape_move STape t1' (map_move c1 mv) ∧ legal_tape ls1 〈c2,false〉 rs1). + +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.*) + +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 : + 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_action (sem_move_r …)) + (sem_nop …)))) + (sem_nop …) + …) +[@sem_test_char||] +[ #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. +*) \ No newline at end of file