From 67948c54e4e20ef530d2d2115c9a056275360012 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Thu, 17 May 2012 07:04:54 +0000 Subject: [PATCH] Added null character. --- .../matita/lib/turing/universal/alphabet.ma | 9 +++- matita/matita/lib/turing/universal/marks.ma | 47 ++++++++++++------- .../lib/turing/universal/move_char_l.ma | 9 ++-- matita/matita/lib/turing/universal/tuples.ma | 40 +++++++++------- .../matita/lib/turing/universal/universal.ma | 31 ++++++++---- 5 files changed, 88 insertions(+), 48 deletions(-) diff --git a/matita/matita/lib/turing/universal/alphabet.ma b/matita/matita/lib/turing/universal/alphabet.ma index 646d8ebbd..04701aeec 100644 --- a/matita/matita/lib/turing/universal/alphabet.ma +++ b/matita/matita/lib/turing/universal/alphabet.ma @@ -20,6 +20,7 @@ include "turing/universal/tests.ma". *) inductive unialpha : Type[0] ≝ | bit : bool → unialpha +| null : unialpha | comma : unialpha | bar : unialpha | grid : unialpha. @@ -27,6 +28,7 @@ inductive unialpha : Type[0] ≝ definition unialpha_eq ≝ λa1,a2.match a1 with [ bit x ⇒ match a2 with [ bit y ⇒ ¬ xorb x y | _ ⇒ false ] + | null ⇒ match a2 with [ null ⇒ true | _ ⇒ false ] | comma ⇒ match a2 with [ comma ⇒ true | _ ⇒ false ] | bar ⇒ match a2 with [ bar ⇒ true | _ ⇒ false ] | grid ⇒ match a2 with [ grid ⇒ true | _ ⇒ false ] ]. @@ -34,19 +36,22 @@ definition unialpha_eq ≝ definition DeqUnialpha ≝ mk_DeqSet unialpha unialpha_eq ?. * [ #x * [ #y cases x cases y normalize % // #Hfalse destruct | *: normalize % #Hfalse destruct ] - |*: * [1,5,9,13: #y ] normalize % #H1 destruct % ] + |*: * [1,6,11,16: #y ] normalize % #H1 destruct % ] qed. axiom unialpha_unique : uniqueb DeqUnialpha [bit true;bit false;comma;bar;grid] = true. definition FSUnialpha ≝ - mk_FinSet DeqUnialpha [bit true;bit false;comma;bar;grid] unialpha_unique. + mk_FinSet DeqUnialpha [bit true;bit false;null;comma;bar;grid] unialpha_unique. definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ]. +definition is_null ≝ λc.match c with [ null ⇒ true | _ ⇒ false ]. + definition is_grid ≝ λc.match c with [ grid ⇒ true | _ ⇒ false ]. definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ]. definition is_comma ≝ λc.match c with [ comma ⇒ true | _ ⇒ false ]. +definition bit_or_null ≝ λc.is_bit c ∨ is_null c. diff --git a/matita/matita/lib/turing/universal/marks.ma b/matita/matita/lib/turing/universal/marks.ma index 4b66e6af5..17992f95f 100644 --- a/matita/matita/lib/turing/universal/marks.ma +++ b/matita/matita/lib/turing/universal/marks.ma @@ -678,7 +678,8 @@ definition comp_step ≝ ifTM ? (test_char ? (is_marked ?)) (single_finalTM … (comp_step_subcase FSUnialpha 〈bit false,true〉 (comp_step_subcase FSUnialpha 〈bit true,true〉 - (clear_mark …)))) + (comp_step_subcase FSUnialpha 〈null,true〉 + (clear_mark …))))) (nop ?) tc_true. @@ -686,7 +687,7 @@ definition R_comp_step_true ≝ λt1,t2. ∀l0,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) l0 c rs → ∃c'. c = 〈c',true〉 ∧ - ((is_bit c' = true ∧ + ((bit_or_null c' = true ∧ ∀a,l1,c0,a0,l2. rs = 〈a,false〉::l1@〈c0,true〉::〈a0,false〉::l2 → (∀c.memb ? c l1 = true → is_marked ? c = false) → @@ -695,7 +696,7 @@ definition R_comp_step_true ≝ (c0 ≠ c' ∧ t2 = midtape (FinProd … FSUnialpha FinBool) (reverse ? l1@〈a,false〉::〈c',true〉::l0) 〈c0,false〉 (〈a0,false〉::l2))) ∨ - (is_bit c' = false ∧ t2 = midtape ? l0 〈c',false〉 rs)). + (bit_or_null c' = false ∧ t2 = midtape ? l0 〈c',false〉 rs)). definition R_comp_step_false ≝ λt1,t2. @@ -709,7 +710,8 @@ lemma sem_comp_step : cases (acc_sem_if … (sem_test_char ? (is_marked ?)) (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ?? (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ?? - (sem_clear_mark …))) + (sem_comp_step_subcase FSUnialpha 〈null,true〉 ?? + (sem_clear_mark …)))) (sem_nop …) intape) #k * #outc * * #Hloop #H1 #H2 @(ex_intro ?? k) @(ex_intro ?? outc) % @@ -737,13 +739,24 @@ cases (acc_sem_if … (sem_test_char ? (is_marked ?)) [ @sym_not_eq // | @Houtc ] ] - | * #Hc' whd in ⊢ (%→?); #Helse2 %2 % - [ generalize in match Hc'; generalize in match Hc; - cases c' - [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) % - | #Hfalse @False_ind @(absurd ?? Hfalse) % ] - |*: #_ #_ % ] - | @(Helse2 … Hta) + | * #Hc' #Helse2 cases (Helse2 … Hta) + [ * #Hc'' #H1 % % [destruct (Hc'') % ] + #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1 + cases (H1 … Hl1 Hrs) + [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc + | * #Hneq #Houtc %2 % + [ @sym_not_eq // + | @Houtc ] + ] + | * #Hc'' whd in ⊢ (%→?); #Helse3 %2 % + [ generalize in match Hc''; generalize in match Hc'; generalize in match Hc; + cases c' + [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) % + | #Hfalse @False_ind @(absurd ?? Hfalse) % ] + | #_ #_ #Hfalse @False_ind @(absurd ?? Hfalse) % + |*: #_ #_ #_ % ] + | @(Helse3 … Hta) + ] ] ] ] @@ -807,16 +820,16 @@ RIFIUTO: c ≠ d definition R_compare := λt1,t2. ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs → - (∀c'.is_bit c' = false → c = 〈c',true〉 → t2 = midtape ? ls 〈c',false〉 rs) ∧ + (∀c'.bit_or_null c' = false → c = 〈c',true〉 → t2 = midtape ? ls 〈c',false〉 rs) ∧ (∀c'. c = 〈c',false〉 → t2 = t1) ∧ ∀b,b0,bs,b0s,l1,l2. |bs| = |b0s| → - (∀c.memb (FinProd … FSUnialpha FinBool) c bs = true → is_bit (\fst c) = true) → - (∀c.memb (FinProd … FSUnialpha FinBool) c b0s = true → is_bit (\fst c) = true) → + (∀c.memb (FinProd … FSUnialpha FinBool) c bs = true → bit_or_null (\fst c) = true) → + (∀c.memb (FinProd … FSUnialpha FinBool) c b0s = true → bit_or_null (\fst c) = true) → (∀c.memb ? c bs = true → is_marked ? c = false) → (∀c.memb ? c b0s = true → is_marked ? c = false) → (∀c.memb ? c l1 = true → is_marked ? c = false) → - c = 〈b,true〉 → is_bit b = true → + c = 〈b,true〉 → bit_or_null b = true → rs = bs@〈grid,false〉::l1@〈b0,true〉::b0s@〈comma,false〉::l2 → (〈b,true〉::bs = 〈b0,true〉::b0s ∧ t2 = midtape ? (reverse ? bs@〈b,false〉::ls) @@ -873,7 +886,7 @@ lapply (sem_while ?????? sem_comp_step t i outc Hloop) [%] ] | #tapea #tapeb #tapec #Hleft #Hright #IH #Htapec lapply (IH Htapec) -Htapec -IH #IH whd in Hleft; #ls #c #rs #Htapea cases (Hleft … Htapea) -Hleft - #c' * #Hc >Hc cases (true_or_false (is_bit c')) #Hc' + #c' * #Hc >Hc cases (true_or_false (bit_or_null c')) #Hc' [2: * [ * >Hc' #H @False_ind destruct (H) | * #_ #Htapeb cases (IH … Htapeb) * #_ #H #_ % @@ -912,7 +925,7 @@ lapply (sem_while ?????? sem_comp_step t i outc Hloop) [%] | @Hl1 ] | * #b' #bitb' * #b0' #bitb0' #bs' #b0s' #Hbs #Hb0s generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?); - cut (is_bit b' = true ∧ is_bit b0' = true ∧ + cut (bit_or_null b' = true ∧ bit_or_null b0' = true ∧ bitb' = false ∧ bitb0' = false) [ % [ % [ % [ >Hbs in Hbs1; #Hbs1 @(Hbs1 〈b',bitb'〉) @memb_hd | >Hb0s in Hb0s1; #Hb0s1 @(Hb0s1 〈b0',bitb0'〉) @memb_hd ] diff --git a/matita/matita/lib/turing/universal/move_char_l.ma b/matita/matita/lib/turing/universal/move_char_l.ma index a35d714d8..57ba67bdc 100644 --- a/matita/matita/lib/turing/universal/move_char_l.ma +++ b/matita/matita/lib/turing/universal/move_char_l.ma @@ -62,7 +62,7 @@ definition mcl_step ≝ 〈0,sep〉 (λq.let 〈q',a〉 ≝ q in q' == 3 ∨ q' == 4). -lemma mcc_q0_q1 : +lemma mcl_q0_q1 : ∀alpha:FinSet.∀sep,a,ls,a0,rs. a0 == sep = false → step alpha (mcl_step alpha sep) @@ -145,12 +145,13 @@ lemma sem_mcl_step : | @(ex_intro ?? 4) cases rt [ @ex_intro [|% [ % - [ >loop_S_false // >mcc_q0_q1 // + [ >loop_S_false // >mcl_q0_q1 // | normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ] | normalize in ⊢ (%→?); #_ #H1 @False_ind @(absurd ?? H1) % ] ] - | #r0 #rt0 @ex_intro + + | #r0 #rt0 @ex_intro [| % [ % - [ >loop_S_false // >mcc_q0_q1 // + [ >loop_S_false // >mcl_q0_q1 // | #_ #a #b #ls #rs #Hb destruct (Hb) % [ @(\Pf Hc) | >mcl_q1_q2 >mcl_q2_q3 cases ls normalize // ] ] diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma index 21679f885..3b1e9a393 100644 --- a/matita/matita/lib/turing/universal/tuples.ma +++ b/matita/matita/lib/turing/universal/tuples.ma @@ -18,8 +18,8 @@ include "turing/universal/marks.ma". definition STape ≝ FinProd … FSUnialpha FinBool. -definition only_bits ≝ λl. - ∀c.memb STape c l = true → is_bit (\fst c) = true. +definition only_bits_or_nulls ≝ λl. + ∀c.memb STape c l = true → bit_or_null (\fst c) = true. definition no_grids ≝ λl. ∀c.memb STape c l = true → is_grid (\fst c) = false. @@ -34,17 +34,25 @@ lemma bit_not_grid: ∀d. is_bit d = true → is_grid d = false. * // normalize #H destruct qed. +lemma bit_or_null_not_grid: ∀d. bit_or_null d = true → is_grid d = false. +* // normalize #H destruct +qed. + lemma bit_not_bar: ∀d. is_bit d = true → is_bar d = false. * // normalize #H destruct qed. +lemma bit_or_null_not_bar: ∀d. bit_or_null d = true → is_bar d = false. +* // normalize #H destruct +qed. + (* by definition, a tuple is not marked *) definition tuple_TM : nat → list STape → Prop ≝ λn,t.∃qin,qout,mv. no_marks t ∧ - only_bits qin ∧ only_bits qout ∧ only_bits mv ∧ + only_bits_or_nulls qin ∧ only_bits_or_nulls qout ∧ bit_or_null mv = true ∧ |qin| = n ∧ |qout| = n (* ∧ |mv| = ? *) ∧ - t = qin@〈comma,false〉::qout@〈comma,false〉::mv. + t = qin@〈comma,false〉::qout@〈comma,false〉::[〈mv,false〉]. inductive table_TM : nat → list STape → Prop ≝ | ttm_nil : ∀n.table_TM n [] @@ -58,14 +66,14 @@ lemma no_grids_in_table: ∀n.∀l.table_TM n l → no_grids l. whd >Heq #x #membx cases (memb_append … membx) -membx #membx [cases (memb_append … membx) -membx #membx - [@bit_not_grid @Hqin // + [@bit_or_null_not_grid @Hqin // |cases (orb_true_l … membx) -membx #membx [>(\P membx) // |cases (memb_append … membx) -membx #membx - [@bit_not_grid @Hqout // + [@bit_or_null_not_grid @Hqout // |cases (orb_true_l … membx) -membx #membx [>(\P membx) // - |@bit_not_grid @Hmv // + |@bit_or_null_not_grid >(memb_single … membx) @Hmv ] ] ] @@ -271,8 +279,8 @@ definition match_tuple_step ≝ definition R_match_tuple_step_true ≝ λt1,t2. ∀ls,c,l1,l2,c1,l3,l4,rs,n. - is_bit c = true → only_bits l1 → no_marks l1 (* → no_grids l2 *) → is_bit c1 = true → - only_bits l3 → n = |l1| → |l1| = |l3| → + bit_or_null c = true → only_bits_or_nulls l1 → no_marks l1 (* → no_grids l2 *) → bit_or_null c1 = true → + only_bits_or_nulls l3 → n = |l1| → |l1| = |l3| → table_TM (S n) (l2@〈bar,false〉::〈c1,false〉::l3@〈comma,false〉::l4) → t1 = midtape STape (〈grid,false〉::ls) 〈c,true〉 (l1@〈grid,false〉::l2@〈bar,false〉::〈c1,true〉::l3@〈comma,false〉::l4@〈grid,false〉::rs) → @@ -355,7 +363,7 @@ lemma sem_match_tuple_step: |#x #tl @not_to_not normalize #H destruct // ] ] #Hnoteq %2 - cut (is_bit d' = true) + cut (bit_or_null d' = true) [cases la in H3; [normalize in ⊢ (%→?); #H destruct // |#x #tl #H @(Hl3 〈d',false〉) @@ -364,7 +372,7 @@ lemma sem_match_tuple_step: ] #Hd' >Htapec in Hor; -Htapec * [* #taped * whd in ⊢ (%→?); #H @False_ind - cases (H … (refl …)) >(bit_not_grid ? Hd') #Htemp destruct (Htemp) + cases (H … (refl …)) >(bit_or_null_not_grid ? Hd') #Htemp destruct (Htemp) |* #taped * whd in ⊢ (%→?); #H cases (H … (refl …)) -H #_ #Htaped * #tapee * whd in ⊢ (%→?); #Htapee <(associative_append ? lc (〈comma,false〉::l4)) in Htaped; #Htaped @@ -417,12 +425,12 @@ lemma sem_match_tuple_step: [normalize in ⊢ (%→?); #Htemp destruct (Htemp) @injective_notb @notgridc |#x #tl normalize in ⊢ (%→?); #Htemp destruct (Htemp) - @bit_not_grid @(Hl1bars 〈c',false〉) @memb_append_l2 @memb_hd + @bit_or_null_not_grid @(Hl1bars 〈c',false〉) @memb_append_l2 @memb_hd ] - |cut (only_bits (la@(〈c',false〉::lb))) + |cut (only_bits_or_nulls (la@(〈c',false〉::lb))) [

(\P eqc0) @Hc |@Hl1bars] - |#Hl1' #x #Hx @bit_not_grid @Hl1' + |#Hl1' #x #Hx @bit_or_null_not_grid @Hl1' @memb_append_l1 @daemon ] |@daemon @@ -509,7 +517,7 @@ lemma sem_match_tuple_step: @memb_append_l2 @memb_cons cut (∀A,l1,l2.∀a:A. a::l1@l2=(a::l1)@l2) [//] #Hcut >Hcut >H3 >associative_append @memb_append_l2 @memb_cons @membx - |whd in ⊢ (??%?); >(bit_not_grid … Hd') >(bit_not_bar … Hd') % + |whd in ⊢ (??%?); >(bit_or_null_not_grid … Hd') >(bit_or_null_not_bar … Hd') % ] ] |#x #membx @(no_marks_in_table … Htable) @@ -534,7 +542,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 l1 → is_bit c1 = true → n = |l1| → + is_bit c = true → only_bits_or_nulls l1 → is_bit c1 = true → n = |l1| → table_TM (S n) (〈c1,true〉::l2) → t1 = midtape STape (〈grid,false〉::ls) 〈c,true〉 (l1@〈grid,false〉::〈c1,true〉::l2@〈grid,false〉::rs) → diff --git a/matita/matita/lib/turing/universal/universal.ma b/matita/matita/lib/turing/universal/universal.ma index aa75b326a..1ef5b07ef 100644 --- a/matita/matita/lib/turing/universal/universal.ma +++ b/matita/matita/lib/turing/universal/universal.ma @@ -16,19 +16,32 @@ include "turing/universal/copy.ma". +(* +moves: +0_ = N +10 = L +11 = R +*) + (* step : -init_current; -init_table; -match_tuple; -if is_marked(current) = false (* match *) - then init_current; (* preconditions? *) - adv_to_mark_r; - adv_mark_r; - copy; - ...move... +if is_true(current) (* current state is final *) + then nop + else + match_tuple; + if is_marked(current) = false (* match *) + then adv_mark_r; + move_l; + init_current; + move_r; + adv_to_mark_r; + copy; + ...move... + reset; + else sink; +MANCANO MOVE E RESET *) \ No newline at end of file -- 2.39.2