Module CommonStreams

From Coq Require Import Setoid.
From Coq Require Import Streams.


Delimit Scope stream_scope with Stream.
Infix "⋅" := Cons (at level 60, right associativity) : stream_scope.
Infix "≡" := EqSt (at level 70, no associativity) : stream_scope.
Notation "s # n " := (Str_nth n s) (at level 9) : stream_scope.
Open Scope stream_scope.

Fact Str_nth_0:
  forall {A} (xs: Stream A) x,
    (x ⋅ xs) # 0 = x.

Fact Str_nth_S:
  forall {A} (xs: Stream A) x n,
    (x ⋅ xs) # (S n) = xs # n.

Fact Str_nth_S_tl:
  forall {A} (xs: Stream A) n,
    xs # (S n) = (tl xs) # n.

Section map.
  Context {A B : Type}.

  Variable (f : (A -> B)).

  Lemma map_Cons : forall a (sa : Stream A),
      (map f (a ⋅ sa)) = ((f a) ⋅ (map f sa)).
End map.

Section map2.
  Context {A B C : Type}.

  Variable (f : (A -> B -> C)).

  CoFixpoint map2 (sa : Stream A) (sb : Stream B) : Stream C :=
    match sa, sb with
    | hda ⋅ tla, hdb ⋅ tlb =>
      (f hda hdb) ⋅ (map2 tla tlb)
    end.

  Lemma map2_Cons : forall a b (sa : Stream A) (sb : Stream B),
      (map2 (a ⋅ sa) (b ⋅ sb)) = ((f a b) ⋅ (map2 sa sb)).

  Lemma map2_hd : forall (sa : Stream A) (sb : Stream B),
      f (hd sa) (hd sb) = hd (map2 sa sb).

  Lemma map2_tl : forall (sa : Stream A) (sb : Stream B),
      map2 (tl sa) (tl sb) = tl (map2 sa sb).

  Lemma Str_nth_tl_map2 : forall n (sa : Stream A) (sb : Stream B),
      Str_nth_tl n (map2 sa sb) = map2 (Str_nth_tl n sa) (Str_nth_tl n sb).

  Lemma Str_nth_map2 : forall n (sa : Stream A) (sb : Stream B),
      Str_nth n (map2 sa sb) = f (Str_nth n sa) (Str_nth n sb).
End map2.

Add Parametric Relation A : (Stream A) (@EqSt A)
    reflexivity proved by (@EqSt_reflex A)
    symmetry proved by (@sym_EqSt A)
    transitivity proved by (@trans_EqSt A)
      as EqStrel.

Add Parametric Morphism A B C f : (@map2 A B C f)
    with signature (@EqSt A) ==> (@EqSt B) ==> (@EqSt C) as map2_EqSt.

Section Forall.
  Context {A : Type}.
  Variable (P : A -> Prop).

  CoInductive SForall : Stream A -> Prop :=
  | Forall_Cons : forall a sa,
      P a ->
      SForall sa ->
      SForall (a ⋅ sa).

  Lemma SForall_forall : forall sa,
      SForall sa <-> forall n, P (Str_nth n sa).
End Forall.