StreamCalculus.catalan

Require Import StreamCalculus.sde.
Require Import StreamCalculus.conv_ring.
Require Import StreamCalculus.conv_ring_ring.
Require Import StreamCalculus.special_streams.
Require Import StreamCalculus.streamscommon.
Require Import StreamCalculus.stream_addition.
Require Import StreamCalculus.math_stream.
Require Import StreamCalculus.conv_sqrt.
Require Import StreamCalculus.stream_equality_up_to.
Require Import MathClasses.interfaces.abstract_algebra.
Require Import Ring.
Require Import StreamCalculus.conv_division.

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

  Add Ring conv_ring: (conv_ring T).

  Context `{apart01: 0 = 1 -> False}.

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

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

  Definition cat' := corec (X:=False)
                           (fun _ => 1)
                           (fun i a=>(a i) * (a i)) (* maybe use streamsum *)
                           (fun i=>match i with end).

  Definition cat := 0 + X * cat'.

  Lemma cat'':
    derive (derive cat) = (derive cat) * (derive cat).
  Proof.
    unfold cat.
    rewrite addition_derive, derive_X_id.
    unfold one. try rewrite scalar_derive_null. rewrite nullStream_derive. rewrite left_identity.
    unfold cat' at 1.
    rewrite corec_tail.
    - reflexivity.
    - now destruct R, ring_group, abgroup_group, group_monoid, monoid_semigroup.
    - now intros in1 in2 x.
    - intros a1 a2 in1 in2 n Ha Hi.
      rewrite Ha.
      * reflexivity.
      * intros. now apply eqUpTo_back.
  Qed.

  Lemma cat_char:
    cat = X + cat * cat.
  Proof.
    rewrite <- fundamental_theorem at 1.
    unfold cat at 1. rewrite addition_pointwise. cbn.
    assert ([0 0%nat + 0 * 1] = 0).
    { rewrite left_absorb, right_identity.
      unfold zero at 1. unfold streamZero, nullStream.
      apply scalar0_is_nullStream. }
    rewrite H. rewrite left_identity. clear H.
    rewrite <- (fundamental_theorem (derive cat)) at 1.
    rewrite distribute_l.
    unfold cat at 1.
    unfold derive at 1. rewrite addition_pointwise.
    unfold zero, streamZero, nullStream at 1.
    assert ([0 + (X * cat') 1%nat] = 1).
    { rewrite left_identity. cbn.
      rewrite left_absorb.
      repeat rewrite right_identity.
      reflexivity. }
    rewrite H, right_identity. clear H.
    rewrite cat''.
    assert (X * (X *(derive cat * derive cat))=(X * derive cat) * (X * derive cat)).
    { ring. }
    rewrite H.
    assert ([0 + (X * cat') 0%nat] = 0).
    { rewrite left_identity. cbn.
      rewrite left_absorb.
      apply scalar0_is_nullStream. }
    assert (cat = X * derive cat).
    { rewrite <- fundamental_theorem at 1.
      unfold cat at 1.
      now rewrite H0, left_identity. }
    now rewrite <- H1.
  Qed.

  Lemma closed_cat:
    cat = (1 - conv_sqrt (- 4)) * conv_ainverse 2.
  Proof.
    destruct (abc T (null_division_free:=null_division_free) (-cat)).
    - rewrite cat_char at 3. ring.
    - assert (- - cat = - (-1 + conv_sqrt (-4)) * conv_ainverse 2).
      { rewrite H. ring. }
      rewrite double_negation in H0.
      rewrite H0. ring.
    - exfalso.
      specialize (H 0%nat).
      cbn in H. rewrite addition_pointwise in H.
      unfold conv_ainverse, conv_apreinverse, conv_inverse, conv_inverse_tail in H. destruct i2, ex_inv.
      cbn in H. rewrite addition_pointwise in H.
      cbn in H. rewrite left_absorb, right_identity, left_identity in H.
      unfold conv_sqrt, sqrt_tail in H.
      unfold negate, streamNegate in H.
      rewrite addition_pointwise in H. cbn in H.
      rewrite left_absorb, right_identity in H.
      assert ((-1 + - 1) * [x] = - (2 * [x])). { ring. }
      specialize (H0 0%nat). unfold negate, streamNegate in H0. cbn in H0.
      rewrite addition_pointwise in H0.
      cbn in H0.
      rewrite H0 in H.
      rewrite e in H.
      unfold cat in H. rewrite addition_pointwise in H.
      cbn in H. rewrite left_absorb, right_identity in H.
      apply apart01.
      assert (0 = 1 - 1). {rewrite negate_r. reflexivity. now destruct R, ring_group. }
      rewrite H1.
      rewrite <- H.
      unfold zero, streamZero, nullStream.
      assert (forall s:Stream T, 0 +s = -0 + s). { intros. ring. }
      specialize (H2 0). repeat rewrite right_identity in H2.
      specialize (H2 0%nat).
      unfold zero, streamZero, nullStream in H2.
      rewrite <- H2.
      now rewrite right_identity.
  Qed.
End CatalanStream.