Library rt.util.sum

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

(* Lemmas about sum. *)
Section ExtraLemmas.

  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.

  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 leq_sum1_smaller_range m n (P Q: pred nat) a b:
    (∀ i, m ≤ i < n ∧ P i → a ≤ i < b ∧ Q i) →
    \sum_(m ≤ i < n | P i) 1 ≤ \sum_(a ≤ i < b | Q i) 1.

  Lemma sum_seq_gt0P:
    ∀ (T:eqType) (r: seq T) (F: T → nat),
      reflect (∃ i, i \in r ∧ 0 < F i) (0 < \sum_(i <- r) F i).

  (* Trivial identity: any sum of zeros is zero. *)
  Lemma sum0 m n:
    \sum_(m ≤ i < n) 0 = 0.

  (* A sum of natural numbers equals zero iff all terms are zero. *)
  Lemma big_nat_eq0 m n F:
    \sum_(m ≤ i < n) F i = 0 ↔ (∀ i, m ≤ i < n → F i = 0).

  Lemma leq_pred_sum:
    ∀ (T:eqType) (r: seq T) (P1 P2: pred T) F,
      (∀ i, P1 i → P2 i) →
      \sum_(i <- r | P1 i) F i ≤
      \sum_(i <- r | P2 i) F i.

  Lemma sum_notin_rem_eqn:
    ∀ (T:eqType) (a: T) xs P F,
      a \notin xs →
      \sum_(x <- xs | P x && (x != a)) F x = \sum_(x <- xs | P x) F x.

  (* We prove that if any element of a set r is bounded by constant const, 
     then the sum of the whole set is bounded by [const * size r]. *)
  Lemma sum_majorant_constant:
    ∀ (T: eqType) (r: seq T) (P: pred T) F const,
      (∀ a, a \in r → P a → F a ≤ const) →
      \sum_(j <- r | P j) F j ≤ const × (size [seq j <- r | P j]).

  (* We prove that if for any element x of a set xs the following two statements hold 
     (1) [F1 x] is less than or equal to [F2 x] and (2) the sum [F1 x_1, ..., F1 x_n] 
     is equal to the sum of [F2 x_1, ..., F2 x_n], then [F1 x] is equal to [F2 x] for 
     any element x of xs. *)
  Lemma sum_majorant_eqn:
    ∀ (T: eqType) xs F1 F2 (P: pred T),
      (∀ x, x \in xs → P x → F1 x ≤ F2 x) →
      \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x →
      (∀ x, x \in xs → P x → F1 x = F2 x).

  (* We prove that the sum of Δ ones is equal to Δ. *)
  Lemma sum_of_ones:
    ∀ t Δ,
      \sum_(t ≤ x < t + Δ) 1 = Δ.

End ExtraLemmas.

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

  Lemma sum_seq_diff:
    ∀ (T:eqType) (rs: seq T) (F G : T → nat),
      (∀ i : T, i \in rs → G i ≤ F i) →
      \sum_(i <- rs) (F i - G i) = \sum_(i <- rs) F i - \sum_(i <- rs) G 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 sum_pred_diff:
    ∀ (T: eqType) (rs: seq T) (P: T → bool) (F: T → nat),
      \sum_(r <- rs | P r) F r =
      \sum_(r <- rs) F r - \sum_(r <- rs | ~~ P r) F r.

  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.