matita/matita/lib/turing/multi_universal/unistep_aux.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/multi_universal/moves_2.ma".
  13 include "turing/multi_universal/match.ma".
  14 include "turing/multi_universal/copy.ma".
  15 include "turing/multi_universal/alphabet.ma".
  16
  17 (*
  18
  19   in.obj : ...  x ...
  20                 ^
  21   in.cfg : ...  ? ? ...
  22                     ^
  23
  24   out.cfg : ... 1 x ...
  25                   ^
  26
  27   ---------------------
  28   current (in.obj) = None
  29
  30   in.cfg : ...  ? ? ...
  31                     ^
  32
  33   out.cfg : ... 0 0 ...
  34                   ^
  35
  36   obj_to_cfg ≝
  37     move_l(cfg);
  38     move_l(cfg);
  39     (if (current(in.obj)) == None
  40        then write(0,cfg);
  41             move_r(cfg);
  42             write(0,cfg);
  43        else write(1,cfg);
  44             move_r(cfg);
  45             copy_step(obj,cfg);
  46             move_l(obj);)
  47     move_to_end_l(cfg);
  48     move_r(cfg);
  49
  50
  51   cfg_to_obj
  52 *)
  53
  54 definition obj ≝ 0.
  55 definition cfg ≝ 1.
  56 definition prg ≝ 2.
  57
  58 definition obj_to_cfg ≝
  59   mmove cfg FSUnialpha 2 L ·
  60   mmove cfg FSUnialpha 2 L ·
  61   (ifTM ?? (inject_TM ? (test_null ?) 2 obj)
  62     (inject_TM ? (write FSUnialpha (bit false)) 2 cfg ·
  63      inject_TM ? (move_r FSUnialpha) 2 cfg ·
  64      inject_TM ? (write FSUnialpha (bit false)) 2 cfg)
  65     (inject_TM ? (write FSUnialpha (bit true)) 2 cfg ·
  66      inject_TM ? (move_r FSUnialpha) 2 cfg ·
  67      copy_step obj cfg FSUnialpha 2) tc_true) ·
  68   inject_TM ? (move_l FSUnialpha) 2 cfg ·
  69   inject_TM ? (move_to_end FSUnialpha L) 2 cfg ·
  70   inject_TM ? (move_r FSUnialpha) 2 cfg.
  71
  72 definition R_obj_to_cfg ≝ λt1,t2:Vector (tape FSUnialpha) 3.
  73   ∀c,opt,ls.
  74   nth cfg ? t1 (niltape ?) = mk_tape FSUnialpha (c::opt::ls) (None ?) [ ] →
  75   (∀lso,x,rso.nth obj ? t1 (niltape ?) = midtape FSUnialpha lso x rso →
  76    t2 = change_vec ?? t1
  77          (mk_tape ? [ ] (option_hd ? (reverse ? (c::opt::ls))) (tail ? (reverse ? (c::opt::ls)))) cfg) ∧
  78   (current ? (nth obj ? t1 (niltape ?)) = None ? →
  79    t2 = change_vec ?? t1
  80          (mk_tape ? [ ] (option_hd FSUnialpha (reverse ? (bit false::bit false::ls)))
  81            (tail ? (reverse ? (bit false :: bit false::ls)))) cfg).
  82
  83 axiom sem_move_to_end_l : ∀sig. move_to_end sig L ⊨ R_move_to_end_l sig.
  84 axiom accRealize_to_Realize :
  85   ∀sig,n.∀M:mTM sig n.∀Rtrue,Rfalse,acc.
  86   M ⊨ [ acc: Rtrue, Rfalse ] →  M ⊨ Rtrue ∪ Rfalse.
  87
  88 lemma eq_mk_tape_rightof :
  89  ∀alpha,a,al.mk_tape alpha (a::al) (None ?) [ ] = rightof ? a al.
  90 #alpha #a #al %
  91 qed.
  92
  93 lemma sem_obj_to_cfg : obj_to_cfg ⊨  R_obj_to_cfg.
  94 @(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?)
  95   (sem_seq ?????? (sem_move_multi ? 2 cfg L ?)
  96    (sem_seq ??????
  97     (sem_if ??????????
  98      (sem_test_null_multi ?? obj ?)
  99      (sem_seq ?????? (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false)))
 100       (sem_seq ?????? (sem_inject ???? cfg ? (sem_move_r ?))
 101        (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false)))))
 102       (sem_seq ?????? (sem_inject ???? cfg ? (sem_write FSUnialpha (bit true)))
 103        (sem_seq ?????? (sem_inject ???? cfg ? (sem_move_r ?)) (accRealize_to_Realize … (sem_copy_step …)))))
 104      (sem_seq ?????? (sem_inject ???? cfg ? (sem_move_l ?))
 105       (sem_seq ?????? (sem_inject ???? cfg ? (sem_move_to_end_l ?))
 106        (sem_inject ???? cfg ? (sem_move_r ?))))))) //
 107 #ta #tb *
 108 #tc * whd in ⊢ (%→?); #Htc *
 109 #td * whd in ⊢ (%→?); #Htd *
 110 #te * *
 111 [ * #tf * * #Hcurtd #Htf *
 112   #tg * * whd in ⊢ (%→?); #Htg1 #Htg2 *
 113   #th * * * whd in ⊢ (%→%→?); #Hth1 #Hth2 #Hth3 * whd in ⊢ (%→?);
 114   #Hte1 #Hte2 *
 115   #tj * * * #Htj1 #Htj2 #Htj3 *
 116   #tk * * * #Htk1 #Htk2 #Htk3 * whd in ⊢ (%→?);
 117   #Htb1 #Htb2 #c #opt_mark #ls #Hta1 %
 118   [ #lso #x #rso #Hta2 >Hta1 in Htc; >eq_mk_tape_rightof whd in match (tape_move ???); #Htc
 119     >Htc in Htd; >nth_change_vec // >change_vec_change_vec
 120     change with (midtape ????) in match (tape_move ???); #Htd >Htd in Htf; #Htf
 121     destruct (Htf)
 122
 123
 124
 125
 126 lemma wsem_copy : ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
 127   copy src dst sig n ⊫ R_copy src dst sig n.
 128 #src #dst #sig #n #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
 129 lapply (sem_while … (sem_copy_step src dst sig n Hneq Hsrc Hdst) … Hloop) //
 130 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
 131 [ whd in ⊢ (%→?); * #Hnone #Hout %
 132   [#_ @Hout
 133   |#ls #x #x0 #rs #ls0 #rs0 #Hsrc1 #Hdst1 @False_ind cases Hnone
 134     [>Hsrc1 normalize #H destruct (H) | >Hdst1 normalize #H destruct (H)]
 135   ]
 136 |#tc #td * #x * #y * * #Hcx #Hcy #Htd #Hstar #IH #He lapply (IH He) -IH *
 137  #IH1 #IH2 %
 138   [* [>Hcx #H destruct (H) | >Hcy #H destruct (H)]
 139   |#ls #x' #y' #rs #ls0 #rs0 #Hnth_src #Hnth_dst
 140    >Hnth_src in Hcx; whd in ⊢ (??%?→?); #H destruct (H)
 141    >Hnth_dst in Hcy; whd in ⊢ (??%?→?); #H destruct (H)
 142    >Hnth_src in Htd; >Hnth_dst -Hnth_src -Hnth_dst
 143    cases rs
 144     [(* the source tape is empty after the move *)
 145      #Htd lapply (IH1 ?)
 146       [%1 >Htd >nth_change_vec_neq [2:@(not_to_not … Hneq) //] >nth_change_vec //]
 147      #Hout (* whd in match (tape_move ???); *) %1 %{([])} %{rs0} %
 148       [% [// | // ]
 149       |whd in match (reverse ??); whd in match (reverse ??);
 150        >Hout >Htd @eq_f2 // cases rs0 //
 151       ]
 152     |#c1 #tl1 cases rs0
 153       [(* the dst tape is empty after the move *)
 154        #Htd lapply (IH1 ?) [%2 >Htd >nth_change_vec //]
 155        #Hout (* whd in match (tape_move ???); *) %2 %{[ ]} %{(c1::tl1)} %
 156         [% [// | // ]
 157         |whd in match (reverse ??); whd in match (reverse ??);
 158          >Hout >Htd @eq_f2 //
 159         ]
 160       |#c2 #tl2 whd in match (tape_move_mono ???); whd in match (tape_move_mono ???);
 161        #Htd
 162        cut (nth src (tape sig) td (niltape sig)=midtape sig (x::ls) c1 tl1)
 163          [>Htd >nth_change_vec_neq [2:@(not_to_not … Hneq) //] @nth_change_vec //]
 164        #Hsrc_td
 165        cut (nth dst (tape sig) td (niltape sig)=midtape sig (x::ls0) c2 tl2)
 166          [>Htd @nth_change_vec //]
 167        #Hdst_td cases (IH2 … Hsrc_td Hdst_td) -Hsrc_td -Hdst_td
 168         [* #rs01 * #rs02 * * #H1 #H2 #H3 %1
 169          %{(c2::rs01)} %{rs02} % [% [@eq_f //|normalize @eq_f @H2]]
 170          >Htd in H3; >change_vec_commute // >change_vec_change_vec
 171          >change_vec_commute [2:@(not_to_not … Hneq) //] >change_vec_change_vec
 172          #H >reverse_cons >associative_append >associative_append @H
 173         |* #rs11 * #rs12 * * #H1 #H2 #H3 %2
 174          %{(c1::rs11)} %{rs12} % [% [@eq_f //|normalize @eq_f @H2]]
 175          >Htd in H3; >change_vec_commute // >change_vec_change_vec
 176          >change_vec_commute [2:@(not_to_not … Hneq) //] >change_vec_change_vec
 177          #H >reverse_cons >associative_append >associative_append @H
 178         ]
 179       ]
 180     ]
 181   ]
 182 qed.
 183
 184
 185 lemma terminate_copy :  ∀src,dst,sig,n,t.
 186   src ≠ dst → src < S n → dst < S n → copy src dst sig n ↓ t.
 187 #src #dst #sig #n #t #Hneq #Hsrc #Hdts
 188 @(terminate_while … (sem_copy_step …)) //
 189 <(change_vec_same … t src (niltape ?))
 190 cases (nth src (tape sig) t (niltape ?))
 191 [ % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 192 |2,3: #a0 #al0 % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 193 | #ls #c #rs lapply c -c lapply ls -ls lapply t -t elim rs
 194   [#t #ls #c % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?);
 195    #H1 destruct (H1) #_ >change_vec_change_vec #Ht1 %
 196    #t2 * #x0 * #y0 * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
 197    >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H)
 198   |#r0 #rs0 #IH #t #ls #c % #t1 * #x * #y * * >nth_change_vec //
 199    normalize in ⊢ (%→?); #H destruct (H) #Hcur
 200    >change_vec_change_vec >change_vec_commute // #Ht1 >Ht1 @IH
 201   ]
 202 ]
 203 qed.
 204
 205 lemma sem_copy : ∀src,dst,sig,n.
 206   src ≠ dst → src < S n → dst < S n →
 207   copy src dst sig n ⊨ R_copy src dst sig n.
 208 #i #j #sig #n #Hneq #Hi #Hj @WRealize_to_Realize [/2/| @wsem_copy // ]
 209 qed.