StreamCalculus.conv_ring_ring

Require Import Ring.
Require Import MathClasses.interfaces.abstract_algebra.
Require Import StreamCalculus.streamscommon.
Require Import StreamCalculus.stream_addition.
Require Import StreamCalculus.conv_ring.
Require Import StreamCalculus.stream_equality.
Require Import Setoid.

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

  Lemma conv_ring:
    ring_theory (R:=Stream T) 0 1
      plus mult (fun a b=> a + (- b)) negate
      equiv.
  Proof.
    constructor; intros.
    - now rewrite left_identity.
    - now rewrite commutativity.
    - now rewrite associativity.
    - now rewrite left_identity.
    - now rewrite commutativity.
    - now rewrite associativity.
    - now rewrite distribute_r.
    - reflexivity.
    - rewrite negate_r.
      + reflexivity.
      + now destruct StreamRing, ring_group.
  Qed.

  Add Parametric Morphism: mult with signature (streamEquality ==> streamEquality ==> streamEquality) as conv_prod_morph.
  Proof.
    intros.
    now rewrite H, H0.
  Qed.

  Add Ring conv_ring: conv_ring.
End Conv_Ring.