From 5a641566011deca8c2894144fbbca3ac35ba915d Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Thu, 24 May 2012 15:15:14 +0000 Subject: [PATCH] Progress --- .../matita/lib/turing/universal/move_tape.ma | 4 +- matita/matita/lib/turing/universal/tuples.ma | 60 +++++++++++++++---- .../matita/lib/turing/universal/uni_step.ma | 15 +++-- 3 files changed, 61 insertions(+), 18 deletions(-) diff --git a/matita/matita/lib/turing/universal/move_tape.ma b/matita/matita/lib/turing/universal/move_tape.ma index 2f5a342d6..4ec94cbc3 100644 --- a/matita/matita/lib/turing/universal/move_tape.ma +++ b/matita/matita/lib/turing/universal/move_tape.ma @@ -330,8 +330,8 @@ definition move_of_unialpha ≝ 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 → + match_in_table n (〈c,false〉::curs) 〈curc,false〉 + (〈c1,false〉::news) 〈newc,false〉 〈mv,false〉 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 → diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma index 18da8b92e..909c817e2 100644 --- a/matita/matita/lib/turing/universal/tuples.ma +++ b/matita/matita/lib/turing/universal/tuples.ma @@ -66,17 +66,19 @@ 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) +inductive match_in_table (n:nat) (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 + tuple_TM n (mk_tuple qin cin qout cout mv) → + match_in_table n 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 + tuple_TM n (mk_tuple qin0 cin0 qout0 cout0 mv0) → + match_in_table n qin cin qout cout mv tb → + match_in_table n qin cin qout cout mv (mk_tuple qin0 cin0 qout0 cout0 mv0@〈bar,false〉::tb). axiom append_l1_injective : @@ -101,6 +103,26 @@ axiom list_decompose_r : axiom list_decompose_memb : ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → |l1| < |l3| → memb A a l3 = true.*) +lemma table_invert_r : ∀n,t,T. + tuple_TM n t → table_TM n (t@〈bar,false〉::T) → table_TM n T. +#n #t #T #Htuple #Htable inversion Htable +[ cases t normalize [ #Hfalse | #p #t0 #Hfalse ] destruct (Hfalse) +| #t0 #T0 #Htuple0 #Htable0 #_ #Heq lapply (append_l2_injective ?????? Heq) + [ >(tuple_len … Htuple) >(tuple_len … Htuple0) % ] + -Heq #Heq destruct (Heq) // ] +qed. + +lemma match_in_table_to_tuple : + ∀n,T,qin,cin,qout,cout,mv. + match_in_table n qin cin qout cout mv T → table_TM n T → + tuple_TM n (mk_tuple qin cin qout cout mv). +#n #T #qin #cin #qout #cout #mv #Hmatch elim Hmatch +[ // +| #qin0 #cin0 #qout0 #cout0 #mv0 #tb #Htuple #Hmatch #IH #Htable + @IH @(table_invert_r ???? Htable) @Htuple +] +qed. + lemma generic_match_to_match_in_table : ∀n,T.table_TM n T → ∀qin,cin,qout,cout,mv.|qin| = n → |qout| = n → @@ -109,16 +131,17 @@ lemma generic_match_to_match_in_table : 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. + match_in_table n 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 in H1; #H1 + lapply (ttm_cons … T0 H1 Htable0) #Htable cases t1 in HT; [ >Htuple normalize in ⊢ (??%%→?); >associative_append >associative_append #HT @@ -144,7 +167,8 @@ elim Htable = mk_tuple qin cin qout cout mv@〈bar,false〉::T0) [|>Hqin >Hqout >Hcin >Hcout >Hmv normalize >associative_append >associative_append normalize >associative_append % ] - % + % %{qin0} %{cin0} %{qout0} %{cout0} %{mv0} % // % [|@Hlenqout0] % // % + [ | @Hcout0mv0 ] % // % // % // % // % // % // % | #c0 #cs0 #HT cut (∃cs1.c0::cs0 = tuple@〈bar,false〉::cs1) [ cases (append_eq_tech1 ?????? HT ?) [ -HT #ta #Hta cases (append_eq_tech2 … Hta ?) @@ -158,11 +182,24 @@ elim Htable * #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) + Htuple %2 // @(IH … HT) ] ] qed. +(* +lemma table_invert_l : ∀n,T0,qin,cin,qout,cout,mv. + table_TM n (mk_tuple qin cin qout cout mv@〈bar,false〉::T0) → + tuple_TM n (mk_tuple qin cin qout cout mv). +#n #T #qin #cin #qout #cout #mv #HT inversion HT +[ change with (append ???) in ⊢ (??(??%?)?→?);cases qin [ #Hfalse | #t0 #ts0 #Hfalse] normalize in Hfalse; destruct (Hfalse) +| #t0 #T0 #Ht0 #HT0 #_ + + +lemma table_invert_r : ∀n,T0,qin,cin,qout,cout,mv. + table n (mk_tuple qin cin qout cout mv@〈bar,false〉::T0) → table n T0. +*) + 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 @@ -196,6 +233,7 @@ lemma no_marks_in_tuple : ∀n,l.tuple_TM n l → no_marks l. | 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) % ]]]]]] diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma index 128c81aa5..ea8e991e2 100644 --- a/matita/matita/lib/turing/universal/uni_step.ma +++ b/matita/matita/lib/turing/universal/uni_step.ma @@ -463,12 +463,12 @@ definition uni_step ≝ tc_true)))) (nop ?) tc_true. - + definition R_uni_step_true ≝ λt1,t2. ∀n,t0,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv. table_TM (S n) (〈t0,false〉::table) → - match_in_table (〈s0,false〉::curconfig@[〈c0,false〉]) - (〈s1,false〉::newconfig@[〈c1,false〉]) mv (〈t0,false〉::table) → + match_in_table (S n) (〈s0,false〉::curconfig) 〈c0,false〉 + (〈s1,false〉::newconfig) 〈c1,false〉 〈mv,false〉 (〈t0,false〉::table) → legal_tape ls 〈c0,false〉 rs → t1 = midtape STape (〈grid,false〉::ls) 〈s0,false〉 (curconfig@〈c0,false〉::〈grid,false〉::〈t0,false〉::table@〈grid,false〉::rs) → @@ -506,7 +506,10 @@ lemma sem_uni_step : #tb * whd in ⊢ (%→?); #Htb lapply (Htb (〈grid,false〉::ls) (curconfig@[〈c0,false〉]) (table@〈grid,false〉::rs) s0 t0 ???) [ >Hta >associative_append % - | (* da decidere se aggiungere un'assunzione o utilizzare Hmatch *) @daemon + | (* utilizzare Hmatch + cases (match_in_table_to_tuple … Hmatch Htable) + ma serve l'iniettività di mk_tuple... + *) @daemon | (* idem *) @daemon | -Hta -Htb #Htb * #tc * whd in ⊢ (%→?); #Htc cases (Htc … Htable … Htb) -Htb -Htc @@ -515,7 +518,9 @@ lemma sem_uni_step : | >Hs0 % | (* da decidere se aggiungere un'assunzione o utilizzare Hmatch *) @daemon | (* Htable *) @daemon - | (* Htable, Hmatch → |config| = n *) @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 #Htd cases (Htd ? (refl ??)) #_ -Htd -- 2.39.2