StreamCalculus.stream_equality_up_to

Require Import MathClasses.interfaces.abstract_algebra.
Require Import StreamCalculus.streamscommon.
Require Import Omega.
Set Implicit Arguments.

Section StreamEqualityUpTo.
  Context {T:Type}.
  Context `{E: Setoid T}.

  Inductive StreamEqualUpTo: nat -> relation (Stream T):=
  | equalO s1 s2: StreamEqualUpTo O s1 s2
  | equalS s1 s2 n: StreamEqualUpTo n (derive s1) (derive s2) -> (s1 O) = (s2 O) -> StreamEqualUpTo (S n) s1 s2.

  Lemma streamEqualUpTo_inverse n s1 s2:
    StreamEqualUpTo (S n) s1 s2 -> (s1 O) = (s2 O) /\ StreamEqualUpTo n (derive s1) (derive s2).
  Proof.
    assert (S n>=1). {omega. }
    assert (forall n', eq (S n) (S n') -> eq n n').
    { intros. omega. }
    destruct 1. {omega. }
    split. { trivial. }
    rewrite (H0 n0); trivial.
  Qed.

  Lemma eqUpTo_inverse_head n s1 s2:
    StreamEqualUpTo (S n) s1 s2 -> (s1 O) = (s2 O).
  Proof.
    apply streamEqualUpTo_inverse.
  Qed.

  Lemma eqUpTo_inverse_tail n s1 s2:
    StreamEqualUpTo (S n) s1 s2 -> StreamEqualUpTo n (derive s1) (derive s2).
  Proof.
    apply streamEqualUpTo_inverse.
  Qed.

  Lemma eqUpTo_refl:
    (forall n' s1, StreamEqualUpTo n' s1 s1).
  Proof.
    induction n'. { constructor. }
    constructor.
    - apply IHn'.
    - reflexivity.
  Qed.

  Lemma eqUpTo_symm:
    (forall n' s1 s2, StreamEqualUpTo n' s1 s2 -> StreamEqualUpTo n' s2 s1).
  Proof.
    induction n'. { constructor. }
    intros.
    - intros.
      specialize (streamEqualUpTo_inverse H).
      intros. destruct H0.
      constructor.
      + apply IHn'. exact H1.
      + now rewrite H0.
  Qed.

  Lemma eqUpTo_trans:
    (forall n' s1 s2 s3, StreamEqualUpTo n' s1 s2 -> StreamEqualUpTo n' s2 s3 -> StreamEqualUpTo n' s1 s3).
  Proof.
    induction n'. { constructor. }
    intros.
    specialize (streamEqualUpTo_inverse H).
    specialize (streamEqualUpTo_inverse H0).
    intros.
    destruct H1.
    destruct H2.
    constructor.
    - now apply (IHn' (derive s1) (derive s2)).
    - rewrite H2. now rewrite H1.
  Qed.

  Context (n:nat).
  Global Instance upToEq: Equiv (Stream T):=StreamEqualUpTo n.
  Global Instance upToSetoid: Setoid (Stream T).
  Proof.
    constructor;
      cbv [equiv upToEq].
      - cbv [Reflexive]. apply (eqUpTo_refl).
      - cbv [Symmetric]. apply eqUpTo_symm.
      - cbv [Transitive]. apply eqUpTo_trans.
  Qed.

  Lemma eqUpTo_back:
    forall n' s1 s2, StreamEqualUpTo (S n') s1 s2 -> StreamEqualUpTo n' s1 s2.
  Proof.
    induction n'. { constructor. }
    intros.
    specialize (streamEqualUpTo_inverse H).
    destruct 1.
    constructor.
    - now apply IHn'.
    - trivial.
  Qed.

  Instance nat_lt': Lt nat:=nat_lt.

  Lemma eqUpTo_lePointwise:
    forall n p q,
      StreamEqualUpTo n p q <-> (forall n', n' < n -> p n' = q n').
  Proof.
    induction n0.
    - intros; split; intros.
      + cbv in H0. omega.
      + constructor.
    - split; intros.
      + specialize (eqUpTo_inverse_tail H).
        specialize (eqUpTo_inverse_head H).
        intros.
        destruct n'.
        * trivial.
        * repeat rewrite derive_rewrite.
          apply IHn0.
          -- trivial.
          -- cbv. cbv in H0. omega.
      + constructor.
        * apply IHn0.
          intros.
          cbv [derive].
          apply H.
          cbv. cbv in H0.
          omega.
        * apply H. cbv. omega.
  Qed.
End StreamEqualityUpTo.
Notation "s1 =- n s2" := (StreamEqualUpTo n s1 s2) (at level 50).