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

   1 include "turing/auxiliary_machines1.ma".
   2 include "turing/multi_to_mono/shift_trace_machines.ma".
   3
   4 (******************************************************************************)
   5 (* mtiL: complete move L for tape i. We reaching the left border of trace i,  *)
   6 (* add a blank if there is no more tape, then move the i-trace and finally    *)
   7 (* come back to the head position.                                            *)
   8 (******************************************************************************)
   9
  10 (******************************* move_to_blank_L ******************************)
  11 (* we compose machines together to reduce the number of output cases, and
  12    improve semantics *)
  13
  14 definition move_to_blank_L ≝ λsig,n,i.
  15   (move_until ? L (no_blank sig n i)) · extend ? (all_blank sig n).
  16
  17 definition R_move_to_blank_L ≝ λsig,n,i,t1,t2.
  18 (current ? t1 = None ? →
  19   t2 = midtape (multi_sig sig n) (left ? t1) (all_blank …) (right ? t1)) ∧
  20 ∀ls,a,rs.t1 = midtape ? ls a rs →
  21   ((no_blank sig n i a = false) ∧ t2 = t1) ∨
  22   (∃b,ls1,ls2.
  23     (no_blank sig n i b = false) ∧
  24     (∀j.j ≤n → to_blank_i ?? j (ls1@b::ls2) = to_blank_i ?? j ls) ∧
  25     t2 = midtape ? ls2 b ((reverse ? (a::ls1))@rs)).
  26
  27 definition R_move_to_blank_L_new ≝ λsig,n,i,t1,t2.
  28 (current ? t1 = None ? →
  29   t2 = midtape (multi_sig sig n) (left ? t1) (all_blank …) (right ? t1)) ∧
  30 ∀ls,a,rs.t1 = midtape ? ls a rs →
  31   (∃b,ls1,ls2.
  32     (no_blank sig n i b = false) ∧
  33     (hd ? (ls1@[b]) (all_blank …) = a) ∧ (* not implied by the next fact *)
  34     (∀j.j ≤n → to_blank_i ?? j (ls1@b::ls2) = to_blank_i ?? j (a::ls)) ∧
  35     t2 = midtape ? ls2 b ((reverse ? ls1)@rs)).
  36
  37 theorem sem_move_to_blank_L: ∀sig,n,i.
  38   move_to_blank_L sig n i  ⊨ R_move_to_blank_L sig n i.
  39 #sig #n #i
  40 @(sem_seq_app ??????
  41   (ssem_move_until_L ? (no_blank sig n i)) (sem_extend ? (all_blank sig n)))
  42 #tin #tout * #t1 * * #Ht1a #Ht1b * #Ht2a #Ht2b %
  43   [#Hcur >(Ht1a Hcur) in Ht2a; /2 by /
  44   |#ls #a #rs #Htin -Ht1a cases (Ht1b … Htin)
  45     [* #Hnb #Ht1 -Ht1b -Ht2a >Ht1 in Ht2b; >Htin #H %1
  46      % [//|@H normalize % #H1 destruct (H1)]
  47     |*
  48     [(* we find the blank *)
  49      * #ls1 * #b * #ls2 * * * #H1 #H2 #H3 #H4 %2
  50      %{b} %{ls1} %{ls2}
  51      %[%[@H2|>H1 //]
  52       |-Ht1b -Ht2a >H4 in Ht2b; #H5 @H5
  53        % normalize #H6 destruct (H6)
  54       ]
  55     |* #b * #lss * * #H1 #H2 #H3 %2
  56      %{(all_blank …)} %{ls} %{[ ]}
  57      %[%[whd in match (no_blank ????); >blank_all_blank // @daemon
  58         |@daemon (* make a lemma *)]
  59       |-Ht1b -Ht2b >H3 in Ht2a;
  60        whd in match (left ??); whd in match (right ??); #H4
  61        >H2 >reverse_append >reverse_single @H4 normalize //
  62       ]
  63     ]
  64   ]
  65 qed.
  66
  67 theorem sem_move_to_blank_L_new: ∀sig,n,i.
  68   move_to_blank_L sig n i  ⊨ R_move_to_blank_L_new sig n i.
  69 #sig #n #i
  70 @(Realize_to_Realize … (sem_move_to_blank_L sig n i))
  71 #t1 #t2 * #H1 #H2 % [@H1]
  72 #ls #a #rs #Ht1 lapply (H2 ls a rs Ht1) -H2 *
  73   [* #Ha #Ht2 >Ht2 %{a} %{[ ]} %{ls}
  74    %[%[%[@Ha| //]| normalize //] | @Ht1]
  75   |* #b * #ls1 * #ls2 * * * #Hblank #Ht2
  76    %{b} %{(a::ls1)} %{ls2}
  77    %[2:@Ht2|%[%[//|//]|
  78    #j #lejn whd in match (to_blank_i ????);
  79    whd in match (to_blank_i ???(a::ls));
  80    lapply (Hblank j lejn) whd in match (to_blank_i ????);
  81    whd in match (to_blank_i ???(a::ls)); #H >H %
  82   ]
  83 qed.
  84
  85 (******************************************************************************)
  86
  87 definition shift_i_L ≝ λsig,n,i.
  88    ncombf_r (multi_sig …) (shift_i sig n i) (all_blank sig n) ·
  89    mti sig n i ·
  90    extend ? (all_blank sig n).
  91
  92 definition R_shift_i_L ≝ λsig,n,i,t1,t2.
  93   (* ∀b:multi_sig sig n.∀ls.
  94     (t1 = midtape ? ls b [ ] →
  95      t2 = midtape (multi_sig sig n)
  96       ((shift_i sig n i b (all_blank sig n))::ls) (all_blank sig n) [ ]) ∧ *)
  97     (∀a,ls,rs.
  98       t1 = midtape ? ls a rs  →
  99       ((∃rs1,b,rs2,a1,rss.
 100         rs = rs1@b::rs2 ∧
 101         nth i ? (vec … b) (blank ?) = (blank ?) ∧
 102         (∀x. mem ? x rs1 → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
 103         shift_l sig n i (a::rs1) (a1::rss) ∧
 104         t2 = midtape (multi_sig sig n) ((reverse ? (a1::rss))@ls) b rs2) ∨
 105       (∃b,rss.
 106         (∀x. mem ? x rs → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
 107         shift_l sig n i (a::rs) (rss@[b]) ∧
 108         t2 = midtape (multi_sig sig n)
 109           ((reverse ? (rss@[b]))@ls) (all_blank sig n) [ ]))).
 110
 111 definition R_shift_i_L_new ≝ λsig,n,i,t1,t2.
 112   (∀a,ls,rs.
 113    t1 = midtape ? ls a rs  →
 114    ∃rs1,b,rs2,rss.
 115       b = hd ? rs2 (all_blank sig n) ∧
 116       nth i ? (vec … b) (blank ?) = (blank ?) ∧
 117       rs = rs1@rs2 ∧
 118       (∀x. mem ? x rs1 → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
 119       shift_l sig n i (a::rs1) rss ∧
 120       t2 = midtape (multi_sig sig n) ((reverse ? rss)@ls) b (tail ? rs2)).
 121
 122 theorem sem_shift_i_L: ∀sig,n,i. shift_i_L sig n i  ⊨ R_shift_i_L sig n i.
 123 #sig #n #i
 124 @(sem_seq_app ??????
 125   (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
 126    (sem_seq ????? (ssem_mti sig n i)
 127     (sem_extend ? (all_blank sig n))))
 128 #tin #tout * #t1 * * #Ht1a #Ht1b * #t2 * * #Ht2a #Ht2b * #Htout1 #Htout2
 129 (* #b #ls %
 130   [#Htin lapply (Ht1a … Htin) -Ht1a -Ht1b #Ht1
 131    lapply (Ht2a … Ht1) -Ht2a -Ht2b #Ht2 >Ht2 in Htout1;
 132    >Ht1 whd in match (left ??); whd in match (right ??); #Htout @Htout // *)
 133 #a #ls #rs cases rs
 134   [#Htin %2 %{(shift_i sig n i a (all_blank sig n))} %{[ ]}
 135    %[%[#x @False_ind | @daemon]
 136     |lapply (Ht1a … Htin) -Ht1a -Ht1b #Ht1
 137      lapply (Ht2a … Ht1) -Ht2a -Ht2b #Ht2 >Ht2 in Htout1;
 138      >Ht1 whd in match (left ??); whd in match (right ??); #Htout @Htout //
 139     ]
 140   |#a1 #rs1 #Htin
 141    lapply (Ht1b … Htin) -Ht1a -Ht1b #Ht1
 142    lapply (Ht2b … Ht1) -Ht2a -Ht2b *
 143     [(* a1 is blank *) * #H1 #H2 %1
 144      %{[ ]} %{a1} %{rs1} %{(shift_i sig n i a a1)} %{[ ]}
 145      %[%[%[%[// |//] |#x @False_ind] | @daemon]
 146       |>Htout2 [>H2 >reverse_single @Ht1 |>H2 >Ht1 normalize % #H destruct (H)]
 147       ]
 148     |*
 149     [* #rs10 * #b * #rs2 * #rss * * * * #H1 #H2 #H3 #H4
 150      #Ht2 %1
 151      %{(a1::rs10)} %{b} %{rs2} %{(shift_i sig n i a a1)} %{rss}
 152      %[%[%[%[>H1 //|//] |@H3] |@daemon ]
 153       |>reverse_cons >associative_append
 154        >H2 in Htout2; #Htout >Htout [@Ht2| >Ht2 normalize % #H destruct (H)]
 155       ]
 156     |* #b * #rss * * #H1 #H2
 157      #Ht2 %2
 158      %{(shift_i sig n i b (all_blank sig n))} %{(shift_i sig n i a a1::rss)}
 159      %[%[@H1 |@daemon ]
 160       |>Ht2 in Htout1; #Htout >Htout //
 161        whd in match (left ??); whd in match (right ??);
 162        >reverse_append >reverse_single >associative_append  >reverse_cons
 163        >associative_append //
 164        ]
 165      ]
 166    ]
 167  ]
 168 qed.
 169
 170 theorem sem_shift_i_L_new: ∀sig,n,i.
 171   shift_i_L sig n i  ⊨ R_shift_i_L_new sig n i.
 172 #sig #n #i
 173 @(Realize_to_Realize … (sem_shift_i_L sig n i))
 174 #t1 #t2 #H #a #ls #rs #Ht1 lapply (H a ls rs Ht1) *
 175   [* #rs1 * #b * #rs2 * #a1 * #rss * * * * #H1 #H2 #H3 #H4 #Ht2
 176    %{rs1} %{b} %{(b::rs2)} %{(a1::rss)}
 177    %[%[%[%[%[//|@H2]|@H1]|@H3]|@H4] | whd in match (tail ??); @Ht2]
 178   |* #b * #rss * * #H1 #H2 #Ht2
 179    %{rs} %{(all_blank sig n)} %{[]} %{(rss@[b])}
 180    %[%[%[%[%[//|@blank_all_blank]|//]|@H1]|@H2] | whd in match (tail ??); @Ht2]
 181   ]
 182 qed.
 183
 184
 185 (******************************************************************************)
 186
 187 definition mtiL ≝ λsig,n,i.
 188    move_to_blank_L sig n i ·
 189    shift_i_L sig n i ·
 190    move_until ? L (no_head sig n).
 191
 192 definition Rmtil ≝ λsig,n,i,t1,t2.
 193   ∀ls,a,rs.
 194    t1 = midtape (multi_sig sig n) ls a rs →
 195    nth n ? (vec … a) (blank ?) = head ? →
 196    no_head_in … ls →
 197    no_head_in … rs  →
 198    (∃ls1,a1,rs1.
 199      t2 = midtape (multi_sig …) ls1 a1 rs1 ∧
 200      (∀j. j ≤ n → j ≠ i → to_blank_i ? n j (a1::ls1) = to_blank_i ? n j (a::ls)) ∧
 201      (∀j. j ≤ n → j ≠ i → to_blank_i ? n j rs1 = to_blank_i ? n j rs) ∧
 202      (to_blank_i ? n i ls1 = to_blank_i ? n i (a::ls)) ∧
 203      (to_blank_i ? n i (a1::rs1)) = to_blank_i ? n i rs).
 204
 205 theorem sem_Rmtil: ∀sig,n,i. i < n → mtiL sig n i  ⊨ Rmtil sig n i.
 206 #sig #n #i #lt_in
 207 @(sem_seq_app ??????
 208   (sem_move_to_blank_L_new … )
 209    (sem_seq ????? (sem_shift_i_L_new …)
 210     (ssem_move_until_L ? (no_head sig n))))
 211 #tin #tout * #t1 * * #_ #Ht1 * #t2 * #Ht2 * #_ #Htout
 212 (* we start looking into Rmitl *)
 213 #ls #a #rs #Htin (* tin is a midtape *)
 214 #Hhead #Hnohead_ls #Hnohead_rs
 215 lapply (Ht1 … Htin) -Ht1 -Htin
 216 * #b * #ls1 * #ls2 * * * #Hno_blankb #Hhead #Hls1 #Ht1
 217 lapply (Ht2 … Ht1) -Ht2 -Ht1
 218 * #rs1 * #b0 * #rs2 * #rss * * * * * #Hb0 #Hb0blank #Hrs1 #Hrs1b #Hrss #Ht2
 219 (* we need to recover the position of the head of the emulated machine
 220    that is the head of ls1. This is somewhere inside rs1 *)
 221 cut (∃rs11. rs1 = (reverse ? ls1)@rs11)
 222      [cut (ls1 = [ ] ∨ ∃aa,tlls1. ls1 = aa::tlls1)
 223        [cases ls1 [%1 // | #aa #tlls1 %2 %{aa} %{tlls1} //]] *
 224        [#H1ls1 %{rs1} >H1ls1 //
 225        |* #aa * #tlls1 #H1ls1 >H1ls1 in Hrs1;
 226         cut (aa = a) [>H1ls1 in Hls1; #H @(to_blank_hd … H)] #eqaa >eqaa
 227         #Hrs1_aux cases (compare_append … (sym_eq … Hrs1_aux)) #l *
 228          [* #H1 #H2 %{l} @H1
 229          |(* this is absurd : if l is empty, the case is as before.
 230            if l is not empty then it must start with a blank, since it is the
 231            frist character in rs2. But in this case we would have a blank
 232            inside ls1=attls1 that is absurd *)
 233           @daemon
 234          ]]]
 235    * #rs11 #H1
 236 lapply (Htout … Ht2) -Htout -Ht2 *
 237   [(* the current character on trace i hold the head-mark.
 238       The case is absurd, since b0 is the head of rs2, that is a sublist of rs,
 239       and the head-mark is not in rs *)
 240    @daemon
 241    (* something is missing
 242    * #H @False_ind @(absurd ? H) @eqnot_to_noteq whd in ⊢ (???%);
 243    cut (rs2 = [ ] ∨ ∃c,rs21. rs2 = c::rs21)
 244     [cases rs2 [ %1 // | #c #rs22 %2 %{c} %{rs22} //]]
 245    * (* by cases on rs2 *)
 246     [#Hrs2 >Hb0 >Hrs2 normalize >all_blank_n //
 247     |* #c * #rs22 #Hrs2 destruct (Hrs2) @no_head_true @Hnohead_rs
 248      > *)
 249   |*
 250   [(* we reach the head position *)
 251    (* cut (trace sig n j (a1::ls20)=trace sig n j (ls1@b::ls2)) *)
 252    * #ls10 * #a1 * #ls20 * * * #Hls20 #Ha1 #Hnh #Htout
 253    cut (∀j.j ≠ i →
 254       trace sig n j (reverse (multi_sig sig n) rs1@b::ls2) =
 255       trace sig n j (ls10@a1::ls20))
 256     [#j #ineqj >append_cons <reverse_cons >trace_def <map_append <reverse_map
 257      lapply (trace_shift_neq …lt_in ? (sym_not_eq … ineqj) … Hrss) [//] #Htr
 258      <(trace_def …  (b::rs1)) <Htr >reverse_map >map_append @eq_f @Hls20 ]
 259    #Htracej
 260    cut (trace sig n i (reverse (multi_sig sig n) (rs1@[b0])@ls2) =
 261         trace sig n i (ls10@a1::ls20))
 262     [>trace_def <map_append <reverse_map <map_append <(trace_def … [b0])
 263      cut (trace sig n i [b0] = [blank ?]) [@daemon] #Hcut >Hcut
 264      lapply (trace_shift … lt_in … Hrss) [//] whd in match (tail ??); #Htr <Htr
 265      >reverse_map >map_append <trace_def <Hls20 %
 266     ]
 267    #Htracei
 268    cut (∀j. j ≠ i →
 269       (trace sig n j (reverse (multi_sig sig n) rs11) = trace sig n j ls10) ∧
 270       (trace sig n j (ls1@b::ls2) = trace sig n j (a1::ls20)))
 271    [@daemon (* si fa
 272      #j #ineqj @(first_P_to_eq ? (λx. x ≠ head ?))
 273       [lapply (Htracej … ineqj) >trace_def in ⊢ (%→?); <map_append
 274        >trace_def in ⊢ (%→?); <map_append #H @H
 275       | *) ] #H2
 276   cut ((trace sig n i (b0::reverse ? rs11) = trace sig n i (ls10@[a1])) ∧
 277       (trace sig n i (ls1@ls2) = trace sig n i ls20))
 278     [>H1 in Htracei; >reverse_append >reverse_single >reverse_append
 279      >reverse_reverse >associative_append >associative_append
 280      @daemon
 281     ] #H3
 282    %{ls20} %{a1} %{(reverse ? (b0::ls10)@tail (multi_sig sig n) rs2)}
 283    %[%[%[%[@Htout
 284     |#j #lejn #jneqi <(Hls1 … lejn)
 285      >to_blank_i_def >to_blank_i_def @eq_f @sym_eq @(proj2 … (H2 j jneqi))]
 286     |#j #lejn #jneqi >reverse_cons >associative_append >Hb0
 287      <to_blank_hd_cons >to_blank_i_def >to_blank_i_def @eq_f
 288      @(injective_append_l … (trace sig n j (reverse ? ls1))) (* >trace_def >trace_def *)
 289      >map_append >map_append >Hrs1 >H1 >associative_append
 290      <map_append <map_append in ⊢ (???%); @eq_f
 291      <map_append <map_append @eq_f2 // @sym_eq
 292      <(reverse_reverse … rs11) <reverse_map <reverse_map in ⊢ (???%);
 293      @eq_f @(proj1 … (H2 j jneqi))]
 294     |<(Hls1 i) [2:@lt_to_le //] (* manca un invariante: dopo un blank
 295      posso avere solo blank *) @daemon ]
 296     |>reverse_cons >associative_append
 297      cut (to_blank_i sig n i rs = to_blank_i sig n i (rs11@[b0])) [@daemon]
 298      #Hcut >Hcut >(to_blank_i_chop  … b0 (a1::reverse …ls10)) [2: @Hb0blank]
 299      >to_blank_i_def >to_blank_i_def @eq_f
 300      >trace_def >trace_def @injective_reverse >reverse_map >reverse_cons
 301      >reverse_reverse >reverse_map >reverse_append >reverse_single @sym_eq
 302      @(proj1 … H3)
 303     ]
 304   |(*we do not find the head: this is absurd *)
 305    * #b1 * #lss * * #H2 @False_ind
 306    cut (∀x0. mem ? x0 (trace sig n n (b0::reverse ? rss@ls2)) → x0 ≠ head ?)
 307      [@daemon] -H2 #H2
 308    lapply (trace_shift_neq sig n i n … lt_in … Hrss)
 309      [@lt_to_not_eq @lt_in | // ]
 310    #H3 @(absurd
 311         (nth n ? (vec … (hd ? (ls1@[b]) (all_blank sig n))) (blank ?) = head ?))
 312      [>Hhead //
 313      |@H2 >trace_def %2 <map_append @mem_append_l1 <reverse_map <trace_def
 314       >H3 >H1 >trace_def >reverse_map >reverse_cons >reverse_append
 315       >reverse_reverse >associative_append <map_append @mem_append_l2
 316       cases ls1 [%1 % |#x #ll %1 %]
 317      ]
 318    ]
 319  ]
 320 qed.