Library rt.util.sum

Require Import rt.util.tactics rt.util.notation rt.util.sorting rt.util.nat.

(* Lemmas about arithmetic with sums. *)
Section SumArithmetic.

  (* Inequality with sums is monotonic with their functions. *)
  Lemma sum_diff_monotonic :
     n G F,
      ( i : nat, i < n G i F i)
      (\sum_(0 i < n) (G i)) (\sum_(0 i < n) (F i)).

  Lemma sum_diff :
     n F G,
      ( i (LT: i < n), F i G i)
      \sum_(0 i < n) (F i - G i) =
        (\sum_(0 i < n) (F i)) - (\sum_(0 i < n) (G i)).

  Lemma telescoping_sum :
     (T: Type) (F: Tnat) r (x0: T),
    ( i, i < (size r).-1 F (nth x0 r i) F (nth x0 r i.+1))
      F (nth x0 r (size r).-1) - F (nth x0 r 0) =
        \sum_(0 i < (size r).-1) (F (nth x0 r (i.+1)) - F (nth x0 r i)).

End SumArithmetic.

(* Additional lemmas about sum and max big operators. *)
Section ExtraLemmasSumMax.

  Lemma leq_big_max I r (P : pred I) (E1 E2 : I nat) :
    ( i, P i E1 i E2 i)
      \max_(i <- r | P i) E1 i \max_(i <- r | P i) E2 i.

  Lemma sum_nat_eq0_nat (T : eqType) (F : T nat) (r: seq T) :
    all (fun xF x == 0) r = (\sum_(i <- r) F i == 0).

  Lemma extend_sum :
     t1 t2 t1' t2' F,
      t1' t1
      t2 t2'
      \sum_(t1 t < t2) F t \sum_(t1' t < t2') F t.

  Lemma leq_sum_nat m n (P : pred nat) (E1 E2 : nat nat) :
    ( i, m i < n P i E1 i E2 i)
    \sum_(m i < n | P i) E1 i \sum_(m i < n | P i) E2 i.

  Lemma leq_sum_seq (I: eqType) (r: seq I) (P : pred I) (E1 E2 : I nat) :
    ( i, i \in r P i E1 i E2 i)
    \sum_(i <- r | P i) E1 i \sum_(i <- r | P i) E2 i.

End ExtraLemmasSumMax.