(midtape sig ls0 y0 (reverse ? target@y::rs0)) src) ∧
(∀x,rs.nth src ? int (niltape ?) = midtape sig [] x rs →
∀ls0,y,rs0.nth dst ? int (niltape ?) = midtape sig ls0 y rs0 →
+ outt = int) ∧
+ (∀x,rs.nth dst ? int (niltape ?) = midtape sig [] x rs →
+ ∀ls0,y,rs0.nth src ? int (niltape ?) = midtape sig ls0 y rs0 →
outt = int).
definition R_rewind ≝ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
@(sem_seq_app sig n ????? (sem_parmoveL src dst sig n Hneq Hsrc Hdst) ?)
[| @(sem_seq_app sig n ????? (sem_move_multi … R ?) (sem_move_multi … R ?)) //
@le_S_S_to_le // ]
-#ta #tb * #tc * * * #Htc1 #Htc2 #_ * #td * whd in ⊢ (%→%→?); #Htd #Htb % [ %
+#ta #tb * #tc * * * #Htc1 #Htc2 #_ * #td * whd in ⊢ (%→%→?); #Htd #Htb % [ % [ %
[ #x #x0 #xs #rs #Hmidta_src #ls0 #y #y0 #target #rs0 #Hlen #Hmidta_dst
>(Htc1 ??? Hmidta_src ls0 y (target@[y0]) rs0 ??) in Htd;
[|>Hmidta_dst //
>nth_change_vec // >change_vec_change_vec
whd in match (tape_move ???);whd in match (tape_move ???); <Hmidta_src
<Hls0 <Hmidta_dst >change_vec_same >change_vec_same //
-]]
+ ] ]
+| #x #rs #Hmidta_dst #ls0 #y #rs0 #Hmidta_src
+ lapply (Htc2 … Hmidta_dst … (refl ??) Hmidta_src) -Htc2 #Htc >Htc in Htd;
+ >change_vec_change_vec >change_vec_commute [|@sym_not_eq //]
+ >nth_change_vec // lapply (refl ? ls0) cases ls0 in ⊢ (???%→%);
+ [ #Hls0 destruct (Hls0) #Htd >Htd in Htb;
+ >nth_change_vec // >change_vec_change_vec
+ whd in match (tape_move ???);whd in match (tape_move ???);
+ <Hmidta_src <Hmidta_dst >change_vec_same >change_vec_same //
+ | #l1 #ls1 #Hls0 destruct (Hls0) #Htd >Htd in Htb;
+ >nth_change_vec // >change_vec_change_vec
+ whd in match (tape_move ???); whd in match (tape_move ???); <Hmidta_src
+ <Hmidta_dst >change_vec_same >change_vec_same //
+ ]
+]
qed.
lemma sem_rewind : ∀src,dst,sig,n.
src ≠ dst → src < S n → dst < S n →
rewind src dst sig n ⊨ R_rewind src dst sig n.
#src #dst #sig #n #Hneq #Hsrc #Hdst @(Realize_to_Realize … (sem_rewind_strong …)) //
-#ta #tb * * #H1 #H2 #H3 % /2/
+#ta #tb * * * #H1 #H2 #H3 #H4 % /2/
qed.
definition match_step ≝ λsrc,dst,sig,n.
axiom daemon : ∀P:Prop.P.
+(* XXX: move to turing (or mono) *)
+definition option_cons ≝ λsig.λc:option sig.λl.
+ match c with [ None ⇒ l | Some c0 ⇒ c0::l ].
+
definition R_match_step_true_naive ≝
λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
|left ? (nth src ? outt (niltape ?))| +
- |right ? (nth dst ? outt (niltape ?))| <
+ |option_cons ? (current ? (nth dst ? outt (niltape ?))) (right ? (nth dst ? outt (niltape ?)))| <
|left ? (nth src ? int (niltape ?))| +
- |right ? (nth dst ? int (niltape ?))|.
+ |option_cons ? (current ? (nth dst ? int (niltape ?))) (right ? (nth dst ? int (niltape ?)))|.
axiom right_mk_tape : ∀sig,ls,c,rs.right ? (mk_tape sig ls c rs) = rs.
axiom left_mk_tape : ∀sig,ls,c,rs.left ? (mk_tape sig ls c rs) = ls.
+axiom current_mk_tape : ∀sig,ls,c,rs.current ? (mk_tape sig ls c rs) = c.
axiom length_tail : ∀A,l.0 < |l| → |tail A l| < |l|.
axiom lists_length_split :
∀A.∀l1,l2:list A.(∃la,lb.(|la| = |l1| ∧ l2 = la@lb) ∨ (|la| = |l2| ∧ l1 = la@lb)).
+axiom opt_cons_tail_expand : ∀A,l.l = option_cons A (option_hd ? l) (tail ? l).
lemma sem_match_step_termination :
∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
]]
normalize in ⊢ (%→?); #H destruct (H) ]
| * #xs * #ci * #cj * #rs'' * #rs0' * * * #Hcicj #Hrs #Hrs0
- #Htc * #td * * #Hmatch #Htd destruct (Htd) * #te * *
+ #Htc * #td * * #Hmatch #Htd destruct (Htd) * #te * * *
>Htc >change_vec_commute // >nth_change_vec //
>change_vec_commute [|@sym_not_eq //] >nth_change_vec //
cases (lists_length_split ? ls ls0) #lsa * #lsb * * #Hlen #Hlsalsb
[ #Hte #_ #_ <(reverse_reverse … ls) in Hte; <(reverse_reverse … lsa)
cut (|reverse ? lsa| = |reverse ? ls|) [ // ] #Hlen'
@(list_cases2 … Hlen')
- [ #H1 #H2 >H1 >H2 -H1 -H2 normalize in match (reverse ? [ ]); #Hte
+ [ #H1 #H2 >H1 >H2 -H1 -H2 normalize in match (reverse ? [ ]); #Hte #_
lapply (Hte … (refl ??) … (refl ??) (refl ??)) -Hte
>change_vec_commute // >change_vec_change_vec
>change_vec_commute [|@sym_not_eq //] >change_vec_change_vec #Hte
[@daemon] -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec //
>nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
>right_mk_tape normalize in match (left ??);
- >Hmidta_src >Hmidta_dst >length_tail >Hrs0 >length_append
- normalize in ⊢ (?(?%)(?%?)); >commutative_plus //
+ >Hmidta_src >Hmidta_dst >current_mk_tape <opt_cons_tail_expand
+ whd in match (option_cons ???); >Hrs0
+ normalize in ⊢ (?(?%)%); //
| #hda #hdb #tla #tlb #H1 #H2 >H1 >H2
>reverse_cons >reverse_cons #Hte
lapply (Hte ci hdb (reverse ? xs@s0::reverse ? tlb) rs'' ?
>H1 in Hlen'; >H2 whd in ⊢ (??%%→?); #Hlen'
>length_reverse >length_reverse destruct (Hlen') //
| /2 by refl, trans_eq/ ] -Hte
- #Hte * * #_ >Hte >nth_change_vec // #Htb1 #Htb2
+ #Hte #_ * * #_ >Hte >nth_change_vec // #Htb1 #Htb2
cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta
(mk_tape sig (hda::lsb) (option_hd ? (reverse sig (reverse sig xs@s0::reverse sig tla)@cj::rs0')) (tail ? (reverse sig (reverse sig xs@s0::reverse sig tla)@cj::rs0'))) dst)
(midtape ? [ ] hdb (reverse sig (reverse sig xs@s0::reverse sig tlb)@ci::rs'')) src)
>nth_change_vec // >nth_change_vec_neq // >nth_change_vec //
>right_mk_tape >Hmidta_src >Hmidta_dst
whd in match (left ??); whd in match (left ??); whd in match (right ??);
- >length_tail >Hrs0 >length_append >length_append >length_reverse
+ >current_mk_tape <opt_cons_tail_expand whd in match (option_cons ???);
+ >Hrs0 >length_append whd in ⊢ (??(??%)); >length_append >length_reverse
>length_append >commutative_plus in match (|reverse ??| + ?);
whd in match (|?::?|); >length_reverse >length_reverse
<(length_reverse ? ls) <Hlen' >H1 normalize // ]
[ #H1 #H2 >H1 >H2 normalize in match (reverse ? [ ]); #Hte
lapply (Hte … (refl ??) … (refl ??) (refl ??)) -Hte
>change_vec_change_vec >change_vec_commute [|@sym_not_eq //]
- >change_vec_change_vec #Hte
+ >change_vec_change_vec #Hte #_
>Hte * * #_ >nth_change_vec // >reverse_reverse
#H lapply (H … (refl ??)) -H #Htb1 #Htb2
- (* cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (midtape sig [] s0 (xs@ci::rs'')) src) (mk_tape sig (s0::lsb) (option_hd sig (xs@cj::rs0')) (tail sig (xs@cj::rs0'))) dst) *)
cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (mk_tape ? [s0] (option_hd ? (xs@cj::rs0')) (tail ? (xs@cj::rs0'))) dst)
(midtape ? lsb s0 (xs@ci::rs'')) src)
[@daemon] -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec //
>nth_change_vec_neq // >nth_change_vec //
>right_mk_tape normalize in match (left ??);
- >Hmidta_src >Hmidta_dst >length_tail >Hrs0 >length_append
- >commutative_plus in match (pred ?); normalize
- >length_append >(?:|lsa| = O)
- [ normalize <plus_n_Sm <plus_n_Sm // | <(length_reverse ? lsa) >H1 % ]
+ >Hmidta_src >Hmidta_dst >current_mk_tape <opt_cons_tail_expand >Hrs0
+ >length_append normalize >length_append >length_append
+ <(reverse_reverse ? lsa) >H1 normalize //
| #hda #hdb #tla #tlb #H1 #H2 >H1 >H2
>reverse_cons >reverse_cons #Hte
lapply (Hte cj hdb (reverse ? xs@s0::reverse ? tlb) rs0' ?
>H1 in Hlen'; >H2 whd in ⊢ (??%%→?); #Hlen'
>length_reverse >length_reverse destruct (Hlen') //
| /2 by refl, trans_eq/ ] -Hte
- #Hte * * #_ >Hte >nth_change_vec_neq // >nth_change_vec // #Htb1 #Htb2
+ #Hte #_ * * #_ >Hte >nth_change_vec_neq // >nth_change_vec // #Htb1 #Htb2
cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta
(mk_tape sig [hdb] (option_hd ? (reverse sig (reverse sig xs@s0::reverse sig tlb)@cj::rs0')) (tail ? (reverse sig (reverse sig xs@s0::reverse sig tlb)@cj::rs0'))) dst)
(midtape ? lsb hda (reverse sig (reverse sig xs@s0::reverse sig tla)@ci::rs'')) src)
>nth_change_vec // >nth_change_vec_neq // >nth_change_vec //
>right_mk_tape >Hmidta_src >Hmidta_dst
whd in match (left ??); whd in match (left ??); whd in match (right ??);
- >length_tail >Hrs0 >length_append >length_append >length_reverse
+ >current_mk_tape <opt_cons_tail_expand
+ whd in match (option_cons ???);
+ >Hrs0 >length_append whd in ⊢ (??(??%)); >length_append >length_reverse
>length_append >commutative_plus in match (|reverse ??| + ?);
- whd in match (|?::?|); >length_reverse >length_reverse >Hlen
- <(length_reverse ? ls0) >H2 whd in match (|?::?|);
- >length_append normalize //
+ whd in match (|?::?|); >length_reverse >length_reverse
+ <(length_reverse ? lsa) >Hlen' >H2 >length_append
+ normalize //
]
]
]
- | FIXME
- (* lapply (\Pf Hss0) -Hss0 #Hss0 #Htc cut (tc = ta)
+ | 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 * * * # #_ >Hmidta_src >Hmidta_dst #Hte
- lapply (Hte … (refl ??) … (refl ??)) * * #_ #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/ ] *)
- ]
- ]
- ]
+ #Htd destruct (Htd) * #te * * * * >Hmidta_src >Hmidta_dst
+ cases (lists_length_split ? ls ls0) #lsa * #lsb * * #Hlen #Hlsalsb
+ destruct (Hlsalsb)
+ [ <(reverse_reverse … ls) <(reverse_reverse … lsa)
+ cut (|reverse ? lsa| = |reverse ? ls|) [ // ] #Hlen'
+ @(list_cases2 … Hlen')
+ [ #H1 #H2 >H1 >H2 -H1 -H2 #_ #_ normalize in match (reverse ? [ ]); #Hte #_
+ lapply (Hte … (refl ??) … (refl ??)) -Hte #Hte destruct (Hte) * * #_
+ >Hmidta_dst #Htb1 lapply (Htb1 … (refl ??)) -Htb1 #Htb1 #Htb2
+ cut (tb = change_vec ?? ta (mk_tape ? (s0::lsa@lsb) (option_hd ? rs0) (tail ? rs0)) dst)
+ [@daemon] -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec //
+ >nth_change_vec_neq [|@sym_not_eq //] >Hmidta_src >Hmidta_dst
+ >right_mk_tape normalize in match (left ??); normalize in match (right ??);
+ >Hmidta_src >Hmidta_dst >current_mk_tape <opt_cons_tail_expand
+ normalize //
+ | #hda #hdb #tla #tlb #H1 #H2 >H1 >H2
+ >reverse_cons >reverse_cons >associative_append #Hte
+ lapply (Hte ???? (refl ??) ? s0 ? (reverse ? tla) ?? (refl ??))
+ [ >length_reverse >length_reverse cut (|hda::tla| = |hdb::tlb|) //
+ normalize #H destruct (H) // ] #Hte #_ #_ #_
+ * * #_ >Hte >nth_change_vec // #Htb1 #Htb2
+ cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta
+ (mk_tape sig (hda::lsb) (option_hd ? (reverse sig (reverse sig tla)@s0::rs0)) (tail ? (reverse sig (reverse sig tla)@s0::rs0))) dst)
+ (midtape ? [ ] hdb (reverse sig (reverse sig tlb)@s::rs)) src)
+ [@daemon] -Htb1 -Htb2 #Htb >Htb whd
+ >nth_change_vec // >nth_change_vec_neq // >nth_change_vec //
+ >right_mk_tape >Hmidta_src >Hmidta_dst
+ whd in match (left ??); whd in match (left ??); whd in match (right ??);
+ >current_mk_tape <opt_cons_tail_expand >length_append
+ >length_reverse >length_reverse <(length_reverse ? ls) <Hlen'
+ >H1 normalize // ]
+ | #_ <(reverse_reverse … ls0) <(reverse_reverse … lsa)
+ cut (|reverse ? lsa| = |reverse ? ls0|) [ // ] #Hlen'
+ @(list_cases2 … Hlen')
+ [ #H1 #H2 >H1 >H2 normalize in match (reverse ? [ ]); #_ #_ #Hte
+ lapply (Hte … (refl ??) … (refl ??)) -Hte #Hte destruct (Hte)
+ * * #_ >Hmidta_dst #Htb1 lapply (Htb1 … (refl ??)) -Htb1 #Htb1 #Htb2
+ cut (tb = change_vec (tape sig) (S n) ta (mk_tape ? (s0::ls0) (option_hd ? rs0) (tail ? rs0)) dst)
+ [@daemon] -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec //
+ >nth_change_vec_neq [|@sym_not_eq //] >Hmidta_src >Hmidta_dst
+ >current_mk_tape >right_mk_tape normalize in ⊢ (??%); <opt_cons_tail_expand
+ normalize //
+ | #hda #hdb #tla #tlb #H1 #H2 >H1 >H2
+ >reverse_cons >reverse_cons #Hte #_ #_
+ lapply (Hte s0 hdb (reverse ? tlb) rs0 ?
+ lsb s hda (reverse ? tla) rs ??)
+ [ /2 by cons_injective_l, nil/
+ | >length_reverse >length_reverse cut (|hda::tla| = |hdb::tlb|) //
+ normalize #H destruct (H) //
+ | /2 by refl, trans_eq/ ] -Hte
+ #Hte * * #_ >Hte >nth_change_vec_neq // >nth_change_vec // #Htb1 #Htb2
+ cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta
+ (mk_tape sig [hdb] (option_hd ? (reverse sig (reverse sig tlb)@s0::rs0)) (tail ? (reverse sig (reverse sig tlb)@s0::rs0))) dst)
+ (midtape ? lsb hda (reverse sig (reverse sig tla)@s::rs)) src)
+ [@daemon] -Htb1 -Htb2 #Htb >Htb whd
+ >nth_change_vec // >nth_change_vec_neq // >nth_change_vec //
+ >right_mk_tape >Hmidta_src >Hmidta_dst
+ whd in match (left ??); whd in match (left ??); whd in match (right ??);
+ >current_mk_tape <opt_cons_tail_expand >length_append
+ normalize in ⊢ (??%); >length_append >reverse_reverse
+ <(length_reverse ? lsa) >Hlen' >H2 normalize //
+ ]
+ ]
+ ]
+ ]
+ ]
| #ta #tb #tc * #Hcomp1 #Hcomp2 * #td * * #Htest #Htd destruct (Htd)
whd in ⊢ (%→?); #Htb destruct (Htb) #ls #x #xs #Hta_src
lapply (refl ? (current ? (nth dst ? ta (niltape ?))))
normalize #H destruct (H) ] ] ]
qed.
-
-definition Pre_match_m ≝
- λsrc,sig,n.λt: Vector (tape sig) (S n).
- ∃x,xs.
- nth src (tape sig) t (niltape sig) = midtape ? [] x xs.
-
-lemma terminate_match_m :
+axiom terminate_match_m :
∀src,dst,sig,n,t.
src ≠ dst → src < S n → dst < S n →
- Pre_match_m src sig n t →
match_m src dst sig n ↓ t.
-#src #dst #sig #n #t #Hneq #Hsrc #Hdst * #start * #xs
-#Hmid_src
-@(terminate_while … (sem_match_step src dst sig n Hneq Hsrc Hdst)) //
+(*#src #dst #sig #n #ta #Hneq #Hsrc #Hdst
+@(terminate_while … (sem_match_step_termination src dst sig n Hneq Hsrc Hdst)) // % #tb
+letin f ≝ (λt0:Vector (tape sig) (S n).|left ? (nth src (tape ?) t0 (niltape ?))|
+ +|option_cons ? (current ? (nth dst (tape ?) t0 (niltape ?)))
+ (right ? (nth dst (tape ?) t0 (niltape ?)))|)
+change with (f tb < f ta) in ⊢ (%→?); @(nat_elim1 (f tb))
+#x lapply (refl ? x) cases x in ⊢ (???%→%);
+[ #Hx
+*
+#x #IH #Hx cases
+
+ @IH % #tc change with (f tc < f tb) in ⊢ (%→?);
+
+ )(|left @(nat_elim1 (|left ? (nth ? (tape ?) t (niltape ?))|
+ +|option_cons sig (current ? (nth dst (tape ?) t (niltape ?)))
+ (right ? (nth dst (tape ?) t (niltape ?)))|))
<(change_vec_same … t dst (niltape ?))
+<(change_vec_same … t src (niltape ?)) in ⊢ (???(???%??));
lapply (refl ? (nth dst (tape sig) t (niltape ?)))
cases (nth dst (tape sig) t (niltape ?)) in ⊢ (???%→?);
[ #Htape_dst % #t1 whd in ⊢ (%→?); >nth_change_vec_neq [|@sym_not_eq //]
| >Ht1 >nth_change_vec // ]
]
]
-qed.
\ No newline at end of file
+qed. *)
+
+lemma sem_match_m : ∀src,dst,sig,n.
+src ≠ dst → src < S n → dst < S n →
+ match_m src dst sig n \vDash R_match_m src dst sig n.
+#src #dst #sig #n #Hneq #Hsrc #Hdst @WRealize_to_Realize [/2/| @wsem_match_m // ]
+qed.
projects / helm.git / blobdiff