StreamCalculus.fib_basic

Require Import StreamCalculus.streamscommon.
Require Import StreamCalculus.stream_equality.
Require Import StreamCalculus.stream_addition.
Require Import StreamCalculus.special_streams.
Require Import StreamCalculus.conv_division.
Require Import StreamCalculus.conv_ring.
Require Import MathClasses.interfaces.abstract_algebra.

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

  Fixpoint fibonacci n: T:=
    match n with
    | 0 => 1
    | S n' => match n' with
              | 0 => 1
              | S n''=> fibonacci n' + fibonacci n''
              end
    end.

  Lemma fib_tail:
    derive (derive fibonacci) = fibonacci + (derive fibonacci).
  Proof.
    apply s_eq_pointwise. intros n.
    rewrite (addition_pointwise fibonacci).
    now rewrite commutativity.
  Qed.

  Lemma fib_closed:
    fibonacci = conv_inverse (-1-X).
  Proof.
    assert (fibonacci = 1 + X * X * fibonacci + X * fibonacci).
    {
      remember (1 + X * X * fibonacci + X * fibonacci).
      rewrite <- fundamental_theorem.
      rewrite <- (fundamental_theorem (derive fibonacci)).
      cbn.
      rewrite fib_tail.
      repeat rewrite distribute_l.
      rewrite (commutativity (X * [1])).
      rewrite <- associativity.
      rewrite <- distribute_l.
      rewrite <- (commutativity [1]).
      assert ([1] = [fibonacci 0]) by now cbn.
      rewrite H at 2.
      rewrite (fundamental_theorem fibonacci).
      rewrite Heqs.
      now repeat rewrite associativity.
    }

    assert (fibonacci * (1 - X - X * X) = 1).
    {
      repeat rewrite distribute_l.
      rewrite right_identity.
      rewrite <- associativity.
      assert (fibonacci * - (X * X) = -1 * (X * X * fibonacci)).
      { rewrite minus_eq_minusOne, commutativity.
        now rewrite <- associativity. exact R.
      }
      rewrite H0.
      assert (fibonacci * -X = -1 * (X * fibonacci)).
      { now rewrite commutativity, minus_eq_minusOne, associativity. }
      rewrite H1.
      rewrite <- distribute_l.
      rewrite <- minus_eq_minusOne.
      apply move_plus_right.
      rewrite (commutativity (X*fibonacci)).
      rewrite associativity.
      exact H. exact R.
    }
    apply divide_right.
    - exact R.
    - rewrite (distribute_l X).
      rewrite associativity.
      repeat rewrite (commutativity X).
      rewrite (move_minus X).
      now rewrite <- minus_eq_minusOne.
  Qed.
End FibBasic.