X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fbasic_machines.ma;h=c1559702a59770c27dc68bbfcf98e2d50f6aaa46;hb=caf822cbe34e204e6d1b72e272373b561c1a565a;hp=82d4758c250c31eeac7545f6dd89179c2996d52c;hpb=53656d48b302c50e775159dc62e56cd7b1550676;p=helm.git

diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma
index 82d4758c2..c1559702a 100644
--- a/matita/matita/lib/turing/basic_machines.ma
+++ b/matita/matita/lib/turing/basic_machines.ma
@@ -21,8 +21,8 @@ definition write ≝ λalpha,c.
   mk_TM alpha write_states
   (λp.let 〈q,a〉 ≝ p in
     match pi1 … q with 
-    [ O ⇒ 〈wr1,Some ? 〈c,N〉〉
-    | S _ ⇒ 〈wr1,None ?〉 ])
+    [ O ⇒ 〈wr1,Some ? c,N〉
+    | S _ ⇒ 〈wr1,None ?,N〉 ])
   wr0 (λx.x == wr1).
   
 definition R_write ≝ λalpha,c,t1,t2.
@@ -32,7 +32,35 @@ lemma sem_write : ∀alpha,c.Realize ? (write alpha c) (R_write alpha c).
 #alpha #c #t @(ex_intro … 2) @ex_intro
   [|% [% |#ls #c #rs #Ht >Ht % ] ]
 qed. 
- 
+
+definition R_write_strong ≝ λalpha,c,t1,t2.
+  t2 = midtape alpha (left ? t1) c (right ? t1).
+  
+lemma sem_write_strong : ∀alpha,c.Realize ? (write alpha c) (R_write_strong alpha c).
+#alpha #c #t @(ex_intro … 2) @ex_intro
+  [|% [% |cases t normalize // ] ]
+qed. 
+
+(***************************** replace a with f a *****************************)
+
+definition writef ≝ λalpha,f.
+  mk_TM alpha write_states
+  (λp.let 〈q,a〉 ≝ p in
+    match pi1 … q with 
+    [ O ⇒ 〈wr1,Some ? (f a),N〉
+    | S _ ⇒ 〈wr1,None ?,N〉 ])
+  wr0 (λx.x == wr1).
+
+definition R_writef ≝ λalpha,f,t1,t2.
+  ∀c. current ? t1 = c  →
+  t2 = midtape alpha (left ? t1) (f c) (right ? t1).
+  
+lemma sem_writef : ∀alpha,f.
+  writef alpha f  ⊨ R_writef alpha f.
+#alpha #f #t @(ex_intro … 2) @ex_intro
+  [|% [% |cases t normalize // ] ]
+qed. 
+
 (******************** moves the head one step to the right ********************)
 
 definition move_states ≝ initN 2.
@@ -43,10 +71,10 @@ definition move_r ≝
   λalpha:FinSet.mk_TM alpha move_states
   (λp.let 〈q,a〉 ≝ p in
     match a with
-    [ None ⇒ 〈move1,None ?〉
+    [ None ⇒ 〈move1,None ?,N〉
     | Some a' ⇒ match (pi1 … q) with
-      [ O ⇒ 〈move1,Some ? 〈a',R〉〉
-      | S q ⇒ 〈move1,None ?〉 ] ])
+      [ O ⇒ 〈move1,Some ? a',R〉
+      | S q ⇒ 〈move1,None ?,N〉 ] ])
   move0 (λq.q == move1).
   
 definition R_move_r ≝ λalpha,t1,t2.
@@ -80,10 +108,10 @@ definition move_l ≝
   λalpha:FinSet.mk_TM alpha move_states
   (λp.let 〈q,a〉 ≝ p in
     match a with
-    [ None ⇒ 〈move1,None ?〉
+    [ None ⇒ 〈move1,None ?,N〉
     | Some a' ⇒ match pi1 … q with
-      [ O ⇒ 〈move1,Some ? 〈a',L〉〉
-      | S q ⇒ 〈move1,None ?〉 ] ])
+      [ O ⇒ 〈move1,Some ? a',L〉
+      | S q ⇒ 〈move1,None ?,N〉 ] ])
   move0 (λq.q == move1).
 
 definition R_move_l ≝ λalpha,t1,t2.
@@ -106,6 +134,30 @@ lemma sem_move_l :
   #ls1 #c1 #rs1 #H destruct cases ls1 // ] ] ]
 qed.
 
+(* a slightly different move machine. *)
+definition smove_states ≝ initN 2.
+
+definition smove0 : smove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
+definition smove1 : smove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
+
+definition trans_smove ≝ 
+ λsig,D.
+ λp:smove_states × (option sig).
+ let 〈q,a〉 ≝ p in match (pi1 … q) with
+ [ O ⇒ 〈smove1,None sig, D〉
+ | S _ ⇒ 〈smove1,None sig, N〉 ].
+
+definition move ≝ 
+  λsig,D.mk_TM sig smove_states (trans_smove sig D) smove0 (λq.q == smove1).
+
+definition Rmove ≝ 
+  λalpha,D,t1,t2. t2 = tape_move alpha t1 D.
+
+lemma sem_move_single :
+  ∀alpha,D.move alpha D ⊨ Rmove alpha D.
+#alpha #D #int %{2} %{(mk_config ? smove_states smove1 ?)} [| % % ]
+qed.
+
 (********************************* test char **********************************)
 
 (* the test_char machine ends up in two different states q1 and q2 wether or not
@@ -125,11 +177,11 @@ definition test_char ≝
   mk_TM alpha tc_states
   (λp.let 〈q,a〉 ≝ p in
    match a with
-   [ None ⇒ 〈tc_false, None ?〉
+   [ None ⇒ 〈tc_false, None ?,N〉
    | Some a' ⇒ 
      match test a' with
-     [ true ⇒ 〈tc_true,None ?〉
-     | false ⇒ 〈tc_false,None ?〉 ]])
+     [ true ⇒ 〈tc_true,None ?,N〉
+     | false ⇒ 〈tc_false,None ?,N〉 ]])
   tc_start (λx.notb (x == tc_start)).
 
 definition Rtc_true ≝ 
@@ -197,6 +249,27 @@ lemma test_char_inv :
 #sig #P #f #t #t0 #HPt * #_ //
 qed.
 
+definition test_null ≝ λalpha.test_char alpha (λ_.true).
+
+definition R_test_null_true ≝ λalpha,t1,t2.
+  current alpha t1 ≠ None ? ∧ t1 = t2.
+  
+definition R_test_null_false ≝ λalpha,t1,t2.
+  current alpha t1 = None ? ∧ t1 = t2.
+  
+lemma sem_test_null : ∀alpha.
+  test_null alpha ⊨ [ tc_true : R_test_null_true alpha, R_test_null_false alpha].
+#alpha #t1 cases (sem_test_char alpha (λ_.true) t1) #k * #outc * * #Hloop #Htrue
+#Hfalse %{k} %{outc} % [ %
+[ @Hloop
+| #Houtc cases (Htrue ?) [| @Houtc] * #c * #Hcurt1 #_ #Houtc1 %
+  [ >Hcurt1 % #H destruct (H) | <Houtc1 % ] ]
+| #Houtc cases (Hfalse ?) [| @Houtc] #Habsurd #Houtc %
+  [ cases (current alpha t1) in Habsurd; // #c1 #Habsurd 
+    lapply (Habsurd ? (refl ??)) #H destruct (H)
+  | <Houtc % ] ]
+qed.
+
 (************************************* swap ***********************************)
 definition swap_states : FinSet → FinSet ≝ 
   λalpha:FinSet.FinProd (initN 4) alpha.
@@ -213,15 +286,15 @@ definition swap_r ≝
   let 〈q',b〉 ≝ q in
   let q' ≝ pi1 nat (λi.i<4) q' in
   match a with 
-  [ None ⇒ 〈〈swap3,foo〉,None ?〉 (* if tape is empty then stop *)
+  [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
   | Some a' ⇒ 
   match q' with
-  [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? 〈a',R〉〉  (* save in register and move R *)
+  [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? a',R〉  (* save in register and move R *)
   | S q' ⇒ match q' with
-    [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? 〈b,L〉〉 (* swap with register and move L *)
+    [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? b,L〉 (* swap with register and move L *)
     | 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 *)
+      [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
+      | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
       ]
     ]
   ]])
@@ -262,15 +335,15 @@ definition swap_l ≝
   let 〈q',b〉 ≝ q in
   let q' ≝ pi1 nat (λi.i<4) q' in
   match a with 
-  [ None ⇒ 〈〈swap3,foo〉,None ?〉 (* if tape is empty then stop *)
+  [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
   | Some a' ⇒ 
   match q' with
-  [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? 〈a',L〉〉  (* save in register and move L *)
+  [ 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 *)
+    [ 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 *)
+      [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
+      | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
       ]
     ]
   ]])
@@ -302,4 +375,230 @@ lemma sem_swap_l : ∀alpha,foo.
       [#b #rs #H destruct | #a #b #ls #rs #H destruct normalize //
     ]
   ]
-qed.
\ No newline at end of file
+qed.
+
+(********************************** combine ***********************************)
+(* replace the content x of a cell with a combiation f(x,y) of x and the content
+y of the adiacent cell *)
+
+definition combf_states : FinSet → FinSet ≝ 
+  λalpha:FinSet.FinProd (initN 4) alpha.
+
+definition combf0 : initN 4 ≝ mk_Sig ?? 0 (leb_true_to_le 1 4 (refl …)).
+definition combf1 : initN 4 ≝ mk_Sig ?? 1 (leb_true_to_le 2 4 (refl …)).
+definition combf2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)).
+definition combf3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)).
+
+definition combf_r ≝ 
+ λalpha:FinSet.λf.λfoo:alpha.
+ mk_TM alpha (combf_states alpha)
+ (λp.let 〈q,a〉 ≝ p in
+  let 〈q',b〉 ≝ q in
+  let q' ≝ pi1 nat (λi.i<4) q' in
+  match a with 
+  [ None ⇒ 〈〈combf3,foo〉,None ?,N〉 (* if tape is empty then stop *)
+  | Some a' ⇒ 
+  match q' with
+  [ O ⇒ (* q0 *) 〈〈combf1,a'〉,Some ? a',R〉  (* save in register and move R *)
+  | S q' ⇒ match q' with
+    [ O ⇒ (* q1 *) 〈〈combf2,f b a'〉,Some ? a',L〉 
+      (* combine in register and move L *)
+    | S q' ⇒ match q' with
+      [ O ⇒ (* q2 *) 〈〈combf3,foo〉,Some ? b,R〉 
+        (* copy from register and move R *)
+      | S q' ⇒ (* q3 *) 〈〈combf3,foo〉,None ?,N〉 (* final state *)
+      ]
+    ]
+  ]])
+  〈combf0,foo〉
+  (λq.\fst q == combf3).
+  
+definition Rcombf_r ≝ 
+  λalpha,f,t1,t2.
+    (∀b,ls.
+      t1 = midtape alpha ls b [ ] → 
+      t2 = rightof ? b ls) ∧
+    (∀a,b,ls,rs. 
+      t1 = midtape alpha ls b (a::rs) → 
+      t2 = midtape alpha ((f b a)::ls) a rs).
+
+lemma sem_combf_r : ∀alpha,f,foo.
+  combf_r alpha f foo ⊨ Rcombf_r alpha f. 
+#alpha #f #foo *
+  [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (niltape ?)))
+   % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
+  |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (leftof ? l0 lt0)))
+   % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
+  |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (rightof ? r0 rt0)))
+   % [% |% [#b #ls | #a #b #ls #rs] #H destruct] 
+  | #lt #c #rt @(ex_intro ?? 4) cases rt
+    [@ex_intro [|% [ % | %
+      [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
+    |#r0 #rt0 @ex_intro [| % [ % | %
+      [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
+    ]
+  ]
+qed.
+
+definition combf_l ≝ 
+ λalpha:FinSet.λf.λfoo:alpha.
+ mk_TM alpha (combf_states alpha)
+ (λp.let 〈q,a〉 ≝ p in
+  let 〈q',b〉 ≝ q in
+  let q' ≝ pi1 nat (λi.i<4) q' in
+  match a with 
+  [ None ⇒ 〈〈combf3,foo〉,None ?,N〉 (* if tape is empty then stop *)
+  | Some a' ⇒ 
+  match q' with
+  [ O ⇒ (* q0 *) 〈〈combf1,a'〉,Some ? a',L〉  (* save in register and move R *)
+  | S q' ⇒ match q' with
+    [ O ⇒ (* q1 *) 〈〈combf2,f b a'〉,Some ? a',R〉 
+      (* combine in register and move L *)
+    | S q' ⇒ match q' with
+      [ O ⇒ (* q2 *) 〈〈combf3,foo〉,Some ? b,L〉 
+        (* copy from register and move R *)
+      | S q' ⇒ (* q3 *) 〈〈combf3,foo〉,None ?,N〉 (* final state *)
+      ]
+    ]
+  ]])
+  〈combf0,foo〉
+  (λq.\fst q == combf3).
+  
+definition Rcombf_l ≝ 
+  λalpha,f,t1,t2.
+    (∀b,rs.
+      t1 = midtape alpha [ ] b rs → 
+      t2 = leftof ? b rs) ∧
+    (∀a,b,ls,rs. 
+      t1 = midtape alpha (a::ls) b rs → 
+      t2 = midtape alpha ls a ((f b a)::rs)).
+
+lemma sem_combf_l : ∀alpha,f,foo.
+  combf_l alpha f foo ⊨ Rcombf_l alpha f. 
+#alpha #f #foo *
+  [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (niltape ?)))
+   % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
+  |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (leftof ? l0 lt0)))
+   % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
+  |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (rightof ? r0 rt0)))
+   % [% |% [#b #ls | #a #b #ls #rs] #H destruct] 
+  | #lt #c #rt @(ex_intro ?? 4) cases lt
+    [@ex_intro [|% [ % | %
+      [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
+    |#r0 #rt0 @ex_intro [| % [ % | %
+      [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
+    ]
+  ]
+qed.
+
+(********************************* new_combine ********************************)
+(* replace the content x of a cell with a combiation f(x,y) of x and the content
+y of the adiacent cell; if there is no adjacent cell, combines with a default 
+value foo *)
+
+definition ncombf_r ≝ 
+ λalpha:FinSet.λf.λfoo:alpha.
+ mk_TM alpha (combf_states alpha)
+ (λp.let 〈q,a〉 ≝ p in
+  let 〈q',b〉 ≝ q in
+  let q' ≝ pi1 nat (λi.i<4) q' in
+  match a with 
+  [ None ⇒ if (eqb q' 1)then (* if on right cell, combine in register and move L *) 
+           〈〈combf2,f b foo〉,None ?,L〉
+           else 〈〈combf3,foo〉,None ?,N〉 (* else stop *)
+  | Some a' ⇒ 
+  match q' with
+  [ O ⇒ (* q0 *) 〈〈combf1,a'〉,Some ? a',R〉  (* save in register and move R *)
+  | S q' ⇒ match q' with
+    [ O ⇒ (* q1 *) 〈〈combf2,f b a'〉,Some ? a',L〉 
+      (* combine in register and move L *)
+    | S q' ⇒ match q' with
+      [ O ⇒ (* q2 *) 〈〈combf3,foo〉,Some ? b,R〉 
+        (* copy from register and move R *)
+      | S q' ⇒ (* q3 *) 〈〈combf3,foo〉,None ?,N〉 (* final state *)
+      ]
+    ]
+  ]])
+  〈combf0,foo〉
+  (λq.\fst q == combf3).
+  
+definition Rncombf_r ≝ 
+  λalpha,f,foo,t1,t2.
+    (∀b,ls.
+      t1 = midtape alpha ls b [ ] → 
+      t2 = rightof ? (f b foo) ls) ∧
+    (∀a,b,ls,rs. 
+      t1 = midtape alpha ls b (a::rs) → 
+      t2 = midtape alpha ((f b a)::ls) a rs).
+
+lemma sem_ncombf_r : ∀alpha,f,foo.
+  ncombf_r alpha f foo ⊨ Rncombf_r alpha f foo. 
+#alpha #f #foo *
+  [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (niltape ?)))
+   % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
+  |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (leftof ? l0 lt0)))
+   % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
+  |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (rightof ? r0 rt0)))
+   % [% |% [#b #ls | #a #b #ls #rs] #H destruct] 
+  | #lt #c #rt @(ex_intro ?? 4) cases rt
+    [@ex_intro [|% [ % | %
+      [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
+    |#r0 #rt0 @ex_intro [| % [ % | %
+      [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
+    ]
+  ]
+qed.
+
+definition ncombf_l ≝ 
+ λalpha:FinSet.λf.λfoo:alpha.
+ mk_TM alpha (combf_states alpha)
+ (λp.let 〈q,a〉 ≝ p in
+  let 〈q',b〉 ≝ q in
+  let q' ≝ pi1 nat (λi.i<4) q' in
+  match a with 
+  [ None ⇒ if (eqb q' 1)then 
+           (* if on left cell, combine in register and move R *) 
+           〈〈combf2,f b foo〉,None ?,R〉
+           else 〈〈combf3,foo〉,None ?,N〉 (* else stop *)
+  | Some a' ⇒ 
+  match q' with
+  [ O ⇒ (* q0 *) 〈〈combf1,a'〉,Some ? a',L〉  (* save in register and move R *)
+  | S q' ⇒ match q' with
+    [ O ⇒ (* q1 *) 〈〈combf2,f b a'〉,Some ? a',R〉 
+      (* combine in register and move L *)
+    | S q' ⇒ match q' with
+      [ O ⇒ (* q2 *) 〈〈combf3,foo〉,Some ? b,L〉 
+        (* copy from register and move R *)
+      | S q' ⇒ (* q3 *) 〈〈combf3,foo〉,None ?,N〉 (* final state *)
+      ]
+    ]
+  ]])
+  〈combf0,foo〉
+  (λq.\fst q == combf3).
+  
+definition Rncombf_l ≝ 
+  λalpha,f,foo,t1,t2.
+    (∀b,rs.
+      t1 = midtape alpha [ ] b rs → 
+      t2 = leftof ? (f b foo) rs) ∧
+    (∀a,b,ls,rs. 
+      t1 = midtape alpha (a::ls) b rs → 
+      t2 = midtape alpha ls a ((f b a)::rs)).
+
+lemma sem_ncombf_l : ∀alpha,f,foo.
+  ncombf_l alpha f foo ⊨ Rncombf_l alpha f foo. 
+#alpha #f #foo *
+  [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (niltape ?)))
+   % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
+  |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (leftof ? l0 lt0)))
+   % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
+  |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈combf3,foo〉 (rightof ? r0 rt0)))
+   % [% |% [#b #ls | #a #b #ls #rs] #H destruct] 
+  | #lt #c #rt @(ex_intro ?? 4) cases lt
+    [@ex_intro [|% [ % | %
+      [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
+    |#r0 #rt0 @ex_intro [| % [ % | %
+      [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
+    ]
+  ]
+qed.