Library prosa.util.sum
Require Export prosa.util.notation.
Require Export prosa.util.nat.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
(* Lemmas about sum. *)
Section ExtraLemmas.
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 eq_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 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).
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.
(* 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).
(* 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 = Δ.
(* 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.
Require Export prosa.util.nat.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
(* Lemmas about sum. *)
Section ExtraLemmas.
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 eq_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 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).
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.
(* 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).
(* 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 = Δ.
(* 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.
If a function F gives same values at t1 + g and t2 + g for all g strictly
less than an integer d and for any t1 and t2, then summation of F over
the intervals [t1, t1 + d) and [t2, t2 + d) is equal.
Lemma big_sum_eq_in_eq_sized_intervals:
∀ t1 t2 d (F1 F2 : nat → nat),
(∀ g, g < d → F1 (t1 + g) = F2 (t2 + g)) →
\sum_(t1 ≤ t < t1 + d) F1 t = \sum_(t2 ≤ t < t2 + d) F2 t.
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.
∀ t1 t2 d (F1 F2 : nat → nat),
(∀ g, g < d → F1 (t1 + g) = F2 (t2 + g)) →
\sum_(t1 ≤ t < t1 + d) F1 t = \sum_(t2 ≤ t < t2 + d) F2 t.
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.
Summing natural numbers over a superset can only yields a greater sum.
Requiring the absence of duplicate in r1 is a simple way to
guarantee that the set inclusion r1 <= r2 implies the actually
required multiset inclusion.