(* *)
(**************************************************************************)
-include "turing/turing.ma".
+include "turing/multi_universal/moves.ma".
+include "turing/if_multi.ma".
include "turing/inject.ma".
-include "turing/while_multi.ma".
+include "turing/basic_machines.ma".
definition compare_states ≝ initN 3.
definition R_compare ≝
λi,j,sig,n.λint,outt: Vector (tape sig) (S n).
- (current sig (nth i (tape sig) int (niltape sig))
- ≠current sig (nth j (tape sig) int (niltape sig)) →
- outt = int) ∧
+ ((current ? (nth i ? int (niltape ?))
+ ≠ current ? (nth j ? int (niltape ?)) ∨
+ current ? (nth i ? int (niltape ?)) = None ? ∨
+ current ? (nth j ? int (niltape ?)) = None ?) → outt = int) ∧
(∀ls,x,xs,ci,rs,ls0,cj,rs0.
nth i ? int (niltape ?) = midtape sig ls x (xs@ci::rs) →
nth j ? int (niltape ?) = midtape sig ls0 x (xs@cj::rs0) → ci ≠ cj →
outt = change_vec ??
(change_vec ?? int (midtape sig (reverse ? xs@x::ls) ci rs) i)
(midtape sig (reverse ? xs@x::ls0) cj rs0) j).
-
+
lemma wsem_compare : ∀i,j,sig,n.i ≠ j → i < S n → j < S n →
compare i j sig n ⊫ R_compare i j sig n.
#i #j #sig #n #Hneq #Hi #Hj #ta #k #outc #Hloop
lapply (sem_while … (sem_comp_step i j sig n Hneq Hi Hj) … Hloop) //
-Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
[ #tc whd in ⊢ (%→?); * * [ *
- [ #Hcicj #Houtc %
+ [ #Hcicj #Houtc %
[ #_ @Houtc
| #ls #x #xs #ci #rs #ls0 #cj #rs0 #Hnthi #Hnthj
>Hnthi in Hcicj; >Hnthj normalize in ⊢ (%→?); * #H @False_ind @H %
normalize in ⊢ (%→?); #H destruct (H) ] ]
| #tc #td #te * #x * * #Hci #Hcj #Hd #Hstar #IH #He lapply (IH He) -IH *
#IH1 #IH2 %
- [ >Hci >Hcj * #H @False_ind @H %
+ [ >Hci >Hcj * [* [* #H @False_ind @H % | #H destruct (H)] | #H destruct (H)]
| #ls #c0 #xs #ci #rs #ls0 #cj #rs0 cases xs
[ #Hnthi #Hnthj #Hcicj >IH1
[ >Hd @eq_f3 //
| >(?:c0=x) [ >Hnthj % ]
>Hnthi in Hci;normalize #H destruct (H) % ]
| >Hd >nth_change_vec // >nth_change_vec_neq [|@sym_not_eq //]
- >nth_change_vec // >Hnthi >Hnthj normalize @(not_to_not ??? Hcicj)
+ >nth_change_vec // >Hnthi >Hnthj normalize %1 %1 @(not_to_not ??? Hcicj)
#H destruct (H) % ]
| #x0 #xs0 #Hnthi #Hnthj #Hcicj
>(IH2 (c0::ls) x0 xs0 ci rs (c0::ls0) cj rs0 … Hcicj)
#i #j #sig #n #Hneq #Hi #Hj @WRealize_to_Realize /2/
qed.
+(*
+ |conf1 $
+ |confin 0/1 confout move
+
+ match machine step ≝
+ compare;
+ if (cur(src) != $)
+ then
+ parmoveL;
+ moveR(dst);
+ else nop
+ *)
+
+definition match_step ≝ λsrc,dst,sig,n,is_startc,is_endc.
+ compare src dst sig n ·
+ (ifTM ?? (inject_TM ? (test_char ? (λa.is_endc a == false)) n src)
+ (single_finalTM ??
+ (parmove src dst sig n L is_startc · (inject_TM ? (move_r ?) n dst)))
+ (nop …)
+ tc_true).
+
+definition Rtc_multi_true ≝
+ λalpha,test,n,i.λt1,t2:Vector ? (S n).
+ (∃c. current alpha (nth i ? t1 (niltape ?)) = Some ? c ∧ test c = true) ∧ t2 = t1.
+
+definition Rtc_multi_false ≝
+ λalpha,test,n,i.λt1,t2:Vector ? (S n).
+ (∀c. current alpha (nth i ? t1 (niltape ?)) = Some ? c → test c = false) ∧ t2 = t1.
+
+definition R_match_step_false ≝
+ λsrc,dst,sig,n,is_endc.λint,outt: Vector (tape sig) (S n).
+ ((current ? (nth src ? int (niltape ?)) ≠ current ? (nth dst ? int (niltape ?)) ∨
+ current sig (nth src (tape sig) int (niltape sig)) = None ? ∨
+ current sig (nth dst (tape sig) int (niltape sig)) = None ? ) ∧ outt = int) ∨
+ ∃ls,ls0,rs,rs0,x,xs. ∀rsi,rsj,end,c.
+ rs = end::rsi → rs0 = c::rsj →
+ is_endc end = true ∧
+ nth src ? int (niltape ?) = midtape sig ls x (xs@rs) ∧
+ nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) ∧
+ outt = change_vec ??
+ (change_vec ?? int (midtape sig (reverse ? xs@x::ls) end rsi) src)
+ (midtape sig (reverse ? xs@x::ls0) c rsj) dst.
+
+definition R_match_step_true ≝
+ λsrc,dst,sig,n,is_startc,is_endc.λint,outt: Vector (tape sig) (S n).
+ ∀s.current sig (nth src (tape sig) int (niltape sig)) = Some ? s →
+ is_startc s = true →
+ (∀s1.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s1 →
+ s ≠ s1 →
+ outt = change_vec ?? int
+ (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈s1,R〉)) dst ∧ is_endc s = false) ∧
+ (∀ls,x,xs,ci,rs,ls0,cj,rs0.
+ nth src ? int (niltape ?) = midtape sig ls x (xs@ci::rs) →
+ nth dst ? int (niltape ?) = midtape sig ls0 x (xs@cj::rs0) → ci ≠ cj →
+ outt = change_vec ?? int
+ (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈x,R〉)) dst ∧ is_endc ci = false).
+
+lemma sem_test_char_multi :
+ ∀alpha,test,n,i.i ≤ n →
+ inject_TM ? (test_char ? test) n i ⊨
+ [ tc_true : Rtc_multi_true alpha test n i, Rtc_multi_false alpha test n i ].
+#alpha #test #n #i #Hin #int
+cases (acc_sem_inject … Hin (sem_test_char alpha test) int)
+#k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ %
+[ @Hloop
+| #Hqtrue lapply (Htrue Hqtrue) * * * #c *
+ #Hcur #Htestc #Hnth_i #Hnth_j %
+ [ %{c} % //
+ | @(eq_vec … (niltape ?)) #i0 #Hi0
+ cases (decidable_eq_nat i0 i) #Hi0i
+ [ >Hi0i @Hnth_i
+ | @sym_eq @Hnth_j @sym_not_eq // ] ] ]
+| #Hqfalse lapply (Hfalse Hqfalse) * * #Htestc #Hnth_i #Hnth_j %
+ [ @Htestc
+ | @(eq_vec … (niltape ?)) #i0 #Hi0
+ cases (decidable_eq_nat i0 i) #Hi0i
+ [ >Hi0i @Hnth_i
+ | @sym_eq @Hnth_j @sym_not_eq // ] ] ]
+qed.
+
+axiom comp_list: ∀S:DeqSet. ∀l1,l2:list S. ∃l,tl1,tl2.
+ l1 = l@tl1 ∧ l2 = l@tl2 ∧ ∀a,b,tla,tlb. tl1 = a::tla → tl2 = b::tlb → a≠b.
+
+axiom daemon : ∀X:Prop.X.
+
+lemma sem_match_step :
+ ∀src,dst,sig,n,is_startc,is_endc.src ≠ dst → src < S n → dst < S n →
+ match_step src dst sig n is_startc is_endc ⊨
+ [ inr ?? (inr ?? (inl … (inr ?? start_nop))) :
+ R_match_step_true src dst sig n is_startc is_endc,
+ R_match_step_false src dst sig n is_endc ].
+#src #dst #sig #n #is_startc #is_endc #Hneq #Hsrc #Hdst
+@(acc_sem_seq_app sig n … (sem_compare src dst sig n Hneq Hsrc Hdst)
+ (acc_sem_if ? n … (sem_test_char_multi sig (λa.is_endc a == false) n src (le_S_S_to_le … Hsrc))
+ (sem_seq …
+ (sem_parmoveL ???? is_startc Hneq Hsrc Hdst)
+ (sem_inject … dst (le_S_S_to_le … Hdst) (sem_move_r ? )))
+ (sem_nop …)))
+[#ta #tb #tc * #Hcomp1 #Hcomp2 * #td * * * #c * #Hcurtc #Hcend #Htd >Htd -Htd
+ #Htb #s #Hcurta_src #Hstart %
+ [ #s1 #Hcurta_dst #Hneqss1
+ lapply Htb lapply Hcurtc -Htb -Hcurtc >(?:tc=ta)
+ [|@Hcomp1 % % >Hcurta_src >Hcurta_dst @(not_to_not … Hneqss1) #H destruct (H) % ]
+ #Hcurtc * #te * * #_ #Hte >Hte // whd in ⊢ (%→?); * * #_ #Htbdst #Htbelse %
+ [ @(eq_vec … (niltape ?)) #i #Hi cases (decidable_eq_nat i dst) #Hidst
+ [ >Hidst >nth_change_vec // cases (current_to_midtape … Hcurta_dst)
+ #ls * #rs #Hta_mid >(Htbdst … Hta_mid) >Hta_mid cases rs //
+ | >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @Htbelse @sym_not_eq // ]
+ | >Hcurtc in Hcurta_src; #H destruct (H) cases (is_endc s) in Hcend;
+ normalize #H destruct (H) // ]
+ |#ls #x #xs #ci #rs #ls0 #cj #rs0 #Htasrc_mid #Htadst_mid #Hcicj
+ lapply (Hcomp2 … Htasrc_mid Htadst_mid Hcicj) -Hcomp2 #Hcomp2
+ cases Htb #td * * #Htd #_ >Htasrc_mid in Hcurta_src; normalize in ⊢ (%→?);
+ #H destruct (H)
+ >(Htd ls ci (reverse ? xs) rs s ??? ls0 cj (reverse ? xs) s rs0 (refl ??)) //
+ [| >Hcomp2 >nth_change_vec //
+ | @daemon
+ | >Hcomp2 >nth_change_vec_neq [|@sym_not_eq // ] @nth_change_vec // ]
+ * * #_ #Htbdst #Htbelse %
+ [ @(eq_vec … (niltape ?)) #i #Hi cases (decidable_eq_nat i dst) #Hidst
+ [ >Hidst >nth_change_vec // >Htadst_mid >(Htbdst ls0 s (xs@cj::rs0))
+ [ cases xs //
+ | >nth_change_vec // ]
+ | >nth_change_vec_neq [|@sym_not_eq //]
+ <Htbelse [|@sym_not_eq // ]
+ >nth_change_vec_neq [|@sym_not_eq //]
+ STOP.
+
+ >nth_change_vec in Htbdst; // #Htbdst >(Htbdst
+ … Htadst_mid) >Hta_mid cases rs //
+ | >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @Htbelse @sym_not_eq // ]
+ | >Hcurtc in Hcurta_src; #H destruct (H) cases (is_endc s) in Hcend;
+ normalize #H destruct (H) // ]
+|#intape #outtape #ta * #Hcomp1 #Hcomp2 * #tb * * #Hc #Htb
+ whd in ⊢ (%→?); #Hout >Hout >Htb whd
+ lapply (current_to_midtape sig (nth src ? intape (niltape ?)))
+ cases (current … (nth src ? intape (niltape ?))) in Hcomp1;
+ [#Hcomp1 #_ %1 % [%1 %2 // | @Hcomp1 %1 %2 %]
+ |#c_src lapply (current_to_midtape sig (nth dst ? intape (niltape ?)))
+ cases (current … (nth dst ? intape (niltape ?)))
+ [#_ #Hcomp1 #_ %1 % [%2 % | @Hcomp1 %2 %]
+ |#c_dst cases (true_or_false (c_src == c_dst)) #Hceq
+ [#Hmid_dst cases (Hmid_dst c_dst (refl …)) -Hmid_dst
+ #ls_dst * #rs_dst #Hmid_dst #_
+ #Hmid_src cases (Hmid_src c_src (refl …)) -Hmid_src
+ #ls_src * #rs_src #Hmid_src %2
+ cases (comp_list … rs_src rs_dst) #xs * #rsi * #rsj * *
+ #Hrs_src #Hrs_dst #Hneq
+ %{ls_src} %{ls_dst} %{rsi} %{rsj} %{c_src} %{xs}
+ #rsi0 #rsj0 #end #c #Hend #Hc_dst
+ >Hrs_src in Hmid_src; >Hend #Hmid_src
+ >Hrs_dst in Hmid_dst; >Hc_dst <(\P Hceq) #Hmid_dst
+ lapply(Hcomp2 … Hmid_src Hmid_dst ?)
+ [@(Hneq … Hend Hc_dst)]
+ -Hcomp2 #Hcomp2 <Hcomp2
+ % // % [ %
+ [>Hcomp2 in Hc; >nth_change_vec_neq [|@sym_not_eq //]
+ >nth_change_vec // #H lapply (H ? (refl …))
+ cases (is_endc end) normalize //
+ |@Hmid_src]
+ |@Hmid_dst]
+ |#_ #Hcomp1 #_ %1 %
+ [% % @(not_to_not ??? (\Pf Hceq)) #H destruct (H) //
+ |@Hcomp1 %1 %1 @(not_to_not ??? (\Pf Hceq)) #H destruct (H) //
+ ]
+ ]
+ ]
+ ]
+
+
+2:#t1 #t2 #t3 whd in ⊢ (%→?); * #Hc #H #H1 whd #ls #c #rs #Ht1 %
+ [lapply(Hc c ?) [>Ht1 %] #Hgrid @injective_notb @Hgrid |>H1 @H]
+
+
+
+