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 tail_trace:  ∀sig,n,i,l.
  62   tail ? (trace sig n i l) = trace sig n i (tail ? l).
  63 #sig #n #i #l elim l //
  64 qed.
  65
  66 lemma trace_append :  ∀sig,n,i,l1,l2.
  67   trace sig n i (l1 @ l2) = trace sig n i l1 @ trace sig n i l2.
  68 #sig #n #i #l1 #l2 elim l1 // #a #tl #Hind normalize >Hind //
  69 qed.
  70
  71 lemma trace_reverse : ∀sig,n,i,l.
  72   trace sig n i (reverse ? l) = reverse (sig_ext sig) (trace sig n i l).
  73 #sig #n #i #l elim l //
  74 #a #tl #Hind whd in match (trace ??? (a::tl)); >reverse_cons >reverse_cons
  75 >trace_append >Hind //
  76 qed.
  77
  78 lemma length_trace: ∀sig,n,i,l.
  79   |trace sig n i l| = |l|.
  80 #sig #n #i #l elim l // #a #tl #Hind normalize @eq_f @Hind
  81 qed.
  82
  83 lemma nth_trace : ∀sig,n,i,j,l.
  84   nth j ? (trace sig n i l) (blank ?) =
  85     nth i ? (nth j ? l (all_blank sig n)) (blank ?).
  86 #sig #n #i #j elim j
  87   [#l cases l normalize // >blank_all_blank //
  88   |-j #j #Hind #l whd in match (nth ????); whd in match (nth ????);
  89    cases l
  90     [normalize >nth_nil >nth_nil >blank_all_blank //
  91     |#a #tl normalize @Hind]
  92   ]
  93 qed.
  94
  95 definition no_head_in ≝ λsig,n,l.
  96   ∀x. mem ? x (trace sig n n l) → x ≠ head ?.
  97
  98 (* some lemmas over lists, to be moved *)
  99 lemma injective_append_l: ∀A,l. injective ?? (append A l).
 100 #A #l elim l
 101   [#l1 #l2 normalize //
 102   |#a #tl #Hind #l1 #l2 normalize #H @Hind @(cons_injective_r … H)
 103   ]
 104 qed.
 105
 106 lemma injective_append_r: ∀A,l. injective ?? (λl1.append A l1 l).
 107 #A #l #l1 #l2 #H
 108 cut (reverse ? (l1@l) = reverse ? (l2@l)) [//]
 109 >reverse_append >reverse_append #Hrev
 110 lapply (injective_append_l … Hrev) -Hrev #Hrev
 111 <(reverse_reverse … l1) <(reverse_reverse … l2) //
 112 qed.
 113
 114 lemma reverse_map: ∀A,B,f,l.
 115   reverse B (map … f l) = map … f (reverse A l).
 116 #A #B #f #l elim l //
 117 #a #l #Hind >reverse_cons >reverse_cons <map_append >Hind //
 118 qed.
 119
 120 lemma injective_reverse: ∀A. injective ?? (reverse A).
 121 #A #l1 #l2 #H <(reverse_reverse … l1) <(reverse_reverse … l2) //
 122 qed.
 123
 124 lemma first_P_to_eq : ∀A:Type[0].∀P:A→Prop.∀l1,l2,l3,l4,a1,a2.
 125   l1@a1::l2 = l3@a2::l4 → (∀x. mem A x l1 → P x) → (∀x. mem A x l2 → P x) →
 126   ¬ P a1 → ¬ P a2 → l1 = l3 ∧ a1::l2 = a2::l4.
 127 #A #P #l1 elim l1
 128   [#l2 *
 129     [#l4 #a1 #a2 normalize #H destruct /2/
 130     |#c #tl #l4 #a1 #a2 normalize #H destruct
 131      #_ #H #_ #H1 @False_ind @(absurd ?? H1) @H @mem_append_l2 %1 //
 132     ]
 133   |#b #tl1 #Hind #l2 *
 134     [#l4 #a1 #a2 normalize #H destruct
 135      #H1 #_ #_ #H2 @False_ind @(absurd ?? H2) @H1 %1 //
 136     |#c #tl2 #l4 #a1 #a2 normalize #H1 #H2 #H3 #H4 #H5
 137      lapply (Hind l2 tl2 l4 … H4 H5)
 138       [destruct @H3 |#x #H6 @H2 %2 // | destruct (H1) //
 139       |* #H6 #H7 % // >H7 in H1; #H1 @(injective_append_r … (a2::l4)) @H1
 140     ]
 141   ]
 142 qed.
 143
 144 lemma nth_to_eq: ∀A,l1,l2,a. |l1| = |l2| →
 145   (∀i. nth i A l1 a = nth i A l2 a) → l1 = l2.
 146 #A #l1 elim l1
 147   [* // #a #tl #d normalize #H destruct (H)
 148   |#a #tl #Hind *
 149     [#d normalize #H destruct (H)
 150     |#b #tl1 #d #Hlen #Hnth @eq_f2
 151       [@(Hnth 0) | @(Hind tl1 d) [@injective_S @Hlen | #i @(Hnth (S i)) ]]
 152     ]
 153   ]
 154 qed.
 155
 156 lemma nth_extended: ∀A,i,l,a.
 157   nth i A l a = nth i A (l@[a]) a.
 158 #A #i elim i [* // |#j #Hind * // #b #tl #a normalize @Hind]
 159 qed.
 160
 161 (******************************* shifting a trace *****************************)
 162
 163 (* (shift_i sig n i a b) replace the i-th trace of the character a with the
 164 i-th trace of b *)
 165
 166 definition shift_i ≝ λsig,n,i.λa,b:Vector (sig_ext sig) n.
 167   change_vec (sig_ext sig) n a (nth i ? b (blank ?)) i.
 168
 169 (* given two strings v1 and v2 of the mono-tape machine, (shift_l … i v1 v2)
 170 asserts that v1 is obtained from v2 by shifting_left the i-trace *)
 171
 172 definition shift_l ≝ λsig,n,i,v1,v2.  (* multi_sig sig n *)
 173   |v1| = |v2| ∧
 174   ∀j.nth j ? v2 (all_blank sig n) =
 175       change_vec ? n (nth j ? v1 (all_blank sig n))
 176         (nth i ? (vec … (nth (S j) ? v1 (all_blank sig n))) (blank ?)) i.
 177
 178 (* supposing (shift_l … i v1 v2), the i-th trace of v2 is equal to the tail of
 179 the i-th trace of v1, plus a trailing blank *)
 180
 181 lemma trace_shift: ∀sig,n,i,v1,v2. i < n → 0 < |v1| →
 182   shift_l sig n i v1 v2 → trace ? n i v2 = tail ? (trace ? n i v1)@[blank sig].
 183 #sig #n #i #v1 #v2 #lein #Hlen * #Hlen1 #Hnth @(nth_to_eq … (blank ?))
 184   [>length_trace <Hlen1 generalize in match Hlen; cases v1
 185     [normalize #H @(le_n_O_elim … H) //
 186     |#b #tl #_ normalize >length_append >length_trace normalize //
 187     ]
 188   |#j >nth_trace >Hnth >nth_change_vec // >tail_trace
 189    cut (trace ? n i [all_blank sig n] = [blank sig])
 190      [normalize >blank_all_blank //]
 191    #Hcut <Hcut <trace_append >nth_trace
 192    <nth_extended //
 193   ]
 194 qed.
 195
 196 (* supposing (shift_l … i v1 v2), and j≠i, the j-th trace of v2 is equal to the
 197 j-th trace of v1 *)
 198
 199 lemma trace_shift_neq: ∀sig,n,i,j,v1,v2. i < n → 0 < |v1| → i ≠ j →
 200   shift_l sig n i v1 v2 → trace ? n j v2 = trace ? n j v1.
 201 #sig #n #i #j #v1 #v2 #lein #Hlen #Hneq * #Hlen1 #Hnth @(nth_to_eq … (blank ?))
 202   [>length_trace >length_trace @sym_eq @Hlen1
 203   |#k >nth_trace >Hnth >nth_change_vec_neq // >nth_trace //
 204   ]
 205 qed.
 206
 207 (******************************************************************************)
 208
 209 let rec to_blank sig l on l ≝
 210   match l with
 211   [ nil ⇒  [ ]
 212   | cons a tl ⇒
 213       if a == blank sig then [ ] else a::(to_blank sig tl)].
 214
 215 definition to_blank_i ≝ λsig,n,i,l. to_blank ? (trace sig n i l).
 216
 217 lemma to_blank_i_def : ∀sig,n,i,l.
 218   to_blank_i sig n i l = to_blank ? (trace sig n i l).
 219 // qed.
 220
 221 lemma to_blank_cons_b : ∀sig,n,i,a,l.
 222   nth i ? (vec … n a) (blank sig) = blank ? →
 223   to_blank_i sig n i (a::l) = [ ].
 224 #sig #n #i #a #l #H whd in match (to_blank_i ????);
 225 >(\b H) //
 226 qed.
 227
 228 lemma to_blank_cons_nb: ∀sig,n,i,a,l.
 229   nth i ? (vec … n a) (blank sig) ≠ blank ? →
 230   to_blank_i sig n i (a::l) =
 231     nth i ? (vec … n a) (blank sig)::(to_blank_i sig n i l).
 232 #sig #n #i #a #l #H whd in match (to_blank_i ????);
 233 >(\bf H) //
 234 qed.
 235
 236 axiom to_blank_hd : ∀sig,n,a,b,l1,l2.
 237   (∀i. i ≤ n → to_blank_i sig n i (a::l1) = to_blank_i sig n i (b::l2)) → a = b.
 238
 239 lemma to_blank_i_ext : ∀sig,n,i,l.
 240   to_blank_i sig n i l = to_blank_i sig n i (l@[all_blank …]).
 241 #sig #n #i #l elim l
 242   [@sym_eq @to_blank_cons_b @blank_all_blank
 243   |#a #tl #Hind whd in match (to_blank_i ????); >Hind <to_blank_i_def >Hind %
 244   ]
 245 qed.
 246
 247 lemma to_blank_hd_cons : ∀sig,n,i,l1,l2.
 248   to_blank_i sig n i (l1@l2) =
 249     to_blank_i … i (l1@(hd … l2 (all_blank …))::tail … l2).
 250 #sig #n #i #l1 #l2 cases l2
 251   [whd in match (hd ???); whd in match (tail ??); >append_nil @to_blank_i_ext
 252   |#a #tl %
 253   ]
 254 qed.
 255
 256 lemma to_blank_i_chop : ∀sig,n,i,a,l1,l2.
 257  (nth i ? (vec … a) (blank ?))= blank ? →
 258  to_blank_i sig n i (l1@a::l2) = to_blank_i sig n i l1.
 259 #sig #n #i #a #l1 elim l1
 260   [#l2 #H @to_blank_cons_b //
 261   |#x #tl #Hind #l2 #H whd in match (to_blank_i ????);
 262    >(Hind l2 H) <to_blank_i_def >(Hind l2 H) %
 263   ]
 264 qed.
 265
 266
 267
 268
 269