From 06913146ad4e17070d27b6b0a08d48f14fefb188 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Fri, 18 May 2012 15:43:37 +0000 Subject: [PATCH] Progress --- matita/matita/lib/turing/universal/copy.ma | 55 ++++++++++- matita/matita/lib/turing/universal/tuples.ma | 2 +- .../matita/lib/turing/universal/uni_step.ma | 92 ++++++++++++++++++- 3 files changed, 142 insertions(+), 7 deletions(-) diff --git a/matita/matita/lib/turing/universal/copy.ma b/matita/matita/lib/turing/universal/copy.ma index 6b77ef9b7..de39fb88c 100644 --- a/matita/matita/lib/turing/universal/copy.ma +++ b/matita/matita/lib/turing/universal/copy.ma @@ -301,11 +301,58 @@ lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop (* by IH, we proceed by cases, whether a = comma (consequently several lists = []) or not *) * - [ * #Ha #Houtc1 >Hl1cons in Hl1; >Hla + [ * #Ha #Houtc1 +(* cut (l1 = [〈a,false〉]) + [ cases l1'' in Hl1cons; // #y #ly #Hly + >Hly in Hl1; cases l1' in Hl1bits; + [ #_ normalize #Hfalse destruct (Hfalse) + | #p #lp #Hl1bits normalize #Heq destruct (Heq) + @False_ind lapply (Hl1bits 〈a,false〉 ?) + [ cases lp in e0; + [ normalize #Hfalse destruct (Hfalse) + | #p0 #lp0 normalize in ⊢ (%→?); #Heq destruct (Heq) + @memb_cons @memb_hd ] + | >Ha normalize #Hfalse destruct (Hfalse) ] + ] + ] #Hl1a + cut (l4 = [〈a0,false〉]) + [ generalize in match Hl4bits; cases l4' in Hl4; + [ >Hl4cons #Hfalse #_ + lapply (inj_append_singleton_l1 ?? [] ?? Hfalse) + cases (reverse ? l4'') normalize + [ #Hfalse1 | #p0 #lp0 #Hfalse1 ] destruct (Hfalse1) + | #p #lp + + cases l4'' in Hl4cons; // #y #ly #Hly + >Hly in Hl4; cases l4' in Hl4bits; + [ #_ >reverse_cons #Hfalse + lapply (inj_append_singleton_l1 ?? [] ?? Hfalse) + -Hfalse cases ly normalize + [ #Hfalse | #p #Hp #Hfalse ] destruct (Hfalse) + + | #p #lp #Hl1bits normalize #Heq destruct (Heq) + @False_ind lapply (Hl1bits 〈a,false〉 ?) + [ cases lp in e0; + [ normalize #Hfalse destruct (Hfalse) + | #p0 #lp0 normalize in ⊢ (%→?); #Heq destruct (Heq) + @memb_cons @memb_hd ] + | >Ha normalize #Hfalse destruct (Hfalse) ] + ] + ] #Hl1a + + >Hla normalize #Hl1 destruct (Hl1) lapply (inj_append_ @False_ind + + cut (l1'' = [] ∧ l4'' = []) + [ % [ >Hla in Hl1; normalize #Hl1 destruct (Hl1) + + cases l1'' in Hl1bits; + + [ #_ normalize #H *) + cut (la = [] ∧ lb = [] ∧ l1'' = [] ∧ l4'' = []) + [ @daemon ] * * * #Hla1 #Hlb1 #Hl1nil #Hl4nil + >Hl1cons in Hl1; >Hla >Houtc1 >Htc #Hl1 >Hl4cons in Hl4; >Hlb #Hl4 - cut (la = [] ∧ lb = [] ∧ l1'' = [] ∧ l4'' = []) - [@daemon] * * * #Hla1 #Hlb1 #Hl1nil #Hl4nil >Hla1 >Hlb1 >Hl1nil >Hl4nil >Hx cut (a0 = grid) [ @daemon ] #Ha0 associative_append % @@ -363,7 +410,7 @@ definition R_copy ≝ λt1,t2. ∀ls,c,c0,rs,l1,l3,l4. t1 = midtape STape (l3@〈grid,false〉::l4@〈c0,true〉::ls) 〈c,true〉 (l1@〈comma,false〉::rs) → no_marks l1 → no_marks l3 → no_marks l4 → |l1| = |l4| → - only_bits_or_nulls (〈c0,true〉::l4) → only_bits_or_nulls (〈c,true〉::l1) → + only_bits_or_nulls (l4@[〈c0,true〉]) → only_bits_or_nulls (〈c,true〉::l1) → t2 = midtape STape (reverse ? l1@l3@〈grid,false〉:: merge_config (l4@[〈c0,false〉]) (reverse ? (〈c,false〉::l1))@ls) 〈comma,false〉 rs. diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma index a7afb0b2b..2520fed51 100644 --- a/matita/matita/lib/turing/universal/tuples.ma +++ b/matita/matita/lib/turing/universal/tuples.ma @@ -653,7 +653,7 @@ 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_or_nulls l1 → is_bit c1 = true → n = |l1| → - table_TM (S n) (〈c1,true〉::l2) → + 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 *) diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma index 1cb035a6a..701972f3f 100644 --- a/matita/matita/lib/turing/universal/uni_step.ma +++ b/matita/matita/lib/turing/universal/uni_step.ma @@ -170,5 +170,93 @@ cases HR -HR ] ] qed. - ]-Htf -qed. + +include "turing/universal/move_tape.ma". + +definition exec_move ≝ + seq ? (adv_to_mark_r … (is_marked ?)) + (seq ? init_copy + (seq ? copy + (seq ? (move_r …) + (seq ? move_tape (move_r …))))). + +definition lift_tape ≝ λls,c,rs. + let 〈c0,b〉 ≝ c in + let c' ≝ match c0 with + [ null ⇒ None ? + | _ ⇒ Some ? c ] + in + mk_tape STape ls c' rs. + +definition sim_current_of_tape ≝ λt. + match current STape t with + [ None ⇒ 〈null,false〉 + | Some c0 ⇒ c0 ]. + +(* + t1 = ls # cs c # table # rs + + let simt ≝ lift_tape ls c rs in + let simt' ≝ move_left simt' in + + t2 = left simt'# cs (sim_current_of_tape simt') # table # right simt' +*) + +(* +definition R_move + +definition R_exec_move ≝ λt1,t2. + ∀ls,current,table1,newcurrent,table2,rs. + t1 = midtape STape (current@〈grid,false〉::ls) 〈grid,false〉 + (table1@〈comma,true〉::newcurrent@〈comma,false〉::move::table2@ + 〈grid,false〉::rs) → + table_TM (table1@〈comma,false〉::newcurrent@〈comma,false〉::move::table2) → + t2 = midtape +*) + +(* + +step : + +if is_true(current) (* current state is final *) + then nop + else + init_match; + match_tuple; + if is_marked(current) = false (* match ok *) + then exec_move; + else sink; + +*) + +definition mk_tuple ≝ λc,newc,mv. + c @ 〈comma,false〉:: newc @ 〈comma,false〉 :: [〈mv,false〉]. + +inductive match_in_table (c,newc:list STape) (mv:unialpha) : list STape → Prop ≝ +| mit_hd : + ∀tb. + match_in_table c newc mv (mk_tuple c newc mv@〈bar,false〉::tb) +| mit_tl : + ∀c0,newc0,mv0,tb. + match_in_table c newc mv tb → + match_in_table c newc mv (mk_tuple c0 newc0 mv0@〈bar,false〉::tb). + +definition move_of_unialpha ≝ + λc.match c with + [ bit x ⇒ match x with [ true ⇒ R | false ⇒ L ] + | _ ⇒ N ]. + +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〉)). + + \ No newline at end of file -- 2.39.2