theory.streams

Require Export Streams.
Require Import Morphisms peano_naturals abstract_algebra.

Section streams.
Context `{Setoid A}.

CoInductive Stream_eq_coind (s1 s2: Stream A) : Prop :=
  stream_eq_coind : hd s1 = hd s2 Stream_eq_coind (tl s1) (tl s2) Stream_eq_coind s1 s2.

Global Instance stream_eq: Equiv (Stream A) := Stream_eq_coind.

Global Instance: Setoid (Stream A).

Global Instance: Proper ((=) ==> (=)) (@Cons A).

Global Instance: Proper ((=) ==> (=)) (@hd A).

Global Instance: Proper ((=) ==> (=)) (@tl A).

Global Instance: Proper ((=) ==> (=) ==> (=)) (@Str_nth_tl A).

Global Instance: Proper ((=) ==> (=) ==> (=)) (@Str_nth A).

Lemma stream_eq_Str_nth s1 s2 : s1 = s2 n, Str_nth n s1 = Str_nth n s2.

Global Instance ForAll_proper `{!Proper ((=) ==> iff) (P : Stream A Prop)} :
  Proper ((=) ==> iff) (ForAll P).

Lemma ForAll_tl (P : Stream A Prop) s : ForAll P s ForAll P (tl s).

Lemma ForAll_True (s : Stream A) : ForAll (λ _, True) s.

Definition EventuallyForAll (P : Stream A Prop) := ForAll (λ s, P s P (tl s)).

Lemma EventuallyForAll_tl P s : EventuallyForAll P s EventuallyForAll P (tl s).

Lemma EventuallyForAll_Str_nth_tl P n s :
  EventuallyForAll P s EventuallyForAll P (Str_nth_tl n s).

Global Instance EventuallyForAll_proper `{!Proper ((=) ==> iff) (P : Stream A Prop)} :
  Proper ((=) ==> iff) (EventuallyForAll P).
End streams.

Section more.
Context `{Setoid A} `{Setoid B}.

CoInductive ForAllIf (PA : Stream A Prop) (PB : Stream B Prop) : Stream A Stream B Prop :=
  ext_if : s1 s2, (PA s1 PB s2) ForAllIf PA PB (tl s1) (tl s2) ForAllIf PA PB s1 s2.

Global Instance ForAllIf_proper `{!Proper ((=) ==> iff) (PA : Stream A Prop)} `{!Proper ((=) ==> iff) (PB : Stream B Prop)} :
  Proper ((=) ==> (=) ==> iff) (ForAllIf PA PB).

Global Instance map_proper `{!Proper ((=) ==> (=)) (f : A B)} :
  Proper ((=) ==> (=)) (map f).

Context `{Setoid C}.
Global Instance zipWith_proper `{!Proper ((=) ==> (=) ==> (=)) (f : A B C)} :
  Proper ((=) ==> (=) ==> (=)) (zipWith f).
End more.