X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Ftuples.ma;h=18da8b92eafa0531f4d657aa50b755c4d689afd0;hb=77f07b39ced234d0aea7526e6c5bfc713515dc58;hp=2520fed514fd5d4512336911279202625207dfe0;hpb=06913146ad4e17070d27b6b0a08d48f14fefb188;p=helm.git diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma index 2520fed51..18da8b92e 100644 --- a/matita/matita/lib/turing/universal/tuples.ma +++ b/matita/matita/lib/turing/universal/tuples.ma @@ -18,6 +18,9 @@ include "turing/universal/marks.ma". 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. @@ -46,59 +49,178 @@ 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_or_nulls qin ∧ only_bits_or_nulls qout ∧ bit_or_null mv = true ∧ - |qin| = n ∧ |qout| = n (* ∧ |mv| = ? *) ∧ - t = qin@〈comma,false〉::qout@〈comma,false〉::[〈mv,false〉]. + λ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. +axiom cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → a1 = a2. +axiom cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → l1 = l2. +axiom tuple_len : ∀n,t.tuple_TM n t → |t| = 2*n+5. +axiom append_eq_tech1 : + ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → |l1| < |l3| → ∃la:list A.l1@a::la = l3. +axiom append_eq_tech2 : + ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → memb A a l4 = false → ∃la:list A.l3 = l1@a::la. +(*axiom list_decompose_cases : + ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → ∃la,lb:list A.l3 = la@a::lb ∨ l4 = la@a::lb. +axiom list_decompose_l : + ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → memb A a l4 = false → + ∃la,lb.l2 = la@lb ∧ l3 = l1@a::la. +axiom list_decompose_r : + ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → memb A a l3 = false → + ∃la,lb.l1 = la@lb ∧ l4 = lb@a::l2. +axiom list_decompose_memb : + ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → |l1| < |l3| → memb A a l3 = true.*) + +lemma generic_match_to_match_in_table : + ∀n,T.table_TM n T → + ∀qin,cin,qout,cout,mv.|qin| = n → |qout| = n → + only_bits qin → only_bits qout → + bit_or_null (\fst cin) = true → bit_or_null (\fst cout) = true → + bit_or_null (\fst mv) = true → + ∀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 +#Hqinbits #Hqoutbits #Hcin #Hcout #Hmv +elim Htable +[ #t1 #t2 Htuple normalize in ⊢ (??%%→?); + >associative_append >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 + lapply (cons_injective_l ????? HT) #Hcin % [ @Hcin ] -Hcin + lapply (cons_injective_r ????? HT) -HT #HT + lapply (cons_injective_r ????? HT) -HT + >associative_append >associative_append #HT + lapply (append_l1_injective … HT) [ >Hlenqout @Hlenqout0 ] + #Hqout % [ @Hqout ] -Hqout + lapply (append_l2_injective … HT) [ >Hlenqout @Hlenqout0 ] -HT normalize #HT + lapply (cons_injective_l ????? HT) #Hcout % [ @Hcout ] -Hcout + lapply (cons_injective_r ????? HT) -HT #HT + lapply (cons_injective_r ????? HT) -HT #HT + lapply (cons_injective_l ????? HT) #Hmv % [ @Hmv ] -Hmv + @(cons_injective_r ????? HT) ] + -HT * #Hqin * #Hcin * #Hqout * #Hcout * #Hmv #HT0 + >(?:qin0@(〈cin0,false〉::〈comma,false〉::qout0@[〈cout0,false〉;〈comma,false〉;〈mv0,false〉])@〈bar,false〉::T0 + = mk_tuple qin cin qout cout mv@〈bar,false〉::T0) + [|>Hqin >Hqout >Hcin >Hcout >Hmv normalize >associative_append >associative_append + normalize >associative_append % ] + % + | #c0 #cs0 #HT cut (∃cs1.c0::cs0 = tuple@〈bar,false〉::cs1) + [ cases (append_eq_tech1 ?????? HT ?) + [ -HT #ta #Hta cases (append_eq_tech2 … Hta ?) + [ -Hta #tb #Htb %{tb} @Htb + | @daemon ] + | @le_S_S >length_append >(plus_n_O (|tuple|)) >commutative_plus @le_plus + [ @le_O_n + | >Htuple normalize >length_append >length_append @le_plus [ >Hlenqin >Hlenqin0 % ] + @le_S_S @le_S_S >length_append >length_append @le_plus [ >Hlenqout >Hlenqout0 % ] %] ] + ] + * #cs1 #Hcs1 >Hcs1 in HT; >associative_append >associative_append #HT + lapply (append_l2_injective … HT) // -HT #HT + lapply (cons_injective_r ????? HT) -HT + Htuple %2 @(IH ?? HT) + ] +] +qed. + +lemma no_grids_in_tuple : ∀n,l.tuple_TM n l → no_grids l. +#n #l * #qin * #cin * #qout * #cout * #mv * * * * * * * * * * +#_ #_ #Hqin #Hqout #Hcin #Hcout #Hmv #_ #_ #_ #Hl >Hl +#c #Hc normalize in Hc; cases (memb_append … Hc) -Hc #Hc +[ @bit_not_grid @(Hqin … Hc) +| cases (orb_true_l … Hc) -Hc #Hc +[ change with (c == 〈cin,false〉 = true) in Hc; >(\P Hc) @bit_or_null_not_grid // +| cases (orb_true_l … Hc) -Hc #Hc +[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) % +| cases (memb_append …Hc) -Hc #Hc +[ @bit_not_grid @(Hqout … Hc) +| cases (orb_true_l … Hc) -Hc #Hc +[ change with (c == 〈cout,false〉 = true) in Hc; >(\P Hc) @bit_or_null_not_grid // +| cases (orb_true_l … Hc) -Hc #Hc +[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) % +| >(memb_single … Hc) @bit_or_null_not_grid @Hmv +]]]]]] +qed. + +lemma no_marks_in_tuple : ∀n,l.tuple_TM n l → no_marks l. +#n #l * #qin * #cin * #qout * #cout * #mv * * * * * * * * * * +#Hqin #Hqout #_ #_ #_ #_ #_ #_ #_ #_ #Hl >Hl +#c #Hc normalize in Hc; cases (memb_append … Hc) -Hc #Hc +[ @(Hqin … Hc) +| cases (orb_true_l … Hc) -Hc #Hc +[ change with (c == 〈cin,false〉 = true) in Hc; >(\P Hc) % +| cases (orb_true_l … Hc) -Hc #Hc +[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) % +| cases (memb_append … Hc) -Hc #Hc +[ @(Hqout … Hc) +| cases (orb_true_l … Hc) -Hc #Hc +[ change with (c == 〈cout,false〉 = true) in Hc; >(\P Hc) % +| cases (orb_true_l … Hc) -Hc #Hc +[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) % +| >(memb_single … Hc) % +]]]]]] +qed. lemma no_grids_in_table: ∀n.∀l.table_TM n l → no_grids l. #n #l #t elim t - [normalize #n #x #H destruct - |#m #t1 #t2 * #qin * #qout * #mv * * * * * * - #Hmarks #Hqin #Hqout #Hmv #_ #_ #Heq #Ht2 #Hind - whd >Heq #x #membx - cases (memb_append … membx) -membx #membx - [cases (memb_append … membx) -membx #membx - [@bit_or_null_not_grid @Hqin // - |cases (orb_true_l … membx) -membx #membx - [>(\P membx) // - |cases (memb_append … membx) -membx #membx - [@bit_or_null_not_grid @Hqout // - |cases (orb_true_l … membx) -membx #membx - [>(\P membx) // - |@bit_or_null_not_grid >(memb_single … membx) @Hmv - ] - ] - ] - ] - |cases (orb_true_l … membx) -membx #membx - [>(\P membx) // - |@Hind // - ] - ] - ] + [normalize #c #H destruct + |#t1 #t2 #Ht1 #Ht2 #IH lapply (no_grids_in_tuple … Ht1) -Ht1 #Ht1 #x #Hx + cases (memb_append … Hx) -Hx #Hx + [ @(Ht1 … Hx) + | cases (orb_true_l … Hx) -Hx #Hx + [ >(\P Hx) % + | @(IH … Hx) ] ] ] qed. lemma no_marks_in_table: ∀n.∀l.table_TM n l → no_marks l. #n #l #t elim t - [normalize #n #x #H destruct - |#m #t1 #t2 * #qin * #qout * #mv * * * * * * - #Hmarks #_ #_ #_ #_ #_ #_ #Ht2 #Hind - #x #Hx cases (memb_append … Hx) -Hx #Hx - [@Hmarks // - |cases (orb_true_l … Hx) -Hx #Hx - [>(\P Hx) // - |@Hind // - ] - ] - ] + [normalize #c #H destruct + |#t1 #t2 #Ht1 #Ht2 #IH lapply (no_marks_in_tuple … Ht1) -Ht1 #Ht1 #x #Hx + cases (memb_append … Hx) -Hx #Hx + [ @(Ht1 … Hx) + | cases (orb_true_l … Hx) -Hx #Hx + [ >(\P Hx) % + | @(IH … Hx) ] ] ] qed. axiom last_of_table: ∀n,l,b.¬ table_TM n (l@[〈bar,b〉]). @@ -225,52 +347,45 @@ lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid) qed. definition init_current_on_match ≝ - seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c))) - (seq ? (move_l ?) - (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c))) - (seq ? (move_r ?) (mark ?)))). + (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,l3,d,rs. no_grids l1 → no_grids l2 → is_grid c = false → is_grid (\fst d) = false → - t1 = midtape STape (l1@〈grid,false〉::l2@〈c,false〉::〈grid,false〉::l3) d rs → - t2 = midtape STape (〈grid,false〉::l3) 〈c,true〉 - ((reverse ? (l1@〈grid,false〉::l2)@d::rs)). + ∀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_adv_to_mark_l ? (λc:STape.is_grid (\fst c))) - (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) +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 #l3 #d #rs #Hl1 #Hl2 #Hc #Hd #Hintape -cases HR -HR #ta * whd in ⊢ (%→?); #Hta cases (Hta … Hintape) -Hta -Hintape - [ * >Hd #Hfalse normalize in Hfalse; destruct (Hfalse) ] -* #_ #Hta lapply (Hta l1 〈grid,false〉 ? (refl ??) (refl …) Hl1) -Hta #Hta -* #tb * whd in ⊢ (%→?); #Htb lapply (Htb … Hta) -Htb -Hta -generalize in match Hl2; cases l2 - [#Hl2 whd in ⊢ ((???(??%%%))→?); #Htb - * #tc * whd in ⊢ (%→?); #Htc cases (Htc … Htb) -Htb +#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 …) Hl2) + * #_ #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 >reverse_append % - |#d #tl #Htl whd in ⊢ ((???(??%%%))→?); #Htb - * #tc * whd in ⊢ (%→?); #Htc cases (Htc … Htb) -Htc + >Houtc % + |#d #tl #Htl whd in ⊢ ((???(??%%%))→?); #Hta + * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Htb [* >(Htl … (memb_hd …)) #Htemp destruct (Htemp)] - * #Hd >append_cons #Htc lapply (Htc … (refl ??) (refl …) ?) + * #Hd >append_cons #Htb lapply (Htb … (refl ??) (refl …) ?) [#x #membx cases (memb_append … membx) -membx #membx - [@Htl @memb_cons @membx | >(memb_single … membx) @Hc]] #Htc - * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htc -Htd - >reverse_append >associative_append whd in ⊢ ((???(??%%%))→?); #Htd - whd in ⊢ (%→?); #Houtc lapply (Houtc … Htd) -Houtc #Houtc - >Houtc >reverse_append >reverse_cons >reverse_cons - >associative_append >associative_append >associative_append % + [@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. @@ -658,13 +773,13 @@ definition R_match_tuple ≝ λt1,t2. (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).