StreamCalculus.special_streams

Require Import StreamCalculus.streamscommon.
Require Import StreamCalculus.stream_equality.
Require Import StreamCalculus.stream_equality_up_to.
Require Import MathClasses.interfaces.abstract_algebra.
Section SpecialStreams.
  Context {T:Type}.
  Context `{R:Ring T}.
  Instance streamEq'': Equiv (Stream T):=streamEq.

  Definition nullStream := fun (_:nat)=>Azero.
  Global Instance streamZero: Zero (Stream T):=nullStream.

  Definition scalar_to_stream s:Stream T:= fun n=> match n with
                                    | 0 => s
                                    | S n => 0 n
                                    end.
  Notation "[ t ]":=(scalar_to_stream t).

  Definition X:Stream T:=fun n=>match n with
                       | 0 => 0
                       | S n=> [ 1 ] n
                       end.

  Lemma nullStream_derive: (derive 0) = 0.
  Proof.
    cbv. intros.
    reflexivity.
  Qed.

  Lemma eq_scalar_stream t1 t2: t1=t2 -> [ t1 ] = [ t2 ].
  Proof.
    intros.
    cbv.
    destruct n; now cbn.
  Qed.

  Instance scalar_to_streamProp: Proper (equiv==>equiv) scalar_to_stream.
  Proof.
    exact eq_scalar_stream.
  Qed.

  Lemma scalar_derive_null t1: derive [t1]=0.
  Proof.
    now cbn.
  Qed.

  Lemma scalar_derive_upto t1 n:StreamEqualUpTo n (derive [t1]) 0.
  Proof.
    now cbn.
  Qed.

  Lemma scalar0_is_nullStream: [0]=0.
  Proof.
    cbv.
    destruct n.
    - cbv[zero nullStream]. cbn. reflexivity.
    - cbv [zero]. cbn. cbv[nullStream]. reflexivity.
  Qed.

  Lemma derive_X: derive X=[1].
  Proof.
    cbv [derive X].
    now cbv.
  Qed.

End SpecialStreams.
Notation "[ t ]":=(scalar_to_stream t).