X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Ftuples.ma;h=7967331b5d1fb0b23e86417eeb1d67e04f660350;hb=690675dde36407d039e9d05047bc7909202170c1;hp=83e7337a08036ecaeff07c3c3111d11141bb80ff;hpb=89e319c06a4f27b26095cacce9784ae1584abf6d;p=helm.git diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma index 83e7337a0..7967331b5 100644 --- a/matita/matita/lib/turing/universal/tuples.ma +++ b/matita/matita/lib/turing/universal/tuples.ma @@ -20,6 +20,9 @@ definition STape ≝ FinProd … FSUnialpha FinBool. definition only_bits ≝ λl. ∀c.memb STape c l = true → is_bit (\fst c) = true. + +definition only_bits_or_nulls ≝ λl. + ∀c.memb STape c l = true → bit_or_null (\fst c) = true. definition no_grids ≝ λl. ∀c.memb STape c l = true → is_grid (\fst c) = false. @@ -34,21 +37,78 @@ lemma bit_not_grid: ∀d. is_bit d = true → is_grid d = false. * // normalize #H destruct qed. +lemma bit_or_null_not_grid: ∀d. bit_or_null d = true → is_grid d = false. +* // normalize #H destruct +qed. + lemma bit_not_bar: ∀d. is_bit d = true → is_bar d = false. * // normalize #H destruct qed. +lemma bit_or_null_not_bar: ∀d. bit_or_null d = true → is_bar d = false. +* // normalize #H destruct +qed. + +definition mk_tuple ≝ λqin,cin,qout,cout,mv. + qin @ cin :: 〈comma,false〉:: qout @ cout :: 〈comma,false〉 :: [mv]. + (* by definition, a tuple is not marked *) definition tuple_TM : nat → list STape → Prop ≝ - λn,t.∃qin,qout,mv. - no_marks t ∧ - only_bits qin ∧ only_bits qout ∧ only_bits mv ∧ - |qin| = n ∧ |qout| = n (* ∧ |mv| = ? *) ∧ - t = qin@〈comma,false〉::qout@〈comma,false〉::mv. + λn,t.∃qin,cin,qout,cout,mv. + no_marks qin ∧ no_marks qout ∧ + only_bits qin ∧ only_bits qout ∧ + bit_or_null cin = true ∧ bit_or_null cout = true ∧ bit_or_null mv = true ∧ + (cout = null → mv = null) ∧ + |qin| = n ∧ |qout| = n ∧ + t = mk_tuple qin 〈cin,false〉 qout 〈cout,false〉 〈mv,false〉. -inductive table_TM : nat → list STape → Prop ≝ -| ttm_nil : ∀n.table_TM n [] -| ttm_cons : ∀n,t1,T.tuple_TM n t1 → table_TM n T → table_TM n (t1@〈bar,false〉::T). +inductive table_TM (n:nat) : list STape → Prop ≝ +| ttm_nil : table_TM n [] +| ttm_cons : ∀t1,T.tuple_TM n t1 → table_TM n T → table_TM n (t1@〈bar,false〉::T). + +inductive match_in_table (qin:list STape) (cin: STape) + (qout:list STape) (cout:STape) (mv:STape) +: list STape → Prop ≝ +| mit_hd : + ∀tb. + match_in_table qin cin qout cout mv + (mk_tuple qin cin qout cout mv @〈bar,false〉::tb) +| mit_tl : + ∀qin0,cin0,qout0,cout0,mv0,tb. + match_in_table qin cin qout cout mv tb → + match_in_table qin cin qout cout mv + (mk_tuple qin0 cin0 qout0 cout0 mv0@〈bar,false〉::tb). + +axiom append_l1_injective : + ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l1 = l2. +axiom append_l2_injective : + ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l3 = l4. + + +lemma generic_match_to_match_in_table : + ∀n,T.table_TM n T → + ∀qin,cin,qout,cout,mv.|qin| = n → |qout| = n → + ∀t1,t2. + T = t1@qin@cin::〈comma,false〉::qout@cout::〈comma,false〉::mv::t2 → + match_in_table qin cin qout cout mv T. +#n #T #Htable #qin #cin #qout #cout #mv #Hlenqin #Hlenqout +elim Htable +[ #t1 #t2 Htuple normalize in ⊢ (??%%→?); + >associative_append #HT + cut (qin0 = qin ∧ (〈cin0,false〉 = cin ∧ (qout0 = qout ∧ + (〈cout0,false〉 = cout ∧ (〈mv0,false〉 = mv ∧ 〈bar,false〉::T0 = t2))))) + [ lapply (append_l1_injective … HT) [ >Hlenqin @Hlenqin0 ] + #Hqin % [ @Hqin ] -Hqin + lapply (append_l2_injective … HT) [ >Hlenqin @Hlenqin0 ] -HT #HT + destruct (HT) + lemma no_grids_in_table: ∀n.∀l.table_TM n l → no_grids l. #n #l #t elim t @@ -58,14 +118,14 @@ lemma no_grids_in_table: ∀n.∀l.table_TM n l → no_grids l. whd >Heq #x #membx cases (memb_append … membx) -membx #membx [cases (memb_append … membx) -membx #membx - [@bit_not_grid @Hqin // + [@bit_or_null_not_grid @Hqin // |cases (orb_true_l … membx) -membx #membx [>(\P membx) // |cases (memb_append … membx) -membx #membx - [@bit_not_grid @Hqout // + [@bit_or_null_not_grid @Hqout // |cases (orb_true_l … membx) -membx #membx [>(\P membx) // - |@bit_not_grid @Hmv // + |@bit_or_null_not_grid >(memb_single … membx) @Hmv ] ] ] @@ -216,6 +276,109 @@ lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid) ]]]] qed. +definition init_current_on_match ≝ + (seq ? (move_l ?) + (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c))) + (seq ? (move_r ?) (mark ?)))). + +definition R_init_current_on_match ≝ λt1,t2. + ∀l1,l2,c,rs. no_grids l1 → is_grid c = false → + t1 = midtape STape (l1@〈c,false〉::〈grid,false〉::l2) 〈grid,false〉 rs → + t2 = midtape STape (〈grid,false〉::l2) 〈c,true〉 ((reverse ? l1)@〈grid,false〉::rs). + +lemma sem_init_current_on_match : + Realize ? init_current_on_match R_init_current_on_match. +#intape +cases (sem_seq ????? (sem_move_l ?) + (sem_seq ????? (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c))) + (sem_seq ????? (sem_move_r ?) (sem_mark ?))) intape) +#k * #outc * #Hloop #HR +@(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop +#l1 #l2 #c #rs #Hl1 #Hc #Hintape +cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta -Hintape +generalize in match Hl1; cases l1 + [#Hl1 whd in ⊢ ((???(??%%%))→?); #Hta + * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Hta + [* >Hc #Htemp destruct (Htemp) ] + * #_ #Htc lapply (Htc [ ] 〈grid,false〉 ? (refl ??) (refl …) Hl1) + whd in ⊢ ((???(??%%%))→?); -Htc #Htc + * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htc -Htd + whd in ⊢ ((???(??%%%))→?); #Htd + whd in ⊢ (%→?); #Houtc lapply (Houtc … Htd) -Houtc #Houtc + >Houtc % + |#d #tl #Htl whd in ⊢ ((???(??%%%))→?); #Hta + * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Htb + [* >(Htl … (memb_hd …)) #Htemp destruct (Htemp)] + * #Hd >append_cons #Htb lapply (Htb … (refl ??) (refl …) ?) + [#x #membx cases (memb_append … membx) -membx #membx + [@Htl @memb_cons @membx | >(memb_single … membx) @Hc]]-Htb #Htb + * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htb -Htc + >reverse_append >associative_append whd in ⊢ ((???(??%%%))→?); #Htc + whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc) -Houtc #Houtc + >Houtc >reverse_cons >associative_append % + ] +qed. + +(* +definition init_current_gen ≝ + seq ? (adv_to_mark_l ? (is_marked ?)) + (seq ? (clear_mark ?) + (seq ? (move_l ?) + (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c))) + (seq ? (move_r ?) (mark ?))))). + +definition R_init_current_gen ≝ λt1,t2. + ∀l1,c,l2,b,l3,c1,rs,c0,b0. no_marks l1 → no_grids l2 → + Some ? 〈c0,b0〉 = option_hd ? (reverse ? (〈c,true〉::l2)) → + t1 = midtape STape (l1@〈c,true〉::l2@〈grid,b〉::l3) 〈c1,false〉 rs → + t2 = midtape STape (〈grid,b〉::l3) 〈c0,true〉 + ((tail ? (reverse ? (l1@〈c,false〉::l2))@〈c1,false〉::rs)). + +lemma sem_init_current_gen : Realize ? init_current_gen R_init_current_gen. +#intape +cases (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?)) + (sem_seq ????? (sem_clear_mark ?) + (sem_seq ????? (sem_move_l ?) + (sem_seq ????? (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c))) + (sem_seq ????? (sem_move_r ?) (sem_mark ?))))) intape) +#k * #outc * #Hloop #HR +@(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop +#l1 #c #l2 #b #l3 #c1 #rs #c0 #b0 #Hl1 #Hl2 #Hc #Hintape +cases HR -HR #ta * whd in ⊢ (%→?); #Hta cases (Hta … Hintape) -Hta -Hintape + [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ] +* #_ #Hta lapply (Hta l1 〈c,true〉 ? (refl ??) ??) [@Hl1|%] -Hta #Hta +* #tb * whd in ⊢ (%→?); #Htb lapply (Htb … Hta) -Htb -Hta #Htb +* #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc -Htb +generalize in match Hc; generalize in match Hl2; cases l2 + [#_ whd in ⊢ ((???%)→?); #Htemp destruct (Htemp) + whd in ⊢ ((???(??%%%))→?); #Htc + * #td * whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd + [2: * whd in ⊢ (??%?→?); #Htemp destruct (Htemp) ] + * #_ #Htd >Htd in Htc; -Htd #Htd + * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Htd + >reverse_append >reverse_cons + whd in ⊢ ((???(??%%%))→?); #Hte + whd in ⊢ (%→?); #Houtc lapply (Houtc … Hte) -Houtc -Hte #Houtc + >Houtc % + |#d #tl #Htl #Hc0 whd in ⊢ ((???(??%%%))→?); #Htc + * #td * whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd + [* >(Htl … (memb_hd …)) whd in ⊢ (??%?→?); #Htemp destruct (Htemp)] + * #Hd #Htd lapply (Htd … (refl ??) (refl ??) ?) + [#x #membx @Htl @memb_cons @membx] -Htd #Htd + * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Htd + >reverse_append >reverse_cons >reverse_cons + >reverse_cons in Hc0; >reverse_cons cases (reverse ? tl) + [normalize in ⊢ (%→?); #Hc0 destruct (Hc0) #Hte + whd in ⊢ (%→?); #Houtc lapply (Houtc … Hte) -Houtc -Hte #Houtc + >Houtc % + |* #c2 #b2 #tl2 normalize in ⊢ (%→?); #Hc0 destruct (Hc0) + whd in ⊢ ((???(??%%%))→?); #Hte + whd in ⊢ (%→?); #Houtc lapply (Houtc … Hte) -Houtc -Hte #Houtc + >Houtc >associative_append >associative_append >associative_append % + ] + ] +qed. +*) definition init_current ≝ seq ? (adv_to_mark_l ? (is_marked ?)) (seq ? (clear_mark ?) @@ -271,8 +434,8 @@ definition match_tuple_step ≝ definition R_match_tuple_step_true ≝ λt1,t2. ∀ls,c,l1,l2,c1,l3,l4,rs,n. - is_bit c = true → only_bits l1 → no_marks l1 (* → no_grids l2 *) → is_bit c1 = true → - only_bits l3 → n = |l1| → |l1| = |l3| → + bit_or_null c = true → only_bits_or_nulls l1 → no_marks l1 (* → no_grids l2 *) → bit_or_null c1 = true → + only_bits_or_nulls l3 → n = |l1| → |l1| = |l3| → table_TM (S n) (l2@〈bar,false〉::〈c1,false〉::l3@〈comma,false〉::l4) → t1 = midtape STape (〈grid,false〉::ls) 〈c,true〉 (l1@〈grid,false〉::l2@〈bar,false〉::〈c1,true〉::l3@〈comma,false〉::l4@〈grid,false〉::rs) → @@ -311,6 +474,12 @@ lemma some_option_hd: ∀A.∀l:list A.∀a.∃b. #A #l #a cases l normalize /2/ qed. +axiom tech_split2 : ∀A,l1,l2,l3,l4,x. + memb A x l1 = false → memb ? x l3 = false → + l1@x::l2 = l3@x::l4 → l1 = l3 ∧ l2 = l4. + +axiom injective_append : ∀A,l.injective … (λx.append A x l). + lemma sem_match_tuple_step: accRealize ? match_tuple_step (inr … (inl … (inr … 0))) R_match_tuple_step_true R_match_tuple_step_false. @@ -349,7 +518,7 @@ lemma sem_match_tuple_step: |#x #tl @not_to_not normalize #H destruct // ] ] #Hnoteq %2 - cut (is_bit d' = true) + cut (bit_or_null d' = true) [cases la in H3; [normalize in ⊢ (%→?); #H destruct // |#x #tl #H @(Hl3 〈d',false〉) @@ -358,7 +527,7 @@ lemma sem_match_tuple_step: ] #Hd' >Htapec in Hor; -Htapec * [* #taped * whd in ⊢ (%→?); #H @False_ind - cases (H … (refl …)) >(bit_not_grid ? Hd') #Htemp destruct (Htemp) + cases (H … (refl …)) >(bit_or_null_not_grid ? Hd') #Htemp destruct (Htemp) |* #taped * whd in ⊢ (%→?); #H cases (H … (refl …)) -H #_ #Htaped * #tapee * whd in ⊢ (%→?); #Htapee <(associative_append ? lc (〈comma,false〉::l4)) in Htaped; #Htaped @@ -374,9 +543,16 @@ lemma sem_match_tuple_step: @last_of_table |(* rs4 not empty *) * #d2 #b2 #rs3' * #d * #b * * * #Heq1 #Hnobars + cut (memb STape 〈d2,b2〉 (l2@〈bar,false〉::〈c1,false〉::l3@〈comma,false〉::l4) = true) + [@memb_append_l2 @memb_cons + cut (∀A,l1,l2.∀a:A. a::l1@l2=(a::l1)@l2) [//] #Hcut + >Hcut >H3 >associative_append @memb_append_l2 + @memb_cons >Heq1 @memb_append_l2 @memb_cons @memb_hd] #d2intable cut (is_grid d2 = false) - [@(no_grids_in_table … Htable … 〈d2,b2〉) - @daemon (* no grids in table *)] #Hd2 + [@(no_grids_in_table … Htable … 〈d2,b2〉 d2intable)] #Hd2 + cut (b2 = false) + [@(no_marks_in_table … Htable … 〈d2,b2〉 d2intable)] #Hb2 + >Hb2 in Heq1; #Heq1 -Hb2 -b2 whd in ⊢ ((???%)→?); #Htemp destruct (Htemp) #Htapee >Htapee -Htapee * [(* we know current is not grid *) * #tapef * whd in ⊢ (%→?); #Htapef @@ -392,9 +568,6 @@ lemma sem_match_tuple_step: whd in ⊢ (%→?); #Htapeout %1 cases (some_option_hd ? (reverse ? (reverse ? la)) 〈c',true〉) * #c00 #b00 #Hoption - (* cut - ((reverse ? rs3 @〈d',false〉::reverse ? la@reverse ? (l2@[〈bar,false〉])@(〈grid,false〉::reverse ? lb)) - = *) lapply (Htapeout (reverse ? rs3 @〈d',false〉::reverse ? la@reverse ? (l2@[〈bar,false〉])@(〈grid,false〉::reverse ? lb)) c' (reverse ? la) false ls bar (〈d2,true〉::rs3'@〈grid,false〉::rs) c00 b00 ?????) -Htapeout @@ -407,12 +580,12 @@ lemma sem_match_tuple_step: [normalize in ⊢ (%→?); #Htemp destruct (Htemp) @injective_notb @notgridc |#x #tl normalize in ⊢ (%→?); #Htemp destruct (Htemp) - @bit_not_grid @(Hl1bars 〈c',false〉) @memb_append_l2 @memb_hd + @bit_or_null_not_grid @(Hl1bars 〈c',false〉) @memb_append_l2 @memb_hd ] - |cut (only_bits (la@(〈c',false〉::lb))) + |cut (only_bits_or_nulls (la@(〈c',false〉::lb))) [

(\P eqc0) @Hc |@Hl1bars] - |#Hl1' #x #Hx @bit_not_grid @Hl1' + |#Hl1' #x #Hx @bit_or_null_not_grid @Hl1' @memb_append_l1 @daemon ] |@daemon @@ -423,28 +596,54 @@ lemma sem_match_tuple_step: >reverse_reverse #Htapeout % [@Hnoteq] @(ex_intro … d2) - cut (∃rs31,rs32.rs3 = rs31@〈comma,false〉::rs32) - [@daemon] * #rs31 * #rs32 #Hrs3 + cut (∃rs32.rs3 = lc@〈comma,false〉::rs32) + [ (*cases (tech_split STape (λc.c == 〈bar,false〉) l4) + [ + | * #l41 * * #cbar #bfalse * #l42 * * #Hbar #Hl4 #Hl41 + @(ex_intro ?? l41) >Hl4 in Heq1; #Heq1 + + cut (sublist … lc l3) + [ #x #Hx cases la in H3; + [ normalize #H3 destruct (H3) @Hx + | #p #la' normalize #Hla' destruct (Hla') + @memb_append_l2 @memb_cons @Hx ] ] #Hsublist*) + @daemon] + * #rs32 #Hrs3 (* cut (〈c1,false〉::l3@〈comma,false〉::l4= la@〈d',false〉::rs3@〈bar,false〉::〈d2,b2〉::rs3') [@daemon] #Hcut *) + cut (l4=rs32@〈bar,false〉::〈d2,false〉::rs3') + [ >Hrs3 in Heq1; @daemon ] #Hl4 @(ex_intro … rs32) @(ex_intro … rs3') % - [>Hrs3 in Heq1; @daemon + [@Hl4 |>Htapeout @eq_f2 [@daemon - |(associative_append …la)

associative_append >associative_append + |(*>Hrs3 *)>append_cons + > (?:l1@〈grid,false〉::l2@〈bar,false〉::〈c1,false〉::l3@〈comma,false〉::rs32@〈bar,false〉::〈d2,true〉::rs3'@〈grid,false〉::rs + = (l1@〈grid,false〉::l2@〈bar,false〉::〈c1,false〉::l3@〈comma,false〉::rs32@[〈bar,false〉])@〈d2,true〉::rs3'@〈grid,false〉::rs) + [|>associative_append normalize + >associative_append normalize + >associative_append normalize + >associative_append normalize + % ] + @eq_f2 [|%] + @(injective_append … (〈d2,false〉::rs3')) + >(?:(la@[〈c',false〉])@((((lb@[〈grid,false〉])@l2@[〈bar,false〉])@la)@[〈d',false〉])@rs3 + =((la@〈c',false〉::lb)@([〈grid,false〉]@l2@[〈bar,false〉]@la@[〈d',false〉]@rs3))) + [|>associative_append >associative_append + >associative_append >associative_append >associative_append + >associative_append >associative_append % ] +

associative_append >associative_append >associative_append - >associative_append normalize @eq_f @eq_f @eq_f @eq_f - cut (true = b2) [@daemon] #Hcut >Hcut - cut (∀A,l1,l2,l3. l1 = l2 → l1@l3 = - (associative_append …la) - cut (true = b2 - - + @eq_f normalize @eq_f >associative_append + >associative_append @eq_f normalize @eq_f + >(append_cons ? 〈d',false〉) >associative_append + Hl4 associative_append normalize + >associative_append normalize % + ] + ] ] ] ] @@ -473,7 +672,7 @@ lemma sem_match_tuple_step: @memb_append_l2 @memb_cons cut (∀A,l1,l2.∀a:A. a::l1@l2=(a::l1)@l2) [//] #Hcut >Hcut >H3 >associative_append @memb_append_l2 @memb_cons @membx - |whd in ⊢ (??%?); >(bit_not_grid … Hd') >(bit_not_bar … Hd') % + |whd in ⊢ (??%?); >(bit_or_null_not_grid … Hd') >(bit_or_null_not_bar … Hd') % ] ] |#x #membx @(no_marks_in_table … Htable) @@ -498,19 +697,19 @@ definition match_tuple ≝ whileTM ? match_tuple_step (inr … (inl … (inr definition R_match_tuple ≝ λt1,t2. ∀ls,c,l1,c1,l2,rs,n. - is_bit c = true → only_bits l1 → is_bit c1 = true → n = |l1| → - table_TM (S n) (〈c1,true〉::l2) → + is_bit c = true → only_bits_or_nulls l1 → is_bit c1 = true → n = |l1| → + table_TM (S n) (〈c1,false〉::l2) → t1 = midtape STape (〈grid,false〉::ls) 〈c,true〉 (l1@〈grid,false〉::〈c1,true〉::l2@〈grid,false〉::rs) → (* facciamo match *) (∃l3,newc,mv,l4. - 〈c1,false〉::l2 = l3@〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv@l4 ∧ + 〈c1,false〉::l2 = l3@〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv::l4 ∧ t2 = midtape ? (reverse ? l1@〈c,false〉::〈grid,false〉::ls) 〈grid,false〉 - (l3@〈c,false〉::l1@〈comma,true〉::newc@〈comma,false〉::mv@l4@〈grid,false〉::rs)) + (l3@〈c,false〉::l1@〈comma,true〉::newc@〈comma,false〉::mv::l4@〈grid,false〉::rs)) ∨ (* non facciamo match su nessuna tupla; non specifichiamo condizioni sul nastro di output, perché non eseguiremo altre operazioni, quindi il suo formato non ci interessa *) (current ? t2 = Some ? 〈grid,true〉 ∧ ∀l3,newc,mv,l4. - 〈c1,false〉::l2 ≠ l3@〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv@l4). + 〈c1,false〉::l2 ≠ l3@〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv::l4).