Library prosa.classic.util.sum

Require Export prosa.util.sum.
Require Export prosa.util.ssrlia.

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.

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.

  Lemma sum_le_summation_range :
    ∀ f t Δ,
      \sum_(t ≤ x < t + Δ) f x < Δ →
      ∃ x, t ≤ x < t + Δ ∧ f x = 0.

End ExtraLemmas.

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.