From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 6 Jun 2012 09:07:48 +0000 (+0000)
Subject: swap machine; move_char revisited
X-Git-Tag: make_still_working~1655
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d17dfeccb51f1dd6f94645018c15078ef4d329a4;p=helm.git

swap machine; move_char revisited
---

diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma
index 5612353a8..1d873ee86 100644
--- a/matita/matita/lib/turing/basic_machines.ma
+++ b/matita/matita/lib/turing/basic_machines.ma
@@ -185,3 +185,55 @@ lemma sem_test_char :
 ]
 qed.
 
+(************************************* swap ***********************************)
+definition swap_states : FinSet → FinSet ≝ 
+  λalpha:FinSet.FinProd (initN 4) alpha.
+
+definition swap0 : initN 4 ≝ mk_Sig ?? 0 (leb_true_to_le 1 4 (refl …)).
+definition swap1 : initN 4 ≝ mk_Sig ?? 1 (leb_true_to_le 2 4 (refl …)).
+definition swap2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)).
+definition swap3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)).
+
+definition swap ≝ 
+ λalpha:FinSet.λfoo:alpha.
+ mk_TM alpha (swap_states alpha)
+ (λp.let 〈q,a〉 ≝ p in
+  let 〈q',b〉 ≝ q in
+  let q' ≝ pi1 nat (λi.i<4) q' in (* perche' devo passare il predicato ??? *)
+  match a with 
+  [ None ⇒ 〈〈swap3,foo〉,None ?〉 (* if tape is empty then stop *)
+  | Some a' ⇒ 
+  match q' with
+  [ 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 *)
+    | 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 *)
+      ]
+    ]
+  ]])
+  〈swap0,foo〉
+  (λq.\fst q == swap3).
+
+definition Rswap ≝ 
+  λalpha,t1,t2.
+   ∀a,b,ls,rs.  
+    t1 = midtape alpha ls b (a::rs) → 
+    t2 = midtape alpha ls a (b::rs).
+
+lemma sem_swap : ∀alpha,foo.
+  swap alpha foo ⊨ Rswap alpha. 
+#alpha #foo *
+  [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
+   % [% |#a #b #ls #rs #H destruct]
+  |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
+   % [% |#a #b #ls #rs #H destruct] 
+  |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
+   % [% |#a #b #ls #rs #H destruct] 
+  | #lt #c #rt @(ex_intro ?? 4) cases rt
+    [@ex_intro [|% [ % | #a #b #ls #rs #H destruct]]
+    |#r0 #rt0 @ex_intro [| % [ % | #a #b #ls #rs #H destruct //
+    ]
+  ]
+qed.
diff --git a/matita/matita/lib/turing/universal/move_char_l.ma b/matita/matita/lib/turing/universal/move_char_l.ma
index 2fa78ec6a..b85385705 100644
--- a/matita/matita/lib/turing/universal/move_char_l.ma
+++ b/matita/matita/lib/turing/universal/move_char_l.ma
@@ -12,7 +12,8 @@
 
 (* MOVE_CHAR (left) MACHINE
 
-Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra.
+Sposta il carattere binario su cui si trova la testina appena prima del primo # 
+alla sua sinistra.
 
 Input:
 (ls,cs,rs can be empty; # is a parameter)
@@ -31,7 +32,8 @@ Final state = 〈4,#〉
 
 *)
 
-include "turing/while_machine.ma".
+include "turing/basic_machines.ma".
+include "turing/if_machine.ma".
 
 definition mcl_states : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 5) alpha.
 
@@ -41,6 +43,12 @@ definition mcl2 : initN 5 ≝ mk_Sig ?? 2 (leb_true_to_le 3 5 (refl …)).
 definition mcl3 : initN 5 ≝ mk_Sig ?? 3 (leb_true_to_le 4 5 (refl …)).
 definition mcl4 : initN 5 ≝ mk_Sig ?? 4 (leb_true_to_le 5 5 (refl …)).
 
+definition mcl_step ≝ λalpha:FinSet.λsep:alpha.
+  ifTM alpha (test_char ? (λc.¬c==sep))
+     (single_finalTM … (seq … (swap alpha sep) (move_l ?))) (nop ?) tc_true.
+     
+
+(*
 definition mcl_step ≝ 
  λalpha:FinSet.λsep:alpha.
  mk_TM alpha (mcl_states alpha)
@@ -101,6 +109,7 @@ lemma mcl_q2_q3 :
     (tape_move_left alpha ls a rs).
 #alpha #sep #a #ls #a0 * //
 qed.
+*)
 
 definition Rmcl_step_true ≝ 
   λalpha,sep,t1,t2.
@@ -113,7 +122,7 @@ definition Rmcl_step_false ≝
   λalpha,sep,t1,t2.
     right ? t1 ≠ [] →  current alpha t1 ≠ None alpha → 
       current alpha t1 = Some alpha sep ∧ t2 = t1.
-    
+(*      
 lemma mcl_trans_init_sep: 
   ∀alpha,sep,x.
   trans ? (mcl_step alpha sep) 〈〈mcl0,x〉,Some ? sep〉 = 〈〈mcl4,sep〉,None ?〉.
@@ -125,7 +134,29 @@ lemma mcl_trans_init_not_sep:
   trans ? (mcl_step alpha sep) 〈〈mcl0,x〉,Some ? y〉 = 〈〈mcl1,y〉,Some ? 〈y,R〉〉.
 #alpha #sep #x #y #H1 normalize >H1 //
 qed.
+*)
 
+lemma sem_mcl_step :
+  ∀alpha,sep.
+  mcl_step alpha sep ⊨ 
+    [inr … (inl … (inr … start_nop)): Rmcl_step_true alpha sep, Rmcl_step_false alpha sep].
+#alpha #sep 
+  @(acc_sem_if_app … 
+     (sem_test_char …) (sem_seq …(sem_swap …) (sem_move_l …)) (sem_nop …))
+  [#intape #outtape #tapea whd in ⊢ (%→%→%);
+   #Htapea * #tapeb * whd in ⊢ (%→%→?);
+   #Htapeb #Houttape #a #b #ls #rs #Hintape
+   >Hintape in Htapea; #Htapea cases (Htapea ? (refl …)) -Htapea
+   #Hbsep #Htapea % [@(\Pf (injective_notb ? false Hbsep))]
+   @Houttape
+  |#intape #outtape #tapea whd in ⊢ (%→%→%);
+   cases (current alpha intape) 
+    [#_ #_ #_ * #Hfalse @False_ind @Hfalse %
+    |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % //
+     lapply (injective_notb ? true csep) -csep #csep >(\P csep) 
+    ]
+  
+    
 lemma sem_mcl_step :
   ∀alpha,sep.
   accRealize alpha (mcl_step alpha sep) 
diff --git a/matita/matita/lib/turing/universal/move_tape.ma b/matita/matita/lib/turing/universal/move_tape.ma
index dad01b719..cd8a87c5f 100644
--- a/matita/matita/lib/turing/universal/move_tape.ma
+++ b/matita/matita/lib/turing/universal/move_tape.ma
@@ -9,7 +9,7 @@
      \ /   GNU General Public License Version 2   
       V_____________________________________________________________*)
 
-(* include "turing/universal/move_char_c.ma". *)
+include "turing/universal/move_char_c.ma".
 include "turing/universal/move_char_l.ma".
 include "turing/universal/tuples.ma".