matita/matita/lib/turing/multi_to_mono/exec_trace_move.ma

   1 (* include "turing/auxiliary_machines.ma". *)
   2
   3 include "turing/multi_to_mono/shift_trace.ma".
   4
   5 (******************************************************************************)
   6
   7 (* exec_move_R : before shifting the trace left - to simulate a right move of
   8 the head - we must be sure we are not in rightoverflow, that is that the symbol
   9 at the right of the head, if any, is not blank *)
  10
  11 (* a simple look-ahead machine *)
  12 definition mtestR ≝ λsig,test.
  13   (move sig R) ·
  14     (ifTM ? (test_char ? test)
  15     (single_finalTM ? (move sig L))
  16     (move sig L) tc_true).
  17
  18 (* underspecified *)
  19 definition RmtestR_true ≝ λsig,test.λt1,t2.
  20   ∀ls,c,rs.
  21     t1 = midtape sig ls c rs →
  22     ∃c1,rs1. rs = c1::rs1 ∧ t1 = t2 ∧ (test c1 = true).
  23
  24 definition RmtestR_false ≝ λsig,test.λt1,t2.
  25   (∀ls,c,c1,rs.
  26     t1 = midtape sig ls c (c1::rs) →
  27     t1 = t2 ∧ (test c1 = false)) ∧
  28   (∀ls,c.
  29     t1 = midtape sig ls c [] → t1 = t2).
  30
  31 definition mtestR_acc: ∀sig,test.states ? (mtestR sig test).
  32 #sig #test @inr @inr @inl @inr @start_nop
  33 qed.
  34
  35 lemma sem_mtestR: ∀sig,test.
  36   mtestR sig test ⊨
  37     [mtestR_acc sig test:
  38        RmtestR_true sig  test, RmtestR_false sig test].
  39 #sig #test
  40 @(acc_sem_seq_app sig … (sem_move_single  … )
  41    (acc_sem_if sig …
  42      (sem_test_char sig test)
  43      (sem_move_single  … )
  44      (sem_move_single … )))
  45   [#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in  ⊢ (%→?); * *
  46    #cx * #Hcx #H1cx #Htx #Ht2 #ls #c #rs #Ht1
  47    >Ht1 in Hmove; cases rs
  48     [#H >H in Hcx; whd in ⊢ (??%?→?); #H1 destruct (H1)
  49     |#c1 #rs1 #Ht3 %{c1} %{rs1} %
  50       [% [//|>Htx in Ht2; >Ht3 whd in ⊢ (%→?); #H @sym_eq @H ]
  51       |>Ht3 in Hcx; whd in ⊢ (??%?→?); #H1 destruct (H1) //
  52       ]
  53     ]
  54   |#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in  ⊢ (%→?); *
  55    #Hcx #Heqtx #Htx %
  56     [#ls #c #c1 #rs #Ht1
  57      >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
  58      >Ht3 in Hcx; #Hcx lapply (Hcx ? (refl ??))
  59      #Htest % // >Heqtx in Htx; >Ht3 whd in ⊢ (%→?); #H @sym_eq @H
  60     |#ls0 #c0 #Ht1 >Ht1 in Hmove; whd in match (tape_move ???);
  61      <Heqtx #H1tx >H1tx in Htx; #H @sym_eq @H
  62     ]
  63   ]
  64 qed.
  65
  66 definition guarded_M ≝ λsig,n,i,M.
  67   (ifTM ? (test_char ? (not_blank sig n i))
  68    M
  69    (ifTM ? (mtestR ? (not_blank sig n i))
  70     M
  71     (nop ?) (mtestR_acc …)) tc_true).
  72
  73 definition R_guarded_M ≝ λsig,n,i,RM,t1,t2.
  74   ∀ls,a,rs. t1 = midtape ? ls a rs →
  75    (not_blank sig n i a = false →
  76      not_blank sig n i (hd ? rs (all_blanks …)) = false → t1=t2) ∧
  77    (not_blank sig n i a = true ∨
  78      not_blank sig n i (hd ? rs (all_blanks …)) = true → RM t1 t2).
  79
  80 lemma sem_R_guarded: ∀sig,n,i,M,RM. M ⊨ RM →
  81    guarded_M sig n i M ⊨ R_guarded_M sig n i RM.
  82 #sig #n #i #M #RM #HM
  83 @(sem_if_app … (sem_test_char … ) HM
  84   (sem_if … (sem_mtestR … ) HM (sem_nop ?)))
  85 #tin #tout #t1 *
  86   [* * * #c * #Hc #H1c #Ht1 #Htout #ls #a #rs #Htin
  87    >Htin in Hc; normalize in ⊢ (%→?); #H1 destruct (H1) %
  88     [>H1c #H2 @False_ind destruct (H2)
  89     |#H1 <Htin <Ht1 @Htout
  90     ]
  91   |* * #Hc #Ht1 #H #ls #a #rs lapply (Hc a) <Ht1 -Ht1 #Ha #Ht1
  92    cases H
  93     [* #t2 * #Ht2 lapply (Ht2 … Ht1)
  94      * #c1 * #rs1 * * #H1 #H2 #H3 #H4 % [2: //]
  95      #Ha >H1 whd in match (hd ???); >H3 #H destruct (H)
  96     |lapply Ht1 -Ht1 cases rs
  97       [#Ht1 * #t2 * * #_ #Ht2 lapply (Ht2 … Ht1) -Ht2 #Ht2
  98        whd in ⊢ (%→?); #Htout % [//] *
  99         [>Ha [#H destruct (H)| >Ht1 %]
 100         |whd in ⊢ (??%?→?); >blank_all_blanks whd in ⊢ (??%?→?);
 101          #H destruct (H)
 102         ]
 103       |#c #rs1 #Ht1 * #t2 * * #Ht2 #_ lapply (Ht2 … Ht1) -Ht2 *
 104        #Ht2 whd in ⊢ (??%?→?); #Hnb whd in ⊢ (%→?); #Htout % [//] *
 105         [>Ha [#H destruct (H)| >Ht1 %]
 106         |whd in ⊢ (??%?→?); whd in match (hd ???); >Hnb whd in ⊢ (??%?→?);
 107          #H destruct (H)
 108         ]
 109       ]
 110     ]
 111   ]
 112 qed.
 113
 114 definition move_R_i ≝ λA,sig,n,i.
 115   guarded_M ? (S n) i (mtiL A sig n i).
 116
 117 definition Rmove_R_i ≝ λA,sig,n,i.
 118   R_guarded_M ? (S n) i (Rmtil A sig n i).
 119
 120
 121 (*************************** readback of the tape *****************************)
 122
 123 definition opt_cur ≝ λsig,a.
 124   if a == blank sig then None ? else Some ? a.
 125
 126 definition rb_trace ≝ λsig,ls,a,rs.
 127   mk_tape ? (to_blank ? ls) (opt_cur sig a) (to_blank ? rs).
 128
 129 lemma rb_trace_def: ∀sig,ls,a,rs.
 130   rb_trace sig ls a rs =
 131     mk_tape ? (to_blank ? ls) (opt_cur sig a) (to_blank ? rs).
 132 // qed.
 133
 134 definition rb_trace_i ≝ λsig,n,ls,a,rs,i.
 135   rb_trace sig (trace ? n i ls) (nth i ? a (blank ?)) (trace ? n i rs).
 136
 137 lemma rb_trace_i_def: ∀sig,n,ls,a,rs,i.
 138   rb_trace_i sig n ls a rs i =
 139     rb_trace sig (trace ? n i ls) (nth i ? a (blank ?)) (trace ? n i rs).
 140 // qed.
 141
 142 let rec readback sig n ls a rs i on i : Vector (tape (sig_ext sig)) i ≝
 143   match i with
 144   [ O ⇒ mk_Vector ? 0 (nil ?) (refl ??)
 145   | S j ⇒ vec_cons ? (rb_trace_i sig n ls a rs j) j (readback sig n ls a rs j)
 146   ].
 147
 148 lemma orb_false_l: ∀b1,b2:bool.
 149   (b1 ∨ b2) = false → (b1 = false) ∧ (b2 = false).
 150 * * normalize /2/ qed.
 151
 152 lemma no_blank_true_to_not_blank: ∀sig,n,a,i.
 153   (not_blank sig n i a = true) → nth i ? (vec … n a) (blank sig) ≠ blank ?.
 154 #sig #n #a #i #H @(not_to_not … (eqnot_to_noteq … false H))
 155 -H #H normalize >H %
 156 qed.
 157
 158 lemma rb_move_R : ∀A,sig,n,ls,a,rs,outt,i.
 159   (∀i.regular_trace (TA A sig) (S n) a ls rs i) →
 160   is_head ?? (nth n ? (vec … a) (blank ?)) = true →
 161   no_head_in … ls →
 162   no_head_in … rs →
 163   Rmove_R_i … i (midtape ? ls a rs) outt →
 164   ∃ls1,a1,rs1.
 165    outt = midtape ? ls1 a1 rs1 ∧
 166    (∀i.regular_trace (TA A sig) (S n) a1 ls1 rs1 i) ∧
 167    rb_trace_i ? (S n) ls1 (vec … a1) rs1 i =
 168      tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs i) R ∧
 169    ∀j. j ≤ n → j ≠ i →
 170     rb_trace_i ? (S n) ls1 (vec … a1) rs1 j =
 171       rb_trace_i ? (S n) ls (vec … a) rs j.
 172 #A #sig #n #ls #a #rs #outt #i #Hreg #Hha #Hhls #Hhrs #Hmove
 173 lapply (Hmove … (refl …)) -Hmove * #HMove1 #HMove2
 174 cases (true_or_false (not_blank ? (S n) i a ∨
 175         not_blank ? (S n) i (hd ? rs (all_blanks ? (S n)))))
 176   [2: #Hcase cases (orb_false_l … Hcase) -Hcase #Hb1 #Hb2
 177    lapply (HMove1 … Hb1 Hb2) #Hout %{ls} %{a} %{rs}
 178    %[%[%[@sym_eq @Hout |@Hreg]
 179       |>rb_trace_i_def
 180        cut (nth i ? (vec … a) (blank ?) = blank ?)
 181         [@(\P ?) @injective_notb @Hb1] #Ha >Ha
 182        >rb_trace_def whd in match (opt_cur ??);
 183        cut (to_blank ? (trace ? (S n) i rs) = [])
 184         [@daemon] #Hrs >Hrs
 185        cases (to_blank ? (trace ? (S n) i ls)) //
 186       ]
 187     |//]
 188   |-HMove1 #Hb
 189    lapply(HMove2 (orb_true_l … Hb) … (refl …) Hha Hreg ? Hhls Hhrs) -HMove2
 190     [#Hb1 lapply Hb -Hb  whd in match (not_blank ? (S n) i a);
 191      >Hb1 #H @no_blank_true_to_not_blank @H]
 192    * #ls1 * #a1 * #rs1 * * * * * #H1 #H2 #H3 #H4 #H5 #H6
 193    %{ls1} %{a1} %{rs1}
 194    %[%[%[@H1|@H2]
 195       |(* either a is blank or not *)
 196        cases (true_or_false (not_blank ? (S n) i a)) #Hba
 197         [(* a not blank *)
 198          >rb_trace_i_def >rb_trace_def <to_blank_i_def >H5 >to_blank_cons_nb
 199           [2: @no_blank_true_to_not_blank //]
 200          lapply H6 -H6 #Hrs >(rb_trace_i_def … rs i) >rb_trace_def
 201          <(to_blank_i_def … rs) <Hrs
 202          cut (opt_cur ? (nth i ? (vec … a) (blank ?)) =
 203               Some ? (nth i ? (vec … a) (blank ?))) [@daemon] #Ha >Ha
 204          (* either a1 is blank or not *)
 205          cases (true_or_false (not_blank ? (S n) i a1)) #Hba1
 206           [cut (opt_cur ? (nth i ? (vec … a1) (blank ?)) =
 207                 Some ? (nth i ? (vec … a1) (blank ?))) [@daemon] #Ha1 >Ha1
 208            >to_blank_cons_nb [%|@(\Pf ?) @injective_notb @Hba1]
 209           |cut (opt_cur ? (nth i ? (vec … a1) (blank ?)) = None ?) [@daemon]
 210            #Ha1 >Ha1
 211            cut (to_blank_i … i (a1::rs1) = [ ]) [@daemon] #Ha1rs1 >Ha1rs1
 212            cut (to_blank_i … i rs1 = [ ]) [@daemon] #Hrs1 <to_blank_i_def >Hrs1 %
 213           ]
 214         |>rb_trace_i_def >rb_trace_def <to_blank_i_def (* >H5 >to_blank_cons_nb *)
 215          >rb_trace_i_def >rb_trace_def <(to_blank_i_def … rs) <H6 >H5
 216          cut (to_blank_i … i (a::ls) = [ ]) [@daemon] #Hals >Hals
 217          cut (to_blank_i … i ls = [ ]) [@daemon] #Hls <(to_blank_i_def … ls) >Hls
 218          cut (opt_cur ? (nth i ? (vec … a) (blank ?)) = None ?) [@daemon] #Ha >Ha
 219          cut (nth i ? (vec … a1) (blank ?) ≠ blank ?) [@daemon] #Ha1
 220          >(to_blank_cons_nb … Ha1)
 221          cut (opt_cur ? (nth i ? (vec … a1) (blank ?)) =
 222               Some ? (nth i ? (vec … a1) (blank ?))) [@daemon] -Ha1 #Ha1 >Ha1 %
 223         ]
 224       ]
 225     |(* case j ≠ i *)
 226      #j #Hle #Hneq >rb_trace_i_def >rb_trace_i_def >rb_trace_def >rb_trace_def
 227      <(to_blank_i_def … rs) <(to_blank_i_def … rs1) >(H4 j Hle Hneq)
 228      cut ((to_blank_i ? (S n) j ls1 = to_blank_i ? (S n) j ls) ∧
 229           (opt_cur ? (nth j ? (vec … a1) (blank ?)) =
 230            opt_cur ? (nth j ? (vec … a) (blank ?))))
 231       [@daemon] * #H7 #H8 <to_blank_i_def >H7 >H8 //
 232     ]
 233   ]
 234 qed.
 235
 236 definition Rmove_R_i_rb ≝ λA,sig,n,i,t1,t2.
 237 ∀ls,a,rs.
 238   t1 = midtape ? ls a rs →
 239   (∀i.regular_trace (TA A sig) (S n) a ls rs i) →
 240   is_head ?? (nth n ? (vec … a) (blank ?)) = true →
 241   no_head_in … ls →
 242   no_head_in … rs →
 243   ∃ls1,a1,rs1.
 244    t2 = midtape (MTA A sig (S n)) ls1 a1 rs1 ∧
 245    (∀i.regular_trace (TA A sig) (S n) a1 ls1 rs1 i) ∧
 246    rb_trace_i ? (S n) ls1 (vec … a1) rs1 i =
 247      tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs i) R ∧
 248    ∀j. j ≤ n → j ≠ i →
 249     rb_trace_i ? (S n) ls1 (vec … a1) rs1 j =
 250       rb_trace_i ? (S n) ls (vec … a) rs j.
 251
 252 lemma sem_move_R_i : ∀A,sig,n,i.i < n →
 253   move_R_i A sig n i ⊨ Rmove_R_i_rb A sig n i.
 254 #A #sig #n #i #ltin @(Realize_to_Realize … (Rmove_R_i A sig n i))
 255   [#t1 #t2 #H #ls #a #rs #H1 #H2 #H3 #H4 #H5 @rb_move_R // <H1 //
 256   |@sem_R_guarded @sem_Rmtil //
 257   ]
 258 qed.
 259
 260 (* move_L_i axiomatized *)
 261
 262 axiom move_L_i : ∀A,sig.∀n,i:nat.TM (MTA A sig (S n)).
 263
 264 definition Rmove_L_i_rb ≝ λA,sig,n,i,t1,t2.
 265 ∀ls,a,rs.
 266   t1 = midtape ? ls a rs →
 267   (∀i.regular_trace (TA A sig) (S n) a ls rs i) →
 268   is_head ?? (nth n ? (vec … a) (blank ?)) = true →
 269   no_head_in … ls →
 270   no_head_in … rs →
 271   ∃ls1,a1,rs1.
 272    t2 = midtape (MTA A sig (S n)) ls1 a1 rs1 ∧
 273    (∀i.regular_trace ? (S n) a1 ls1 rs1 i) ∧
 274    rb_trace_i ? (S n) ls1 (vec … a1) rs1 i =
 275      tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs i) L ∧
 276    ∀j. j ≤ n → j ≠ i →
 277     rb_trace_i ? (S n) ls1 (vec … a1) rs1 j =
 278       rb_trace_i ? (S n) ls (vec … a) rs j.
 279
 280 axiom sem_move_L_i : ∀A,sig,n,i.i < n →
 281   move_L_i A sig n i ⊨ Rmove_L_i_rb A sig n i.
 282
 283 (*
 284 lemma rb_move_L : ∀sig,n,ls,a,rs,outt,i.
 285   (∀i.regular_trace sig n a ls rs i) →
 286   nth n ? (vec … a) (blank ?) = head ? →
 287   no_head_in … ls →
 288   no_head_in … rs →
 289   Rmove_L_i … i (midtape ? ls a rs) outt →
 290   ∃ls1,a1,rs1.
 291    outt = midtape ? ls1 a1 rs1 ∧
 292    rb_trace_i sig n ls1 (vec … a1) rs1 i =
 293      tape_move ? (rb_trace_i sig n ls (vec … a) rs i) L ∧
 294    ∀j. j ≤n → j ≠ i →
 295     rb_trace_i sig n ls1 (vec … a1) rs1 j =
 296       rb_trace_i sig n ls (vec … a) rs j. *)
 297
 298 (* The following function read a move from  a vector of moves and executes it *)
 299
 300 (* The head character contains a state and a sequence of moves *)
 301
 302 definition HC ≝ λQ,n.FinProd Q (FinVector FinMove n).
 303
 304 let rec all_N n on n : FinVector FinMove n ≝
 305   match n with
 306   [ O ⇒ Vector_of_list ? []
 307   | S m ⇒ vec_cons ? N m (all_N m)
 308   ].
 309
 310 definition get_moves ≝ λQ,sig,n.λa:MTA (HC Q n) sig (S n).
 311   match nth n ? (vec … a) (blank ?) with
 312   [ None ⇒ all_N n
 313   | Some x ⇒ match x with
 314     [inl y ⇒ snd ?? y
 315     |inr y ⇒ all_N n]].
 316
 317 definition get_move ≝ λQ,sig,n.λa:MTA (HC Q n) sig (S n).λi.
 318   nth i ? (vec … (get_moves Q sig n a)) N.
 319
 320 definition exec_move_i ≝ λQ,sig,n,i.
 321     (ifTM ? (test_char ? (λa. (get_move Q sig n a i == R)))
 322       (move_R_i (HC Q n) sig n i)
 323       (ifTM ? (test_char ? (λa. (get_move Q sig n a i == L)))
 324         (move_L_i (HC Q n) sig n i)
 325         (nop ?) tc_true) tc_true).
 326
 327 definition R_exec_move_i ≝ λQ,sig,n,i,t1,t2.
 328 ∀a,ls,rs.
 329   t1 = midtape (MTA (HC Q n) sig (S n)) ls a rs →
 330   (∀i.regular_trace ? (S n) a ls rs i) →
 331   is_head ?? (nth n ? (vec … a) (blank ?)) = true →
 332   no_head_in … ls →
 333   no_head_in … rs →
 334   ∃ls1,a1,rs1.
 335    t2 = midtape (MTA (HC Q n) sig (S n)) ls1 a1 rs1 ∧
 336    (∀i.regular_trace ? (S n) a1 ls1 rs1 i) ∧
 337    rb_trace_i ? (S n) ls1 (vec … a1) rs1 i =
 338      tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs i) (get_move Q sig n a i) ∧
 339    ∀j. j ≤ n → j ≠ i →
 340     rb_trace_i ? (S n) ls1 (vec … a1) rs1 j =
 341       rb_trace_i ? (S n) ls (vec … a) rs j.
 342
 343 lemma  tape_move_N: ∀A,t. tape_move A t N = t.
 344 // qed.
 345
 346 lemma sem_exec_move_i: ∀Q,sig,n,i. i < n →
 347   exec_move_i Q sig n i ⊨ R_exec_move_i Q sig n i.
 348 #Q #sig #n #i #ltin
 349 @(sem_if_app … (sem_test_char …)
 350   (sem_move_R_i … ltin)
 351   (sem_if … (sem_test_char …)
 352     (sem_move_L_i … ltin) (sem_nop ?)))
 353 #tin #tout #t1 *
 354   [* * * #c * #Hc #HR #Ht1 #HMR
 355    #a #ls #rs #Htin >Htin in Hc; whd in ⊢ (??%?→?); #H destruct (H)
 356     >(\P HR) whd in HMR; @HMR >Ht1 @Htin
 357   |* * #HR #Ht1 >Ht1 *
 358     [* #t2 * * * #c * #Hc #HL #Ht2 #HML
 359      #a #ls #rs #Htin >Htin in Hc; whd in ⊢ (??%?→?); #H destruct (H)
 360      >(\P HL) @HML >Ht2 @Htin
 361     |* #t2 * * #HL #Ht2 >Ht2 whd in ⊢ (%→?); #Htout >Htout
 362      #a #ls #rs #Htin >Htin in HR; #HR >Htin in HL; #HL
 363      cut (get_move Q sig n a i = N)
 364       [lapply (HR a (refl … )) lapply (HL a (refl … ))
 365        cases (get_move Q sig n a i) normalize
 366         [#H destruct (H) |#_ #H destruct (H) | //]]
 367      #HN >HN >tape_move_N #Hreg #_ #_ #_
 368      %{ls} %{a} %{rs}
 369      %[%[%[%|@Hreg] |%] | //]
 370     ]
 371   ]
 372 qed.
 373
 374 axiom reg_inv : ∀A,sig,n,a,ls,rs,a1,ls1,rs1.
 375   regular_trace (TA A sig) (S n) a1 ls1 rs1 n →
 376   (rb_trace_i ? (S n) ls1 (vec … a1) rs1 n =
 377       rb_trace_i ? (S n) ls (vec  …  a) rs n) →
 378   is_head ?? (nth n ? (vec … (S n) a) (blank ?)) = true →
 379   no_head_in … ls →
 380   no_head_in … rs →
 381   is_head ?? (nth n ? (vec … a1) (blank ?)) = true ∧
 382   no_head_in … ls1 ∧ no_head_in … rs1.
 383
 384
 385
 386
 387
 388
 389
 390
 391
 392
 393
 394
 395