X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Funiversal.ma;h=2b8618213bbd673e160fc57b076bcd08d54f6d59;hb=4d5f398cd2818b9eee57d6efdbb49a51d4a97a76;hp=3f8d2910ce2389e25adfea32a13b154b2361b867;hpb=c62c83d3be87bfb0744902a5998e5708bc698cd7;p=helm.git

diff --git a/matita/matita/lib/turing/universal/universal.ma b/matita/matita/lib/turing/universal/universal.ma
index 3f8d2910c..2b8618213 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]))
@@ -141,18 +121,9 @@ definition high_move ≝ λc,mv.
   | _ ⇒ None ?
   ].
 
-(* lemma high_of_lift ≝ ∀ls,c,rs.
-  high_tape ls c rs = *)
-
 definition map_move ≝ 
   λc,mv.match c with [ null ⇒ None ? | _ ⇒ Some ? 〈c,false,move_of_unialpha mv〉 ].
 
-(* axiom high_tape_move : ∀t1,ls,c,rs, c1,mv.
-  legal_tape ls c rs →
-  t1 = lift_tape ls c rs →
-  high_tape_from_tape (tape_move STape t1 (map_move c1 mv)) =
-    tape_move FinBool (high_tape_from_tape t1) (high_move c1 mv). *)
-
 definition low_step_R_true ≝ λt1,t2.
   ∀M:normalTM.
   ∀c: nconfig (no_states M). 
@@ -282,7 +253,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) 
@@ -301,7 +272,7 @@ midtape STape (〈grid,false〉::ls)
   ]
 qed.
 
-lemma unistep_to_low_step: ∀t1,t2.
+lemma unistep_true_to_low_step: ∀t1,t2.
   R_uni_step_true t1 t2 → low_step_R_true t1 t2.
 #t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step * #n #posn #t #h * #qin #tape #eqt1
 cases (low_config_eq … eqt1) 
@@ -331,7 +302,7 @@ lapply (Huni_step n table q_low_hd (\fst qout_low_hd)
   [whd in ⊢ (??%?); >q_low_head_false in Hq_low; 
    whd in ⊢ ((???%)→?); generalize in match (h qin);
    #x #H destruct (H) %
-  |>Ht2 whd in match (step ???); 
+  |>Ht2 whd in match (step FinBool ??); 
    whd in match (trans ???); 
    >(eq_pair_fst_snd … (t ?))
    @is_low_config // >Hlift
@@ -344,41 +315,38 @@ lapply (Huni_step n table q_low_hd (\fst qout_low_hd)
     ]
   ]
 qed.
-    
+
 definition low_step_R_false ≝ λt1,t2.
   ∀M:normalTM.
   ∀c: nconfig (no_states M).  
     t1 = low_config M c → halt ? M (cstate … c) = true  ∧ t1 = t2.
 
+lemma unistep_false_to_low_step: ∀t1,t2.
+  R_uni_step_false t1 t2 → low_step_R_false t1 t2.
+#t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step * #n #posn #t #h * #qin #tape #eqt1
+cases (low_config_eq … eqt1) #low_left * #low_right * #table * #q_low_hd * #q_low_tl * #current_low
+***** #_ #_ #_ #Hqin #_ #Ht1 whd in match (halt ???);
+cases (Huni_step (h qin) ?) [/2/] >Ht1 whd in ⊢ (??%?); @eq_f
+normalize in Hqin; destruct (Hqin) %
+qed.
+
 definition low_R ≝ λM,qstart,R,t1,t2.
     ∀tape1. t1 = low_config M (mk_config ?? qstart tape1) → 
     ∃q,tape2.R tape1 tape2 ∧
     halt ? M q = true ∧ t2 = low_config M (mk_config ?? q tape2).
 
-definition R_TM ≝ λsig.λM:TM sig.λq.λt1,t2.
-∃i,outc.
-  loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (mk_config ?? q t1) = Some ? outc ∧ 
-  t2 = (ctape ?? outc).
-
-(*
-definition universal_R ≝ λM,R,t1,t2. 
-    Realize ? M R →    
-    ∀tape1,tape2.
-    R tape1 tape 2 ∧
-    t1 = low_config M (initc ? M tape1) ∧
-    ∃q.halt ? M q = true → t2 = low_config M (mk_config ?? q tape2).*)
-
-axiom uni_step: TM STape.
-axiom us_acc: states ? uni_step.
-
-axiom sem_uni_step: accRealize ? uni_step us_acc low_step_R_true low_step_R_false.
+lemma sem_uni_step1: 
+  uni_step ⊨ [us_acc: low_step_R_true, low_step_R_false].
+@(acc_Realize_to_acc_Realize … sem_uni_step) 
+  [@unistep_true_to_low_step | @unistep_false_to_low_step ]
+qed. 
 
 definition universalTM ≝ whileTM ? uni_step us_acc.
 
 theorem sem_universal: ∀M:normalTM. ∀qstart.
-  WRealize ? universalTM (low_R M qstart (R_TM FinBool M qstart)).
+  universalTM ⊫ (low_R M qstart (R_TM FinBool M qstart)).
 #M #q #intape #i #outc #Hloop
-lapply (sem_while … sem_uni_step intape i outc Hloop)
+lapply (sem_while … sem_uni_step1 intape i outc Hloop)
   [@daemon] -Hloop 
 * #ta * #Hstar generalize in match q; -q 
 @(star_ind_l ??????? Hstar)
@@ -396,14 +364,14 @@ lapply (sem_while … sem_uni_step intape i outc Hloop)
    #q #Htd #tape1 #Htb 
    lapply (IH (\fst (trans ? M 〈q,current ? tape1〉)) Htd) -IH 
    #IH cases (Htc … Htb); -Htc #Hhaltq 
-   whd in match (step ???); >(eq_pair_fst_snd ?? (trans ???)) 
+   whd in match (step FinBool ??); >(eq_pair_fst_snd ?? (trans ???)) 
    #Htc change with (mk_config ????) in Htc:(???(??%)); 
    cases (IH ? Htc) #q1 * #tape2 * * #HRTM #Hhaltq1 #Houtc
    @(ex_intro … q1) @(ex_intro … tape2) % 
     [%
       [cases HRTM #k * #outc1 * #Hloop #Houtc1
        @(ex_intro … (S k)) @(ex_intro … outc1) % 
-        [>loop_S_false [2://] whd in match (step ???); 
+        [>loopM_unfold >loop_S_false [2://] whd in match (step FinBool ??); 
          >(eq_pair_fst_snd ?? (trans ???)) @Hloop
         |@Houtc1
         ]
@@ -413,20 +381,14 @@ lapply (sem_while … sem_uni_step intape i outc Hloop)
   ]
 qed.
 
-lemma R_TM_to_R: ∀sig,M,R. ∀t1,t2. 
-  WRealize sig M R → R_TM ? M (start ? M) t1 t2 → R t1 t2.
-#sig #M #R #t1 #t2 whd in ⊢ (%→?); #HMR * #i * #outc *
-#Hloop #Ht2 >Ht2 @(HMR … Hloop)
-qed.
-
-axiom WRealize_to_WRealize: ∀sig,M,R1,R2.
-  (∀t1,t2.R1 t1 t2 → R2 t1 t2) → WRealize sig M R1 → WRealize ? M R2.
-
 theorem sem_universal2: ∀M:normalTM. ∀R.
-  WRealize ? M R → WRealize ? universalTM (low_R M (start ? M) R).
+  M ⊫ R → universalTM ⊫ (low_R M (start ? M) R).
 #M #R #HMR lapply (sem_universal … M (start ? M)) @WRealize_to_WRealize
 #t1 #t2 whd in ⊢ (%→%); #H #tape1 #Htape1 cases (H ? Htape1)
 #q * #tape2 * * #HRTM #Hhalt #Ht2 @(ex_intro … q) @(ex_intro … tape2)
 % [% [@(R_TM_to_R … HRTM) @HMR | //] | //]
 qed.
  
+axiom terminate_UTM: ∀M:normalTM.∀t. 
+  M ↓ t → universalTM ↓ (low_config M (mk_config ?? (start ? M) t)).
+