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