2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_____________________________________________________________*)
12 include "turing/turing.ma".
14 (******************* inject a mono machine into a multi tape one **********************)
15 definition inject_trans ≝ λsig,states:FinSet.λn,i:nat.
16 λtrans:states × (option sig) → states × (option (sig × move)).
17 λp:states × (Vector (option sig) (S n)).
19 let 〈nq,na〉 ≝ trans 〈q,nth i ? a (None ?)〉 in
20 〈nq, change_vec ? (S n) (null_action ? n) na i〉.
22 definition inject_TM ≝ λsig.λM:TM sig.λn,i.
25 (inject_trans ?? n i (trans ? M))
29 axiom current_chars_change_vec: ∀sig,n,v,a,i. i < S n →
30 current_chars sig ? (change_vec ? (S n) v a i) =
31 change_vec ? (S n)(current_chars ?? v) (current ? a) i.
33 lemma inject_trans_def :∀sig:FinSet.∀n,i:nat.i < S n →
35 trans sig M 〈s,a〉 = 〈sn,an〉 →
36 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〉 =
37 〈sn,change_vec ? (S n) (null_action ? n) an i〉.
38 #sig #n #i #Hlt #trans #v #s #a #sn #an #Htrans
39 whd in ⊢ (??%?); >nth_change_vec // >Htrans //
42 lemma inject_step : ∀sig,n,M,i,q,t,nq,nt,v. i < S n →
43 step sig M (mk_config ?? q t) = mk_config ?? nq nt →
44 cic:/matita/turing/turing/step.def(10) sig n (inject_TM sig M n i)
45 (mk_mconfig ?? n q (change_vec ? (S n) v t i))
46 = mk_mconfig ?? n nq (change_vec ? (S n) v nt i).
47 #sig #n #M #i #q #t #nq #nt #v #lein whd in ⊢ (??%?→?);
48 whd in match (step ????); >(current_chars_change_vec … lein)
49 >(eq_pair_fst_snd … (trans sig M ?)) whd in ⊢ (??%?→?); #H
50 >(inject_trans_def sig n i lein M … (eq_pair_fst_snd … ))
51 whd in ⊢ (??%?); @eq_f2 [destruct (H) // ]
52 @(eq_vec … (niltape ?)) #i0 #lei0n
53 cases (decidable_eq_nat … i i0) #Hii0
54 [ >Hii0 >nth_change_vec // >pmap_change >nth_change_vec // destruct (H) //
55 | >nth_change_vec_neq // >pmap_change >nth_change_vec_neq
56 >tape_move_null_action //
60 lemma halt_inject: ∀sig,n,M,i,x.
61 cic:/matita/turing/turing/halt.fix(0,2,9) sig n (inject_TM sig M n i) x
65 lemma de_option: ∀A,a,b. Some A a = Some A b → a = b.
66 #A #a #b #H destruct //
69 lemma loop_inject: ∀sig,n,M,i,k,ins,int,outs,outt,vt.i < S n →
70 loopM sig M k (mk_config ?? ins int) = Some ? (mk_config ?? outs outt) →
71 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))
72 =Some ? (mk_mconfig sig ? n outs (change_vec ?? vt outt i)).
73 #sig #n #M #i #k elim k -k
74 [#ins #int #outs #outt #vt #Hin normalize in ⊢ (%→?); #H destruct
75 |#k #Hind #ins #int #outs #outt #vt #Hin whd in ⊢ (??%?→??%?);
76 >halt_inject whd in match (cstate ????);
77 cases (true_or_false (halt sig M ins)) #Hhalt >Hhalt
79 [#H @eq_f whd in ⊢ (??%?); lapply (de_option ??? H) -H
80 whd in ⊢ (??%?→?); #H @eq_f2
81 [whd in ⊢ (??%?); destruct (H) //
82 |@(eq_vec … (niltape ?)) #j #lejn
83 cases (true_or_false (eqb i j)) #eqij
84 [>(eqb_true_to_eq … eqij) >nth_change_vec //
85 destruct (H) >nth_change_vec //
89 |>(config_expand … (step ???)) #H <(Hind … H) //
90 >loopM_unfold @eq_f >inject_step //
96 lemma cstate_inject: ∀sig,n,M,i,x. *)
98 definition inject_R ≝ λsig.λR:relation (tape sig).λn,i:nat.
99 λv1,v2: (Vector (tape sig) (S n)).
100 R (nth i ? v1 (niltape ?)) (nth i ? v2 (niltape ?)) ∧
101 ∀j. i ≠ j → nth j ? v1 (niltape ?) = nth j ? v2 (niltape ?).
104 lemma nth_make : ∀A,i,n,j,a,d. i < n → nth i ? (make_veci A a n j) d = a (j+i).
106 [#n #j #a #d #ltOn @(lt_O_n_elim … ltOn) <plus_n_O //
107 |#m #Hind #n #j #a #d #Hlt lapply Hlt @(lt_O_n_elim … (ltn_to_ltO … Hlt))
108 #p <plus_n_Sm #ltmp @Hind @le_S_S_to_le //
113 lemma mk_config_eq_s: ∀S,sig,s1,s2,t1,t2.
114 mk_config S sig s1 t1 = mk_config S sig s2 t2 → s1=s2.
115 #S #sig #s1 #s2 #t1 #t2 #H destruct //
118 lemma mk_config_eq_t: ∀S,sig,s1,s2,t1,t2.
119 mk_config S sig s1 t1 = mk_config S sig s2 t2 → s1=s2.
120 #S #sig #s1 #s2 #t1 #t2 #H destruct //
124 theorem sem_inject: ∀sig.∀M:TM sig.∀R.∀n,i.
125 i≤n → M ⊨ R → inject_TM sig M n i ⊨ inject_R sig R n i.
126 #sig #M #R #n #i #lein #HR #vt cases (HR (nth i ? vt (niltape ?)))
127 #k * * #outs #outt * #Hloop #HRout @(ex_intro ?? k)
128 @(ex_intro ?? (mk_mconfig ?? n outs (change_vec ? (S n) vt outt i))) %
129 [whd in ⊢ (??(?????%)?); <(change_vec_same ?? vt i (niltape ?)) in ⊢ (??%?);
130 @loop_inject /2 by refl, trans_eq, le_S_S/
131 |%[>nth_change_vec // @le_S_S //
132 |#j #i >nth_change_vec_neq //
137 theorem acc_sem_inject: ∀sig.∀M:TM sig.∀Rtrue,Rfalse,acc.∀n,i.
138 i≤n → M ⊨ [ acc : Rtrue, Rfalse ] →
139 inject_TM sig M n i ⊨ [ acc : inject_R sig Rtrue n i, inject_R sig Rfalse n i ].
140 #sig #M #Rtrue #Rfalse #acc #n #i #lein #HR #vt cases (HR (nth i ? vt (niltape ?)))
141 #k * * #outs #outt * * #Hloop #HRtrue #HRfalse @(ex_intro ?? k)
142 @(ex_intro ?? (mk_mconfig ?? n outs (change_vec ? (S n) vt outt i))) % [ %
143 [whd in ⊢ (??(?????%)?); <(change_vec_same ?? vt i (niltape ?)) in ⊢ (??%?);
144 @loop_inject /2 by refl, trans_eq, le_S_S/
146 [>nth_change_vec /2 by le_S_S/
147 |#j #Hneq >nth_change_vec_neq //
150 [>nth_change_vec /2 by le_S_S/ @HRfalse @Hqfalse
151 |#j #Hneq >nth_change_vec_neq //