Library prosa.classic.util.sum

Require Export prosa.util.sum.
Require Export mathcomp.zify.zify.

Require Import prosa.classic.util.tactics.
Require Import prosa.classic.util.notation.
Require Import prosa.classic.util.sorting.
Require Import prosa.classic.util.nat.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.

(* 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_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 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.

  (* We show that the fact that the sum is smaller than the range 
     of the summation implies the existence of a zero element. *)
  Lemma sum_le_summation_range :
    ∀ f t Δ,
      \sum_(t ≤ x < t + Δ) f x < Δ →
      ∃ x, t ≤ x < t + Δ ∧ f x = 0.

End ExtraLemmas.

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

  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.