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