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
  71 (* move a single tape *)
  72 definition smove_states ≝ initN 2.
  73
  74 definition smove0 : smove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
  75 definition smove1 : smove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
  76
  77 definition trans_smove ≝
  78  λsig,D.
  79  λp:smove_states × (option sig).
  80  let 〈q,a〉 ≝ p in match (pi1 … q) with
  81  [ O ⇒ 〈smove1,None sig, D〉
  82  | S _ ⇒ 〈smove1,None sig, N〉 ].
  83
  84 definition move ≝
  85   λsig,D.mk_TM sig smove_states (trans_smove sig D) smove0 (λq.q == smove1).
  86
  87 definition mmove ≝ λi,sig,n,D.inject_TM sig (move sig D) n i.
  88
  89 definition Rmove ≝
  90   λalpha,D,t1,t2. t2 = tape_move alpha t1 D.
  91
  92 lemma sem_move_single :
  93   ∀alpha,D.move alpha D ⊨ Rmove alpha D.
  94 #alpha #D #int %{2} %{(mk_config ? smove_states smove1 ?)} [| % % ]
  95 qed.
  96
  97 definition Rm_multi ≝
  98   λalpha,n,i,D.λt1,t2:Vector ? (S n).
  99   t2 = change_vec ? (S n) t1 (tape_move alpha (nth i ? t1 (niltape ?)) D) i.
 100
 101 lemma sem_move_multi :
 102   ∀alpha,n,i,D.i ≤ n →
 103   mmove i alpha n D ⊨ Rm_multi alpha n i D.
 104 #alpha #n #i #D #Hin #ta cases (sem_inject … Hin (sem_move_single alpha D) ta)
 105 #k * #outc * #Hloop * whd in ⊢ (%→?); #Htb1 #Htb2 %{k} %{outc} % [ @Hloop ]
 106 whd @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) #Hi0i
 107 [ >Hi0i >Htb1 >nth_change_vec //
 108 | >nth_change_vec_neq [|@sym_not_eq //] <Htb2 // @sym_not_eq // ]
 109 qed.
 110
 111 (* simple copy with no move *)
 112 definition copy_states ≝ initN 3.
 113
 114 definition cc0 : copy_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
 115 definition cc1 : copy_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
 116
 117 definition trans_copy_char_N ≝
 118  λsrc,dst.λsig:FinSet.λn.
 119  λp:copy_states × (Vector (option sig) (S n)).
 120  let 〈q,a〉 ≝ p in
 121  match pi1 … q with
 122  [ O ⇒ 〈cc1,change_vec ? (S n)
 123            (change_vec ? (S n) (null_action ? n) (〈None ?,N〉) src)
 124            (〈nth src ? a (None ?),N〉) dst〉
 125  | S _ ⇒ 〈cc1,null_action ? n〉 ].
 126
 127 definition copy_char_N ≝
 128   λsrc,dst,sig,n.
 129   mk_mTM sig n copy_states (trans_copy_char_N src dst sig n)
 130     cc0 (λq.q == cc1).
 131
 132 definition R_copy_char_N ≝
 133   λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
 134   outt = change_vec ?? int
 135           (tape_write  ? (nth dst ? int (niltape ?))
 136             (current ? (nth src ? int (niltape ?)))) dst.
 137
 138 lemma copy_char_N_q0_q1 :
 139   ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n →
 140   step sig n (copy_char_N src dst sig n) (mk_mconfig ??? cc0 v) =
 141     mk_mconfig ??? cc1
 142      (change_vec ?? v
 143        (tape_write  ? (nth dst ? v (niltape ?))
 144           (current ? (nth src ? v (niltape ?)))) dst).
 145 #src #dst #sig #n #v #Heq #Hsrc #Hdst
 146 whd in ⊢ (??%?); @eq_f
 147 <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
 148 <(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
 149 >tape_move_multi_def
 150 >pmap_change >pmap_change <tape_move_multi_def
 151 >tape_move_null_action @eq_f3 //
 152 [ >change_vec_same %
 153 | >change_vec_same >change_vec_same >nth_current_chars // ]
 154 qed.
 155
 156 lemma sem_copy_char_N:
 157   ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
 158   copy_char_N src dst sig n ⊨ R_copy_char_N src dst sig n.
 159 #src #dst #sig #n #Hneq #Hsrc #Hdst #int
 160 %{2} % [| % [ % | whd >copy_char_N_q0_q1 // ]]
 161 qed.
 162
 163 (**************** copy and advance  ***********************)
 164 definition copy_char_states ≝ initN 3.
 165
 166 definition trans_copy_char ≝
 167  λsrc,dst.λsig:FinSet.λn.
 168  λp:copy_char_states × (Vector (option sig) (S n)).
 169  let 〈q,a〉 ≝ p in
 170  match pi1 … q with
 171  [ O ⇒ 〈cc1,change_vec ? (S n)
 172            (change_vec ? (S n) (null_action ? n) (〈None ?,R〉) src)
 173            (〈nth src ? a (None ?),R〉) dst〉
 174  | S _ ⇒ 〈cc1,null_action ? n〉 ].
 175
 176 definition copy_char ≝
 177   λsrc,dst,sig,n.
 178   mk_mTM sig n copy_char_states (trans_copy_char src dst sig n)
 179     cc0 (λq.q == cc1).
 180
 181 definition R_copy_char ≝
 182   λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
 183   outt = change_vec ??
 184          (change_vec ?? int
 185           (tape_move_mono ? (nth src ? int (niltape ?)) 〈None ?, R〉) src)
 186           (tape_move_mono ? (nth dst ? int (niltape ?))
 187            〈current ? (nth src ? int (niltape ?)), R〉) dst.
 188
 189 lemma copy_char_q0_q1 :
 190   ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n →
 191   step sig n (copy_char src dst sig n) (mk_mconfig ??? cc0 v) =
 192     mk_mconfig ??? cc1
 193      (change_vec ? (S n)
 194        (change_vec ?? v
 195          (tape_move_mono ? (nth src ? v (niltape ?)) 〈None ?, R〉) src)
 196             (tape_move_mono ? (nth dst ? v (niltape ?)) 〈current ? (nth src ? v (niltape ?)), R〉) dst).
 197 #src #dst #sig #n #v #Heq #Hsrc #Hdst
 198 whd in ⊢ (??%?);
 199 <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
 200 <(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
 201 >tape_move_multi_def @eq_f2 //
 202 >pmap_change >pmap_change <tape_move_multi_def
 203 >tape_move_null_action @eq_f2 // @eq_f2
 204 [ >change_vec_same %
 205 | >change_vec_same >change_vec_same // ]
 206 qed.
 207
 208 lemma sem_copy_char:
 209   ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
 210   copy_char src dst sig n ⊨ R_copy_char src dst sig n.
 211 #src #dst #sig #n #Hneq #Hsrc #Hdst #int
 212 %{2} % [| % [ % | whd >copy_char_q0_q1 // ]]
 213 qed.
 214
 215
 216
 217 (********************** look_ahead test *************************)
 218
 219 definition mtestR ≝ λsig,i,n,test.
 220   (mmove i sig n R) ·
 221     (ifTM ?? (inject_TM ? (test_char ? test) n i)
 222     (single_finalTM ?? (mmove i sig n L))
 223     (mmove i sig n L) tc_true).
 224
 225
 226 (* underspecified *)
 227 definition RmtestR_true ≝ λsig,i,n,test.λt1,t2:Vector ? n.
 228   ∀ls,c,c1,rs.
 229     nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
 230     t1 = t2 ∧ (test c1 = true).
 231
 232 definition RmtestR_false ≝ λsig,i,n,test.λt1,t2:Vector ? n.
 233   ∀ls,c,c1,rs.
 234     nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
 235     t1 = t2 ∧ (test c1 = false).
 236
 237 definition mtestR_acc: ∀sig,i,n,test.states ?? (mtestR sig i n test).
 238 #sig #i #n #test @inr @inr @inl @inr @start_nop
 239 qed.
 240
 241 lemma sem_mtestR: ∀sig,i,n,test. i ≤ n →
 242   mtestR sig i n test ⊨
 243     [mtestR_acc sig i n test:
 244        RmtestR_true sig  i (S n) test, RmtestR_false sig i (S n) test].
 245 #sig #i #n #test #Hlein
 246 @(acc_sem_seq_app sig n … (sem_move_multi … R Hlein)
 247    (acc_sem_if sig n ????????
 248      (sem_test_char_multi sig test n i Hlein)
 249      (sem_move_multi … L Hlein)
 250      (sem_move_multi … L Hlein)))
 251   [#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in  ⊢ (%→?); * *
 252    #cx #Hcx #Htx #Ht2 #ls #c #c1 #rs #Ht1
 253    >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
 254    >Ht3 in Hcx; >nth_change_vec [|@le_S_S //] * whd in ⊢ (??%?→?);
 255    #Hsome destruct (Hsome) #Htest % [2:@Htest]
 256    >Htx in Ht2; whd in ⊢ (%→?); #Ht2 @(eq_vec … (niltape ?))
 257    #j #lejn cases (true_or_false (eqb i j)) #Hij
 258     [lapply lejn <(eqb_true_to_eq … Hij) #lein >Ht2 >nth_change_vec [2://]
 259      >Ht3 >nth_change_vec >Ht1 //
 260     |lapply (eqb_false_to_not_eq … Hij) #Hneq >Ht2 >nth_change_vec_neq [2://]
 261      >Ht3 >nth_change_vec_neq //
 262     ]
 263   |#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in  ⊢ (%→?); *
 264    #Hcx #Heqtx #Htx #ls #c #c1 #rs #Ht1
 265    >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
 266    >Ht3 in Hcx; >nth_change_vec [2:@le_S_S //] #Hcx lapply (Hcx ? (refl ??))
 267    #Htest % // @(eq_vec … (niltape ?))
 268    #j #lejn cases (true_or_false (eqb i j)) #Hij
 269     [lapply lejn <(eqb_true_to_eq … Hij) #lein >Htx >nth_change_vec [2://]
 270      >Heqtx >Ht3 >nth_change_vec >Ht1 //
 271     |lapply (eqb_false_to_not_eq … Hij) #Hneq >Htx >nth_change_vec_neq [2://]
 272      >Heqtx >Ht3 >nth_change_vec_neq //
 273     ]
 274   ]
 275 qed.
 276