matita/matita/lib/turing/multi_universal/tuples.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_____________________________________________________________*)
  11
  12
  13 (****************************** table of tuples *******************************)
  14 include "turing/multi_universal/normalTM.ma".
  15
  16 (* a well formed table is a list of tuples *)
  17
  18 definition table_TM ≝ λn,l,h.flatten ? (tuples_list n h l).
  19
  20 lemma table_TM_cons: ∀n,h,t,o.
  21   table_TM n (t::o) h = (tuple_encoding n h t)@(table_TM n o h).
  22 // qed.
  23
  24 lemma initial_bar: ∀n,h,l. l ≠ [ ] →
  25   table_TM n l h = bar :: tail ? (table_TM n l h).
  26 #n #h *
  27   [* #H @False_ind @H //
  28   |#a #tl #_ >table_TM_cons lapply (is_tuple n h a)
  29    * #qin * #cin * #qout * #cout * #mv * #_ #Htup >Htup %
  30   ]
  31 qed.
  32
  33 (************************** matching in a table *******************************)
  34 lemma list_to_table: ∀n,l,h,t. mem ? t l →
  35   ∃ll,lr.table_TM n l h = ll@(tuple_encoding n h t)@lr.
  36 #n #l #h #t elim l
  37   [@False_ind
  38   |#hd #tl #Hind *
  39     [#Htup %{[]} %{(table_TM n tl h)} >Htup %
  40     |#H cases (Hind H) #ll * #lr #H1
  41      %{((tuple_encoding n h hd)@ll)} %{lr}
  42      >associative_append <H1 %
  43     ]
  44   ]
  45 qed.
  46
  47 lemma list_to_table1: ∀n,l,h,tup. mem ? tup (tuples_list n h l) →
  48   ∃ll,lr.table_TM n l h = ll@tup@lr.
  49 #n #l #h #tup elim l
  50   [@False_ind
  51   |#hd #tl #Hind *
  52     [#Htup %{[]} %{(table_TM n tl h)} >Htup %
  53     |#H cases (Hind H) #ll * #lr #H1
  54      %{((tuple_encoding n h hd)@ll)} %{lr}
  55      >associative_append <H1 %
  56     ]
  57   ]
  58 qed.
  59
  60 definition is_config : nat → list unialpha → Prop ≝
  61  λn,t.∃qin,cin.
  62  only_bits qin ∧ cin ≠ bar ∧ |qin| = S n ∧ t = bar::qin@[cin].
  63
  64 lemma table_to_list: ∀n,l,h,c. is_config n c →
  65   ∀ll,lr.table_TM n l h = ll@c@lr →
  66     ∃out,lr0,t. lr = out@lr0 ∧ tuple_encoding n h t = (c@out) ∧ mem ? t l.
  67 #n #l #h #c * #qin * #cin * * * #H1 #H2 #H3 #H4
  68 #ll #lr lapply ll -ll elim l
  69   [>H4 #ll cases ll normalize [|#hd #tl ] #Habs destruct
  70   |#t1 #othert #Hind #ll >table_TM_cons #Htuple
  71    cut (S n < |ll@c@lr|)
  72      [<Htuple >length_append >(length_of_tuple  … (is_tuple … ))
  73       /2 by transitive_lt, le_n/] #Hsplit lapply Htuple -Htuple
  74    cases (is_tuple … n h t1) #q1 * #c1 * #q2 * #c2 * #m
  75    * * * * * * * #Hq1 #Hq2 #Hc1 #Hc2 #Hm #Hlen1 #Hlen2
  76    whd in ⊢ (???%→?); #Ht1
  77    (* if ll is empty we match the first tuple t1, otherwise
  78       we match inside othert *)
  79    cases ll
  80     [>H4 >Ht1 normalize in ⊢ (???%→?);
  81      >associative_append whd in ⊢ (??%?→?); #Heq destruct (Heq) -Heq
  82      >associative_append in e0; #e0
  83      lapply (append_l1_injective  … e0) [>H3 @Hlen1] #Heq1
  84      lapply (append_l2_injective  … e0) [>H3 @Hlen1]
  85      normalize in ⊢ (???%→?); whd in ⊢ (??%?→?); #Htemp
  86      lapply (cons_injective_l ????? Htemp) #Hc1
  87      lapply (cons_injective_r ????? Htemp) -Htemp #Heq2
  88      %{(q2@[c2;m])} %{(table_TM n othert h)} %{t1} %
  89       [ %[ // |>Ht1 >Heq1 >Hc1 @eq_f >associative_append % ]
  90       |%1 %
  91       ]
  92     |(* ll not nil *)
  93      #b #tl >Ht1 normalize in ⊢ (???%→?);
  94      whd in ⊢ (??%?→?); #Heq destruct (Heq)
  95      cases (compare_append … e0) #l *
  96       [* cases l
  97         [#_ #Htab cases (Hind [ ] (sym_eq … Htab))
  98          #out * #lr0  * #t * * #Hlr #Ht #Hmemt
  99          %{out} %{lr0} %{t} % [% //| %2 //]
 100         |(* this case is absurd *)
 101          #al #tll #Heq1 >H4 #Heq2 @False_ind
 102          lapply (cons_injective_l ? bar … Heq2) #Hbar <Hbar in Heq1; #Heq1
 103          @(absurd (mem ? bar (q1@(c1::q2@[c2; m]))))
 104           [>Heq1 @mem_append_l2 %1 //
 105           |% #Hmembar cases (mem_append ???? Hmembar) -Hmembar
 106             [#Hmembar lapply(Hq1 bar Hmembar) normalize #Habs destruct (Habs)
 107             |* [#Habs @absurd //]
 108              #Hmembar cases (mem_append ???? Hmembar) -Hmembar
 109               [#Hmembar lapply(Hq2 bar Hmembar) normalize #Habs destruct (Habs)
 110               |* [#Habs @absurd //] #Hmembar @(absurd ?? Hm) @sym_eq @mem_single //
 111               ]
 112             ]
 113           ]
 114         ]
 115       |* #Htl #Htab cases (Hind … Htab) #out * #lr0 * #t * * #Hlr #Ht #Hmemt
 116        %{out} %{lr0} %{t} % [% // | %2 //]
 117       ]
 118     ]
 119   ]
 120 qed.
 121
 122 (*
 123 lemma tuple_to_config: ∀n,h,t,out,c. is_config n c →
 124   tuple_encoding n h t = c@out →
 125     ∃outq,outa,m. out = outq@[outa;m] ∧ is_config n (bar::outq@[outa]).
 126 #n #h * * #q0 #a0 * * #q1 #a1 #m #out #c * #q * #a * * * #Hq #Ha #Hlen #Hc
 127 whd in ⊢ (??%?→?); #Heq
 128 %{(bits_of_state n h q1)} %{(low_char a1)} %{(low_mv m)} %
 129   [% [ %[ // | cases a1 [|#b] normalize % #H destruct (H)]
 130      |whd in ⊢ (??%?); @eq_f //]
 131   |@eq_f cut (∀A.∀a:A.∀l1,l2. a::l1@l2 = (a::l1)@l2) [//] #Hcut
 132    >append_cons in Heq; >Hcut <associative_append
 133    >(append_cons ? (low_char a1)) <associative_append #Heq
 134    lapply (append_l1_injective_r ?? (c@out) ??? Heq) [%] -Heq
 135    >associative_append #Heq @sym_eq @(append_l2_injective ?????? Heq)
 136    >Hc whd in ⊢ (??%%); @eq_f >length_append >length_append
 137    @eq_f2 // >length_map >Hlen whd in ⊢ (??%?); @eq_f //
 138   ]
 139 qed.
 140 *)
 141
 142 lemma tuple_to_config: ∀n,h,t,out,m,c. is_config n c →
 143   tuple_encoding n h t = c@out@[m] → is_config n (bar::out).
 144 #n #h * * #q0 #a0 * * #q1 #a1 #m #out #lowm #c * #q * #a * * * #Hq #Ha #Hlen #Hc
 145 whd in ⊢ (??%?→?); #Heq %{(bits_of_state n h q1)} %{(low_char a1)} %
 146   [% [ %[ // | cases a1 [|#b] normalize % #H destruct (H)]
 147      |whd in ⊢ (??%?); @eq_f //]
 148   |@eq_f cut (∀A.∀a:A.∀l1,l2. a::l1@l2 = (a::l1)@l2) [//] #Hcut
 149    >append_cons in Heq; >Hcut <associative_append
 150    >(append_cons ? (low_char a1)) <associative_append #Heq
 151    lapply (append_l1_injective_r ?? (c@out) ??? Heq) [%] -Heq
 152    >associative_append #Heq @sym_eq @(append_l2_injective ?????? Heq)
 153    >Hc whd in ⊢ (??%%); @eq_f >length_append >length_append
 154    @eq_f2 // >length_map >Hlen whd in ⊢ (??%?); @eq_f //
 155   ]
 156 qed.
 157
 158 (* da spostare *)
 159 lemma injective_nat_of: ∀n. injective … (nat_of n).
 160 #n * #a0 #Ha0 * #b0 #Hb0 normalize #Heq
 161 generalize in match Ha0; generalize in match Hb0; >Heq //
 162 qed.
 163
 164 lemma not_of_lt: ∀n,m. nat_of n m < n.
 165 #n * #a #lta //
 166 qed.
 167
 168 (* da spostare *)
 169 lemma injective_map: ∀A,B,f. injective A B f → injective … (map … f).
 170 #A #B #f #injf #l1 elim l1
 171   [* // #a2 #l2 normalize #H destruct
 172   |#a1 -l1 #l1 #Hind *
 173     [normalize #H destruct
 174     |#a2 #l2 normalize #Hmap
 175      >(injf … (cons_injective_l ????? Hmap))
 176      >(Hind … (cons_injective_r ????? Hmap)) %
 177     ]
 178   ]
 179 qed.
 180
 181 lemma deterministic: ∀M:normalTM.∀l,t1,t2,c,out1,out2.
 182   l = graph_enum ?? (ntrans M) →
 183   mem ? t1 l → mem ? t2 l →
 184   is_config (no_states M) c →
 185   tuple_encoding ? (nhalt M) t1 = (c@out1) →
 186   tuple_encoding ? (nhalt M) t2 = (c@out2) →
 187   out1 = out2.
 188 #M #l * * #q1 #a1 * * #q11 #a11 #m1
 189 * * #q2 #a2 * * #q21 #a21 #m2 #c #out1 #out2 #Hl #memt1 #memt2 *
 190 #state * #char * * * #_ #_ #Hlen #Heqc #tuplet1 #tuplet2
 191 lapply (mem_to_memb … memt1) >Hl #membt1
 192 lapply (graph_enum_correct ?? (ntrans M) ?? membt1) #Ht1
 193 lapply (mem_to_memb … memt2) >Hl #membt2
 194 lapply (graph_enum_correct ?? (ntrans M) ?? membt2) #Ht2
 195 cut (bar::bits_of_state (no_states M) (nhalt M) q1@[low_char a1]=c)
 196   [whd in tuplet1:(??%?); >(append_cons ? (low_char a1)) in tuplet1; #tuplet1
 197    @(append_l1_injective ? (bar::bits_of_state ?? q1@[low_char a1]) ???? tuplet1)
 198    >Heqc whd in ⊢ (??%%); @eq_f >length_append >length_append
 199    @eq_f2 // >length_map whd in ⊢ (??%?); >Hlen @eq_f
 200    >bitlist_length %] #Hcfg1
 201 cut (bar::bits_of_state (no_states M) (nhalt M) q2@[low_char a2]=c)
 202   [whd in tuplet2:(??%?); >(append_cons ? (low_char a2)) in tuplet2; #tuplet2
 203    @(append_l1_injective ? (bar::bits_of_state ?? q2@[low_char a2]) ???? tuplet2)
 204    >Heqc whd in ⊢ (??%%); @eq_f >length_append >length_append
 205    @eq_f2 // >length_map whd in ⊢ (??%?); >Hlen @eq_f
 206    >bitlist_length %] #Hcfg2
 207 cut (a1 = a2)
 208   [@injective_low_char
 209    <Hcfg2 in Hcfg1; #H lapply (cons_injective_r ????? H) -H #H
 210    lapply (append_l2_injective_r … H) [%] -H #H @(cons_injective_l ????? H)]
 211 #Heqa
 212 cut (to_bitlist (no_states M) (nat_of … q1) =
 213      to_bitlist (no_states M)  (nat_of … q2))
 214   [<Hcfg2 in Hcfg1; #H lapply (cons_injective_r ????? H) -H #H
 215    lapply (append_l1_injective_r … H) // -H whd in ⊢ (??%%→?); #H
 216    lapply (cons_injective_r ????? H) -H #H
 217    @(injective_map ?? (λx.bit x) ??? H)
 218    (* injective  bit *) * * #H1 destruct (H1) %]
 219 #Hbits
 220 cut (q1 = q2)
 221   [@injective_nat_of
 222    <(bitlist_inv1 (no_states M) (nat_of … q1)) //
 223    <(bitlist_inv1 (no_states M) (nat_of … q2)) //]
 224 #Heqq
 225 cut (〈q11,a11,m1〉=〈q21,a21,m2〉)
 226   [<Ht1 <Ht2 @eq_f @eq_f2 //]
 227 #Heqout <Heqout in tuplet2; <Heqq <Heqa >tuplet1
 228 @append_l2_injective %
 229 qed.