# Library prosa.util.sum

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.

Require Export prosa.util.notation.

Require Export prosa.util.nat.

(* TODO: PR MathComp *)

Lemma leq_sum_subseq (I : eqType) (r r' : seq I) (P : pred I) (F : I → nat) :

subseq r r' → \sum_(i <- r | P i) F i ≤ \sum_(i <- r' | P i) F i.

Section SumsOverSequences.

Require Export prosa.util.notation.

Require Export prosa.util.nat.

(* TODO: PR MathComp *)

Lemma leq_sum_subseq (I : eqType) (r r' : seq I) (P : pred I) (F : I → nat) :

subseq r r' → \sum_(i <- r | P i) F i ≤ \sum_(i <- r' | P i) F i.

Section SumsOverSequences.

Consider any type I with a decidable equality ...

... and assume we are given a sequence ...

... and a predicate P.

First, we will show some properties of the sum performed over a single function
yielding natural numbers.

Consider any function that yields natural numbers...

We start showing that having every member of r equal to zero is equivalent to
having the sum of all the elements of r equal to zero, and vice-versa.

(* TODO: PR MathComp

this should probably be named sum_nat_eq0,

but there is already a sum_nat_eq0 that is less generic? *)

Lemma sum_nat_eq0_nat :

(\sum_(i <- r | P i) F i == 0) = all (fun x ⇒ F x == 0) [seq x <- r | P x].

this should probably be named sum_nat_eq0,

but there is already a sum_nat_eq0 that is less generic? *)

Lemma sum_nat_eq0_nat :

(\sum_(i <- r | P i) F i == 0) = all (fun x ⇒ F x == 0) [seq x <- r | P x].

In the same way, if at least one element of r is not zero, then the sum of all
elements of r must be strictly positive, and vice-versa.

(* TODO: PR MathComp *)

Lemma sum_nat_gt0 :

(0 < \sum_(i <- r | P i) F i) = has (fun x ⇒ 0 < F x) [seq x <- r | P x].

Lemma sum_nat_gt0 :

(0 < \sum_(i <- r | P i) F i) = has (fun x ⇒ 0 < F x) [seq x <- r | P x].

Next, we show that if a number a is not contained in r, then filtering or not
filtering a when summing leads to the same result.

Lemma sum_notin_rem_eqn a :

a \notin r →

\sum_(x <- r | P x && (x != a)) F x = \sum_(x <- r | P x) F x.

a \notin r →

\sum_(x <- r | P x && (x != a)) F x = \sum_(x <- r | P x) F x.

We prove that if any element of r is bounded by constant c,
then the sum of the whole set is bounded by c × size r.

Lemma sum_majorant_constant c :

(∀ a, a \in r → P a → F a ≤ c) →

\sum_(j <- r | P j) F j ≤ c × (size [seq j <- r | P j]).

(∀ a, a \in r → P a → F a ≤ c) →

\sum_(j <- r | P j) F j ≤ c × (size [seq j <- r | P j]).

Next, we show that the sum of the elements in r respecting P can
be obtained by removing from the total sum over r the sum of the elements
in r not respecting P.

Summing natural numbers over a superset can only yields a greater sum.
Requiring the absence of duplicate in r is a simple way to
guarantee that the set inclusion r ≤ rs implies the actually
required multiset inclusion.

(* TODO: PR MathComp

- add a condition P i *)

Lemma leq_sum_sub_uniq (rs : seq I) :

uniq r → {subset r ≤ rs} →

\sum_(i <- r) F i ≤ \sum_(i <- rs) F i.

End SumOfOneFunction.

- add a condition P i *)

Lemma leq_sum_sub_uniq (rs : seq I) :

uniq r → {subset r ≤ rs} →

\sum_(i <- r) F i ≤ \sum_(i <- rs) F i.

End SumOfOneFunction.

In this section, we show some properties of the sum performed over two different functions.

Consider three functions that yield natural numbers.

Assume that E2 dominates E1 in all the points contained in the set r and respecting
the predicate P. We prove that, if we sum both function over those points, then the sum
of E2 will dominate the sum of E1.

(* TODO: PR MathComp *)

Lemma leq_sum_seq :

(∀ 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 leq_sum_seq :

(∀ i, i \in r → P i → E1 i ≤ E2 i) →

\sum_(i <- r | P i) E1 i ≤ \sum_(i <- r | P i) E2 i.

In the same way, if E1 equals E2 in all the points considered above, then also the two
sums will be identical.

(* TODO: PR MathComp

- generalize as eq_big_seq_cond (nothing specific to addn here)

- replace == with = ? *)

Lemma eq_sum_seq:

(∀ i, i \in r → P i → E1 i == E2 i) →

\sum_(i <- r | P i) E1 i == \sum_(i <- r | P i) E2 i.

- generalize as eq_big_seq_cond (nothing specific to addn here)

- replace == with = ? *)

Lemma eq_sum_seq:

(∀ i, i \in r → P i → E1 i == E2 i) →

\sum_(i <- r | P i) E1 i == \sum_(i <- r | P i) E2 i.

Assume that P1 implies P2 in all the points contained in
the set r. We prove that, if we sum both functions over those
points, then the sum of E conditioned by P2 will dominate
the sum of E conditioned by P1.

(* TODO: PR MathComp

- maybe leq_sum_seq above should be leq_sum_seqr and this one leq_sum_seql *)

Lemma leq_sum_seq_pred:

(∀ i, i \in r → P1 i → P2 i) →

\sum_(i <- r | P1 i) E i ≤ \sum_(i <- r | P2 i) E i.

End SumOfTwoFunctions.

End SumsOverSequences.

- maybe leq_sum_seq above should be leq_sum_seqr and this one leq_sum_seql *)

Lemma leq_sum_seq_pred:

(∀ i, i \in r → P1 i → P2 i) →

\sum_(i <- r | P1 i) E i ≤ \sum_(i <- r | P2 i) E i.

End SumOfTwoFunctions.

End SumsOverSequences.

We continue establishing properties of sums over sequences, but start a new
section here because some of the below proofs depend lemmas in the preceding
section in their full generality.

Consider any type I with a decidable equality ...

... and assume we are given a sequence ...

... and a predicate P.

Consider two functions that yield natural numbers.

First, as an auxiliary lemma, we observe that, if E1 j is less than E2
j for some element j involved in a summation (filtered by P), then
the corresponding totals are not equal.

Lemma ltn_sum_leq_seq j :

j \in r →

P j →

E1 j < E2 j →

(∀ i, i \in r → P i → E1 i ≤ E2 i) →

\sum_(x <- r | P x) E1 x < \sum_(x <- r | P x) E2 x.

j \in r →

P j →

E1 j < E2 j →

(∀ i, i \in r → P i → E1 i ≤ E2 i) →

\sum_(x <- r | P x) E1 x < \sum_(x <- r | P x) E2 x.

Next, we prove that if for any element i of a set r the following two
statements hold (1) E1 i is less than or equal to E2 i and (2) the sum
E1 x_1, ..., E1 x_n is equal to the sum of E2 x_1, ..., E2 x_n, then
E1 x is equal to E2 x for any element x of xs.

(* TODO: PR MathComp *)

Lemma eq_sum_leq_seq :

(∀ i, i \in r → P i → E1 i ≤ E2 i) →

\sum_(x <- r | P x) E1 x == \sum_(x <- r | P x) E2 x

= all (fun x ⇒ E1 x == E2 x) [seq x <- r | P x].

End SumsOverSequences.

Lemma eq_sum_leq_seq :

(∀ i, i \in r → P i → E1 i ≤ E2 i) →

\sum_(x <- r | P x) E1 x == \sum_(x <- r | P x) E2 x

= all (fun x ⇒ E1 x == E2 x) [seq x <- r | P x].

End SumsOverSequences.

In this section, we prove a variety of properties of sums performed over ranges.

First, we prove that the sum of Δ ones is equal to Δ.

Next, we show that a sum of natural numbers equals zero if and only
if all terms are zero.

Moreover, the fact that the sum is smaller than the range of the summation
implies the existence of a zero element.

Next, we prove that the summing over the difference of two functions is
the same as summing over the two functions separately, and then taking the
difference of the two sums. Since we are using natural numbers, we have to
require that one function dominates the other in the summing range.

Lemma sumnB_nat m n F G :

(∀ i, m ≤ i < n → F i ≥ G i) →

\sum_(m ≤ i < n) (F i - G i) =

(\sum_(m ≤ i < n) (F i)) - (\sum_(m ≤ i < n) (G i)).

End SumsOverRanges.

(∀ i, m ≤ i < n → F i ≥ G i) →

\sum_(m ≤ i < n) (F i - G i) =

(\sum_(m ≤ i < n) (F i)) - (\sum_(m ≤ i < n) (G i)).

End SumsOverRanges.

In this section, we show how it is possible to equate the result of two sums performed
on two different functions and on different intervals, provided that the two functions
match point-wise.

Consider two equally-sized intervals

`[t1, t1+d)`

and `[t2, t2+d)`

...
Assume that the two functions match point-wise with each other, with the points taken
in their respective interval.

Lemma big_sum_eq_in_eq_sized_intervals:

\sum_(t1 ≤ t < t1 + d) F1 t = \sum_(t2 ≤ t < t2 + d) F2 t.

End SumOfTwoIntervals.

\sum_(t1 ≤ t < t1 + d) F1 t = \sum_(t2 ≤ t < t2 + d) F2 t.

End SumOfTwoIntervals.

In this section, we relate the sum of items with the sum over partitions of those items.

x_to_y is the mapping from an item to the partition it is contained in.

We prove that summation of f x over all x is less than or equal to the summation of
sum_of_partition over all partitions.

In this section, we prove a stronger result about the equality between
the sum over all items and the sum over all partitions of those items.

In order to prove the stronger result of equality, we additionally
assume that the sequences xs and ys are sets, i.e., that each
element is contained at most once.

We prove that summation of f x over all x is equal to the summation of
sum_of_partition over all partitions.