From 5c1794aba0652c0b0bce80a9ffc426192327709f Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Mon, 7 May 2012 15:34:16 +0000 Subject: [PATCH] progress --- matita/matita/lib/turing/mono.ma | 12 +++ .../lib/turing/universal/move_char_c.ma | 21 ++--- .../lib/turing/universal/move_char_l.ma | 84 ++++++++++++------- 3 files changed, 70 insertions(+), 47 deletions(-) diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma index a9092336d..5813606a1 100644 --- a/matita/matita/lib/turing/mono.ma +++ b/matita/matita/lib/turing/mono.ma @@ -156,6 +156,18 @@ let rec loop (A:Type[0]) n (f:A→A) p a on n ≝ | S m ⇒ if p a then (Some ? a) else loop A m f p (f a) ]. +lemma loop_S_true : + ∀A,n,f,p,a. p a = true → + loop A (S n) f p a = Some ? a. +#A #n #f #p #a #pa normalize >pa // +qed. + +lemma loop_S_false : + ∀A,n,f,p,a. p a = false → + loop A (S n) f p a = loop A n f p (f a). +normalize #A #n #f #p #a #Hpa >Hpa % +qed. + lemma loop_incr : ∀A,f,p,k1,k2,a1,a2. loop A k1 f p a1 = Some ? a2 → loop A (k2+k1) f p a1 = Some ? a2. diff --git a/matita/matita/lib/turing/universal/move_char_c.ma b/matita/matita/lib/turing/universal/move_char_c.ma index 6bd3cef9b..f970da13e 100644 --- a/matita/matita/lib/turing/universal/move_char_c.ma +++ b/matita/matita/lib/turing/universal/move_char_c.ma @@ -107,24 +107,13 @@ definition Rmcc_step_false ≝ left ? t1 ≠ [] → current alpha t1 ≠ None alpha → current alpha t1 = Some alpha sep ∧ t2 = t1. -lemma loop_S_true : - ∀A,n,f,p,a. p a = true → - loop A (S n) f p a = Some ? a. /2/ -qed. - -lemma loop_S_false : - ∀A,n,f,p,a. p a = false → - loop A (S n) f p a = loop A n f p (f a). -normalize #A #n #f #p #a #Hpa >Hpa % -qed. - -lemma trans_init_sep: +lemma mcc_trans_init_sep: ∀alpha,sep,x. trans ? (mcc_step alpha sep) 〈〈0,x〉,Some ? sep〉 = 〈〈4,sep〉,None ?〉. #alpha #sep #x normalize >(\b ?) // qed. -lemma trans_init_not_sep: +lemma mcc_trans_init_not_sep: ∀alpha,sep,x,y.y == sep = false → trans ? (mcc_step alpha sep) 〈〈0,x〉,Some ? y〉 = 〈〈1,y〉,Some ? 〈y,L〉〉. #alpha #sep #x #y #H1 normalize >H1 // @@ -149,8 +138,8 @@ lemma sem_mcc_step : @(ex_intro ?? (mk_config ?? 〈4,sep〉 (midtape ? lt c rt))) % [ % [ >(\P Hc) >loop_S_false // >loop_S_true - [ @eq_f whd in ⊢ (??%?); >trans_init_sep % - |>(\P Hc) whd in ⊢(??(???(???%))?); >trans_init_sep % ] + [ @eq_f whd in ⊢ (??%?); >mcc_trans_init_sep % + |>(\P Hc) whd in ⊢(??(???(???%))?); >mcc_trans_init_sep % ] | #Hfalse destruct ] |#_ #H1 #H2 % // normalize >(\P Hc) % ] | @(ex_intro ?? 4) cases lt @@ -185,7 +174,7 @@ definition R_move_char_c ≝ b ≠ sep → memb ? sep rs1 = false → t2 = midtape alpha (a::reverse ? rs1@b::ls) sep rs2). -lemma sem_while_move_char : +lemma sem_move_char_c : ∀alpha,sep. WRealize alpha (move_char_c alpha sep) (R_move_char_c alpha sep). #alpha #sep #inc #i #outc #Hloop diff --git a/matita/matita/lib/turing/universal/move_char_l.ma b/matita/matita/lib/turing/universal/move_char_l.ma index 8b97dee55..a35d714d8 100644 --- a/matita/matita/lib/turing/universal/move_char_l.ma +++ b/matita/matita/lib/turing/universal/move_char_l.ma @@ -86,7 +86,7 @@ lemma mcl_q1_q2 : #alpha #sep #a #ls #a0 * // qed. -lemma mcc_q2_q3 : +lemma mcl_q2_q3 : ∀alpha:FinSet.∀sep,a,ls,a0,rs. step alpha (mcl_step alpha sep) (mk_config ?? 〈2,a〉 (mk_tape … ls (Some ? a0) rs)) = @@ -119,9 +119,6 @@ lemma mcl_trans_init_not_sep: #alpha #sep #x #y #H1 normalize >H1 // qed. -(* -STOP - lemma sem_mcl_step : ∀alpha,sep. accRealize alpha (mcl_step alpha sep) @@ -131,32 +128,32 @@ lemma sem_mcl_step : @(ex_intro … (mk_config ?? 〈4,sep〉 (niltape ?))) % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 @False_ind @(absurd ?? H2) %] |#l0 #lt0 @(ex_intro ?? 2) - @(ex_intro … (mk_config ?? 〈4,sep〉 (rightof ? l0 lt0))) - % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 @False_ind @(absurd ?? H2) %] + @(ex_intro … (mk_config ?? 〈4,sep〉 (leftof ? l0 lt0))) + % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 #H3 @False_ind @(absurd ?? H3) %] |#r0 #rt0 @(ex_intro ?? 2) - @(ex_intro … (mk_config ?? 〈4,sep〉 (leftof ? r0 rt0))) + @(ex_intro … (mk_config ?? 〈4,sep〉 (rightof ? r0 rt0))) % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 #H3 @False_ind @(absurd ?? H3) %] | #lt #c #rt cases (true_or_false (c == sep)) #Hc [ @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 〈4,sep〉 (midtape ? lt c rt))) % [ % [ >(\P Hc) >loop_S_false // >loop_S_true - [ @eq_f whd in ⊢ (??%?); >trans_init_sep % - |>(\P Hc) whd in ⊢(??(???(???%))?); >trans_init_sep % ] + [ @eq_f whd in ⊢ (??%?); >mcl_trans_init_sep % + |>(\P Hc) whd in ⊢(??(???(???%))?); >mcl_trans_init_sep % ] | #Hfalse destruct ] |#_ #H1 #H2 % // normalize >(\P Hc) % ] - | @(ex_intro ?? 4) cases lt + | @(ex_intro ?? 4) cases rt [ @ex_intro [|% [ % [ >loop_S_false // >mcc_q0_q1 // | normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ] | normalize in ⊢ (%→?); #_ #H1 @False_ind @(absurd ?? H1) % ] ] - | #l0 #lt @ex_intro + | #r0 #rt0 @ex_intro [| % [ % [ >loop_S_false // >mcc_q0_q1 // - | #_ #a #b #ls #rs #Hb destruct % + | #_ #a #b #ls #rs #Hb destruct (Hb) % [ @(\Pf Hc) - | >mcc_q1_q2 >mcc_q2_q3 cases rs normalize // ] ] + | >mcl_q1_q2 >mcl_q2_q3 cases ls normalize // ] ] | normalize in ⊢ (% → ?); * #Hfalse @False_ind /2/ ] ] @@ -166,22 +163,22 @@ lemma sem_mcl_step : qed. (* the move_char (variant c) machine *) -definition move_char_c ≝ - λalpha,sep.whileTM alpha (mcc_step alpha sep) 〈3,sep〉. +definition move_char_l ≝ + λalpha,sep.whileTM alpha (mcl_step alpha sep) 〈3,sep〉. -definition R_move_char_c ≝ +definition R_move_char_l ≝ λalpha,sep,t1,t2. - ∀b,a,ls,rs. t1 = midtape alpha (a::ls) b rs → + ∀b,a,ls,rs. t1 = midtape alpha ls b (a::rs) → (b = sep → t2 = t1) ∧ - (∀rs1,rs2.rs = rs1@sep::rs2 → - b ≠ sep → memb ? sep rs1 = false → - t2 = midtape alpha (a::reverse ? rs1@b::ls) sep rs2). + (∀ls1,ls2.ls = ls1@sep::ls2 → + b ≠ sep → memb ? sep ls1 = false → + t2 = midtape alpha ls2 sep (a::reverse ? ls1@b::rs)). -lemma sem_while_move_char : +lemma sem_move_char_l : ∀alpha,sep. - WRealize alpha (move_char_c alpha sep) (R_move_char_c alpha sep). + WRealize alpha (move_char_l alpha sep) (R_move_char_l alpha sep). #alpha #sep #inc #i #outc #Hloop -lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%] +lapply (sem_while … (sem_mcl_step alpha sep) inc i outc Hloop) [%] -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar) [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea % @@ -201,24 +198,49 @@ lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%] #Ha0 #Htapeb % [ #Hfalse @False_ind @(absurd ?? Ha0) // | * - [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ normalize - >Hrs in Htapeb; normalize #Htapeb + [ #ls2 whd in ⊢ (???%→?); #Hls #_ #_ normalize + >Hls in Htapeb; normalize #Htapeb cases (IH … Htapeb) #Houtc #_ >Houtc // - | #r0 #rs0 #rs2 #Hrs #_ #Hrs0 - cut (r0 ≠ sep ∧ memb … sep rs0 = false) + | #l0 #ls0 #ls2 #Hls #_ #Hls0 + cut (l0 ≠ sep ∧ memb … sep ls0 = false) [ % - [ % #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct - | whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse + [ % #Hl0 >Hl0 in Hls0; >memb_hd #Hfalse destruct + | whd in Hls0:(??%?); cases (sep==l0) in Hls0; normalize #Hfalse [ destruct | @Hfalse ] ] ] * - #Hr0 -Hrs0 #Hrs0 >Hrs in Htapeb; + #Hl0 -Hls0 #Hls0 >Hls in Htapeb; normalize in ⊢ (%→?); #Htapeb cases (IH … Htapeb) -IH #_ #IH >reverse_cons >associative_append @IH // ] ] qed. -*) \ No newline at end of file + +lemma terminate_move_char_l : + ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha ls b (a::rs) → + (b = sep ∨ memb ? sep ls = true) → Terminate alpha (move_char_l alpha sep) t. +#alpha #sep #t #b #a #ls #rs #Ht #Hsep +@(terminate_while … (sem_mcl_step alpha sep)) + [% + |generalize in match Hsep; -Hsep + generalize in match Ht; -Ht + generalize in match rs; -rs + generalize in match a; -a + generalize in match b; -b + generalize in match t; -t + elim ls + [#t #b #a #rs #Ht #Hsep % #tinit + whd in ⊢ (%→?); #H @False_ind + cases (H … Ht) #Hb #_ cases Hb #eqb @eqb + cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct + |#l0 #ls0 #Hind #t #b #a #rs #Ht #Hsep % #tinit + whd in ⊢ (%→?); #H + cases (H … Ht) #Hbsep #Htinit + @(Hind … Htinit) cases Hsep + [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb) + [#eqsep %1 >(\P eqsep) // | #H %2 //] + ] +qed. \ No newline at end of file -- 2.39.2