matita/matita/lib/turing/universal/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 (****************************** table of tuples *******************************)
  14 include "turing/universal/normalTM.ma".
  15
  16 (* a well formed table is a list of tuples *)
  17
  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).
  21
  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 …));
  25 @ttm_cons //
  26 qed.
  27
  28 (*********************** general properties of tables *************************)
  29 lemma no_grids_in_table: ∀n.∀l.table_TM n l → no_grids l.
  30 #n #l #t elim t
  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
  34    [ @(Ht1 … Hx)
  35    | @(IH … Hx) ] ]
  36 qed.
  37
  38 lemma no_marks_in_table: ∀n.∀l.table_TM n l → no_marks l.
  39 #n #l #t elim t
  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
  43    [ @(Ht1 … Hx)
  44    | @(IH … Hx) ] ]
  45 qed.
  46
  47 axiom last_of_table: ∀n,l,b.¬ table_TM n (l@[〈bar,b〉]).
  48
  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)
  52 : list STape → Prop ≝
  53 | mit_hd :
  54    ∀tb.
  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)
  58 | mit_tl :
  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).
  64
  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
  70 #Hp elim l
  71   [whd in ⊢ (%→?); @False_ind
  72   |#p1 #tl #Hind *
  73     [#H whd in match (tuples_list ???);
  74      <H >Hp @mit_hd //
  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 //
  78     ]
  79   ]
  80 qed.
  81
  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).
  87
  88 lemma match_to_tuples_list: ∀n,h,l,qin,cin,qout,cout,mv.
  89   match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_list n h l)) →
  90     ∃p. p = mk_tuple qin cin qout cout mv ∧ mem ? p (tuples_list n h l).
  91 #n #h #l #qin #cin #qout #cout #mv #Hmatch
  92 @(ex_intro … (mk_tuple qin cin qout cout mv)) % //
  93 cases (match_decomp … Hmatch) #l1 * #l2 * * #Hflat #Hlen #Htuple
  94 @(flatten_to_mem … Hflat … Hlen)
  95   [//
  96   |#x #memx @length_of_tuple
  97    cases (mem_map ????? memx) #t * #memt #Ht <Ht //
  98   |@(length_of_tuple … Htuple)
  99   ]
 100 qed.
 101
 102 lemma match_to_tuple: ∀n,h,l,qin,cin,qout,cout,mv.
 103   match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_list n h l)) →
 104     ∃p. tuple_encoding n h p = mk_tuple qin cin qout cout mv ∧ mem ? p l.
 105 #n #h #l #qin #cin #qout #cout #mv #Hmatch
 106 cases (match_to_tuples_list … Hmatch)
 107 #p * #eqp #memb
 108 cases(mem_map … (λp.tuple_encoding n h p) … memb)
 109 #p1 * #Hmem #H @(ex_intro … p1) % /2/
 110 qed.
 111
 112 lemma match_to_trans:
 113   ∀n.∀trans: trans_source n → trans_target n.
 114   ∀h,qin,cin,qout,cout,mv.
 115   match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_list n h (graph_enum ?? trans))) →
 116   ∃s,t. tuple_encoding n h 〈s,t〉 = mk_tuple qin cin qout cout mv
 117     ∧ trans s = t.
 118 #n #trans #h #qin #cin #qout #cout #mv #Hmatch
 119 cases (match_to_tuple … Hmatch) -Hmatch * #s #t * #Heq #Hmem
 120 @(ex_intro … s) @(ex_intro … t) % // @graph_enum_correct
 121 @mem_to_memb @Hmem
 122 qed.
 123
 124 lemma trans_to_match:
 125   ∀n.∀h.∀trans: trans_source n → trans_target n.
 126   ∀s,t,qin,cin,qout,cout,mv. trans s = t →
 127   tuple_encoding n h 〈s,t〉 = mk_tuple qin cin qout cout mv →
 128   match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_list n h (graph_enum ?? trans))).
 129 #n #h #trans #inp #outp #qin #cin #qout #cout #mv #Htrans #Htuple
 130 @(tuple_to_match … (refl…)) <Htuple @mem_map_forward
 131 @(memb_to_mem (FinProd (trans_source n) (trans_target n)))
 132 @graph_enum_complete //
 133 qed.
 134
 135 (*
 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
 146 lemma list_decompose_r :
 147   ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → memb A a l3 = false →
 148   ∃la,lb.l1 = la@lb ∧ l4 = lb@a::l2.
 149 #A #l1 #l2 #l3 generalize in match l1; generalize in match l2; elim l3
 150   [normalize #l1 #l2 #l4 #a #H #_ @(ex_intro … []) @(ex_intro … l2) /2/
 151   |#b #tl #Hind #l1 #l2 #l4 #a cases l2
 152     [normalize #Heq destruct >(\b (refl … b)) normalize #Hfalse destruct
 153     |#c #tl2 whd in ⊢ ((??%%)→?); #Heq destruct #Hmema
 154      cases (Hind l1 tl2 l4 a ??)
 155       [#l5 * #l6 * #eql #eql4
 156        @(ex_intro … (b::l5)) @(ex_intro … l6) % /2/
 157       |@e0
 158       |cases (true_or_false (memb ? a tl)) [2://]
 159        #H @False_ind @(absurd ?? not_eq_true_false)
 160        <Hmema @sym_eq @memb_cons //
 161       ]
 162     ]
 163   ]
 164 qed.
 165
 166 (*axiom list_decompose_memb :
 167   ∀A,l1,l2,l3,l4,a.l1@a::l2 = l3@l4 → |l1| < |l3| → memb A a l3 = true.*)
 168
 169 lemma table_invert_r : ∀n,t,T.
 170   tuple_TM n t → table_TM n (t@T) → table_TM n T.
 171 #n #t #T #Htuple #Htable inversion Htable
 172 [ cases Htuple #qin * #cin * #qout * #cout * #mv * #_ #Ht >Ht
 173   normalize #Hfalse destruct (Hfalse)
 174 | #t0 #T0 #Htuple0 #Htable0 #_ #Heq
 175   lapply (append_l2_injective ?????? Heq)
 176   [ >(length_of_tuple … Htuple) >(length_of_tuple … Htuple0) % ]
 177   -Heq #Heq destruct (Heq) // ]
 178 qed.
 179
 180 lemma match_in_table_to_tuple :
 181   ∀n,T,qin,cin,qout,cout,mv.
 182   match_in_table n qin cin qout cout mv T → table_TM n T →
 183   tuple_TM n (mk_tuple qin cin qout cout mv).
 184 #n #T #qin #cin #qout #cout #mv #Hmatch elim Hmatch
 185 [ //
 186 | #qin0 #cin0 #qout0 #cout0 #mv0 #tb #Htuple #Hmatch #IH #Htable
 187   @IH @(table_invert_r ???? Htable) @Htuple
 188 ]
 189 qed.
 190
 191 lemma match_in_table_append :
 192   ∀n,T,qin,cin,qout,cout,mv,t.
 193   tuple_TM n t →
 194   match_in_table n qin cin qout cout mv (t@T) →
 195   t = mk_tuple qin cin qout cout mv ∨ match_in_table n qin cin qout cout mv T.
 196 #n #T #qin #cin #qout #cout #mv #t #Ht #Hmatch inversion Hmatch
 197 [ #T0 #H #H1 % >(append_l1_injective … H1) //
 198   >(length_of_tuple … Ht) >(length_of_tuple … H) %
 199 | #qin0 #cin0 #qout0 #cout0 #mv0 #T0 #H #H1 #_ #H2 %2
 200   >(append_l2_injective … H2) // >(length_of_tuple … Ht) >(length_of_tuple … H) %
 201 ]
 202 qed.
 203
 204 lemma generic_match_to_match_in_table_tech :
 205   ∀n,t,T0,T1,T2.tuple_TM n t → table_TM n (T1@〈bar,false〉::T2) →
 206    t@T0 = T1@〈bar,false〉::T2 → T1 = [] ∨ ∃T3.T1 = t@T3.
 207 #n #t #T0 #T1 #T2 #Ht cases T1
 208 [ #_ #_ % %
 209 | normalize #c #T1c #Htable #Heq %2
 210   cases Ht in Heq; #qin * #cin * #qout * #cout * #mv **********
 211   #Hqin1 #Hqout1 #Hqin2 #Hqout2 #Hcin #Hcout #Hmv #Hcoutmv #Hqinlen #Hqoutlen
 212   #Heqt >Heqt whd in ⊢ (??%%→?); #Ht lapply (cons_injective_r ????? Ht)
 213   #Ht' cases (list_decompose_r STape … (sym_eq … Ht') ?)
 214   [ #la * #lb * #HT1c #HT0 %{lb} >HT1c @(eq_f2 ??? (append ?) (c::la)) //
 215     >HT0 in Ht'; >HT1c >associative_append in ⊢ (???%→?); #Ht'
 216     <(append_l1_injective_r … Ht') // <(cons_injective_l ????? Ht) %
 217   |@(noteq_to_eqnot ? true) @(not_to_not … not_eq_true_false) #Hbar @sym_eq
 218    cases (memb_append … Hbar) -Hbar #Hbar
 219     [@(Hqin2 … Hbar)
 220     |cases (orb_true_l … Hbar) -Hbar
 221       [#Hbar lapply (\P Hbar) -Hbar #Hbar destruct (Hbar) @Hcin
 222       |whd in ⊢ ((??%?)→?); #Hbar cases (memb_append … Hbar) -Hbar #Hbar
 223         [@(Hqout2 … Hbar)
 224         |cases (orb_true_l … Hbar) -Hbar
 225           [#Hbar lapply (\P Hbar) -Hbar #Hbar destruct (Hbar) @Hcout
 226           |#Hbar cases (orb_true_l … Hbar) -Hbar
 227             [whd in ⊢ ((??%?)→?); #Hbar @Hbar
 228             |#Hbar lapply (memb_single … Hbar) -Hbar #Hbar destruct (Hbar) @Hmv
 229             ]
 230           ]
 231         ]
 232       ]
 233     ]
 234   ]
 235 qed.
 236
 237 lemma generic_match_to_match_in_table :
 238   ∀n,T.table_TM n T →
 239   ∀qin,cin,qout,cout,mv.|qin| = n → |qout| = n →
 240   only_bits qin → only_bits qout →
 241   bit_or_null (\fst cin) = true → bit_or_null (\fst cout) = true →
 242   bit_or_null (\fst mv) = true →
 243   ∀t1,t2.
 244   T = (t1@〈bar,false〉::qin@cin::〈comma,false〉::qout@cout::〈comma,false〉::[mv])@t2 →
 245   match_in_table n qin cin qout cout mv T.
 246 #n #T #Htable #qin #cin #qout #cout #mv #Hlenqin #Hlenqout
 247 #Hqinbits #Hqoutbits #Hcin #Hcout #Hmv
 248 elim Htable
 249 [ * [ #t2 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
 250     | #c0 #t1 #t2 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
 251 | #tuple #T0 #H1 #Htable0#IH #t1 #t2 #HT cases H1 #qin0 * #cin0 * #qout0 * #cout0 * #mv0
 252   * * * * * * * * * *
 253   #Hqin0marks #Hqout0marks #Hqin0bits #Hqout0bits #Hcin0 #Hcout0 #Hmv0 #Hcout0mv0
 254   #Hlenqin0 #Hlenqout0 #Htuple
 255   lapply (generic_match_to_match_in_table_tech n ? T0 t1
 256            (qin@cin::〈comma,false〉::qout@[cout;〈comma,false〉;mv]@t2) H1) #Htmp
 257   >Htuple in H1; #H1
 258   lapply (ttm_cons … T0 H1 Htable0) <Htuple in ⊢ (%→?); >HT
 259   >associative_append normalize >associative_append normalize
 260   >associative_append #Htable cases (Htmp Htable ?)
 261   [ #Ht1 >Htuple in HT; >Ht1 normalize in ⊢ (??%%→?);
 262     >associative_append >associative_append #HT
 263     cut (qin0 = qin ∧ (〈cin0,false〉 = cin ∧ (qout0 = qout ∧
 264          (〈cout0,false〉 = cout ∧ (〈mv0,false〉 = mv ∧ T0 = t2)))))
 265     [ lapply (cons_injective_r ????? HT) -HT #HT
 266       lapply (append_l1_injective … HT) [ >Hlenqin @Hlenqin0 ]
 267       #Hqin % [ @Hqin ] -Hqin
 268       lapply (append_l2_injective … HT) [ >Hlenqin @Hlenqin0 ] -HT #HT
 269       lapply (cons_injective_l ????? HT) #Hcin % [ @Hcin ] -Hcin
 270       lapply (cons_injective_r ????? HT) -HT #HT
 271       lapply (cons_injective_r ????? HT) -HT
 272       >associative_append >associative_append #HT
 273       lapply (append_l1_injective … HT) [ >Hlenqout @Hlenqout0 ]
 274       #Hqout % [ @Hqout ] -Hqout
 275       lapply (append_l2_injective … HT) [ >Hlenqout @Hlenqout0 ] -HT normalize #HT
 276       lapply (cons_injective_l ????? HT) #Hcout % [ @Hcout ] -Hcout
 277       lapply (cons_injective_r ????? HT) -HT #HT
 278       lapply (cons_injective_r ????? HT) -HT #HT
 279       lapply (cons_injective_l ????? HT) #Hmv % [ @Hmv ] -Hmv
 280       @(cons_injective_r ????? HT) ]
 281     -HT * #Hqin * #Hcin * #Hqout * #Hcout * #Hmv #HT0
 282     >(?:〈bar,false〉::qin0@(〈cin0,false〉::〈comma,false〉::qout0@
 283         [〈cout0,false〉;〈comma,false〉;〈mv0,false〉])@T0 = tuple@T0)
 284     [ >Htuple >Hqin >Hqout >Hcin >Hcout >Hmv % //
 285     | >Htuple normalize >associative_append normalize >associative_append
 286       normalize >associative_append % ]
 287   | * #T3 #HT3 >HT3 in HT; >associative_append; >associative_append #HT
 288     lapply (append_l2_injective … HT) // -HT #HT %2 //
 289     @(IH T3 t2) >HT >associative_append %
 290   |>HT >associative_append normalize >associative_append normalize
 291    >associative_append % ]
 292 ]
 293 qed.