Library Beroal.Stream

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 : ∀ 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 : ∀ xs ys,
        EqSt xs ys → ∀ n, take n xs = take n ys.

Check fun n xs ⇒ (refl_equal _) : take n (tl xs) = List.tail (take (S n) xs).

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 : ∀ xs, EqSt xs (app nil xs).

Definition app_comm_cons : ∀ x xs ys,
        EqSt (Streams.Cons x (app xs ys)) (app (x :: xs) ys).

Definition app_single_cons : ∀ x xs,
        EqSt (Streams.Cons x xs) (app (x :: nil) xs).

Definition app_pres_eq : ∀ xs ys, EqSt xs ys
        → ∀ zs, EqSt (app zs xs) (app zs ys).

Definition take_app_degen : ∀ n xs ys, n ≤ length xs
        → TakeDrop.take n xs = take n (app xs ys).

Definition drop_app_degen : ∀ n xs ys, n ≤ length xs
        → EqSt (app (TakeDrop.drop n xs) ys)
                (Str_nth_tl n (app xs ys)).

Definition take_app_part : ∀ n ys xs,
        xs ++ (take n ys) = take (length xs + n) (app xs ys).

Definition drop_app_part : ∀ n ys xs,
        EqSt (Str_nth_tl n ys)
                (Str_nth_tl (length xs + n) (app xs ys)).

Definition take_app_exact : ∀ xs ys,
        xs = take (length xs) (app xs ys).

Definition drop_app_exact : ∀ xs ys,
        EqSt ys (Str_nth_tl (length xs) (app xs ys)).

Definition take_app_drop : ∀ n xs,
        EqSt xs (app (take n xs) (Str_nth_tl n xs)).

Definition drop_plus : ∀ 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 : ∀ 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 : ∀ x n,
        cyclic n (iterate (@Beroal.Init.id _) x).

Definition iterate_id_nth : ∀ x n,
        x = Str_nth n (iterate (@Beroal.Init.id _) x).

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

Definition cycle_single_nth : ∀ x n,
        x = Str_nth n (cycle x nil).

Definition iterate_id_eq_cycle_single : ∀ x,
        EqSt (iterate (@Beroal.Init.id _) x) (cycle x nil).

Definition unfold_cycle : ∀ x xs,
        EqSt ((app (x :: xs) (cycle x xs))) (cycle x xs).

Definition take_cycle_id : ∀ x xs,
        x :: xs = take (S (length xs)) (cycle x xs).

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

Definition cyclic_tl : ∀ period xs,
        cyclic period xs → cyclic period (tl xs).

Definition cyclic_drop : ∀ period xs,
        cyclic period xs → ∀ n, cyclic period (Str_nth_tl n xs).

Definition cyclic_hd_eq : ∀ xs ys,
        cyclic 1 xs → cyclic 1 ys → hd xs = hd ys → EqSt xs ys.

Definition eqst_many : ∀ 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 : ∀ x0 x1 xs,
        EqSt (tl (cycle x0 (x1 :: xs)))
                (app nil (cycle x1 (xs ++ (x0 :: nil)))).

End element.