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_____________________________________________________________*)
14 include "turing/universal/tuples.ma".
16 (* p < n is represented with a list of bits of lenght n with the
17 p-th bit from left set to 1 *)
19 let rec to_bitlist n p: list bool ≝
22 | S q ⇒ (eqb p q)::to_bitlist q p].
24 let rec from_bitlist l ≝
26 [ nil ⇒ 0 (* assert false *)
27 | cons b tl ⇒ if b then |tl| else from_bitlist tl].
29 lemma bitlist_length: ∀n,p.|to_bitlist n p| = n.
30 #n elim n normalize //
33 lemma bitlist_inv1: ∀n,p.p<n → from_bitlist (to_bitlist n p) = p.
34 #n elim n normalize -n
35 [#p #abs @False_ind /2/
37 cases (le_to_or_lt_eq … (le_S_S_to_le … lepn))
38 [#ltpn lapply (lt_to_not_eq … ltpn) #Hpn
39 >(not_eq_to_eqb_false … Hpn) normalize @Hind @ltpn
40 |#Heq >(eq_to_eqb_true … Heq) normalize <Heq //
45 lemma bitlist_lt: ∀l. 0 < |l| → from_bitlist l < |l|.
46 #l elim l normalize // #b #tl #Hind cases b normalize //
47 #Htl cases (le_to_or_lt_eq … (le_S_S_to_le … Htl)) -Htl #Htl
48 [@le_S_S @lt_to_le @Hind //
49 |cut (tl=[ ]) [/2 by append_l2_injective/] #eqtl >eqtl @le_n
53 definition nat_of: ∀n. Nat_to n → nat.
54 #n normalize * #p #_ @p
57 definition bits_of_state ≝ λn.λh:Nat_to n → bool.λs:Nat_to n.
58 h s::(to_bitlist n (nat_of n s)).
60 definition m_bits_of_state ≝ λn.λh.λp.
61 map ? (unialpha×bool) (λx.〈bit x,false〉) (bits_of_state n h p).
63 lemma no_marks_bits_of_state : ∀n,h,p. no_marks (m_bits_of_state n h p).
64 #n #h #p #x whd in match (m_bits_of_state n h p);
65 #H cases (orb_true_l … H) -H
67 |elim (to_bitlist n (nat_of n p))
68 [whd in ⊢ ((??%?)→?); #H destruct
69 |#b #l #Hind #H cases (orb_true_l … H) -H #H
77 lemma only_bits_bits_of_state : ∀n,h,p. only_bits (m_bits_of_state n h p).
78 #n #h #p #x whd in match (m_bits_of_state n h p);
79 #H cases (orb_true_l … H) -H
81 |elim (to_bitlist n (nat_of n p))
82 [whd in ⊢ ((??%?)→?); #H destruct
83 |#b #l #Hind #H cases (orb_true_l … H) -H #H
91 definition tuple_type ≝ λn.
92 (Nat_to n × (option FinBool)) × (Nat_to n × (option (FinBool × move))).
94 definition low_action ≝ λaction.
97 | Some act ⇒ let 〈na,m〉 ≝ act in
99 [ R ⇒ 〈bit na,bit true〉
100 | L ⇒ 〈bit na,bit false〉
104 definition tuple_of_pair ≝ λn.λh:Nat_to n→bool.
106 let 〈inp,outp〉 ≝ p in
108 let cin ≝ match a with [ None ⇒ null | Some b ⇒ bit b ] in
109 let 〈qn,action〉 ≝ outp in
110 let 〈cout,mv〉 ≝ low_action action in
111 let qin ≝ m_bits_of_state n h q in
112 let qout ≝ m_bits_of_state n h qn in
113 mk_tuple qin 〈cin,false〉 qout 〈cout,false〉 〈mv,false〉.
115 definition WFTuple_conditions ≝
116 λn,qin,cin,qout,cout,mv.
117 no_marks qin ∧ no_marks qout ∧ (* queste fuori ? *)
118 only_bits qin ∧ only_bits qout ∧
119 bit_or_null cin = true ∧ bit_or_null cout = true ∧ bit_or_null mv = true ∧
120 (cout = null → mv = null) ∧
121 |qin| = n ∧ |qout| = n.
123 lemma is_tuple: ∀n,h,p. tuple_TM (S n) (tuple_of_pair n h p).
124 #n #h * * #q #a * #qn #action
125 @(ex_intro … (m_bits_of_state n h q))
126 letin cin ≝ match a with [ None ⇒ null | Some b ⇒ bit b ]
128 @(ex_intro … (m_bits_of_state n h qn))
131 [ None ⇒ null | Some act ⇒ bit (\fst act)]
133 letin mv ≝ match action with
137 [ R ⇒ bit true | L ⇒ bit false | N ⇒ null]
141 |whd in match cin ; cases a //
143 |whd in match cout; cases action //
145 |whd in match mv; cases action //
148 |whd in match cout; whd in match mv; cases action
149 [// | #act whd in ⊢ ((??%?)→?); #Hfalse destruct ]
151 |>length_map normalize @eq_f //
153 |>length_map normalize @eq_f //
155 |normalize cases a cases action normalize //
157 |* #c #m #c1 cases m %
162 definition tuple_length ≝ λn.2*n+6.
164 lemma length_of_tuple: ∀n,t. tuple_TM n t →
165 |t| = tuple_length n.
166 #n #t * #qin * #cin * #qout * #cout * #mv *** #_
167 #Hqin #Hqout #eqt >eqt whd in match (mk_tuple ?????);
168 normalize >length_append >Hqin -Hqin normalize
169 >length_append normalize >Hqout -Hqout //
172 definition move_eq ≝ λm1,m2:move.
174 [R ⇒ match m2 with [R ⇒ true | _ ⇒ false]
175 |L ⇒ match m2 with [L ⇒ true | _ ⇒ false]
176 |N ⇒ match m2 with [N ⇒ true | _ ⇒ false]].
178 definition tuples_of_pairs ≝ λn.λh.map … (λp.tuple_of_pair n h p).
180 definition flatten ≝ λA.foldr (list A) (list A) (append A) [].
182 lemma wftable: ∀n,h,l.table_TM (S n) (flatten ? (tuples_of_pairs n h l)).
183 #n #h #l elim l // -l #a #tl #Hind
184 whd in match (flatten … (tuples_of_pairs …));
188 lemma flatten_to_mem: ∀A,n,l,l1,l2.∀a:list A. 0 < n →
189 (∀x. mem ? x l → |x| = n) → |a| = n → flatten ? l = l1@a@l2 →
190 (∃q.|l1| = n*q) → mem ? a l.
192 [normalize #l1 #l2 #a #posn #Hlen #Ha #Hnil @False_ind
193 cut (|a|=0) [@daemon] /2/
194 |#hd #tl #Hind #l1 #l2 #a #posn #Hlen #Ha
195 whd in match (flatten ??); #Hflat * #q cases q
197 cut (a = hd) [@daemon] /2/
198 |#q1 #Hl1 lapply (split_exists … n l1 ?) //
199 * #l11 * #l12 * #Heql1 #Hlenl11 %2
200 @(Hind l12 l2 … posn ? Ha)
201 [#x #memx @Hlen %2 //
202 |@(append_l2_injective ? hd l11)
204 |>Hflat >Heql1 >associative_append %
206 |@(ex_intro …q1) @(injective_plus_r n)
207 <Hlenl11 in ⊢ (??%?); <length_append <Heql1 >Hl1 //
213 lemma tuple_to_match: ∀n,h,l,qin,cin,qout,cout,mv,p.
214 p = mk_tuple qin cin qout cout mv
215 → mem ? p (tuples_of_pairs n h l) →
216 match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h l)).
217 #n #h #l #qin #cin #qout #cout #mv #p
219 [whd in ⊢ (%→?); @False_ind
221 [#H whd in match (tuples_of_pairs ???);
223 |#H whd in match (tuples_of_pairs ???);
224 cases (is_tuple n h p1) #qin1 * #cin1 * #qout1 * #cout1 * #mv1
225 * #_ #Htuplep1 >Htuplep1 @mit_tl // @Hind //
230 axiom match_decomp: ∀n,l,qin,cin,qout,cout,mv.
231 match_in_table (S n) qin cin qout cout mv l →
232 ∃l1,l2. l = l1@(mk_tuple qin cin qout cout mv)@l2 ∧
233 (∃q.|l1| = (tuple_length (S n))*q) ∧ tuple_TM (S n) (mk_tuple qin cin qout cout mv).
235 lemma match_tech: ∀n,l,qin,cin,qout,cout,mv.
236 (∀t. mem ? t l → |t| = |mk_tuple qin cin qout cout mv|) →
237 match_in_table (S n) qin cin qout cout mv (flatten ? l) →
238 ∃p. p = mk_tuple qin cin qout cout mv ∧ mem ? p l.
239 #n #l #qin #cin #qout #cout #mv #Hlen #Hmatch
240 @(ex_intro … (mk_tuple qin cin qout cout mv)) % //
243 lemma match_to_tuple: ∀n,h,l,qin,cin,qout,cout,mv.
244 match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h l)) →
245 ∃p. p = mk_tuple qin cin qout cout mv ∧ mem ? p (tuples_of_pairs n h l).
246 #n #h #l #qin #cin #qout #cout #mv #Hmatch
247 @(ex_intro … (mk_tuple qin cin qout cout mv)) % //
248 cases (match_decomp … Hmatch) #l1 * #l2 * * #Hflat #Hlen #Htuple
249 @(flatten_to_mem … Hflat … Hlen)
252 |@(length_of_tuple … Htuple)
256 lemma mem_map: ∀A,B.∀f:A→B.∀l,b.
257 mem ? b (map … f l) → ∃a. mem ? a l ∧ f a = b.
259 [#b normalize @False_ind
260 |#a #tl #Hind #b normalize *
261 [#eqb @(ex_intro … a) /3/
262 |#memb cases (Hind … memb) #a * #mema #eqb
268 lemma match_to_pair: ∀n,h,l,qin,cin,qout,cout,mv.
269 match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h l)) →
270 ∃p. tuple_of_pair n h p = mk_tuple qin cin qout cout mv ∧ mem ? p l.
271 #n #h #l #qin #cin #qout #cout #mv #Hmatch
272 cases (match_to_tuple … Hmatch)
274 cases(mem_map … (λp.tuple_of_pair n h p) … memb)
275 #p1 * #Hmem #H @(ex_intro … p1) % /2/
278 (* turning DeqMove into a DeqSet *)
279 lemma move_eq_true:∀m1,m2.
280 move_eq m1 m2 = true ↔ m1 = m2.
282 [* normalize [% #_ % |2,3: % #H destruct ]
283 |* normalize [1,3: % #H destruct |% #_ % ]
284 |* normalize [1,2: % #H destruct |% #_ % ]
287 definition DeqMove ≝ mk_DeqSet move move_eq move_eq_true.
289 unification hint 0 ≔ ;
291 (* ---------------------------------------- *) ⊢
294 unification hint 0 ≔ m1,m2;
296 (* ---------------------------------------- *) ⊢
297 move_eq m1 m2 ≡ eqb X m1 m2.
299 (* turning DeqMove into a FinSet *)
300 definition move_enum ≝ [L;R;N].
302 lemma move_enum_unique: uniqueb ? [L;R;N] = true.
305 lemma move_enum_complete: ∀x:move. memb ? x [L;R;N] = true.
309 mk_FinSet DeqMove [L;R;N] move_enum_unique move_enum_complete.
311 unification hint 0 ≔ ;
313 (* ---------------------------------------- *) ⊢
316 definition trans_source ≝ λn.FinProd (initN n) (FinOption FinBool).
317 definition trans_target ≝ λn.FinProd (initN n) (FinOption (FinProd FinBool FinMove)).
319 lemma match_to_trans:
320 ∀n.∀trans: trans_source n → trans_target n.
321 ∀h,qin,cin,qout,cout,mv.
322 match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h (graph_enum ?? trans))) →
323 ∃s,t. tuple_of_pair n h 〈s,t〉 = mk_tuple qin cin qout cout mv
325 #n #trans #h #qin #cin #qout #cout #mv #Hmatch
326 cases (match_to_pair … Hmatch) -Hmatch * #s #t * #Heq #Hmem
327 @(ex_intro … s) @(ex_intro … t) % // @graph_enum_correct
332 lemma mem_map_forward: ∀A,B.∀f:A→B.∀a,l.
333 mem A a l → mem B (f a) (map ?? f l).
334 #A #B #f #a #l elim l
335 [normalize @False_ind
337 [#eqab <eqab normalize %1 % |#memtl normalize %2 @Hind @memtl]
341 lemma memb_to_mem: ∀S:DeqSet.∀l,a. memb S a l =true → mem S a l.
343 [normalize #H destruct
344 |#b #tl #Hind #mema cases (orb_true_l … mema)
345 [#eqab >(\P eqab) %1 % |#memtl %2 @Hind @memtl]
349 lemma trans_to_match:
350 ∀n.∀h.∀trans: trans_source n → trans_target n.
351 ∀inp,outp,qin,cin,qout,cout,mv. trans inp = outp →
352 tuple_of_pair n h 〈inp,outp〉 = mk_tuple qin cin qout cout mv →
353 match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h (graph_enum ?? trans))).
354 #n #h #trans #inp #outp #qin #cin #qout #cout #mv #Htrans #Htuple
355 @(tuple_to_match … (refl…)) <Htuple @mem_map_forward
356 @(memb_to_mem (FinProd (trans_source n) (trans_target n)))
357 @graph_enum_complete //
361 lemma trans_to_match:
362 ∀n.∀h.∀trans: trans_source n → trans_target n.
363 ∀inp,outp,qin,cin,qout,cout,mv. trans inp = outp →
364 tuple_of_pair n h 〈inp,outp〉 = mk_tuple qin cin qout cout mv →
365 match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h (graph_enum ?? trans))).
366 #n #h #trans #inp #outp #qin #cin #qout #cout #mv #Htrans #Htuple
367 @(tuple_to_match … (refl…)) <Htuple @mem_map_forward
368 @(memb_to_mem (FinProd (trans_source n) (trans_target n)))
369 @graph_enum_complete //
374 lemma trans_to_match:
375 ∀n.∀h.∀trans: trans_source n → trans_target n.
376 ∀q,a,qn,action,qin,cin. trans 〈q,a〉 = 〈qn,action〉 →
377 qin = m_bits_of_state n h q →
378 cin = match a with [ None ⇒ null | Some b ⇒ bit b ] →
380 qout = m_bits_of_state n h qn ∧
381 (〈cout,mv〉 = match action with
383 | Some act ⇒ let 〈na,m〉 ≝ act in
384 match m with [ R ⇒ 〈bit na,bit true〉 | L ⇒ 〈bit na,bit false〉 | N ⇒ 〈bit na,null〉] ]) ∧
385 match_in_table (S n) qin 〈cin,false〉 qout 〈cout,false〉 〈mv,false〉 (flatten ? (tuples_of_pairs n h (graph_enum ?? trans))).
386 #n #h #trans #q #a #qn #action #qin #cin #Htrans #Hqin #Hcin
387 @(ex_intro … (m_bits_of_state n h qn))
388 @(ex_intro … ?) [|@(ex_intro ?) [| % [ % [% | //]]
389 @(tuple_to_match … (refl…)) *)