(******************* inject a mono machine into a multi tape one **********************)
definition inject_trans ≝ λsig,states:FinSet.λn,i:nat.
- λtrans:states × (option sig) → states × (option (sig × move)).
+ λtrans:states × (option sig) → states × (option sig × move).
λp:states × (Vector (option sig) (S n)).
let 〈q,a〉 ≝ p in
let 〈nq,na〉 ≝ trans 〈q,nth i ? a (None ?)〉 in
definition inject_TM ≝ λsig.λM:TM sig.λn,i.
mk_mTM sig n
(states ? M)
- (inject_trans ?? n i (trans ? M))
+ (inject_trans sig (states ? M) n i ?) (* (trans sig M))*)
(start ? M)
(halt ? M).
+(* ????? *)
+lapply (trans sig M) #trans #x lapply (trans x) * *
+#s #a #m % [ @s | % [ @a | @m ] ]
+qed.
axiom current_chars_change_vec: ∀sig,n,v,a,i. i < S n →
current_chars sig ? (change_vec ? (S n) v a i) =
change_vec ? (S n)(current_chars ?? v) (current ? a) i.
-
+
lemma inject_trans_def :∀sig:FinSet.∀n,i:nat.i < S n →
- ∀M,v,s,a,sn,an.
- trans sig M 〈s,a〉 = 〈sn,an〉 →
+ ∀M,v,s,a,sn,an,mn.
+ trans sig M 〈s,a〉 = 〈sn,an,mn〉 →
cic:/matita/turing/turing/trans.fix(0,2,9) sig n (inject_TM sig M n i) 〈s,change_vec ? (S n) v a i〉 =
- 〈sn,change_vec ? (S n) (null_action ? n) an i〉.
-#sig #n #i #Hlt #trans #v #s #a #sn #an #Htrans
+ 〈sn,change_vec ? (S n) (null_action ? n) 〈an,mn〉 i〉.
+#sig #n #i #Hlt #M #v #s #a #sn #an #mn #Htrans
whd in ⊢ (??%?); >nth_change_vec // >Htrans //
qed.
-lemma inject_step : ∀sig,n,M,i,q,t,nq,nt,v. i < S n →
+
+axiom inject_step : ∀sig,n,M,i,q,t,nq,nt,v. i < S n →
step sig M (mk_config ?? q t) = mk_config ?? nq nt →
- cic:/matita/turing/turing/step.def(10) sig n (inject_TM sig M n i)
+ cic:/matita/turing/turing/step.def(11) sig n (inject_TM sig M n i)
(mk_mconfig ?? n q (change_vec ? (S n) v t i))
= mk_mconfig ?? n nq (change_vec ? (S n) v nt i).
-#sig #n #M #i #q #t #nq #nt #v #lein whd in ⊢ (??%?→?);
+(*#sig #n #M #i #q #t #nq #nt #v #lein whd in ⊢ (??%?→?);
whd in match (step ????); >(current_chars_change_vec … lein)
>(eq_pair_fst_snd … (trans sig M ?)) whd in ⊢ (??%?→?); #H
->(inject_trans_def sig n i lein M … (eq_pair_fst_snd … ))
+>(inject_trans_def sig n i lein M …)
+[|>(eq_pair_fst_snd ?? (trans sig M 〈q,current sig t〉))
+ >(eq_pair_fst_snd ?? (\fst (trans sig M 〈q,current sig t〉))) %
+| *: skip ]
whd in ⊢ (??%?); @eq_f2 [destruct (H) // ]
@(eq_vec … (niltape ?)) #i0 #lei0n
cases (decidable_eq_nat … i i0) #Hii0
| >nth_change_vec_neq // >pmap_change >nth_change_vec_neq
>tape_move_null_action //
]
-qed.
+qed. *)
lemma halt_inject: ∀sig,n,M,i,x.
cic:/matita/turing/turing/halt.fix(0,2,9) sig n (inject_TM sig M n i) x
lemma loop_inject: ∀sig,n,M,i,k,ins,int,outs,outt,vt.i < S n →
loopM sig M k (mk_config ?? ins int) = Some ? (mk_config ?? outs outt) →
- cic:/matita/turing/turing/loopM.def(11) sig n (inject_TM sig M n i) k (mk_mconfig ?? n ins (change_vec ?? vt int i))
+ cic:/matita/turing/turing/loopM.def(12) sig n (inject_TM sig M n i) k (mk_mconfig ?? n ins (change_vec ?? vt int i))
=Some ? (mk_mconfig sig ? n outs (change_vec ?? vt outt i)).
#sig #n #M #i #k elim k -k
[#ins #int #outs #outt #vt #Hin normalize in ⊢ (%→?); #H destruct
| N ⇒ t
].
+definition tape_move_mono ≝
+ λsig,t,mv.
+ tape_move sig (tape_write sig t (\fst mv)) (\snd mv).
+
record config (sig,states:FinSet): Type[0] ≝
{ cstate : states;
ctape: tape sig
*)
definition trans_compare_step ≝
- λi,j.λsig:FinSet.λn.λis_endc.
+ λi,j.λsig:FinSet.λn.
λp:compare_states × (Vector (option sig) (S n)).
let 〈q,a〉 ≝ p in
match pi1 … q with
[ O ⇒ match nth i ? a (None ?) with
- [ None ⇒ 〈comp2,null_action ? n〉
+ [ None ⇒ 〈comp2,null_action sig n〉
| Some ai ⇒ match nth j ? a (None ?) with
[ None ⇒ 〈comp2,null_action ? n〉
- | Some aj ⇒ if notb (is_endc ai) ∧ ai == aj
+ | Some aj ⇒ if ai == aj
then 〈comp1,change_vec ? (S n)
- (change_vec ? (S n) (null_action ? n) (Some ? 〈ai,R〉) i)
- (Some ? 〈aj,R〉) j〉
+ (change_vec ? (S n) (null_action ? n) (〈None ?,R〉) i)
+ (〈None ?,R〉) j〉
else 〈comp2,null_action ? n〉 ]
]
| S q ⇒ match q with
| S _ ⇒ (* 2 *) 〈comp2,null_action ? n〉 ] ].
definition compare_step ≝
- λi,j,sig,n,is_endc.
- mk_mTM sig n compare_states (trans_compare_step i j sig n is_endc)
+ λi,j,sig,n.
+ mk_mTM sig n compare_states (trans_compare_step i j sig n)
comp0 (λq.q == comp1 ∨ q == comp2).
definition R_comp_step_true ≝
- λi,j,sig,n,is_endc.λint,outt: Vector (tape sig) (S n).
+ λi,j,sig,n.λint,outt: Vector (tape sig) (S n).
∃x.
- is_endc x = false ∧
current ? (nth i ? int (niltape ?)) = Some ? x ∧
current ? (nth j ? int (niltape ?)) = Some ? x ∧
outt = change_vec ??
(change_vec ?? int
- (tape_move ? (nth i ? int (niltape ?)) (Some ? 〈x,R〉)) i)
- (tape_move ? (nth j ? int (niltape ?)) (Some ? 〈x,R〉)) j.
+ (tape_move_right ? (nth i ? int (niltape ?))) i)
+ (tape_move_right ? (nth j ? int (niltape ?))) j.
definition R_comp_step_false ≝
- λi,j:nat.λsig,n,is_endc.λint,outt: Vector (tape sig) (S n).
- ((∃x.current ? (nth i ? int (niltape ?)) = Some ? x ∧ is_endc x = true) ∨
- current ? (nth i ? int (niltape ?)) ≠ current ? (nth j ? int (niltape ?)) ∨
- current ? (nth i ? int (niltape ?)) = None ? ∨
- current ? (nth j ? int (niltape ?)) = None ?) ∧ outt = int.
+ λi,j:nat.λsig,n.λint,outt: Vector (tape sig) (S n).
+ (current ? (nth i ? int (niltape ?)) ≠ current ? (nth j ? int (niltape ?)) ∨
+ current ? (nth i ? int (niltape ?)) = None ? ∨
+ current ? (nth j ? int (niltape ?)) = None ?) ∧ outt = int.
lemma comp_q0_q2_null :
- ∀i,j,sig,n,is_endc,v.i < S n → j < S n →
+ ∀i,j,sig,n,v.i < S n → j < S n →
(nth i ? (current_chars ?? v) (None ?) = None ? ∨
nth j ? (current_chars ?? v) (None ?) = None ?) →
- step sig n (compare_step i j sig n is_endc) (mk_mconfig ??? comp0 v)
+ step sig n (compare_step i j sig n) (mk_mconfig ??? comp0 v)
= mk_mconfig ??? comp2 v.
-#i #j #sig #n #is_endc #v #Hi #Hj
+#i #j #sig #n #v #Hi #Hj
whd in ⊢ (? → ??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (?→??%?);
* #Hcurrent
[ @eq_f2
[ whd in ⊢ (??(???%)?); >Hcurrent %
- | whd in ⊢ (??(???????(???%))?); >Hcurrent @tape_move_null_action ]
+ | whd in ⊢ (??(????(???%))?); >Hcurrent @tape_move_null_action ]
| @eq_f2
[ whd in ⊢ (??(???%)?); >Hcurrent cases (nth i ?? (None sig)) //
- | whd in ⊢ (??(???????(???%))?); >Hcurrent
+ | whd in ⊢ (??(????(???%))?); >Hcurrent
cases (nth i ?? (None sig)) [|#x] @tape_move_null_action ] ]
qed.
lemma comp_q0_q2_neq :
- ∀i,j,sig,n,is_endc,v.i < S n → j < S n →
- ((∃x.nth i ? (current_chars ?? v) (None ?) = Some ? x ∧ is_endc x = true) ∨
- nth i ? (current_chars ?? v) (None ?) ≠ nth j ? (current_chars ?? v) (None ?)) →
- step sig n (compare_step i j sig n is_endc) (mk_mconfig ??? comp0 v)
+ ∀i,j,sig,n,v.i < S n → j < S n →
+ (nth i ? (current_chars ?? v) (None ?) ≠ nth j ? (current_chars ?? v) (None ?)) →
+ step sig n (compare_step i j sig n) (mk_mconfig ??? comp0 v)
= mk_mconfig ??? comp2 v.
-#i #j #sig #n #is_endc #v #Hi #Hj lapply (refl ? (nth i ?(current_chars ?? v)(None ?)))
+#i #j #sig #n #v #Hi #Hj lapply (refl ? (nth i ?(current_chars ?? v)(None ?)))
cases (nth i ?? (None ?)) in ⊢ (???%→?);
[ #Hnth #_ @comp_q0_q2_null // % //
| #ai #Hai lapply (refl ? (nth j ?(current_chars ?? v)(None ?)))
cases (nth j ?? (None ?)) in ⊢ (???%→?);
[ #Hnth #_ @comp_q0_q2_null // %2 //
- | #aj #Haj *
- [ * #c * >Hai #Heq #Hendc whd in ⊢ (??%?);
- >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
- [ whd in match (trans ????); >Hai >Haj destruct (Heq)
- whd in ⊢ (??(???%)?); >Hendc //
- | whd in match (trans ????); >Hai >Haj destruct (Heq)
- whd in ⊢ (??(???????(???%))?); >Hendc @tape_move_null_action
- ]
- | #Hneq
- whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
- [ whd in match (trans ????); >Hai >Haj
- whd in ⊢ (??(???%)?); cut ((¬is_endc ai∧ai==aj)=false)
- [>(\bf ?) /2 by not_to_not/ cases (is_endc ai) // |#Hcut >Hcut //]
- | whd in match (trans ????); >Hai >Haj
- whd in ⊢ (??(???????(???%))?); cut ((¬is_endc ai∧ai==aj)=false)
- [>(\bf ?) /2 by not_to_not/ cases (is_endc ai) //
- |#Hcut >Hcut @tape_move_null_action
- ]
- ]
+ | #aj #Haj * #Hneq
+ whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
+ [ whd in match (trans ????); >Hai >Haj
+ whd in ⊢ (??(???%)?); cut ((ai==aj)=false)
+ [>(\bf ?) /2 by not_to_not/ % #Haiaj @Hneq
+ >Hai >Haj //
+ | #Haiaj >Haiaj % ]
+ | whd in match (trans ????); >Hai >Haj
+ whd in ⊢ (??(????(???%))?); cut ((ai==aj)=false)
+ [>(\bf ?) /2 by not_to_not/ % #Haiaj @Hneq
+ >Hai >Haj //
+ |#Hcut >Hcut @tape_move_null_action
]
]
+ ]
]
qed.
-lemma comp_q0_q1 :
- ∀i,j,sig,n,is_endc,v,a.i ≠ j → i < S n → j < S n →
- nth i ? (current_chars ?? v) (None ?) = Some ? a → is_endc a = false →
+axiom comp_q0_q1 :
+ ∀i,j,sig,n,v,a.i ≠ j → i < S n → j < S n →
+ nth i ? (current_chars ?? v) (None ?) = Some ? a →
nth j ? (current_chars ?? v) (None ?) = Some ? a →
- step sig n (compare_step i j sig n is_endc) (mk_mconfig ??? comp0 v) =
+ step sig n (compare_step i j sig n) (mk_mconfig ??? comp0 v) =
mk_mconfig ??? comp1
(change_vec ? (S n)
(change_vec ?? v
- (tape_move ? (nth i ? v (niltape ?)) (Some ? 〈a,R〉)) i)
- (tape_move ? (nth j ? v (niltape ?)) (Some ? 〈a,R〉)) j).
-#i #j #sig #n #is_endc #v #a #Heq #Hi #Hj #Ha1 #Hnotendc #Ha2
+ (tape_move_right ? (nth i ? v (niltape ?))) i)
+ (tape_move_right ? (nth j ? v (niltape ?))) j).
+(*
+#i #j #sig #n #v #a #Heq #Hi #Hj #Ha1 #Ha2
whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
[ whd in match (trans ????);
- >Ha1 >Ha2 whd in ⊢ (??(???%)?); >Hnotendc >(\b ?) //
+ >Ha1 >Ha2 whd in ⊢ (??(???%)?); >(\b ?) //
| whd in match (trans ????);
- >Ha1 >Ha2 whd in ⊢ (??(???????(???%))?); >Hnotendc >(\b ?) //
- change with (change_vec ?????) in ⊢ (??(???????%)?);
+ >Ha1 >Ha2 whd in ⊢ (??(????(???%))?); >(\b ?) //
+ change with (change_vec ?????) in ⊢ (??(????%)?);
<(change_vec_same … v j (niltape ?)) in ⊢ (??%?);
<(change_vec_same … v i (niltape ?)) in ⊢ (??%?);
>pmap_change >pmap_change >tape_move_null_action
@eq_f2 // @eq_f2 // >nth_change_vec_neq //
]
qed.
+*)
lemma sem_comp_step :
- ∀i,j,sig,n,is_endc.i ≠ j → i < S n → j < S n →
- compare_step i j sig n is_endc ⊨
- [ comp1: R_comp_step_true i j sig n is_endc,
- R_comp_step_false i j sig n is_endc ].
-#i #j #sig #n #is_endc #Hneq #Hi #Hj #int
+ ∀i,j,sig,n.i ≠ j → i < S n → j < S n →
+ compare_step i j sig n ⊨
+ [ comp1: R_comp_step_true i j sig n,
+ R_comp_step_false i j sig n ].
+#i #j #sig #n #Hneq #Hi #Hj #int
lapply (refl ? (current ? (nth i ? int (niltape ?))))
cases (current ? (nth i ? int (niltape ?))) in ⊢ (???%→?);
[ #Hcuri %{2} %
[ whd in ⊢ (??%?); >comp_q0_q2_null /2/ %2 <Hcurj in ⊢ (???%);
@sym_eq @nth_vec_map
| normalize in ⊢ (%→?); #H destruct (H) ]
- | #_ % // >Ha >Hcurj % % %2 % #H destruct (H) ] ]
- | #b #Hb %{2}
- cases (true_or_false (is_endc a)) #Haendc
+ | #_ % // >Ha >Hcurj % % % #H destruct (H) ] ]
+ | #b #Hb %{2} cases (true_or_false (a == b)) #Hab
[ %
+ [| % [ %
+ [whd in ⊢ (??%?); >(comp_q0_q1 … a Hneq Hi Hj) //
+ [>(\P Hab) <Hb @sym_eq @nth_vec_map
+ |<Ha @sym_eq @nth_vec_map ]
+ | #_ whd >(\P Hab) %{b} % // % // <(\P Hab) // ]
+ | * #H @False_ind @H %
+ ] ]
+ | %
[| % [ %
[whd in ⊢ (??%?); >comp_q0_q2_neq //
- % %{a} % // <Ha @sym_eq @nth_vec_map
+ <(nth_vec_map ?? (current …) i ? int (niltape ?))
+ <(nth_vec_map ?? (current …) j ? int (niltape ?)) >Ha >Hb
+ @(not_to_not ??? (\Pf Hab)) #H destruct (H) %
| normalize in ⊢ (%→?); #H destruct (H) ]
- | #_ % // % % % >Ha %{a} % // ]
- ]
- |cases (true_or_false (a == b)) #Hab
- [ %
- [| % [ %
- [whd in ⊢ (??%?); >(comp_q0_q1 … a Hneq Hi Hj) //
- [>(\P Hab) <Hb @sym_eq @nth_vec_map
- |<Ha @sym_eq @nth_vec_map ]
- | #_ whd >(\P Hab) %{b} % // % // <(\P Hab) % // ]
- | * #H @False_ind @H %
- ] ]
- | %
- [| % [ %
- [whd in ⊢ (??%?); >comp_q0_q2_neq //
- <(nth_vec_map ?? (current …) i ? int (niltape ?))
- <(nth_vec_map ?? (current …) j ? int (niltape ?)) %2 >Ha >Hb
- @(not_to_not ??? (\Pf Hab)) #H destruct (H) %
- | normalize in ⊢ (%→?); #H destruct (H) ]
- | #_ % // % % %2 >Ha >Hb @(not_to_not ??? (\Pf Hab)) #H destruct (H) % ] ]
- ]
+ | #_ % // % % >Ha >Hb @(not_to_not ??? (\Pf Hab)) #H destruct (H) % ] ]
]
]
]
qed.
-definition compare ≝ λi,j,sig,n,is_endc.
- whileTM … (compare_step i j sig n is_endc) comp1.
+definition compare ≝ λi,j,sig,n.
+ whileTM … (compare_step i j sig n) comp1.
definition R_compare ≝
- λi,j,sig,n,is_endc.λint,outt: Vector (tape sig) (S n).
- ((∃x.current ? (nth i ? int (niltape ?)) = Some ? x ∧ is_endc x = true) ∨
- (current ? (nth i ? int (niltape ?)) ≠ current ? (nth j ? int (niltape ?)) ∨
+ λi,j,sig,n.λint,outt: Vector (tape sig) (S n).
+ ((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,rs0.
nth i ? int (niltape ?) = midtape sig ls x (xs@ci::rs) →
nth j ? int (niltape ?) = midtape sig ls0 x (xs@rs0) →
- (∀c0. memb ? c0 (x::xs) = true → is_endc c0 = false) →
(rs0 = [ ] ∧
outt = change_vec ??
(change_vec ?? int (midtape sig (reverse ? xs@x::ls) ci rs) i)
(mk_tape sig (reverse ? xs@x::ls0) (None ?) []) j) ∨
∃cj,rs1.rs0 = cj::rs1 ∧
- ((is_endc ci = true ∨ ci ≠ cj) →
+ (ci ≠ cj →
outt = change_vec ??
(change_vec ?? int (midtape sig (reverse ? xs@x::ls) ci rs) i)
(midtape sig (reverse ? xs@x::ls0) cj rs1) j)).
-lemma wsem_compare : ∀i,j,sig,n,is_endc.i ≠ j → i < S n → j < S n →
- compare i j sig n is_endc ⊫ R_compare i j sig n is_endc.
-#i #j #sig #n #is_endc #Hneq #Hi #Hj #ta #k #outc #Hloop
-lapply (sem_while … (sem_comp_step i j sig n is_endc Hneq Hi Hj) … Hloop) //
+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
-[ whd in ⊢ (%→?); * * [ * [ *
- [* #curi * #Hcuri #Hendi #Houtc %
- [ #_ @Houtc
- | #ls #x #xs #ci #rs #ls0 #rs0 #Hnthi #Hnthj #Hnotendc
- @False_ind
- >Hnthi in Hcuri; normalize in ⊢ (%→?); #H destruct (H)
- >(Hnotendc ? (memb_hd … )) in Hendi; #H destruct (H)
- ]
- |#Hcicj #Houtc %
- [ #_ @Houtc
- | #ls #x #xs #ci #rs #ls0 #rs0 #Hnthi #Hnthj
- >Hnthi in Hcicj; >Hnthj normalize in ⊢ (%→?); * #H @False_ind @H %
- ]]
- | #Hci #Houtc %
- [ #_ @Houtc
- | #ls #x #xs #ci #rs #ls0 #rs0 #Hnthi >Hnthi in Hci;
- normalize in ⊢ (%→?); #H destruct (H) ] ]
- | #Hcj #Houtc %
- [ #_ @Houtc
- | #ls #x #xs #ci #rs #ls0 #rs0 #_ #Hnthj >Hnthj in Hcj;
- normalize in ⊢ (%→?); #H destruct (H) ] ]
- | #td #te * #x * * * #Hendcx #Hci #Hcj #Hd #Hstar #IH #He lapply (IH He) -IH *
- #IH1 #IH2 %
- [ >Hci >Hcj * [* #x0 * #H destruct (H) >Hendcx #H destruct (H)
- |* [* #H @False_ind [cases H -H #H @H % | destruct (H)] | #H destruct (H)]]
- | #ls #c0 #xs #ci #rs #ls0 #rs0 cases xs
- [ #Hnthi #Hnthj #Hnotendc cases rs0 in Hnthj;
- [ #Hnthj % % // >IH1
- [ >Hd @eq_f3 //
- [ @eq_f3 // >(?:c0=x) [ >Hnthi % ]
- >Hnthi in Hci;normalize #H destruct (H) %
- | >(?:c0=x) [ >Hnthj % ]
- >Hnthi in Hci;normalize #H destruct (H) % ]
- | >Hd %2 %2 >nth_change_vec // >Hnthj % ]
- | #r1 #rs1 #Hnthj %2 %{r1} %{rs1} % // *
- [ #Hendci >IH1
- [ >Hd @eq_f3 //
- [ @eq_f3 // >(?:c0=x) [ >Hnthi % ]
- >Hnthi in Hci;normalize #H destruct (H) %
- | >(?:c0=x) [ >Hnthj % ]
- >Hnthi in Hci;normalize #H destruct (H) % ]
+[ whd in ⊢ (%→?); * * [ *
+ [ #Hcicj #Houtc %
+ [ #_ @Houtc
+ | #ls #x #xs #ci #rs #ls0 #rs0 #Hnthi #Hnthj
+ >Hnthi in Hcicj; >Hnthj normalize in ⊢ (%→?); * #H @False_ind @H %
+ ]
+ | #Hci #Houtc %
+ [ #_ @Houtc
+ | #ls #x #xs #ci #rs #ls0 #rs0 #Hnthi >Hnthi in Hci;
+ normalize in ⊢ (%→?); #H destruct (H) ] ]
+ | #Hcj #Houtc %
+ [ #_ @Houtc
+ | #ls #x #xs #ci #rs #ls0 #rs0 #_ #Hnthj >Hnthj in Hcj;
+ normalize in ⊢ (%→?); #H destruct (H) ] ]
+| #td #te * #x * * #Hci #Hcj #Hd #Hstar #IH #He lapply (IH He) -IH *
+ #IH1 #IH2 %
+ [ >Hci >Hcj * [ *
+ [ * #H @False_ind @H % | #H destruct (H)] | #H destruct (H)]
+ | #ls #c0 #xs #ci #rs #ls0 #rs0 cases xs
+ [ #Hnthi #Hnthj cases rs0 in Hnthj;
+ [ #Hnthj % % // >IH1
+ [ >Hd @eq_f3 //
+ [ @eq_f3 // >Hnthi %
+ | >Hnthj % ]
+ | >Hd %2 >nth_change_vec // >Hnthj % ]
+ | #r1 #rs1 #Hnthj %2 %{r1} %{rs1} % // #Hcir1 >IH1
+ [ >Hd @eq_f3 //
+ [ @eq_f3 // >Hnthi %
+ | >Hnthj % ]
| >Hd >nth_change_vec // >nth_change_vec_neq [|@sym_not_eq //]
- >nth_change_vec // >Hnthi >Hnthj normalize % %{ci} % //
+ >nth_change_vec // >Hnthi >Hnthj normalize % %
+ @(not_to_not … Hcir1) #H destruct (H) %
]
- |#Hcir1 >IH1
- [>Hd @eq_f3 //
- [ @eq_f3 // >(?:c0=x) [ >Hnthi % ]
- >Hnthi in Hci;normalize #H destruct (H) %
- | >(?:c0=x) [ >Hnthj % ]
- >Hnthi in Hci;normalize #H destruct (H) % ]
- | >Hd %2 % % >nth_change_vec //
- >nth_change_vec_neq [|@sym_not_eq //]
- >nth_change_vec // >Hnthi >Hnthj normalize @(not_to_not … Hcir1)
- #H destruct (H) % ]
]
- ]
- |#x0 #xs0 #Hnthi #Hnthj #Hnotendc
- cut (c0 = x) [ >Hnthi in Hci; normalize #H destruct (H) // ]
- #Hcut destruct (Hcut) cases rs0 in Hnthj;
- [ #Hnthj % % //
- cases (IH2 (x::ls) x0 xs0 ci rs (x::ls0) [ ] ???) -IH2
- [ * #_ #IH2 >IH2 >Hd >change_vec_commute in ⊢ (??%?); //
- >change_vec_change_vec >change_vec_commute in ⊢ (??%?); //
- @sym_not_eq //
- | * #cj * #rs1 * #H destruct (H)
- | >Hd >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
- >Hnthi %
- | >Hd >nth_change_vec // >Hnthj %
- | #c0 #Hc0 @Hnotendc @memb_cons @Hc0 ]
- | #r1 #rs1 #Hnthj %2 %{r1} %{rs1} % // #Hcir1
- cases(IH2 (x::ls) x0 xs0 ci rs (x::ls0) (r1::rs1) ???)
- [ * #H destruct (H)
- | * #r1' * #rs1' * #H destruct (H) #Hc1r1 >Hc1r1 //
- >Hd >change_vec_commute in ⊢ (??%?); //
- >change_vec_change_vec >change_vec_commute in ⊢ (??%?); //
+ | #x0 #xs0 #Hnthi #Hnthj
+ cut (c0 = x) [ >Hnthi in Hci; normalize #H destruct (H) // ]
+ #Hcut destruct (Hcut) cases rs0 in Hnthj;
+ [ #Hnthj % % //
+ cases (IH2 (x::ls) x0 xs0 ci rs (x::ls0) [ ] ??) -IH2
+ [ * #_ #IH2 >IH2 >Hd >change_vec_commute in ⊢ (??%?); //
+ >change_vec_change_vec >change_vec_commute in ⊢ (??%?); //
@sym_not_eq //
- | >Hd >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
- >Hnthi //
- | >Hd >nth_change_vec // >Hnthi >Hnthj %
- | #c0 #Hc0 @Hnotendc @memb_cons @Hc0
+ | * #cj * #rs1 * #H destruct (H)
+ | >Hd >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
+ >Hnthi %
+ | >Hd >nth_change_vec // >Hnthj % ]
+ | #r1 #rs1 #Hnthj %2 %{r1} %{rs1} % // #Hcir1
+ cases(IH2 (x::ls) x0 xs0 ci rs (x::ls0) (r1::rs1) ??)
+ [ * #H destruct (H)
+ | * #r1' * #rs1' * #H destruct (H) #Hc1r1 >Hc1r1 //
+ >Hd >change_vec_commute in ⊢ (??%?); //
+ >change_vec_change_vec >change_vec_commute in ⊢ (??%?); //
+ @sym_not_eq //
+ | >Hd >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
+ >Hnthi //
+ | >Hd >nth_change_vec // >Hnthi >Hnthj %
]]]]]
-qed.
+qed.
-lemma terminate_compare : ∀i,j,sig,n,is_endc,t.
+lemma terminate_compare : ∀i,j,sig,n,t.
i ≠ j → i < S n → j < S n →
- compare i j sig n is_endc ↓ t.
-#i #j #sig #n #is_endc #t #Hneq #Hi #Hj
+ compare i j sig n ↓ t.
+#i #j #sig #n #t #Hneq #Hi #Hj
@(terminate_while … (sem_comp_step …)) //
<(change_vec_same … t i (niltape ?))
cases (nth i (tape sig) t (niltape ?))
-[ % #t1 * #x * * * #_ >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
-|2,3: #a0 #al0 % #t1 * #x * * * #_ >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
+[ % #t1 * #x * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
+|2,3: #a0 #al0 % #t1 * #x * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
| #ls #c #rs lapply c -c lapply ls -ls lapply t -t elim rs
- [#t #ls #c % #t1 * #x * * * #Hendcx >nth_change_vec // normalize in ⊢ (%→?);
- #H1 destruct (H1) #Hxsep >change_vec_change_vec #Ht1 %
- #t2 * #x0 * * * #Hendcx0 >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
+ [#t #ls #c % #t1 * #x * * >nth_change_vec // normalize in ⊢ (%→?);
+ #H1 destruct (H1) #_ >change_vec_change_vec #Ht1 %
+ #t2 * #x0 * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
>nth_change_vec // normalize in ⊢ (%→?); #H destruct (H)
|#r0 #rs0 #IH #t #ls #c % #t1 * #x * * >nth_change_vec //
normalize in ⊢ (%→?); #H destruct (H) #Hcur
]
qed.
-lemma sem_compare : ∀i,j,sig,n,is_endc.
+lemma sem_compare : ∀i,j,sig,n.
i ≠ j → i < S n → j < S n →
- compare i j sig n is_endc ⊨ R_compare i j sig n is_endc.
-#i #j #sig #n #is_endc #Hneq #Hi #Hj @WRealize_to_Realize /2/
+ compare i j sig n ⊨ R_compare i j sig n.
+#i #j #sig #n #Hneq #Hi #Hj @WRealize_to_Realize /2/
qed.
| Some a0 ⇒ if is_sep a0 then 〈copy2,null_action ? n〉
else 〈copy1,change_vec ? (S n)
(change_vec ?(S n)
- (null_action ? n) (Some ? 〈a0,R〉) src)
- (Some ? 〈a0,R〉) dst〉 ]
+ (null_action ? n) (〈Some ? a0,R〉) src)
+ (〈Some ? a0,R〉) dst〉 ]
| S q ⇒ match q with
[ O ⇒ (* 1 *) 〈copy1,null_action ? n〉
| S _ ⇒ (* 2 *) 〈copy2,null_action ? n〉 ] ].
is_sep x1 = false ∧
outt = change_vec ??
(change_vec ?? int
- (tape_move ? (nth src ? int (niltape ?)) (Some ? 〈x1,R〉)) src)
- (tape_move ? (nth dst ? int (niltape ?)) (Some ? 〈x1,R〉)) dst.
+ (tape_move_mono ? (nth src ? int (niltape ?)) (〈Some ? x1,R〉)) src)
+ (tape_move_mono ? (nth dst ? int (niltape ?)) (〈Some ? x1,R〉)) dst.
definition R_copy_step_false ≝
λsrc,dst:nat.λsig,n,is_sep.λint,outt: Vector (tape sig) (S n).
[ >current_chars_change_vec // whd in match (trans ????);
>nth_change_vec // >Hcurrent whd in ⊢ (??(???%)?); >Hsep %
| >current_chars_change_vec // whd in match (trans ????);
- >nth_change_vec // >Hcurrent whd in ⊢ (??(???????(???%))?);
+ >nth_change_vec // >Hcurrent whd in ⊢ (??(????(???%))?);
>Hsep @tape_move_null_action
]
qed.
-lemma copy_q0_q1 :
+axiom copy_q0_q1 :
∀src,dst,sig,n,is_sep,v,t.src ≠ dst → src < S n → dst < S n →
∀s.current ? t = Some ? s → is_sep s = false →
step sig n (copy_step src dst sig n is_sep)
mk_mconfig ??? copy1
(change_vec ? (S n)
(change_vec ?? v
- (tape_move ? t (Some ? 〈s,R〉)) src)
- (tape_move ? (nth dst ? v (niltape ?)) (Some ? 〈s,R〉)) dst).
+ (tape_move_mono ? t (〈Some ? s,R〉)) src)
+ (tape_move_mono ? (nth dst ? v (niltape ?)) (〈Some ? s,R〉)) dst).
+(*
#src #dst #sig #n #is_sep #v #t #Hneq #Hsrc #Hdst #s #Hcurrent #Hsep
whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
[ >current_chars_change_vec // whd in match (trans ????);
>nth_change_vec // >Hcurrent whd in ⊢ (??(???%)?); >Hsep %
| >current_chars_change_vec // whd in match (trans ????);
- >nth_change_vec // >Hcurrent whd in ⊢ (??(???????(???%))?);
- >Hsep whd in ⊢ (??(???????(???%))?); >change_vec_commute // >pmap_change
+ >nth_change_vec // >Hcurrent whd in ⊢ (??(????(???%))?);
+ >Hsep whd in ⊢ (??(????(???%))?); >change_vec_commute // >pmap_change
>change_vec_commute // @eq_f3 //
<(change_vec_same ?? v dst (niltape ?)) in ⊢(??%?);
>pmap_change @eq_f3 //
]
-qed.
+qed.*)
lemma sem_copy_step :
∀src,dst,sig,n,is_sep.src ≠ dst → src < S n → dst < S n →
include "turing/multi_universal/compare.ma".
include "turing/multi_universal/par_test.ma".
-
+include "turing/multi_universal/moves_2.ma".
definition Rtc_multi_true ≝
λalpha,test,n,i.λt1,t2:Vector ? (S n).
#Hi0i @sym_eq @Hnth_j @sym_not_eq // ] ]
qed.
-lemma comp_list: ∀S:DeqSet. ∀l1,l2:list S.∀is_endc. ∃l,tl1,tl2.
- l1 = l@tl1 ∧ l2 = l@tl2 ∧ (∀c.c ∈ l = true → is_endc c = false) ∧
- ∀a,tla. tl1 = a::tla →
- is_endc a = true ∨ (is_endc a = false ∧∀b,tlb.tl2 = b::tlb → a≠b).
-#S #l1 #l2 #is_endc elim l1 in l2;
-[ #l2 %{[ ]} %{[ ]} %{l2} normalize %
- [ % [ % // | #c #H destruct (H) ] | #a #tla #H destruct (H) ]
-| #x #l3 #IH cases (true_or_false (is_endc x)) #Hendcx
- [ #l %{[ ]} %{(x::l3)} %{l} normalize
- % [ % [ % // | #c #H destruct (H) ] | #a #tla #H destruct (H) >Hendcx % % ]
- | *
- [ %{[ ]} %{(x::l3)} %{[ ]} normalize %
- [ % [ % // | #c #H destruct (H) ]
- | #a #tla #H destruct (H) cases (is_endc a)
- [ % % | %2 % // #b #tlb #H destruct (H) ]
- ]
- | #y #l4 cases (true_or_false (x==y)) #Hxy
- [ lapply (\P Hxy) -Hxy #Hxy destruct (Hxy)
- cases (IH l4) -IH #l * #tl1 * #tl2 * * * #Hl3 #Hl4 #Hl #IH
- %{(y::l)} %{tl1} %{tl2} normalize
- % [ % [ % //
- | #c cases (true_or_false (c==y)) #Hcy >Hcy normalize
- [ >(\P Hcy) //
- | @Hl ]
- ]
- | #a #tla #Htl1 @(IH … Htl1) ]
- | %{[ ]} %{(x::l3)} %{(y::l4)} normalize %
- [ % [ % // | #c #H destruct (H) ]
- | #a #tla #H destruct (H) cases (is_endc a)
- [ % % | %2 % // #b #tlb #H destruct (H) @(\Pf Hxy) ]
- ]
- ]
- ]
- ]
-]
-qed.
-
-definition match_test ≝ λsrc,dst.λsig:DeqSet.λn,is_endc.λv:Vector ? n.
+definition match_test ≝ λsrc,dst.λsig:DeqSet.λn.λv:Vector ? n.
match (nth src (option sig) v (None ?)) with
[ None ⇒ false
- | Some x ⇒ notb ((is_endc x) ∨ (nth dst (DeqOption sig) v (None ?) == None ?))].
+ | Some x ⇒ notb (nth dst (DeqOption sig) v (None ?) == None ?) ].
+
+definition rewind ≝ λsrc,dst,sig,n.parmove src dst sig n L · parmove_step src dst sig n R.
+
+definition R_rewind ≝ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
+ (∀x,x0,xs,rs.
+ nth src ? int (niltape ?) = midtape sig (xs@[x0]) x rs →
+ ∀ls0,y,y0,target,rs0.|xs| = |target| →
+ nth dst ? int (niltape ?) = midtape sig (target@y0::ls0) y rs0 →
+ outt = change_vec ??
+ (change_vec ?? int (midtape sig [] x0 (reverse ? xs@x::rs)) src)
+ (midtape sig ls0 y0 (reverse ? target@y::rs0)) dst).
+
+theorem accRealize_to_Realize :
+ ∀sig,n.∀M:mTM sig n.∀Rtrue,Rfalse,acc.
+ M ⊨ [ acc: Rtrue, Rfalse ] → M ⊨ Rtrue ∪ Rfalse.
+#sig #n #M #Rtrue #Rfalse #acc #HR #t
+cases (HR t) #k * #outc * * #Hloop
+#Htrue #Hfalse %{k} %{outc} % //
+cases (true_or_false (cstate sig (states sig n M) n outc == acc)) #Hcase
+[ % @Htrue @(\P Hcase) | %2 @Hfalse @(\Pf Hcase) ]
+qed.
+
+lemma sem_rewind : ∀src,dst,sig,n.
+ src ≠ dst → src < S n → dst < S n →
+ rewind src dst sig n ⊨ R_rewind src dst sig n.
+#src #dst #sig #n #Hneq #Hsrc #Hdst
+check acc_sem_seq_app
+@(sem_seq_app sig n ????? (sem_parmoveL src dst sig n Hneq Hsrc Hdst)
+ (accRealize_to_Realize … (sem_parmove_step src dst sig n R Hneq Hsrc Hdst)))
+#ta #tb * #tc * * #HR1 #_ #HR2
+#x #x0 #xs #rs #Hmidta_src #ls0 #y #y0 #target #rs0 #Hlen #Hmidta_dst
+>(HR1 ??? Hmidta_src ls0 y (target@[y0]) rs0 ??) in HR2;
+[|>Hmidta_dst //
+|>length_append >length_append >Hlen % ] *
+[ whd in ⊢ (%→?); * #x1 * #x2 * *
+ >change_vec_commute in ⊢ (%→?); // >nth_change_vec //
+ cases (reverse sig (xs@[x0])@x::rs)
+ [|#z #zs] normalize in ⊢ (%→?); #H destruct (H)
+| whd in ⊢ (%→?); * #_ #Htb >Htb -Htb FAIL
+
+ normalize in ⊢ (%→?);
+ (sem_parmove_step src dst sig n R Hneq Hsrc Hdst))
+ (acc_sem_if ? n … (sem_partest sig n (match_test src dst sig ?))
+ (sem_seq …
+ (sem_parmoveL ???? Hneq Hsrc Hdst)
+ (sem_inject … dst (le_S_S_to_le … Hdst) (sem_move_r ? )))
+ (sem_nop …)))
+
-definition match_step ≝ λsrc,dst,sig,n,is_startc,is_endc.
- compare src dst sig n is_endc ·
- (ifTM ?? (partest sig n (match_test src dst sig ? is_endc))
+definition match_step ≝ λsrc,dst,sig,n.
+ compare src dst sig n ·
+ (ifTM ?? (partest sig n (match_test src dst sig ?))
(single_finalTM ??
- (parmove src dst sig n L is_startc · (inject_TM ? (move_r ?) n dst)))
+ (rewind src dst sig n · (inject_TM ? (move_r ?) n dst)))
(nop …)
partest1).
definition R_match_step_false ≝
- λsrc,dst,sig,n,is_endc.λint,outt: Vector (tape sig) (S n).
- ∀ls,x,xs,end,rs.
- nth src ? int (niltape ?) = midtape sig ls x (xs@end::rs) →
- (∀c0. memb ? c0 (x::xs) = true → is_endc c0 = false) → is_endc end = true →
- ((current sig (nth dst (tape sig) int (niltape sig)) = None ?) ∧ outt = int) ∨
+ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
+ ∀ls,x,xs.
+ nth src ? int (niltape ?) = midtape sig ls x xs →
+ ((current sig (nth dst (tape sig) int (niltape sig)) = None ?) ∧ outt = int) ∨
(∃ls0,rs0,xs0. nth dst ? int (niltape ?) = midtape sig ls0 x rs0 ∧
xs = rs0@xs0 ∧
current sig (nth dst (tape sig) outt (niltape sig)) = None ?) ∨
(∃ls0,rs0.
nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) ∧
- ∀rsj,c.
- rs0 = c::rsj →
+ (* ∀rsj,c.
+ rs0 = c::rsj → *)
outt = change_vec ??
- (change_vec ?? int (midtape sig (reverse ? xs@x::ls) end rs) src)
- (midtape sig (reverse ? xs@x::ls0) c rsj) dst).
+ (change_vec ?? int (mk_tape sig (reverse ? xs@x::ls) (None ?) [ ]) src)
+ (mk_tape sig (reverse ? xs@x::ls0) (option_hd ? rs0) (tail ? rs0)) dst).
+(*definition R_match_step_true ≝
+ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
+ ∀s,rs.current sig (nth src (tape sig) int (niltape sig)) = Some ? s →
+ current sig (nth dst (tape sig) int (niltape sig)) ≠ None ? ∧
+ (∀s1.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s1 → s ≠ s1 →
+ outt = change_vec ?? int
+ (tape_move_mono … (nth dst ? int (niltape ?)) (〈Some ? s1,R〉)) dst) ∧
+ (∀ls,x,xs,ci,rs,ls0,rs0.
+ nth src ? int (niltape ?) = midtape sig ls x (xs@ci::rs) →
+ nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) →
+ rs0 ≠ [] ∧
+ ∀cj,rs1.rs0 = cj::rs1 →
+ ci ≠ cj →
+ (outt = change_vec ?? int
+ (tape_move_mono … (nth dst ? int (niltape ?)) (〈None ?,R〉)) dst)).
+*)
definition R_match_step_true ≝
- λsrc,dst,sig,n,is_startc,is_endc.λint,outt: Vector (tape sig) (S n).
+ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
∀s.current sig (nth src (tape sig) int (niltape sig)) = Some ? s →
- current sig (nth dst (tape sig) int (niltape sig)) ≠ None ? ∧
- (is_startc s = true →
- (∀c.c ∈ right ? (nth src (tape sig) int (niltape sig)) = true → is_startc c = false) →
- (∀s1.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s1 → s ≠ s1 →
+ ∃s1.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s1 ∧
+ (left ? (nth src ? int (niltape ?)) = [ ] →
+ (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,rs0.
- nth src ? int (niltape ?) = midtape sig ls x (xs@ci::rs) →
- nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) →
- (∀c0. memb ? c0 (x::xs) = true → is_endc c0 = false) →
- is_endc ci = false ∧ rs0 ≠ [] ∧
- ∀cj,rs1.rs0 = cj::rs1 →
- ci ≠ cj →
- (outt = change_vec ?? int
- (tape_move … (nth dst ? int (niltape ?)) (Some ? 〈x,R〉)) dst ∧ is_endc ci = false))).
-
+ (tape_move_mono … (nth dst ? int (niltape ?)) (〈None ?,R〉)) dst) ∧
+ (∀xs,ci,rs,ls0,rs0.
+ nth src ? int (niltape ?) = midtape sig [] s (xs@ci::rs) →
+ nth dst ? int (niltape ?) = midtape sig ls0 s (xs@rs0) →
+ rs0 ≠ [] ∧
+ ∀cj,rs1.rs0 = cj::rs1 →
+ ci ≠ cj →
+ (outt = change_vec ?? int
+ (tape_move_mono … (nth dst ? int (niltape ?)) (〈None ?,R〉)) dst))).
+
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 ⊨
+ ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
+ match_step src dst sig n ⊨
[ 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 is_endc Hneq Hsrc Hdst)
- (acc_sem_if ? n … (sem_partest sig n (match_test src dst sig ? is_endc))
+ R_match_step_true src dst sig n,
+ R_match_step_false src dst sig n ].
+#src #dst #sig #n #Hneq #Hsrc #Hdst
+@(acc_sem_seq_app sig n … (sem_compare src dst sig n Hneq Hsrc Hdst)
+ (acc_sem_if ? n … (sem_partest sig n (match_test src dst sig ?))
(sem_seq …
- (sem_parmoveL ???? is_startc Hneq Hsrc Hdst)
+ (sem_parmoveL ???? Hneq Hsrc Hdst)
(sem_inject … dst (le_S_S_to_le … Hdst) (sem_move_r ? )))
(sem_nop …)))
-[#ta #tb #tc * #Hcomp1 #Hcomp2 * #td * * #Htest #Htd >Htd -Htd
- * #te * #Hte #Htb whd
- #s #Hcurta_src %
- [ lapply (refl ? (current ? (nth dst ? ta (niltape ?))))
+[#ta #tb #tc * #Hcomp1 #Hcomp2 * #td * #Htest
+ * #te * #Hte #Htb #s #Hcurta_src whd
+ cut (∃s1.current sig (nth dst (tape sig) ta (niltape sig))=Some sig s1)
+ [ lapply Hcomp1 -Hcomp1
+ lapply (refl ? (current ? (nth dst ? ta (niltape ?))))
cases (current ? (nth dst ? ta (niltape ?))) in ⊢ (???%→%);
- [| #c #_ % #Hfalse destruct (Hfalse) ]
+ [ #Hcurta_dst #Hcomp1 >Hcomp1 in Htest; // *
+ change with (vec_map ?????) in match (current_chars ???); whd in ⊢ (??%?→?);
+ <(nth_vec_map ?? (current ?) src ? ta (niltape ?))
+ <(nth_vec_map ?? (current ?) dst ? ta (niltape ?))
+ >Hcurta_src >Hcurta_dst whd in ⊢ (??%?→?); #H destruct (H)
+ | #s1 #_ #_ %{s1} % ] ]
+ * #s1 #Hcurta_dst %{s1} % // #Hleftta %
+ [ #Hneqss1 -Hcomp2 cut (tc = ta)
+ [@Hcomp1 %1 %1 >Hcurta_src >Hcurta_dst @(not_to_not … Hneqss1) #H destruct (H) //]
+ #H destruct (H) -Hcomp1 cut (td = ta)
+ [ cases Htest -Htest // ] #Htdta destruct (Htdta)
+ cases Hte -Hte #Hte #_
+ cases (current_to_midtape … Hcurta_src) #ls * #rs #Hmidta_src
+ cases (current_to_midtape … Hcurta_dst) #ls0 * #rs0 #Hmidta_dst
+ >Hmidta_src in Hleftta; normalize in ⊢ (%→?); #Hls destruct (Hls)
+ >(Hte s [ ] rs Hmidta_src ls0 s1 [ ] rs0 (refl ??) Hmidta_dst) in Htb;
+ * whd in ⊢ (%→?);
+ mid
+
+ in Htb;
+ cut (te = ta)
+ [ cases Htest -Htest #Htest #Htdta <Htdta @Hte %1 >Htdta @Hcurta_src %{s} % //]
+ -Hte #H destruct (H) %
+ [cases Htb * #_ #Hmove #Hmove1 @(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 >(Hmove … Hta_mid) >Hta_mid cases rs //
+ | >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @Hmove1 @sym_not_eq // ]
+ | whd in Htest:(??%?); >(nth_vec_map ?? (current sig)) in Hcurta_src; #Hcurta_src
+ >Hcurta_src in Htest; whd in ⊢ (??%?→?);
+ cases (is_endc s) // whd in ⊢ (??%?→?); #H @sym_eq //
+ ]
+ <(nth_vec_map ?? (current ?) dst ? tc (niltape ?))
+ >Hcurta_src normalize
+ lapply (refl ? (current ? (nth dst ? ta (niltape ?))))
+ cases (current ? (nth dst ? ta (niltape ?))) in ⊢ (???%→%);
+ [| #s1 #Hcurta_dst %
+ [ % #Hfalse destruct (Hfalse)
+ | #s1' #Hs1 destruct (Hs1) #Hneqss1 -Hcomp2
+ cut (tc = ta)
+ [@Hcomp1 %1 %1 >Hcurta_src >Hcurta_dst @(not_to_not … Hneqss1) #H destruct (H) //]
+ #H destruct (H) -Hcomp1 cases Hte -Hte #_ #Hte
+ cut (te = ta) [ cases Htest -Htest #Htest #Htdta <Htdta @Hte %1 %{s} % //] -Hte #H destruct (H) %
+ [cases Htb * #_ #Hmove #Hmove1 @(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 >(Hmove … Hta_mid) >Hta_mid cases rs //
+ | >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @Hmove1 @sym_not_eq // ]
+ | whd in Htest:(??%?); >(nth_vec_map ?? (current sig)) in Hcurta_src; #Hcurta_src
+ >Hcurta_src in Htest; whd in ⊢ (??%?→?);
+ cases (is_endc s) // whd in ⊢ (??%?→?); #H @sym_eq //
+ ]
+
+ ]
#Hcurta_dst >Hcomp1 in Htest; [| %2 %2 //]
whd in ⊢ (??%?→?); change with (current ? (niltape ?)) in match (None ?);
<nth_vec_map >Hcurta_src whd in ⊢ (??%?→?); <nth_vec_map
[ None ⇒ 〈parmove2,null_action ? n〉
| Some a1 ⇒ 〈parmove1,change_vec ? (S n)
(change_vec ?(S n)
- (null_action ? n) (Some ? 〈a0,D〉) src)
- (Some ? 〈a1,D〉) dst〉 ] ]
+ (null_action ? n) (〈Some ? a0,D〉) src)
+ (〈Some ? a1,D〉) dst〉 ] ]
| S q ⇒ match q with
[ O ⇒ (* 1 *) 〈parmove1,null_action ? n〉
| S _ ⇒ (* 2 *) 〈parmove2,null_action ? n〉 ] ].
is_sep x1 = false ∧
outt = change_vec ??
(change_vec ?? int
- (tape_move ? (nth src ? int (niltape ?)) (Some ? 〈x1,D〉)) src)
- (tape_move ? (nth dst ? int (niltape ?)) (Some ? 〈x2,D〉)) dst.
+ (tape_move ? (tape_write ? (nth src ? int (niltape ?)) (Some ? x1)) D) src)
+ (tape_move ? (tape_write ? (nth dst ? int (niltape ?)) (Some ? x2)) D) dst.
definition R_parmove_step_false ≝
λsrc,dst:nat.λsig,n,is_sep.λint,outt: Vector (tape sig) (S n).
whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
@eq_f2
[ whd in ⊢ (??(???%)?); >Hcurrent %
-| whd in ⊢ (??(???????(???%))?); >Hcurrent @tape_move_null_action ]
+| whd in ⊢ (??(????(???%))?); >Hcurrent @tape_move_null_action ]
qed.
lemma parmove_q0_q2_sep :
whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
@eq_f2
[ whd in ⊢ (??(???%)?); >Hcurrent whd in ⊢ (??(???%)?); >Hsep %
-| whd in ⊢ (??(???????(???%))?); >Hcurrent
- whd in ⊢ (??(???????(???%))?); >Hsep @tape_move_null_action ]
+| whd in ⊢ (??(????(???%))?); >Hcurrent
+ whd in ⊢ (??(????(???%))?); >Hsep @tape_move_null_action ]
qed.
lemma parmove_q0_q2_null_dst :
whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
@eq_f2
[ whd in ⊢ (??(???%)?); >Hcursrc whd in ⊢ (??(???%)?); >Hsep >Hcurdst %
-| whd in ⊢ (??(???????(???%))?); >Hcursrc
- whd in ⊢ (??(???????(???%))?); >Hsep >Hcurdst @tape_move_null_action ]
+| whd in ⊢ (??(????(???%))?); >Hcursrc
+ whd in ⊢ (??(????(???%))?); >Hsep >Hcurdst @tape_move_null_action ]
qed.
-lemma parmove_q0_q1 :
+axiom parmove_q0_q1 :
∀src,dst,sig,n,D,is_sep,v.src ≠ dst → src < S n → dst < S n →
∀a1,a2.
nth src ? (current_chars ?? v) (None ?) = Some ? a1 →
mk_mconfig ??? parmove1
(change_vec ? (S n)
(change_vec ?? v
- (tape_move ? (nth src ? v (niltape ?)) (Some ? 〈a1,D〉)) src)
- (tape_move ? (nth dst ? v (niltape ?)) (Some ? 〈a2,D〉)) dst).
+ (tape_move ? (tape_write ? (nth src ? v (niltape ?)) (Some ? a1)) D) src)
+ (tape_move ? (tape_write ? (nth dst ? v (niltape ?)) (Some ? a2)) D) dst).
+(*
#src #dst #sig #n #D #is_sep #v #Hneq #Hsrc #Hdst
#a1 #a2 #Hcursrc #Hcurdst #Hsep
whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
[ whd in match (trans ????);
>Hcursrc >Hcurdst whd in ⊢ (??(???%)?); >Hsep //
| whd in match (trans ????);
- >Hcursrc >Hcurdst whd in ⊢ (??(???????(???%))?); >Hsep
- change with (change_vec ?????) in ⊢ (??(???????%)?);
- <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
- <(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
+ >Hcursrc >Hcurdst whd in ⊢ (??(????(???%))?); >Hsep whd in ⊢ (??(????(???%))?);
+ change with (pmap_vec ???????) in ⊢ (??%?);
+ whd in match (vec_map ?????);
>pmap_change >pmap_change >tape_move_null_action
@eq_f2 // @eq_f2 // >nth_change_vec_neq //
]
qed.
+*)
lemma sem_parmove_step :
∀src,dst,sig,n,D,is_sep.src ≠ dst → src < S n → dst < S n →
λsig,n,test.λint,outt: Vector (tape sig) (S n).
test (current_chars ?? int) = false ∧ outt = int.
-lemma partest_q0_q1:
+axiom partest_q0_q1:
∀sig,n,test,v.
test (current_chars ?? v) = true →
step sig n (partest sig n test)(mk_mconfig ??? partest0 v)
= mk_mconfig ??? partest1 v.
-#sig #n #test #v #Htest
+(*#sig #n #test #v #Htest
whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
@eq_f2
[ whd in ⊢ (??(???%)?); >Htest %
| whd in ⊢ (??(???????(???%))?); >Htest @tape_move_null_action ]
-qed.
+qed.*)
-lemma partest_q0_q2:
+axiom partest_q0_q2:
∀sig,n,test,v.
test (current_chars ?? v) = false →
step sig n (partest sig n test)(mk_mconfig ??? partest0 v)
= mk_mconfig ??? partest2 v.
+(*
#sig #n #test #v #Htest
whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
@eq_f2
[ whd in ⊢ (??(???%)?); >Htest %
| whd in ⊢ (??(???????(???%))?); >Htest @tape_move_null_action ]
qed.
+*)
lemma sem_partest:
∀sig,n,test.
record mTM (sig:FinSet) (tapes_no:nat) : Type[1] ≝
{ states : FinSet;
trans : states × (Vector (option sig) (S tapes_no)) →
- states × (Vector (option (sig × move))(S tapes_no));
+ states × (Vector ((option sig) × move) (S tapes_no));
start: states;
halt : states → bool
}.
definition current_chars ≝ λsig.λn.λtapes.
vec_map ?? (current sig) (S n) tapes.
+definition tape_move_multi ≝
+ λsig,n,ts,mvs.
+ pmap_vec ??? (tape_move sig) ?
+ (pmap_vec ??? (tape_write sig) n ts (vec_map ?? (λx.\fst x) ? mvs))
+ (vec_map ?? (λx.\snd x) ? mvs).
+
definition step ≝ λsig.λn.λM:mTM sig n.λc:mconfig sig (states ?? M) n.
let 〈news,mvs〉 ≝ trans sig n M 〈cstate ??? c,current_chars ?? (ctapes ??? c)〉 in
- mk_mconfig ???
- news
- (pmap_vec ??? (tape_move sig) ? (ctapes ??? c) mvs).
+ mk_mconfig ??? news (tape_move_multi sig ? (ctapes ??? c) mvs).
definition empty_tapes ≝ λsig.λn.
mk_Vector ? n (make_list (tape sig) (niltape sig) n) ?.
definition nop ≝
λalpha:FinSet.λn.mk_mTM alpha n nop_states
- (λp.let 〈q,a〉 ≝ p in 〈q,mk_Vector ? (S n) (make_list ? (None ?) (S n)) ?〉)
+ (λp.let 〈q,a〉 ≝ p in 〈q,mk_Vector ? (S n) (make_list ? (〈None ?,N〉) (S n)) ?〉)
start_nop (λ_.true).
elim n normalize //
qed.
(************************** Sequential Composition ****************************)
definition null_action ≝ λsig.λn.
-mk_Vector ? (S n) (make_list (option (sig × move)) (None ?) (S n)) ?.
+mk_Vector ? (S n) (make_list (option sig × move) (〈None ?,N〉) (S n)) ?.
elim (S n) // normalize //
qed.
lemma tape_move_null_action: ∀sig,n,tapes.
- pmap_vec ??? (tape_move sig) (S n) tapes (null_action sig n) = tapes.
+ tape_move_multi sig (S n) tapes (null_action sig n) = tapes.
#sig #n #tapes cases tapes -tapes #tapes whd in match (null_action ??);
#Heq @Vector_eq <Heq -Heq elim tapes //
#a #tl #Hind whd in ⊢ (??%?); @eq_f2 // @Hind
projects / helm.git / commitdiff