matita/matita/lib/turing/multi_to_mono/full.ma

   1
   2 include "turing/multi_to_mono/step.ma".
   3
   4 definition stop ≝ λsig,n.λM:mTM sig n.λc.
   5    notb (halt sig n M (get_state (states sig n M) sig (S n) c (start sig n M))).
   6
   7 definition mtm_body ≝ λsig,n.λM:mTM sig n.
   8   ifTM ? (test_char … (stop sig n M))
   9     (single_finalTM ? (stepM (states sig n M) sig n (trans sig n M)))
  10     (nop … ) tc_true.
  11
  12 definition acc_mtm : ∀sig,n,M.states ? (mtm_body sig n M) ≝
  13   λsig,n,M. (inr … (inl … (inr … start_nop))).
  14
  15 definition mtm_R_true ≝ λsig,n.λM:mTM sig n.λt1,t2.
  16 ∀a:multi_sig (TA (HC (states sig n M) (S n)) sig) (S (S n)).
  17 ∀ls,rs.
  18   t1 = midtape ? ls a rs →
  19   let cin ≝ readback_config ? sig n (start … M) ls a rs in
  20   halt sig n M (cstate … cin) = false ∧
  21   R_stepM sig n M t1 t2.
  22
  23 definition mtm_R_false ≝ λsig,n.λM:mTM sig n.λt1,t2.
  24 ∀a:multi_sig (TA (HC (states sig n M) (S n)) sig) (S (S n)).
  25 ∀ls,rs.
  26   t1 = midtape ? ls a rs →
  27   let cin ≝ readback_config ? sig n (start … M) ls a rs in
  28   halt sig n M (cstate … cin) = true ∧ t1 = t2.
  29
  30 lemma sem_mtm_body: ∀sig,n,M.
  31   mtm_body sig n M ⊨ [acc_mtm sig n M: mtm_R_true sig n M,
  32                                        mtm_R_false sig n M].
  33 #sig #n #M
  34 @(acc_sem_if_app ??????????? (sem_test_char … (stop sig n M))
  35    (sem_stepM sig n M)
  36    (sem_nop …))
  37 [#tin #tout #t1 * * #c * #Hc #Hstop #Ht1 >Ht1 #Hstep
  38  #a #ls #rs #Htin % [2:@Hstep] >Htin in Hc; whd in ⊢ (??%?→?);
  39  #H destruct (H) >state_readback @injective_notb @Hstop
  40 |#tin #tout #t1 * #Hc #Ht1 #Htout #a #ls #rs #Htin % //
  41  >Htin in Hc; #Hc lapply (Hc … (refl ??)) #H @injective_notb @H
  42 ]
  43 qed.
  44
  45 definition multi_to_monoTM ≝ λsig,n,M.
  46   whileTM ? (mtm_body sig n M) (acc_mtm sig n M).
  47
  48 definition multi_to_mono_R ≝ λsig,n.λM:mTM sig n.λt1,t2.
  49 ∀a:multi_sig (TA (HC (states sig n M) (S n)) sig) (S (S n)).
  50 ∀ls,rs.
  51   t1 = midtape ? ls a rs →
  52   (∀i.regular_trace (TA (HC (states … M) (S n)) sig) (S(S n)) a ls rs i) →
  53   is_head ?? (nth (S n) ? (vec … a) (blank ?)) = true →
  54   no_head_in … ls →
  55   no_head_in … rs →
  56   let cin ≝ readback_config ? sig n (start … M) ls a rs in
  57   ∃a1:multi_sig (TA (HC (states sig n M) (S n)) sig) (S (S n)).
  58   ∃ls1,rs1,i.
  59     t2 = midtape ? ls1 a1 rs1 ∧
  60     let cout ≝ readback_config ? sig n (start … M) ls1 a1 rs1 in
  61     loopM sig n M i cin = Some ? cout.
  62
  63 theorem sem_universal: ∀sig,n,M.
  64   multi_to_monoTM sig n M ⊫ multi_to_mono_R sig n M.
  65 #sig #n #M #intape #i #outc #Hloop
  66 lapply (sem_while ?????? (sem_mtm_body sig n M) intape i outc Hloop) [%] -Hloop
  67 * #tin * #Hstar #Hfalse @(star_ind_l ??????? Hstar) -Hstar
  68 [#a #ls #rs #Htin #_ #_ #_ #_ lapply (Hfalse … Htin) * #Hhalt #Houtc
  69 %{a} %{ls} %{rs} %{1} % [<Houtc @Htin |@loop_S_true @Hhalt]
  70 |#ta #tb #Hab #Hstar #Hind #a #ls #rs #Ha #H1 #H2 #H3 #H4 lapply (Hab … Ha)
  71  * #Hfalseb -Hab #Hab lapply (Hab … Ha H1 H2 H3 H4) -H1 -H2 -H3 -H4
  72  * #ls1 * #a1 * #rs1 * * #Htb #Hregb #Hrb_b
  73  lapply (Hind … Htb Hregb ???) [@daemon | @daemon |@daemon]
  74  * #a2 * #ls2 * #rs2 * #i * #Hc #Hloop
  75  %{a2} %{ls2} %{rs2} %{(S i)} % [@Hc] whd
  76  whd in match (loopM ?????); >Hfalseb whd in ⊢ (??%?); <Hrb_b @Hloop
  77 ]
  78 qed.
  79
  80