From e94a85ba0e6313f88f0c1b6b9d28eb4c3294ba52 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 8 Jun 2012 10:49:53 +0000
Subject: [PATCH] A recompiling version

---
 matita/matita/lib/turing/universal/copy.ma    | 14 +++++++---
 .../matita/lib/turing/universal/move_tape.ma  | 12 ++++----
 .../matita/lib/turing/universal/uni_step.ma   |  1 +
 .../matita/lib/turing/universal/universal.ma  | 28 +++----------------
 4 files changed, 21 insertions(+), 34 deletions(-)

diff --git a/matita/matita/lib/turing/universal/copy.ma b/matita/matita/lib/turing/universal/copy.ma
index 331bf6881..5d8f4caab 100644
--- a/matita/matita/lib/turing/universal/copy.ma
+++ b/matita/matita/lib/turing/universal/copy.ma
@@ -10,7 +10,7 @@
       V_____________________________________________________________*)
 
 
-include "turing/universal/tuples.ma".
+include "turing/universal/marks.ma".
 
 definition copy_step_subcase ≝
   λalpha,c,elseM.ifTM ? (test_char ? (λx.x == 〈c,true〉))
@@ -68,7 +68,9 @@ cases (sem_if ? (test_char ? (λx. x == 〈c,true〉)) ?????? tc_true (sem_test_
     #Hth whd in ⊢ (%→?); #Houtc cases (Houtc … Hth) -Houtc
     [ * >Hl1marks [ #Hfalse destruct (Hfalse) ] @memb_append_l2 @memb_hd ]
     * #_ #Houtc lapply (Houtc (reverse ? l1@[〈x,false〉]) 〈a,true〉 l3 ? (refl ??) ?) -Houtc
-    [ #x1 #Hx1 cases (memb_append … Hx1) -Hx1 #Hx1 [ @Hl1marks @memb_append_l1 @daemon | >(memb_single … Hx1) % ]
+    [ #x1 #Hx1 cases (memb_append … Hx1) -Hx1 #Hx1   
+      [@Hl1marks @memb_append_l1 <(reverse_reverse … l1) @memb_reverse @Hx1 
+      |>(memb_single … Hx1) % ]
     | normalize >associative_append % ] 
     #Houtc lapply (\P Hx) -Hx #Hx destruct (Hx) % % [%] >Houtc
     >reverse_append >reverse_reverse >associative_append >associative_append % ]
@@ -154,7 +156,9 @@ cases (sem_if ? (test_char ? (λx:STape.x == 〈null,true〉)) ?????? tc_true
     #Hth whd in ⊢ (%→?); #Houtc cases (Houtc … Hth) -Houtc
     [ * >Hl1marks [ #Hfalse destruct (Hfalse) ] @memb_append_l2 @memb_hd ]
     * #_ #Houtc lapply (Houtc (reverse ? l1@[〈x,false〉]) 〈a,true〉 l3 ? (refl ??) ?) -Houtc
-    [ #x1 #Hx1 cases (memb_append … Hx1) -Hx1 #Hx1 [ @Hl1marks @memb_append_l1 @daemon | >(memb_single … Hx1) % ]
+    [ #x1 #Hx1 cases (memb_append … Hx1) -Hx1 #Hx1
+      [@Hl1marks @memb_append_l1 <(reverse_reverse … l1) @memb_reverse @Hx1 
+      |>(memb_single … Hx1) % ]
     | normalize >associative_append % ] 
     #Houtc lapply (\P Hx) -Hx #Hx destruct (Hx) % % [%] >Houtc
     >reverse_append >reverse_reverse >associative_append >associative_append % ]
@@ -272,6 +276,8 @@ lemma inj_append_singleton_l2 :
 >reverse_append >reverse_append normalize #H1 destruct %
 qed.
 
+axiom daemon : ∀P:Prop.P.
+
 lemma wsem_copy0 : WRealize ? copy0 R_copy0.
 #intape #k #outc #Hloop 
 lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop
@@ -292,7 +298,7 @@ lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop
   #Hl1 #Hl1bits #l4' #bg #Hl4 #Hl4bits %2
   cases (Htc … Htb) -Htc #Hcbitnull #Htc
   % [ % #Hc' >Hc' in Hcbitnull; normalize #Hfalse destruct (Hfalse) ]
-  cut (|l1| = |reverse ? l4|) [@daemon] #Hlen1
+  cut (|l1| = |reverse ? l4|) [>length_reverse @Hlen] #Hlen1
   @(list_cases2 … Hlen1)
   [ (* case l1 = [] is discriminated because l1 contains at least comma *)
     #Hl1nil @False_ind >Hl1nil in Hl1; cases l1' normalize
diff --git a/matita/matita/lib/turing/universal/move_tape.ma b/matita/matita/lib/turing/universal/move_tape.ma
index 9ad227dbe..ecc9fa208 100644
--- a/matita/matita/lib/turing/universal/move_tape.ma
+++ b/matita/matita/lib/turing/universal/move_tape.ma
@@ -9,8 +9,8 @@
      \ /   GNU General Public License Version 2   
       V_____________________________________________________________*)
 
-include "turing/universal/move_char_c.ma".
-include "turing/universal/move_char_l.ma".
+include "turing/move_char.ma".
+include "turing/universal/marks.ma".
 include "turing/universal/tuples.ma".
 
 definition init_cell_states ≝ initN 2.
@@ -197,7 +197,7 @@ MOVE TAPE LEFT:
 *)
 definition mtl_aux ≝ 
   seq ? (swap STape 〈grid,false〉)
-   (seq ? (move_r …) (seq ? (move_r …) (seq ? (move_char_c STape 〈grid,false〉) (move_l …)))).
+   (seq ? (move_r …) (seq ? (move_r …) (seq ? (move_char_r STape 〈grid,false〉) (move_l …)))).
 definition R_mtl_aux ≝ λt1,t2.
   ∀l1,l2,l3,r. t1 = midtape STape l1 r (〈grid,false〉::l2@〈grid,false〉::l3) → no_grids l2 → 
   t2 = midtape STape (reverse ? l2@〈grid,false〉::l1) r (〈grid,false〉::l3).
@@ -205,7 +205,7 @@ definition R_mtl_aux ≝ λt1,t2.
 lemma sem_mtl_aux : Realize ? mtl_aux R_mtl_aux.
 #intape 
 cases (sem_seq … (sem_swap STape 〈grid,false〉) (sem_seq … (sem_move_r …)
-        (sem_seq … (sem_move_r …) (sem_seq … (ssem_move_char_c STape 〈grid,false〉) 
+        (sem_seq … (sem_move_r …) (sem_seq … (ssem_move_char_r STape 〈grid,false〉) 
           (sem_move_l …)))) intape)
 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
 #l1 #l2 #l3  #r #Hintape #Hl2
@@ -340,14 +340,14 @@ cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Htapein)
 qed.
 
 (*definition mtl_aux ≝ 
-  seq ? (move_r …) (seq ? (move_char_c STape 〈grid,false〉) (move_l …)).
+  seq ? (move_r …) (seq ? (move_char_r STape 〈grid,false〉) (move_l …)).
 definition R_mtl_aux ≝ λt1,t2.
   ∀l1,l2,l3,r. t1 = midtape STape l1 r (l2@〈grid,false〉::l3) → no_grids l2 → 
   t2 = midtape STape (reverse ? l2@l1) r (〈grid,false〉::l3).
 
 lemma sem_mtl_aux : Realize ? mtl_aux R_mtl_aux.
 #intape 
-cases (sem_seq … (sem_move_r …) (sem_seq … (ssem_move_char_c STape 〈grid,false〉) (sem_move_l …)) intape)
+cases (sem_seq … (sem_move_r …) (sem_seq … (ssem_move_char_r STape 〈grid,false〉) (sem_move_l …)) intape)
 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
 #l1 #l2 #l3  #r #Hintape #Hl2
 cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta #Hta
diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma
index b28efc472..395decac2 100644
--- a/matita/matita/lib/turing/universal/uni_step.ma
+++ b/matita/matita/lib/turing/universal/uni_step.ma
@@ -16,6 +16,7 @@
 
 include "turing/universal/copy.ma".
 include "turing/universal/move_tape.ma".
+include "turing/universal/match_machines.ma".
 
 (*
 
diff --git a/matita/matita/lib/turing/universal/universal.ma b/matita/matita/lib/turing/universal/universal.ma
index 5ffbc8d4e..3350b0965 100644
--- a/matita/matita/lib/turing/universal/universal.ma
+++ b/matita/matita/lib/turing/universal/universal.ma
@@ -10,30 +10,10 @@
       V_____________________________________________________________*)
 
 
-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). *)
 
-record normalTM : Type[0] ≝ 
-{ no_states : nat;
-  pos_no_states : (0 < no_states); 
-  ntrans : trans_source no_states → trans_target no_states;
-  nhalt : initN no_states → bool
-}.
-
-definition normalTM_to_TM ≝ λM:normalTM.
-  mk_TM FinBool (initN (no_states M)) 
-   (ntrans M) (mk_Sig ?? 0 (pos_no_states M)) (nhalt M).
-
-coercion normalTM_to_TM.
-
-definition nconfig ≝ λn. config FinBool (initN n).
-
-(* 
-definition normalTM ≝ λn,t,h. 
-  λk:0<n.mk_TM FinBool (initN n) t (mk_Sig ?? 0 k) h. *)
-
 definition low_config: ∀M:normalTM.nconfig (no_states M) → tape STape ≝ 
 λM:normalTM.λc.
   let n ≝ no_states M in
@@ -44,7 +24,7 @@ definition low_config: ∀M:normalTM.nconfig (no_states M) → tape STape ≝
   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
+  let table ≝ flatten ? (tuples_list n h (graph_enum ?? t)) in
   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).
   
@@ -52,14 +32,14 @@ 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))) ∧
+  table = flatten ? (tuples_list (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 … (flatten ? (tuples_list (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]))
@@ -282,7 +262,7 @@ lemma current_of_low:∀M,tape,ls,c,rs. legal_tape ls c rs →
 (* sufficent conditions to have a low_level_config *)
 lemma is_low_config: ∀ls,c,rs,M,s,tape,qhd,q_tl,table.
 legal_tape ls c rs →
-table = flatten ? (tuples_of_pairs (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) →
+table = flatten ? (tuples_list (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) →
 lift_tape ls c rs = low_tape_aux M tape →
 〈qhd,false〉::q_tl = m_bits_of_state (no_states M) (nhalt M) s →
 midtape STape (〈grid,false〉::ls) 
-- 
2.39.2