StreamCalculus.stream_addition

Require Import MathClasses.interfaces.abstract_algebra.
Require Import StreamCalculus.streamscommon.
Require Import StreamCalculus.special_streams.
Require Import StreamCalculus.stream_equality.
Require Import StreamCalculus.stream_equality_up_to.
Require Import StreamCalculus.stream_equalities.
Set Implicit Arguments.
Require Import Omega.
Section Addition.
  Context {T:Type}.
  Context `{R:Ring T}.
  Global Instance streamAddition: Plus (Stream T):=fun s1 s2 n=>(s1 n) + (s2 n).

End Addition.
Section StreamPlusEquality.
  Context {T:Type}.
  Context `{R:Ring T}.
  Notation "[ t ]":=(scalar_to_stream t).

  Global Instance streamOne: One (Stream T):=[ 1 ].
  Global Instance streamNegate: Negate (Stream T):=fun s n=>- (s n).

  Lemma addition_derive s1 s2:
    derive (s1 + s2) = (derive s1) + (derive s2).
  Proof.
    intros n.
    now cbv.
  Qed.


  Lemma addition_pointwise (s1: Stream T) s2 n:
    (s1 + s2) n ≡ s1 n + s2 n.
  Proof. now cbv. Qed.

  Require Import MathClasses.theory.rings.
  Instance stream_add_semigroup: SemiGroup (Stream T).
  Proof.
    constructor.
    - exact streamSetoid.
    - intros x y z n.
      apply plus_assoc.
    - cbv.
      intros.
      now rewrite H, H0.
  Qed.

  Instance stream_add_monoid: Monoid (Stream T).
  Proof.
    constructor.
    - exact stream_add_semigroup.
    - intros s n.
      cbv [sg_op plus_is_sg_op].
      cbv [streamZero nullStream].
      apply plus_0_l.
    - cbv [RightIdentity mon_unit zero_is_mon_unit].
      intros s n.
      cbv [sg_op plus_is_sg_op].
      cbv [streamZero nullStream].
      apply plus_0_r.
  Qed.

  Instance stream_add_group: Group (Stream T).
  Proof.
    destruct R.
    destruct ring_group.
    destruct abgroup_group.
    constructor.
    - exact stream_add_monoid.
    - constructor.
      + exact streamSetoid.
      + exact streamSetoid.
      + destruct negate_proper.
        cbv.
        intros.
        apply sm_proper, H.
    - cbv [LeftInverse].
      intros s n.
      cbv [mon_unit zero_is_mon_unit].
      cbv [streamZero nullStream].
      cbv [sg_op plus_is_sg_op].
      apply negate_l.
    - cbv [RightInverse].
      intros s n.
      cbv [mon_unit zero_is_mon_unit].
      cbv [streamZero nullStream].
      cbv [sg_op plus_is_sg_op].
      apply negate_r.
  Qed.

  Global Instance stream_add_abgroup: AbGroup (Stream T).
  Proof.
    constructor.
    - exact stream_add_group.
    - cbv.
      intros.
      apply plus_comm.
  Qed.

  Lemma scalar_plus a b: [a + b] = [a] + [b].
  Proof.
    apply recursive_equality. split.
    - now cbn.
    - rewrite addition_derive.
      repeat rewrite scalar_derive_null.
      now rewrite left_identity.
  Qed.

  Instance plusProp: Proper (equiv==>equiv==>equiv) streamAddition.
  Proof.
    cbv [Proper respectful].
    intros.
    cbv.
    intros.
    cbv in H.
    rewrite H.
    cbv in H0.
    rewrite H0.
    reflexivity.
  Qed.

  Lemma minus_derive s:
    -(derive s) = derive(- s).
  Proof.
    apply s_eq_pointwise.
    intros n.
    cbv [derive].
    now cbv [negate streamNegate].
  Qed.

  Lemma minus_one:
    [ -1 ] = -1.
  Proof.
    apply s_eq_pointwise.
    intros.
    destruct n.
    - now cbn.
    - cbv [negate streamNegate].
      cbn.
      cbv [zero streamZero nullStream].
      assert (0 - 0 = 0). { apply right_inverse. }
      cbv [zero] in H.
      remember (Anegate Azero).
      rewrite <- H.
      rewrite Heqt.
      now rewrite left_identity.
  Qed.

  Lemma add_both x y (a: Stream T):
    x + a = y + a -> x = y.
  Proof.
    intros.
    assert (x = x + a - a). { rewrite <- associativity. rewrite right_inverse. now rewrite right_identity. }
    assert (y = y + a - a). { rewrite <- associativity. rewrite right_inverse. now rewrite right_identity. }
    rewrite H0, H1.
    now rewrite H.
  Qed.

  Lemma move_plus_right a x (y:Stream T):
    x = y + a -> x - a = y.
  Proof.
    intros.
    rewrite H.
    rewrite <- associativity.
    rewrite right_inverse.
    cbv [mon_unit zero_is_mon_unit].
    now rewrite right_identity.
  Qed.

  Lemma double_negation (s: Stream T):
    - - s = s.
  Proof.
    assert (--s - s=0).
    { rewrite negate_l. reflexivity. exact stream_add_group. }
    assert (s -s = 0).
    { rewrite negate_r. reflexivity. exact stream_add_group. }
    apply (add_both (a:=-s)).
    now rewrite H, H0.
  Qed.

End StreamPlusEquality.

Section StreamPlusEqUpTo.
  Context {T:Type}.
  Context `{R:Ring T}.
  Notation "[ t ]":=(scalar_to_stream t).
  Context (n:nat).

  Lemma plusAssocUpTo:
    (forall n' (s1:Stream T) s2 s3, StreamEqualUpTo n' (s1 & (s2 & s3)) ((s1 & s2) & s3)).
  Proof.
    induction n'. { constructor. }
    intros.
    constructor.
    - apply IHn'.
    - apply plus_assoc.
  Qed.

  Global Instance properUpTo n': Proper (StreamEqualUpTo n' ==> StreamEqualUpTo n' ==> StreamEqualUpTo n') streamAddition.
  Proof.
    induction n'. { constructor. }
    intros s1 s2 H0 s3 s4 H1.
    constructor.
    - apply IHn'.
      + specialize (streamEqualUpTo_inverse H0).
        destruct 1.
        exact H2.
      + specialize (streamEqualUpTo_inverse H1).
        destruct 1.
        exact H2.
    - specialize (streamEqualUpTo_inverse H0). destruct 1.
      specialize (streamEqualUpTo_inverse H1). destruct 1.
      cbv [streamAddition].
      rewrite H.
      now rewrite H3.
  Qed.

  Require Import MathClasses.theory.rings.
  Lemma stream_add_semigroup': @SemiGroup (Stream T) (StreamEqualUpTo n) streamAddition.
  Proof.
    constructor.
    - exact (upToSetoid n).
    - cbv [Associative HeteroAssociative].
      intros x y z.
      cbv [sg_op plus_is_sg_op].
      apply plusAssocUpTo.
    - apply properUpTo.
  Qed.

  Lemma derive_minus_upto s n':
    StreamEqualUpTo n' (derive (- s)) (- derive s).
  Proof.
    apply streamEqualUpTo_streamEquality.
    now rewrite minus_derive.
  Qed.

  Lemma addition_derive_up_to s1 s2 n':
    StreamEqualUpTo n' (derive (s1 + s2)) ((derive s1) + (derive s2)).
  Proof.
    now apply streamEqualUpTo_streamEquality.
  Qed.

End StreamPlusEqUpTo.