matita/matita/lib/turing/universal/universal.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 include "turing/universal/uni_step.ma".
  14
  15 (* definition zero : ∀n.initN n ≝ λn.mk_Sig ?? 0 (le_O_n n). *)
  16
  17 definition low_config: ∀M:normalTM.nconfig (no_states M) → tape STape ≝
  18 λM:normalTM.λc.
  19   let n ≝ no_states M in
  20   let h ≝ nhalt M in
  21   let t ≝ntrans M in
  22   let q ≝ cstate … c in
  23   let q_low ≝  m_bits_of_state n h q in
  24   let current_low ≝ match current … (ctape … c) with [ None ⇒ null | Some b ⇒ bit b] in
  25   let low_left ≝ map … (λb.〈bit b,false〉) (left … (ctape …c)) in
  26   let low_right ≝ map … (λb.〈bit b,false〉) (right … (ctape …c)) in
  27   let table ≝ flatten ? (tuples_list n h (graph_enum ?? t)) in
  28   let right ≝ q_low@〈current_low,false〉::〈grid,false〉::table@〈grid,false〉::low_right in
  29   mk_tape STape (〈grid,false〉::low_left) (option_hd … right) (tail … right).
  30
  31 lemma low_config_eq: ∀t,M,c. t = low_config M c →
  32   ∃low_left,low_right,table,q_low_hd,q_low_tl,c_low.
  33   low_left = map … (λb.〈bit b,false〉) (left … (ctape …c)) ∧
  34   low_right = map … (λb.〈bit b,false〉) (right … (ctape …c)) ∧
  35   table = flatten ? (tuples_list (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) ∧
  36   〈q_low_hd,false〉::q_low_tl = m_bits_of_state (no_states M) (nhalt M) (cstate … c) ∧
  37   c_low =  match current … (ctape … c) with [ None ⇒ null| Some b ⇒ bit b] ∧
  38   t = midtape STape (〈grid,false〉::low_left) 〈q_low_hd,false〉 (q_low_tl@〈c_low,false〉::〈grid,false〉::table@〈grid,false〉::low_right).
  39 #t #M #c #eqt
  40   @(ex_intro … (map … (λb.〈bit b,false〉) (left … (ctape …c))))
  41   @(ex_intro … (map … (λb.〈bit b,false〉) (right … (ctape …c))))
  42   @(ex_intro … (flatten ? (tuples_list (no_states M) (nhalt M) (graph_enum ?? (ntrans M)))))
  43   @(ex_intro … (\fst (hd ? (m_bits_of_state (no_states M) (nhalt M) (cstate … c)) 〈bit true,false〉)))
  44   @(ex_intro … (tail ? (m_bits_of_state (no_states M) (nhalt M) (cstate … c))))
  45   @(ex_intro … (match current … (ctape … c) with [ None ⇒ null| Some b ⇒ bit b]))
  46 % [% [% [% [% // | // ] | // ] | // ] | >eqt //]
  47 qed.
  48
  49 let rec to_bool_list (l: list (unialpha×bool)) ≝
  50   match l with
  51   [ nil ⇒ nil ?
  52   | cons a tl ⇒
  53     match \fst a with
  54     [bit b ⇒ b::to_bool_list tl
  55     |_ ⇒ nil ?
  56     ]
  57   ].
  58
  59 definition high_c ≝ λc:unialpha×bool.
  60   match \fst c with
  61   [ null ⇒ None ?
  62   | bit b ⇒ Some ? b
  63   | _ ⇒ None ?].
  64
  65 definition high_tape ≝ λls,c,rs.
  66   mk_tape FinBool (to_bool_list ls) (high_c c) (to_bool_list rs).
  67
  68 lemma high_tape_eq : ∀ls,c,rs. high_tape ls c rs =
  69   mk_tape FinBool (to_bool_list ls) (high_c c) (to_bool_list rs).
  70 // qed.
  71
  72 definition high_tape_from_tape ≝ λt:tape STape.
  73   match t with
  74   [niltape ⇒ niltape ?
  75   |leftof a l ⇒ match \fst a with
  76      [bit b ⇒ leftof ? b (to_bool_list l)
  77      |_ ⇒ niltape ?
  78      ]
  79   |rightof a r ⇒ match \fst a with
  80      [bit b ⇒ rightof ? b (to_bool_list r)
  81      |_ ⇒ niltape ?
  82      ]
  83   |midtape l c r ⇒ high_tape l c r
  84   ].
  85
  86 lemma high_tape_of_lift : ∀ls,c,rs. legal_tape ls c rs →
  87   high_tape ls c rs =
  88     high_tape_from_tape (lift_tape ls c rs).
  89 #ls * #c #b #rs * #H cases c //
  90 >high_tape_eq
  91 * [ * [#H @False_ind /2/
  92       | #Heq >Heq cases rs // * #a #b1 #tl
  93         whd in match (lift_tape ???); cases a //
  94       ]
  95   |#Heq >Heq cases ls // * #a #b1 #tl
  96         whd in match (lift_tape ???); cases a //
  97   ]
  98 qed.
  99
 100 lemma bool_embedding: ∀l.
 101   to_bool_list (map ?? (λb.〈bit b,false〉) l) = l.
 102 #l elim l // #a #tl #Hind normalize @eq_f @Hind
 103 qed.
 104
 105 lemma current_embedding: ∀c.
 106   high_c (〈match c with [None ⇒ null | Some b ⇒ bit b],false〉) = c.
 107   * normalize // qed.
 108
 109 lemma tape_embedding: ∀ls,c,rs.
 110  high_tape
 111    (map ?? (λb.〈bit b,false〉) ls)
 112    (〈match c with [None ⇒ null | Some b ⇒ bit b],false〉)
 113    (map ?? (λb.〈bit b,false〉) rs) = mk_tape ? ls c rs.
 114 #ls #c #rs >high_tape_eq >bool_embedding >bool_embedding
 115 >current_embedding %
 116 qed.
 117
 118 definition high_move ≝ λc,mv.
 119   match c with
 120   [ bit b ⇒ Some ? 〈b,move_of_unialpha mv〉
 121   | _ ⇒ None ?
 122   ].
 123
 124 (* lemma high_of_lift ≝ ∀ls,c,rs.
 125   high_tape ls c rs = *)
 126
 127 definition map_move ≝
 128   λc,mv.match c with [ null ⇒ None ? | _ ⇒ Some ? 〈c,false,move_of_unialpha mv〉 ].
 129
 130 (* axiom high_tape_move : ∀t1,ls,c,rs, c1,mv.
 131   legal_tape ls c rs →
 132   t1 = lift_tape ls c rs →
 133   high_tape_from_tape (tape_move STape t1 (map_move c1 mv)) =
 134     tape_move FinBool (high_tape_from_tape t1) (high_move c1 mv). *)
 135
 136 definition low_step_R_true ≝ λt1,t2.
 137   ∀M:normalTM.
 138   ∀c: nconfig (no_states M).
 139     t1 = low_config M c →
 140     halt ? M (cstate … c) = false ∧
 141       t2 = low_config M (step ? M c).
 142
 143 definition low_tape_aux : ∀M:normalTM.tape FinBool → tape STape ≝
 144 λM:normalTM.λt.
 145   let current_low ≝ match current … t with
 146     [ None ⇒ None ? | Some b ⇒ Some ? 〈bit b,false〉] in
 147   let low_left ≝ map … (λb.〈bit b,false〉) (left … t) in
 148   let low_right ≝ map … (λb.〈bit b,false〉) (right … t) in
 149   mk_tape STape low_left current_low low_right.
 150
 151 lemma left_of_low_tape: ∀M,t.
 152   left ? (low_tape_aux M t) = map … (λb.〈bit b,false〉) (left … t).
 153 #M * //
 154 qed.
 155
 156 lemma right_of_low_tape: ∀M,t.
 157   right ? (low_tape_aux M t) = map … (λb.〈bit b,false〉) (right … t).
 158 #M * //
 159 qed.
 160
 161 definition low_move ≝ λaction:option (bool × move).
 162   match action with
 163   [None ⇒ None ?
 164   |Some act ⇒ Some ? (〈〈bit (\fst act),false〉,\snd act〉)].
 165
 166 (* simulation lemma *)
 167 lemma low_tape_move : ∀M,action,t.
 168   tape_move STape (low_tape_aux M t) (low_move action) =
 169   low_tape_aux M (tape_move FinBool t action).
 170 #M * // (* None *)
 171 * #b #mv #t cases mv cases t //
 172   [#ls #c #rs cases ls //|#ls #c #rs cases rs //]
 173 qed.
 174
 175 lemma left_of_lift: ∀ls,c,rs. left ? (lift_tape ls c rs) = ls.
 176 #ls * #c #b #rs cases c // cases ls // cases rs //
 177 qed.
 178
 179 lemma right_of_lift: ∀ls,c,rs. legal_tape ls c rs →
 180   right ? (lift_tape ls c rs) = rs.
 181 #ls * #c #b #rs * #_ cases c // cases ls cases rs // #a #tll #b #tlr
 182 #H @False_ind cases H [* [#H1 /2/ |#H1 destruct] |#H1 destruct]
 183 qed.
 184
 185
 186 lemma current_of_lift: ∀ls,c,b,rs. legal_tape ls 〈c,b〉 rs →
 187   current STape (lift_tape ls 〈c,b〉 rs) =
 188     match c with [null ⇒ None ? | _ ⇒ Some ? 〈c,b〉].
 189 #ls #c #b #rs cases c // whd in ⊢ (%→?); * #_
 190 * [* [#Hnull @False_ind /2/ | #Hls >Hls whd in ⊢ (??%%); cases rs //]
 191   |#Hrs >Hrs whd in ⊢ (??%%); cases ls //]
 192 qed.
 193
 194 lemma current_of_lift_None: ∀ls,c,b,rs. legal_tape ls 〈c,b〉 rs →
 195   current STape (lift_tape ls 〈c,b〉 rs) = None ? →
 196     c = null.
 197 #ls #c #b #rs #Hlegal >(current_of_lift … Hlegal) cases c normalize
 198   [#b #H destruct |// |3,4,5:#H destruct ]
 199 qed.
 200
 201 lemma current_of_lift_Some: ∀ls,c,c1,rs. legal_tape ls c rs →
 202   current STape (lift_tape ls c rs) = Some ? c1 →
 203     c = c1.
 204 #ls * #c #cb #b #rs #Hlegal >(current_of_lift … Hlegal) cases c normalize
 205  [#b1 #H destruct // |#H destruct |3,4,5:#H destruct //]
 206 qed.
 207
 208 lemma current_of_low_None: ∀M,t. current FinBool t = None ? →
 209   current STape (low_tape_aux M t) = None ?.
 210 #M #t cases t // #l #b #r whd in ⊢ ((??%?)→?); #H destruct
 211 qed.
 212
 213 lemma current_of_low_Some: ∀M,t,b. current FinBool t = Some ? b →
 214   current STape (low_tape_aux M t) = Some ? 〈bit b,false〉.
 215 #M #t cases t
 216   [#b whd in ⊢ ((??%?)→?); #H destruct
 217   |#b #l #b1 whd in ⊢ ((??%?)→?); #H destruct
 218   |#b #l #b1 whd in ⊢ ((??%?)→?); #H destruct
 219   |#c #c1 #l #r whd in ⊢ ((??%?)→?); #H destruct %
 220   ]
 221 qed.
 222
 223 lemma current_of_low:∀M,tape,ls,c,rs. legal_tape ls c rs →
 224   lift_tape ls c rs = low_tape_aux M tape →
 225   c = 〈match current … tape  with
 226        [ None ⇒ null | Some b ⇒ bit b], false〉.
 227 #M #tape #ls * #c #cb #rs #Hlegal #Hlift
 228 cut (current ? (lift_tape ls 〈c,cb〉 rs) = current ? (low_tape_aux M tape))
 229   [@eq_f @Hlift] -Hlift #Hlift
 230 cut (current … tape = None ? ∨ ∃b.current … tape = Some ? b)
 231   [cases (current … tape) [%1 // | #b1 %2 /2/ ]] *
 232   [#Hcurrent >Hcurrent normalize
 233    >(current_of_low_None …Hcurrent) in Hlift; #Hlift
 234    >(current_of_lift_None … Hlegal Hlift)
 235    @eq_f cases Hlegal * * #Hmarks #_ #_ #_ @(Hmarks 〈c,cb〉) @memb_hd
 236   |* #b #Hcurrent >Hcurrent normalize
 237    >(current_of_low_Some …Hcurrent) in Hlift; #Hlift
 238    @(current_of_lift_Some … Hlegal Hlift)
 239   ]
 240 qed.
 241
 242 (*
 243 lemma current_of_low:∀M,tape,ls,c,rs. legal_tape ls c rs →
 244   lift_tape ls c rs = low_tape_aux M tape →
 245   c = 〈match current … tape  with
 246        [ None ⇒ null | Some b ⇒ bit b], false〉.
 247 #M #tape #ls * #c #cb #rs * * #_ #H cases (orb_true_l … H)
 248   [cases c [2,3,4,5: whd in ⊢ ((??%?)→?); #Hfalse destruct]
 249    #b #_ #_ cases tape
 250     [whd in ⊢ ((??%%)→?); #H destruct
 251     |#a #l whd in ⊢ ((??%%)→?); #H destruct
 252     |#a #l whd in ⊢ ((??%%)→?); #H destruct
 253     |#a #l #r whd in ⊢ ((??%%)→?); #H destruct //
 254     ]
 255   |cases c
 256     [#b whd in ⊢ ((??%?)→?); #Hfalse destruct
 257     |3,4,5:whd in ⊢ ((??%?)→?); #Hfalse destruct]
 258    #_ * [* [#Habs @False_ind /2/
 259            |#Hls >Hls whd in ⊢ ((??%%)→?); *)
 260
 261
 262 (* sufficent conditions to have a low_level_config *)
 263 lemma is_low_config: ∀ls,c,rs,M,s,tape,qhd,q_tl,table.
 264 legal_tape ls c rs →
 265 table = flatten ? (tuples_list (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) →
 266 lift_tape ls c rs = low_tape_aux M tape →
 267 〈qhd,false〉::q_tl = m_bits_of_state (no_states M) (nhalt M) s →
 268 midtape STape (〈grid,false〉::ls)
 269   〈qhd,false〉
 270   (q_tl@c::〈grid,false〉::table@〈grid,false〉::rs) =
 271   low_config M (mk_config ?? s tape).
 272 #ls #c #rs #M #s #tape #qhd #q_tl #table #Hlegal #Htable
 273 #Hlift #Hstate whd in match (low_config ??); <Hstate
 274 @eq_f3
 275   [@eq_f <(left_of_lift ls c rs) >Hlift //
 276   | cut (∀A.∀a,b:A.∀l1,l2. a::l1 = b::l2 → a=b)
 277     [#A #a #b #l1 #l2 #H destruct (H) %] #Hcut
 278    @(Hcut …Hstate)
 279   |@eq_f <(current_of_low … Hlegal Hlift) @eq_f @eq_f <Htable @eq_f @eq_f
 280    <(right_of_lift ls c rs Hlegal) >Hlift @right_of_low_tape
 281   ]
 282 qed.
 283
 284 lemma unistep_to_low_step: ∀t1,t2.
 285   R_uni_step_true t1 t2 → low_step_R_true t1 t2.
 286 #t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step * #n #posn #t #h * #qin #tape #eqt1
 287 cases (low_config_eq … eqt1)
 288 #low_left * #low_right * #table * #q_low_hd * #q_low_tl * #current_low
 289 ***** #Hlow_left #Hlow_right #Htable #Hq_low #Hcurrent_low #Ht1
 290 letin trg ≝ (t 〈qin,current ? tape〉)
 291 letin qout_low ≝ (m_bits_of_state n h (\fst trg))
 292 letin qout_low_hd ≝ (hd ? qout_low 〈bit true,false〉)
 293 letin qout_low_tl ≝ (tail ? qout_low)
 294 letin low_act ≝ (low_action (\snd (t 〈qin,current ? tape〉)))
 295 letin low_cout ≝ (\fst low_act)
 296 letin low_m ≝ (\snd low_act)
 297 lapply (Huni_step n table q_low_hd (\fst qout_low_hd)
 298        current_low low_cout low_left low_right q_low_tl qout_low_tl low_m … Ht1)
 299   [@daemon
 300   |>Htable
 301    @(trans_to_match n h t 〈qin,current ? tape〉 … (refl …))
 302    >Hq_low  >Hcurrent_low whd in match (mk_tuple ?????);
 303    >(eq_pair_fst_snd … (t …)) whd in ⊢ (??%?);
 304    >(eq_pair_fst_snd … (low_action …)) %
 305   |//
 306   |@daemon
 307   ]
 308 -Ht1 #Huni_step lapply (Huni_step ? (refl …)) -Huni_step *
 309 #q_low_head_false * #ls1 * #rs1 * #c2 * *
 310 #Ht2 #Hlift #Hlegal %
 311   [whd in ⊢ (??%?); >q_low_head_false in Hq_low;
 312    whd in ⊢ ((???%)→?); generalize in match (h qin);
 313    #x #H destruct (H) %
 314   |>Ht2 whd in match (step FinBool ??);
 315    whd in match (trans ???);
 316    >(eq_pair_fst_snd … (t ?))
 317    @is_low_config // >Hlift
 318    <low_tape_move @eq_f2
 319     [>Hlow_left >Hlow_right >Hcurrent_low whd in ⊢ (??%%);
 320      cases (current …tape) [%] #b whd in ⊢ (??%%); %
 321     |whd in match low_cout; whd in match low_m; whd in match low_act;
 322      generalize in match (\snd (t ?)); * [%] * #b #mv
 323      whd in  ⊢ (??(?(???%)?)%); cases mv %
 324     ]
 325   ]
 326 qed.
 327
 328 definition low_step_R_false ≝ λt1,t2.
 329   ∀M:normalTM.
 330   ∀c: nconfig (no_states M).
 331     t1 = low_config M c → halt ? M (cstate … c) = true  ∧ t1 = t2.
 332
 333 definition low_R ≝ λM,qstart,R,t1,t2.
 334     ∀tape1. t1 = low_config M (mk_config ?? qstart tape1) →
 335     ∃q,tape2.R tape1 tape2 ∧
 336     halt ? M q = true ∧ t2 = low_config M (mk_config ?? q tape2).
 337
 338 definition R_TM ≝ λsig.λM:TM sig.λq.λt1,t2.
 339 ∃i,outc.
 340   loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (mk_config ?? q t1) = Some ? outc ∧
 341   t2 = (ctape ?? outc).
 342
 343 (*
 344 definition universal_R ≝ λM,R,t1,t2.
 345     Realize ? M R →
 346     ∀tape1,tape2.
 347     R tape1 tape 2 ∧
 348     t1 = low_config M (initc ? M tape1) ∧
 349     ∃q.halt ? M q = true → t2 = low_config M (mk_config ?? q tape2).*)
 350
 351 axiom uni_step: TM STape.
 352 axiom us_acc: states ? uni_step.
 353
 354 axiom sem_uni_step: accRealize ? uni_step us_acc low_step_R_true low_step_R_false.
 355
 356 definition universalTM ≝ whileTM ? uni_step us_acc.
 357
 358 theorem sem_universal: ∀M:normalTM. ∀qstart.
 359   WRealize ? universalTM (low_R M qstart (R_TM FinBool M qstart)).
 360 #M #q #intape #i #outc #Hloop
 361 lapply (sem_while … sem_uni_step intape i outc Hloop)
 362   [@daemon] -Hloop
 363 * #ta * #Hstar generalize in match q; -q
 364 @(star_ind_l ??????? Hstar)
 365   [#tb #q0 whd in ⊢ (%→?); #Htb #tape1 #Htb1
 366    cases (Htb … Htb1) -Htb #Hhalt #Htb
 367    <Htb >Htb1 @ex_intro
 368    [|%{tape1} %
 369      [ %
 370        [ whd @(ex_intro … 1) @(ex_intro … (mk_config … q0 tape1))
 371         % [|%] whd in ⊢ (??%?); >Hhalt %
 372        | @Hhalt ]
 373      | % ]
 374    ]
 375   |#tb #tc #td whd in ⊢ (%→?); #Htc #Hstar1 #IH
 376    #q #Htd #tape1 #Htb
 377    lapply (IH (\fst (trans ? M 〈q,current ? tape1〉)) Htd) -IH
 378    #IH cases (Htc … Htb); -Htc #Hhaltq
 379    whd in match (step FinBool ??); >(eq_pair_fst_snd ?? (trans ???))
 380    #Htc change with (mk_config ????) in Htc:(???(??%));
 381    cases (IH ? Htc) #q1 * #tape2 * * #HRTM #Hhaltq1 #Houtc
 382    @(ex_intro … q1) @(ex_intro … tape2) %
 383     [%
 384       [cases HRTM #k * #outc1 * #Hloop #Houtc1
 385        @(ex_intro … (S k)) @(ex_intro … outc1) %
 386         [>loop_S_false [2://] whd in match (step FinBool ??);
 387          >(eq_pair_fst_snd ?? (trans ???)) @Hloop
 388         |@Houtc1
 389         ]
 390       |@Hhaltq1]
 391     |@Houtc
 392     ]
 393   ]
 394 qed.
 395
 396 lemma R_TM_to_R: ∀sig,M,R. ∀t1,t2.
 397   WRealize sig M R → R_TM ? M (start ? M) t1 t2 → R t1 t2.
 398 #sig #M #R #t1 #t2 whd in ⊢ (%→?); #HMR * #i * #outc *
 399 #Hloop #Ht2 >Ht2 @(HMR … Hloop)
 400 qed.
 401
 402 axiom WRealize_to_WRealize: ∀sig,M,R1,R2.
 403   (∀t1,t2.R1 t1 t2 → R2 t1 t2) → WRealize sig M R1 → WRealize ? M R2.
 404
 405 theorem sem_universal2: ∀M:normalTM. ∀R.
 406   WRealize ? M R → WRealize ? universalTM (low_R M (start ? M) R).
 407 #M #R #HMR lapply (sem_universal … M (start ? M)) @WRealize_to_WRealize
 408 #t1 #t2 whd in ⊢ (%→%); #H #tape1 #Htape1 cases (H ? Htape1)
 409 #q * #tape2 * * #HRTM #Hhalt #Ht2 @(ex_intro … q) @(ex_intro … tape2)
 410 % [% [@(R_TM_to_R … HRTM) @HMR | //] | //]
 411 qed.
 412