matita/matita/lib/turing/auxiliary_multi_machines.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/basic_machines.ma".
  13 include "turing/if_multi.ma".
  14 include "turing/while_multi.ma".
  15 include "turing/inject.ma".
  16 include "turing/basic_multi_machines.ma".
  17
  18 (**************************** injected machines *******************************)
  19
  20 definition Rtc_multi_true ≝
  21   λalpha,test,n,i.λt1,t2:Vector ? (S n).
  22    (∃c. current alpha (nth i ? t1 (niltape ?)) = Some ? c ∧ test c = true) ∧ t2 = t1.
  23
  24 definition Rtc_multi_false ≝
  25   λalpha,test,n,i.λt1,t2:Vector ? (S n).
  26     (∀c. current alpha (nth i ? t1 (niltape ?)) = Some ? c → test c = false) ∧ t2 = t1.
  27
  28 lemma sem_test_char_multi :
  29   ∀alpha,test,n,i.i ≤ n →
  30   inject_TM ? (test_char ? test) n i ⊨
  31   [ tc_true : Rtc_multi_true alpha test n i, Rtc_multi_false alpha test n i ].
  32 #alpha #test #n #i #Hin #int
  33 cases (acc_sem_inject … Hin (sem_test_char alpha test) int)
  34 #k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ %
  35 [ @Hloop
  36 | #Hqtrue lapply (Htrue Hqtrue) * * * #c *
  37   #Hcur #Htestc #Hnth_i #Hnth_j %
  38   [ %{c} % //
  39   | @(eq_vec … (niltape ?)) #i0 #Hi0
  40     cases (decidable_eq_nat i0 i) #Hi0i
  41     [ >Hi0i @Hnth_i
  42     | @sym_eq @Hnth_j @sym_not_eq // ] ] ]
  43 | #Hqfalse lapply (Hfalse Hqfalse) * * #Htestc #Hnth_i #Hnth_j %
  44   [ @Htestc
  45   | @(eq_vec … (niltape ?)) #i0 #Hi0
  46     cases (decidable_eq_nat i0 i) #Hi0i
  47     [ >Hi0i @Hnth_i
  48     | @sym_eq @Hnth_j @sym_not_eq // ] ] ]
  49 qed.
  50
  51 definition Rm_test_null_true ≝
  52   λalpha,n,i.λt1,t2:Vector ? (S n).
  53    current alpha (nth i ? t1 (niltape ?)) ≠ None ? ∧ t2 = t1.
  54
  55 definition Rm_test_null_false ≝
  56   λalpha,n,i.λt1,t2:Vector ? (S n).
  57     current alpha (nth i ? t1 (niltape ?)) = None ? ∧ t2 = t1.
  58
  59 lemma sem_test_null_multi : ∀alpha,n,i.i ≤ n →
  60   inject_TM ? (test_null ?) n i ⊨
  61     [ tc_true : Rm_test_null_true alpha n i, Rm_test_null_false alpha n i ].
  62 #alpha #n #i #Hin #int
  63 cases (acc_sem_inject … Hin (sem_test_null alpha) int)
  64 #k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ %
  65 [ @Hloop
  66 | #Hqtrue lapply (Htrue Hqtrue) * * #Hcur #Hnth_i #Hnth_j % //
  67   @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) #Hi0i
  68   [ >Hi0i @sym_eq @Hnth_i | @sym_eq @Hnth_j @sym_not_eq // ] ]
  69 | #Hqfalse lapply (Hfalse Hqfalse) * * #Hcur #Hnth_i #Hnth_j %
  70   [ @Hcur
  71   | @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) //
  72     #Hi0i @sym_eq @Hnth_j @sym_not_eq // ] ]
  73 qed.
  74
  75 (* move a single tape *)
  76 definition mmove ≝ λi,sig,n,D.inject_TM sig (move sig D) n i.
  77
  78 definition Rm_multi ≝
  79   λalpha,n,i,D.λt1,t2:Vector ? (S n).
  80   t2 = change_vec ? (S n) t1 (tape_move alpha (nth i ? t1 (niltape ?)) D) i.
  81
  82 lemma sem_move_multi :
  83   ∀alpha,n,i,D.i ≤ n →
  84   mmove i alpha n D ⊨ Rm_multi alpha n i D.
  85 #alpha #n #i #D #Hin #ta cases (sem_inject … Hin (sem_move_single alpha D) ta)
  86 #k * #outc * #Hloop * whd in ⊢ (%→?); #Htb1 #Htb2 %{k} %{outc} % [ @Hloop ]
  87 whd @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) #Hi0i
  88 [ >Hi0i >Htb1 >nth_change_vec //
  89 | >nth_change_vec_neq [|@sym_not_eq //] <Htb2 // @sym_not_eq // ]
  90 qed.
  91
  92 (********************** look_ahead test *************************)
  93
  94 definition mtestR ≝ λsig,i,n,test.
  95   (mmove i sig n R) ·
  96     (ifTM ?? (inject_TM ? (test_char ? test) n i)
  97     (single_finalTM ?? (mmove i sig n L))
  98     (mmove i sig n L) tc_true).
  99
 100
 101 (* underspecified *)
 102 definition RmtestR_true ≝ λsig,i,n,test.λt1,t2:Vector ? n.
 103   ∀ls,c,c1,rs.
 104     nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
 105     t1 = t2 ∧ (test c1 = true).
 106
 107 definition RmtestR_false ≝ λsig,i,n,test.λt1,t2:Vector ? n.
 108   ∀ls,c,c1,rs.
 109     nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
 110     t1 = t2 ∧ (test c1 = false).
 111
 112 definition mtestR_acc: ∀sig,i,n,test.states ?? (mtestR sig i n test).
 113 #sig #i #n #test @inr @inr @inl @inr @start_nop
 114 qed.
 115
 116 lemma sem_mtestR: ∀sig,i,n,test. i ≤ n →
 117   mtestR sig i n test ⊨
 118     [mtestR_acc sig i n test:
 119        RmtestR_true sig  i (S n) test, RmtestR_false sig i (S n) test].
 120 #sig #i #n #test #Hlein
 121 @(acc_sem_seq_app sig n … (sem_move_multi … R Hlein)
 122    (acc_sem_if sig n ????????
 123      (sem_test_char_multi sig test n i Hlein)
 124      (sem_move_multi … L Hlein)
 125      (sem_move_multi … L Hlein)))
 126   [#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in  ⊢ (%→?); * *
 127    #cx #Hcx #Htx #Ht2 #ls #c #c1 #rs #Ht1
 128    >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
 129    >Ht3 in Hcx; >nth_change_vec [|@le_S_S //] * whd in ⊢ (??%?→?);
 130    #Hsome destruct (Hsome) #Htest % [2:@Htest]
 131    >Htx in Ht2; whd in ⊢ (%→?); #Ht2 @(eq_vec … (niltape ?))
 132    #j #lejn cases (true_or_false (eqb i j)) #Hij
 133     [lapply lejn <(eqb_true_to_eq … Hij) #lein >Ht2 >nth_change_vec [2://]
 134      >Ht3 >nth_change_vec >Ht1 //
 135     |lapply (eqb_false_to_not_eq … Hij) #Hneq >Ht2 >nth_change_vec_neq [2://]
 136      >Ht3 >nth_change_vec_neq //
 137     ]
 138   |#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in  ⊢ (%→?); *
 139    #Hcx #Heqtx #Htx #ls #c #c1 #rs #Ht1
 140    >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
 141    >Ht3 in Hcx; >nth_change_vec [2:@le_S_S //] #Hcx lapply (Hcx ? (refl ??))
 142    #Htest % // @(eq_vec … (niltape ?))
 143    #j #lejn cases (true_or_false (eqb i j)) #Hij
 144     [lapply lejn <(eqb_true_to_eq … Hij) #lein >Htx >nth_change_vec [2://]
 145      >Heqtx >Ht3 >nth_change_vec >Ht1 //
 146     |lapply (eqb_false_to_not_eq … Hij) #Hneq >Htx >nth_change_vec_neq [2://]
 147      >Heqtx >Ht3 >nth_change_vec_neq //
 148     ]
 149   ]
 150 qed.
 151 (* advance in parallel along two tapes src and dst until we reach the end
 152    of one tape *)
 153
 154 definition parmove ≝ λsrc,dst,sig,n,D.
 155   whileTM … (parmove_step src dst sig n D) parmove1.
 156
 157 definition R_parmoveL ≝
 158   λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
 159   (∀x,xs,rs.
 160     nth src ? int (niltape ?) = midtape sig xs x rs →
 161     ∀ls0,x0,target,rs0.|xs| = |target| →
 162     nth dst ? int (niltape ?) = midtape sig (target@ls0) x0 rs0 →
 163     outt = change_vec ??
 164            (change_vec ?? int (mk_tape sig [] (None ?) (reverse ? xs@x::rs)) src)
 165            (mk_tape sig (tail ? ls0) (option_hd ? ls0) (reverse ? target@x0::rs0)) dst) ∧
 166   (∀x,xs,rs.
 167     nth dst ? int (niltape ?) = midtape sig xs x rs →
 168     ∀ls0,x0,target,rs0.|xs| = |target| →
 169     nth src ? int (niltape ?) = midtape sig (target@ls0) x0 rs0 →
 170     outt = change_vec ??
 171            (change_vec ?? int (mk_tape sig [] (None ?) (reverse ? xs@x::rs)) dst)
 172            (mk_tape sig (tail ? ls0) (option_hd ? ls0) (reverse ? target@x0::rs0)) src) ∧
 173   ((current ? (nth src ? int (niltape ?)) = None ? ∨
 174     current ? (nth dst ? int (niltape ?)) = None ?) →
 175     outt = int).
 176
 177 lemma wsem_parmoveL : ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
 178   parmove src dst sig n L ⊫ R_parmoveL src dst sig n.
 179 #src #dst #sig #n #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
 180 lapply (sem_while … (sem_parmove_step src dst sig n L Hneq Hsrc Hdst) … Hloop) //
 181 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
 182 [ whd in ⊢ (%→?); * #H #Houtc % [2: #_ @Houtc ] cases H #Hcurtb
 183   [ %
 184     [ #x #xs #rs #Hsrctb >Hsrctb in Hcurtb; normalize in ⊢ (%→?);
 185       #Hfalse destruct (Hfalse)
 186     | #x #xs #rs #Hdsttb #ls0 #x0 #target #rs0 #Hlen #Hsrctb >Hsrctb in Hcurtb;
 187       normalize in ⊢ (%→?); #H destruct (H)
 188     ]
 189   | %
 190     [ #x #xs #rs #Hsrctb #ls0 #x0 #target
 191       #rs0 #Hlen #Hdsttb >Hdsttb in Hcurtb; normalize in ⊢ (%→?); #H destruct (H)
 192     | #x #xs #rs #Hdsttb >Hdsttb in Hcurtb; normalize in ⊢ (%→?);
 193       #Hfalse destruct (Hfalse)
 194     ]
 195   ]
 196 | #td #te * #c0 * #c1 * * #Hc0 #Hc1 #Hd #Hstar #IH #He
 197   lapply (IH He) -IH * * #IH1a #IH1b #IH2 % [ %
 198   [ #x #xs #rs #Hsrc_td #ls0 #x0 #target
 199     #rs0 #Hlen #Hdst_td
 200     >Hsrc_td in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
 201     >Hdst_td in Hd; >Hsrc_td @(list_cases2 … Hlen)
 202     [ #Hxsnil #Htargetnil >Hxsnil >Htargetnil #Hd >IH2
 203       [2: %1 >Hd >nth_change_vec_neq [|@(sym_not_eq … Hneq)]
 204       >nth_change_vec //]
 205       >Hd -Hd @(eq_vec … (niltape ?))
 206       #i #Hi cases (decidable_eq_nat i src) #Hisrc
 207       [ >Hisrc >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
 208         >nth_change_vec //
 209         >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
 210         >nth_change_vec //
 211       | cases (decidable_eq_nat i dst) #Hidst
 212         [ >Hidst >nth_change_vec // >nth_change_vec //
 213           >Hdst_td in Hc1; >Htargetnil
 214           normalize in ⊢ (%→?); #Hc1 destruct (Hc1) cases ls0 //
 215         | >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
 216           >nth_change_vec_neq [|@(sym_not_eq … Hisrc)]
 217           >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
 218           >nth_change_vec_neq [|@(sym_not_eq … Hisrc)] %
 219         ]
 220       ]
 221     | #hd1 #hd2 #tl1 #tl2 #Hxs #Htarget >Hxs >Htarget #Hd
 222       >(IH1a hd1 tl1 (c0::rs) ? ls0 hd2 tl2 (x0::rs0))
 223       [ >Hd >(change_vec_commute … ?? td ?? src dst) //
 224         >change_vec_change_vec
 225         >(change_vec_commute … ?? td ?? dst src) [|@sym_not_eq //]
 226         >change_vec_change_vec
 227         >reverse_cons >associative_append
 228         >reverse_cons >associative_append %
 229       | >Hd >nth_change_vec //
 230       | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
 231       | >Hd >nth_change_vec_neq [|@sym_not_eq //]
 232         >nth_change_vec // ]
 233     ]
 234   | #x #xs #rs #Hdst_td #ls0 #x0 #target
 235     #rs0 #Hlen #Hsrc_td
 236     >Hdst_td in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
 237     >Hsrc_td in Hd; >Hdst_td @(list_cases2 … Hlen)
 238     [ #Hxsnil #Htargetnil >Hxsnil >Htargetnil #Hd >IH2
 239       [2: %2 >Hd >nth_change_vec //]
 240       >Hd -Hd @(eq_vec … (niltape ?))
 241       #i #Hi cases (decidable_eq_nat i dst) #Hidst
 242       [ >Hidst >(nth_change_vec_neq … dst src) //
 243         >nth_change_vec // >nth_change_vec //
 244       | cases (decidable_eq_nat i src) #Hisrc
 245         [ >Hisrc >nth_change_vec // >(nth_change_vec_neq …) [|@sym_not_eq //]
 246           >Hsrc_td in Hc1; >Htargetnil
 247           normalize in ⊢ (%→?); #Hc1 destruct (Hc1) >nth_change_vec //
 248           cases ls0 //
 249         | >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
 250           >nth_change_vec_neq [|@(sym_not_eq … Hisrc)]
 251           >nth_change_vec_neq [|@(sym_not_eq … Hisrc)]
 252           >nth_change_vec_neq [|@(sym_not_eq … Hidst)] %
 253         ]
 254       ]
 255     | #hd1 #hd2 #tl1 #tl2 #Hxs #Htarget >Hxs >Htarget #Hd
 256       >(IH1b hd1 tl1 (x::rs) ? ls0 hd2 tl2 (x0::rs0))
 257       [ >Hd >(change_vec_commute … ?? td ?? dst src) [|@sym_not_eq //]
 258         >change_vec_change_vec
 259         >(change_vec_commute … ?? td ?? src dst) //
 260         >change_vec_change_vec
 261         >reverse_cons >associative_append
 262         >reverse_cons >associative_append
 263         >change_vec_commute [|@sym_not_eq //] %
 264       | >Hd >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
 265       | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
 266       | >Hd >nth_change_vec // ]
 267     ]
 268   ]
 269 | >Hc0 >Hc1 * [ #Hc0 destruct (Hc0) | #Hc1 destruct (Hc1) ]
 270 ] ]
 271 qed.
 272
 273 lemma terminate_parmoveL :  ∀src,dst,sig,n,t.
 274   src ≠ dst → src < S n → dst < S n →
 275   parmove src dst sig n L ↓ t.
 276 #src #dst #sig #n #t #Hneq #Hsrc #Hdst
 277 @(terminate_while … (sem_parmove_step …)) //
 278 <(change_vec_same … t src (niltape ?))
 279 cases (nth src (tape sig) t (niltape ?))
 280 [ % #t1 * #x1 * #x2 * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 281 |2,3: #a0 #al0 % #t1 * #x1 * #x2 * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 282 | #ls lapply t -t elim ls
 283   [#t #c #rs % #t1 * #x1 * #x2 * * >nth_change_vec // normalize in ⊢ (%→?);
 284    #H1 destruct (H1) #Hcurdst >change_vec_change_vec #Ht1 %
 285    #t2 * #y1 * #y2 * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
 286    >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H)
 287   |#l0 #ls0 #IH #t #c #rs % #t1 * #x1 * #x2 * * >nth_change_vec //
 288    normalize in ⊢ (%→?); #H destruct (H) #Hcurdst
 289    >change_vec_change_vec >change_vec_commute // #Ht1 >Ht1 @IH
 290   ]
 291 ]
 292 qed.
 293
 294 lemma sem_parmoveL : ∀src,dst,sig,n.
 295   src ≠ dst → src < S n → dst < S n →
 296   parmove src dst sig n L ⊨ R_parmoveL src dst sig n.
 297 #src #dst #sig #n #Hneq #Hsrc #Hdst @WRealize_to_Realize
 298 [/2/ | @wsem_parmoveL //]
 299 qed.
 300
 301 (* compare *)
 302 definition compare ≝ λi,j,sig,n.
 303   whileTM … (compare_step i j sig n) comp1.
 304
 305 (*    (∃rs'.rs = rs0@rs' ∧ current ? (nth j ? outt (niltape ?)) = None ?) ∨
 306     (∃rs0'.rs0 = rs@rs0' ∧
 307      outt = change_vec ??
 308             (change_vec ?? int
 309               (mk_tape sig (reverse sig rs@x::ls) (None sig) []) i)
 310             (mk_tape sig (reverse sig rs@x::ls0) (option_hd sig rs0')
 311             (tail sig rs0')) j) ∨
 312     (∃xs,ci,cj,rs',rs0'.ci ≠ cj ∧ rs = xs@ci::rs' ∧ rs0 = xs@cj::rs0' ∧
 313      outt = change_vec ??
 314             (change_vec ?? int (midtape sig (reverse ? xs@x::ls) ci rs') i)
 315             (midtape sig (reverse ? xs@x::ls0) cj rs0') j)).*)
 316 definition R_compare ≝
 317   λi,j,sig,n.λint,outt: Vector (tape sig) (S n).
 318   ((current ? (nth i ? int (niltape ?)) ≠ current ? (nth j ? int (niltape ?)) ∨
 319     current ? (nth i ? int (niltape ?)) = None ? ∨
 320     current ? (nth j ? int (niltape ?)) = None ?) → outt = int) ∧
 321   (∀ls,x,rs,ls0,rs0.
 322 (*    nth i ? int (niltape ?) = midtape sig ls x (xs@ci::rs) → *)
 323     nth i ? int (niltape ?) = midtape sig ls x rs →
 324     nth j ? int (niltape ?) = midtape sig ls0 x rs0 →
 325     (∃rs'.rs = rs0@rs' ∧
 326      outt = change_vec ??
 327             (change_vec ?? int
 328               (mk_tape sig (reverse sig rs0@x::ls) (option_hd sig rs') (tail ? rs')) i)
 329             (mk_tape sig (reverse sig rs0@x::ls0) (None ?) [ ]) j) ∨
 330     (∃rs0'.rs0 = rs@rs0' ∧
 331      outt = change_vec ??
 332             (change_vec ?? int
 333               (mk_tape sig (reverse sig rs@x::ls) (None sig) []) i)
 334             (mk_tape sig (reverse sig rs@x::ls0) (option_hd sig rs0')
 335             (tail sig rs0')) j) ∨
 336     (∃xs,ci,cj,rs',rs0'.ci ≠ cj ∧ rs = xs@ci::rs' ∧ rs0 = xs@cj::rs0' ∧
 337      outt = change_vec ??
 338             (change_vec ?? int (midtape sig (reverse ? xs@x::ls) ci rs') i)
 339             (midtape sig (reverse ? xs@x::ls0) cj rs0') j)).
 340
 341 lemma wsem_compare : ∀i,j,sig,n.i ≠ j → i < S n → j < S n →
 342   compare i j sig n ⊫ R_compare i j sig n.
 343 #i #j #sig #n #Hneq #Hi #Hj #ta #k #outc #Hloop
 344 lapply (sem_while … (sem_comp_step i j sig n Hneq Hi Hj) … Hloop) //
 345 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
 346 [ whd in ⊢ (%→?); * * [ *
 347  [ #Hcicj #Houtc %
 348    [ #_ @Houtc
 349    | #ls #x #rs #ls0 #rs0 #Hnthi #Hnthj
 350      >Hnthi in Hcicj; >Hnthj normalize in ⊢ (%→?); * #H @False_ind @H %
 351    ]
 352  | #Hci #Houtc %
 353    [ #_ @Houtc
 354    | #ls #x #rs #ls0 #rs0 #Hnthi >Hnthi in Hci;
 355      normalize in ⊢ (%→?); #H destruct (H) ] ]
 356  | #Hcj #Houtc %
 357   [ #_ @Houtc
 358   | #ls #x #rs #ls0 #rs0 #_ #Hnthj >Hnthj in Hcj;
 359     normalize in ⊢ (%→?); #H destruct (H) ] ]
 360 | #td #te * #x * * #Hci #Hcj #Hd #Hstar #IH #He lapply (IH He) -IH *
 361   #IH1 #IH2 %
 362   [ >Hci >Hcj * [ *
 363     [ * #H @False_ind @H % | #H destruct (H)] | #H destruct (H)]
 364   | #ls #c0 #rs #ls0 #rs0 cases rs
 365     [ -IH2 #Hnthi #Hnthj % %2 %{rs0} % [%]
 366       >Hnthi in Hd; #Hd >Hd in IH1; #IH1 >IH1
 367       [| % %2 >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec // % ]
 368       >Hnthj cases rs0 [| #r1 #rs1 ] %
 369     | #r1 #rs1 #Hnthi cases rs0
 370       [ -IH2 #Hnthj % % %{(r1::rs1)} % [%]
 371         >Hnthj in Hd; #Hd >Hd in IH1; #IH1 >IH1
 372         [| %2 >nth_change_vec // ]
 373         >Hnthi >Hnthj %
 374       | #r2 #rs2 #Hnthj lapply IH2; >Hd in IH1; >Hnthi >Hnthj
 375         >nth_change_vec //
 376         >nth_change_vec_neq [| @sym_not_eq // ] >nth_change_vec //
 377         cases (true_or_false (r1 == r2)) #Hr1r2
 378         [ >(\P Hr1r2) #_ #IH2 cases (IH2 … (refl ??) (refl ??)) [ *
 379           [ * #rs' * #Hrs1 #Hcurout_j % % %{rs'}
 380             >Hrs1 %
 381             [ %
 382             | >Hcurout_j >change_vec_commute // >change_vec_change_vec
 383               >change_vec_commute // @sym_not_eq // ]
 384           | * #rs0' * #Hrs2 #Hcurout_i % %2 %{rs0'}
 385             >Hrs2 >Hcurout_i % //
 386             >change_vec_commute // >change_vec_change_vec
 387             >change_vec_commute [|@sym_not_eq//] >change_vec_change_vec
 388             >reverse_cons >associative_append >associative_append % ]
 389           | * #xs * #ci * #cj * #rs' * #rs0' * * * #Hcicj #Hrs1 #Hrs2
 390             >change_vec_commute // >change_vec_change_vec
 391             >change_vec_commute [| @sym_not_eq ] // >change_vec_change_vec
 392             #Houtc %2 %{(r2::xs)} %{ci} %{cj} %{rs'} %{rs0'}
 393             % [ % [ % [ // | >Hrs1 // ] | >Hrs2 // ]
 394               | >reverse_cons >associative_append >associative_append >Houtc % ] ]
 395         | lapply (\Pf Hr1r2) -Hr1r2 #Hr1r2 #IH1 #_ %2
 396           >IH1 [| % % normalize @(not_to_not … Hr1r2) #H destruct (H) % ]
 397           %{[]} %{r1} %{r2} %{rs1} %{rs2} % [ % [ % /2/ | % ] | % ] ]]]]]
 398 qed.
 399
 400 lemma terminate_compare :  ∀i,j,sig,n,t.
 401   i ≠ j → i < S n → j < S n →
 402   compare i j sig n ↓ t.
 403 #i #j #sig #n #t #Hneq #Hi #Hj
 404 @(terminate_while … (sem_comp_step …)) //
 405 <(change_vec_same … t i (niltape ?))
 406 cases (nth i (tape sig) t (niltape ?))
 407 [ % #t1 * #x * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 408 |2,3: #a0 #al0 % #t1 * #x * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 409 | #ls #c #rs lapply c -c lapply ls -ls lapply t -t elim rs
 410   [#t #ls #c % #t1 * #x * * >nth_change_vec // normalize in ⊢ (%→?);
 411    #H1 destruct (H1) #_ >change_vec_change_vec #Ht1 %
 412    #t2 * #x0 * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
 413    >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H)
 414   |#r0 #rs0 #IH #t #ls #c % #t1 * #x * * >nth_change_vec //
 415    normalize in ⊢ (%→?); #H destruct (H) #Hcur
 416    >change_vec_change_vec >change_vec_commute // #Ht1 >Ht1 @IH
 417   ]
 418 ]
 419 qed.
 420
 421 lemma sem_compare : ∀i,j,sig,n.
 422   i ≠ j → i < S n → j < S n →
 423   compare i j sig n ⊨ R_compare i j sig n.
 424 #i #j #sig #n #Hneq #Hi #Hj @WRealize_to_Realize
 425   [/2/| @wsem_compare // ]
 426 qed.
 427
 428 (* copy *)
 429
 430 definition copy ≝ λsrc,dst,sig,n.
 431   whileTM … (copy_step src dst sig n) copy1.
 432
 433 definition R_copy ≝
 434   λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
 435   ((current ? (nth src ? int (niltape ?)) = None ? ∨
 436     current ? (nth dst ? int (niltape ?)) = None ?) → outt = int) ∧
 437   (∀ls,x,x0,rs,ls0,rs0.
 438     nth src ? int (niltape ?) = midtape sig ls x rs →
 439     nth dst ? int (niltape ?) = midtape sig ls0 x0 rs0 →
 440     (∃rs01,rs02.rs0 = rs01@rs02 ∧ |rs01| = |rs| ∧
 441      outt = change_vec ??
 442             (change_vec ?? int
 443               (mk_tape sig (reverse sig rs@x::ls) (None sig) []) src)
 444             (mk_tape sig (reverse sig rs@x::ls0) (option_hd sig rs02)
 445             (tail sig rs02)) dst) ∨
 446     (∃rs1,rs2.rs = rs1@rs2 ∧ |rs1| = |rs0| ∧
 447      outt = change_vec ??
 448             (change_vec ?? int
 449               (mk_tape sig (reverse sig rs1@x::ls) (option_hd sig rs2)
 450             (tail sig rs2)) src)
 451             (mk_tape sig (reverse sig rs1@x::ls0) (None sig) []) dst)).
 452
 453 lemma wsem_copy : ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
 454   copy src dst sig n ⊫ R_copy src dst sig n.
 455 #src #dst #sig #n #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
 456 lapply (sem_while … (sem_copy_step src dst sig n Hneq Hsrc Hdst) … Hloop) //
 457 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
 458 [ whd in ⊢ (%→?); * #Hnone #Hout %
 459   [#_ @Hout
 460   |#ls #x #x0 #rs #ls0 #rs0 #Hsrc1 #Hdst1 @False_ind cases Hnone
 461     [>Hsrc1 normalize #H destruct (H) | >Hdst1 normalize #H destruct (H)]
 462   ]
 463 |#tc #td * #x * #y * * #Hcx #Hcy #Htd #Hstar #IH #He lapply (IH He) -IH *
 464  #IH1 #IH2 %
 465   [* [>Hcx #H destruct (H) | >Hcy #H destruct (H)]
 466   |#ls #x' #y' #rs #ls0 #rs0 #Hnth_src #Hnth_dst
 467    >Hnth_src in Hcx; whd in ⊢ (??%?→?); #H destruct (H)
 468    >Hnth_dst in Hcy; whd in ⊢ (??%?→?); #H destruct (H)
 469    >Hnth_src in Htd; >Hnth_dst -Hnth_src -Hnth_dst
 470    cases rs
 471     [(* the source tape is empty after the move *)
 472      #Htd lapply (IH1 ?)
 473       [%1 >Htd >nth_change_vec_neq [2:@(not_to_not … Hneq) //] >nth_change_vec //]
 474      #Hout (* whd in match (tape_move ???); *) %1 %{([])} %{rs0} %
 475       [% [// | // ]
 476       |whd in match (reverse ??); whd in match (reverse ??);
 477        >Hout >Htd @eq_f2 // cases rs0 //
 478       ]
 479     |#c1 #tl1 cases rs0
 480       [(* the dst tape is empty after the move *)
 481        #Htd lapply (IH1 ?) [%2 >Htd >nth_change_vec //]
 482        #Hout (* whd in match (tape_move ???); *) %2 %{[ ]} %{(c1::tl1)} %
 483         [% [// | // ]
 484         |whd in match (reverse ??); whd in match (reverse ??);
 485          >Hout >Htd @eq_f2 //
 486         ]
 487       |#c2 #tl2 whd in match (tape_move_mono ???); whd in match (tape_move_mono ???);
 488        #Htd
 489        cut (nth src (tape sig) td (niltape sig)=midtape sig (x::ls) c1 tl1)
 490          [>Htd >nth_change_vec_neq [2:@(not_to_not … Hneq) //] @nth_change_vec //]
 491        #Hsrc_td
 492        cut (nth dst (tape sig) td (niltape sig)=midtape sig (x::ls0) c2 tl2)
 493          [>Htd @nth_change_vec //]
 494        #Hdst_td cases (IH2 … Hsrc_td Hdst_td) -Hsrc_td -Hdst_td
 495         [* #rs01 * #rs02 * * #H1 #H2 #H3 %1
 496          %{(c2::rs01)} %{rs02} % [% [@eq_f //|normalize @eq_f @H2]]
 497          >Htd in H3; >change_vec_commute // >change_vec_change_vec
 498          >change_vec_commute [2:@(not_to_not … Hneq) //] >change_vec_change_vec
 499          #H >reverse_cons >associative_append >associative_append @H
 500         |* #rs11 * #rs12 * * #H1 #H2 #H3 %2
 501          %{(c1::rs11)} %{rs12} % [% [@eq_f //|normalize @eq_f @H2]]
 502          >Htd in H3; >change_vec_commute // >change_vec_change_vec
 503          >change_vec_commute [2:@(not_to_not … Hneq) //] >change_vec_change_vec
 504          #H >reverse_cons >associative_append >associative_append @H
 505         ]
 506       ]
 507     ]
 508   ]
 509 qed.
 510
 511
 512 lemma terminate_copy :  ∀src,dst,sig,n,t.
 513   src ≠ dst → src < S n → dst < S n → copy src dst sig n ↓ t.
 514 #src #dst #sig #n #t #Hneq #Hsrc #Hdts
 515 @(terminate_while … (sem_copy_step …)) //
 516 <(change_vec_same … t src (niltape ?))
 517 cases (nth src (tape sig) t (niltape ?))
 518 [ % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 519 |2,3: #a0 #al0 % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 520 | #ls #c #rs lapply c -c lapply ls -ls lapply t -t elim rs
 521   [#t #ls #c % #t1 * #x * #y * * >nth_change_vec // normalize in ⊢ (%→?);
 522    #H1 destruct (H1) #_ >change_vec_change_vec #Ht1 %
 523    #t2 * #x0 * #y0 * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
 524    >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H)
 525   |#r0 #rs0 #IH #t #ls #c % #t1 * #x * #y * * >nth_change_vec //
 526    normalize in ⊢ (%→?); #H destruct (H) #Hcur
 527    >change_vec_change_vec >change_vec_commute // #Ht1 >Ht1 @IH
 528   ]
 529 ]
 530 qed.
 531
 532 lemma sem_copy : ∀src,dst,sig,n.
 533   src ≠ dst → src < S n → dst < S n →
 534   copy src dst sig n ⊨ R_copy src dst sig n.
 535 #i #j #sig #n #Hneq #Hi #Hj @WRealize_to_Realize [/2/| @wsem_copy // ]
 536 qed.