matita/matita/lib/turing/inject.ma

   1 (*
   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.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_____________________________________________________________*)
  11
  12 include "turing/turing.ma".
  13 (* include "turing/basic_machines.ma". *)
  14
  15 (******************* inject a mono machine into a multi tape one **********************)
  16
  17 definition inject_trans ≝ λsig,states:FinSet.λn,i:nat.
  18   λtrans:states × (option sig) → states  × (option sig × move).
  19   λp:states × (Vector (option sig) (S n)).
  20   let 〈q,a〉 ≝ p in
  21   let 〈nq,na〉 ≝ trans 〈q,nth i ? a (None ?)〉 in
  22   〈nq, change_vec ? (S n) (null_action ? n) na i〉.
  23
  24 definition inject_TM ≝ λsig.λM:TM sig.λn,i.
  25   mk_mTM sig n
  26     (states ? M)
  27     (inject_trans sig (states ? M) n i ?) (* (trans sig M))*)
  28     (start ? M)
  29     (halt ? M).
  30 (* ????? *)
  31 lapply (trans sig M)  #trans #x lapply (trans x) * *
  32 #s #a #m % [ @s | % [ @a | @m ] ]
  33 qed.
  34
  35 lemma current_chars_change_vec: ∀sig,n,v,a,i. i < S n →
  36    current_chars sig ? (change_vec ? (S n) v a i) =
  37    change_vec ? (S n)(current_chars ?? v) (current ? a) i.
  38 #sig #n #v #a #i #Hi @(eq_vec … (None ?)) #i0 #Hi0
  39 change with (vec_map ?????) in match (current_chars ???);
  40 <(nth_vec_map … (niltape ?))
  41 cases (decidable_eq_nat i i0) #Hii0
  42 [ >Hii0 >nth_change_vec // >nth_change_vec //
  43 | >nth_change_vec_neq // >nth_change_vec_neq // @nth_vec_map ]
  44 qed.
  45
  46 lemma inject_trans_def :∀sig:FinSet.∀n,i:nat.i < S n →
  47   ∀M,v,s,a,sn,an,mn.
  48   trans sig M 〈s,a〉 = 〈sn,an,mn〉 →
  49   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〉 =
  50     〈sn,change_vec ? (S n) (null_action ? n) 〈an,mn〉 i〉.
  51 #sig #n #i #Hlt #M #v #s #a #sn #an #mn #Htrans
  52 whd in ⊢ (??%?); >nth_change_vec // >Htrans //
  53 qed.
  54
  55 lemma inj_ter: ∀A,B,C.∀p:A×B×C.
  56   p = 〈\fst (\fst p), \snd (\fst p), \snd p〉.
  57 // qed.
  58
  59 lemma inject_step : ∀sig,n,M,i,q,t,nq,nt,v. i < S n →
  60   step sig M (mk_config ?? q t) = mk_config ?? nq nt →
  61   cic:/matita/turing/turing/step#def:12 sig n (inject_TM sig M n i)
  62     (mk_mconfig ?? n q (change_vec ? (S n) v t i))
  63   = mk_mconfig ?? n nq (change_vec ? (S n) v nt i).
  64 #sig #n #M #i #q #t #nq #nt #v #lein whd in ⊢ (??%?→?);
  65 whd in match (step ????); >(current_chars_change_vec … lein)
  66 >(inj_ter … (trans sig M ?)) whd in ⊢ (??%?→?); #H
  67 >(inject_trans_def sig n i lein M …)
  68 [|>(eq_pair_fst_snd ?? (trans sig M 〈q,current sig t〉))
  69   >(eq_pair_fst_snd ?? (\fst (trans sig M 〈q,current sig t〉))) %
  70 | *: skip ]
  71 whd in ⊢ (??%?); @eq_f2 [destruct (H) // ]
  72 @(eq_vec … (niltape ?)) #i0 #lei0n
  73 cases (decidable_eq_nat … i i0) #Hii0
  74 [ >Hii0 >nth_change_vec // >tape_move_multi_def >pmap_change >nth_change_vec // destruct (H) //
  75 | >nth_change_vec_neq // >tape_move_multi_def  >pmap_change >nth_change_vec_neq //
  76   <tape_move_multi_def >tape_move_null_action //
  77 ]
  78 qed.
  79
  80 lemma halt_inject: ∀sig,n,M,i,x.
  81   cic:/matita/turing/turing/halt#fix:0:2:9 sig n (inject_TM sig M n i) x
  82    = halt sig M x.
  83 // qed.
  84
  85 lemma de_option: ∀A,a,b. Some A a = Some A b → a = b.
  86 #A #a #b #H destruct //
  87 qed.
  88
  89 lemma loop_inject: ∀sig,n,M,i,k,ins,int,outs,outt,vt.i < S n →
  90  loopM sig M k (mk_config ?? ins int) = Some ? (mk_config ?? outs outt) →
  91  cic:/matita/turing/turing/loopM#def:13 sig n (inject_TM sig M n i) k (mk_mconfig ?? n ins (change_vec ?? vt int i))
  92   =Some ? (mk_mconfig sig ? n outs (change_vec ?? vt outt i)).
  93 #sig #n #M #i #k elim k -k
  94   [#ins #int #outs #outt #vt #Hin normalize in ⊢ (%→?); #H destruct
  95   |#k #Hind #ins #int #outs #outt #vt #Hin whd in ⊢ (??%?→??%?);
  96    >halt_inject whd in match (cstate ????);
  97    cases (true_or_false (halt sig M ins)) #Hhalt >Hhalt
  98    whd in ⊢ (??%?→??%?);
  99     [#H @eq_f whd in ⊢ (??%?); lapply (de_option ??? H) -H
 100      whd  in ⊢ (??%?→?); #H @eq_f2
 101       [whd in ⊢ (??%?); destruct (H) //
 102       |@(eq_vec … (niltape ?)) #j #lejn
 103        cases (true_or_false (eqb i j)) #eqij
 104         [>(eqb_true_to_eq … eqij) >nth_change_vec //
 105          destruct (H) >nth_change_vec //
 106         |destruct (H) //
 107         ]
 108       ]
 109     |>(config_expand … (step ???)) #H <(Hind … H) //
 110      >loopM_unfold @eq_f >inject_step //
 111     ]
 112   ]
 113 qed.
 114
 115 definition inject_R ≝ λsig.λR:relation (tape sig).λn,i:nat.
 116   λv1,v2: (Vector (tape sig) (S n)).
 117   R (nth i ? v1 (niltape ?)) (nth i ? v2 (niltape ?)) ∧
 118   ∀j. i ≠ j → nth j ? v1 (niltape ?) = nth j ? v2 (niltape ?).
 119
 120 theorem sem_inject: ∀sig.∀M:TM sig.∀R.∀n,i.
 121  i≤n → M ⊨ R → inject_TM sig M n i ⊨ inject_R sig R n i.
 122 #sig #M #R #n #i #lein #HR #vt cases (HR (nth i ? vt (niltape ?)))
 123 #k * * #outs #outt * #Hloop #HRout @(ex_intro ?? k)
 124 @(ex_intro ?? (mk_mconfig ?? n outs (change_vec ? (S n) vt outt i))) %
 125   [whd in ⊢ (??(?????%)?); <(change_vec_same ?? vt i (niltape ?)) in ⊢ (??%?);
 126    @loop_inject /2 by refl, trans_eq, le_S_S/
 127   |%[>nth_change_vec // @le_S_S //
 128     |#j #i >nth_change_vec_neq //
 129     ]
 130   ]
 131 qed.
 132
 133 theorem acc_sem_inject: ∀sig.∀M:TM sig.∀Rtrue,Rfalse,acc.∀n,i.
 134  i≤n → M ⊨ [ acc : Rtrue, Rfalse ] →
 135  inject_TM sig M n i ⊨ [ acc : inject_R sig Rtrue n i, inject_R sig Rfalse n i ].
 136 #sig #M #Rtrue #Rfalse #acc #n #i #lein #HR #vt cases (HR (nth i ? vt (niltape ?)))
 137 #k * * #outs #outt * * #Hloop #HRtrue #HRfalse @(ex_intro ?? k)
 138 @(ex_intro ?? (mk_mconfig ?? n outs (change_vec ? (S n) vt outt i))) % [ %
 139   [whd in ⊢ (??(?????%)?); <(change_vec_same ?? vt i (niltape ?)) in ⊢ (??%?);
 140    @loop_inject /2 by refl, trans_eq, le_S_S/
 141   |#Hqtrue %
 142     [>nth_change_vec /2 by le_S_S/
 143     |#j #Hneq >nth_change_vec_neq //
 144     ] ]
 145   |#Hqfalse %
 146     [>nth_change_vec /2 by le_S_S/ @HRfalse @Hqfalse
 147     |#j #Hneq >nth_change_vec_neq //
 148     ] ]
 149 qed.