Ultimately Periodic (UP) Sequences
UP sequences form an instance of abstract sequences. Defining all operations apart zipping is straight forward.Section BaseUP.
Variable (X:Type).
Implicit Types (sigma : UPSeq X).
Definition up_hd sigma := match sigma with
| mkUPSeq (sing a) _ => a
| mkUPSeq (ncons a _) _ => a end.
Definition up_tl sigma := match sigma with
| mkUPSeq (sing a) x => mkUPSeq x x
| mkUPSeq (ncons a x) y => mkUPSeq x y end.
Definition up_cons a sigma := match sigma with
| mkUPSeq x y => mkUPSeq (ncons a x) y end.
End BaseUP.
Existing Instance Sequence.
Instance UPSequence : AbstractSequence := {| hd := up_hd; tl := up_tl; scons := up_cons|}.
Proof.
- now intros X b [[a |a x] y].
- now intros X b [[a| ax ] y] [|n].
Defined.
Definition up_const (X:Type) (a: X) := mkUPSeq (sing a) (sing a).
Lemma up_const_correct (X: Type) (a:X) : up_const a == up_cons a (up_const a).
Proof.
intros n. destruct n; reflexivity.
Qed.
Global Instance UPWithConst : WithConst UPSequence := {|
const := up_const
|}.
Proof.
- intros X a. apply up_const_correct.
Defined.
Two show that two UP sequences are equivalent, we first show that we can
retract to sequences as functions and hence have all lemmas for these
sequences available.
Definition unfold (X:Type) (sigma : UPSeq X) := match sigma with mkUPSeq x y => x +++ omega_iter y end.
Lemma up_hd_correct (X: Type) (sigma: UPSeq X) : up_hd sigma = hd (unfold sigma).
Proof.
now destruct sigma as [[a |a x] y]; simpl; rewrite hd_correct.
Qed.
Lemma up_tl_correct (X:Type) (sigma: UPSeq X) : unfold (up_tl sigma) == tl (unfold sigma).
Proof.
destruct sigma as [[a| a x] y]; simpl; rewrite tl_correct.
- now rewrite <-omega_iter_correct.
- reflexivity.
Qed.
Lemma up_drop_correct (X:Type) (sigma: UPSeq X) (n: nat) : unfold (@drop UPSequence X sigma n) == drop (unfold sigma) n.
Proof.
revert sigma. induction n; intros sigma.
- reflexivity.
- simpl. now rewrite IHn, up_tl_correct.
Qed.
Lemma up_cons_unfold (X:Type) (a:X) (sigma: UPSeq X) : unfold (up_cons a sigma) == a ::: (unfold sigma).
Proof.
destruct sigma as [x y].
intros [|n]; simpl; reflexivity.
Qed.
Lemma up_equiv (X:Type) (sigma tau : UPSeq X) : unfold sigma == unfold tau <-> sigma == tau.
Proof.
split.
- intros E n. revert sigma tau E. induction n; intros [x y] [u v] E.
+ now rewrite 2nth_first_hd, 2up_hd_correct, E.
+ rewrite nth_step_tl. apply IHn. now rewrite 2up_tl_correct, E.
- intros E n. revert sigma tau E. induction n; intros [x y] [u v] E.
+ simpl. specialize (E 0). destruct x; destruct u; simpl; now rewrite !nth_first.
+ simpl. destruct x, u; simpl in *; rewrite !nth_step.
* setoid_rewrite omega_iter_correct at 1 2. apply (IHn (mkUPSeq y y) (mkUPSeq v v)).
intros m. apply (E (S m)).
* setoid_rewrite omega_iter_correct at 1. apply (IHn (mkUPSeq y y) (mkUPSeq u v)).
intros m. apply (E (S m)).
* setoid_rewrite omega_iter_correct at 2. apply (IHn (mkUPSeq x y) (mkUPSeq v v)).
intros m. apply (E (S m)).
* apply (IHn (mkUPSeq x y) (mkUPSeq u v)). intros m. apply (E (S m)).
Qed.
Lemma up_nth_correct (X: Type)(sigma: UPSeq X) n : nth sigma n = nth(unfold sigma) n.
Proof.
destruct sigma as [x y]. unfold nth.
now rewrite up_hd_correct, up_drop_correct.
Qed.
Section UPMap.
Variable (X Y : Type).
Implicit Types (sigma : UPSeq X).
Definition up_map (f: X -> Y) sigma : UPSeq Y :=
match sigma with mkUPSeq x y => mkUPSeq (nstr_map f x) (nstr_map f y) end.
Lemma up_map_correct (f: X -> Y) sigma: unfold (up_map f sigma) == map f (unfold sigma).
Proof.
intros n. destruct sigma as [x y]. revert x y. simpl. induction n; intros x y; simpl; rewrite map_correct.
- destruct x as [a|a x]; simpl; now rewrite 2nth_first, hd_correct.
- destruct x as [a|a x]; simpl; rewrite 2nth_step, tl_correct.
+ setoid_rewrite omega_iter_correct at 1 2. apply IHn.
+ apply IHn.
Qed.
End UPMap.
Zipping Two UP Sequences
Two zip UP sequences, one needs to align the lengths of the strings. For a UP Sequences x +++ (omega_iter y) we call x the "prefix" and y the "loop". We do this in several steps:- Make the lengths of the prefixes equal
- Make the lengths of the loops equal
- Zip UP sequences where prefix and loop have the same length.
Section NStrZip.
Context {X Y: Type}.
Fixpoint nstr_zip (x: NStr X) (y : NStr Y) : NStr (X * Y) := match x,y with
| sing a , sing b => sing (a,b)
| ncons a x , sing b => sing (a,b)
| sing a , ncons b y => sing (a,b)
| ncons a x, ncons b y => ncons (a,b) (nstr_zip x y)
end.
Lemma nstr_zip_delta x y : delta x = delta y -> delta (nstr_zip x y) = delta x.
Proof.
revert y. induction x as [a| a x]; intros [b| b y]; simpl; intros E; auto.
Qed.
Lemma nstr_zip_nth x y n: delta x = delta y -> n <= delta x -> nstr_zip x y n = (x n, y n).
Proof.
revert y n. induction x as [a| a x]; intros [b |b y] [|n]; simpl; intros E L; auto.
Qed.
Lemma nstr_zip_append x y a b: delta x = delta y -> nstr_concat' (nstr_zip x y) (sing (a, b)) = nstr_zip (nstr_concat' x (sing a)) (nstr_concat' y (sing b)).
Proof.
revert y a b. induction x as [a|a x]; intros [b| b y] c d; simpl; intros E; auto. f_equal. auto.
Qed.
End NStrZip.
Lemma split_string_eq (X: Type) (x: NStr X) n : n < delta x -> nstr_concat' (closed_take x n) (nstr_drop x (S n)) = x.
Proof.
revert n. induction x; intros [|n]; intros L1 ; simpl in L1; try now exfalso.
- simpl. destruct x as [b|b x]; simpl; auto.
- simpl. f_equal. destruct x as [b|b x].
+ simpl in L1. exfalso. omega.
+ apply IHx; simpl in *; omega.
Qed.
Lemma up_prefix_correct X (x y : NStr X) : up_prefix (mkUPSeq x y) = x.
Proof. reflexivity. Qed.
(*Lemma up_loop_correct X (x y : NStr X) : up_loop (mkUPSeq x y) = y.
Proof. reflexivity. Qed.*)
Section ZipEqUP.
Context {X Y: Type}.
Definition up_eq_zip (sigma : UPSeq X) (tau:UPSeq Y):=
match sigma, tau with mkUPSeq x y, mkUPSeq u v => mkUPSeq (nstr_zip x u) (nstr_zip y v) end.
Lemma up_eq_zip_correct sigma tau: delta (up_prefix sigma) = delta (up_prefix tau) -> delta (up_loop sigma) = delta (up_loop tau) ->
unfold (up_eq_zip sigma tau) == zip (unfold sigma) (unfold tau).
Proof.
intros E1 E2 n. destruct sigma as [x y]. destruct tau as [u v]. simpl in *. rewrite zip_nth. decide (n <= delta x) as [D|D].
- rewrite !prepend_nstr_nth_first; auto.
+ now rewrite nstr_zip_nth.
+ now rewrite nstr_zip_delta.
- rewrite !prepend_nstr_nth_rest_sub; auto.
+ rewrite nstr_zip_delta, <-E1 by assumption.
generalize (n - S (delta x)) as m. intros m. revert y v E2.
induction m; intros y v E2; setoid_rewrite omega_iter_step at 1 2 3.
* destruct y,v; simpl; now rewrite !nth_first.
* destruct y,v; simpl; rewrite !nth_step.
-- now apply (IHm (sing a) (sing a0)).
-- exfalso. now simpl in E2.
-- exfalso. now simpl in E2.
-- rewrite nstr_zip_append.
++ apply IHm. rewrite !nstr_concat'_delta. simpl in *. omega.
++ simpl in *. omega.
+ rewrite nstr_zip_delta; omega.
Qed.
Section UPEqualizePrefix .
Definition equalize_first l (sigma:UPSeq X) :=
match sigma with mkUPSeq x y =>
if (decision (delta x = l))
then mkUPSeq x y
else mkUPSeq
(nstr_concat' x (closed_take (nstr_finIter y (S l)) (l - S(delta x))))
(nstr_concat' (nstr_drop (nstr_finIter y (S l)) (S(l-S(delta x)))) (closed_take (nstr_finIter y (S l)) (l-S (delta x)))) end.
Lemma equalize_first_correct l sigma : delta (up_prefix sigma) <= l ->
equalize_first l sigma == sigma.
Proof.
intros L. apply up_equiv. destruct sigma as [x y]. unfold equalize_first. simpl.
destruct decision; simpl.
- reflexivity.
- symmetry. rewrite omega_iter_iter with (n0:=S l), <-split_string_eq with (x:= nstr_finIter y (S l))(n:=l- S(delta x)) at 1.
+ now rewrite omega_iter_rotate, prepend_nstr_assoc.
+ rewrite nstr_finIter_delta. simpl in L. remember (S (S l) * delta y) as z. omega.
Qed.
Lemma equalize_first_delta l sigma : delta (up_prefix sigma) <= l -> delta (up_prefix (equalize_first l sigma)) = l.
Proof.
intros L. unfold equalize_first. destruct sigma as [x y]. simpl in *.
destruct decision; auto.
rewrite !up_prefix_correct, nstr_concat'_delta, closed_take_delta. omega.
rewrite nstr_concat'_delta. rewrite nstr_finIter_delta. remember (S l * delta y) as z. omega.
Qed.
Definition up_iter_loop l (sigma: UPSeq X) :=
match sigma with mkUPSeq x y => mkUPSeq x (nstr_finIter y l) end.
Lemma up_iter_loop_correct l sigma :
up_iter_loop l sigma == sigma.
Proof.
unfold up_iter_loop. destruct sigma as [x y]. apply up_equiv. simpl.
now rewrite <-omega_iter_iter.
Qed.
Lemma up_iter_loop_prefix l sigma : up_prefix (up_iter_loop l sigma) = up_prefix sigma.
Proof.
destruct sigma as [x y]. reflexivity.
Qed.
Lemma up_iter_loop_loop_length l sigma : | up_loop (up_iter_loop l sigma) | = S l * | up_loop sigma|.
Proof.
destruct sigma as [x y]. unfold up_iter_loop. simpl. apply nstr_finIter_length.
Qed.
End UPEqualizePrefix.
End ZipEqUP.
Section UPZip.
Variables (X Y : Type).
Definition up_zip (sigma : UPSeq X) (tau : UPSeq Y) :=
let n := (max ((delta (up_prefix sigma))) ((delta (up_prefix tau)))) in
up_eq_zip (up_iter_loop ( (delta(up_loop (equalize_first n tau)))) (equalize_first n sigma))
(up_iter_loop ( (delta(up_loop (equalize_first n sigma)))) (equalize_first n tau)).
Lemma up_zip_correct sigma tau: unfold (up_zip sigma tau) == zip (unfold sigma) (unfold tau).
Proof.
unfold up_zip. rewrite up_eq_zip_correct.
- apply zip_proper.
+ apply up_equiv. rewrite up_iter_loop_correct, equalize_first_correct.
* reflexivity.
* apply Nat.le_max_l.
+ apply up_equiv. rewrite up_iter_loop_correct, equalize_first_correct.
* reflexivity.
* apply Nat.le_max_r.
- rewrite 2up_iter_loop_prefix, 2equalize_first_delta; auto using Nat.le_max_l, Nat.le_max_r.
- apply eq_add_S. rewrite !nstr_to_str_length, 2up_iter_loop_loop_length, !nstr_to_str_length.
rewrite Nat.mul_comm. reflexivity.
Qed.
End UPZip.
Global Instance UPWithZipMap: WithZipMap UPSequence := {|
zip := up_zip;
map := up_map
|}.
Proof.
- intros X Y f sigma. apply up_equiv.
now rewrite up_cons_unfold, 2up_map_correct, map_correct, up_hd_correct, up_tl_correct.
- intros X Y sigma tau. apply up_equiv.
now rewrite up_cons_unfold, 2up_zip_correct, zip_correct, 2up_hd_correct, 2up_tl_correct.
Qed.
End SeqInstances.