]> matita.cs.unibo.it Git - helm.git/commitdiff
Added null character.
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Thu, 17 May 2012 07:04:54 +0000 (07:04 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Thu, 17 May 2012 07:04:54 +0000 (07:04 +0000)
matita/matita/lib/turing/universal/alphabet.ma
matita/matita/lib/turing/universal/marks.ma
matita/matita/lib/turing/universal/move_char_l.ma
matita/matita/lib/turing/universal/tuples.ma
matita/matita/lib/turing/universal/universal.ma

index 646d8ebbd2cb4beef9bbfabe93937f2cde220b2e..04701aeec180b8b868e7388f186cb173900bb2ef 100644 (file)
@@ -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.
index 4b66e6af524fe89362fdc19d455a3ac80b37aa53..17992f95fca7cdef66e89e4f82c85abc174f338b 100644 (file)
@@ -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 ]
index a35d714d8928b3d9b3ac985413cc598981fd118f..57ba67bdcde1d07ada92fd0e95b8b40ede91386d 100644 (file)
@@ -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 // ] ]
index 21679f88544bc22307030cd2ebfa42b1d38922c8..3b1e9a39392a47ed93c2cf110c3edbed489b0167 100644 (file)
@@ -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)))
                 [<H2 whd #c0 #Hmemb cases (orb_true_l … Hmemb)
                   [#eqc0 >(\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) → 
index aa75b326aa7ca1f5216a0d9b03c0f6bf6df5c45c..1ef5b07ef2290388f3af01de3ac9ab0b3b3ad23f 100644 (file)
 
 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