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:DeqNat).
  55 definition cfg ≝ (1:DeqNat).
  56 definition prg ≝ (2:DeqNat).
  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 true)) 2 cfg ·
  63      inject_TM ? (move_r FSUnialpha) 2 cfg ·
  64      copy_step obj cfg FSUnialpha 2)
  65     (inject_TM ? (write FSUnialpha (bit false)) 2 cfg ·
  66      inject_TM ? (move_r FSUnialpha) 2 cfg ·
  67      inject_TM ? (write FSUnialpha (bit false)) 2 cfg)
  68      tc_true) ·
  69   inject_TM ? (move_l FSUnialpha) 2 cfg ·
  70   inject_TM ? (move_to_end FSUnialpha L) 2 cfg ·
  71   mmove cfg FSUnialpha 2 L.
  72
  73 definition R_obj_to_cfg ≝ λt1,t2:Vector (tape FSUnialpha) 3.
  74   ∀c,opt,ls.
  75   nth cfg ? t1 (niltape ?) = mk_tape FSUnialpha (c::opt::ls) (None ?) [ ] →
  76   (∀lso,x,rso.nth obj ? t1 (niltape ?) = midtape FSUnialpha lso x rso →
  77    t2 = change_vec ?? t1
  78          (mk_tape ? [ ] (option_hd ? (reverse ? (c::opt::ls))) (tail ? (reverse ? (c::opt::ls)))) cfg) ∧
  79   (current ? (nth obj ? t1 (niltape ?)) = None ? →
  80    t2 = change_vec ?? t1
  81          (mk_tape ? [ ] (option_hd FSUnialpha (reverse ? (bit false::bit false::ls)))
  82            (tail ? (reverse ? (bit false :: bit false::ls)))) cfg).
  83
  84 axiom sem_move_to_end_l : ∀sig. move_to_end sig L ⊨ R_move_to_end_l sig.
  85 axiom accRealize_to_Realize :
  86   ∀sig,n.∀M:mTM sig n.∀Rtrue,Rfalse,acc.
  87   M ⊨ [ acc: Rtrue, Rfalse ] →  M ⊨ Rtrue ∪ Rfalse.
  88
  89 lemma eq_mk_tape_rightof :
  90  ∀alpha,a,al.mk_tape alpha (a::al) (None ?) [ ] = rightof ? a al.
  91 #alpha #a #al %
  92 qed.
  93
  94 axiom daemon : ∀P:Prop.P.
  95
  96 lemma sem_obj_to_cfg : obj_to_cfg ⊨  R_obj_to_cfg.
  97 @(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?)
  98   (sem_seq ?????? (sem_move_multi ? 2 cfg L ?)
  99    (sem_seq ??????
 100     (sem_if ??????????
 101      (sem_test_null_multi ?? obj ?)
 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_write FSUnialpha (bit false)))
 105       (sem_seq ?????? (sem_inject ???? cfg ? (sem_move_r ?))
 106        (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false))))))
 107      (sem_seq ?????? (sem_inject ???? cfg ? (sem_move_l ?))
 108       (sem_seq ?????? (sem_inject ???? cfg ? (sem_move_to_end_l ?))
 109        (sem_move_multi ? 2 cfg L ?)))))) //
 110 #ta #tb *
 111 #tc * whd in ⊢ (%→?); #Htc *
 112 #td * whd in ⊢ (%→?); #Htd *
 113 #te * *
 114 [
 115 | * #tf * * #Hcurtd #Htf *
 116   #tg * * whd in ⊢ (%→?); #Htg1 #Htg2 *
 117   #th * * * whd in ⊢ (%→%→?); #Hth1 #Hth2 #Hth3 * whd in ⊢ (%→?);
 118   #Hte1 #Hte2 *
 119   #tj * * * #Htj1 #Htj2 #Htj3 *
 120   #tk * * * #Htk1 #Htk2 #Htk3 whd in ⊢ (%→?); #Htb
 121   #c #opt_mark #ls #Hta1 %
 122   [ #lso #x #rso #Hta2 >Htd in Hcurtd; >Htc >change_vec_change_vec
 123     >nth_change_vec_neq [|@sym_not_eq //] >Hta2 normalize in ⊢ (%→?); #H destruct (H)
 124   | #_ >Hta1 in Htc; >eq_mk_tape_rightof whd in match (tape_move ???); #Htc
 125     >Htc in Htd; >nth_change_vec // >change_vec_change_vec
 126     change with (midtape ????) in match (tape_move ???); #Htd >Htd in Htf; #Htf
 127     destruct (Htf) cut (tg = change_vec ?? ta (midtape ? ls (bit false) [c]) cfg)
 128     [ @(eq_vec … (niltape ?)) #i #Hi cases (true_or_false (cfg == i)) #Hcfgi
 129       [ <(\P Hcfgi) >nth_change_vec // @Htg1 //
 130       | <(Htg2 ? (\Pf Hcfgi)) >(nth_change_vec_neq ??????? (\Pf Hcfgi))
 131         >(nth_change_vec_neq ??????? (\Pf Hcfgi)) % ] ] -Htg1 -Htg2 #Htg
 132     -Hth1 cut (th = change_vec ?? tg (midtape ? (bit false::ls) c []) cfg)
 133     [ @(eq_vec … (niltape ?)) #i #Hi cases (true_or_false (cfg == i)) #Hcfgi
 134       [ <(\P Hcfgi) >nth_change_vec // >Htg in Hth2; >nth_change_vec // #Hth2
 135         @(Hth2 … (refl ??))
 136       | <(Hth3 ? (\Pf Hcfgi)) >(nth_change_vec_neq ??????? (\Pf Hcfgi)) // ] ]
 137     -Hth2 -Hth3 #Hth
 138     cut (te = change_vec ?? th (midtape ? (bit false::ls) (bit false) [ ]) cfg)
 139     [@daemon] -Hte1 -Hte2 #Hte
 140     -Htj1 cut (tj = change_vec ?? te (midtape ? ls (bit false) [bit false]) cfg)
 141     [@daemon] -Htj2 -Htj3 #Htj
 142     -Htk1 cut (tk = change_vec ?? tj (mk_tape ? [ ] (None ?) (reverse ? ls@[bit false;bit false])) cfg)
 143     [ @(eq_vec … (niltape ?)) #i #Hi cases (true_or_false (cfg == i)) #Hcfgi
 144       [ <(\P Hcfgi) >nth_change_vec // >Htj in Htk2; >nth_change_vec // #Htk2
 145         @(Htk2 … (refl ??))
 146       | <(Htk3 ? (\Pf Hcfgi)) >(nth_change_vec_neq ??????? (\Pf Hcfgi)) // ] ]
 147     -Htk2 -Htk3 #Htk >Htb >Htk >change_vec_change_vec >nth_change_vec //
 148     >Htj >change_vec_change_vec >Hte >change_vec_change_vec
 149     >Hth >change_vec_change_vec >Htg >change_vec_change_vec
 150     >reverse_cons >reverse_cons
 151
 152
 153      >nth_change_vec in Htg1; // #Htg1 lapply (Htg1 … (refl ??)) -Htg1 #Htg1
 154     cut (∀j.cfg ≠ j → nth j ? ta (niltape ?) = nth j ? tg (niltape ?))
 155     [ #j #Hj <Htg2 // >nth_change_vec_neq // ] -Htg2 #Htg2
 156
 157
 158
 159
 160 lemma wsem_copy : ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
 161   copy src dst sig n ⊫ R_copy src dst sig n.
 162 #src #dst #sig #n #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
 163 lapply (sem_while … (sem_copy_step src dst sig n Hneq Hsrc Hdst) … Hloop) //
 164 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
 165 [ whd in ⊢ (%→?); * #Hnone #Hout %
 166   [#_ @Hout
 167   |#ls #x #x0 #rs #ls0 #rs0 #Hsrc1 #Hdst1 @False_ind cases Hnone
 168     [>Hsrc1 normalize #H destruct (H) | >Hdst1 normalize #H destruct (H)]
 169   ]
 170 |#tc #td * #x * #y * * #Hcx #Hcy #Htd #Hstar #IH #He lapply (IH He) -IH *
 171  #IH1 #IH2 %
 172   [* [>Hcx #H destruct (H) | >Hcy #H destruct (H)]
 173   |#ls #x' #y' #rs #ls0 #rs0 #Hnth_src #Hnth_dst
 174    >Hnth_src in Hcx; whd in ⊢ (??%?→?); #H destruct (H)
 175    >Hnth_dst in Hcy; whd in ⊢ (??%?→?); #H destruct (H)
 176    >Hnth_src in Htd; >Hnth_dst -Hnth_src -Hnth_dst
 177    cases rs
 178     [(* the source tape is empty after the move *)
 179      #Htd lapply (IH1 ?)
 180       [%1 >Htd >nth_change_vec_neq [2:@(not_to_not … Hneq) //] >nth_change_vec //]
 181      #Hout (* whd in match (tape_move ???); *) %1 %{([])} %{rs0} %
 182       [% [// | // ]
 183       |whd in match (reverse ??); whd in match (reverse ??);
 184        >Hout >Htd @eq_f2 // cases rs0 //
 185       ]
 186     |#c1 #tl1 cases rs0
 187       [(* the dst tape is empty after the move *)
 188        #Htd lapply (IH1 ?) [%2 >Htd >nth_change_vec //]
 189        #Hout (* whd in match (tape_move ???); *) %2 %{[ ]} %{(c1::tl1)} %
 190         [% [// | // ]
 191         |whd in match (reverse ??); whd in match (reverse ??);
 192          >Hout >Htd @eq_f2 //
 193         ]
 194       |#c2 #tl2 whd in match (tape_move_mono ???); whd in match (tape_move_mono ???);
 195        #Htd
 196        cut (nth src (tape sig) td (niltape sig)=midtape sig (x::ls) c1 tl1)
 197          [>Htd >nth_change_vec_neq [2:@(not_to_not … Hneq) //] @nth_change_vec //]
 198        #Hsrc_td
 199        cut (nth dst (tape sig) td (niltape sig)=midtape sig (x::ls0) c2 tl2)
 200          [>Htd @nth_change_vec //]
 201        #Hdst_td cases (IH2 … Hsrc_td Hdst_td) -Hsrc_td -Hdst_td
 202         [* #rs01 * #rs02 * * #H1 #H2 #H3 %1
 203          %{(c2::rs01)} %{rs02} % [% [@eq_f //|normalize @eq_f @H2]]
 204          >Htd in H3; >change_vec_commute // >change_vec_change_vec
 205          >change_vec_commute [2:@(not_to_not … Hneq) //] >change_vec_change_vec
 206          #H >reverse_cons >associative_append >associative_append @H
 207         |* #rs11 * #rs12 * * #H1 #H2 #H3 %2
 208          %{(c1::rs11)} %{rs12} % [% [@eq_f //|normalize @eq_f @H2]]
 209          >Htd in H3; >change_vec_commute // >change_vec_change_vec
 210          >change_vec_commute [2:@(not_to_not … Hneq) //] >change_vec_change_vec
 211          #H >reverse_cons >associative_append >associative_append @H
 212         ]
 213       ]
 214     ]
 215   ]
 216 qed.
 217
 218
 219 lemma terminate_copy :  ∀src,dst,sig,n,t.
 220   src ≠ dst → src < S n → dst < S n → copy src dst sig n ↓ t.
 221 #src #dst #sig #n #t #Hneq #Hsrc #Hdts
 222 @(terminate_while … (sem_copy_step …)) //
 223 <(change_vec_same … t src (niltape ?))
 224 cases (nth src (tape sig) t (niltape ?))
 225 [ % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 226 |2,3: #a0 #al0 % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 227 | #ls #c #rs lapply c -c lapply ls -ls lapply t -t elim rs
 228   [#t #ls #c % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?);
 229    #H1 destruct (H1) #_ >change_vec_change_vec #Ht1 %
 230    #t2 * #x0 * #y0 * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
 231    >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H)
 232   |#r0 #rs0 #IH #t #ls #c % #t1 * #x * #y * * >nth_change_vec //
 233    normalize in ⊢ (%→?); #H destruct (H) #Hcur
 234    >change_vec_change_vec >change_vec_commute // #Ht1 >Ht1 @IH
 235   ]
 236 ]
 237 qed.
 238
 239 lemma sem_copy : ∀src,dst,sig,n.
 240   src ≠ dst → src < S n → dst < S n →
 241   copy src dst sig n ⊨ R_copy src dst sig n.
 242 #i #j #sig #n #Hneq #Hi #Hj @WRealize_to_Realize [/2/| @wsem_copy // ]
 243 qed.