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
  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)).
  18   let 〈q,a〉 ≝ p in
  19   let 〈nq,na〉 ≝ trans 〈q,nth i ? a (None ?)〉 in
  20   let nai ≝ λj.if (eqb j i) then na else (None ?) in
  21   〈q, make_veci ? nai (S n) 0〉.
  22
  23 definition inject_TM ≝ λsig.λM:TM sig.λn,i.
  24   mk_mTM sig n
  25     (states ? M)
  26     (inject_trans ?? n i (trans ? M))
  27     (start ? M)
  28     (halt ? M).
  29
  30 definition inject_R ≝ λsig.λR:relation (tape sig).λn,i:nat.
  31   λv1,v2: (Vector (tape sig) (S n)).
  32   R (nth i ? v1 (niltape ?)) (nth i ? v2 (niltape ?)) ∧
  33   ∀j. j ≠ i → nth j ? v1 (niltape ?) = nth j ? v2 (niltape ?).
  34
  35 lemma nth_make : ∀A,i,n,j,a,d. i < n → nth i ? (make_veci A a n j) d = a (j+i).
  36 #A #i elim i
  37   [#n #j #a #d #ltOn @(lt_O_n_elim … ltOn) <plus_n_O //
  38   |#m #Hind #n #j #a #d #Hlt lapply Hlt @(lt_O_n_elim … (ltn_to_ltO … Hlt))
  39    #p <plus_n_Sm #ltmp @Hind @le_S_S_to_le //
  40   ]
  41 qed.
  42
  43 theorem sem_inject: ∀sig.∀M:TM sig.∀R.∀n,i.
  44  i≤n → M ⊨ R → inject_TM sig M n i ⊨ inject_R sig R n i.
  45 #sig #M #R #n #i #lein #HR #vt cases (HR (nth i ? vt (niltape ?)))
  46 #k * * #outs #outt * #Hloop #HRout @(ex_intro ?? k)
  47 @(ex_intro ?? (mk_mconfig ?? n outs ?) )
  48   [(* this is the vector of tapes in the last mk_config *)
  49    @(make_veci ? (λj.if (eqb j i) then outt else (nth j ? vt (niltape ?))) (S n) 0)
  50   |%
  51     [
  52     |%[>nth_make [>(eq_to_eqb_true … (refl ? i)) @HRout|@le_S_S //]
  53       |#j #neqji >nth_make [>(not_eq_to_eqb_false … neqji) // |@le_S_S //]
  54        normalize
  55
  56
  57
  58
  59
  60
  61