From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 22 Jan 2013 12:21:58 +0000 (+0000)
Subject: Universal machine
X-Git-Tag: make_still_working~1318
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3b280742956d9d62aab53dd81704c250e3befe91;p=helm.git

Universal machine
---

diff --git a/matita/matita/lib/turing/multi_universal/universal.ma b/matita/matita/lib/turing/multi_universal/universal.ma
index 56af5405d..e43851aa3 100644
--- a/matita/matita/lib/turing/multi_universal/universal.ma
+++ b/matita/matita/lib/turing/multi_universal/universal.ma
@@ -9,86 +9,92 @@
      \ /   GNU General Public License Version 2   
       V_____________________________________________________________*)
 
-
+include "turing/simple_machines.ma".
 include "turing/multi_universal/unistep_aux.ma".
 
-axiom sem_unistep: ∀M,cf. unistep ⊨ R_unistep_high M cf.
+axiom sem_unistep: ∀M. unistep ⊨ R_unistep_high M.
 
-definition loop_uni ≝ 
-  ifTM ?? (inject_TM ? (test_char ? (λc.c == bit false)) 2 cfg)
+definition stop ≝ λc.
+  match c with [ bit b ⇒ notb b | _ ⇒ true].
+  
+definition uni_body ≝ 
+  ifTM ?? (mtestR ? cfg 2 stop)
     (single_finalTM ?? unistep)
-    (nop …) tc_true.
+    (nop …) (mtestR_acc ? cfg 2 stop).
+
+definition acc_body : states ?? uni_body ≝ (inr … (inl … (inr … start_nop))).
 
-definition lu_acc : states ?? loop_uni ≝ (inr … (inl … (inr … start_nop))).
+definition ub_R_true ≝ λM,t1,t2.
+  ∀c: nconfig (no_states M). 
+  t1=low_tapes M c→
+    t2=low_tapes M (step FinBool M c) ∧ halt ? M (cstate … c) = false.
+  
+definition ub_R_false ≝ λM,t1,t2.
+  ∀c: nconfig (no_states M).  
+  t1 = low_tapes M c → t1 = t2 ∧ halt ? M (cstate … c) = true.
 
-lemma sem_loop_uni: ∀M,cf.
-  loop_uni ⊨ [lu_acc: R_unistep_high M cf, λt1,t2.t1=t2].
+lemma sem_uni_body: ∀M.
+  uni_body ⊨ [acc_body: ub_R_true M, ub_R_false M].
 #M #cf 
 @(acc_sem_if_app ????????????
-   (sem_test_char_multi ? (λc.c == bit false) 2 cfg (le_S ?? (le_n 1)))
-   (sem_unistep M cf)
+   (sem_mtestR ? cfg 2 stop (le_S ?? (le_n 1)))
+   (sem_unistep M)
    (sem_nop …))
-[#t1 #t2 #t3 * #_ #Ht3 >Ht3 // |#t1 #t2 #t3 * #_ #Ht3 whd in ⊢ (%→?); //]
+[#t1 #t2 #t3 whd in ⊢ (%→?); #Htest #Ht2 * #q #Mt #Ht1
+ >Ht1 in Htest; >cfg_low_tapes whd in match (bits_of_state ???);
+ #Htest lapply (Htest … (refl ??)) * <Ht1 #Ht3 #Hstop >Ht3 in Ht2;
+ #Ht2 % [@Ht2 //] lapply Hstop  whd in match (nhalt ??); 
+ cases (nhalt M q) whd in match (stop ?); * /2/
+|#t1 #t2 #t3 whd in ⊢ (%→?); #Htest #Hnop >Hnop -Hnop * #q #Mt #Ht1 >Ht1 in Htest;
+ >cfg_low_tapes whd in match (bits_of_state ???); 
+ #Htest lapply (Htest … (refl ??)) whd in match (nhalt ??); 
+ cases (nhalt M q) whd in match (stop ?); * /2/ 
+]
 qed.
 
-definition universalTM ≝ whileTM ?? loop_uni lu_acc.
+definition universalTM ≝ whileTM ?? uni_body acc_body.
 
-definition low_R ≝ λM,R.λt1,t2:Vector (tape FSUnialpha) 3.
-    ∀cin. t1 = low_tapes M cin  → 
-    ∃cout. R (ctape … cin) (ctape … cout) ∧
+definition low_R ≝ λM,q,R.λt1,t2:Vector (tape FSUnialpha) 3.
+    ∀Mt. t1 = low_tapes M (mk_config ?? q Mt) → 
+    ∃cout. R Mt (ctape … cout) ∧
     halt ? M (cstate … cout) = true ∧ t2 = low_tapes M cout.
 
-theorem sem_universal: ∀M:normalTM. ∀startc.
-  universalTM ⊫ (low_R M (R_TM FinBool M startc)).
-#M #cin #intape #i #outc #Hloop
-lapply (sem_while … (sem_loop_uni intape i outc Hloop)
-  [@daemon] -Hloop 
-* #ta * #Hstar generalize in match q; -q 
-@(star_ind_l ??????? Hstar)
-  [#tb #q0 whd in ⊢ (%→?); #Htb #tape1 #Htb1
-   cases (Htb … Htb1) -Htb #Hhalt #Htb
-   <Htb >Htb1 @ex_intro 
-   [|%{tape1} %
-     [ % 
-       [ whd @(ex_intro … 1) @(ex_intro … (mk_config … q0 tape1))
-        % [|%] whd in ⊢ (??%?); >Hhalt % 
-       | @Hhalt ]
-     | % ]
-   ]
-  |#tb #tc #td whd in ⊢ (%→?); #Htc #Hstar1 #IH 
-   #q #Htd #tape1 #Htb 
-   lapply (IH (\fst (trans ? M 〈q,current ? tape1〉)) Htd) -IH 
-   #IH cases (Htc … Htb); -Htc #Hhaltq 
-   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) % 
-        [>loopM_unfold >loop_S_false [2://] whd in match (step FinBool ??); 
-         >(eq_pair_fst_snd ?? (trans ???)) @Hloop
+theorem sem_universal: ∀M:normalTM. ∀q.
+  universalTM ⊫ low_R M q (R_TM FinBool M q).
+#M #q #intape #i #outc #Hloop
+lapply (sem_while … (sem_uni_body M … ) intape i outc Hloop) [%] -Hloop 
+* #ta * #Hstar lapply q -q @(star_ind_l ??????? Hstar) -Hstar
+  [#q whd in ⊢ (%→?); #HFalse whd #Mt #Hta 
+   lapply (HFalse … Hta) * #Hta1 #Hhalt %{(mk_config ?? q Mt)} %
+    [%[%{1} %{(mk_config ?? q Mt)} % // whd in ⊢ (??%?); >Hhalt % |@Hhalt]
+    |<Hta1 @Hta  
+    ]
+  |#t1 #t2 whd in ⊢ (%→?); #Hstep #Hstar #IH #q #Hta whd #Mt #Ht1
+   lapply (Hstep … Ht1) * -Hstep #Ht2 #Hhalt
+   lapply(IH (cstate … (step FinBool M (mk_config ?? q Mt))) Hta ??) [@Ht2|skip] -IH 
+   * #cout * * #HRTM #Hhalt1 #Houtc
+   %{cout} 
+   %[%[cases HRTM #k * #outc1 * <config_expand #Hloop #Houtc1
+       %{(S k)} %{outc1} % 
+        [whd in ⊢ (??%?); >Hhalt whd in ⊢ (??%?); @Hloop 
         |@Houtc1
         ]
-      |@Hhaltq1]
+      |@Hhalt1]
     |@Houtc
     ]
-  ]
-*)  
+  ] 
 qed.
   
-qed.
-
 theorem sem_universal2: ∀M:normalTM. ∀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)
+#c * * #HRTM #Hhalt #Ht2 %{c}
 % [% [@(R_TM_to_R … HRTM) @HMR | //] | //]
 qed.
  
 axiom terminate_UTM: ∀M:normalTM.∀t. 
-  M ↓ t → universalTM ↓ (low_config M (mk_config ?? (start ? M) t)).
+  M ↓ t → universalTM ↓ (low_tapes M (mk_config ?? (start ? M) t)).
  
 
 
diff --git a/matita/matita/lib/turing/simple_machines.ma b/matita/matita/lib/turing/simple_machines.ma
new file mode 100644
index 000000000..66ca59a06
--- /dev/null
+++ b/matita/matita/lib/turing/simple_machines.ma
@@ -0,0 +1,73 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic   
+    ||A||  Library of Mathematics, developed at the Computer Science 
+    ||T||  Department of the University of Bologna, Italy.           
+    ||I||                                                            
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_____________________________________________________________*)
+
+include "turing/multi_universal/match.ma".
+
+(********************** look_ahead test *************************)
+
+definition mtestR ≝ λsig,i,n,test.
+  (mmove i sig n R) · 
+    (ifTM ?? (inject_TM ? (test_char ? test) n i)
+    (single_finalTM ?? (mmove i sig n L))
+    (mmove i sig n L) tc_true).
+
+
+(* underspecified *)
+definition RmtestR_true ≝ λsig,i,n,test.λt1,t2:Vector ? n.
+  ∀ls,c,c1,rs.
+    nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
+    t1 = t2 ∧ (test c1 = true).
+
+definition RmtestR_false ≝ λsig,i,n,test.λt1,t2:Vector ? n.
+  ∀ls,c,c1,rs.
+    nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
+    t1 = t2 ∧ (test c1 = false).   
+    
+definition mtestR_acc: ∀sig,i,n,test.states ?? (mtestR sig i n test). 
+#sig #i #n #test @inr @inr @inl @inr @start_nop 
+qed.
+
+lemma sem_mtestR: ∀sig,i,n,test. i ≤ n →
+  mtestR sig i n test ⊨ 
+    [mtestR_acc sig i n test: 
+       RmtestR_true sig  i (S n) test, RmtestR_false sig i (S n) test].
+#sig #i #n #test #Hlein
+@(acc_sem_seq_app sig n … (sem_move_multi … R Hlein)
+   (acc_sem_if sig n ????????
+     (sem_test_char_multi sig test n i Hlein)
+     (sem_move_multi … L Hlein)
+     (sem_move_multi … L Hlein)))
+  [#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in  ⊢ (%→?); * *
+   #cx #Hcx #Htx #Ht2 #ls #c #c1 #rs #Ht1
+   >Ht1 in Hmove; whd in match (tape_move ???); #Ht3 
+   >Ht3 in Hcx; >nth_change_vec [|@le_S_S //] * whd in ⊢ (??%?→?);
+   #Hsome destruct (Hsome) #Htest % [2:@Htest]
+   >Htx in Ht2; whd in ⊢ (%→?); #Ht2 @(eq_vec … (niltape ?))
+   #j #lejn cases (true_or_false (eqb i j)) #Hij
+    [lapply lejn <(eqb_true_to_eq … Hij) #lein >Ht2 >nth_change_vec [2://]
+     >Ht3 >nth_change_vec >Ht1 // 
+    |lapply (eqb_false_to_not_eq … Hij) #Hneq >Ht2 >nth_change_vec_neq [2://]
+     >Ht3 >nth_change_vec_neq //
+    ]
+  |#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in  ⊢ (%→?); *
+   #Hcx #Heqtx #Htx #ls #c #c1 #rs #Ht1
+   >Ht1 in Hmove; whd in match (tape_move ???); #Ht3 
+   >Ht3 in Hcx; >nth_change_vec [2:@le_S_S //] #Hcx lapply (Hcx ? (refl ??)) 
+   #Htest % // @(eq_vec … (niltape ?))
+   #j #lejn cases (true_or_false (eqb i j)) #Hij
+    [lapply lejn <(eqb_true_to_eq … Hij) #lein >Htx >nth_change_vec [2://]
+     >Heqtx >Ht3 >nth_change_vec >Ht1 // 
+    |lapply (eqb_false_to_not_eq … Hij) #Hneq >Htx >nth_change_vec_neq [2://]
+     >Heqtx >Ht3 >nth_change_vec_neq //
+    ]
+  ]
+qed.
+