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
  85 lemma sem_obj_to_cfg : obj_to_cfg ⊨  R_obj_to_cfg.
  86 @(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?)
  87   (sem_seq_app ?? ????? (sem_move_multi ? 2 cfg L ?)
  88    (sem_seq_app ???????
  89     (sem_seq_app ???????
  90      (sem_if ? 2 ????????
  91       (sem_test_null_multi ?? obj ?)
  92       (sem_seq_app ??????? (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false)))
  93        (sem_seq_app ??????? (sem_inject ???? cfg ? (sem_move_r ?))
  94         (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false))) ?) ?)
  95       ?)
  96      ??) ??) ?) ?)
  97 [|||||||||||||||| @
  98
  99         ??) ??) ??) ?) ?)
 100        ?) ?) ?) ?)
 101
 102
 103 @(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?) ??)
 104 [||
 105 @(sem_seq_app ?? ????? (sem_move_multi ? 2 cfg L ?) ??)
 106 [|| @sem_seq_app
 107 [|| @sem_seq_app
 108 [|| @(sem_if ? 2 ???????? (sem_test_null_multi ?? obj ?))
 109 [|||@(sem_seq_app ??????? (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false))) ?)
 110 [||@(sem_seq_app ??????? (sem_inject ???? cfg ? (sem_move_r ?))
 111        (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false))) ?)
 112 [||
 113
 114 @(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?)
 115   (sem_seq_app ?? ????? (sem_move_multi ? 2 cfg L ?)
 116    (sem_seq_app ???????
 117     (sem_if ? 2 ????????
 118      (sem_test_null_multi ?? obj ?)
 119      (sem_seq_app ??????? (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false)))
 120       (sem_seq_app ??????? (sem_inject ???? cfg ? (sem_move_r ?))
 121        (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false))) ?) ?)
 122        ?)
 123     (sem_seq_app ??????? (sem_inject ???? cfg ? (sem_move_to_end_l ?))
 124      (sem_inject ???? cfg ? (sem_move_r ?)) ?) ?) ?) ?)
 125
 126
 127 lemma wsem_copy : ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
 128   copy src dst sig n ⊫ R_copy src dst sig n.
 129 #src #dst #sig #n #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
 130 lapply (sem_while … (sem_copy_step src dst sig n Hneq Hsrc Hdst) … Hloop) //
 131 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
 132 [ whd in ⊢ (%→?); * #Hnone #Hout %
 133   [#_ @Hout
 134   |#ls #x #x0 #rs #ls0 #rs0 #Hsrc1 #Hdst1 @False_ind cases Hnone
 135     [>Hsrc1 normalize #H destruct (H) | >Hdst1 normalize #H destruct (H)]
 136   ]
 137 |#tc #td * #x * #y * * #Hcx #Hcy #Htd #Hstar #IH #He lapply (IH He) -IH *
 138  #IH1 #IH2 %
 139   [* [>Hcx #H destruct (H) | >Hcy #H destruct (H)]
 140   |#ls #x' #y' #rs #ls0 #rs0 #Hnth_src #Hnth_dst
 141    >Hnth_src in Hcx; whd in ⊢ (??%?→?); #H destruct (H)
 142    >Hnth_dst in Hcy; whd in ⊢ (??%?→?); #H destruct (H)
 143    >Hnth_src in Htd; >Hnth_dst -Hnth_src -Hnth_dst
 144    cases rs
 145     [(* the source tape is empty after the move *)
 146      #Htd lapply (IH1 ?)
 147       [%1 >Htd >nth_change_vec_neq [2:@(not_to_not … Hneq) //] >nth_change_vec //]
 148      #Hout (* whd in match (tape_move ???); *) %1 %{([])} %{rs0} %
 149       [% [// | // ]
 150       |whd in match (reverse ??); whd in match (reverse ??);
 151        >Hout >Htd @eq_f2 // cases rs0 //
 152       ]
 153     |#c1 #tl1 cases rs0
 154       [(* the dst tape is empty after the move *)
 155        #Htd lapply (IH1 ?) [%2 >Htd >nth_change_vec //]
 156        #Hout (* whd in match (tape_move ???); *) %2 %{[ ]} %{(c1::tl1)} %
 157         [% [// | // ]
 158         |whd in match (reverse ??); whd in match (reverse ??);
 159          >Hout >Htd @eq_f2 //
 160         ]
 161       |#c2 #tl2 whd in match (tape_move_mono ???); whd in match (tape_move_mono ???);
 162        #Htd
 163        cut (nth src (tape sig) td (niltape sig)=midtape sig (x::ls) c1 tl1)
 164          [>Htd >nth_change_vec_neq [2:@(not_to_not … Hneq) //] @nth_change_vec //]
 165        #Hsrc_td
 166        cut (nth dst (tape sig) td (niltape sig)=midtape sig (x::ls0) c2 tl2)
 167          [>Htd @nth_change_vec //]
 168        #Hdst_td cases (IH2 … Hsrc_td Hdst_td) -Hsrc_td -Hdst_td
 169         [* #rs01 * #rs02 * * #H1 #H2 #H3 %1
 170          %{(c2::rs01)} %{rs02} % [% [@eq_f //|normalize @eq_f @H2]]
 171          >Htd in H3; >change_vec_commute // >change_vec_change_vec
 172          >change_vec_commute [2:@(not_to_not … Hneq) //] >change_vec_change_vec
 173          #H >reverse_cons >associative_append >associative_append @H
 174         |* #rs11 * #rs12 * * #H1 #H2 #H3 %2
 175          %{(c1::rs11)} %{rs12} % [% [@eq_f //|normalize @eq_f @H2]]
 176          >Htd in H3; >change_vec_commute // >change_vec_change_vec
 177          >change_vec_commute [2:@(not_to_not … Hneq) //] >change_vec_change_vec
 178          #H >reverse_cons >associative_append >associative_append @H
 179         ]
 180       ]
 181     ]
 182   ]
 183 qed.
 184
 185
 186 lemma terminate_copy :  ∀src,dst,sig,n,t.
 187   src ≠ dst → src < S n → dst < S n → copy src dst sig n ↓ t.
 188 #src #dst #sig #n #t #Hneq #Hsrc #Hdts
 189 @(terminate_while … (sem_copy_step …)) //
 190 <(change_vec_same … t src (niltape ?))
 191 cases (nth src (tape sig) t (niltape ?))
 192 [ % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 193 |2,3: #a0 #al0 % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 194 | #ls #c #rs lapply c -c lapply ls -ls lapply t -t elim rs
 195   [#t #ls #c % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?);
 196    #H1 destruct (H1) #_ >change_vec_change_vec #Ht1 %
 197    #t2 * #x0 * #y0 * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
 198    >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H)
 199   |#r0 #rs0 #IH #t #ls #c % #t1 * #x * #y * * >nth_change_vec //
 200    normalize in ⊢ (%→?); #H destruct (H) #Hcur
 201    >change_vec_change_vec >change_vec_commute // #Ht1 >Ht1 @IH
 202   ]
 203 ]
 204 qed.
 205
 206 lemma sem_copy : ∀src,dst,sig,n.
 207   src ≠ dst → src < S n → dst < S n →
 208   copy src dst sig n ⊨ R_copy src dst sig n.
 209 #i #j #sig #n #Hneq #Hi #Hj @WRealize_to_Realize [/2/| @wsem_copy // ]
 210 qed.