StreamCalculus.conv_division

Require Import StreamCalculus.streamscommon.
Require Import StreamCalculus.sde.
Require Import StreamCalculus.special_streams.
Require Import StreamCalculus.conv_ring.
Require Import StreamCalculus.stream_addition.
Require Import StreamCalculus.stream_equality_up_to.
Require Import StreamCalculus.stream_equality.
Require Import StreamCalculus.stream_equalities.
Require Import MathClasses.interfaces.abstract_algebra.
Require Import StreamCalculus.conv_ring_ring.
Require Import Ring.
Set Implicit Arguments.

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

  Add Ring conv_ring: (conv_ring T).

  Definition conv_inverse_tail_tail (s:unit -> Stream T) (recip_tail: ((unit -> Stream T) -> Stream T)): Stream T:=
    - (recip_tail s) * (s ()) - derive (s ()).

  Lemma conv_inverse_tail_tail_causal2:
    causal2 conv_inverse_tail_tail.
  Proof.
    intros a1 a2 i1 i2 n Ha Hi.
    unfold conv_inverse_tail_tail.
    rewrite (Ha i1 i2).
    rewrite (eqUpTo_inverse_tail (Hi ())).
    now repeat rewrite (eqUpTo_back (Hi _)).
    intros. now rewrite (eqUpTo_back (Hi _)).
  Qed.

  Definition conv_inverse_tail s: Stream T:=corec (fun i=>- i ()) conv_inverse_tail_tail (fun _=>s).

  Lemma conv_inverse_tail_tail_cor s:
    derive (conv_inverse_tail s) = - conv_inverse_tail s * s - (derive s) . (* - s * (conv_inverse_tail s).*)
  Proof.
    unfold conv_inverse_tail.
    rewrite corec_tail.
    unfold conv_inverse_tail_tail at 1.
    - reflexivity.
    - destruct R, ring_group, abgroup_group, group_monoid, monoid_semigroup.
      trivial.
    - intros i1 i2 H. now rewrite H.
    - exact conv_inverse_tail_tail_causal2.
  Qed.

  Definition conv_inverse s:=1 + X * conv_inverse_tail s.

  Lemma conv_inverse_tail_cor (s: Stream T):
    derive (conv_inverse s) = - s * (conv_inverse s).
  Proof.
    unfold conv_inverse at 1.
    rewrite addition_derive.
    unfold one at 1. rewrite scalar_derive_null.
    rewrite derive_X_id.
    rewrite left_identity.
    unfold equiv. rewrite recursive_equality; split; unfold conv_inverse.
    - cbn.
      rewrite addition_pointwise.
      cbn.
      now rewrite left_absorb, right_identity, right_identity.
    - rewrite commutativity.
      rewrite cleaner_mult_derive.
      rewrite conv_inverse_tail_tail_cor.
      rewrite addition_derive.
      unfold one at 1. rewrite scalar_derive_null, left_identity.
      rewrite derive_X_id.
      rewrite addition_pointwise. cbn.
      assert ([1 + 0 * - s 0%nat] = [1]).
      {now rewrite left_absorb, right_identity. }
      rewrite H, left_identity.
      rewrite (minus_eq_minusOne (conv_inverse_tail s)).
      rewrite <- minus_derive.
      ring.
  Qed.

  Lemma conv_inverse_cor s:
    (1 + X * s) * conv_inverse s = 1.
  Proof.
    apply recursive_equality. split.
    - unfold conv_inverse.
      cbn.
      repeat rewrite addition_pointwise.
      cbn.
      repeat rewrite left_absorb.
      now repeat rewrite right_identity.
    - cbv [one stream_addition.streamOne].
      rewrite scalar_derive_null.
      rewrite cleaner_mult_derive.
      rewrite addition_derive.
      rewrite scalar_derive_null.
      rewrite left_identity.
      rewrite derive_X_id.
      rewrite addition_pointwise.
      cbn.
      assert ([Aone + 0 * s 0%nat] = [ 1 ]).
      { rewrite left_absorb. now rewrite right_identity. }
      rewrite H.
      rewrite left_identity.
      rewrite conv_inverse_tail_cor.
      rewrite (minus_eq_minusOne s).
      + rewrite <- (conv_left_identity s) at 1.
        repeat rewrite <- distribute_r.
        rewrite negate_r.
        * now repeat rewrite left_absorb.
        * exact stream_add_group.
  Qed.
End ConvInverse.

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

  Add Ring conv_ring': (conv_ring T).

  Lemma divide_right a (x:Stream T):
    x * (1 + X * a) = 1 -> x = conv_inverse a.
  Proof.
    intros.
    assert (x = x * ((1 + X * a) * conv_inverse a)).
    {now rewrite conv_inverse_cor, right_identity. }
    rewrite H0.
    rewrite associativity.
    now rewrite H, left_identity.
  Qed.

  Global Instance conv_proper_up_to: @Proper (Stream T -> Stream T) (StreamEqualUpTo n ==> StreamEqualUpTo (S n)) (conv_inverse (T:=T)).
  Proof.
    intros n s1 s2 H.
    constructor.
    - unfold conv_inverse.
      repeat rewrite addition_derive_up_to.
      repeat rewrite derive_X_upto.
      unfold one. rewrite scalar_derive_upto.
      repeat rewrite plus_left_absorb; [ | exact R | exact R].
      unfold conv_inverse_tail.
      apply corec_causal; trivial.
      + now destruct R, ring_group, abgroup_group, group_monoid, monoid_semigroup.
      + intros i1 i2 H'. now rewrite H'.
      + exact (conv_inverse_tail_tail_causal2 (T:=T)).
    - unfold conv_inverse.
      repeat rewrite addition_pointwise.
      cbn. repeat rewrite left_absorb.
      now repeat rewrite right_identity.
  Qed.

  Global Instance conv_proper: @Proper (Stream T -> Stream T) (equiv ==> equiv) (conv_inverse (T:=T)).
  Proof.
    intros s1 s2 H.
    apply streamEqualUpTo_streamEquality.
    specialize (streamEqualUpTo_streamEquality s1 s2). destruct 1.
    specialize (H1 H).
    intros n.
    apply eqUpTo_back.
    now rewrite H1.
  Qed.

  Class Inverse (s:T):= {ex_inv: { i | s * i = 1} }.

  Definition conv_apreinverse s x:=conv_inverse (derive s * [x]) * [x].

  Lemma conv_ainverse s `{H: Inverse (s 0%nat)}: Stream T.
    destruct H, ex_inv0.
    exact (conv_apreinverse s x).
  Defined.

  Lemma conv_apreinverse_cor s x:
    s 0%nat * x = 1 ->
    s * conv_apreinverse s x= 1.
  Proof.
    unfold conv_apreinverse.
    specialize (fundamental_theorem s). intros.
    rewrite <- H at 1.
    rewrite <- conv_left_identity at 1.
    unfold one at 1, streamOne at 1.
    assert (forall a, a=1 -> [ 1 ] = [ a ]).
    { intros. now rewrite H1. }
    rewrite (H1 ((s 0%nat) * x)).
    rewrite conv_scalar.
    (*ring. Not working here *)
    repeat rewrite associativity.
    rewrite <- (associativity [s 0%nat]).
    rewrite distribute_left.
    rewrite (commutativity [x]).
    rewrite <- conv_scalar.
    rewrite <- (H1 ((s 0%nat) * x)).
    rewrite (commutativity [x]).
    rewrite <- (associativity X).
    rewrite <- (associativity [s 0%nat]).
    assert ([1] = 1). { now cbv. }
    rewrite H2.
    rewrite conv_inverse_cor.
    rewrite commutativity.
    rewrite associativity.
    rewrite (commutativity [x]).
    rewrite <- conv_scalar.
    rewrite right_identity.
    now rewrite H0.
    exact R.
    exact H0.
    exact H0.
  Qed.

  Lemma conv_ainverse_cor s `{H: Inverse (s 0%nat)}:
    s * conv_ainverse s= 1.
  Proof.
    specialize (conv_apreinverse_cor s). intros.
    unfold conv_ainverse.
    destruct H, ex_inv0.
    now apply H0.
  Qed.
End ConvInverseProp.