theory.series

Require Import
  Ring Factorial workaround_tactics
  abstract_algebra interfaces.additional_operations interfaces.orders
  interfaces.naturals interfaces.integers
  theory.nat_pow theory.int_pow theory.streams.

Section series.
Context `{SemiRing A} `{!SemiRingOrder Ale}.
Add Ring A : (rings.stdlib_semiring_theory A).
Add Ring nat : (rings.stdlib_semiring_theory nat).

Class DecreasingNonNegative (s : Stream A) : Prop :=
  decreasing_nonneg : ForAll (λ t, 0 hd (tl t) hd t) s.

Lemma dnn_alt (s : Stream A) :
  DecreasingNonNegative s ForAll (λ s, ForAll (λ t, 0 hd t hd s) s) s.

Definition dnn_Str_nth (s : Stream A) :
  DecreasingNonNegative s n, 0 Str_nth (S n) s Str_nth n s.

Global Instance dnn_tl `(dnn : DecreasingNonNegative s) : DecreasingNonNegative (tl s).

Global Instance dnn_Str_nth_tl `(dnn : DecreasingNonNegative s) : n, DecreasingNonNegative (Str_nth_tl n s).

Lemma dnn_hd_nonneg `(dnn : DecreasingNonNegative s) : 0 hd s.

Lemma dnn_Str_nth_nonneg `(dnn : DecreasingNonNegative s) n : 0 Str_nth n s.

Class IncreasingNonNegative (s : Stream A) : Prop :=
  increasing_nonneg : ForAll (λ s, 0 hd s hd (tl s)) s.

Lemma inn_Str_nth (s : Stream A) :
  IncreasingNonNegative s n, 0 Str_nth n s Str_nth (S n) s.

Global Instance inn_tl `(inn : IncreasingNonNegative s) : IncreasingNonNegative (tl s).

Global Instance inn_Str_nth_tl `(inn : IncreasingNonNegative s) : n, IncreasingNonNegative (Str_nth_tl n s).

Section every_other.
  CoFixpoint everyOther (s : Stream A) : Stream A := Cons (hd s) (everyOther (tl (tl s))).

  Lemma Str_nth_tl_everyOther (n : nat) (s : Stream A) : Str_nth_tl n (everyOther s) everyOther (Str_nth_tl (2 * n) s).

  Lemma Str_nth_everyOther (n : nat) (s : Stream A) : Str_nth n (everyOther s) = Str_nth (2 * n) s.

  Global Instance everyOther_dnn `(dnn : !DecreasingNonNegative s) : DecreasingNonNegative (everyOther s).

  Global Instance everyOther_inc `(inn : !IncreasingNonNegative s) : IncreasingNonNegative (everyOther s).
End every_other.

Section mult.
  Definition mult_Streams := zipWith (.*.).

  Global Instance mult_Streams_dnn `(dnn1 : !DecreasingNonNegative s1) `(dnn2 : !DecreasingNonNegative s2) :
    DecreasingNonNegative (mult_Streams s1 s2).

  Global Instance mult_Streams_inc `(inn1 : !IncreasingNonNegative s1) `(inn2 : !IncreasingNonNegative s2) :
    IncreasingNonNegative (mult_Streams s1 s2).

  Global Instance: Proper ((=) ==> (=) ==> (=)) mult_Streams.
End mult.

Section powers.
  Context (a : A).

  CoFixpoint powers_help (c : A) : Stream A := Cons c (powers_help (c * a)).

  Definition powers : Stream A := powers_help 1.

  Section with_nat_pow.
  Context `{Naturals N} `{!NatPowSpec A N pw} (f : nat N) `{!SemiRing_Morphism f}.

  Lemma Str_nth_powers_help (n : nat) (c : A) : Str_nth n (powers_help c) = c * a ^ (f n).

  Lemma Str_nth_powers (n : nat) : Str_nth n powers = a ^ (f n).
  End with_nat_pow.

  Section with_int_pow.
  Context `{!GroupInv A} `{!DecMultInv A} `{!DecField A} `{ x y : A, Decision (x = y)}
     `{Integers Z} `{!IntPowSpec A Z pw} (f : nat Z) `{!SemiRing_Morphism f}.

  Lemma Str_nth_powers_help_int_pow (n : nat) (c : A) : Str_nth n (powers_help c) = c * a ^ (f n).

  Lemma Str_nth_powers_int_pow (n : nat) : Str_nth n powers = a ^ (f n).
  End with_int_pow.
End powers.

Global Instance powers_help_proper: Proper ((=) ==> (=) ==> (=)) powers_help.

Global Instance powers_proper: Proper ((=) ==> (=)) powers.

Section positives.
  CoFixpoint positives_help (x : A) : Stream A := Cons x (positives_help (1 + x)).

  Lemma Str_nth_positives_help (n : nat) (x : A) :
    Str_nth n (positives_help x) = x + naturals_to_semiring nat A n.

  Definition positives : Stream A := positives_help 1.

  Lemma Str_nth_positives (n : nat) :
    Str_nth n positives = 1 + naturals_to_semiring nat A n.
End positives.

Section factorials.
  CoFixpoint factorials_help (n c : A) : Stream A := Cons c (factorials_help (1 + n) (n * c)).

  Fixpoint fac_help (n : nat) (m c : A) : A :=
    match n with
    | O => c
    | S n' => (m + naturals_to_semiring nat A n') * fac_help n' m c
    end.

  Lemma Str_nth_factorials_help (n : nat) (m c : A) :
    Str_nth n (factorials_help m c) = fac_help n m c.

  Definition factorials := factorials_help 1 1.

  Lemma Str_nth_factorials (n : nat) :
    Str_nth n factorials = naturals_to_semiring nat A (fact n).
End factorials.
End series.

Section preservation.
  Context `{SemiRing A} `{!SemiRingOrder (A:=A) Ale}.
  Context `{SemiRing B} `{!SemiRingOrder (A:=B) Ble}.
  Context `{!SemiRing_Morphism (f : A B)}.

  Lemma preserves_powers_help (a c : A) (n : nat) :
    f (Str_nth n (powers_help a c)) = Str_nth n (powers_help (f a) (f c)).

  Lemma preserves_powers (a : A) (n : nat) :
    f (Str_nth n (powers a)) = Str_nth n (powers (f a)).

  Lemma preserves_positives (n : nat) :
    f (Str_nth n positives) = Str_nth n positives.

  Lemma preserves_factorials (n : nat) :
    f (Str_nth n factorials) = Str_nth n factorials.
End preservation.