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