From bc02962ed23518a09e7f4ed875d7d967a33de135 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 6 Jun 2012 15:34:08 +0000 Subject: [PATCH] More conjectures proved. --- matita/matita/lib/turing/basic_machines.ma | 44 +++ .../lib/turing/universal/move_char_c.ma | 157 ++------- .../lib/turing/universal/move_char_l.ma | 19 +- .../matita/lib/turing/universal/move_tape.ma | 303 +++++++++++------- 4 files changed, 272 insertions(+), 251 deletions(-) diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma index 1d873ee86..796992e22 100644 --- a/matita/matita/lib/turing/basic_machines.ma +++ b/matita/matita/lib/turing/basic_machines.ma @@ -237,3 +237,47 @@ lemma sem_swap : ∀alpha,foo. ] ] qed. + +definition swap_r ≝ + λalpha:FinSet.λfoo:alpha. + mk_TM alpha (swap_states alpha) + (λp.let 〈q,a〉 ≝ p in + let 〈q',b〉 ≝ q in + let q' ≝ pi1 nat (λi.i<4) q' in (* perche' devo passare il predicato ??? *) + match a with + [ None ⇒ 〈〈swap3,foo〉,None ?〉 (* if tape is empty then stop *) + | Some a' ⇒ + match q' with + [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? 〈a',L〉〉 (* save in register and move L *) + | S q' ⇒ match q' with + [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? 〈b,R〉〉 (* swap with register and move R *) + | S q' ⇒ match q' with + [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? 〈b,N〉〉 (* copy from register and stay *) + | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?〉 (* final state *) + ] + ] + ]]) + 〈swap0,foo〉 + (λq.\fst q == swap3). + +definition Rswap_r ≝ + λalpha,t1,t2. + ∀a,b,ls,rs. + t1 = midtape alpha (a::ls) b rs → + t2 = midtape alpha (b::ls) a rs. + +lemma sem_swap_r : ∀alpha,foo. + swap_r alpha foo ⊨ Rswap_r alpha. +#alpha #foo * + [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?))) + % [% |#a #b #ls #rs #H destruct] + |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0))) + % [% |#a #b #ls #rs #H destruct] + |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0))) + % [% |#a #b #ls #rs #H destruct] + | #lt #c #rt @(ex_intro ?? 4) cases lt + [@ex_intro [|% [ % | #a #b #ls #rs #H destruct]] + |#l0 #lt0 @ex_intro [| % [ % | #a #b #ls #rs #H destruct // + ] + ] +qed. \ No newline at end of file diff --git a/matita/matita/lib/turing/universal/move_char_c.ma b/matita/matita/lib/turing/universal/move_char_c.ma index 4d2490ee0..6e601ad2b 100644 --- a/matita/matita/lib/turing/universal/move_char_c.ma +++ b/matita/matita/lib/turing/universal/move_char_c.ma @@ -31,76 +31,12 @@ Final state = 〈4,#〉 *) -include "turing/while_machine.ma". - -definition mcc_states : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 5) alpha. - -definition mcc0 : initN 5 ≝ mk_Sig ?? 0 (leb_true_to_le 1 5 (refl …)). -definition mcc1 : initN 5 ≝ mk_Sig ?? 1 (leb_true_to_le 2 5 (refl …)). -definition mcc2 : initN 5 ≝ mk_Sig ?? 2 (leb_true_to_le 3 5 (refl …)). -definition mcc3 : initN 5 ≝ mk_Sig ?? 3 (leb_true_to_le 4 5 (refl …)). -definition mcc4 : initN 5 ≝ mk_Sig ?? 4 (leb_true_to_le 5 5 (refl …)). - -definition mcc_step ≝ - λalpha:FinSet.λsep:alpha. - mk_TM alpha (mcc_states alpha) - (λp.let 〈q,a〉 ≝ p in - let 〈q',b〉 ≝ q in - let q' ≝ pi1 nat (λi.i<5) q' in (* perche' devo passare il predicato ??? *) - match a with - [ None ⇒ 〈〈mcc4,sep〉,None ?〉 - | Some a' ⇒ - match q' with - [ O ⇒ (* qinit *) - match a' == sep with - [ true ⇒ 〈〈mcc4,sep〉,None ?〉 - | false ⇒ 〈〈mcc1,a'〉,Some ? 〈a',L〉〉 ] - | S q' ⇒ match q' with - [ O ⇒ (* q1 *) - 〈〈mcc2,a'〉,Some ? 〈b,R〉〉 - | S q' ⇒ match q' with - [ O ⇒ (* q2 *) - 〈〈mcc3,sep〉,Some ? 〈b,R〉〉 - | S q' ⇒ match q' with - [ O ⇒ (* qacc *) - 〈〈mcc3,sep〉,None ?〉 - | S q' ⇒ (* qfail *) - 〈〈mcc4,sep〉,None ?〉 ] ] ] ] ]) - 〈mcc0,sep〉 - (λq.let 〈q',a〉 ≝ q in q' == mcc3 ∨ q' == mcc4). - -lemma mcc_q0_q1 : - ∀alpha:FinSet.∀sep,a,ls,a0,rs. - a0 == sep = false → - step alpha (mcc_step alpha sep) - (mk_config ?? 〈mcc0,a〉 (mk_tape … ls (Some ? a0) rs)) = - mk_config alpha (states ? (mcc_step alpha sep)) 〈mcc1,a0〉 - (tape_move_left alpha ls a0 rs). -#alpha #sep #a * -[ #a0 #rs #Ha0 whd in ⊢ (??%?); - normalize in match (trans ???); >Ha0 % -| #a1 #ls #a0 #rs #Ha0 whd in ⊢ (??%?); - normalize in match (trans ???); >Ha0 % -] -qed. - -lemma mcc_q1_q2 : - ∀alpha:FinSet.∀sep,a,ls,a0,rs. - step alpha (mcc_step alpha sep) - (mk_config ?? 〈mcc1,a〉 (mk_tape … ls (Some ? a0) rs)) = - mk_config alpha (states ? (mcc_step alpha sep)) 〈mcc2,a0〉 - (tape_move_right alpha ls a rs). -#alpha #sep #a #ls #a0 * // -qed. +include "turing/basic_machines.ma". +include "turing/if_machine.ma". -lemma mcc_q2_q3 : - ∀alpha:FinSet.∀sep,a,ls,a0,rs. - step alpha (mcc_step alpha sep) - (mk_config ?? 〈mcc2,a〉 (mk_tape … ls (Some ? a0) rs)) = - mk_config alpha (states ? (mcc_step alpha sep)) 〈mcc3,sep〉 - (tape_move_right alpha ls a rs). -#alpha #sep #a #ls #a0 * // -qed. +definition mcc_step ≝ λalpha:FinSet.λsep:alpha. + ifTM alpha (test_char ? (λc.¬c==sep)) + (single_finalTM … (seq … (swap_r alpha sep) (move_r ?))) (nop ?) tc_true. definition Rmcc_step_true ≝ λalpha,sep,t1,t2. @@ -114,70 +50,31 @@ definition Rmcc_step_false ≝ left ? t1 ≠ [] → current alpha t1 ≠ None alpha → current alpha t1 = Some alpha sep ∧ t2 = t1. -lemma mcc_trans_init_sep: - ∀alpha,sep,x. - trans ? (mcc_step alpha sep) 〈〈mcc0,x〉,Some ? sep〉 = 〈〈mcc4,sep〉,None ?〉. -#alpha #sep #x normalize >(\b ?) // -qed. - -lemma mcc_trans_init_not_sep: - ∀alpha,sep,x,y.y == sep = false → - trans ? (mcc_step alpha sep) 〈〈mcc0,x〉,Some ? y〉 = 〈〈mcc1,y〉,Some ? 〈y,L〉〉. -#alpha #sep #x #y #H1 normalize >H1 // -qed. - lemma sem_mcc_step : ∀alpha,sep. - accRealize alpha (mcc_step alpha sep) - 〈mcc3,sep〉 (Rmcc_step_true alpha sep) (Rmcc_step_false alpha sep). + mcc_step alpha sep ⊨ + [inr … (inl … (inr … start_nop)): Rmcc_step_true alpha sep, Rmcc_step_false alpha sep]. #alpha #sep -cut (∀P:Prop.〈mcc4,sep〉=〈mcc3,sep〉→P) - [#P whd in ⊢ ((??(???%?)(???%?))→?); #Hfalse destruct] #Hfalse -* -[@(ex_intro ?? 2) - @(ex_intro … (mk_config ?? 〈mcc4,sep〉 (niltape ?))) % - [% [whd in ⊢ (??%?); % | @Hfalse] - |#H1 #H2 @False_ind @(absurd ?? H2) %] -|#l0 #lt0 @(ex_intro ?? 2) - @(ex_intro … (mk_config ?? 〈mcc4,sep〉 (leftof ? l0 lt0)))% - [% [whd in ⊢ (??%?);% |@Hfalse] - |#H1 #H2 @False_ind @(absurd ?? H2) %] -|#r0 #rt0 @(ex_intro ?? 2) - @(ex_intro … (mk_config ?? 〈mcc4,sep〉 (rightof ? r0 rt0))) % - [% [whd in ⊢ (??%?);% |@Hfalse] - |#H1 #H2 #H3 @False_ind @(absurd ?? H3) %] -| #lt #c #rt cases (true_or_false (c == sep)) #Hc - [ @(ex_intro ?? 2) - @(ex_intro ?? (mk_config ?? 〈mcc4,sep〉 (midtape ? lt c rt))) - % [ % - [ >(\P Hc) >loop_S_false // >loop_S_true - [ @eq_f whd in ⊢ (??%?); >mcc_trans_init_sep % - |>(\P Hc) whd in ⊢(??(???(???%))?); >mcc_trans_init_sep % ] - |@Hfalse] - |#_ #H1 #H2 % // normalize >(\P Hc) % ] - | @(ex_intro ?? 4) cases lt - [ @ex_intro - [|% [ % - [ >loop_S_false // >mcc_q0_q1 // - | normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ] - | normalize in ⊢ (%→?); #_ #H1 @False_ind @(absurd ?? H1) % ] ] - | #l0 #lt @ex_intro - [| % [ % - [ >loop_S_false // >mcc_q0_q1 // - | #_ #a #b #ls #rs #Hb destruct % - [ @(\Pf Hc) - | >mcc_q1_q2 >mcc_q2_q3 cases rs normalize // ] ] - | normalize in ⊢ (% → ?); * #Hfalse - @False_ind /2/ ] - ] - ] - ] -] + @(acc_sem_if_app … + (sem_test_char …) (sem_seq …(sem_swap_r …) (sem_move_r …)) (sem_nop …)) + [#intape #outtape #tapea whd in ⊢ (%→%→%); + #Htapea * #tapeb * whd in ⊢ (%→%→?); + #Htapeb #Houttape #a #b #ls #rs #Hintape + >Hintape in Htapea; #Htapea cases (Htapea ? (refl …)) -Htapea + #Hbsep #Htapea % [@(\Pf (injective_notb ? false Hbsep))] + @Houttape @Htapeb // + |#intape #outtape #tapea whd in ⊢ (%→%→%); + cases (current alpha intape) + [#_ #_ #_ * #Hfalse @False_ind @Hfalse % + |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % // + lapply (injective_notb ? true csep) -csep #csep >(\P csep) // + ] + ] qed. (* the move_char (variant c) machine *) definition move_char_c ≝ - λalpha,sep.whileTM alpha (mcc_step alpha sep) 〈mcc3,sep〉. + λalpha,sep.whileTM alpha (mcc_step alpha sep) (inr … (inl … (inr … start_nop))). definition R_move_char_c ≝ λalpha,sep,t1,t2. @@ -252,4 +149,10 @@ lemma terminate_move_char_c : [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb) [#eqsep %1 >(\P eqsep) // | #H %2 //] ] -qed. \ No newline at end of file +qed. + +(* NO GOOD: we must stop if current = None too!!! *) + +axiom ssem_move_char_c : + ∀alpha,sep. + Realize alpha (move_char_c alpha sep) (R_move_char_c alpha sep). diff --git a/matita/matita/lib/turing/universal/move_char_l.ma b/matita/matita/lib/turing/universal/move_char_l.ma index ea9afc8d8..bed0ba596 100644 --- a/matita/matita/lib/turing/universal/move_char_l.ma +++ b/matita/matita/lib/turing/universal/move_char_l.ma @@ -73,9 +73,9 @@ lemma sem_mcl_step : ] qed. -(* the move_char (variant c) machine *) +(* the move_char (variant left) machine *) definition move_char_l ≝ - λalpha,sep.whileTM alpha (mcl_step alpha sep) 〈mcl3,sep〉. + λalpha,sep.whileTM alpha (mcl_step alpha sep) (inr … (inl … (inr … start_nop))). definition R_move_char_l ≝ λalpha,sep,t1,t2. @@ -150,4 +150,17 @@ lemma terminate_move_char_l : [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb) [#eqsep %1 >(\P eqsep) // | #H %2 //] ] -qed. \ No newline at end of file +qed. + +(* NO GOOD: we must stop if current = None too!!! +lemma ssem_move_char_l : + ∀alpha,sep. + Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep). +#alpha #sep * +[ %{5} % [| % [whd in ⊢ (??%?); + @WRealize_to_Realize // @terminate_move_char_l +*) + +axiom ssem_move_char_l : + ∀alpha,sep. + Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep). diff --git a/matita/matita/lib/turing/universal/move_tape.ma b/matita/matita/lib/turing/universal/move_tape.ma index cd8a87c5f..9ad227dbe 100644 --- a/matita/matita/lib/turing/universal/move_tape.ma +++ b/matita/matita/lib/turing/universal/move_tape.ma @@ -34,94 +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 swap0 : initN 4 ≝ mk_Sig ?? 0 (leb_true_to_le 1 4 (refl …)). -definition swap1 : initN 4 ≝ mk_Sig ?? 1 (leb_true_to_le 2 4 (refl …)). -definition swap2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)). -definition swap3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)). - -definition swap ≝ - λalpha:FinSet.λd:alpha. - mk_TM alpha (swap_states alpha) - (λp.let 〈q,a〉 ≝ p in - let 〈q',b〉 ≝ q in - let q' ≝ pi1 nat (λi.i<4) q' in (* perche' devo passare il predicato ??? *) - match a with - [ None ⇒ 〈〈swap3,d〉,None ?〉 - | Some a' ⇒ - match q' with - [ O ⇒ (* qinit *) - 〈〈swap1,a'〉,Some ? 〈a',R〉〉 - | S q' ⇒ match q' with - [ O ⇒ (* q1 *) - 〈〈swap2,a'〉,Some ? 〈b,L〉〉 - | S q' ⇒ match q' with - [ O ⇒ (* q2 *) - 〈〈swap3,d〉,Some ? 〈b,N〉〉 - | S _⇒ (* qacc *) - 〈〈swap3,d〉,None ?〉 ] ] ] ]) - 〈swap0,d〉 - (λq.let 〈q',a〉 ≝ q in q' == swap3). - -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: @@ -260,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 - ^ - 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 ^ - -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_c 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_c 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 = [] ∧ @@ -308,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_c 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_c 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: @@ -513,7 +573,7 @@ lemma mtl_concrete_to_abstract : #t1 #t2 whd in ⊢(%→?); #Hconcrete #rs #n #table #curc #curconfig #ls #Hcurc #Hcurconfig #Htable #Ht1 * * * #Hnomarks #Hbits #Hcurc #Hlegal #t1' #Ht1' -cases (Hconcrete … Htable Ht1) // +cases (Hconcrete … Htable ? Ht1) // [ * #Hls #Ht2 @(ex_intro ?? []) @(ex_intro ?? (〈curc,false〉::rs)) @@ -563,7 +623,8 @@ cases (Hconcrete … Htable Ht1) // | % % % #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 Realize_to_Realize : -- 2.39.2