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
  16 (*
  17
  18   in.obj : ...  x ...
  19                 ^
  20   in.cfg : ...  ? ? ...
  21                     ^
  22
  23   out.cfg : ... 1 x ...
  24                   ^
  25
  26   ---------------------
  27   current (in.obj) = None
  28
  29   in.cfg : ...  ? ? ...
  30                     ^
  31
  32   out.cfg : ... 0 0 ...
  33                   ^
  34
  35   obj_to_cfg ≝
  36     move_l(cfg);
  37     move_l(cfg);
  38     (if (current(in.obj)) == None
  39        then write(0,cfg);
  40             move_r(cfg);
  41             write(0,cfg);
  42        else write(1,cfg);
  43             move_r(cfg);
  44             copy_step(obj,cfg);
  45             move_l(obj);)
  46     move_to_end_l(cfg);
  47     move_r(cfg);
  48
  49
  50   cfg_to_obj
  51 *)
  52
  53 inductive unialpha : Type[0] ≝
  54 | bit : bool → unialpha
  55 | bar : unialpha.
  56
  57 definition unialpha_eq ≝
  58   λa1,a2.match a1 with
  59   [ bit x ⇒ match a2 with [ bit y ⇒ ¬ xorb x y | _ ⇒ false ]
  60   | bar ⇒ match a2 with [ bar ⇒ true | _ ⇒ false ] ].
  61
  62 definition DeqUnialpha ≝ mk_DeqSet unialpha unialpha_eq ?.
  63 * [ #x * [ #y cases x cases y normalize % // #Hfalse destruct
  64          | *: normalize % #Hfalse destruct ]
  65   | * [ #y ] normalize % #H1 destruct % ]
  66 qed.
  67
  68 lemma unialpha_unique :
  69   uniqueb DeqUnialpha [bit true;bit false;bar] = true.
  70 // qed.
  71
  72 lemma unialpha_complete :∀x:DeqUnialpha.
  73   memb ? x [bit true;bit false;bar] = true.
  74 * // * //
  75 qed.
  76
  77 definition FSUnialpha ≝
  78   mk_FinSet DeqUnialpha [bit true;bit false;bar]
  79   unialpha_unique unialpha_complete.
  80
  81 (*************************** testing characters *******************************)
  82 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
  83 definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ].
  84
  85 definition obj ≝ 0.
  86 definition cfg ≝ 1.
  87 definition prg ≝ 2.
  88
  89 definition obj_to_cfg ≝
  90   mmove cfg FSUnialpha 2 L ·
  91   mmove cfg FSUnialpha 2 L ·
  92   (ifTM ?? (inject_TM ? (test_null ?) 2 obj)
  93     (inject_TM ? (write FSUnialpha (bit false)) 2 cfg ·
  94      inject_TM ? (move_r FSUnialpha) 2 cfg ·
  95      inject_TM ? (write FSUnialpha (bit false)) 2 cfg)
  96     (inject_TM ? (write FSUnialpha (bit true)) 2 cfg ·
  97      inject_TM ? (move_r FSUnialpha) 2 cfg ·
  98      copy_step obj cfg FSUnialpha 2) tc_true ·
  99      inject_TM ? (move_l FSUnialpha) 2 cfg) ·
 100   inject_TM ? (move_to_end FSUnialpha L) 2 cfg ·
 101   inject_TM ? (move_r FSUnialpha) 2 cfg.
 102
 103 definition R_obj_to_cfg ≝ λt1,t2:Vector (tape FSUnialpha) 3.
 104   ∀c,opt,ls.
 105   nth cfg ? t1 (niltape ?) = mk_tape FSUnialpha (c::opt::ls) (None ?) [ ] →
 106   (∀lso,x,rso.nth obj ? t1 (niltape ?) = midtape FSUnialpha lso x rso →
 107    t2 = change_vec ?? t1
 108          (mk_tape ? [ ] (option_hd ? (reverse ? (c::opt::ls))) (tail ? (reverse ? (c::opt::ls)))) cfg) ∧
 109   (current ? (nth obj ? t1 (niltape ?)) = None ? →
 110    t2 = change_vec ?? t1
 111          (mk_tape ? [ ] (option_hd FSUnialpha (reverse ? (bit false::bit false::ls)))
 112            (tail ? (reverse ? (bit false :: bit false::ls)))) cfg).
 113
 114 axiom sem_move_to_end_l : ∀sig. move_to_end sig L ⊨ R_move_to_end_l sig.
 115
 116 lemma sem_obj_to_cfg : obj_to_cfg ⊨  R_obj_to_cfg.
 117 @(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?)
 118   (sem_seq_app ?? ????? (sem_move_multi ? 2 cfg L ?)
 119    (sem_seq_app ???????
 120     (sem_seq_app ???????
 121      (sem_if ? 2 ????????
 122       (sem_test_null_multi ?? obj ?)
 123       (sem_seq_app ??????? (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false)))
 124        (sem_seq_app ??????? (sem_inject ???? cfg ? (sem_move_r ?))
 125         (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false))) ?) ?)
 126       ?)
 127      ??) ??) ?) ?)
 128 [|||||||||||||||| @
 129
 130         ??) ??) ??) ?) ?)
 131        ?) ?) ?) ?)
 132
 133
 134 @(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?) ??)
 135 [||
 136 @(sem_seq_app ?? ????? (sem_move_multi ? 2 cfg L ?) ??)
 137 [|| @sem_seq_app
 138 [|| @sem_seq_app
 139 [|| @(sem_if ? 2 ???????? (sem_test_null_multi ?? obj ?))
 140 [|||@(sem_seq_app ??????? (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false))) ?)
 141 [||@(sem_seq_app ??????? (sem_inject ???? cfg ? (sem_move_r ?))
 142        (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false))) ?)
 143 [||
 144
 145 @(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?)
 146   (sem_seq_app ?? ????? (sem_move_multi ? 2 cfg L ?)
 147    (sem_seq_app ???????
 148     (sem_if ? 2 ????????
 149      (sem_test_null_multi ?? obj ?)
 150      (sem_seq_app ??????? (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false)))
 151       (sem_seq_app ??????? (sem_inject ???? cfg ? (sem_move_r ?))
 152        (sem_inject ???? cfg ? (sem_write FSUnialpha (bit false))) ?) ?)
 153        ?)
 154     (sem_seq_app ??????? (sem_inject ???? cfg ? (sem_move_to_end_l ?))
 155      (sem_inject ???? cfg ? (sem_move_r ?)) ?) ?) ?) ?)
 156
 157
 158 lemma wsem_copy : ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
 159   copy src dst sig n ⊫ R_copy src dst sig n.
 160 #src #dst #sig #n #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
 161 lapply (sem_while … (sem_copy_step src dst sig n Hneq Hsrc Hdst) … Hloop) //
 162 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
 163 [ whd in ⊢ (%→?); * #Hnone #Hout %
 164   [#_ @Hout
 165   |#ls #x #x0 #rs #ls0 #rs0 #Hsrc1 #Hdst1 @False_ind cases Hnone
 166     [>Hsrc1 normalize #H destruct (H) | >Hdst1 normalize #H destruct (H)]
 167   ]
 168 |#tc #td * #x * #y * * #Hcx #Hcy #Htd #Hstar #IH #He lapply (IH He) -IH *
 169  #IH1 #IH2 %
 170   [* [>Hcx #H destruct (H) | >Hcy #H destruct (H)]
 171   |#ls #x' #y' #rs #ls0 #rs0 #Hnth_src #Hnth_dst
 172    >Hnth_src in Hcx; whd in ⊢ (??%?→?); #H destruct (H)
 173    >Hnth_dst in Hcy; whd in ⊢ (??%?→?); #H destruct (H)
 174    >Hnth_src in Htd; >Hnth_dst -Hnth_src -Hnth_dst
 175    cases rs
 176     [(* the source tape is empty after the move *)
 177      #Htd lapply (IH1 ?)
 178       [%1 >Htd >nth_change_vec_neq [2:@(not_to_not … Hneq) //] >nth_change_vec //]
 179      #Hout (* whd in match (tape_move ???); *) %1 %{([])} %{rs0} %
 180       [% [// | // ]
 181       |whd in match (reverse ??); whd in match (reverse ??);
 182        >Hout >Htd @eq_f2 // cases rs0 //
 183       ]
 184     |#c1 #tl1 cases rs0
 185       [(* the dst tape is empty after the move *)
 186        #Htd lapply (IH1 ?) [%2 >Htd >nth_change_vec //]
 187        #Hout (* whd in match (tape_move ???); *) %2 %{[ ]} %{(c1::tl1)} %
 188         [% [// | // ]
 189         |whd in match (reverse ??); whd in match (reverse ??);
 190          >Hout >Htd @eq_f2 //
 191         ]
 192       |#c2 #tl2 whd in match (tape_move_mono ???); whd in match (tape_move_mono ???);
 193        #Htd
 194        cut (nth src (tape sig) td (niltape sig)=midtape sig (x::ls) c1 tl1)
 195          [>Htd >nth_change_vec_neq [2:@(not_to_not … Hneq) //] @nth_change_vec //]
 196        #Hsrc_td
 197        cut (nth dst (tape sig) td (niltape sig)=midtape sig (x::ls0) c2 tl2)
 198          [>Htd @nth_change_vec //]
 199        #Hdst_td cases (IH2 … Hsrc_td Hdst_td) -Hsrc_td -Hdst_td
 200         [* #rs01 * #rs02 * * #H1 #H2 #H3 %1
 201          %{(c2::rs01)} %{rs02} % [% [@eq_f //|normalize @eq_f @H2]]
 202          >Htd in H3; >change_vec_commute // >change_vec_change_vec
 203          >change_vec_commute [2:@(not_to_not … Hneq) //] >change_vec_change_vec
 204          #H >reverse_cons >associative_append >associative_append @H
 205         |* #rs11 * #rs12 * * #H1 #H2 #H3 %2
 206          %{(c1::rs11)} %{rs12} % [% [@eq_f //|normalize @eq_f @H2]]
 207          >Htd in H3; >change_vec_commute // >change_vec_change_vec
 208          >change_vec_commute [2:@(not_to_not … Hneq) //] >change_vec_change_vec
 209          #H >reverse_cons >associative_append >associative_append @H
 210         ]
 211       ]
 212     ]
 213   ]
 214 qed.
 215
 216
 217 lemma terminate_copy :  ∀src,dst,sig,n,t.
 218   src ≠ dst → src < S n → dst < S n → copy src dst sig n ↓ t.
 219 #src #dst #sig #n #t #Hneq #Hsrc #Hdts
 220 @(terminate_while … (sem_copy_step …)) //
 221 <(change_vec_same … t src (niltape ?))
 222 cases (nth src (tape sig) t (niltape ?))
 223 [ % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 224 |2,3: #a0 #al0 % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 225 | #ls #c #rs lapply c -c lapply ls -ls lapply t -t elim rs
 226   [#t #ls #c % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?);
 227    #H1 destruct (H1) #_ >change_vec_change_vec #Ht1 %
 228    #t2 * #x0 * #y0 * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
 229    >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H)
 230   |#r0 #rs0 #IH #t #ls #c % #t1 * #x * #y * * >nth_change_vec //
 231    normalize in ⊢ (%→?); #H destruct (H) #Hcur
 232    >change_vec_change_vec >change_vec_commute // #Ht1 >Ht1 @IH
 233   ]
 234 ]
 235 qed.
 236
 237 lemma sem_copy : ∀src,dst,sig,n.
 238   src ≠ dst → src < S n → dst < S n →
 239   copy src dst sig n ⊨ R_copy src dst sig n.
 240 #i #j #sig #n #Hneq #Hi #Hj @WRealize_to_Realize [/2/| @wsem_copy // ]
 241 qed.