# Library Beroal.Stream

This greatly seconds "TakeDrop" module, but for streams instead of lists

Require Coq.Arith.Le.

Require Import Coq.Lists.List.

Require Import Coq.Lists.Streams.

Require Beroal.Init.

Require Import Beroal.TakeDrop.

Section element.

Variable e : Type.

Definition drop_pres_eq : forall n (xs ys : Stream e),

EqSt xs ys -> EqSt (Str_nth_tl n xs) (Str_nth_tl n ys).

Definition In (x : e) := Exists (fun xs => x = hd xs).

Definition non_dup := ForAll (fun xs => ~ In (hd xs) (tl xs)).

Definition filtered_finite (p : e -> Prop)

:= Exists (ForAll (fun ys => ~ p (hd ys))).

Definition filtered_infinite (p : e -> Prop)

:= ForAll (Exists (fun ys => p (hd ys))).

Definition app xs0 (ys : Stream e) := (cofix rec (xs : list e)

:= match xs with

| nil => ys

| List.cons x xss => Streams.Cons x (rec xss)

end) xs0.

Definition take := fix rec (n : nat) (xs : Stream e)

:= match n with

| O => nil

| S pn => List.cons (hd xs) (rec pn (tl xs))

end.

Definition take_pres_eq : forall xs ys,

EqSt xs ys -> forall n, take n xs = take n ys.

permuting take and tail

obvious simplifications

Check fun x xs ys => conj (refl_equal _)

(conj (refl_equal _)

(conj (refl_equal _)

(refl_equal _)))

: hd ys = hd (app nil ys)

/\ tl ys = tl (app nil ys)

/\ x = hd (app (x :: xs) ys)

/\ app xs ys = tl (app (x :: xs) ys).

Definition app_nil_id : forall xs, EqSt xs (app nil xs).

Definition app_comm_cons : forall x xs ys,

EqSt (Streams.Cons x (app xs ys)) (app (x :: xs) ys).

Definition app_single_cons : forall x xs,

EqSt (Streams.Cons x xs) (app (x :: nil) xs).

Definition app_pres_eq : forall xs ys, EqSt xs ys

-> forall zs, EqSt (app zs xs) (app zs ys).

Definition take_app_degen : forall n xs ys, n <= length xs

-> TakeDrop.take n xs = take n (app xs ys).

Definition drop_app_degen : forall n xs ys, n <= length xs

-> EqSt (app (TakeDrop.drop n xs) ys)

(Str_nth_tl n (app xs ys)).

Definition take_app_part : forall n ys xs,

xs ++ (take n ys) = take (length xs + n) (app xs ys).

Definition drop_app_part : forall n ys xs,

EqSt (Str_nth_tl n ys)

(Str_nth_tl (length xs + n) (app xs ys)).

Definition take_app_exact : forall xs ys,

xs = take (length xs) (app xs ys).

Definition drop_app_exact : forall xs ys,

EqSt ys (Str_nth_tl (length xs) (app xs ys)).

Definition take_app_drop : forall n xs,

EqSt xs (app (take n xs) (Str_nth_tl n xs)).

Definition drop_plus : forall n m xs,

EqSt (Str_nth_tl n xs)

(app (take m (Str_nth_tl n xs)) (Str_nth_tl (n + m) xs)).

Definition take_plus : forall n m xs,

take (n + m) xs = take n xs ++ take m (Str_nth_tl n xs).

Definition iterate (f : e -> e) := cofix rec (x : e)

:= (Streams.Cons x (rec (f x))).

Definition cycle (x : e) (xs : list e)

:= cofix rec := Streams.Cons x (app xs rec).

Definition cyclic (period : nat) (xs : Stream e)

:= EqSt xs (Str_nth_tl period xs).

Definition repeat (x : e)

:= cofix rec := Streams.Cons x rec.

Definition replicate n (x : e) := take n (repeat x).

Definition iterate_id_cyclic : forall x n,

cyclic n (iterate (@Beroal.Init.id _) x).

Definition iterate_id_nth : forall x n,

x = Str_nth n (iterate (@Beroal.Init.id _) x).

Definition cycle_single_cyclic : forall x n, cyclic n (cycle x nil).

Definition cycle_single_nth : forall x n,

x = Str_nth n (cycle x nil).

Definition iterate_id_eq_cycle_single : forall x,

EqSt (iterate (@Beroal.Init.id _) x) (cycle x nil).

Definition unfold_cycle : forall x xs,

EqSt ((app (x :: xs) (cycle x xs))) (cycle x xs).

Definition take_cycle_id : forall x xs,

x :: xs = take (S (length xs)) (cycle x xs).

Definition cycle_cyclic : forall x xs, cyclic (S (length xs)) (cycle x xs).

Definition cyclic_tl : forall period xs,

cyclic period xs -> cyclic period (tl xs).

Definition cyclic_drop : forall period xs,

cyclic period xs -> forall n, cyclic period (Str_nth_tl n xs).

Definition cyclic_hd_eq : forall xs ys,

cyclic 1 xs -> cyclic 1 ys -> hd xs = hd ys -> EqSt xs ys.

Definition eqst_many : forall n xs ys, take n xs = take n ys

-> EqSt (Str_nth_tl n xs) (Str_nth_tl n ys) -> EqSt xs ys.

Definition cycle_rotate_tl_app_nil : forall x0 x1 xs,

EqSt (tl (cycle x0 (x1 :: xs)))

(app nil (cycle x1 (xs ++ (x0 :: nil)))).

End element.

Require Coq.Arith.Plus.

Section Stream_nat.

Definition enum := iterate S.

Definition enum_nth n s : Str_nth n (enum s) = n + s.

Definition enum_step step := iterate (plus step).

Definition enum_step_nth step n start0

: Str_nth n (enum_step step start0) = n * step + start0.

End Stream_nat.

Definition zip_with (e0 e1 e2 : Type) (f : e0 -> e1 -> e2)

:= fix rec (xs : list e0) (ys : Stream e1) := match xs with

| nil => nil

| List.cons x xs => match ys with

| Streams.Cons y ys => List.cons (f x y) (rec xs ys) end

end.

Definition zip (e0 e1 : Type) := @zip_with e0 e1 _

(fun x0 x1 => (x0, x1)).

(conj (refl_equal _)

(conj (refl_equal _)

(refl_equal _)))

: hd ys = hd (app nil ys)

/\ tl ys = tl (app nil ys)

/\ x = hd (app (x :: xs) ys)

/\ app xs ys = tl (app (x :: xs) ys).

Definition app_nil_id : forall xs, EqSt xs (app nil xs).

Definition app_comm_cons : forall x xs ys,

EqSt (Streams.Cons x (app xs ys)) (app (x :: xs) ys).

Definition app_single_cons : forall x xs,

EqSt (Streams.Cons x xs) (app (x :: nil) xs).

Definition app_pres_eq : forall xs ys, EqSt xs ys

-> forall zs, EqSt (app zs xs) (app zs ys).

Definition take_app_degen : forall n xs ys, n <= length xs

-> TakeDrop.take n xs = take n (app xs ys).

Definition drop_app_degen : forall n xs ys, n <= length xs

-> EqSt (app (TakeDrop.drop n xs) ys)

(Str_nth_tl n (app xs ys)).

Definition take_app_part : forall n ys xs,

xs ++ (take n ys) = take (length xs + n) (app xs ys).

Definition drop_app_part : forall n ys xs,

EqSt (Str_nth_tl n ys)

(Str_nth_tl (length xs + n) (app xs ys)).

Definition take_app_exact : forall xs ys,

xs = take (length xs) (app xs ys).

Definition drop_app_exact : forall xs ys,

EqSt ys (Str_nth_tl (length xs) (app xs ys)).

Definition take_app_drop : forall n xs,

EqSt xs (app (take n xs) (Str_nth_tl n xs)).

Definition drop_plus : forall n m xs,

EqSt (Str_nth_tl n xs)

(app (take m (Str_nth_tl n xs)) (Str_nth_tl (n + m) xs)).

Definition take_plus : forall n m xs,

take (n + m) xs = take n xs ++ take m (Str_nth_tl n xs).

Definition iterate (f : e -> e) := cofix rec (x : e)

:= (Streams.Cons x (rec (f x))).

Definition cycle (x : e) (xs : list e)

:= cofix rec := Streams.Cons x (app xs rec).

Definition cyclic (period : nat) (xs : Stream e)

:= EqSt xs (Str_nth_tl period xs).

Definition repeat (x : e)

:= cofix rec := Streams.Cons x rec.

Definition replicate n (x : e) := take n (repeat x).

Definition iterate_id_cyclic : forall x n,

cyclic n (iterate (@Beroal.Init.id _) x).

Definition iterate_id_nth : forall x n,

x = Str_nth n (iterate (@Beroal.Init.id _) x).

Definition cycle_single_cyclic : forall x n, cyclic n (cycle x nil).

Definition cycle_single_nth : forall x n,

x = Str_nth n (cycle x nil).

Definition iterate_id_eq_cycle_single : forall x,

EqSt (iterate (@Beroal.Init.id _) x) (cycle x nil).

Definition unfold_cycle : forall x xs,

EqSt ((app (x :: xs) (cycle x xs))) (cycle x xs).

Definition take_cycle_id : forall x xs,

x :: xs = take (S (length xs)) (cycle x xs).

Definition cycle_cyclic : forall x xs, cyclic (S (length xs)) (cycle x xs).

Definition cyclic_tl : forall period xs,

cyclic period xs -> cyclic period (tl xs).

Definition cyclic_drop : forall period xs,

cyclic period xs -> forall n, cyclic period (Str_nth_tl n xs).

Definition cyclic_hd_eq : forall xs ys,

cyclic 1 xs -> cyclic 1 ys -> hd xs = hd ys -> EqSt xs ys.

Definition eqst_many : forall n xs ys, take n xs = take n ys

-> EqSt (Str_nth_tl n xs) (Str_nth_tl n ys) -> EqSt xs ys.

Definition cycle_rotate_tl_app_nil : forall x0 x1 xs,

EqSt (tl (cycle x0 (x1 :: xs)))

(app nil (cycle x1 (xs ++ (x0 :: nil)))).

End element.

Require Coq.Arith.Plus.

Section Stream_nat.

Definition enum := iterate S.

Definition enum_nth n s : Str_nth n (enum s) = n + s.

Definition enum_step step := iterate (plus step).

Definition enum_step_nth step n start0

: Str_nth n (enum_step step start0) = n * step + start0.

End Stream_nat.

Definition zip_with (e0 e1 e2 : Type) (f : e0 -> e1 -> e2)

:= fix rec (xs : list e0) (ys : Stream e1) := match xs with

| nil => nil

| List.cons x xs => match ys with

| Streams.Cons y ys => List.cons (f x y) (rec xs ys) end

end.

Definition zip (e0 e1 : Type) := @zip_with e0 e1 _

(fun x0 x1 => (x0, x1)).