StreamCalculus.conv_ring

Require Import Omega.
Require Import MathClasses.interfaces.abstract_algebra.
Require Import StreamCalculus.streamscommon.
Require Import StreamCalculus.stream_addition.
Require Import StreamCalculus.special_streams.
Require Import MathClasses.theory.rings.
Require Import StreamCalculus.companion.
Require Import StreamCalculus.stream_equality.
Require Import StreamCalculus.stream_equality_up_to.
Require Import StreamCalculus.stream_equalities.
Require Import Coq.Setoids.Setoid.

Set Implicit Arguments.

Section StreamRingConv.
  Context {T:Type}.
  Context `{R:Ring T}.

  Instance sSetoid: Setoid (Stream T):=streamSetoid.

  Global Instance sPlusProper: Proper (equiv==>equiv==>equiv) streamAddition:=plusProp.
  Global Instance deriveProper: Proper (equiv==>equiv) (@derive T):=deriveProp.
  Global Instance scalar_to_streamProper: @Proper (T -> Stream T) (equiv==>equiv) scalar_to_stream:=scalar_to_streamProp.
  Lemma nullStream_derive: (derive 0) = 0.
  Proof.
      exact nullStream_derive.
  Qed.

  Global Instance scalar_to_stream_upto: Proper (Ae ==> StreamEqualUpTo n) scalar_to_stream.
  Proof.
    intros n t1 t2 H.
    apply streamEqualUpTo_streamEquality.
    now rewrite H.
  Qed.

  Instance subRel: subrelation streamEquality (StreamEqualUpTo n)|2.
  Proof.
    cbv [subrelation].
    intros.
    now apply streamEqualUpTo_streamEquality.
  Qed.

  Instance id_proper n: Proper ((StreamEqualUpTo n)==>(StreamEqualUpTo n)) id.
  Proof. cbv. trivial. Qed.

  Goal forall (s1:Stream T) s2 s3 n, StreamEqualUpTo n s1 s2 -> StreamEqualUpTo n s2 s3 -> StreamEqualUpTo n s1 s3.
  Proof.
    intros. now rewrite H.
  Qed.

  Global Instance streamEqualUpTo_streamEquality': @Proper (Stream T -> Stream T) (streamEquality ==> StreamEqualUpTo n) id.
  Proof.
    intros n s1 s2 H.
    apply streamEqualUpTo_streamEquality.
    now cbn.
  Qed.

  Lemma id_test (o:Stream T) n: StreamEqualUpTo n (id o) o.
  Proof. now cbv. Qed.

  Goal forall (s1:Stream T) s2 n, streamEquality s1 s2 -> StreamEqualUpTo n s1 s2.
  Proof.
    intros. rewrite <- id_test. rewrite <- (id_test s2). now rewrite H.
  Qed.

  Global Instance streamMult: Mult (Stream T):=fix sMult s1 s2 n:=match n with
  

| 0 => (s1 O) * (s2 O)
  

| S n=> ((sMult (derive s1) s2 n) + (sMult (scalar_to_stream (s1 O)) (derive s2) n))
  

end.

  Lemma cleaner_mult_derive s1 s2:
    (derive (s1 * s2)) = (derive s1 * s2) + ([s1 O] * (derive s2)).
  Proof.
    intros n. cbn. cbv[plus streamAddition]. reflexivity.
  Qed.

  Lemma conv_prod_uptoproper:
    forall n, Proper (StreamEqualUpTo n ==> StreamEqualUpTo n ==> StreamEqualUpTo n) mult.
  Proof.
    induction n. { constructor. }
    cbv [Proper respectful].
    intros s1 s2 H s3 s4 H'.
    specialize (streamEqualUpTo_inverse H). destruct 1.
    specialize (streamEqualUpTo_inverse H'). destruct 1.
    constructor.
    - rewrite <- id_test. rewrite <- (id_test (derive (s2 * s4))).

      rewrite cleaner_mult_derive. rewrite cleaner_mult_derive.
      rewrite id_test. rewrite id_test.
      assert (StreamEqualUpTo n (derive s1 * s3) (derive s2 * s4)).
      { apply IHn. exact H1. now apply eqUpTo_back. }
      rewrite H4.
      assert (StreamEqualUpTo n ([s1 O] * derive s3) ([s2 O] * derive s4)).
      { apply IHn. rewrite <- id_test. rewrite <- (id_test ([s2 O])). now rewrite H0. exact H3. }
      now rewrite H5.
    - cbn. rewrite H0. now rewrite H2.
  Qed.

  Global Instance conv_prod_proper_upto n: Proper (StreamEqualUpTo n ==> StreamEqualUpTo n ==> StreamEqualUpTo n) mult.
  Proof.
    apply conv_prod_uptoproper.
  Qed.

  Global Instance conv_prod_proper: @Proper (Stream T -> Stream T -> Stream T) (equiv==>equiv==>equiv) mult.
  Proof.
    cbv [equiv streamEq].
    apply streamTowerInduction;
      cbv [Proper respectful].
    - intros. apply streamEqualUpTo_streamEquality.
      intros n. apply H; apply streamEqualUpTo_streamEquality. apply H0. apply H1.
    - constructor.
    - intros n H''.
      intros s1 s2 H sa sb H'.
      rewrite H. now rewrite H'.
  Qed.

  Global Instance neg_proper n: @Proper (Stream T -> Stream T) (StreamEqualUpTo n ==> StreamEqualUpTo n) negate.
  Proof.
    induction n.
    - constructor.
    - intros s1 s2 H.
      constructor.
      + apply IHn.
        now apply streamEqualUpTo_inverse.
      + apply streamEqualUpTo_inverse in H. destruct H.
        cbv. now rewrite H.
  Qed.

  Global Instance neg_proper_upto: @Proper (Stream T -> Stream T) (equiv ==> equiv) negate.
  Proof.
    intros s1 s2 H.
    intros n.
    cbv. now rewrite (H n).
  Qed.

  Lemma conv_left_absorb (s:Stream T): 0 * s = 0.
  Proof.
    apply (equalityByTower3 (fun s1 s2 s3=>0 * s1) (fun s1 s2 s3=>0)).
    - intros n H s1 _ _.
      constructor.
      + rewrite <- (id_test (derive 0)).
        rewrite nullStream_derive.
          rewrite <- (id_test (derive (0 * s1))).
        rewrite cleaner_mult_derive.
        rewrite nullStream_derive.
          rewrite id_test.
        rewrite H.
          specialize (id_test (scalar_to_stream (zero O))). intros. rewrite <- H0.
        rewrite scalar0_is_nullStream.
          rewrite id_test.
        rewrite H.
        apply streamEqualUpTo_streamEquality.
        cbv. intros.
        apply left_identity.
        exact s. exact s. exact s. exact s.
      + cbv. apply left_absorb.
    - exact s.
    - exact s.
  Qed.

  Lemma conv_left_identity (s:Stream T): 1 * s = s.
  Proof.
    apply (equalityByTower3 (fun s1 s2 s3=>[1] * s1) (fun s1 s2 s3=>s1)).
    - intros n H s0 _ _.
      constructor.
      + rewrite <- (id_test (derive ([1]*s0))).
        rewrite cleaner_mult_derive.
        rewrite scalar_derive_null.
        rewrite conv_left_absorb.
        rewrite left_identity.
        rewrite id_test.
        cbn.
        apply H.
        exact s0. exact s0.
      + cbn. now rewrite left_identity.
    - exact s.
    - exact s.
  Qed.

  Lemma derive_X_id s1:
    derive ( X * s1 ) = s1.
  Proof.
    rewrite cleaner_mult_derive.
    rewrite derive_X.
    cbn.
    rewrite conv_left_identity.
    rewrite scalar0_is_nullStream.
    rewrite conv_left_absorb.
    now rewrite right_identity.
  Qed.

  Lemma derive_X_upto s1 n:
    StreamEqualUpTo n (derive ( X * s1 )) s1.
  Proof.
    rewrite cleaner_mult_derive.
    rewrite derive_X.
    cbn.
    rewrite conv_left_identity.
    rewrite scalar0_is_nullStream.
    rewrite conv_left_absorb.
    now rewrite right_identity.
  Qed.

  Lemma fundamental_theorem (s: Stream T):
    [s O] + X * (derive s) = s.
  Proof.
    apply recursive_equality. split.
    - cbv.
      now rewrite left_absorb, right_identity.
    - rewrite addition_derive.
      rewrite derive_X_id.
      rewrite scalar_derive_null.
      now rewrite left_identity.
  Qed.

  Lemma X_assoc s1 s2:
    X * (s1 * s2) = (X * s1) * s2.
  Proof.
    apply recursive_equality. split.
    - cbn.
      now repeat rewrite left_absorb.
    - rewrite derive_X_id.
      rewrite cleaner_mult_derive.
      rewrite derive_X_id.
      cbn.
      cbv [equiv].
      assert ([0 * s1 O] * derive s2 = 0).
      { rewrite left_absorb, scalar0_is_nullStream, conv_left_absorb. reflexivity. }
      rewrite H.
      (*rewrite left_absorb, scalar0_is_nullStream, conv_left_absorb. || takes way too long *)
      now rewrite right_identity.
  Qed.

  Lemma distribute_left (s1: Stream T) s2 s3:
    s1 * (s2 + s3) = s1 * s2 + s1 * s3.
  Proof.
    apply (equalityByTower3 (fun s1 s2 s3=>s1 * (s2 + s3)) (fun s1 s2 s3=>s1*s2 + s1*s3)).
    intros n H s4 s5 s6.
    constructor.
    - rewrite <- id_test.
      rewrite cleaner_mult_derive.
      rewrite addition_derive.
      rewrite id_test.
      repeat rewrite H.
      apply streamEqualUpTo_streamEquality.
      rewrite addition_derive.
      repeat rewrite cleaner_mult_derive.
      rewrite associativity.
      rewrite <- (associativity (derive s4 * s5) (derive s4 * s6) ([s4 O]*derive s5)).
      rewrite (commutativity (derive s4 * s6)).
      rewrite associativity.
      now rewrite associativity.
    - cbn.
      repeat rewrite addition_pointwise.
      cbn.
      now rewrite distribute_l.
  Qed.

  Lemma conv_comm (s1: Stream T) s2:
    s1 * s2 = s2 * s1.
  Proof.
    apply (equalityByTower3 (fun s1 s2 s3=>s1 * s2) (fun s1 s2 s3=>s2 * s1)).
    * intros n H sa sb _.
      constructor.
      - rewrite <- id_test. rewrite <- (id_test (derive (sb * sa))).
        repeat rewrite cleaner_mult_derive.
        rewrite <- (fundamental_theorem sb) at 1.
        rewrite <- (fundamental_theorem sa) at 3.
        repeat rewrite distribute_left.
          repeat rewrite id_test.
        rewrite (H [sb O] (derive sa)).
        rewrite (H [sa O] (derive sb)).
        rewrite (H (derive sa) (X*derive sb)).
        rewrite (H (derive sb) (X*derive sa)).
          rewrite <- (id_test (X*derive sb*derive sa)).
          rewrite <- (id_test (X*derive sa*derive sb)).
        repeat rewrite <- X_assoc.
          repeat rewrite id_test.
        rewrite (H (derive sb) (derive sa)).
          apply streamEqualUpTo_streamEquality.
        rewrite commutativity, associativity.
        rewrite <- (associativity (derive sb * [sa O]) (X*(derive sa * derive sb))).
        rewrite (commutativity (X*(derive sa * derive sb))).
        now rewrite associativity.
          exact s1. exact s1. exact s1. exact s1. exact s1.
      - cbn. now rewrite commutativity.
    * exact s1.
  Qed.

  Lemma conv_scalar t1 t2:
    [ t1 * t2 ] = [ t1 ] * [ t2 ].
  Proof.
    apply recursive_equality. split.
    - now cbn.
    - rewrite cleaner_mult_derive.
      repeat rewrite scalar_derive_null.
      rewrite (conv_comm [[t1] O]).
      repeat rewrite conv_left_absorb.
      now rewrite left_identity.
  Qed.

  Lemma conv_assoc (s1: Stream T) s2 s3:
    s1 * (s2 * s3) = (s1 * s2) * s3.
  Proof.
    apply (equalityByTower3 (fun s1 s2 s3=>s1 * (s2 * s3)) (fun s1 s2 s3=>(s1 * s2) * s3)).
    intros n H sa sb sc.
    constructor.
    - rewrite <- id_test. rewrite <- (id_test (derive (sa * sb * sc))).
      repeat rewrite cleaner_mult_derive.
      rewrite (conv_comm (derive sa * sb + [sa O] * derive sb)).
      repeat rewrite distribute_left.
        repeat rewrite id_test.
      rewrite H. rewrite H. rewrite H.
        apply streamEqualUpTo_streamEquality.
      rewrite associativity.
      rewrite (conv_comm (sc)).
      rewrite (conv_comm (sc)).
      cbn.
      now rewrite conv_scalar.
    - cbn.
      now rewrite associativity.
  Qed.

  Instance conv_comm_monoid: @CommutativeMonoid (Stream T) streamEquality (streamMult) [1].
  Proof.
    constructor.
    - constructor.
      + constructor.
        * exact streamSetoid.
        * cbv [Associative HeteroAssociative].
          apply conv_assoc.
        * exact conv_prod_proper.
      + cbv [mon_unit zero_is_mon_unit LeftIdentity].
        apply conv_left_identity.
      + cbv [mon_unit zero_is_mon_unit RightIdentity].
        intros x.
        specialize (conv_left_identity x). intros. rewrite conv_comm in H.
        apply H.
    - cbv [Commutative].
      apply conv_comm.
  Qed.

  Global Instance StreamRing : Ring (Stream T).
  Proof.
    constructor.
    - exact stream_add_abgroup.
    - exact conv_comm_monoid.
    - cbv [LeftDistribute LeftHeteroDistribute].
      apply distribute_left.
  Qed.
End StreamRingConv.

Section StreamConvProperties.
  Variable (T: Type).
  Context `{R: Ring T}.

  Lemma move_minus a (b:Stream T):
    -a * b = - (a * b).
  Proof.
    apply (add_both (a:=(a * b))).
    rewrite commutativity.
    rewrite <- distribute_r.
    rewrite left_inverse.
    rewrite right_inverse.
    now rewrite left_absorb.
  Qed.

  Lemma minus_eq_minusOne (s:Stream T):
    - s = -1 * s.
  Proof.
    assert (s = 1 * s) by now rewrite left_identity.
    rewrite H at 1.
    now rewrite move_minus.
  Qed.

  Lemma minusOne_squared:
    -1 * -streamOne = 1.
  Proof.
    specialize (minus_eq_minusOne (- streamOne)). intros.
    rewrite <- H.
    rewrite double_negation. reflexivity.
  Qed.
End StreamConvProperties.

Section StreamRingConvUpTo.
  Variable (T: Type).
  Context `{R: Ring T}.

  Instance ConvRingUpTo: Ring (Ae:=upToEq n) (Aplus:=streamAddition) (Stream T).
  Proof.
    intros n.
    constructor.
    - constructor.
      + constructor.
        * constructor.
          -- constructor.
             ++ apply upToSetoid.
             ++ intros x y z.
                cbv [equiv upToEq sg_op plus_is_sg_op].
                apply streamEqualUpTo_streamEquality.
                now rewrite associativity.
             ++ intros s1 s2 H0 s3 s4 H1.
                cbv [sg_op plus_is_sg_op].
                now apply properUpTo.
          -- intros s.
             apply streamEqualUpTo_streamEquality.
             apply left_identity.
          -- intros s.
             apply streamEqualUpTo_streamEquality.
             apply right_identity.
        * constructor.
          -- apply upToSetoid.
          -- apply upToSetoid.
          -- intros s1 s2 H0.
             now rewrite H0.
        * intros s.
          apply streamEqualUpTo_streamEquality.
          apply left_inverse.
        * intros s.
          apply streamEqualUpTo_streamEquality.
          apply right_inverse.
      + intros s1 s2.
        apply streamEqualUpTo_streamEquality.
        apply commutativity.
    - constructor.
      + constructor.
        * constructor.
          -- apply upToSetoid.
          -- intros s1 s2 s3.
             apply streamEqualUpTo_streamEquality.
             apply associativity.
          -- intros s1 s2 H0 s3 s4 H1.
             now rewrite H0, H1.
        * intros s.
          apply streamEqualUpTo_streamEquality.
          apply left_identity.
        * intros s.
          apply streamEqualUpTo_streamEquality.
          apply right_identity.
      + intros s1 s2.
        apply streamEqualUpTo_streamEquality.
        apply commutativity.
    - intros s1 s2 s3.
      apply streamEqualUpTo_streamEquality.
      apply distribute_l.
  Qed.

  Lemma plus_left_absorb s n:
    upToEq n (0 + s) s.
  Proof.
    apply streamEqualUpTo_streamEquality.
    now rewrite left_identity.
  Qed.
End StreamRingConvUpTo.