StreamCalculus.stream_equalities

Require Import MathClasses.interfaces.abstract_algebra.
Require Import StreamCalculus.streamscommon.
Require Import StreamCalculus.stream_equality_up_to.
Require Import StreamCalculus.stream_equality.
Section StreamEqualities.
  Context {T:Type}.
  Context `{R:Ring T}.
  Lemma streamEqualUpTo_streamEquality s1 s2:
    (forall n, StreamEqualUpTo n s1 s2) <-> streamEquality s1 s2.
  Proof.
    split.
    - intros H n.
      specialize (H (S n)).
      specialize (streamEqualUpTo_inverse H).
      intros. destruct H0.
      revert H1. revert H0. revert H. revert s1. revert s2.
      induction n. { trivial. }
      intros.
      specialize (streamEqualUpTo_inverse H1).
      intros. destruct H2.
      now apply (IHn (derive s2) (derive s1) H1).
    - intros.
      revert H. revert s1. revert s2.
      induction n. { constructor. }
      constructor.
      + apply IHn. now apply eq_derive.
      + apply H.
  Qed.

  Lemma eqUpTo_fromPointwise s1 s2:
    s1 = s2 -> (forall n, StreamEqualUpTo n s1 s2).
  Proof.
    apply streamEqualUpTo_streamEquality.
  Qed.

End StreamEqualities.