# 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)).

Lemma leq_sum_sub_uniq :
(T: eqType) (r1 r2: seq T) F,
uniq r1
{subset r1 r2}
\sum_(i <- r1) F i \sum_(i <- r2) F i.

End SumArithmetic.

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 r P i E1 i E2 i)
\sum_(i <- r | P i) E1 i \sum_(i <- r | P i) E2 i.

End ExtraLemmasSumMax.