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/universal/normalTM.ma".
16 (* a well formed table is a list of tuples *)
18 inductive table_TM (n:nat) : list STape → Prop ≝
19 | ttm_nil : table_TM n []
20 | ttm_cons : ∀t1,T.tuple_TM n t1 → table_TM n T → table_TM n (t1@T).
22 lemma wftable: ∀n,h,l.table_TM (S n) (flatten ? (tuples_list n h l)).
23 #n #h #l elim l // -l #a #tl #Hind
24 whd in match (flatten … (tuples_list …));
28 (*********************** general properties of tables *************************)
29 lemma no_grids_in_table: ∀n.∀l.table_TM n l → no_grids l.
31 [normalize #c #H destruct
32 |#t1 #t2 #Ht1 #Ht2 #IH lapply (no_grids_in_tuple … Ht1) -Ht1 #Ht1 #x #Hx
33 cases (memb_append … Hx) -Hx #Hx
38 lemma no_marks_in_table: ∀n.∀l.table_TM n l → no_marks l.
40 [normalize #c #H destruct
41 |#t1 #t2 #Ht1 #Ht2 #IH lapply (no_marks_in_tuple … Ht1) -Ht1 #Ht1 #x #Hx
42 cases (memb_append … Hx) -Hx #Hx
47 axiom last_of_table: ∀n,l,b.¬ table_TM n (l@[〈bar,b〉]).
49 (************************** matching in a table *******************************)
50 inductive match_in_table (n:nat) (qin:list STape) (cin: STape)
51 (qout:list STape) (cout:STape) (mv:STape)
55 tuple_TM n (mk_tuple qin cin qout cout mv) →
56 match_in_table n qin cin qout cout mv
57 (mk_tuple qin cin qout cout mv @tb)
59 ∀qin0,cin0,qout0,cout0,mv0,tb.
60 tuple_TM n (mk_tuple qin0 cin0 qout0 cout0 mv0) →
61 match_in_table n qin cin qout cout mv tb →
62 match_in_table n qin cin qout cout mv
63 (mk_tuple qin0 cin0 qout0 cout0 mv0@tb).
65 lemma tuple_to_match: ∀n,h,l,qin,cin,qout,cout,mv,p.
66 p = mk_tuple qin cin qout cout mv
67 → mem ? p (tuples_list n h l) →
68 match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_list n h l)).
69 #n #h #l #qin #cin #qout #cout #mv #p
71 [whd in ⊢ (%→?); @False_ind
73 [#H whd in match (tuples_list ???);
75 |#H whd in match (tuples_list ???);
76 cases (is_tuple n h p1) #qin1 * #cin1 * #qout1 * #cout1 * #mv1
77 * #_ #Htuplep1 >Htuplep1 @mit_tl // @Hind //
82 axiom match_decomp: ∀n,l,qin,cin,qout,cout,mv.
83 match_in_table (S n) qin cin qout cout mv l →
84 ∃l1,l2. l = l1@(mk_tuple qin cin qout cout mv)@l2 ∧
85 (∃q.|l1| = (tuple_length (S n))*q) ∧
86 tuple_TM (S n) (mk_tuple qin cin qout cout mv).
88 axiom daemon: ∀P:Prop. P.
90 lemma match_to_tuples_list: ∀n,h,l,qin,cin,qout,cout,mv.
91 match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_list n h l)) →
92 ∃p. p = mk_tuple qin cin qout cout mv ∧ mem ? p (tuples_list n h l).
93 #n #h #l #qin #cin #qout #cout #mv #Hmatch
94 @(ex_intro … (mk_tuple qin cin qout cout mv)) % //
95 cases (match_decomp … Hmatch) #l1 * #l2 * * #Hflat #Hlen #Htuple
96 @(flatten_to_mem … Hflat … Hlen)
99 |@(length_of_tuple … Htuple)
103 lemma match_to_tuple: ∀n,h,l,qin,cin,qout,cout,mv.
104 match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_list n h l)) →
105 ∃p. tuple_encoding n h p = mk_tuple qin cin qout cout mv ∧ mem ? p l.
106 #n #h #l #qin #cin #qout #cout #mv #Hmatch
107 cases (match_to_tuples_list … Hmatch)
109 cases(mem_map … (λp.tuple_encoding n h p) … memb)
110 #p1 * #Hmem #H @(ex_intro … p1) % /2/
113 lemma match_to_trans:
114 ∀n.∀trans: trans_source n → trans_target n.
115 ∀h,qin,cin,qout,cout,mv.
116 match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_list n h (graph_enum ?? trans))) →
117 ∃s,t. tuple_encoding n h 〈s,t〉 = mk_tuple qin cin qout cout mv
119 #n #trans #h #qin #cin #qout #cout #mv #Hmatch
120 cases (match_to_tuple … Hmatch) -Hmatch * #s #t * #Heq #Hmem
121 @(ex_intro … s) @(ex_intro … t) % // @graph_enum_correct
125 lemma trans_to_match:
126 ∀n.∀h.∀trans: trans_source n → trans_target n.
127 ∀s,t,qin,cin,qout,cout,mv. trans s = t →
128 tuple_encoding n h 〈s,t〉 = mk_tuple qin cin qout cout mv →
129 match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_list n h (graph_enum ?? trans))).
130 #n #h #trans #inp #outp #qin #cin #qout #cout #mv #Htrans #Htuple
131 @(tuple_to_match … (refl…)) <Htuple @mem_map_forward
132 @(memb_to_mem (FinProd (trans_source n) (trans_target n)))
133 @graph_enum_complete //
136 axiom append_eq_tech1 :
137 ∀A,l1,l2,l3,l4.l1@l2 = l3@l4 → |l1| < |l3| → ∃la:list A.l1@la = l3.
138 axiom append_eq_tech2 :
139 ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → memb A a l4 = false → ∃la:list A.l3 = l1@a::la.
140 (*axiom list_decompose_cases :
141 ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → ∃la,lb:list A.l3 = la@a::lb ∨ l4 = la@a::lb.
142 axiom list_decompose_l :
143 ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → memb A a l4 = false →
144 ∃la,lb.l2 = la@lb ∧ l3 = l1@a::la.*)
145 axiom list_decompose_r :
146 ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → memb A a l3 = false →
147 ∃la,lb.l1 = la@lb ∧ l4 = lb@a::l2.
148 (*axiom list_decompose_memb :
149 ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → |l1| < |l3| → memb A a l3 = true.*)
151 lemma table_invert_r : ∀n,t,T.
152 tuple_TM n t → table_TM n (t@T) → table_TM n T.
153 #n #t #T #Htuple #Htable inversion Htable
154 [ cases Htuple #qin * #cin * #qout * #cout * #mv * #_ #Ht >Ht
155 normalize #Hfalse destruct (Hfalse)
156 | #t0 #T0 #Htuple0 #Htable0 #_ #Heq
157 lapply (append_l2_injective ?????? Heq)
158 [ >(length_of_tuple … Htuple) >(length_of_tuple … Htuple0) % ]
159 -Heq #Heq destruct (Heq) // ]
162 lemma match_in_table_to_tuple :
163 ∀n,T,qin,cin,qout,cout,mv.
164 match_in_table n qin cin qout cout mv T → table_TM n T →
165 tuple_TM n (mk_tuple qin cin qout cout mv).
166 #n #T #qin #cin #qout #cout #mv #Hmatch elim Hmatch
168 | #qin0 #cin0 #qout0 #cout0 #mv0 #tb #Htuple #Hmatch #IH #Htable
169 @IH @(table_invert_r ???? Htable) @Htuple
173 lemma match_in_table_append :
174 ∀n,T,qin,cin,qout,cout,mv,t.
176 match_in_table n qin cin qout cout mv (t@T) →
177 t = mk_tuple qin cin qout cout mv ∨ match_in_table n qin cin qout cout mv T.
178 #n #T #qin #cin #qout #cout #mv #t #Ht #Hmatch inversion Hmatch
179 [ #T0 #H #H1 % >(append_l1_injective … H1) //
180 >(length_of_tuple … Ht) >(length_of_tuple … H) %
181 | #qin0 #cin0 #qout0 #cout0 #mv0 #T0 #H #H1 #_ #H2 %2
182 >(append_l2_injective … H2) // >(length_of_tuple … Ht) >(length_of_tuple … H) %
186 lemma generic_match_to_match_in_table_tech :
187 ∀n,t,T0,T1,T2.tuple_TM n t → table_TM n (T1@〈bar,false〉::T2) →
188 t@T0 = T1@〈bar,false〉::T2 → T1 = [] ∨ ∃T3.T1 = t@T3.
189 #n #t #T0 #T1 #T2 #Ht cases T1
191 | normalize #c #T1c #Htable #Heq %2
192 cases Ht in Heq; #qin * #cin * #qout * #cout * #mv **********
193 #Hqin1 #Hqout1 #Hqin2 #Hqout2 #Hcin #Hcout #Hmv #Hcoutmv #Hqinlen #Hqoutlen
194 #Heqt >Heqt whd in ⊢ (??%%→?); #Ht lapply (cons_injective_r ????? Ht)
195 #Ht' cases (list_decompose_r STape … (sym_eq … Ht') ?)
196 [ #la * #lb * #HT1c #HT0 %{lb} >HT1c @(eq_f2 ??? (append ?) (c::la)) //
197 >HT0 in Ht'; >HT1c >associative_append in ⊢ (???%→?); #Ht'
198 <(append_l1_injective_r … Ht') // <(cons_injective_l ????? Ht) %
199 |@(noteq_to_eqnot ? true) @(not_to_not … not_eq_true_false) #Hbar @sym_eq
200 cases (memb_append … Hbar) -Hbar #Hbar
202 |cases (orb_true_l … Hbar) -Hbar
203 [#Hbar lapply (\P Hbar) -Hbar #Hbar destruct (Hbar) @Hcin
204 |whd in ⊢ ((??%?)→?); #Hbar cases (memb_append … Hbar) -Hbar #Hbar
206 |cases (orb_true_l … Hbar) -Hbar
207 [#Hbar lapply (\P Hbar) -Hbar #Hbar destruct (Hbar) @Hcout
208 |#Hbar cases (orb_true_l … Hbar) -Hbar
209 [whd in ⊢ ((??%?)→?); #Hbar @Hbar
210 |#Hbar lapply (memb_single … Hbar) -Hbar #Hbar destruct (Hbar) @Hmv
219 lemma generic_match_to_match_in_table :
221 ∀qin,cin,qout,cout,mv.|qin| = n → |qout| = n →
222 only_bits qin → only_bits qout →
223 bit_or_null (\fst cin) = true → bit_or_null (\fst cout) = true →
224 bit_or_null (\fst mv) = true →
226 T = (t1@〈bar,false〉::qin@cin::〈comma,false〉::qout@cout::〈comma,false〉::[mv])@t2 →
227 match_in_table n qin cin qout cout mv T.
228 #n #T #Htable #qin #cin #qout #cout #mv #Hlenqin #Hlenqout
229 #Hqinbits #Hqoutbits #Hcin #Hcout #Hmv
231 [ * [ #t2 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
232 | #c0 #t1 #t2 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
233 | #tuple #T0 #H1 #Htable0#IH #t1 #t2 #HT cases H1 #qin0 * #cin0 * #qout0 * #cout0 * #mv0
235 #Hqin0marks #Hqout0marks #Hqin0bits #Hqout0bits #Hcin0 #Hcout0 #Hmv0 #Hcout0mv0
236 #Hlenqin0 #Hlenqout0 #Htuple
237 lapply (generic_match_to_match_in_table_tech n ? T0 t1
238 (qin@cin::〈comma,false〉::qout@[cout;〈comma,false〉;mv]@t2) H1) #Htmp
240 lapply (ttm_cons … T0 H1 Htable0) <Htuple in ⊢ (%→?); >HT
241 >associative_append normalize >associative_append normalize
242 >associative_append #Htable cases (Htmp Htable ?)
243 [ #Ht1 >Htuple in HT; >Ht1 normalize in ⊢ (??%%→?);
244 >associative_append >associative_append #HT
245 cut (qin0 = qin ∧ (〈cin0,false〉 = cin ∧ (qout0 = qout ∧
246 (〈cout0,false〉 = cout ∧ (〈mv0,false〉 = mv ∧ T0 = t2)))))
247 [ lapply (cons_injective_r ????? HT) -HT #HT
248 lapply (append_l1_injective … HT) [ >Hlenqin @Hlenqin0 ]
249 #Hqin % [ @Hqin ] -Hqin
250 lapply (append_l2_injective … HT) [ >Hlenqin @Hlenqin0 ] -HT #HT
251 lapply (cons_injective_l ????? HT) #Hcin % [ @Hcin ] -Hcin
252 lapply (cons_injective_r ????? HT) -HT #HT
253 lapply (cons_injective_r ????? HT) -HT
254 >associative_append >associative_append #HT
255 lapply (append_l1_injective … HT) [ >Hlenqout @Hlenqout0 ]
256 #Hqout % [ @Hqout ] -Hqout
257 lapply (append_l2_injective … HT) [ >Hlenqout @Hlenqout0 ] -HT normalize #HT
258 lapply (cons_injective_l ????? HT) #Hcout % [ @Hcout ] -Hcout
259 lapply (cons_injective_r ????? HT) -HT #HT
260 lapply (cons_injective_r ????? HT) -HT #HT
261 lapply (cons_injective_l ????? HT) #Hmv % [ @Hmv ] -Hmv
262 @(cons_injective_r ????? HT) ]
263 -HT * #Hqin * #Hcin * #Hqout * #Hcout * #Hmv #HT0
264 >(?:〈bar,false〉::qin0@(〈cin0,false〉::〈comma,false〉::qout0@
265 [〈cout0,false〉;〈comma,false〉;〈mv0,false〉])@T0 = tuple@T0)
266 [ >Htuple >Hqin >Hqout >Hcin >Hcout >Hmv % //
267 | >Htuple normalize >associative_append normalize >associative_append
268 normalize >associative_append % ]
269 | * #T3 #HT3 >HT3 in HT; >associative_append; >associative_append #HT
270 lapply (append_l2_injective … HT) // -HT #HT %2 //
271 @(IH T3 t2) >HT >associative_append %
272 |>HT >associative_append normalize >associative_append normalize
273 >associative_append % ]