-lemma sem_comp_step :
- ∀i,j,sig,n.i ≠ j → i < S n → j < S n →
- compare_step i j sig n ⊨
- [ comp1: R_comp_step_true i j sig n,
- R_comp_step_false i j sig n ].
-#i #j #sig #n #Hneq #Hi #Hj #int
-lapply (refl ? (current ? (nth i ? int (niltape ?))))
-cases (current ? (nth i ? int (niltape ?))) in ⊢ (???%→?);
-[ #Hcuri %{2} %
- [| % [ %
- [ whd in ⊢ (??%?); >comp_q0_q2_null /2/ % <Hcuri in ⊢ (???%);
- @sym_eq @nth_vec_map
- | normalize in ⊢ (%→?); #H destruct (H) ]
- | #_ % // % %2 // ] ]
-| #a #Ha lapply (refl ? (current ? (nth j ? int (niltape ?))))
- cases (current ? (nth j ? int (niltape ?))) in ⊢ (???%→?);
- [ #Hcurj %{2} %
- [| % [ %
- [ whd in ⊢ (??%?); >comp_q0_q2_null /2/ %2 <Hcurj in ⊢ (???%);
- @sym_eq @nth_vec_map
- | normalize in ⊢ (%→?); #H destruct (H) ]
- | #_ % >Ha >Hcurj % % % #H destruct (H) ] ]
- | #b #Hb %{2} cases (true_or_false (a == b)) #Hab
- [ %
- [| % [ %
- [whd in ⊢ (??%?); >(comp_q0_q1 … a Hneq Hi Hj) //
- [>(\P Hab) <Hb @sym_eq @nth_vec_map
- |<Ha @sym_eq @nth_vec_map ]
- | #_ whd >(\P Hab) %{b} % // % // <(\P Hab) // ]
- | * #H @False_ind @H %
- ] ]
- | %
- [| % [ %
- [whd in ⊢ (??%?); >comp_q0_q2_neq //
- <(nth_vec_map ?? (current …) i ? int (niltape ?))
- <(nth_vec_map ?? (current …) j ? int (niltape ?)) >Ha >Hb
- @(not_to_not ??? (\Pf Hab)) #H destruct (H) %
- | normalize in ⊢ (%→?); #H destruct (H) ]
- | #_ % // % % >Ha >Hb @(not_to_not ??? (\Pf Hab)) #H destruct (H) % ] ]
+definition match_step ≝ λsrc,dst,sig,n.
+ compare src dst sig n ·
+ (ifTM ?? (partest sig n (match_test src dst sig ?))
+ (single_finalTM ??
+ (rewind src dst sig n · (inject_TM ? (move_r ?) n dst)))
+ (nop …)
+ partest1).
+
+(* we assume the src is a midtape
+ we stop
+ if the dst is out of bounds (outt = int)
+ or dst.right is shorter than src.right (outt.current → None)
+ or src.right is a prefix of dst.right (out = just right of the common prefix) *)
+definition R_match_step_false ≝
+ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
+ ∀ls,x,xs.
+ nth src ? int (niltape ?) = midtape sig ls x xs →
+ ((current sig (nth dst (tape sig) int (niltape sig)) = None ?) ∧ outt = int) ∨
+ (∃ls0,rs0,xs0. nth dst ? int (niltape ?) = midtape sig ls0 x rs0 ∧
+ xs = rs0@xs0 ∧
+ outt = change_vec ??
+ (change_vec ?? int (mk_tape sig (reverse ? rs0@x::ls) (option_hd ? xs0) (tail ? xs0)) src)
+ (mk_tape ? (reverse ? rs0@x::ls0) (None ?) [ ]) dst) ∨
+ (∃ls0,rs0.
+ nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) ∧
+ (* ∀rsj,c.
+ rs0 = c::rsj → *)
+ outt = change_vec ??
+ (change_vec ?? int (mk_tape sig (reverse ? xs@x::ls) (None ?) [ ]) src)
+ (mk_tape sig (reverse ? xs@x::ls0) (option_hd ? rs0) (tail ? rs0)) dst).
+
+(*
+ we assume the src is a midtape [ ] s rs
+ if we iterate
+ then dst.current = Some ? s1
+ and if s ≠ s1 then outt = int.dst.move_right()
+ and if s = s1
+ then int.src.right and int.dst.right have a common prefix
+ and the heads of their suffixes are different
+ and outt = int.dst.move_right().
+
+ *)
+definition R_match_step_true ≝
+ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
+ ∀s,rs.nth src ? int (niltape ?) = midtape ? [ ] s rs →
+ outt = change_vec ?? int
+ (tape_move_mono … (nth dst ? int (niltape ?)) (〈None ?,R〉)) dst ∧
+ (∃s0.current sig (nth dst (tape sig) int (niltape sig)) = Some ? s0 ∧
+ (s0 = s →
+ ∃xs,ci,rs',ls0,cj,rs0.
+ rs = xs@ci::rs' ∧
+ nth dst ? int (niltape ?) = midtape sig ls0 s (xs@cj::rs0) ∧
+ ci ≠ cj)).
+
+lemma sem_match_step :
+ ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
+ match_step src dst sig n ⊨
+ [ inr ?? (inr ?? (inl … (inr ?? start_nop))) :
+ R_match_step_true src dst sig n,
+ R_match_step_false src dst sig n ].
+#src #dst #sig #n #Hneq #Hsrc #Hdst
+@(acc_sem_seq_app sig n … (sem_compare src dst sig n Hneq Hsrc Hdst)
+ (acc_sem_if ? n … (sem_partest sig n (match_test src dst sig ?))
+ (sem_seq …
+ (sem_rewind ???? Hneq Hsrc Hdst)
+ (sem_inject … dst (le_S_S_to_le … Hdst) (sem_move_r ? )))
+ (sem_nop …)))
+[ #ta #tb #tc * lapply (refl ? (current ? (nth src ? ta (niltape ?))))
+ cases (current ? (nth src ? ta (niltape ?))) in ⊢ (???%→%);
+ [ #Hcurta_src #Hcomp #_ * #td * >Hcomp [| % %2 %]
+ whd in ⊢ (%→?); * whd in ⊢ (??%?→?);
+ >nth_current_chars >Hcurta_src normalize in ⊢ (%→?); #H destruct (H)
+ | #s #Hs lapply (refl ? (current ? (nth dst ? ta (niltape ?))))
+ cases (current ? (nth dst ? ta (niltape ?))) in ⊢ (???%→%);
+ [ #Hcurta_dst #Hcomp #_ * #td * >Hcomp [| %2 %]
+ whd in ⊢ (%→?); * whd in ⊢ (??%?→?);
+ >nth_current_chars >nth_current_chars >Hs >Hcurta_dst
+ normalize in ⊢ (%→?); #H destruct (H)
+ | #s0 #Hs0
+ cases (current_to_midtape … Hs) #ls * #rs #Hmidta_src >Hmidta_src
+ cases (current_to_midtape … Hs0) #ls0 * #rs0 #Hmidta_dst >Hmidta_dst
+ cases (true_or_false (s == s0)) #Hss0
+ [ lapply (\P Hss0) -Hss0 #Hss0 destruct (Hss0)
+ #_ #Hcomp cases (Hcomp ????? (refl ??) (refl ??)) -Hcomp [ *
+ [ * #rs' * #_ #Hcurtc_dst * #td * whd in ⊢ (%→?); * whd in ⊢ (??%?→?);
+ >nth_current_chars >nth_current_chars >Hcurtc_dst
+ cases (current ? (nth src …))
+ [normalize in ⊢ (%→?); #H destruct (H)
+ | #x >nth_change_vec // cases (reverse ? rs0)
+ [ normalize in ⊢ (%→?); #H destruct (H)
+ | #r1 #rs1 normalize in ⊢ (%→?); #H destruct (H) ] ]
+ | * #rs0' * #_ #Hcurtc_src * #td * whd in ⊢ (%→?); * whd in ⊢ (??%?→?);
+ >(?:nth src ? (current_chars ?? tc) (None ?) = None ?)
+ [|>nth_current_chars >Hcurtc_src >nth_change_vec_neq
+ [>nth_change_vec [cases (append ???) // | @Hsrc]
+ |@(not_to_not … Hneq) //
+ ]]
+ normalize in ⊢ (%→?); #H destruct (H) ]
+ | * #xs * #ci * #cj * #rs'' * #rs0' * * * #Hcicj #Hrs #Hrs0
+ #Htc * #td * * #Hmatch #Htd destruct (Htd) * #te * *
+ >Htc >change_vec_commute // >nth_change_vec //
+ >change_vec_commute [|@sym_not_eq //] >nth_change_vec // #Hte #_ #Htb
+ #s' #rs' >Hmidta_src #H destruct (H)
+ lapply (Hte … (refl ??) … (refl ??) (refl ??)) -Hte
+ >change_vec_commute // >change_vec_change_vec
+ >change_vec_commute [|@sym_not_eq //] >change_vec_change_vec #Hte
+ >Hte in Htb; * * #_ >nth_change_vec // #Htb1
+ lapply (Htb1 … (refl ??)) -Htb1 #Htb1 #Htb2 %
+ [ @(eq_vec … (niltape ?)) #i #Hi
+ cases (true_or_false ((dst : DeqNat) == i)) #Hdsti
+ [ <(\P Hdsti) >Htb1 >nth_change_vec // >Hmidta_dst
+ >Hrs0 >reverse_reverse cases xs [|#r1 #rs1] %
+ | <Htb2 [|@(\Pf Hdsti)] >nth_change_vec_neq [| @(\Pf Hdsti)]
+ >Hrs0 >reverse_reverse >nth_change_vec_neq in ⊢ (???%);
+ <Hrs <Hmidta_src [|@(\Pf Hdsti)] >change_vec_same % ]
+ | >Hmidta_dst %{s'} % [%] #_
+ >Hrs0 %{xs} %{ci} %{rs''} %{ls0} %{cj} %{rs0'} % // % //
+ ]
+ ]
+ | lapply (\Pf Hss0) -Hss0 #Hss0 #Htc cut (tc = ta)
+ [@Htc % % @(not_to_not ??? Hss0) #H destruct (H) %]
+ -Htc #Htc destruct (Htc) #_ * #td * whd in ⊢ (%→?); * #_
+ #Htd destruct (Htd) * #te * * #_ #Hte * * #_ #Htb1 #Htb2
+ #s1 #rs1 >Hmidta_src #H destruct (H)
+ lapply (Hte … Hmidta_src … Hmidta_dst) -Hte #Hte destruct (Hte) %
+ [ @(eq_vec … (niltape ?)) #i #Hi
+ cases (true_or_false ((dst : DeqNat) == i)) #Hdsti
+ [ <(\P Hdsti) >(Htb1 … Hmidta_dst) >nth_change_vec // >Hmidta_dst
+ cases rs0 [|#r2 #rs2] %
+ | <Htb2 [|@(\Pf Hdsti)] >nth_change_vec_neq [| @(\Pf Hdsti)] % ]
+ | >Hs0 %{s0} % // #H destruct (H) @False_ind cases (Hss0) /2/ ]
+ ]