StreamCalculus.math_stream

Require Import StreamCalculus.streamscommon.
Require Import StreamCalculus.special_streams.
Require Import StreamCalculus.conv_ring.
Require Import StreamCalculus.conv_sqrt.
Require Import StreamCalculus.conv_division.
Require Import MathClasses.interfaces.abstract_algebra.
(*Require Import StreamCalculus.stream_equality.*)

Require Import StreamCalculus.conv_ring_ring.
Require Import Ring.
Require Import StreamCalculus.conv_division.

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

  Add Ring conv_ring: (conv_ring T).

  Lemma pointwise_multiply (s: Stream T) t n:
    ([t] * s) n = t * (s n).
  Proof.
    revert s.
    induction n.
    - now cbn.
    - cbn.
      intros.
      assert (derive [t] * s = 0).
      { now rewrite scalar_derive_null, left_absorb. }
      rewrite (H n).
      unfold zero at 1. unfold streamZero, nullStream.
      rewrite left_identity.
      now rewrite IHn.
  Qed.

  Fixpoint stream_sum (s1: Stream T) s2 n:=match n with
           | 0 => s1 0%nat * s2 0%nat
           | S n' => s1 0%nat * s2 n + stream_sum (derive s1) s2 n'
           end.

  Lemma stream_sum_conv_prod s1 s2 n:
    (s1 * s2) n = stream_sum s1 s2 n.
  Proof.
    revert s1.
    induction n.
    - now cbn.
    - cbn.
      intros.
      rewrite pointwise_multiply, commutativity.
      now rewrite <- IHn.
  Qed.

  Lemma abc_step1 (s: Stream T) b c:
    s * s + b * s + c=0 ->
    (2 * s + b) * (2 * s + b) = b * b - 4 * c.
  Proof.
    intros.
    assert ((2 * s + b) * (2 * s + b) = 4 *( s * s + b * s + c) + b * b - 4 * c).
    { ring. }
    rewrite H0, H.
    ring.
  Qed.
End MathStream.

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

  Add Ring conv_ring': (conv_ring T).

  Context `{null_division_free: forall a b, a * b = 0 -> a = 0 \/ b = 0}.

  Context `{i2: @Inverse T Ae Amult Aone 2}.

  Lemma abc s:
    s * s + 1 * s + X=0 ->
    s = (-1 + conv_sqrt (- 4)) * conv_ainverse 2 \/
    s = (-1 - conv_sqrt (- 4)) * conv_ainverse 2.
  Proof.
    intros H.
    specialize (abc_step1 T s 1 X H).
    intros H1. clear H.
    destruct (sqrt_uniqueness (null_division_free:=null_division_free) (-4) (2 * s + 1)).
    - rewrite H1. ring.
    - left.
      rewrite <- H.
      enough (s = s * (2 * conv_ainverse 2)).
      { rewrite H0 at 1. ring. }
      specialize (conv_ainverse_cor 2).
      intros Hp. rewrite Hp.
      rewrite right_identity. (* strange *)
      ring.
    - right.
      rewrite <- H.
      enough (s = s * (2 * conv_ainverse 2)).
      { rewrite H0 at 1. ring. }
      specialize (conv_ainverse_cor 2).
      intros Hp. rewrite Hp.
      rewrite right_identity. (* strange *)
      ring.
  Qed.
End Abc.