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: T→nat) 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.

(* 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 x ⇒ F 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.