From 06913146ad4e17070d27b6b0a08d48f14fefb188 Mon Sep 17 00:00:00 2001
From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Fri, 18 May 2012 15:43:37 +0000
Subject: [PATCH] Progress

---
 matita/matita/lib/turing/universal/copy.ma    | 55 ++++++++++-
 matita/matita/lib/turing/universal/tuples.ma  |  2 +-
 .../matita/lib/turing/universal/uni_step.ma   | 92 ++++++++++++++++++-
 3 files changed, 142 insertions(+), 7 deletions(-)

diff --git a/matita/matita/lib/turing/universal/copy.ma b/matita/matita/lib/turing/universal/copy.ma
index 6b77ef9b7..de39fb88c 100644
--- a/matita/matita/lib/turing/universal/copy.ma
+++ b/matita/matita/lib/turing/universal/copy.ma
@@ -301,11 +301,58 @@ lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop
           (* by IH, we proceed by cases, whether a = comma 
              (consequently several lists = []) or not *)          
           *
-          [ * #Ha #Houtc1 >Hl1cons in Hl1; >Hla
+          [ * #Ha #Houtc1
+(*           cut (l1 = [〈a,false〉])
+           [ cases l1'' in Hl1cons; // #y #ly #Hly
+             >Hly in Hl1; cases l1' in Hl1bits;
+             [ #_ normalize #Hfalse destruct (Hfalse)
+             | #p #lp #Hl1bits normalize #Heq destruct (Heq)
+               @False_ind lapply (Hl1bits 〈a,false〉 ?)
+               [ cases lp in e0;
+                 [ normalize #Hfalse destruct (Hfalse)
+                 | #p0 #lp0 normalize in ⊢ (%→?); #Heq destruct (Heq)
+                   @memb_cons @memb_hd ]
+               | >Ha normalize #Hfalse destruct (Hfalse) ]
+             ]
+           ] #Hl1a
+           cut (l4 = [〈a0,false〉])
+           [ generalize in match Hl4bits; cases l4' in Hl4;
+             [ >Hl4cons #Hfalse #_ 
+               lapply (inj_append_singleton_l1 ?? [] ?? Hfalse)
+               cases (reverse ? l4'') normalize
+               [ #Hfalse1 | #p0 #lp0 #Hfalse1 ] destruct (Hfalse1)
+             | #p #lp 
+           
+             cases l4'' in Hl4cons; // #y #ly #Hly
+             >Hly in Hl4; cases l4' in Hl4bits;
+             [ #_ >reverse_cons #Hfalse
+               lapply (inj_append_singleton_l1 ?? [] ?? Hfalse)
+               -Hfalse cases ly normalize
+               [ #Hfalse | #p #Hp #Hfalse ] destruct (Hfalse)
+                
+             | #p #lp #Hl1bits normalize #Heq destruct (Heq)
+               @False_ind lapply (Hl1bits 〈a,false〉 ?)
+               [ cases lp in e0;
+                 [ normalize #Hfalse destruct (Hfalse)
+                 | #p0 #lp0 normalize in ⊢ (%→?); #Heq destruct (Heq)
+                   @memb_cons @memb_hd ]
+               | >Ha normalize #Hfalse destruct (Hfalse) ]
+             ]
+           ] #Hl1a
+             
+              >Hla normalize #Hl1 destruct (Hl1) lapply (inj_append_ @False_ind
+             
+           cut (l1'' = [] ∧ l4'' = [])
+           [ % [ >Hla in Hl1; normalize #Hl1 destruct (Hl1)
+           
+            cases l1'' in Hl1bits;
+                
+                 [ #_ normalize #H *)
+           cut (la = [] ∧ lb = [] ∧ l1'' = [] ∧ l4'' = [])
+           [ @daemon ] * * * #Hla1 #Hlb1 #Hl1nil #Hl4nil
+           >Hl1cons in Hl1; >Hla
            >Houtc1 >Htc #Hl1
            >Hl4cons in Hl4; >Hlb #Hl4
-           cut (la = [] ∧ lb = [] ∧ l1'' = [] ∧ l4'' = []) 
-           [@daemon] * * * #Hla1 #Hlb1 #Hl1nil #Hl4nil
            >Hla1 >Hlb1 >Hl1nil >Hl4nil >Hx
            cut (a0 = grid) [ @daemon ] #Ha0 <Ha <Ha0
            normalize in ⊢ (??(??%?%)(??%?%)); >associative_append %
@@ -363,7 +410,7 @@ definition R_copy ≝ λt1,t2.
   ∀ls,c,c0,rs,l1,l3,l4.
   t1 = midtape STape (l3@〈grid,false〉::l4@〈c0,true〉::ls) 〈c,true〉 (l1@〈comma,false〉::rs) → 
   no_marks l1 → no_marks l3 → no_marks l4 → |l1| = |l4| → 
-  only_bits_or_nulls (〈c0,true〉::l4) → only_bits_or_nulls (〈c,true〉::l1) → 
+  only_bits_or_nulls (l4@[〈c0,true〉]) → only_bits_or_nulls (〈c,true〉::l1) → 
   t2 = midtape STape (reverse ? l1@l3@〈grid,false〉::
           merge_config (l4@[〈c0,false〉]) (reverse ? (〈c,false〉::l1))@ls) 
      〈comma,false〉 rs.
diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma
index a7afb0b2b..2520fed51 100644
--- a/matita/matita/lib/turing/universal/tuples.ma
+++ b/matita/matita/lib/turing/universal/tuples.ma
@@ -653,7 +653,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_or_nulls l1 → is_bit c1 = true → n = |l1| →
-  table_TM (S n) (〈c1,true〉::l2) → 
+  table_TM (S n) (〈c1,false〉::l2) → 
   t1 = midtape STape (〈grid,false〉::ls) 〈c,true〉 
          (l1@〈grid,false〉::〈c1,true〉::l2@〈grid,false〉::rs) → 
   (* facciamo match *)
diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma
index 1cb035a6a..701972f3f 100644
--- a/matita/matita/lib/turing/universal/uni_step.ma
+++ b/matita/matita/lib/turing/universal/uni_step.ma
@@ -170,5 +170,93 @@ cases HR -HR
     ]
   ]
 qed.
-    ]-Htf
-qed.
+
+include "turing/universal/move_tape.ma".
+
+definition exec_move ≝ 
+  seq ? (adv_to_mark_r … (is_marked ?))
+    (seq ? init_copy
+      (seq ? copy
+        (seq ? (move_r …)
+          (seq ? move_tape (move_r …))))).
+
+definition lift_tape ≝ λls,c,rs.
+  let 〈c0,b〉 ≝ c in
+  let c' ≝ match c0 with
+  [ null ⇒ None ?
+  | _ ⇒ Some ? c ]
+  in
+  mk_tape STape ls c' rs.
+  
+definition sim_current_of_tape ≝ λt.
+  match current STape t with
+  [ None ⇒ 〈null,false〉
+  | Some c0 ⇒ c0 ].
+
+(*
+ t1 =  ls # cs c # table # rs  
+ 
+ let simt ≝ lift_tape ls c rs in
+ let simt' ≝ move_left simt' in
+ 
+ t2 = left simt'# cs (sim_current_of_tape simt') # table # right simt'
+*)
+          
+(*
+definition R_move
+
+definition R_exec_move ≝ λt1,t2.
+  ∀ls,current,table1,newcurrent,table2,rs.
+  t1 = midtape STape (current@〈grid,false〉::ls) 〈grid,false〉
+       (table1@〈comma,true〉::newcurrent@〈comma,false〉::move::table2@
+        〈grid,false〉::rs) → 
+  table_TM (table1@〈comma,false〉::newcurrent@〈comma,false〉::move::table2) →
+  t2 = midtape
+*)
+
+(*
+
+step :
+
+if is_true(current) (* current state is final *)
+   then nop
+   else 
+   init_match;
+   match_tuple;
+   if is_marked(current) = false (* match ok *)
+      then exec_move; 
+      else sink;
+        
+*)
+
+definition mk_tuple ≝ λc,newc,mv.
+  c @ 〈comma,false〉:: newc @ 〈comma,false〉 :: [〈mv,false〉].
+
+inductive match_in_table (c,newc:list STape) (mv:unialpha) : list STape → Prop ≝ 
+| mit_hd : 
+   ∀tb.
+   match_in_table c newc mv (mk_tuple c newc mv@〈bar,false〉::tb)
+| mit_tl :
+   ∀c0,newc0,mv0,tb.
+   match_in_table c newc mv tb → 
+   match_in_table c newc mv (mk_tuple c0 newc0 mv0@〈bar,false〉::tb).
+
+definition move_of_unialpha ≝ 
+  λc.match c with
+  [ bit x ⇒ match x with [ true ⇒ R | false ⇒ L ]
+  | _ ⇒ N ].
+
+definition R_uni_step ≝ λt1,t2.
+  ∀n,table,c,c1,ls,rs,curs,curc,news,newc,mv.
+  table_TM n table → 
+  match_in_table (〈c,false〉::curs@[〈curc,false〉]) 
+    (〈c1,false〉::news@[〈newc,false〉]) mv table → 
+  t1 = midtape STape (〈grid,false〉::ls) 〈c,false〉 
+    (curs@〈curc,false〉::〈grid,false〉::table@〈grid,false〉::rs) → 
+  ∀t1',ls1,rs1.t1' = lift_tape ls 〈curc,false〉 rs → 
+  (t2 = midtape STape (〈grid,false〉::ls1) 〈c1,false〉 
+    (news@〈newc,false〉::〈grid,false〉::table@〈grid,false〉::rs1) ∧
+   lift_tape ls1 〈newc,false〉 rs1 = 
+   tape_move STape t1' (Some ? 〈〈newc,false〉,move_of_unialpha mv〉)).
+  
+  
\ No newline at end of file
-- 
2.39.2