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 (************************** matching in a table *******************************)
  25 lemma list_to_table: ∀n,l,h,tup. mem ? tup (tuples_list n h l) →
  26   ∃ll,lr.table_TM n l h = ll@tup@lr.
  27 #n #l #h #tup elim l
  28   [@False_ind
  29   |#hd #tl #Hind *
  30     [#Htup %{[]} %{(table_TM n tl h)} >Htup %
  31     |#H cases (Hind H) #ll * #lr #H1
  32      %{((tuple_encoding n h hd)@ll)} %{lr}
  33      >associative_append <H1 %
  34     ]
  35   ]
  36 qed.
  37
  38 definition is_config : nat → list unialpha → Prop ≝
  39  λn,t.∃qin,cin.
  40  only_bits qin ∧ cin ≠ bar ∧ |qin| = S n ∧ t = bar::qin@[cin].
  41
  42 lemma compare_append : ∀A,l1,l2,l3,l4. l1@l2 = l3@l4 →
  43 ∃l:list A.(l1 = l3@l ∧ l4=l@l2) ∨ (l3 = l1@l ∧ l2=l@l4).
  44 #A #l1 elim l1
  45   [#l2 #l3 #l4 #Heq %{l3} %2 % // @Heq
  46   |#a1 #tl1 #Hind #l2 #l3 cases l3
  47     [#l4 #Heq %{(a1::tl1)} %1 % // @sym_eq @Heq
  48     |#a3 #tl3 #l4 normalize in ⊢ (%→?); #Heq cases (Hind l2 tl3 l4 ?)
  49       [#l * * #Heq1 #Heq2 %{l}
  50         [%1 % // >Heq1 >(cons_injective_l ????? Heq) //
  51         |%2 % // >Heq1 >(cons_injective_l ????? Heq) //
  52         ]
  53       |@(cons_injective_r ????? Heq)
  54       ]
  55     ]
  56   ]
  57 qed.
  58
  59 lemma table_to_list: ∀n,l,h,c. is_config n c →
  60   (∃ll,lr.table_TM n l h = ll@c@lr) →
  61     ∃out,t. tuple_encoding n h t = (c@out) ∧ mem ? t l.
  62 #n #l #h #c * #qin * #cin * * * #H1 #H2 #H3 #H4
  63  * #ll * #lr lapply ll -ll elim l
  64   [>H4 #ll cases ll normalize [|#hd #tl ] #Habs destruct
  65   |#t1 #othert #Hind #ll >table_TM_cons #Htuple
  66    cut (S n < |ll@c@lr|)
  67      [<Htuple >length_append >(length_of_tuple  … (is_tuple … ))
  68       /2 by transitive_lt, le_n/] #Hsplit lapply Htuple -Htuple
  69    cases (is_tuple … n h t1) #q1 * #c1 * #q2 * #c2 * #m
  70    * * * * * * * #Hq1 #Hq2 #Hc1 #Hc2 #Hm #Hlen1 #Hlen2
  71    whd in ⊢ (???%→?); #Ht1
  72    (* if ll is empty we match the first tuple t1, otherwise
  73       we match inside othert *)
  74    cases ll
  75     [>H4 >Ht1 normalize in ⊢ (???%→?);
  76      >associative_append whd in ⊢ (??%?→?); #Heq destruct (Heq) -Heq
  77      >associative_append in e0; #e0
  78      lapply (append_l1_injective  … e0) [>H3 @Hlen1] #Heq1
  79      lapply (append_l2_injective  … e0) [>H3 @Hlen1]
  80      normalize in ⊢ (???%→?); whd in ⊢ (??%?→?); #Htemp
  81      lapply (cons_injective_l ????? Htemp) #Hc1
  82      lapply (cons_injective_r ????? Htemp) -Htemp #Heq2
  83      %{(q2@[c2;m])} %{t1} %
  84       [>Ht1 >Heq1 >Hc1 @eq_f >associative_append %
  85       |%1 %
  86       ]
  87     |(* ll not nil *)
  88      #b #tl >Ht1 normalize in ⊢ (???%→?);
  89      whd in ⊢ (??%?→?); #Heq destruct (Heq)
  90      cases (compare_append … e0) #l *
  91       [* cases l
  92         [#_ #Htab cases (Hind [ ] (sym_eq … Htab)) #out * #t * #Ht #Hmemt
  93          %{out} %{t} % // %2 //
  94         |(* this case is absurd *)
  95          #al #tll #Heq1 >H4 #Heq2 @False_ind
  96          lapply (cons_injective_l ? bar … Heq2) #Hbar <Hbar in Heq1; #Heq1
  97          @(absurd (mem ? bar (q1@(c1::q2@[c2; m]))))
  98           [>Heq1 @mem_append_l2 %1 //
  99           |% #Hmembar cases (mem_append ???? Hmembar) -Hmembar
 100             [#Hmembar lapply(Hq1 bar Hmembar) normalize #Habs destruct (Habs)
 101             |* [#Habs @absurd //]
 102              #Hmembar cases (mem_append ???? Hmembar) -Hmembar
 103               [#Hmembar lapply(Hq2 bar Hmembar) normalize #Habs destruct (Habs)
 104               |* [#Habs @absurd //] #Hmembar @(absurd ?? Hm) @sym_eq @mem_single //
 105               ]
 106             ]
 107           ]
 108         ]
 109       |* #Htl #Htab cases (Hind … Htab) #out * #t * #Ht #Hmemt
 110        %{out} %{t} % // %2 //
 111       ]
 112     ]
 113   ]
 114 qed.
 115