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