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