StreamCalculus.stream_equality

Require Import StreamCalculus.streamscommon.
Require Import MathClasses.interfaces.abstract_algebra.
Section StreamEquality.
  Context {T:Type}.
  Context `{R:Ring T}.
  Definition streamEquality (s1 s2:Stream T):=forall n, (s1 n) = (s2 n).

  Global Instance streamEq: Equiv (Stream T):=streamEquality.
  Global Instance streamSetoid: Setoid (Stream T).
  Proof.
    constructor; cbv.
    - reflexivity.
    - now symmetry.
    - intros.
      now transitivity (y n).
  Qed.

  Lemma recursive_equality s1 s2:
    streamEquality s1 s2 <-> (s1 O) = (s2 O) /\ (derive s1) = (derive s2).
  Proof.
    split.
    - intros.
      split.
      trivial.
      intros n. cbv [derive]. trivial.
    - destruct 1.
      intros n. destruct n.
      + trivial.
      + now cbv [derive] in H0.
  Qed.

  Lemma s_eq_pointwise s1 s2: s1 = s2 <-> forall n, (s1 n)=(s2 n).
  Proof.
    split.
    - intros.
      cbv [equiv streamEq streamEquality] in H.
      apply H.
    - intros.
      now cbv [equiv streamEq streamEquality].
  Qed.

  Lemma eq_derive s1 s2: s1=s2 -> (derive s1)=(derive s2).
  Proof.
    intros.
    cbv [derive].
    rewrite s_eq_pointwise.
    now rewrite s_eq_pointwise in H.
  Qed.
  Instance deriveProp: Proper (equiv==>equiv) (@derive T).
  Proof.
    exact eq_derive.
  Qed.
End StreamEquality.