From fb0cac5935fe56077893f6f02390c40dd1188953 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 30 May 2012 11:56:33 +0000
Subject: [PATCH] some progress

---
 .../lib/turing/universal/trans_to_tuples.ma   | 23 ++++----
 matita/matita/lib/turing/universal/tuples.ma  | 23 ++++++++
 .../matita/lib/turing/universal/uni_step.ma   | 17 +++---
 .../matita/lib/turing/universal/universal.ma  | 54 ++++++++++++++++---
 4 files changed, 95 insertions(+), 22 deletions(-)

diff --git a/matita/matita/lib/turing/universal/trans_to_tuples.ma b/matita/matita/lib/turing/universal/trans_to_tuples.ma
index e40a0bbc8..8b92473ce 100644
--- a/matita/matita/lib/turing/universal/trans_to_tuples.ma
+++ b/matita/matita/lib/turing/universal/trans_to_tuples.ma
@@ -158,10 +158,15 @@ letin mv ≝ match action with
  ]
 qed. 
 
-definition tuple_length ≝ λn.2*n+3.
+definition tuple_length ≝ λn.2*n+6.
 
-axiom length_of_tuple: ∀n,t. tuple_TM n t → 
+lemma length_of_tuple: ∀n,t. tuple_TM n t → 
   |t| = tuple_length n.
+#n #t * #qin * #cin * #qout * #cout * #mv *** #_
+#Hqin #Hqout #eqt >eqt whd in match (mk_tuple ?????); 
+normalize >length_append >Hqin -Hqin normalize 
+>length_append normalize >Hqout -Hqout //
+qed.
 
 definition move_eq ≝ λm1,m2:move.
   match m1 with
@@ -169,14 +174,14 @@ definition move_eq ≝ λm1,m2:move.
   |L ⇒ match m2 with [L ⇒ true | _ ⇒ false]
   |N ⇒ match m2 with [N ⇒ true | _ ⇒ false]].
   
-definition tuples_of_pairs ≝ λn.λh.map … (λp.(tuple_of_pair n h p)@[〈bar,false〉]).
+definition tuples_of_pairs ≝ λn.λh.map … (λp.tuple_of_pair n h p).
 
 definition flatten ≝ λA.foldr (list A) (list A) (append A) [].
 
 lemma wftable: ∀n,h,l.table_TM (S n) (flatten ? (tuples_of_pairs n h l)).
 #n #h #l elim l // -l #a #tl #Hind 
 whd in match (flatten … (tuples_of_pairs …));
->associative_append @ttm_cons //
+@ttm_cons //
 qed.
 
 lemma flatten_to_mem: ∀A,n,l,l1,l2.∀a:list A. 0 < n →
@@ -206,8 +211,8 @@ qed.
 
 axiom match_decomp: ∀n,l,qin,cin,qout,cout,mv.
   match_in_table (S n) qin cin qout cout mv l →
-  ∃l1,l2. l = l1@((mk_tuple qin cin qout cout mv)@[〈bar,false〉])@l2 ∧
-    (∃q.|l1| = (S (tuple_length (S n)))*q) ∧ tuple_TM (S n) (mk_tuple qin cin qout cout mv).
+  ∃l1,l2. l = l1@(mk_tuple qin cin qout cout mv)@l2 ∧
+    (∃q.|l1| = (tuple_length (S n))*q) ∧ tuple_TM (S n) (mk_tuple qin cin qout cout mv).
 (*
 lemma match_tech: ∀n,l,qin,cin,qout,cout,mv.
   (∀t. mem ? t l → |t| = |mk_tuple qin cin qout cout mv|) →
@@ -219,14 +224,14 @@ lemma match_tech: ∀n,l,qin,cin,qout,cout,mv.
 
 lemma match_to_tuple: ∀n,h,l,qin,cin,qout,cout,mv.
   match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h l)) → 
-    ∃p. p = mk_tuple qin cin qout cout mv ∧ mem ? (p@[〈bar,false〉]) (tuples_of_pairs n h l).
+    ∃p. p = mk_tuple qin cin qout cout mv ∧ mem ? p (tuples_of_pairs n h l).
 #n #h #l #qin #cin #qout #cout #mv #Hmatch 
 @(ex_intro … (mk_tuple qin cin qout cout mv)) % //
 cases (match_decomp … Hmatch) #l1 * #l2 * * #Hflat #Hlen #Htuple
 @(flatten_to_mem … Hflat … Hlen)  
   [// 
   |@daemon
-  |>length_append >(length_of_tuple … Htuple) normalize //
+  |@(length_of_tuple … Htuple) 
   ]
 qed.
 
@@ -248,7 +253,7 @@ lemma match_to_pair: ∀n,h,l,qin,cin,qout,cout,mv.
 #n #h #l #qin #cin #qout #cout #mv #Hmatch 
 cases (match_to_tuple … Hmatch)
 #p * #eqp #memb 
-cases(mem_map … (λp.(tuple_of_pair n h p)@[〈bar,false〉]) … memb)
+cases(mem_map … (λp.tuple_of_pair n h p) … memb)
 #p1 * #Hmem #H @(ex_intro … p1) % /2/
 qed.
 
diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma
index 2ccd367aa..d28017acb 100644
--- a/matita/matita/lib/turing/universal/tuples.ma
+++ b/matita/matita/lib/turing/universal/tuples.ma
@@ -818,6 +818,29 @@ definition R_match_tuple ≝ λt1,t2.
    ∀l3,newc,mv,l4.
    〈c1,false〉::l2 ≠ l3@〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv@l4). 
 
+(* possible variante ? 
+definition weakR_match_tuple ≝ λt1,t2.
+  (∀ls,cur,rs,b. t1 = midtape STape ls 〈grid,b〉 rs → t2 = t1) ∧
+  (∀c,l1,c1,l2,l3,ls0,rs0,n.
+  t1 = midtape STape (〈grid,false〉::ls0) 〈bit c,true〉 rs 
+    (l1@〈grid,false〉::l2@〈bit c1,true〉::l3@〈grid,false〉::rs0) → 
+  only_bits_or_nulls l1 → no_marks l1 → S n = |l1| →
+  table_TM (S n) (l2@〈c1,false〉::l3) → 
+  (* facciamo match *)
+  (∃l4,newc,mv,l5.
+   〈c1,false〉::l3 = l4@〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv::l5 ∧
+   t2 = midtape ? (reverse ? l1@〈c,false〉::〈grid,false〉::ls0) 〈grid,false〉
+        (l2@l4@〈c,false〉::l1@〈comma,true〉::newc@〈comma,false〉::mv::l5@
+        〈grid,false〉::rs0))
+  ∨
+  (* non facciamo match su nessuna tupla;
+     non specifichiamo condizioni sul nastro di output, perché
+     non eseguiremo altre operazioni, quindi il suo formato non ci interessa *)
+  (current ? t2 = Some ? 〈grid,true〉 ∧
+   ∀l4,newc,mv,l5.
+   〈c1,false〉::l3 ≠ l4@〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv::l5)).  
+*) 
+
 definition weakR_match_tuple ≝ λt1,t2.
   ∀ls,cur,rs.
   t1 = midtape STape ls cur rs → 
diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma
index 43968291b..5286a3340 100644
--- a/matita/matita/lib/turing/universal/uni_step.ma
+++ b/matita/matita/lib/turing/universal/uni_step.ma
@@ -465,18 +465,18 @@ definition uni_step ≝
     tc_true.
 
 definition R_uni_step_true ≝ λt1,t2.
-  ∀n,t0,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv.
-  table_TM (S n) (〈t0,false〉::table) → 
+  ∀n,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv.
+  0 < |table| → table_TM (S n) table → 
   match_in_table (S n) (〈s0,false〉::curconfig) 〈c0,false〉
-    (〈s1,false〉::newconfig) 〈c1,false〉 〈mv,false〉 (〈t0,false〉::table) → 
+    (〈s1,false〉::newconfig) 〈c1,false〉 〈mv,false〉 table → 
   legal_tape ls 〈c0,false〉 rs → 
   t1 = midtape STape (〈grid,false〉::ls) 〈s0,false〉 
-    (curconfig@〈c0,false〉::〈grid,false〉::〈t0,false〉::table@〈grid,false〉::rs) → 
+    (curconfig@〈c0,false〉::〈grid,false〉::table@〈grid,false〉::rs) → 
   ∀t1'.t1' = lift_tape ls 〈c0,false〉 rs → 
   s0 = bit false ∧
   ∃ls1,rs1,c2.
   (t2 = midtape STape (〈grid,false〉::ls1) 〈s1,false〉 
-    (newconfig@〈c2,false〉::〈grid,false〉::〈t0,false〉::table@〈grid,false〉::rs1) ∧
+    (newconfig@〈c2,false〉::〈grid,false〉::table@〈grid,false〉::rs1) ∧
    lift_tape ls1 〈c2,false〉 rs1 = 
    tape_move STape t1' (map_move c1 mv) ∧ legal_tape ls1 〈c2,false〉 rs1).
    
@@ -499,12 +499,14 @@ lemma sem_uni_step :
 [@sem_test_char||]
 [ #intape #outtape 
   #ta whd in ⊢ (%→?); #Hta #HR
-  #n #t0 #table #s0 #s1 #c0 #c1 #ls #rs #curconfig #newconfig #mv
+  #n #fulltable #s0 #s1 #c0 #c1 #ls #rs #curconfig #newconfig #mv
+  #Htable_len cut (∃t0,table. fulltable =〈t0,false〉::table) [(* 0 < |table| *) @daemon]
+  * #t0 * #table #Hfulltable >Hfulltable -fulltable 
   #Htable #Hmatch #Htape #Hintape #t1' #Ht1'
   >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta 
   #Hs0 lapply (\P Hs0) -Hs0 #Hs0 #Hta % //
   cases HR -HR 
-  #tb * whd in ⊢ (%→?); #Htb 
+  #tb * whd in ⊢ (%→?); #Htb
   lapply (Htb (〈grid,false〉::ls) (curconfig@[〈c0,false〉]) (table@〈grid,false〉::rs) s0 t0 ???)
   [ >Hta >associative_append %
   | @daemon
@@ -576,3 +578,4 @@ lemma sem_uni_step :
   cases b in Hb'; normalize #H1 //
 ]
 qed.
+
diff --git a/matita/matita/lib/turing/universal/universal.ma b/matita/matita/lib/turing/universal/universal.ma
index d35283a6f..a2f35fc78 100644
--- a/matita/matita/lib/turing/universal/universal.ma
+++ b/matita/matita/lib/turing/universal/universal.ma
@@ -11,6 +11,7 @@
 
 
 include "turing/universal/trans_to_tuples.ma".
+include "turing/universal/uni_step.ma".
 
 (* definition zero : ∀n.initN n ≝ λn.mk_Sig ?? 0 (le_O_n n). *)
 
@@ -40,15 +41,30 @@ definition low_config: ∀M:normalTM.nconfig (no_states M) → tape STape ≝
   let t ≝ntrans M in 
   let q ≝ cstate … c in
   let q_low ≝  m_bits_of_state n h q in 
-  let current_low ≝
-    match current … (ctape … c) with
-    [ None ⇒ 〈null,false〉
-    | Some b ⇒ 〈bit b,false〉] in
+  let current_low ≝ match current … (ctape … c) with [ None ⇒ null | Some b ⇒ bit b] in
   let low_left ≝ map … (λb.〈bit b,false〉) (left … (ctape …c)) in
   let low_right ≝ map … (λb.〈bit b,false〉) (right … (ctape …c)) in
   let table ≝ flatten ? (tuples_of_pairs n h (graph_enum ?? t)) in
-  mk_tape STape low_left (Some ? 〈grid,false〉) 
-    (q_low@current_low::〈grid,false〉::table@〈grid,false〉::low_right).
+  let right ≝ q_low@〈current_low,false〉::〈grid,false〉::table@〈grid,false〉::low_right in
+  mk_tape STape (〈grid,false〉::low_left) (option_hd … right) (tail … right).
+  
+lemma low_config_eq: ∀t,M,c. t = low_config M c → 
+  ∃low_left,low_right,table,q_low_hd,q_low_tl,c_low.
+  low_left = map … (λb.〈bit b,false〉) (left … (ctape …c)) ∧
+  low_right = map … (λb.〈bit b,false〉) (right … (ctape …c)) ∧
+  table = flatten ? (tuples_of_pairs (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) ∧
+  〈q_low_hd,false〉::q_low_tl = m_bits_of_state (no_states M) (nhalt M) (cstate … c) ∧
+  c_low =  match current … (ctape … c) with [ None ⇒ null| Some b ⇒ bit b] ∧
+  t = midtape STape (〈grid,false〉::low_left) 〈q_low_hd,false〉 (q_low_tl@〈c_low,false〉::〈grid,false〉::table@〈grid,false〉::low_right).
+#t #M #c #eqt
+  @(ex_intro … (map … (λb.〈bit b,false〉) (left … (ctape …c))))
+  @(ex_intro … (map … (λb.〈bit b,false〉) (right … (ctape …c))))
+  @(ex_intro … (flatten ? (tuples_of_pairs (no_states M) (nhalt M) (graph_enum ?? (ntrans M)))))
+  @(ex_intro … (\fst (hd ? (m_bits_of_state (no_states M) (nhalt M) (cstate … c)) 〈bit true,false〉)))
+  @(ex_intro … (tail ? (m_bits_of_state (no_states M) (nhalt M) (cstate … c))))
+  @(ex_intro … (match current … (ctape … c) with [ None ⇒ null| Some b ⇒ bit b]))
+% [% [% [% [% // | // ] | // ] | // ] | >eqt //]
+qed.
 
 definition low_step_R_true ≝ λt1,t2.
   ∀M:normalTM.
@@ -56,6 +72,32 @@ definition low_step_R_true ≝ λt1,t2.
     t1 = low_config M c →
     halt ? M (cstate … c) = false ∧
       t2 = low_config M (step ? M c).
+
+lemma unistep_to_low_step: ∀t1,t2.
+  R_uni_step_true t1 t2 → low_step_R_true t1 t2.
+#t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step #M #c #eqt1
+cases (low_config_eq … eqt1) 
+#low_left * #low_right * #table * #q_low_hd * #q_low_tl * #current_low
+***** #Hlow_left #Hlow_right #Htable #Hq_low #Hcurrent_low #Ht1
+lapply (Huni_step ??????????????? Ht1)
+whd in match (low_config M c);
+
+definition R_uni_step_true ≝ λt1,t2.
+  ∀n,t0,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv.
+  table_TM (S n) (〈t0,false〉::table) → 
+  match_in_table (S n) (〈s0,false〉::curconfig) 〈c0,false〉
+    (〈s1,false〉::newconfig) 〈c1,false〉 〈mv,false〉 (〈t0,false〉::table) → 
+  legal_tape ls 〈c0,false〉 rs → 
+  t1 = midtape STape (〈grid,false〉::ls) 〈s0,false〉 
+    (curconfig@〈c0,false〉::〈grid,false〉::〈t0,false〉::table@〈grid,false〉::rs) → 
+  ∀t1'.t1' = lift_tape ls 〈c0,false〉 rs → 
+  s0 = bit false ∧
+  ∃ls1,rs1,c2.
+  (t2 = midtape STape (〈grid,false〉::ls1) 〈s1,false〉 
+    (newconfig@〈c2,false〉::〈grid,false〉::〈t0,false〉::table@〈grid,false〉::rs1) ∧
+   lift_tape ls1 〈c2,false〉 rs1 = 
+   tape_move STape t1' (map_move c1 mv) ∧ legal_tape ls1 〈c2,false〉 rs1).
+   
     
 definition low_step_R_false ≝ λt1,t2.
   ∀M:normalTM.
-- 
2.39.2