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.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_____________________________________________________________*)
13 (****************************** table of tuples *******************************)
14 include "turing/multi_universal/normalTM.ma".
16 (* a well formed table is a list of tuples *)
18 definition table_TM ≝ λn,l,h.flatten ? (tuples_list n h l).
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).
24 lemma initial_bar: ∀n,h,l. l ≠ [ ] →
25 table_TM n l h = bar :: tail ? (table_TM n l 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 %
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.
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 %
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.
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 %
60 definition is_config : nat → list unialpha → Prop ≝
62 only_bits qin ∧ cin ≠ bar ∧ |qin| = S n ∧ t = bar::qin@[cin].
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,t. 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
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 *)
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])} %{t1} %
89 [>Ht1 >Heq1 >Hc1 @eq_f >associative_append %
93 #b #tl >Ht1 normalize in ⊢ (???%→?);
94 whd in ⊢ (??%?→?); #Heq destruct (Heq)
95 cases (compare_append … e0) #l *
97 [#_ #Htab cases (Hind [ ] (sym_eq … Htab)) #out * #t * #Ht #Hmemt
98 %{out} %{t} % // %2 //
99 |(* this case is absurd *)
100 #al #tll #Heq1 >H4 #Heq2 @False_ind
101 lapply (cons_injective_l ? bar … Heq2) #Hbar <Hbar in Heq1; #Heq1
102 @(absurd (mem ? bar (q1@(c1::q2@[c2; m]))))
103 [>Heq1 @mem_append_l2 %1 //
104 |% #Hmembar cases (mem_append ???? Hmembar) -Hmembar
105 [#Hmembar lapply(Hq1 bar Hmembar) normalize #Habs destruct (Habs)
106 |* [#Habs @absurd //]
107 #Hmembar cases (mem_append ???? Hmembar) -Hmembar
108 [#Hmembar lapply(Hq2 bar Hmembar) normalize #Habs destruct (Habs)
109 |* [#Habs @absurd //] #Hmembar @(absurd ?? Hm) @sym_eq @mem_single //
114 |* #Htl #Htab cases (Hind … Htab) #out * #t * #Ht #Hmemt
115 %{out} %{t} % // %2 //