matita/matita/lib/turing/multi_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 include "turing/simple_machines.ma".
  13 include "turing/multi_universal/unistep_aux.ma".
  14
  15 axiom sem_unistep: ∀M. unistep ⊨ R_unistep_high M.
  16
  17 definition stop ≝ λc.
  18   match c with [ bit b ⇒ notb b | _ ⇒ true].
  19
  20 definition uni_body ≝
  21   ifTM ?? (mtestR ? cfg 2 stop)
  22     (single_finalTM ?? unistep)
  23     (nop …) (mtestR_acc ? cfg 2 stop).
  24
  25 definition acc_body : states ?? uni_body ≝ (inr … (inl … (inr … start_nop))).
  26
  27 definition ub_R_true ≝ λM,t1,t2.
  28   ∀c: nconfig (no_states M).
  29   t1=low_tapes M c→
  30     t2=low_tapes M (step FinBool M c) ∧ halt ? M (cstate … c) = false.
  31
  32 definition ub_R_false ≝ λM,t1,t2.
  33   ∀c: nconfig (no_states M).
  34   t1 = low_tapes M c → t1 = t2 ∧ halt ? M (cstate … c) = true.
  35
  36 lemma sem_uni_body: ∀M.
  37   uni_body ⊨ [acc_body: ub_R_true M, ub_R_false M].
  38 #M #cf
  39 @(acc_sem_if_app ????????????
  40    (sem_mtestR ? cfg 2 stop (le_S ?? (le_n 1)))
  41    (sem_unistep M)
  42    (sem_nop …))
  43 [#t1 #t2 #t3 whd in ⊢ (%→?); #Htest #Ht2 * #q #Mt #Ht1
  44  >Ht1 in Htest; >cfg_low_tapes whd in match (bits_of_state ???);
  45  #Htest lapply (Htest … (refl ??)) * <Ht1 #Ht3 #Hstop >Ht3 in Ht2;
  46  #Ht2 % [@Ht2 //] lapply Hstop  whd in match (nhalt ??);
  47  cases (nhalt M q) whd in match (stop ?); * /2/
  48 |#t1 #t2 #t3 whd in ⊢ (%→?); #Htest #Hnop >Hnop -Hnop * #q #Mt #Ht1 >Ht1 in Htest;
  49  >cfg_low_tapes whd in match (bits_of_state ???);
  50  #Htest lapply (Htest … (refl ??)) whd in match (nhalt ??);
  51  cases (nhalt M q) whd in match (stop ?); * /2/
  52 ]
  53 qed.
  54
  55 definition universalTM ≝ whileTM ?? uni_body acc_body.
  56
  57 definition low_R ≝ λM,q,R.λt1,t2:Vector (tape FSUnialpha) 3.
  58     ∀Mt. t1 = low_tapes M (mk_config ?? q Mt) →
  59     ∃cout. R Mt (ctape … cout) ∧
  60     halt ? M (cstate … cout) = true ∧ t2 = low_tapes M cout.
  61
  62 theorem sem_universal: ∀M:normalTM. ∀q.
  63   universalTM ⊫ low_R M q (R_TM FinBool M q).
  64 #M #q #intape #i #outc #Hloop
  65 lapply (sem_while … (sem_uni_body M … ) intape i outc Hloop) [%] -Hloop
  66 * #ta * #Hstar lapply q -q @(star_ind_l ??????? Hstar) -Hstar
  67   [#q whd in ⊢ (%→?); #HFalse whd #Mt #Hta
  68    lapply (HFalse … Hta) * #Hta1 #Hhalt %{(mk_config ?? q Mt)} %
  69     [%[%{1} %{(mk_config ?? q Mt)} % // whd in ⊢ (??%?); >Hhalt % |@Hhalt]
  70     |<Hta1 @Hta
  71     ]
  72   |#t1 #t2 whd in ⊢ (%→?); #Hstep #Hstar #IH #q #Hta whd #Mt #Ht1
  73    lapply (Hstep … Ht1) * -Hstep #Ht2 #Hhalt
  74    lapply(IH (cstate … (step FinBool M (mk_config ?? q Mt))) Hta ??) [@Ht2|skip] -IH
  75    * #cout * * #HRTM #Hhalt1 #Houtc
  76    %{cout}
  77    %[%[cases HRTM #k * #outc1 * <config_expand #Hloop #Houtc1
  78        %{(S k)} %{outc1} %
  79         [whd in ⊢ (??%?); >Hhalt whd in ⊢ (??%?); @Hloop
  80         |@Houtc1
  81         ]
  82       |@Hhalt1]
  83     |@Houtc
  84     ]
  85   ]
  86 qed.
  87
  88 theorem sem_universal2: ∀M:normalTM. ∀R.
  89   M ⊫ R → universalTM ⊫ (low_R M (start ? M) R).
  90 #M #R #HMR lapply (sem_universal … M (start ? M)) @WRealize_to_WRealize
  91 #t1 #t2 whd in ⊢ (%→%); #H #tape1 #Htape1 cases (H ? Htape1)
  92 #c * * #HRTM #Hhalt #Ht2 %{c}
  93 % [% [@(R_TM_to_R … HRTM) @HMR | //] | //]
  94 qed.
  95
  96 axiom terminate_UTM: ∀M:normalTM.∀t.
  97   M ↓ t → universalTM ↓ (low_tapes M (mk_config ?? (start ? M) t)).
  98
  99
 100
 101
 102
 103
 104
 105
 106 lemma current_embedding: ∀c.
 107   high_c (〈match c with [None ⇒ null | Some b ⇒ bit b],false〉) = c.
 108   * normalize // qed.
 109
 110 lemma tape_embedding: ∀ls,c,rs.
 111  high_tape
 112    (map ?? (λb.〈bit b,false〉) ls)
 113    (〈match c with [None ⇒ null | Some b ⇒ bit b],false〉)
 114    (map ?? (λb.〈bit b,false〉) rs) = mk_tape ? ls c rs.
 115 #ls #c #rs >high_tape_eq >bool_embedding >bool_embedding
 116 >current_embedding %
 117 qed.
 118
 119 definition high_move ≝ λc,mv.
 120   match c with
 121   [ bit b ⇒ Some ? 〈b,move_of_unialpha mv〉
 122   | _ ⇒ None ?
 123   ].
 124
 125 definition map_move ≝
 126   λc,mv.match c with [ null ⇒ None ? | _ ⇒ Some ? 〈c,false,move_of_unialpha mv〉 ].
 127
 128 definition low_step_R_true ≝ λt1,t2.
 129   ∀M:normalTM.
 130   ∀c: nconfig (no_states M).
 131     t1 = low_config M c →
 132     halt ? M (cstate … c) = false ∧
 133       t2 = low_config M (step ? M c).
 134
 135 definition low_tape_aux : ∀M:normalTM.tape FinBool → tape STape ≝
 136 λM:normalTM.λt.
 137   let current_low ≝ match current … t with
 138     [ None ⇒ None ? | Some b ⇒ Some ? 〈bit b,false〉] in
 139   let low_left ≝ map … (λb.〈bit b,false〉) (left … t) in
 140   let low_right ≝ map … (λb.〈bit b,false〉) (right … t) in
 141   mk_tape STape low_left current_low low_right.
 142
 143 lemma left_of_low_tape: ∀M,t.
 144   left ? (low_tape_aux M t) = map … (λb.〈bit b,false〉) (left … t).
 145 #M * //
 146 qed.
 147
 148 lemma right_of_low_tape: ∀M,t.
 149   right ? (low_tape_aux M t) = map … (λb.〈bit b,false〉) (right … t).
 150 #M * //
 151 qed.
 152
 153 definition low_move ≝ λaction:option (bool × move).
 154   match action with
 155   [None ⇒ None ?
 156   |Some act ⇒ Some ? (〈〈bit (\fst act),false〉,\snd act〉)].
 157
 158 (* simulation lemma *)
 159 lemma low_tape_move : ∀M,action,t.
 160   tape_move STape (low_tape_aux M t) (low_move action) =
 161   low_tape_aux M (tape_move FinBool t action).
 162 #M * // (* None *)
 163 * #b #mv #t cases mv cases t //
 164   [#ls #c #rs cases ls //|#ls #c #rs cases rs //]
 165 qed.
 166
 167 lemma left_of_lift: ∀ls,c,rs. left ? (lift_tape ls c rs) = ls.
 168 #ls * #c #b #rs cases c // cases ls // cases rs //
 169 qed.
 170
 171 lemma right_of_lift: ∀ls,c,rs. legal_tape ls c rs →
 172   right ? (lift_tape ls c rs) = rs.
 173 #ls * #c #b #rs * #_ cases c // cases ls cases rs // #a #tll #b #tlr
 174 #H @False_ind cases H [* [#H1 /2/ |#H1 destruct] |#H1 destruct]
 175 qed.
 176
 177
 178 lemma current_of_lift: ∀ls,c,b,rs. legal_tape ls 〈c,b〉 rs →
 179   current STape (lift_tape ls 〈c,b〉 rs) =
 180     match c with [null ⇒ None ? | _ ⇒ Some ? 〈c,b〉].
 181 #ls #c #b #rs cases c // whd in ⊢ (%→?); * #_
 182 * [* [#Hnull @False_ind /2/ | #Hls >Hls whd in ⊢ (??%%); cases rs //]
 183   |#Hrs >Hrs whd in ⊢ (??%%); cases ls //]
 184 qed.
 185
 186 lemma current_of_lift_None: ∀ls,c,b,rs. legal_tape ls 〈c,b〉 rs →
 187   current STape (lift_tape ls 〈c,b〉 rs) = None ? →
 188     c = null.
 189 #ls #c #b #rs #Hlegal >(current_of_lift … Hlegal) cases c normalize
 190   [#b #H destruct |// |3,4,5:#H destruct ]
 191 qed.
 192
 193 lemma current_of_lift_Some: ∀ls,c,c1,rs. legal_tape ls c rs →
 194   current STape (lift_tape ls c rs) = Some ? c1 →
 195     c = c1.
 196 #ls * #c #cb #b #rs #Hlegal >(current_of_lift … Hlegal) cases c normalize
 197  [#b1 #H destruct // |#H destruct |3,4,5:#H destruct //]
 198 qed.
 199
 200 lemma current_of_low_None: ∀M,t. current FinBool t = None ? →
 201   current STape (low_tape_aux M t) = None ?.
 202 #M #t cases t // #l #b #r whd in ⊢ ((??%?)→?); #H destruct
 203 qed.
 204
 205 lemma current_of_low_Some: ∀M,t,b. current FinBool t = Some ? b →
 206   current STape (low_tape_aux M t) = Some ? 〈bit b,false〉.
 207 #M #t cases t
 208   [#b whd in ⊢ ((??%?)→?); #H destruct
 209   |#b #l #b1 whd in ⊢ ((??%?)→?); #H destruct
 210   |#b #l #b1 whd in ⊢ ((??%?)→?); #H destruct
 211   |#c #c1 #l #r whd in ⊢ ((??%?)→?); #H destruct %
 212   ]
 213 qed.
 214
 215 lemma current_of_low:∀M,tape,ls,c,rs. legal_tape ls c rs →
 216   lift_tape ls c rs = low_tape_aux M tape →
 217   c = 〈match current … tape  with
 218        [ None ⇒ null | Some b ⇒ bit b], false〉.
 219 #M #tape #ls * #c #cb #rs #Hlegal #Hlift
 220 cut (current ? (lift_tape ls 〈c,cb〉 rs) = current ? (low_tape_aux M tape))
 221   [@eq_f @Hlift] -Hlift #Hlift
 222 cut (current … tape = None ? ∨ ∃b.current … tape = Some ? b)
 223   [cases (current … tape) [%1 // | #b1 %2 /2/ ]] *
 224   [#Hcurrent >Hcurrent normalize
 225    >(current_of_low_None …Hcurrent) in Hlift; #Hlift
 226    >(current_of_lift_None … Hlegal Hlift)
 227    @eq_f cases Hlegal * * #Hmarks #_ #_ #_ @(Hmarks 〈c,cb〉) @memb_hd
 228   |* #b #Hcurrent >Hcurrent normalize
 229    >(current_of_low_Some …Hcurrent) in Hlift; #Hlift
 230    @(current_of_lift_Some … Hlegal Hlift)
 231   ]
 232 qed.
 233
 234 (*
 235 lemma current_of_low:∀M,tape,ls,c,rs. legal_tape ls c rs →
 236   lift_tape ls c rs = low_tape_aux M tape →
 237   c = 〈match current … tape  with
 238        [ None ⇒ null | Some b ⇒ bit b], false〉.
 239 #M #tape #ls * #c #cb #rs * * #_ #H cases (orb_true_l … H)
 240   [cases c [2,3,4,5: whd in ⊢ ((??%?)→?); #Hfalse destruct]
 241    #b #_ #_ cases tape
 242     [whd in ⊢ ((??%%)→?); #H destruct
 243     |#a #l whd in ⊢ ((??%%)→?); #H destruct
 244     |#a #l whd in ⊢ ((??%%)→?); #H destruct
 245     |#a #l #r whd in ⊢ ((??%%)→?); #H destruct //
 246     ]
 247   |cases c
 248     [#b whd in ⊢ ((??%?)→?); #Hfalse destruct
 249     |3,4,5:whd in ⊢ ((??%?)→?); #Hfalse destruct]
 250    #_ * [* [#Habs @False_ind /2/
 251            |#Hls >Hls whd in ⊢ ((??%%)→?); *)
 252
 253
 254 (* sufficent conditions to have a low_level_config *)
 255 lemma is_low_config: ∀ls,c,rs,M,s,tape,qhd,q_tl,table.
 256 legal_tape ls c rs →
 257 table = flatten ? (tuples_list (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) →
 258 lift_tape ls c rs = low_tape_aux M tape →
 259 〈qhd,false〉::q_tl = m_bits_of_state (no_states M) (nhalt M) s →
 260 midtape STape (〈grid,false〉::ls)
 261   〈qhd,false〉
 262   (q_tl@c::〈grid,false〉::table@〈grid,false〉::rs) =
 263   low_config M (mk_config ?? s tape).
 264 #ls #c #rs #M #s #tape #qhd #q_tl #table #Hlegal #Htable
 265 #Hlift #Hstate whd in match (low_config ??); <Hstate
 266 @eq_f3
 267   [@eq_f <(left_of_lift ls c rs) >Hlift //
 268   | cut (∀A.∀a,b:A.∀l1,l2. a::l1 = b::l2 → a=b)
 269     [#A #a #b #l1 #l2 #H destruct (H) %] #Hcut
 270    @(Hcut …Hstate)
 271   |@eq_f <(current_of_low … Hlegal Hlift) @eq_f @eq_f <Htable @eq_f @eq_f
 272    <(right_of_lift ls c rs Hlegal) >Hlift @right_of_low_tape
 273   ]
 274 qed.
 275
 276 lemma unistep_true_to_low_step: ∀t1,t2.
 277   R_uni_step_true t1 t2 → low_step_R_true t1 t2.
 278 #t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step * #n #posn #t #h * #qin #tape #eqt1
 279 cases (low_config_eq … eqt1)
 280 #low_left * #low_right * #table * #q_low_hd * #q_low_tl * #current_low
 281 ***** #Hlow_left #Hlow_right #Htable #Hq_low #Hcurrent_low #Ht1
 282 letin trg ≝ (t 〈qin,current ? tape〉)
 283 letin qout_low ≝ (m_bits_of_state n h (\fst trg))
 284 letin qout_low_hd ≝ (hd ? qout_low 〈bit true,false〉)
 285 letin qout_low_tl ≝ (tail ? qout_low)
 286 letin low_act ≝ (low_action (\snd (t 〈qin,current ? tape〉)))
 287 letin low_cout ≝ (\fst low_act)
 288 letin low_m ≝ (\snd low_act)
 289 lapply (Huni_step n table q_low_hd (\fst qout_low_hd)
 290        current_low low_cout low_left low_right q_low_tl qout_low_tl low_m … Ht1)
 291   [@daemon
 292   |>Htable
 293    @(trans_to_match n h t 〈qin,current ? tape〉 … (refl …))
 294    >Hq_low  >Hcurrent_low whd in match (mk_tuple ?????);
 295    >(eq_pair_fst_snd … (t …)) whd in ⊢ (??%?);
 296    >(eq_pair_fst_snd … (low_action …)) %
 297   |//
 298   |@daemon
 299   ]
 300 -Ht1 #Huni_step lapply (Huni_step ? (refl …)) -Huni_step *
 301 #q_low_head_false * #ls1 * #rs1 * #c2 * *
 302 #Ht2 #Hlift #Hlegal %
 303   [whd in ⊢ (??%?); >q_low_head_false in Hq_low;
 304    whd in ⊢ ((???%)→?); generalize in match (h qin);
 305    #x #H destruct (H) %
 306   |>Ht2 whd in match (step FinBool ??);
 307    whd in match (trans ???);
 308    >(eq_pair_fst_snd … (t ?))
 309    @is_low_config // >Hlift
 310    <low_tape_move @eq_f2
 311     [>Hlow_left >Hlow_right >Hcurrent_low whd in ⊢ (??%%);
 312      cases (current …tape) [%] #b whd in ⊢ (??%%); %
 313     |whd in match low_cout; whd in match low_m; whd in match low_act;
 314      generalize in match (\snd (t ?)); * [%] * #b #mv
 315      whd in  ⊢ (??(?(???%)?)%); cases mv %
 316     ]
 317   ]
 318 qed.
 319
 320 definition low_step_R_false ≝ λt1,t2.
 321   ∀M:normalTM.
 322   ∀c: nconfig (no_states M).
 323     t1 = low_config M c → halt ? M (cstate … c) = true  ∧ t1 = t2.
 324
 325 lemma unistep_false_to_low_step: ∀t1,t2.
 326   R_uni_step_false t1 t2 → low_step_R_false t1 t2.
 327 #t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step * #n #posn #t #h * #qin #tape #eqt1
 328 cases (low_config_eq … eqt1) #low_left * #low_right * #table * #q_low_hd * #q_low_tl * #current_low
 329 ***** #_ #_ #_ #Hqin #_ #Ht1 whd in match (halt ???);
 330 cases (Huni_step (h qin) ?) [/2/] >Ht1 whd in ⊢ (??%?); @eq_f
 331 normalize in Hqin; destruct (Hqin) %
 332 qed.
 333
 334 definition low_R ≝ λM,qstart,R,t1,t2.
 335     ∀tape1. t1 = low_config M (mk_config ?? qstart tape1) →
 336     ∃q,tape2.R tape1 tape2 ∧
 337     halt ? M q = true ∧ t2 = low_config M (mk_config ?? q tape2).
 338
 339 lemma sem_uni_step1:
 340   uni_step ⊨ [us_acc: low_step_R_true, low_step_R_false].
 341 qed.
 342
 343 definition universalTM ≝ whileTM ? uni_step us_acc.
 344
 345 theorem sem_universal: ∀M:normalTM. ∀qstart.
 346   universalTM ⊫ (low_R M qstart (R_TM FinBool M qstart)).
 347 qed.
 348
 349 theorem sem_universal2: ∀M:normalTM. ∀R.
 350   M ⊫ R → universalTM ⊫ (low_R M (start ? M) R).
 351 #M #R #HMR lapply (sem_universal … M (start ? M)) @WRealize_to_WRealize
 352 #t1 #t2 whd in ⊢ (%→%); #H #tape1 #Htape1 cases (H ? Htape1)
 353 #q * #tape2 * * #HRTM #Hhalt #Ht2 @(ex_intro … q) @(ex_intro … tape2)
 354 % [% [@(R_TM_to_R … HRTM) @HMR | //] | //]
 355 qed.
 356
 357 axiom terminate_UTM: ∀M:normalTM.∀t.
 358   M ↓ t → universalTM ↓ (low_config M (mk_config ?? (start ? M) t)).
 359