matita/matita/lib/turing/multi_to_mono/shift_trace_machines.ma

   1 include "turing/basic_machines.ma".
   2 include "turing/if_machine.ma".
   3 include "turing/multi_to_mono/trace_alphabet.ma".
   4
   5 (* a machine that shift the i trace r starting from the bord of the trace *)
   6
   7 (* vec is a coercion. Why should I insert it? *)
   8 definition mti_step ≝ λsig:FinSet.λn,i.
   9   ifTM (multi_sig sig n) (test_char ? (λc:multi_sig sig n.¬(nth i ? (vec … c) (blank ?))==blank ?))
  10      (single_finalTM … (ncombf_r (multi_sig sig n) (shift_i sig n i) (all_blank sig n)))
  11      (nop ?) tc_true.
  12
  13 definition Rmti_step_true ≝
  14 λsig,n,i,t1,t2.
  15   ∃b:multi_sig sig n. (nth i ? (vec … b) (blank ?) ≠ blank ?) ∧
  16     ((∃ls,a,rs.
  17        t1 = midtape (multi_sig sig n) ls b (a::rs) ∧
  18        t2 = midtape (multi_sig sig n) ((shift_i sig n i b a)::ls) a rs) ∨
  19      (∃ls.
  20        t1 = midtape ? ls b [] ∧
  21        t2 = rightof ? (shift_i sig n i b (all_blank sig n)) ls)).
  22
  23 (* 〈combf0,all_blank sig n〉 *)
  24 definition Rmti_step_false ≝
  25   λsig,n,i,t1,t2.
  26     (∀ls,b,rs. t1 = midtape (multi_sig sig n) ls b rs →
  27      (nth i ? (vec … b) (blank ?) = blank ?)) ∧ t2 = t1.
  28
  29 lemma sem_mti_step :
  30   ∀sig,n,i.
  31   mti_step sig n i  ⊨
  32     [inr … (inl … (inr … start_nop)): Rmti_step_true sig n i, Rmti_step_false sig n i].
  33 #sig #n #i
  34 @(acc_sem_if_app (multi_sig sig n) ??????????
  35      (sem_test_char …) (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
  36      (sem_nop (multi_sig sig n)))
  37   [#intape #outtape #tapea whd in ⊢ (%→%→%); * * #c *
  38    #Hcur cases (current_to_midtape … Hcur) #ls * #rs #Hintape
  39    #ctest #Htapea * #Hout1 #Hout2 @(ex_intro … c) %
  40     [@(\Pf (injective_notb … )) @ctest]
  41    generalize in match Hintape; -Hintape cases rs
  42     [#Hintape %2 @(ex_intro …ls) % // @Hout1 >Htapea @Hintape
  43     |#a #rs1 #Hintape %1
  44      @(ex_intro … ls) @(ex_intro … a) @(ex_intro … rs1) % //
  45      @Hout2 >Htapea @Hintape
  46     ]
  47   |#intape #outtape #tapea whd in ⊢ (%→%→%);
  48    * #Htest #tapea #outtape
  49    % // #ls #b #rs
  50    #intape lapply (Htest b ?) [>intape //] -Htest #Htest
  51    lapply (injective_notb ? true Htest) -Htest #Htest @(\P Htest)
  52   ]
  53 qed.
  54
  55 (* move tape i machine *)
  56 definition mti ≝
  57   λsig,n,i.whileTM (multi_sig sig n) (mti_step sig n i) (inr … (inl … (inr … start_nop))).
  58
  59 axiom daemon: ∀P:Prop.P.
  60
  61 definition R_mti ≝
  62   λsig,n,i,t1,t2.
  63     (∀a,rs. t1 = rightof ? a rs → t2 = t1) ∧
  64     (∀a,ls,rs.
  65       t1 = midtape (multi_sig sig n) ls a rs →
  66       (nth i ? (vec … a) (blank ?) = blank ? ∧ t2 = t1) ∨
  67       ((∃rs1,b,rs2,rss.
  68         rs = rs1@b::rs2 ∧
  69         nth i ? (vec … b) (blank ?) = (blank ?) ∧
  70         (∀x. mem ? x (a::rs1) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
  71         shift_l sig n i (a::rs1) rss ∧
  72         t2 = midtape (multi_sig sig n) ((reverse ? rss)@ls) b rs2) ∨
  73       (∃b,rss.
  74         (∀x. mem ? x (a::rs) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
  75         shift_l sig n i (a::rs) (rss@[b]) ∧
  76         t2 = rightof (multi_sig sig n) (shift_i sig n i b (all_blank sig n))
  77          ((reverse ? rss)@ls)))).
  78
  79 lemma sem_mti:
  80   ∀sig,n,i.
  81   WRealize (multi_sig sig n) (mti sig n i) (R_mti sig n i).
  82 #sig #n #i #inc #j #outc #Hloop
  83 lapply (sem_while … (sem_mti_step sig n i) inc j outc Hloop) [%]
  84 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
  85 [ whd in ⊢ (% → ?); * #H1 #H2 %
  86   [#a #rs #Htape1 @H2
  87   |#a #ls #rs #Htapea % % [@(H1 … Htapea) |@H2]
  88   ]
  89 | #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
  90   lapply (IH HRfalse) -IH -HRfalse whd in ⊢ (%→%);
  91   * #IH1 #IH2 %
  92   [#b0 #ls #Htapeb cases Hstar1 #b * #_ *
  93     [* #ls0 * #a * #rs0 * >Htapeb #H destruct (H)
  94     |* #ls0 * >Htapeb #H destruct (H)
  95     ]
  96   |#b0 #ls #rs #Htapeb cases Hstar1 #b * #btest *
  97   [* #ls1 * #a * #rs1 * >Htapeb #H destruct (H) #Htapec
  98    %2 cases (IH2 … Htapec)
  99     [(* case a = None *)
 100      * #testa #Hout %1
 101      %{[ ]} %{a} %{rs1} %{[shift_i sig n i b a]} %
 102       [%[%[% // |#x #Hb >(mem_single ??? Hb) // ]
 103         |@daemon]
 104       |>Hout >reverse_single @Htapec
 105       ]
 106     |*
 107       [ (* case a \= None and exists b = None *) -IH1 -IH2 #IH
 108         %1 cases IH -IH #rs10 * #b0 * #rs2 * #rss * * * *
 109         #H1 #H2 #H3 #H4 #H5
 110         %{(a::rs10)} %{b0} %{rs2} %{(shift_i sig n i b a::rss)}
 111         %[%[%[%[>H1 //|@H2]
 112             |#x * [#eqxa >eqxa (*?? *) @daemon|@H3]]
 113           |@daemon]
 114         |>H5 >reverse_cons >associative_append //
 115         ]
 116       | (* case a \= None and we reach the end of the (full) tape *) -IH1 -IH2 #IH
 117         %2 cases IH -IH #b0 * #rss * * #H1 #H2 #H3
 118         %{b0} %{(shift_i sig n i b a::rss)}
 119         %[%[#x * [#eqxb >eqxb @btest|@H1]
 120            |@daemon]
 121         |>H3 >reverse_cons >associative_append //
 122         ]
 123       ]
 124     ]
 125   |(* b \= None but the left tape is empty *)
 126    * #ls0 * >Htapeb #H destruct (H) #Htapec
 127    %2 %2 %{b} %{[ ]}
 128    %[%[#x * [#eqxb >eqxb @btest|@False_ind]
 129       |@daemon (*shift of  dingle char OK *)]
 130     |>(IH1 … Htapec) >Htapec //
 131     ]
 132   ]
 133 qed.
 134
 135 lemma WF_mti_niltape:
 136   ∀sig,n,i. WF ? (inv ? (Rmti_step_true sig n i)) (niltape ?).
 137 #sig #n #i @wf #t1 whd in ⊢ (%→?); * #b * #_ *
 138   [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
 139 qed.
 140
 141 lemma WF_mti_rightof:
 142   ∀sig,n,i,a,ls. WF ? (inv ? (Rmti_step_true sig n i)) (rightof ? a ls).
 143 #sig #n #i #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ *
 144   [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
 145 qed.
 146
 147 lemma WF_mti_leftof:
 148   ∀sig,n,i,a,ls. WF ? (inv ? (Rmti_step_true sig n i)) (leftof ? a ls).
 149 #sig #n #i #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ *
 150   [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
 151 qed.
 152
 153 lemma terminate_mti:
 154   ∀sig,n,i.∀t. Terminate ? (mti sig n i) t.
 155 #sig #n #i #t @(terminate_while … (sem_mti_step sig n i)) [%]
 156 cases t // #ls #c #rs lapply c -c lapply ls -ls  elim rs
 157   [#ls #c @wf #t1 whd in ⊢ (%→?); * #b * #_ *
 158     [* #ls1 * #a * #rs1 * #H destruct
 159     |* #ls1 * #H destruct #Ht1 >Ht1 //
 160     ]
 161   |#a #rs1 #Hind #ls #c @wf #t1 whd in ⊢ (%→?); * #b * #_ *
 162     [* #ls1 * #a2 * #rs2 * #H destruct (H) #Ht1 >Ht1 //
 163     |* #ls1 *  #H destruct
 164     ]
 165   ]
 166 qed.
 167
 168 lemma ssem_mti: ∀sig,n,i.
 169   Realize ? (mti sig n i) (R_mti sig n i).
 170 /2/ qed.
 171