X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Fmove_tape.ma;h=ab16d56c7f3c1a6af4c9b104a7437ccb26d845b4;hb=31cb2f0b374657eb5acb95708443e2c1b8481891;hp=acd45dcd77fc943593d1d632721b4d442a173c0d;hpb=5018d09db806b85ccf20fe0a4f07219bf704bfb6;p=helm.git diff --git a/matita/matita/lib/turing/universal/move_tape.ma b/matita/matita/lib/turing/universal/move_tape.ma index acd45dcd7..ab16d56c7 100644 --- a/matita/matita/lib/turing/universal/move_tape.ma +++ b/matita/matita/lib/turing/universal/move_tape.ma @@ -9,21 +9,24 @@ \ / GNU General Public License Version 2 V_____________________________________________________________*) -include "turing/universal/move_char_c.ma". -include "turing/universal/move_char_l.ma". +include "turing/move_char.ma". +include "turing/universal/marks.ma". include "turing/universal/tuples.ma". definition init_cell_states ≝ initN 2. +definition ics0 : init_cell_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)). +definition ics1 : init_cell_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)). + definition init_cell ≝ mk_TM STape init_cell_states (λp.let 〈q,a〉 ≝ p in - match q with + match pi1 … q with [ O ⇒ match a with - [ None ⇒ 〈1, Some ? 〈〈null,false〉,N〉〉 - | Some _ ⇒ 〈1, None ?〉 ] - | S _ ⇒ 〈1,None ?〉 ]) - O (λq.q == 1). + [ None ⇒ 〈ics1, Some ? 〈〈null,false〉,N〉〉 + | Some _ ⇒ 〈ics1, None ?〉 ] + | S _ ⇒ 〈ics1,None ?〉 ]) + ics0 (λq.q == ics1). definition R_init_cell ≝ λt1,t2. (∃c.current STape t1 = Some ? c ∧ t2 = t1) ∨ @@ -31,88 +34,6 @@ definition R_init_cell ≝ λt1,t2. axiom sem_init_cell : Realize ? init_cell R_init_cell. -definition swap_states : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 4) alpha. - -definition swap ≝ - λalpha:FinSet.λd:alpha. - mk_TM alpha (mcl_states alpha) - (λp.let 〈q,a〉 ≝ p in - let 〈q',b〉 ≝ q in - match a with - [ None ⇒ 〈〈3,d〉,None ?〉 - | Some a' ⇒ - match q' with - [ O ⇒ (* qinit *) - 〈〈1,a'〉,Some ? 〈a',R〉〉 - | S q' ⇒ match q' with - [ O ⇒ (* q1 *) - 〈〈2,a'〉,Some ? 〈b,L〉〉 - | S q' ⇒ match q' with - [ O ⇒ (* q2 *) - 〈〈3,d〉,Some ? 〈b,N〉〉 - | S _⇒ (* qacc *) - 〈〈3,d〉,None ?〉 ] ] ] ]) - 〈0,d〉 - (λq.let 〈q',a〉 ≝ q in q' == 3). - -definition R_swap ≝ - λalpha,t1,t2. - ∀a,b,ls,rs. - t1 = midtape alpha ls b (a::rs) → - t2 = midtape alpha ls a (b::rs). - -(* -lemma swap_q0_q1 : - ∀alpha:FinSet.∀d,a,ls,a0,rs. - step alpha (swap alpha d) - (mk_config ?? 〈0,a〉 (mk_tape … ls (Some ? a0) rs)) = - mk_config alpha (states ? (swap alpha d)) 〈1,a0〉 - (tape_move_right alpha ls a0 rs). -#alpha #d #a * -[ #a0 #rs % -| #a1 #ls #a0 #rs % -] -qed. - -lemma swap_q1_q2 : - ∀alpha:FinSet.∀d,a,ls,a0,rs. - step alpha (swap alpha d) - (mk_config ?? 〈1,a〉 (mk_tape … ls (Some ? a0) rs)) = - mk_config alpha (states ? (swap alpha d)) 〈2,a0〉 - (tape_move_left alpha ls a rs). -#alpha #sep #a #ls #a0 * // -qed. - -lemma swap_q2_q3 : - ∀alpha:FinSet.∀d,a,ls,a0,rs. - step alpha (swap alpha d) - (mk_config ?? 〈2,a〉 (mk_tape … ls (Some ? a0) rs)) = - mk_config alpha (states ? (swap alpha d)) 〈3,d〉 - (tape_move_left alpha ls a rs). -#alpha #sep #a #ls #a0 * // -qed. -*) - -lemma sem_swap : - ∀alpha,d. - Realize alpha (swap alpha d) (R_swap alpha). -#alpha #d #tapein @(ex_intro ?? 4) cases tapein -[ @ex_intro [| % [ % | #a #b #ls #rs #Hfalse destruct (Hfalse) ] ] -| #a #al @ex_intro [| % [ % | #a #b #ls #rs #Hfalse destruct (Hfalse) ] ] -| #a #al @ex_intro [| % [ % | #a #b #ls #rs #Hfalse destruct (Hfalse) ] ] -| #ls #c #rs cases rs - [ @ex_intro [| % [ % | #a #b #ls0 #rs0 #Hfalse destruct (Hfalse) ] ] - | -rs #r #rs @ex_intro - [|% - [% - | #r0 #c0 #ls0 #rs0 #Htape destruct (Htape) normalize cases ls0 - [% | #l1 #ls1 %] ] ] ] ] -qed. - -axiom ssem_move_char_l : - ∀alpha,sep. - Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep). - (* MOVE TAPE RIGHT: @@ -251,45 +172,106 @@ qed. (* MOVE TAPE LEFT: - ls # current c # table # d rs - ^ - ls # current c # table # d rs - ^ - ls # current c # table d # rs - ^ - ls # current c # d table # rs - ^ - ls # current c # d table # rs - ^ + ls d? # current c # table # rs + ^ move_l; adv_to_mark_l + ls d? # current c # table # rs + ^ move_l; adv_to_mark_l + ls d? # current c # table # rs + ^ move_l + ls d? # current c # table # rs + ^ init_cell + ls d # current c # table # rs + ^ mtl_aux ls # current c d # table # rs - ^ - ls # current c d # table # rs - ^ - ls # c current c # table # rs - ^ - ls # c current c # table # rs + ^ swap_r + ls # current d c # table # rs + ^ mtl_aux + ls # current d # table c # rs + ^ swap + ls # current d # table # c rs + ^ move_l; adv_to_mark_l + ls # current d # table # c rs + ^ move_l; adv_to_mark_l + ls # current d # table # c rs ^ - ls c # current c # table # rs - ^ - -move_to_grid_r; -swap; -move_char_l; -move_l; -swap; -move_l; -move_char_l; -move_l; -swap *) -axiom move_tape_l : TM STape. +definition mtl_aux ≝ + seq ? (swap STape 〈grid,false〉) + (seq ? (move_r …) (seq ? (move_r …) (seq ? (move_char_r STape 〈grid,false〉) (move_l …)))). +definition R_mtl_aux ≝ λt1,t2. + ∀l1,l2,l3,r. t1 = midtape STape l1 r (〈grid,false〉::l2@〈grid,false〉::l3) → no_grids l2 → + t2 = midtape STape (reverse ? l2@〈grid,false〉::l1) r (〈grid,false〉::l3). + +lemma sem_mtl_aux : Realize ? mtl_aux R_mtl_aux. +#intape +cases (sem_seq … (sem_swap STape 〈grid,false〉) (sem_seq … (sem_move_r …) + (sem_seq … (sem_move_r …) (sem_seq … (ssem_move_char_r STape 〈grid,false〉) + (sem_move_l …)))) intape) +#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop +#l1 #l2 #l3 #r #Hintape #Hl2 +cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta #Hta +* #tb * whd in ⊢(%→?); #Htb lapply (Htb … Hta) -Htb -Hta whd in ⊢ (???%→?); #Htb +* #tc * whd in ⊢(%→?); #Htc lapply (Htc … Htb) -Htc -Htb cases l2 in Hl2; +[ #_ #Htc * #td * whd in ⊢(%→?); #Htd lapply (Htd … Htc) -Htd >Htc -Htc * #Htd #_ + whd in ⊢ (%→?); #Houtc lapply (Htd (refl ??)) -Htd @Houtc +| #c0 #l0 #Hnogrids #Htc * + #td * whd in ⊢(%→?); #Htd lapply (Htd … Htc) -Htd -Htc * #_ #Htd + lapply (Htd … (refl ??) ??) + [ cases (true_or_false (memb STape 〈grid,false〉 l0)) #Hmemb + [ @False_ind lapply (Hnogrids 〈grid,false〉 ?) + [ @memb_cons // | normalize #Hfalse destruct (Hfalse) ] + | @Hmemb ] + | % #Hc0 lapply (Hnogrids c0 ?) + [ @memb_hd | >Hc0 normalize #Hfalse destruct (Hfalse) ] + | #Htd whd in ⊢(%→?); >Htd #Houtc lapply (Houtc … (refl ??)) -Houtc #Houtc + >reverse_cons >associative_append @Houtc +]] +qed. + +definition R_ml_atml ≝ λt1,t2. + ∀ls1,ls2,rs.no_grids ls1 → + t1 = midtape STape (ls1@〈grid,false〉::ls2) 〈grid,false〉 rs → + t2 = midtape STape ls2 〈grid,false〉 (reverse ? ls1@〈grid,false〉::rs). + +lemma sem_ml_atml : + Realize ? ((move_l …) · (adv_to_mark_l … (λc:STape.is_grid (\fst c)))) R_ml_atml. +#intape +cases (sem_seq … (sem_move_l …) (sem_adv_to_mark_l … (λc:STape.is_grid (\fst c))) intape) +#k * #outc * #Hloop #HR %{k} %{outc} % [@Hloop] -Hloop +#ls1 #ls2 #rs #Hnogrids #Hintape cases HR -HR +#ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta +cases ls1 in Hnogrids; +[ #_ #Hta whd in ⊢ (%→?); #Houtc cases (Houtc … Hta) -Houtc + [ * #_ >Hta #Houtc @Houtc + | * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ] +| #c0 #l0 #Hnogrids #Hta whd in ⊢ (%→?); #Houtc cases (Houtc … Hta) -Houtc + [ * #Hc0 lapply (Hnogrids c0 (memb_hd …)) >Hc0 #Hfalse destruct (Hfalse) + | * #_ #Htb >reverse_cons >associative_append @Htb // + #x #Hx @Hnogrids @memb_cons // + ] +] +qed. + +definition move_tape_l : TM STape ≝ + seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c)))) + (seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c)))) + (seq ? (move_l …) + (seq ? init_cell + (seq ? mtl_aux + (seq ? (swap_r STape 〈grid,false〉) + (seq ? mtl_aux + (seq ? (swap STape 〈grid,false〉) + (seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c)))) + (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c)))))))))))). + (* seq ? (move_r …) (seq ? init_cell (seq ? (move_l …) (seq ? (swap STape 〈grid,false〉) (seq ? mtr_aux (seq ? (move_l …) mtr_aux))))). *) definition R_move_tape_l ≝ λt1,t2. ∀rs,n,table,c0,bc0,curconfig,ls0. - bit_or_null c0 = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) → + bit_or_null c0 = true → only_bits_or_nulls curconfig → + table_TM n (reverse ? table) → only_bits ls0 → t1 = midtape STape (table@〈grid,false〉::〈c0,bc0〉::curconfig@〈grid,false〉::ls0) 〈grid,false〉 rs → (ls0 = [] ∧ @@ -299,7 +281,94 @@ definition R_move_tape_l ≝ λt1,t2. t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@l1::〈grid,false〉::reverse ? table@〈grid,false〉::〈c0,bc0〉::rs)). -axiom sem_move_tape_l : Realize ? move_tape_l R_move_tape_l. +lemma sem_move_tape_l : Realize ? move_tape_l R_move_tape_l. +#tapein +cases (sem_seq … sem_ml_atml + (sem_seq … sem_ml_atml + (sem_seq … (sem_move_l …) + (sem_seq … sem_init_cell + (sem_seq … sem_mtl_aux + (sem_seq … (sem_swap_r STape 〈grid,false〉) + (sem_seq … sem_mtl_aux + (sem_seq … (sem_swap STape 〈grid,false〉) + (sem_seq … sem_ml_atml sem_ml_atml)))))))) tapein) +#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop +#rs #n #table #c0 #bc0 #curconfig #ls0 #Hbitnullc0 #Hbitnullcc #Htable #Hls0 #Htapein +cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Htapein) +[ @daemon (* by no_grids_in_table, manca un lemma sulla reverse *) ] +-Hta #Hta * #tb * whd in ⊢ (%→?); #Htb lapply (Htb (〈c0,bc0〉::curconfig) … Hta) +[ @daemon ] -Hta -Htb #Htb +* #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htb -Htc #Htc +* #td * whd in ⊢ (%→?); * +[ * #c1 * generalize in match Htc; generalize in match Htapein; -Htapein -Htc + cases ls0 in Hls0; + [ #_ #_ #Htc >Htc normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ] + #l1 #ls1 #Hls0 #Htapein #Htc change with (midtape ? ls1 l1 ?) in Htc:(???%); >Htc + #Hl1 whd in Hl1:(??%?); #Htd + * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?) + [ (* memb_reverse *) @daemon ] -Hte -Htd >reverse_reverse #Hte + * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf -Hte #Htf + * #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?) + [ @(no_grids_in_table … Htable) ] -Htg -Htf >reverse_reverse #Htg + * #th * whd in ⊢ (%→?); #Hth lapply (Hth … Htg) -Hth -Htg #Hth + * #ti * whd in ⊢ (%→?); #Hti lapply (Hti … Hth) + [ (* memb_reverse *) @daemon ] -Hti -Hth #Hti + whd in ⊢ (%→?); #Houtc lapply (Houtc (l1::curconfig) … Hti) + [ #x #Hx cases (orb_true_l … Hx) -Hx #Hx + [ >(\P Hx) lapply (Hls0 l1 (memb_hd …)) @bit_not_grid + | lapply (Hbitnullcc ? Hx) @bit_or_null_not_grid ] ] + -Houtc >reverse_cons >associative_append #Houtc %2 %{l1} %{ls1} % [%] @Houtc +| * generalize in match Htc; generalize in match Htapein; -Htapein -Htc + cases ls0 + [| #l1 #ls1 #_ #Htc >Htc normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ] + #Htapein #Htc change with (leftof ???) in Htc:(???%); >Htc #_ #Htd + * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?) + [ (*memb_reverse*) @daemon ] -Hte -Htd >reverse_reverse #Hte + * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf -Hte #Htf + * #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?) + [ @(no_grids_in_table … Htable) ] -Htg -Htf >reverse_reverse #Htg + * #th * whd in ⊢ (%→?); #Hth lapply (Hth … Htg) -Hth -Htg #Hth + * #ti * whd in ⊢ (%→?); #Hti lapply (Hti … Hth) + [ (*memb_reverse*) @daemon ] -Hti -Hth #Hti + whd in ⊢ (%→?); #Houtc lapply (Houtc (〈null,false〉::curconfig) … Hti) + [ #x #Hx cases (orb_true_l … Hx) -Hx #Hx + [ >(\P Hx) % + | lapply (Hbitnullcc ? Hx) @bit_or_null_not_grid ] ] + -Houtc >reverse_cons >associative_append + >reverse_cons >associative_append #Houtc % % [%] @Houtc +] +qed. + +(*definition mtl_aux ≝ + seq ? (move_r …) (seq ? (move_char_r STape 〈grid,false〉) (move_l …)). +definition R_mtl_aux ≝ λt1,t2. + ∀l1,l2,l3,r. t1 = midtape STape l1 r (l2@〈grid,false〉::l3) → no_grids l2 → + t2 = midtape STape (reverse ? l2@l1) r (〈grid,false〉::l3). + +lemma sem_mtl_aux : Realize ? mtl_aux R_mtl_aux. +#intape +cases (sem_seq … (sem_move_r …) (sem_seq … (ssem_move_char_r STape 〈grid,false〉) (sem_move_l …)) intape) +#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop +#l1 #l2 #l3 #r #Hintape #Hl2 +cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta #Hta +* #tb * whd in ⊢(%→?); generalize in match Hta; -Hta cases l2 in Hl2; +[ #_ #Hta #Htb lapply (Htb … Hta) -Htb * #Htb #_ whd in ⊢ (%→?); #Houtc + lapply (Htb (refl ??)) -Htb >Hta @Houtc +| #c0 #l0 #Hnogrids #Hta #Htb lapply (Htb … Hta) -Htb * #_ #Htb + lapply (Htb … (refl ??) ??) + [ cases (true_or_false (memb STape 〈grid,false〉 l0)) #Hmemb + [ @False_ind lapply (Hnogrids 〈grid,false〉 ?) + [ @memb_cons // | normalize #Hfalse destruct (Hfalse) ] + | @Hmemb ] + | % #Hc0 lapply (Hnogrids c0 ?) + [ @memb_hd | >Hc0 normalize #Hfalse destruct (Hfalse) ] + | #Htb whd in ⊢(%→?); >Htb #Houtc lapply (Houtc … (refl ??)) -Houtc #Houtc + >reverse_cons >associative_append @Houtc +]] +qed. + +check swap*) + (* by cases on current: @@ -321,17 +390,6 @@ definition sim_current_of_tape ≝ λt. [ None ⇒ 〈null,false〉 | Some c0 ⇒ c0 ]. -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 @@ -341,8 +399,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 → @@ -354,18 +412,85 @@ definition R_uni_step ≝ λt1,t2. definition no_nulls ≝ λl:list STape.∀x.memb ? x l = true → is_null (\fst x) = false. +definition current_of_alpha ≝ λc:STape. + match \fst c with [ null ⇒ None ? | _ ⇒ Some ? c ]. + +(* + no_marks (c::ls@rs) + only_bits (ls@rs) + bit_or_null c + +*) +definition legal_tape ≝ λls,c,rs. + no_marks (c::ls@rs) ∧ only_bits (ls@rs) ∧ bit_or_null (\fst c) = true ∧ + (\fst c ≠ null ∨ ls = [] ∨ rs = []). + +lemma legal_tape_left : + ∀ls,c,rs.legal_tape ls c rs → + left ? (mk_tape STape ls (current_of_alpha c) rs) = ls. +#ls * #c #bc #rs * * * #_ #_ #_ * +[ * + [ cases c + [ #c' #_ % + | * #Hfalse @False_ind /2/ + |*: #_ % ] + | #Hls >Hls cases c // cases rs // + ] +| #Hrs >Hrs cases c // cases ls // +] +qed. + +axiom legal_tape_current : + ∀ls,c,rs.legal_tape ls c rs → + current ? (mk_tape STape ls (current_of_alpha c) rs) = current_of_alpha c. + +axiom legal_tape_right : + ∀ls,c,rs.legal_tape ls c rs → + right ? (mk_tape STape ls (current_of_alpha c) rs) = rs. + +(* +lemma legal_tape_cases : + ∀ls,c,rs.legal_tape ls c rs → + \fst c ≠ null ∨ (\fst c = null ∧ (ls = [] ∨ rs = [])). +#ls #c #rs cases c #c0 #bc0 cases c0 +[ #c1 normalize #_ % % #Hfalse destruct (Hfalse) +| cases ls + [ #_ %2 % // % % + | #l0 #ls0 cases rs + [ #_ %2 % // %2 % + | #r0 #rs0 normalize * * #_ #Hrs destruct (Hrs) ] + ] +|*: #_ % % #Hfalse destruct (Hfalse) ] +qed. + +axiom legal_tape_conditions : + ∀ls,c,rs.(\fst c ≠ null ∨ ls = [] ∨ rs = []) → legal_tape ls c rs. +(*#ls #c #rs * +[ * + [ >(eq_pair_fst_snd ?? c) cases (\fst c) + [ #c0 #Hc % % % + | * #Hfalse @False_ind /2/ + |*: #Hc % % % + ] + | cases ls [ * #Hfalse @False_ind /2/ ] + #l0 #ls0 + + #Hc +*) +*) + definition R_move_tape_r_abstract ≝ λt1,t2. ∀rs,n,table,curc,curconfig,ls. - bit_or_null curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) → + is_bit curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) → t1 = midtape STape (table@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls) 〈grid,false〉 rs → - no_nulls rs → + legal_tape ls 〈curc,false〉 rs → ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs → ∃ls1,rs1,newc. - (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@newc:: + (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉:: 〈grid,false〉::reverse ? table@〈grid,false〉::rs1) ∧ - lift_tape ls1 newc rs1 = - tape_move_right STape ls 〈curc,false〉 rs). + lift_tape ls1 〈newc,false〉 rs1 = + tape_move_right STape ls 〈curc,false〉 rs ∧ legal_tape ls1 〈newc,false〉 rs1). lemma lift_tape_not_null : ∀ls,c,rs. is_null (\fst c) = false → @@ -374,68 +499,133 @@ lemma lift_tape_not_null : [|normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ] // qed. + +axiom bit_not_null : ∀d.is_bit d = true → is_null d = false. lemma mtr_concrete_to_abstract : ∀t1,t2.R_move_tape_r t1 t2 → R_move_tape_r_abstract t1 t2. #t1 #t2 whd in ⊢(%→?); #Hconcrete -#rs #n #table #curc #curconfig #ls #Hcurc #Hcurconfig #Htable #Ht1 -#Hrsnonulls #t1' #Ht1' +#rs #n #table #curc #curconfig #ls #Hbitcurc #Hcurconfig #Htable #Ht1 +* * * #Hnomarks #Hbits #Hcurc #Hlegal #t1' #Ht1' cases (Hconcrete … Htable Ht1) // [ * #Hrs #Ht2 @(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? []) - @(ex_intro ?? 〈null,false〉) % - [ >Ht2 % - | >Hrs % ] -| * #r0 * #rs0 * #Hrs #Ht2 + @(ex_intro ?? null) % + [ % + [ >Ht2 % + | >Hrs % ] + | % [ % [ % + [ >append_nil #x #Hx cases (orb_true_l … Hx) #Hx' + [ >(\P Hx') % + | @Hnomarks @(memb_append_l1 … Hx') ] + | >append_nil #x #Hx cases (orb_true_l … Hx) #Hx' + [ >(\P Hx') // + | @Hbits @(memb_append_l1 … Hx') ]] + | % ] + | %2 % ] + ] +| * * #r0 #br0 * #rs0 * #Hrs + cut (br0 = false) + [ @(Hnomarks 〈r0,br0〉) @memb_cons @memb_append_l2 >Hrs @memb_hd] + #Hbr0 >Hbr0 in Hrs; #Hrs #Ht2 @(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? rs0) @(ex_intro ?? r0) % - [ >Ht2 % - | >Hrs >lift_tape_not_null - [ % - | @Hrsnonulls >Hrs @memb_hd ] ] + [ % + [ >Ht2 // + | >Hrs >lift_tape_not_null + [ % + | @bit_not_null @(Hbits 〈r0,false〉) >Hrs @memb_append_l2 @memb_hd ] ] + | % [ % [ % + [ #x #Hx cases (orb_true_l … Hx) #Hx' + [ >(\P Hx') % + | cases (memb_append … Hx') #Hx'' @Hnomarks + [ @(memb_append_l1 … Hx'') + | >Hrs @memb_cons @memb_append_l2 @(memb_cons … Hx'') ] + ] + | whd in ⊢ (?%); #x #Hx cases (orb_true_l … Hx) #Hx' + [ >(\P Hx') // + | cases (memb_append … Hx') #Hx'' @Hbits + [ @(memb_append_l1 … Hx'') | >Hrs @memb_append_l2 @(memb_cons … Hx'') ] + ]] + | whd in ⊢ (??%?); >(Hbits 〈r0,false〉) // + @memb_append_l2 >Hrs @memb_hd ] + | % % % #Hr0 lapply (Hbits 〈r0,false〉?) + [ @memb_append_l2 >Hrs @memb_hd + | >Hr0 normalize #Hfalse destruct (Hfalse) + ] ] ] ] qed. definition R_move_tape_l_abstract ≝ λt1,t2. ∀rs,n,table,curc,curconfig,ls. - bit_or_null curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) → + is_bit curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) → t1 = midtape STape (table@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls) 〈grid,false〉 rs → - no_nulls ls → + legal_tape ls 〈curc,false〉 rs → ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs → ∃ls1,rs1,newc. - (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@newc:: + (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉:: 〈grid,false〉::reverse ? table@〈grid,false〉::rs1) ∧ - lift_tape ls1 newc rs1 = - tape_move_left STape ls 〈curc,false〉 rs). + lift_tape ls1 〈newc,false〉 rs1 = + tape_move_left STape ls 〈curc,false〉 rs ∧ legal_tape ls1 〈newc,false〉 rs1). lemma mtl_concrete_to_abstract : ∀t1,t2.R_move_tape_l t1 t2 → R_move_tape_l_abstract t1 t2. #t1 #t2 whd in ⊢(%→?); #Hconcrete #rs #n #table #curc #curconfig #ls #Hcurc #Hcurconfig #Htable #Ht1 -#Hlsnonulls #t1' #Ht1' -cases (Hconcrete … Htable Ht1) // +* * * #Hnomarks #Hbits #Hcurc #Hlegal #t1' #Ht1' +cases (Hconcrete … Htable ? Ht1) // [ * #Hls #Ht2 @(ex_intro ?? []) @(ex_intro ?? (〈curc,false〉::rs)) - @(ex_intro ?? 〈null,false〉) % - [ >Ht2 % - | >Hls % ] -| * #l0 * #ls0 * #Hls #Ht2 - @(ex_intro ?? ls0) - @(ex_intro ?? (〈curc,false〉::rs)) + @(ex_intro ?? null) % + [ % + [ >Ht2 % + | >Hls % ] + | % [ % [ % + [ #x #Hx cases (orb_true_l … Hx) #Hx' + [ >(\P Hx') % + | @Hnomarks >Hls @Hx' ] + | #x #Hx cases (orb_true_l … Hx) #Hx' + [ >(\P Hx') // + | @Hbits >Hls @Hx' ]] + | % ] + | % %2 % ] + ] +| * * #l0 #bl0 * #ls0 * #Hls + cut (bl0 = false) + [ @(Hnomarks 〈l0,bl0〉) @memb_cons @memb_append_l1 >Hls @memb_hd] + #Hbl0 >Hbl0 in Hls; #Hls #Ht2 + @(ex_intro ?? ls0) @(ex_intro ?? (〈curc,false〉::rs)) @(ex_intro ?? l0) % - [ >Ht2 % - | >Hls >lift_tape_not_null - [ % - | @Hlsnonulls >Hls @memb_hd ] ] -qed. - -lemma Realize_to_Realize : - ∀alpha,M,R1,R2.(∀t1,t2.R1 t1 t2 → R2 t1 t2) → Realize alpha M R1 → Realize alpha M R2. -#alpha #M #R1 #R2 #Himpl #HR1 #intape -cases (HR1 intape) -HR1 #k * #outc * #Hloop #HR1 -@(ex_intro ?? k) @(ex_intro ?? outc) % /2/ -qed. + [ % + [ >Ht2 % + | >Hls >lift_tape_not_null + [ % + | @bit_not_null @(Hbits 〈l0,false〉) >Hls @memb_append_l1 @memb_hd ] ] + | % [ % [ % + [ #x #Hx cases (orb_true_l … Hx) #Hx' + [ >(\P Hx') % + | cases (memb_append … Hx') #Hx'' @Hnomarks + [ >Hls @memb_cons @memb_cons @(memb_append_l1 … Hx'') + | cases (orb_true_l … Hx'') #Hx''' + [ >(\P Hx''') @memb_hd + | @memb_cons @(memb_append_l2 … Hx''')] + ] + ] + | whd in ⊢ (?%); #x #Hx cases (memb_append … Hx) #Hx' + [ @Hbits >Hls @memb_cons @(memb_append_l1 … Hx') + | cases (orb_true_l … Hx') #Hx'' + [ >(\P Hx'') // + | @Hbits @(memb_append_l2 … Hx'') + ]]] + | whd in ⊢ (??%?); >(Hbits 〈l0,false〉) // + @memb_append_l1 >Hls @memb_hd ] + | % % % #Hl0 lapply (Hbits 〈l0,false〉?) + [ @memb_append_l1 >Hls @memb_hd + | >Hl0 normalize #Hfalse destruct (Hfalse) + ] ] ] +| #x #Hx @Hbits @memb_append_l1 @Hx ] +qed. lemma sem_move_tape_l_abstract : Realize … move_tape_l R_move_tape_l_abstract. @(Realize_to_Realize … mtl_concrete_to_abstract) // @@ -494,19 +684,21 @@ definition move_tape ≝ tc_true) tc_true. definition R_move_tape ≝ λt1,t2. - ∀rs,n,table1,c,table2,curc,curconfig,ls. - bit_or_null curc = true → bit_or_null c = true → only_bits_or_nulls curconfig → - table_TM n (reverse ? table1@〈c,false〉::table2) → + ∀rs,n,table1,mv,table2,curc,curconfig,ls. + bit_or_null mv = true → only_bits_or_nulls curconfig → + (is_bit mv = true → is_bit curc = true) → + table_TM n (reverse ? table1@〈mv,false〉::table2) → t1 = midtape STape (table1@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls) - 〈c,false〉 (table2@〈grid,false〉::rs) → - no_nulls ls → no_nulls rs → + 〈mv,false〉 (table2@〈grid,false〉::rs) → + legal_tape ls 〈curc,false〉 rs → ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs → ∃ls1,rs1,newc. - (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@newc:: - 〈grid,false〉::reverse ? table1@〈c,false〉::table2@〈grid,false〉::rs1) ∧ - ((c = bit false ∧ lift_tape ls1 newc rs1 = tape_move_left STape ls 〈curc,false〉 rs) ∨ - (c = bit true ∧ lift_tape ls1 newc rs1 = tape_move_right STape ls 〈curc,false〉 rs) ∨ - (c = null ∧ ls1 = ls ∧ rs1 = rs ∧ 〈curc,false〉 = newc))). + legal_tape ls1 〈newc,false〉 rs1 ∧ + (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉:: + 〈grid,false〉::reverse ? table1@〈mv,false〉::table2@〈grid,false〉::rs1) ∧ + ((mv = bit false ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_left STape ls 〈curc,false〉 rs) ∨ + (mv = bit true ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_right STape ls 〈curc,false〉 rs) ∨ + (mv = null ∧ ls1 = ls ∧ rs1 = rs ∧ curc = newc))). lemma sem_move_tape : Realize ? move_tape R_move_tape. #intape @@ -518,56 +710,69 @@ cases (sem_if ? (test_char ??) … tc_true (sem_test_char ? (λc:STape.c == 〈b (sem_seq … (sem_move_l …) (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c)))))) intape) #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop -#rs #n #table1 #c #table2 #curc #curconfig #ls -#Hcurc #Hc #Hcurconfig #Htable #Hintape #Hls #Hrs #t1' #Ht1' +#rs #n #table1 #mv #table2 #curc #curconfig #ls +#Hmv #Hcurconfig #Hmvcurc #Htable #Hintape #Htape #t1' #Ht1' generalize in match HR; -HR * -[ * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈c,false〉 ?) +[ * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈mv,false〉 ?) [| >Hintape % ] -Hta #Hceq #Hta lapply (\P Hceq) -Hceq #Hceq destruct (Hta Hceq) * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hintape) -Htb -Hintape [ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ] * #_ #Htb lapply (Htb … (refl ??) (refl ??) ?) [ @daemon ] -Htb >append_cons reverse_append >reverse_append >reverse_reverse @Htable |] - -Houtc -Htb * #ls1 * #rs1 * #newc * #Houtc #Hnewtape + [ >reverse_append >reverse_append >reverse_reverse @Htable + | /2/ + ||] + -Houtc -Htb * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) % - [ >Houtc >reverse_append >reverse_append >reverse_reverse - >associative_append >associative_append % - | % % % // ] -| * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈c,false〉 ?) - [| >Hintape % ] -Hta #Hcneq cut (c ≠ bit false) + [ // + | % + [ >Houtc >reverse_append >reverse_append >reverse_reverse + >associative_append >associative_append % + | % % % // ] + ] +| * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈mv,false〉 ?) + [| >Hintape % ] -Hta #Hcneq cut (mv ≠ bit false) [ lapply (\Pf Hcneq) @not_to_not #Heq >Heq % ] -Hcneq #Hcneq #Hta destruct (Hta) * - [ * #tb * whd in ⊢ (%→?);#Htb cases (Htb 〈c,false〉 ?) + [ * #tb * whd in ⊢ (%→?);#Htb cases (Htb 〈mv,false〉 ?) [| >Hintape % ] -Htb #Hceq #Htb lapply (\P Hceq) -Hceq #Hceq destruct (Htb Hceq) * #tc * whd in ⊢ (%→?); #Htc cases (Htc … Hintape) -Htc -Hintape [ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ] * #_ #Htc lapply (Htc … (refl ??) (refl ??) ?) [ @daemon ] -Htc >append_cons reverse_append >reverse_append >reverse_reverse @Htable |] - -Houtc -Htc * #ls1 * #rs1 * #newc * #Houtc #Hnewtape + [ >reverse_append >reverse_append >reverse_reverse @Htable + | /2/ |] + -Houtc -Htc * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) % - [ >Houtc >reverse_append >reverse_append >reverse_reverse - >associative_append >associative_append % - | % %2 % // ] - | * #tb * whd in ⊢ (%→?); #Htb cases (Htb 〈c,false〉 ?) - [| >Hintape % ] -Htb #Hcneq' cut (c ≠ bit true) + [ // + | % + [ >Houtc >reverse_append >reverse_append >reverse_reverse + >associative_append >associative_append % + | % %2 % // ] + ] + | * #tb * whd in ⊢ (%→?); #Htb cases (Htb 〈mv,false〉 ?) + [| >Hintape % ] -Htb #Hcneq' cut (mv ≠ bit true) [ lapply (\Pf Hcneq') @not_to_not #Heq >Heq % ] -Hcneq' #Hcneq' #Htb destruct (Htb) * #tc * whd in ⊢ (%→?); #Htc cases (Htc … Hintape) - [ * >(bit_or_null_not_grid … Hc) #Hfalse destruct (Hfalse) ] -Htc + [ * >(bit_or_null_not_grid … Hmv) #Hfalse destruct (Hfalse) ] -Htc * #_ #Htc lapply (Htc … (refl ??) (refl ??) ?) [@daemon] -Htc #Htc * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd -Htc whd in ⊢ (???%→?); #Htd whd in ⊢ (%→?); #Houtc lapply (Houtc … Htd) -Houtc * - [ * >(bit_or_null_not_grid … Hcurc) #Hfalse destruct (Hfalse) ] + [ * cases Htape * * #_ #_ #Hcurc #_ + >(bit_or_null_not_grid … Hcurc) #Hfalse destruct (Hfalse) ] * #_ #Houtc lapply (Houtc … (refl ??) (refl ??) ?) [@daemon] -Houtc #Houtc - @(ex_intro ?? ls) @(ex_intro ?? rs) @(ex_intro ?? 〈curc,false〉) % - [ @Houtc - | %2 % // % // % // - generalize in match Hcneq; generalize in match Hcneq'; - cases c in Hc; normalize // - [ * #_ normalize [ #Hfalse @False_ind cases Hfalse /2/ | #_ #Hfalse @False_ind cases Hfalse /2/ ] - |*: #Hfalse destruct (Hfalse) ] + @(ex_intro ?? ls) @(ex_intro ?? rs) @(ex_intro ?? curc) % + [ // + | % + [ @Houtc + | %2 % // % // % // + generalize in match Hcneq; generalize in match Hcneq'; + cases mv in Hmv; normalize // + [ * #_ normalize [ #Hfalse @False_ind cases Hfalse /2/ | #_ #Hfalse @False_ind cases Hfalse /2/ ] + |*: #Hfalse destruct (Hfalse) ] + ] ] ] ]