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

   1 (* This file contains the definition of the alphabet for the mono-tape machine
   2 simulating a multi-tape machine, and a library of functions operating on them *)
   3
   4 include "basics/vector_finset.ma".
   5
   6 (* a multi_sig characheter is composed by n+1 sub-characters: n for each tape
   7 of a multitape machine, and an additional one to mark the position of the head.
   8 We extend the tape alphabet with two new symbols true and false.
   9 false is used to pad shorter tapes, and true to mark the head of the tape *)
  10
  11 definition sig_ext ≝ λsig. FinSum FinBool sig.
  12 definition blank : ∀sig.sig_ext sig ≝ λsig. inl … false.
  13 definition head : ∀sig.sig_ext sig ≝ λsig. inl … true.
  14
  15 definition multi_sig ≝ λsig:FinSet.λn.FinVector (sig_ext sig) n.
  16
  17 (* a character containing blank characters in each trace *)
  18 let rec all_blank sig n on n : multi_sig sig n ≝
  19   match n with
  20   [ O ⇒ Vector_of_list ? []
  21   | S m ⇒ vec_cons ? (blank ?) m (all_blank sig m)
  22   ].
  23
  24 lemma blank_all_blank: ∀sig,n,i.
  25   nth i ? (vec … (all_blank sig n)) (blank sig) = blank ?.
  26 #sig #n elim n normalize [#i >nth_nil // |#m #Hind #i cases i // #j @Hind ]
  27 qed.
  28
  29 lemma all_blank_n: ∀sig,n.
  30   nth n ? (vec … (all_blank sig n)) (blank sig) = blank ?.
  31 #sig #n @blank_all_blank
  32 qed.
  33
  34 (* boolen test functions *)
  35
  36 definition no_blank ≝ λsig,n,i.λc:multi_sig sig n.
  37   ¬(nth i ? (vec … c) (blank ?))==blank ?.
  38
  39 definition no_head ≝ λsig,n.λc:multi_sig sig n.
  40   ¬((nth n ? (vec … c) (blank ?))==head ?).
  41
  42 lemma no_head_true: ∀sig,n,a.
  43   nth n ? (vec … n a) (blank sig) ≠ head ? → no_head … a = true.
  44 #sig #n #a normalize cases (nth n ? (vec … n a) (blank sig))
  45 normalize // * normalize // * #H @False_ind @H //
  46 qed.
  47
  48 lemma no_head_false: ∀sig,n,a.
  49   nth n ? (vec … n a) (blank sig) = head ? → no_head … a = false.
  50 #sig #n #a #H normalize >H //
  51 qed.
  52
  53 (**************************** extract the i-th trace **************************)
  54 definition trace ≝ λsig,n,i,l.
  55   map ?? (λa. nth i ? (vec … n a) (blank sig)) l.
  56
  57 lemma trace_def : ∀sig,n,i,l.
  58   trace sig n i l = map ?? (λa. nth i ? (vec … n a) (blank sig)) l.
  59 // qed.
  60
  61 lemma hd_trace:  ∀sig,n,i,l.
  62   hd ? (trace sig n i l) (blank ?) =
  63     nth i ? (hd ? l (all_blank … )) (blank ?).
  64 #sig #n #i #l elim l // normalize >blank_all_blank %
  65 qed.
  66
  67 lemma tail_trace:  ∀sig,n,i,l.
  68   tail ? (trace sig n i l) = trace sig n i (tail ? l).
  69 #sig #n #i #l elim l //
  70 qed.
  71
  72 lemma trace_append :  ∀sig,n,i,l1,l2.
  73   trace sig n i (l1 @ l2) = trace sig n i l1 @ trace sig n i l2.
  74 #sig #n #i #l1 #l2 elim l1 // #a #tl #Hind normalize >Hind //
  75 qed.
  76
  77 lemma trace_reverse : ∀sig,n,i,l.
  78   trace sig n i (reverse ? l) = reverse (sig_ext sig) (trace sig n i l).
  79 #sig #n #i #l elim l //
  80 #a #tl #Hind whd in match (trace ??? (a::tl)); >reverse_cons >reverse_cons
  81 >trace_append >Hind //
  82 qed.
  83
  84 lemma length_trace: ∀sig,n,i,l.
  85   |trace sig n i l| = |l|.
  86 #sig #n #i #l elim l // #a #tl #Hind normalize @eq_f @Hind
  87 qed.
  88
  89 lemma nth_trace : ∀sig,n,i,j,l.
  90   nth j ? (trace sig n i l) (blank ?) =
  91     nth i ? (nth j ? l (all_blank sig n)) (blank ?).
  92 #sig #n #i #j elim j
  93   [#l cases l normalize // >blank_all_blank //
  94   |-j #j #Hind #l whd in match (nth ????); whd in match (nth ????);
  95    cases l
  96     [normalize >nth_nil >nth_nil >blank_all_blank //
  97     |#a #tl normalize @Hind]
  98   ]
  99 qed.
 100
 101 definition no_head_in ≝ λsig,n,l.
 102   ∀x. mem ? x (trace sig n n l) → x ≠ head ?.
 103
 104
 105 (* some lemmas over lists, to be moved *)
 106 lemma injective_append_l: ∀A,l. injective ?? (append A l).
 107 #A #l elim l
 108   [#l1 #l2 normalize //
 109   |#a #tl #Hind #l1 #l2 normalize #H @Hind @(cons_injective_r … H)
 110   ]
 111 qed.
 112
 113 lemma injective_append_r: ∀A,l. injective ?? (λl1.append A l1 l).
 114 #A #l #l1 #l2 #H
 115 cut (reverse ? (l1@l) = reverse ? (l2@l)) [//]
 116 >reverse_append >reverse_append #Hrev
 117 lapply (injective_append_l … Hrev) -Hrev #Hrev
 118 <(reverse_reverse … l1) <(reverse_reverse … l2) //
 119 qed.
 120
 121 lemma reverse_map: ∀A,B,f,l.
 122   reverse B (map … f l) = map … f (reverse A l).
 123 #A #B #f #l elim l //
 124 #a #l #Hind >reverse_cons >reverse_cons <map_append >Hind //
 125 qed.
 126
 127 lemma injective_reverse: ∀A. injective ?? (reverse A).
 128 #A #l1 #l2 #H <(reverse_reverse … l1) <(reverse_reverse … l2) //
 129 qed.
 130
 131 lemma first_P_to_eq : ∀A:Type[0].∀P:A→Prop.∀l1,l2,l3,l4,a1,a2.
 132   l1@a1::l2 = l3@a2::l4 → (∀x. mem A x l1 → P x) → (∀x. mem A x l2 → P x) →
 133   ¬ P a1 → ¬ P a2 → l1 = l3 ∧ a1::l2 = a2::l4.
 134 #A #P #l1 elim l1
 135   [#l2 *
 136     [#l4 #a1 #a2 normalize #H destruct /2/
 137     |#c #tl #l4 #a1 #a2 normalize #H destruct
 138      #_ #H #_ #H1 @False_ind @(absurd ?? H1) @H @mem_append_l2 %1 //
 139     ]
 140   |#b #tl1 #Hind #l2 *
 141     [#l4 #a1 #a2 normalize #H destruct
 142      #H1 #_ #_ #H2 @False_ind @(absurd ?? H2) @H1 %1 //
 143     |#c #tl2 #l4 #a1 #a2 normalize #H1 #H2 #H3 #H4 #H5
 144      lapply (Hind l2 tl2 l4 … H4 H5)
 145       [destruct @H3 |#x #H6 @H2 %2 // | destruct (H1) //
 146       |* #H6 #H7 % // >H7 in H1; #H1 @(injective_append_r … (a2::l4)) @H1
 147     ]
 148   ]
 149 qed.
 150
 151 lemma nth_to_eq: ∀A,l1,l2,a. |l1| = |l2| →
 152   (∀i. nth i A l1 a = nth i A l2 a) → l1 = l2.
 153 #A #l1 elim l1
 154   [* // #a #tl #d normalize #H destruct (H)
 155   |#a #tl #Hind *
 156     [#d normalize #H destruct (H)
 157     |#b #tl1 #d #Hlen #Hnth @eq_f2
 158       [@(Hnth 0) | @(Hind tl1 d) [@injective_S @Hlen | #i @(Hnth (S i)) ]]
 159     ]
 160   ]
 161 qed.
 162
 163 lemma nth_extended: ∀A,i,l,a.
 164   nth i A l a = nth i A (l@[a]) a.
 165 #A #i elim i [* // |#j #Hind * // #b #tl #a normalize @Hind]
 166 qed.
 167
 168 (******************************* shifting a trace *****************************)
 169
 170 (* (shift_i sig n i a b) replace the i-th trace of the character a with the
 171 i-th trace of b *)
 172
 173 definition shift_i ≝ λsig,n,i.λa,b:Vector (sig_ext sig) n.
 174   change_vec (sig_ext sig) n a (nth i ? b (blank ?)) i.
 175
 176 (* given two strings v1 and v2 of the mono-tape machine, (shift_l … i v1 v2)
 177 asserts that v1 is obtained from v2 by shifting_left the i-trace *)
 178
 179 definition shift_l ≝ λsig,n,i,v1,v2.  (* multi_sig sig n *)
 180   |v1| = |v2| ∧
 181   ∀j.nth j ? v2 (all_blank sig n) =
 182       change_vec ? n (nth j ? v1 (all_blank sig n))
 183         (nth i ? (vec … (nth (S j) ? v1 (all_blank sig n))) (blank ?)) i.
 184
 185 (* supposing (shift_l … i v1 v2), the i-th trace of v2 is equal to the tail of
 186 the i-th trace of v1, plus a trailing blank *)
 187
 188 lemma trace_shift: ∀sig,n,i,v1,v2. i < n → 0 < |v1| →
 189   shift_l sig n i v1 v2 → trace ? n i v2 = tail ? (trace ? n i v1)@[blank sig].
 190 #sig #n #i #v1 #v2 #lein #Hlen * #Hlen1 #Hnth @(nth_to_eq … (blank ?))
 191   [>length_trace <Hlen1 generalize in match Hlen; cases v1
 192     [normalize #H @(le_n_O_elim … H) //
 193     |#b #tl #_ normalize >length_append >length_trace normalize //
 194     ]
 195   |#j >nth_trace >Hnth >nth_change_vec // >tail_trace
 196    cut (trace ? n i [all_blank sig n] = [blank sig])
 197      [normalize >blank_all_blank //]
 198    #Hcut <Hcut <trace_append >nth_trace
 199    <nth_extended //
 200   ]
 201 qed.
 202
 203 (* supposing (shift_l … i v1 v2), and j≠i, the j-th trace of v2 is equal to the
 204 j-th trace of v1 *)
 205
 206 lemma trace_shift_neq: ∀sig,n,i,j,v1,v2. i < n → 0 < |v1| → i ≠ j →
 207   shift_l sig n i v1 v2 → trace ? n j v2 = trace ? n j v1.
 208 #sig #n #i #j #v1 #v2 #lein #Hlen #Hneq * #Hlen1 #Hnth @(nth_to_eq … (blank ?))
 209   [>length_trace >length_trace @sym_eq @Hlen1
 210   |#k >nth_trace >Hnth >nth_change_vec_neq // >nth_trace //
 211   ]
 212 qed.
 213
 214 (******************************************************************************)
 215
 216 let rec to_blank sig l on l ≝
 217   match l with
 218   [ nil ⇒  [ ]
 219   | cons a tl ⇒
 220       if a == blank sig then [ ] else a::(to_blank sig tl)].
 221
 222 let rec after_blank sig l on l ≝
 223   match l with
 224   [ nil ⇒  [ ]
 225   | cons a tl ⇒
 226       if a == blank sig then (a::tl) else (after_blank sig tl)].
 227
 228 definition to_blank_i ≝ λsig,n,i,l. to_blank ? (trace sig n i l).
 229
 230 lemma to_blank_i_def : ∀sig,n,i,l.
 231   to_blank_i sig n i l = to_blank ? (trace sig n i l).
 232 // qed.
 233
 234 lemma to_blank_cons_b : ∀sig,n,i,a,l.
 235   nth i ? (vec … n a) (blank sig) = blank ? →
 236   to_blank_i sig n i (a::l) = [ ].
 237 #sig #n #i #a #l #H whd in match (to_blank_i ????);
 238 >(\b H) //
 239 qed.
 240
 241 lemma to_blank_cons_nb: ∀sig,n,i,a,l.
 242   nth i ? (vec … n a) (blank sig) ≠ blank ? →
 243   to_blank_i sig n i (a::l) =
 244     nth i ? (vec … n a) (blank sig)::(to_blank_i sig n i l).
 245 #sig #n #i #a #l #H whd in match (to_blank_i ????);
 246 >(\bf H) //
 247 qed.
 248
 249 axiom to_blank_hd : ∀sig,n,a,b,l1,l2.
 250   (∀i. i ≤ n → to_blank_i sig n i (a::l1) = to_blank_i sig n i (b::l2)) → a = b.
 251
 252 lemma to_blank_i_ext : ∀sig,n,i,l.
 253   to_blank_i sig n i l = to_blank_i sig n i (l@[all_blank …]).
 254 #sig #n #i #l elim l
 255   [@sym_eq @to_blank_cons_b @blank_all_blank
 256   |#a #tl #Hind whd in match (to_blank_i ????); >Hind <to_blank_i_def >Hind %
 257   ]
 258 qed.
 259
 260 lemma to_blank_hd_cons : ∀sig,n,i,l1,l2.
 261   to_blank_i sig n i (l1@l2) =
 262     to_blank_i … i (l1@(hd … l2 (all_blank …))::tail … l2).
 263 #sig #n #i #l1 #l2 cases l2
 264   [whd in match (hd ???); whd in match (tail ??); >append_nil @to_blank_i_ext
 265   |#a #tl %
 266   ]
 267 qed.
 268
 269 lemma to_blank_i_chop : ∀sig,n,i,a,l1,l2.
 270  (nth i ? (vec … a) (blank ?))= blank ? →
 271  to_blank_i sig n i (l1@a::l2) = to_blank_i sig n i l1.
 272 #sig #n #i #a #l1 elim l1
 273   [#l2 #H @to_blank_cons_b //
 274   |#x #tl #Hind #l2 #H whd in match (to_blank_i ????);
 275    >(Hind l2 H) <to_blank_i_def >(Hind l2 H) %
 276   ]
 277 qed.
 278
 279
 280
 281
 282