matita/matita/lib/turing/universal/trans_to_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
  14 include "turing/universal/tuples.ma".
  15
  16 (* p < n is represented with a list of bits of lenght n with the
  17  p-th bit from left set to 1 *)
  18
  19 let rec to_bitlist n p: list bool ≝
  20   match n with
  21   [ O ⇒ [ ]
  22   | S q ⇒ (eqb p q)::to_bitlist q p].
  23
  24 let rec from_bitlist l ≝
  25   match l with
  26   [ nil ⇒ 0 (* assert false *)
  27   | cons b tl ⇒ if b then |tl| else from_bitlist tl].
  28
  29 lemma bitlist_length: ∀n,p.|to_bitlist n p| = n.
  30 #n elim n normalize //
  31 qed.
  32
  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/
  36   |#n #Hind #p #lepn
  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 //
  41     ]
  42   ]
  43 qed.
  44
  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
  50   ]
  51 qed.
  52
  53 definition nat_of: ∀n. Nat_to n → nat.
  54 #n normalize * #p #_ @p
  55 qed.
  56
  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)).
  59
  60 definition m_bits_of_state ≝ λn.λh.λp.
  61   map ? (unialpha×bool) (λx.〈bit x,false〉) (bits_of_state n h p).
  62
  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
  66   [#H >(\P 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
  70       [>(\P H) %
  71       |@Hind @H
  72       ]
  73     ]
  74   ]
  75 qed.
  76
  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
  80   [#H >(\P 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
  84       [>(\P H) %
  85       |@Hind @H
  86       ]
  87     ]
  88   ]
  89 qed.
  90
  91 definition tuple_type ≝ λn.
  92  (Nat_to n × (option FinBool)) × (Nat_to n × (option (FinBool × move))).
  93
  94 definition low_action ≝ λaction.
  95   match action with
  96     [ None ⇒ 〈null,null〉
  97     | Some act ⇒ let 〈na,m〉 ≝ act in
  98       match m with
  99       [ R ⇒ 〈bit na,bit true〉
 100       | L ⇒ 〈bit na,bit false〉
 101       | N ⇒ 〈bit na,null〉]
 102     ].
 103
 104 definition tuple_of_pair ≝ λn.λh:Nat_to n→bool.
 105   λp:tuple_type n.
 106   let 〈inp,outp〉 ≝ p in
 107   let 〈q,a〉 ≝ inp 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〉.
 114
 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.
 122
 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 ]
 127 @(ex_intro … cin)
 128 @(ex_intro … (m_bits_of_state n h qn))
 129 letin cout ≝
 130   match action with
 131   [ None ⇒ null | Some act ⇒ bit (\fst act)]
 132 @(ex_intro … cout)
 133 letin mv ≝ match action with
 134   [ None ⇒ null
 135   | Some act ⇒
 136       match \snd act with
 137       [ R ⇒ bit true | L ⇒ bit false | N ⇒ null]
 138   ]
 139 @(ex_intro … mv)
 140 %[%[%[%[%[%[%[% /3/
 141              |whd in match cin ; cases a //
 142              ]
 143            |whd in match cout; cases action //
 144            ]
 145          |whd in match mv; cases action //
 146           * #b #m cases m //
 147          ]
 148        |whd in match cout; whd in match mv; cases action
 149          [// | #act whd in ⊢ ((??%?)→?); #Hfalse destruct ]
 150        ]
 151      |>length_map normalize @eq_f //
 152      ]
 153    |>length_map normalize @eq_f //
 154    ]
 155  |normalize cases a cases action normalize //
 156    [* #c #m cases m %
 157    |* #c #m #c1 cases m %
 158    ]
 159  ]
 160 qed.
 161
 162 definition tuple_length ≝ λn.2*n+6.
 163
 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 //
 170 qed.
 171
 172 definition move_eq ≝ λm1,m2:move.
 173   match m1 with
 174   [R ⇒ match m2 with [R ⇒ true | _ ⇒ false]
 175   |L ⇒ match m2 with [L ⇒ true | _ ⇒ false]
 176   |N ⇒ match m2 with [N ⇒ true | _ ⇒ false]].
 177
 178 definition tuples_of_pairs ≝ λn.λh.map … (λp.tuple_of_pair n h p).
 179
 180 definition flatten ≝ λA.foldr (list A) (list A) (append A) [].
 181
 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 …));
 185 @ttm_cons //
 186 qed.
 187
 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.
 191 #A #n #l elim 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
 196     [<times_n_O #Hl1
 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)
 203         [>Hlenl11 @Hlen %1 %
 204         |>Hflat >Heql1 >associative_append %
 205         ]
 206       |@(ex_intro …q1) @(injective_plus_r n)
 207        <Hlenl11 in ⊢ (??%?); <length_append <Heql1 >Hl1 //
 208       ]
 209     ]
 210   ]
 211 qed.
 212
 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
 218 #Hp elim l
 219   [whd in ⊢ (%→?); @False_ind
 220   |#p1 #tl #Hind *
 221     [#H whd in match (tuples_of_pairs ???);
 222      <H >Hp @mit_hd //
 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 //
 226     ]
 227   ]
 228 qed.
 229
 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).
 234 (*
 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)) % //
 241 @flatten_to_mem *)
 242
 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)
 250   [//
 251   |@daemon
 252   |@(length_of_tuple … Htuple)
 253   ]
 254 qed.
 255
 256 lemma mem_map: ∀A,B.∀f:A→B.∀l,b.
 257   mem ? b (map … f l) → ∃a. mem ? a l ∧ f a = b.
 258 #A #B #f #l elim l
 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
 263      @(ex_intro … a) /3/
 264     ]
 265   ]
 266 qed.
 267
 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)
 273 #p * #eqp #memb
 274 cases(mem_map … (λp.tuple_of_pair n h p) … memb)
 275 #p1 * #Hmem #H @(ex_intro … p1) % /2/
 276 qed.
 277
 278 (* turning DeqMove into a DeqSet *)
 279 lemma move_eq_true:∀m1,m2.
 280   move_eq m1 m2 = true ↔ m1 = m2.
 281 *
 282   [* normalize [% #_ % |2,3: % #H destruct ]
 283   |* normalize [1,3: % #H destruct |% #_ % ]
 284   |* normalize [1,2: % #H destruct |% #_ % ]
 285 qed.
 286
 287 definition DeqMove ≝ mk_DeqSet move move_eq move_eq_true.
 288
 289 unification hint 0 ≔ ;
 290     X ≟ DeqMove
 291 (* ---------------------------------------- *) ⊢
 292     move ≡ carr X.
 293
 294 unification hint  0 ≔ m1,m2;
 295     X ≟ DeqMove
 296 (* ---------------------------------------- *) ⊢
 297     move_eq m1 m2 ≡ eqb X m1 m2.
 298
 299 (* turning DeqMove into a FinSet *)
 300 definition move_enum ≝ [L;R;N].
 301
 302 lemma move_enum_unique: uniqueb ? [L;R;N] = true.
 303 // qed.
 304
 305 lemma move_enum_complete: ∀x:move. memb ? x [L;R;N] = true.
 306 * // qed.
 307
 308 definition FinMove ≝
 309   mk_FinSet DeqMove [L;R;N] move_enum_unique move_enum_complete.
 310
 311 unification hint  0 ≔ ;
 312     X ≟ FinMove
 313 (* ---------------------------------------- *) ⊢
 314     move ≡ FinSetcarr X.
 315
 316 definition trans_source ≝ λn.FinProd (initN n) (FinOption FinBool).
 317 definition trans_target ≝ λn.FinProd (initN n) (FinOption (FinProd FinBool FinMove)).
 318
 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
 324     ∧ trans s = t.
 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
 328 @mem_to_memb @Hmem
 329 qed.
 330
 331 (* da spistare *)
 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
 336   |#b #tl #Hind *
 337     [#eqab <eqab normalize %1 % |#memtl normalize %2 @Hind @memtl]
 338   ]
 339 qed.
 340
 341 lemma memb_to_mem: ∀S:DeqSet.∀l,a. memb S a l =true → mem S a l.
 342 #S #l #a elim l
 343   [normalize #H destruct
 344   |#b #tl #Hind #mema cases (orb_true_l … mema)
 345     [#eqab >(\P eqab) %1 % |#memtl %2 @Hind @memtl]
 346   ]
 347 qed.
 348
 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 //
 358 qed.
 359
 360 (*
 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 //
 370 qed. *)
 371
 372
 373 (*
 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 ] →
 379   ∃qout,cout,mv.
 380   qout = m_bits_of_state n h qn ∧
 381   (〈cout,mv〉 = match action with
 382     [ None ⇒ 〈null,null〉
 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…)) *)