From 08a53e81b883cc19ddec52a662e9c171656ec364 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Fri, 4 May 2012 15:09:54 +0000 Subject: [PATCH] Added a turing/universal directory for the universal turing machine (and auxiliary definitions). Added the definition of machine move_char (variant c) to be used in the universal machine. Small library refactoring. --- matita/matita/lib/basics/deqsets.ma | 4 + matita/matita/lib/basics/finset.ma | 4 + matita/matita/lib/basics/lists/list.ma | 5 + matita/matita/lib/basics/star.ma | 28 +++ matita/matita/lib/turing/mono.ma | 10 + matita/matita/lib/turing/while_machine.ma | 255 ---------------------- 6 files changed, 51 insertions(+), 255 deletions(-) diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma index 2d6434f65..e874eb8ff 100644 --- a/matita/matita/lib/basics/deqsets.ma +++ b/matita/matita/lib/basics/deqsets.ma @@ -28,6 +28,10 @@ notation "\P H" non associative with precedence 90 notation "\b H" non associative with precedence 90 for @{(proj2 … (eqb_true ???) $H)}. +notation < "𝐃" non associative with precedence 90 + for @{'bigD}. +interpretation "DeqSet" 'bigD = (mk_DeqSet ???). + lemma eqb_false: ∀S:DeqSet.∀a,b:S. (eqb ? a b) = false ↔ a ≠ b. #S #a #b % #H diff --git a/matita/matita/lib/basics/finset.ma b/matita/matita/lib/basics/finset.ma index 3efd26f3f..a8ee13a07 100644 --- a/matita/matita/lib/basics/finset.ma +++ b/matita/matita/lib/basics/finset.ma @@ -19,6 +19,10 @@ record FinSet : Type[1] ≝ enum_unique: uniqueb FinSetcarr enum = true }. +notation < "𝐅" non associative with precedence 90 + for @{'bigF}. +interpretation "FinSet" 'bigF = (mk_FinSet ???). + (* bool *) lemma bool_enum_unique: uniqueb ? [true;false] = true. // qed. diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma index ff7fcf80f..c89bb7856 100644 --- a/matita/matita/lib/basics/lists/list.ma +++ b/matita/matita/lib/basics/lists/list.ma @@ -55,6 +55,11 @@ definition hd ≝ λA.λl: list A.λd:A. definition tail ≝ λA.λl: list A. match l with [ nil ⇒ [] | cons hd tl ⇒ tl]. + +definition option_hd ≝ + λA.λl:list A. match l with + [ nil ⇒ None ? + | cons a _ ⇒ Some ? a ]. interpretation "append" 'append l1 l2 = (append ? l1 l2). diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma index 8fd32c2e1..09730b6f2 100644 --- a/matita/matita/lib/basics/star.ma +++ b/matita/matita/lib/basics/star.ma @@ -88,6 +88,34 @@ theorem star_inv: ∀A,R. #H (elim H) /2/ normalize #c #d #H1 #H2 #H3 @(trans_star … H3) /2/ qed. +lemma star_decomp_l : + ∀A,R,x,y.star A R x y → x = y ∨ ∃z.R x z ∧ star A R z y. +#A #R #x #y #Hstar elim Hstar +[ #b #c #Hleft #Hright * + [ #H1 %2 @(ex_intro ?? c) % // + | * #x0 * #H1 #H2 %2 @(ex_intro ?? x0) % /2/ ] +| /2/ ] +qed. + +axiom star_ind_l : + ∀A:Type[0].∀R:relation A.∀Q:A → A → Prop. + (∀a.Q a a) → + (∀a,b,c.R a b → star A R b c → Q b c → Q a c) → + ∀x,y.star A R x y → Q x y. +(* #A #R #Q #H1 #H2 #x #y #H0 elim H0 +[ #b #c #Hleft #Hright #IH + cases (star_decomp_l ???? Hleft) + [ #Hx @H2 // + | * #z * #H3 #H4 @(H2 … H3) /2/ +[ +| +generalize in match (λb.H2 x b y); elim H0 +[#b #c #Hleft #Hright #H2' #H3 @H3 + @(H3 b) + elim H0 +[ #b #c #Hleft #Hright #IH // +| *) + (* RC and star *) lemma TC_to_star: ∀A,R,a,b.TC A R a b → star A R a b. diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma index cd9598765..fae3c7673 100644 --- a/matita/matita/lib/turing/mono.ma +++ b/matita/matita/lib/turing/mono.ma @@ -44,6 +44,16 @@ definition current ≝ λsig.λt:tape sig.match t with [ midtape _ c _ ⇒ Some ? c | _ ⇒ None ? ]. + +definition mk_tape : + ∀sig:FinSet.list sig → option sig → list sig → tape sig ≝ + λsig,lt,c,rt.match c with + [ Some c' ⇒ midtape sig lt c' rt + | None ⇒ match lt with + [ nil ⇒ match rt with + [ nil ⇒ niltape ? + | cons r0 rs0 ⇒ leftof ? r0 rs0 ] + | cons l0 ls0 ⇒ rightof ? l0 ls0 ] ]. inductive move : Type[0] ≝ | L : move diff --git a/matita/matita/lib/turing/while_machine.ma b/matita/matita/lib/turing/while_machine.ma index 2323094b4..52a0a79b7 100644 --- a/matita/matita/lib/turing/while_machine.ma +++ b/matita/matita/lib/turing/while_machine.ma @@ -123,261 +123,6 @@ cases (loop_split ?? (λc. halt sig M (cstate ?? c)) ????? Hloop) ] qed. -(* inductive move_states : Type[0] ≝ -| start : move_states -| q1 : move_states -| q2 : move_states -| q3 : move_states -| qacc : move_states -| qfail : move_states. - -definition -*) - -definition mystates : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 5) alpha. - -definition move_char ≝ - λalpha:FinSet.λsep:alpha. - mk_TM alpha (mystates alpha) - (λp.let 〈q,a〉 ≝ p in - let 〈q',b〉 ≝ q in - match a with - [ None ⇒ 〈〈4,sep〉,None ?〉 - | Some a' ⇒ - match q' with - [ O ⇒ (* qinit *) - match a' == sep with - [ true ⇒ 〈〈4,sep〉,None ?〉 - | false ⇒ 〈〈1,a'〉,Some ? 〈a',L〉〉 ] - | S q' ⇒ match q' with - [ O ⇒ (* q1 *) - 〈〈2,a'〉,Some ? 〈b,R〉〉 - | S q' ⇒ match q' with - [ O ⇒ (* q2 *) - 〈〈3,sep〉,Some ? 〈b,R〉〉 - | S q' ⇒ match q' with - [ O ⇒ (* qacc *) - 〈〈3,sep〉,None ?〉 - | S q' ⇒ (* qfail *) - 〈〈4,sep〉,None ?〉 ] ] ] ] ]) - 〈0,sep〉 - (λq.let 〈q',a〉 ≝ q in q' == 3 ∨ q' == 4). - -definition mk_tape : - ∀sig:FinSet.list sig → option sig → list sig → tape sig ≝ - λsig,lt,c,rt.match c with - [ Some c' ⇒ midtape sig lt c' rt - | None ⇒ match lt with - [ nil ⇒ match rt with - [ nil ⇒ niltape ? - | cons r0 rs0 ⇒ leftof ? r0 rs0 ] - | cons l0 ls0 ⇒ rightof ? l0 ls0 ] ]. - -lemma cmove_q0_q1 : - ∀alpha:FinSet.∀sep,a,ls,a0,rs. - a0 == sep = false → - step alpha (move_char alpha sep) - (mk_config ?? 〈0,a〉 (mk_tape … ls (Some ? a0) rs)) = - mk_config alpha (states ? (move_char alpha sep)) 〈1,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 cmove_q1_q2 : - ∀alpha:FinSet.∀sep,a,ls,a0,rs. - step alpha (move_char alpha sep) - (mk_config ?? 〈1,a〉 (mk_tape … ls (Some ? a0) rs)) = - mk_config alpha (states ? (move_char alpha sep)) 〈2,a0〉 - (tape_move_right alpha ls a rs). -#alpha #sep #a #ls #a0 * // -qed. - -lemma cmove_q2_q3 : - ∀alpha:FinSet.∀sep,a,ls,a0,rs. - step alpha (move_char alpha sep) - (mk_config ?? 〈2,a〉 (mk_tape … ls (Some ? a0) rs)) = - mk_config alpha (states ? (move_char alpha sep)) 〈3,sep〉 - (tape_move_right alpha ls a rs). -#alpha #sep #a #ls #a0 * // -qed. - -definition option_hd ≝ - λA.λl:list A. match l with - [ nil ⇒ None ? - | cons a _ ⇒ Some ? a ]. - -definition Rmove_char_true ≝ - λalpha,sep,t1,t2. - ∀a,b,ls,rs. b ≠ sep → - t1 = midtape alpha (a::ls) b rs → - t2 = mk_tape alpha (a::b::ls) (option_hd ? rs) (tail ? rs). - -definition Rmove_char_false ≝ - λalpha,sep,t1,t2. - 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. - -notation < "𝐅" non associative with precedence 90 - for @{'bigF}. -notation < "𝐃" non associative with precedence 90 - for @{'bigD}. - -interpretation "FinSet" 'bigF = (mk_FinSet ???). -interpretation "DeqSet" 'bigD = (mk_DeqSet ???). - -lemma trans_init_sep: - ∀alpha,sep,x. - trans ? (move_char alpha sep) 〈〈0,x〉,Some ? sep〉 = 〈〈4,sep〉,None ?〉. -#alpha #sep #x normalize >(\b ?) // -qed. - -lemma trans_init_not_sep: - ∀alpha,sep,x,y.y == sep = false → - trans ? (move_char alpha sep) 〈〈0,x〉,Some ? y〉 = 〈〈1,y〉,Some ? 〈y,L〉〉. -#alpha #sep #x #y #H1 normalize >H1 // -qed. - -lemma sem_move_char : - ∀alpha,sep. - accRealize alpha (move_char alpha sep) - 〈3,sep〉 (Rmove_char_true alpha sep) (Rmove_char_false alpha sep). -#alpha #sep * -[@(ex_intro ?? 2) - @(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〉 (leftof ? l0 lt0))) - % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 @False_ind @(absurd ?? H2) %] -|#r0 #rt0 @(ex_intro ?? 2) - @(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 % ] - | #Hfalse destruct - ] - |#_ #H1 #H2 % // normalize >(\P Hc) % ] - | @(ex_intro ?? 4) - cases lt - [ @ex_intro - [|% - [ % - [ >loop_S_false // - >cmove_q0_q1 // - | normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) - ] - | normalize in ⊢ (%→?); #_ #H1 @False_ind @(absurd ?? H1) % - ] - ] - | #l0 #lt @ex_intro - [| % - [ % - [ >loop_S_false // - >cmove_q0_q1 // - | #_ #a #b #ls #rs #Hb #Htape - destruct (Htape) - >cmove_q1_q2 - >cmove_q2_q3 - cases rs normalize // - ] - | normalize in ⊢ (% → ?); * #Hfalse - @False_ind /2/ - ] - ] - ] - ] -] -qed. - -definition R_while_cmove ≝ - λalpha,sep,t1,t2. - ∀a,b,ls,rs,rs'. b ≠ sep → memb ? sep rs = false → - t1 = midtape alpha (a::ls) b (rs@sep::rs') → - t2 = midtape alpha (a::reverse ? rs@b::ls) sep rs'. - -lemma star_cases : - ∀A,R,x,y.star A R x y → x = y ∨ ∃z.R x z ∧ star A R z y. -#A #R #x #y #Hstar elim Hstar -[ #b #c #Hleft #Hright * - [ #H1 %2 @(ex_intro ?? c) % // - | * #x0 * #H1 #H2 %2 @(ex_intro ?? x0) % /2/ ] -| /2/ ] -qed. - -axiom star_ind_r : - ∀A:Type[0].∀R:relation A.∀Q:A → A → Prop. - (∀a.Q a a) → - (∀a,b,c.R a b → star A R b c → Q b c → Q a c) → - ∀x,y.star A R x y → Q x y. -(* #A #R #Q #H1 #H2 #x #y #H0 elim H0 -[ #b #c #Hleft #Hright #IH - cases (star_cases ???? Hleft) - [ #Hx @H2 // - | * #z * #H3 #H4 @(H2 … H3) /2/ -[ -| -generalize in match (λb.H2 x b y); elim H0 -[#b #c #Hleft #Hright #H2' #H3 @H3 - @(H3 b) - elim H0 -[ #b #c #Hleft #Hright #IH // -| *) - -lemma sem_move_char : - ∀alpha,sep. - WRealize alpha (whileTM alpha (move_char alpha sep) 〈3,sep〉) - (R_while_cmove alpha sep). -#alpha #sep #inc #i #outc #Hloop -lapply (sem_while … (sem_move_char alpha sep) inc i outc Hloop) [%] -* #t1 * #Hstar @(star_ind_r ??????? Hstar) -[ #a whd in ⊢ (% → ?); #H1 #a #b #ls #rs #rs' #Hb #Hrs #Hinc - >Hinc in H1; normalize in ⊢ (% → ?); #H1 - cases (H1 ??) - [ #Hfalse @False_ind @(absurd ?? Hb) destruct % - |% #H2 destruct (H2) - |% #H2 destruct ] -| #a #b #c #Hstar1 #HRtrue #IH #HRfalse - lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH - #a0 #b0 #ls #rs #rs' #Hb0 #Hrs #Ha - whd in Hstar1; - lapply (Hstar1 … Hb0 Ha) #Hb - @(IH … Hb0 Hrs) >Hb whd in HRfalse; - [ - inc Rtrue* b Rtrue c Rfalse outc - -| -] -qed. - - #H1 - #a #b #ls #rs #rs #Hb #Hrs #Hinc - >Hinc in H2;whd in ⊢ ((??%? → ?) → ?); - -lapply (H inc i outc Hloop) * - (* (* -- 2.39.2