matita/matita/lib/turing/simple_machines.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/if_multi.ma".
  13 include "turing/inject.ma".
  14 include "turing/basic_machines.ma".
  15
  16 definition Rtc_multi_true ≝
  17   λalpha,test,n,i.λt1,t2:Vector ? (S n).
  18    (∃c. current alpha (nth i ? t1 (niltape ?)) = Some ? c ∧ test c = true) ∧ t2 = t1.
  19
  20 definition Rtc_multi_false ≝
  21   λalpha,test,n,i.λt1,t2:Vector ? (S n).
  22     (∀c. current alpha (nth i ? t1 (niltape ?)) = Some ? c → test c = false) ∧ t2 = t1.
  23
  24 lemma sem_test_char_multi :
  25   ∀alpha,test,n,i.i ≤ n →
  26   inject_TM ? (test_char ? test) n i ⊨
  27   [ tc_true : Rtc_multi_true alpha test n i, Rtc_multi_false alpha test n i ].
  28 #alpha #test #n #i #Hin #int
  29 cases (acc_sem_inject … Hin (sem_test_char alpha test) int)
  30 #k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ %
  31 [ @Hloop
  32 | #Hqtrue lapply (Htrue Hqtrue) * * * #c *
  33   #Hcur #Htestc #Hnth_i #Hnth_j %
  34   [ %{c} % //
  35   | @(eq_vec … (niltape ?)) #i0 #Hi0
  36     cases (decidable_eq_nat i0 i) #Hi0i
  37     [ >Hi0i @Hnth_i
  38     | @sym_eq @Hnth_j @sym_not_eq // ] ] ]
  39 | #Hqfalse lapply (Hfalse Hqfalse) * * #Htestc #Hnth_i #Hnth_j %
  40   [ @Htestc
  41   | @(eq_vec … (niltape ?)) #i0 #Hi0
  42     cases (decidable_eq_nat i0 i) #Hi0i
  43     [ >Hi0i @Hnth_i
  44     | @sym_eq @Hnth_j @sym_not_eq // ] ] ]
  45 qed.
  46
  47 definition Rm_test_null_true ≝
  48   λalpha,n,i.λt1,t2:Vector ? (S n).
  49    current alpha (nth i ? t1 (niltape ?)) ≠ None ? ∧ t2 = t1.
  50
  51 definition Rm_test_null_false ≝
  52   λalpha,n,i.λt1,t2:Vector ? (S n).
  53     current alpha (nth i ? t1 (niltape ?)) = None ? ∧ t2 = t1.
  54
  55 lemma sem_test_null_multi : ∀alpha,n,i.i ≤ n →
  56   inject_TM ? (test_null ?) n i ⊨
  57     [ tc_true : Rm_test_null_true alpha n i, Rm_test_null_false alpha n i ].
  58 #alpha #n #i #Hin #int
  59 cases (acc_sem_inject … Hin (sem_test_null alpha) int)
  60 #k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ %
  61 [ @Hloop
  62 | #Hqtrue lapply (Htrue Hqtrue) * * #Hcur #Hnth_i #Hnth_j % //
  63   @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) #Hi0i
  64   [ >Hi0i @sym_eq @Hnth_i | @sym_eq @Hnth_j @sym_not_eq // ] ]
  65 | #Hqfalse lapply (Hfalse Hqfalse) * * #Hcur #Hnth_i #Hnth_j %
  66   [ @Hcur
  67   | @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) //
  68     #Hi0i @sym_eq @Hnth_j @sym_not_eq // ] ]
  69 qed.
  70 (* move a single tape *)
  71 definition mmove_states ≝ initN 2.
  72
  73 definition mmove0 : mmove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
  74 definition mmove1 : mmove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
  75
  76 definition trans_mmove ≝
  77  λi,sig,n,D.
  78  λp:mmove_states × (Vector (option sig) (S n)).
  79  let 〈q,a〉 ≝ p in match (pi1 … q) with
  80  [ O ⇒ 〈mmove1,change_vec ? (S n) (null_action ? n) (〈None ?,D〉) i〉
  81  | S _ ⇒ 〈mmove1,null_action sig n〉 ].
  82
  83 definition mmove ≝
  84   λi,sig,n,D.
  85   mk_mTM sig n mmove_states (trans_mmove i sig n D)
  86     mmove0 (λq.q == mmove1).
  87
  88 definition Rm_multi ≝
  89   λalpha,n,i,D.λt1,t2:Vector ? (S n).
  90   t2 = change_vec ? (S n) t1 (tape_move alpha (nth i ? t1 (niltape ?)) D) i.
  91
  92 lemma sem_move_multi :
  93   ∀alpha,n,i,D.i ≤ n →
  94   mmove i alpha n D ⊨ Rm_multi alpha n i D.
  95 #alpha #n #i #D #Hin #int %{2}
  96 %{(mk_mconfig ? mmove_states n mmove1 ?)}
  97 [| %
  98  [ whd in ⊢ (??%?); @eq_f whd in ⊢ (??%?); @eq_f %
  99  | whd >tape_move_multi_def
 100    <(change_vec_same … (ctapes …) i (niltape ?))
 101    >pmap_change <tape_move_multi_def >tape_move_null_action % ] ]
 102  qed.
 103
 104 (* simple copy with no move *)
 105 definition copy_states ≝ initN 3.
 106
 107 definition cc0 : copy_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
 108 definition cc1 : copy_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
 109
 110 definition trans_copy_char_N ≝
 111  λsrc,dst.λsig:FinSet.λn.
 112  λp:copy_states × (Vector (option sig) (S n)).
 113  let 〈q,a〉 ≝ p in
 114  match pi1 … q with
 115  [ O ⇒ 〈cc1,change_vec ? (S n)
 116            (change_vec ? (S n) (null_action ? n) (〈None ?,N〉) src)
 117            (〈nth src ? a (None ?),N〉) dst〉
 118  | S _ ⇒ 〈cc1,null_action ? n〉 ].
 119
 120 definition copy_char_N ≝
 121   λsrc,dst,sig,n.
 122   mk_mTM sig n copy_states (trans_copy_char_N src dst sig n)
 123     cc0 (λq.q == cc1).
 124
 125 definition R_copy_char_N ≝
 126   λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
 127   outt = change_vec ?? int
 128           (tape_write  ? (nth dst ? int (niltape ?))
 129             (current ? (nth src ? int (niltape ?)))) dst.
 130
 131 lemma copy_char_N_q0_q1 :
 132   ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n →
 133   step sig n (copy_char_N src dst sig n) (mk_mconfig ??? cc0 v) =
 134     mk_mconfig ??? cc1
 135      (change_vec ?? v
 136        (tape_write  ? (nth dst ? v (niltape ?))
 137           (current ? (nth src ? v (niltape ?)))) dst).
 138 #src #dst #sig #n #v #Heq #Hsrc #Hdst
 139 whd in ⊢ (??%?); @eq_f
 140 <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
 141 <(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
 142 >tape_move_multi_def
 143 >pmap_change >pmap_change <tape_move_multi_def
 144 >tape_move_null_action @eq_f3 //
 145 [ >change_vec_same %
 146 | >change_vec_same >change_vec_same >nth_current_chars // ]
 147 qed.
 148
 149 lemma sem_copy_char_N:
 150   ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
 151   copy_char_N src dst sig n ⊨ R_copy_char_N src dst sig n.
 152 #src #dst #sig #n #Hneq #Hsrc #Hdst #int
 153 %{2} % [| % [ % | whd >copy_char_N_q0_q1 // ]]
 154 qed.
 155
 156 (**************** copy and advance  ***********************)
 157 definition copy_char_states ≝ initN 3.
 158
 159 definition trans_copy_char ≝
 160  λsrc,dst.λsig:FinSet.λn.
 161  λp:copy_char_states × (Vector (option sig) (S n)).
 162  let 〈q,a〉 ≝ p in
 163  match pi1 … q with
 164  [ O ⇒ 〈cc1,change_vec ? (S n)
 165            (change_vec ? (S n) (null_action ? n) (〈None ?,R〉) src)
 166            (〈nth src ? a (None ?),R〉) dst〉
 167  | S _ ⇒ 〈cc1,null_action ? n〉 ].
 168
 169 definition copy_char ≝
 170   λsrc,dst,sig,n.
 171   mk_mTM sig n copy_char_states (trans_copy_char src dst sig n)
 172     cc0 (λq.q == cc1).
 173
 174 definition R_copy_char ≝
 175   λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
 176   outt = change_vec ??
 177          (change_vec ?? int
 178           (tape_move_mono ? (nth src ? int (niltape ?)) 〈None ?, R〉) src)
 179           (tape_move_mono ? (nth dst ? int (niltape ?))
 180            〈current ? (nth src ? int (niltape ?)), R〉) dst.
 181
 182 lemma copy_char_q0_q1 :
 183   ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n →
 184   step sig n (copy_char src dst sig n) (mk_mconfig ??? cc0 v) =
 185     mk_mconfig ??? cc1
 186      (change_vec ? (S n)
 187        (change_vec ?? v
 188          (tape_move_mono ? (nth src ? v (niltape ?)) 〈None ?, R〉) src)
 189             (tape_move_mono ? (nth dst ? v (niltape ?)) 〈current ? (nth src ? v (niltape ?)), R〉) dst).
 190 #src #dst #sig #n #v #Heq #Hsrc #Hdst
 191 whd in ⊢ (??%?);
 192 <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
 193 <(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
 194 >tape_move_multi_def @eq_f2 //
 195 >pmap_change >pmap_change <tape_move_multi_def
 196 >tape_move_null_action @eq_f2 // @eq_f2
 197 [ >change_vec_same %
 198 | >change_vec_same >change_vec_same // ]
 199 qed.
 200
 201 lemma sem_copy_char:
 202   ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
 203   copy_char src dst sig n ⊨ R_copy_char src dst sig n.
 204 #src #dst #sig #n #Hneq #Hsrc #Hdst #int
 205 %{2} % [| % [ % | whd >copy_char_q0_q1 // ]]
 206 qed.
 207
 208
 209
 210 (********************** look_ahead test *************************)
 211
 212 definition mtestR ≝ λsig,i,n,test.
 213   (mmove i sig n R) ·
 214     (ifTM ?? (inject_TM ? (test_char ? test) n i)
 215     (single_finalTM ?? (mmove i sig n L))
 216     (mmove i sig n L) tc_true).
 217
 218
 219 (* underspecified *)
 220 definition RmtestR_true ≝ λsig,i,n,test.λt1,t2:Vector ? n.
 221   ∀ls,c,c1,rs.
 222     nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
 223     t1 = t2 ∧ (test c1 = true).
 224
 225 definition RmtestR_false ≝ λsig,i,n,test.λt1,t2:Vector ? n.
 226   ∀ls,c,c1,rs.
 227     nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
 228     t1 = t2 ∧ (test c1 = false).
 229
 230 definition mtestR_acc: ∀sig,i,n,test.states ?? (mtestR sig i n test).
 231 #sig #i #n #test @inr @inr @inl @inr @start_nop
 232 qed.
 233
 234 lemma sem_mtestR: ∀sig,i,n,test. i ≤ n →
 235   mtestR sig i n test ⊨
 236     [mtestR_acc sig i n test:
 237        RmtestR_true sig  i (S n) test, RmtestR_false sig i (S n) test].
 238 #sig #i #n #test #Hlein
 239 @(acc_sem_seq_app sig n … (sem_move_multi … R Hlein)
 240    (acc_sem_if sig n ????????
 241      (sem_test_char_multi sig test n i Hlein)
 242      (sem_move_multi … L Hlein)
 243      (sem_move_multi … L Hlein)))
 244   [#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in  ⊢ (%→?); * *
 245    #cx #Hcx #Htx #Ht2 #ls #c #c1 #rs #Ht1
 246    >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
 247    >Ht3 in Hcx; >nth_change_vec [|@le_S_S //] * whd in ⊢ (??%?→?);
 248    #Hsome destruct (Hsome) #Htest % [2:@Htest]
 249    >Htx in Ht2; whd in ⊢ (%→?); #Ht2 @(eq_vec … (niltape ?))
 250    #j #lejn cases (true_or_false (eqb i j)) #Hij
 251     [lapply lejn <(eqb_true_to_eq … Hij) #lein >Ht2 >nth_change_vec [2://]
 252      >Ht3 >nth_change_vec >Ht1 //
 253     |lapply (eqb_false_to_not_eq … Hij) #Hneq >Ht2 >nth_change_vec_neq [2://]
 254      >Ht3 >nth_change_vec_neq //
 255     ]
 256   |#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in  ⊢ (%→?); *
 257    #Hcx #Heqtx #Htx #ls #c #c1 #rs #Ht1
 258    >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
 259    >Ht3 in Hcx; >nth_change_vec [2:@le_S_S //] #Hcx lapply (Hcx ? (refl ??))
 260    #Htest % // @(eq_vec … (niltape ?))
 261    #j #lejn cases (true_or_false (eqb i j)) #Hij
 262     [lapply lejn <(eqb_true_to_eq … Hij) #lein >Htx >nth_change_vec [2://]
 263      >Heqtx >Ht3 >nth_change_vec >Ht1 //
 264     |lapply (eqb_false_to_not_eq … Hij) #Hneq >Htx >nth_change_vec_neq [2://]
 265      >Heqtx >Ht3 >nth_change_vec_neq //
 266     ]
 267   ]
 268 qed.
 269