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 include "basics/fun_graph.ma".
  16
  17 (* p < n is represented with a list of bits of lenght n with the
  18  p-th bit from left set to 1 *)
  19
  20 let rec to_bitlist n p: list bool ≝
  21   match n with
  22   [ O ⇒ [ ]
  23   | S q ⇒ (eqb p q)::to_bitlist q p].
  24
  25 let rec from_bitlist l ≝
  26   match l with
  27   [ nil ⇒ 0 (* assert false *)
  28   | cons b tl ⇒ if b then |tl| else from_bitlist tl].
  29
  30 lemma bitlist_length: ∀n,p.|to_bitlist n p| = n.
  31 #n elim n normalize //
  32 qed.
  33
  34 lemma bitlist_inv1: ∀n,p.p<n → from_bitlist (to_bitlist n p) = p.
  35 #n elim n normalize -n
  36   [#p #abs @False_ind /2/
  37   |#n #Hind #p #lepn
  38    cases (le_to_or_lt_eq … (le_S_S_to_le … lepn))
  39     [#ltpn lapply (lt_to_not_eq … ltpn) #Hpn
  40      >(not_eq_to_eqb_false … Hpn) normalize @Hind @ltpn
  41     |#Heq >(eq_to_eqb_true … Heq) normalize <Heq //
  42     ]
  43   ]
  44 qed.
  45
  46 lemma bitlist_lt: ∀l. 0 < |l| → from_bitlist l < |l|.
  47 #l elim l normalize // #b #tl #Hind cases b normalize //
  48 #Htl cases (le_to_or_lt_eq … (le_S_S_to_le … Htl)) -Htl #Htl
  49   [@le_S_S @lt_to_le @Hind //
  50   |cut (tl=[ ]) [/2 by append_l2_injective/] #eqtl >eqtl @le_n
  51   ]
  52 qed.
  53
  54 definition nat_of: ∀n. Nat_to n → nat.
  55 #n normalize * #p #_ @p
  56 qed.
  57
  58 definition bits_of_state ≝ λn.λh:Nat_to n → bool.λs:Nat_to n.
  59   h s::(to_bitlist n (nat_of n s)).
  60
  61 definition m_bits_of_state ≝ λn.λh.λp.
  62   map ? (unialpha×bool) (λx.〈bit x,false〉) (bits_of_state n h p).
  63
  64 lemma no_marks_bits_of_state : ∀n,h,p. no_marks (m_bits_of_state n h p).
  65 #n #h #p #x whd in match (m_bits_of_state n h p);
  66 #H cases (orb_true_l … H) -H
  67   [#H >(\P H) %
  68   |elim (to_bitlist n (nat_of n p))
  69     [whd in ⊢ ((??%?)→?); #H destruct
  70     |#b #l #Hind #H cases (orb_true_l … H) -H #H
  71       [>(\P H) %
  72       |@Hind @H
  73       ]
  74     ]
  75   ]
  76 qed.
  77
  78 lemma only_bits_bits_of_state : ∀n,h,p. only_bits (m_bits_of_state n h p).
  79 #n #h #p #x whd in match (m_bits_of_state n h p);
  80 #H cases (orb_true_l … H) -H
  81   [#H >(\P H) %
  82   |elim (to_bitlist n (nat_of n p))
  83     [whd in ⊢ ((??%?)→?); #H destruct
  84     |#b #l #Hind #H cases (orb_true_l … H) -H #H
  85       [>(\P H) %
  86       |@Hind @H
  87       ]
  88     ]
  89   ]
  90 qed.
  91
  92 definition tuple_type ≝ λn.
  93  (Nat_to n × (option FinBool)) × (Nat_to n × (option (FinBool × move))).
  94
  95 definition tuple_of_pair ≝ λn.λh:Nat_to n→bool.
  96   λp:tuple_type n.
  97   let 〈inp,outp〉 ≝ p in
  98   let 〈q,a〉 ≝ inp in
  99   let cin ≝ match a with [ None ⇒ null | Some b ⇒ bit b ] in
 100   let 〈qn,action〉 ≝ outp in
 101   let 〈cout,mv〉 ≝
 102     match action with
 103     [ None ⇒ 〈null,null〉
 104     | Some act ⇒ let 〈na,m〉 ≝ act in
 105       match m with
 106       [ R ⇒ 〈bit na,bit true〉
 107       | L ⇒ 〈bit na,bit false〉
 108       | N ⇒ 〈bit na,null〉]
 109     ] in
 110   let qin ≝ m_bits_of_state n h q in
 111   let qout ≝ m_bits_of_state n h qn in
 112   mk_tuple qin 〈cin,false〉 qout 〈cout,false〉 〈mv,false〉.
 113
 114 definition WFTuple_conditions ≝
 115  λn,qin,cin,qout,cout,mv.
 116  no_marks qin ∧ no_marks qout ∧ (* queste fuori ? *)
 117  only_bits qin ∧ only_bits qout ∧
 118  bit_or_null cin = true ∧ bit_or_null cout = true ∧ bit_or_null mv = true ∧
 119  (cout = null → mv = null) ∧
 120  |qin| = n ∧ |qout| = n.
 121
 122 lemma is_tuple: ∀n,h,p. tuple_TM (S n) (tuple_of_pair n h p).
 123 #n #h * * #q #a * #qn #action
 124 @(ex_intro … (m_bits_of_state n h q))
 125 letin cin ≝ match a with [ None ⇒ null | Some b ⇒ bit b ]
 126 @(ex_intro … cin)
 127 @(ex_intro … (m_bits_of_state n h qn))
 128 letin cout ≝
 129   match action with
 130   [ None ⇒ null | Some act ⇒ bit (\fst act)]
 131 @(ex_intro … cout)
 132 letin mv ≝ match action with
 133   [ None ⇒ null
 134   | Some act ⇒
 135       match \snd act with
 136       [ R ⇒ bit true | L ⇒ bit false | N ⇒ null]
 137   ]
 138 @(ex_intro … mv)
 139 %[%[%[%[%[%[%[% /3/
 140              |whd in match cin ; cases a //
 141              ]
 142            |whd in match cout; cases action //
 143            ]
 144          |whd in match mv; cases action //
 145           * #b #m cases m //
 146          ]
 147        |whd in match cout; whd in match mv; cases action
 148          [// | #act whd in ⊢ ((??%?)→?); #Hfalse destruct ]
 149        ]
 150      |>length_map normalize @eq_f //
 151      ]
 152    |>length_map normalize @eq_f //
 153    ]
 154  |normalize cases a cases action normalize //
 155    [* #c #m cases m %
 156    |* #c #m #c1 cases m %
 157    ]
 158  ]
 159 qed.
 160
 161 definition tuple_length ≝ λn.2*n+6.
 162
 163 lemma length_of_tuple: ∀n,t. tuple_TM n t →
 164   |t| = tuple_length n.
 165 #n #t * #qin * #cin * #qout * #cout * #mv *** #_
 166 #Hqin #Hqout #eqt >eqt whd in match (mk_tuple ?????);
 167 normalize >length_append >Hqin -Hqin normalize
 168 >length_append normalize >Hqout -Hqout //
 169 qed.
 170
 171 definition move_eq ≝ λm1,m2:move.
 172   match m1 with
 173   [R ⇒ match m2 with [R ⇒ true | _ ⇒ false]
 174   |L ⇒ match m2 with [L ⇒ true | _ ⇒ false]
 175   |N ⇒ match m2 with [N ⇒ true | _ ⇒ false]].
 176
 177 definition tuples_of_pairs ≝ λn.λh.map … (λp.tuple_of_pair n h p).
 178
 179 definition flatten ≝ λA.foldr (list A) (list A) (append A) [].
 180
 181 lemma wftable: ∀n,h,l.table_TM (S n) (flatten ? (tuples_of_pairs n h l)).
 182 #n #h #l elim l // -l #a #tl #Hind
 183 whd in match (flatten … (tuples_of_pairs …));
 184 @ttm_cons //
 185 qed.
 186
 187 lemma flatten_to_mem: ∀A,n,l,l1,l2.∀a:list A. 0 < n →
 188   (∀x. mem ? x l → |x| = n) → |a| = n → flatten ? l = l1@a@l2  →
 189     (∃q.|l1| = n*q)  → mem ? a l.
 190 #A #n #l elim l
 191   [normalize #l1 #l2 #a #posn #Hlen #Ha #Hnil @False_ind
 192    cut (|a|=0) [@daemon] /2/
 193   |#hd #tl #Hind #l1 #l2 #a #posn #Hlen #Ha
 194    whd in match (flatten ??); #Hflat * #q cases q
 195     [<times_n_O #Hl1
 196      cut (a = hd) [@daemon] /2/
 197     |#q1 #Hl1 lapply (split_exists … n l1 ?) //
 198      * #l11 * #l12 * #Heql1 #Hlenl11 %2
 199      @(Hind l12 l2 … posn ? Ha)
 200       [#x #memx @Hlen %2 //
 201       |@(append_l2_injective ? hd l11)
 202         [>Hlenl11 @Hlen %1 %
 203         |>Hflat >Heql1 >associative_append %
 204         ]
 205       |@(ex_intro …q1) @(injective_plus_r n)
 206        <Hlenl11 in ⊢ (??%?); <length_append <Heql1 >Hl1 //
 207       ]
 208     ]
 209   ]
 210 qed.
 211
 212 axiom match_decomp: ∀n,l,qin,cin,qout,cout,mv.
 213   match_in_table (S n) qin cin qout cout mv l →
 214   ∃l1,l2. l = l1@(mk_tuple qin cin qout cout mv)@l2 ∧
 215     (∃q.|l1| = (tuple_length (S n))*q) ∧ tuple_TM (S n) (mk_tuple qin cin qout cout mv).
 216 (*
 217 lemma match_tech: ∀n,l,qin,cin,qout,cout,mv.
 218   (∀t. mem ? t l → |t| = |mk_tuple qin cin qout cout mv|) →
 219   match_in_table (S n) qin cin qout cout mv (flatten ? l) →
 220     ∃p. p = mk_tuple qin cin qout cout mv ∧ mem ? p l.
 221 #n #l #qin #cin #qout #cout #mv #Hlen #Hmatch
 222 @(ex_intro … (mk_tuple qin cin qout cout mv)) % //
 223 @flatten_to_mem *)
 224
 225 lemma match_to_tuple: ∀n,h,l,qin,cin,qout,cout,mv.
 226   match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h l)) →
 227     ∃p. p = mk_tuple qin cin qout cout mv ∧ mem ? p (tuples_of_pairs n h l).
 228 #n #h #l #qin #cin #qout #cout #mv #Hmatch
 229 @(ex_intro … (mk_tuple qin cin qout cout mv)) % //
 230 cases (match_decomp … Hmatch) #l1 * #l2 * * #Hflat #Hlen #Htuple
 231 @(flatten_to_mem … Hflat … Hlen)
 232   [//
 233   |@daemon
 234   |@(length_of_tuple … Htuple)
 235   ]
 236 qed.
 237
 238 lemma mem_map: ∀A,B.∀f:A→B.∀l,b.
 239   mem ? b (map … f l) → ∃a. mem ? a l ∧ f a = b.
 240 #A #B #f #l elim l
 241   [#b normalize @False_ind
 242   |#a #tl #Hind #b normalize *
 243     [#eqb @(ex_intro … a) /3/
 244     |#memb cases (Hind … memb) #a * #mema #eqb
 245      @(ex_intro … a) /3/
 246     ]
 247   ]
 248 qed.
 249
 250 lemma match_to_pair: ∀n,h,l,qin,cin,qout,cout,mv.
 251   match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h l)) →
 252     ∃p. tuple_of_pair n h p = mk_tuple qin cin qout cout mv ∧ mem ? p l.
 253 #n #h #l #qin #cin #qout #cout #mv #Hmatch
 254 cases (match_to_tuple … Hmatch)
 255 #p * #eqp #memb
 256 cases(mem_map … (λp.tuple_of_pair n h p) … memb)
 257 #p1 * #Hmem #H @(ex_intro … p1) % /2/
 258 qed.
 259
 260 (* turning DeqMove into a DeqSet *)
 261 lemma move_eq_true:∀m1,m2.
 262   move_eq m1 m2 = true ↔ m1 = m2.
 263 *
 264   [* normalize [% #_ % |2,3: % #H destruct ]
 265   |* normalize [1,3: % #H destruct |% #_ % ]
 266   |* normalize [1,2: % #H destruct |% #_ % ]
 267 qed.
 268
 269 definition DeqMove ≝ mk_DeqSet move move_eq move_eq_true.
 270
 271 unification hint 0 ≔ ;
 272     X ≟ DeqMove
 273 (* ---------------------------------------- *) ⊢
 274     move ≡ carr X.
 275
 276 unification hint  0 ≔ m1,m2;
 277     X ≟ DeqMove
 278 (* ---------------------------------------- *) ⊢
 279     move_eq m1 m2 ≡ eqb X m1 m2.
 280
 281 (* turning DeqMove into a FinSet *)
 282 definition move_enum ≝ [L;R;N].
 283
 284 lemma move_enum_unique: uniqueb ? [L;R;N] = true.
 285 // qed.
 286
 287 lemma move_enum_complete: ∀x:move. memb ? x [L;R;N] = true.
 288 * // qed.
 289
 290 definition FinMove ≝
 291   mk_FinSet DeqMove [L;R;N] move_enum_unique move_enum_complete.
 292
 293 unification hint  0 ≔ ;
 294     X ≟ FinMove
 295 (* ---------------------------------------- *) ⊢
 296     move ≡ FinSetcarr X.
 297
 298 definition trans_source ≝ λn.FinProd (initN n) (FinOption FinBool).
 299 definition trans_target ≝ λn.FinProd (initN n) (FinOption (FinProd FinBool FinMove)).
 300
 301 lemma match_to_trans:
 302   ∀n.∀trans: trans_source n → trans_target n.
 303   ∀h,qin,cin,qout,cout,mv.
 304   match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h (graph_enum ?? trans))) →
 305   ∃s,t. tuple_of_pair n h 〈s,t〉 = mk_tuple qin cin qout cout mv
 306     ∧ trans s = t.
 307 #n #trans #h #qin #cin #qout #cout #mv #Hmatch
 308 cases (match_to_pair … Hmatch) -Hmatch * #s #t * #Heq #Hmem
 309 @(ex_intro … s) @(ex_intro … t) % // @graph_enum_correct
 310 @mem_to_memb @Hmem
 311 qed.
 312