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.
Proof.
intros LE.
rewrite big_seq_cond [\sum_(_ <- _| P _)_]big_seq_cond.
by apply leq_sum; move ⇒ j /andP [IN H]; apply LE.
Qed.
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.
Proof.
intros; rewrite eqn_leq; apply/andP; split.
- apply leq_sum_seq; intros.
by move: (H i H0 H1) ⇒ /eqP EQ; rewrite EQ.
- apply leq_sum_seq; intros.
by move: (H i H0 H1) ⇒ /eqP EQ; rewrite EQ.
Qed.
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).
Proof.
destruct (all (fun x ⇒ F x == 0) r) eqn:ZERO.
- move: ZERO ⇒ /allP ZERO; rewrite -leqn0.
rewrite big_seq_cond (eq_bigr (fun x ⇒ 0));
first by rewrite big_const_seq iter_addn mul0n addn0 leqnn.
intro i; rewrite andbT; intros IN.
specialize (ZERO i); rewrite IN in ZERO.
by move: ZERO ⇒ /implyP ZERO; apply/eqP; apply ZERO.
- apply negbT in ZERO; rewrite -has_predC in ZERO.
move: ZERO ⇒ /hasP ZERO; destruct ZERO as [x IN NEQ]; simpl in NEQ.
rewrite (big_rem x) /=; last by done.
symmetry; apply negbTE; rewrite neq_ltn; apply/orP; right.
apply leq_trans with (n := F x); last by apply leq_addr.
by rewrite lt0n.
Qed.
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).
Proof.
intros; apply: (iffP idP); intros.
{
induction r; first by rewrite big_nil in H.
destruct (F a > 0) eqn:POS.
∃ a; split; [by rewrite in_cons; apply/orP; left | by done].
apply negbT in POS; rewrite -leqNgt leqn0 in POS; move: POS ⇒ /eqP POS.
rewrite big_cons POS add0n in H. clear POS.
feed IHr; first by done. move: IHr ⇒ [i [IN POS]].
∃ i; split; [by rewrite in_cons; apply/orP;right | by done].
}
{
move: H ⇒ [i [IN POS]].
rewrite (big_rem i) //=.
apply leq_trans with (F i); [by done | by rewrite leq_addr].
}
Qed.
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.
Proof.
intros ? ? ? ? ? NOTIN.
induction xs; first by rewrite !big_nil.
rewrite !big_cons.
rewrite IHxs; clear IHxs; last first.
{ apply/memPn; intros y IN.
move: NOTIN ⇒ /memPn NOTIN.
by apply NOTIN; rewrite in_cons; apply/orP; right.
}
move: NOTIN ⇒ /memPn NOTIN.
move: (NOTIN a0) ⇒ NEQ.
feed NEQ; first by (rewrite in_cons; apply/orP; left).
by rewrite NEQ Bool.andb_true_r.
Qed.
(* Trivial identity: any sum of zeros is zero. *)
Lemma sum0 m n:
\sum_(m ≤ i < n) 0 = 0.
Proof.
by rewrite big_const_nat iter_addn mul0n addn0 //.
Qed.
(* 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).
Proof.
split.
- rewrite /index_iota ⇒ /eqP.
rewrite -sum_nat_eq0_nat ⇒ /allP ZERO i.
rewrite -mem_index_iota /index_iota ⇒ IN.
by apply/eqP; apply ZERO.
- move⇒ ZERO.
have ->: \sum_(m ≤ i < n) F i = \sum_(m ≤ i < n) 0
by apply eq_big_nat ⇒ //.
by apply sum0.
Qed.
(* 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]).
Proof.
clear; intros.
induction r; first by rewrite big_nil.
feed IHr.
{ intros; apply H.
- by rewrite in_cons; apply/orP; right.
- by done. }
rewrite big_cons.
destruct (P a) eqn:EQ.
{ rewrite -cat1s filter_cat size_cat.
rewrite mulnDr.
apply leq_add; last by done.
rewrite size_filter.
simpl; rewrite addn0.
rewrite EQ muln1.
apply H; last by done.
by rewrite in_cons; apply/orP; left.
}
{ apply leq_trans with (const × size [seq j <- r | P j]); first by done.
rewrite leq_mul2l; apply/orP; right.
rewrite -cat1s filter_cat size_cat.
by rewrite leq_addl.
}
Qed.
(* 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).
Proof.
intros T xs F1 F2 P H1 H2 x IN PX.
induction xs; first by done.
have Fact: \sum_(j <- xs | P j) F1 j ≤ \sum_(j <- xs | P j) F2 j.
{ rewrite [in X in X ≤ _]big_seq_cond [in X in _ ≤ X]big_seq_cond leq_sum //.
move ⇒ y /andP [INy PY].
apply: H1; last by done.
by rewrite in_cons; apply/orP; right. }
feed IHxs.
{ intros x' IN' PX'.
apply H1; last by done.
by rewrite in_cons; apply/orP; right. }
rewrite big_cons [RHS]big_cons in H2.
have EqLeq: ∀ a b c d, a + b = c + d → a ≤ c → b ≥ d.
{ clear; intros; ssromega. }
move: IN; rewrite in_cons; move ⇒ /orP [/eqP EQ | IN].
{ subst a.
rewrite PX in H2.
specialize (H1 x).
feed_n 2 H1; [ by rewrite in_cons; apply/orP; left | by done | ].
move: (EqLeq
(F1 x) (\sum_(j <- xs | P j) F1 j)
(F2 x) (\sum_(j <- xs | P j) F2 j) H2 H1) ⇒ Q.
have EQ: \sum_(j <- xs | P j) F1 j = \sum_(j <- xs | P j) F2 j.
{ by apply/eqP; rewrite eqn_leq; apply/andP; split. }
by move: H2 ⇒ /eqP; rewrite EQ eqn_add2r; move ⇒ /eqP EQ'.
}
{ destruct (P a) eqn:PA; last by apply IHxs.
apply: IHxs; last by done.
specialize (H1 a).
feed_n 2 (H1); [ by rewrite in_cons; apply/orP; left | by done | ].
move: (EqLeq
(F1 a) (\sum_(j <- xs | P j) F1 j)
(F2 a) (\sum_(j <- xs | P j) F2 j) H2 H1) ⇒ Q.
by apply/eqP; rewrite eqn_leq; apply/andP; split.
}
Qed.
(* We prove that the sum of Δ ones is equal to Δ. *)
Lemma sum_of_ones:
∀ t Δ,
\sum_(t ≤ x < t + Δ) 1 = Δ.
Proof.
intros.
rewrite big_const_nat iter_addn_0 mul1n.
rewrite addnC -addnBA; last by done.
by rewrite subnn addn0.
Qed.
(* 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.
Proof.
induction Δ; intros; first by rewrite ltn0 in H.
destruct (f (t + Δ)) eqn: EQ.
{ ∃ (t + Δ); split; last by done.
by apply/andP; split; [rewrite leq_addr | rewrite addnS ltnS].
}
{ move: H; rewrite addnS big_nat_recr //= ?leq_addr // EQ addnS ltnS; move ⇒ H.
feed IHΔ.
{ by apply leq_ltn_trans with (\sum_(t ≤ i < t + Δ) f i + n); first rewrite leq_addr. }
move: IHΔ ⇒ [z [/andP [LE GE] ZERO]].
∃ z; split; last by done.
apply/andP; split; first by done.
by rewrite ltnS ltnW.
}
Qed.
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.
Proof.
intros.
induction rs; first by rewrite !big_nil subn0.
rewrite !big_cons subh2.
- apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHrs.
by intros; apply H; rewrite in_cons; apply/orP; right.
- by apply H; rewrite in_cons; apply/orP; left.
- rewrite big_seq_cond [in X in _ ≤ X]big_seq_cond.
rewrite leq_sum //; move ⇒ i /andP [IN _].
by apply H; rewrite in_cons; apply/orP; right.
Qed.
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)).
Proof.
intros n F G ALL.
rewrite sum_seq_diff; first by done.
move ⇒ i; rewrite mem_index_iota; move ⇒ /andP [_ LT].
by apply ALL.
Qed.
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.
Proof.
clear; intros.
induction rs; first by rewrite !big_nil subn0.
rewrite !big_cons !IHrs; clear IHrs.
case (P a); simpl; last by rewrite subnDl.
rewrite addnBA; first by done.
rewrite big_mkcond leq_sum //.
intros t _.
by case (P t).
Qed.
End SumArithmetic.
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.
Proof.
intros LE.
rewrite big_seq_cond [\sum_(_ <- _| P _)_]big_seq_cond.
by apply leq_sum; move ⇒ j /andP [IN H]; apply LE.
Qed.
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.
Proof.
intros; rewrite eqn_leq; apply/andP; split.
- apply leq_sum_seq; intros.
by move: (H i H0 H1) ⇒ /eqP EQ; rewrite EQ.
- apply leq_sum_seq; intros.
by move: (H i H0 H1) ⇒ /eqP EQ; rewrite EQ.
Qed.
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).
Proof.
destruct (all (fun x ⇒ F x == 0) r) eqn:ZERO.
- move: ZERO ⇒ /allP ZERO; rewrite -leqn0.
rewrite big_seq_cond (eq_bigr (fun x ⇒ 0));
first by rewrite big_const_seq iter_addn mul0n addn0 leqnn.
intro i; rewrite andbT; intros IN.
specialize (ZERO i); rewrite IN in ZERO.
by move: ZERO ⇒ /implyP ZERO; apply/eqP; apply ZERO.
- apply negbT in ZERO; rewrite -has_predC in ZERO.
move: ZERO ⇒ /hasP ZERO; destruct ZERO as [x IN NEQ]; simpl in NEQ.
rewrite (big_rem x) /=; last by done.
symmetry; apply negbTE; rewrite neq_ltn; apply/orP; right.
apply leq_trans with (n := F x); last by apply leq_addr.
by rewrite lt0n.
Qed.
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).
Proof.
intros; apply: (iffP idP); intros.
{
induction r; first by rewrite big_nil in H.
destruct (F a > 0) eqn:POS.
∃ a; split; [by rewrite in_cons; apply/orP; left | by done].
apply negbT in POS; rewrite -leqNgt leqn0 in POS; move: POS ⇒ /eqP POS.
rewrite big_cons POS add0n in H. clear POS.
feed IHr; first by done. move: IHr ⇒ [i [IN POS]].
∃ i; split; [by rewrite in_cons; apply/orP;right | by done].
}
{
move: H ⇒ [i [IN POS]].
rewrite (big_rem i) //=.
apply leq_trans with (F i); [by done | by rewrite leq_addr].
}
Qed.
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.
Proof.
intros ? ? ? ? ? NOTIN.
induction xs; first by rewrite !big_nil.
rewrite !big_cons.
rewrite IHxs; clear IHxs; last first.
{ apply/memPn; intros y IN.
move: NOTIN ⇒ /memPn NOTIN.
by apply NOTIN; rewrite in_cons; apply/orP; right.
}
move: NOTIN ⇒ /memPn NOTIN.
move: (NOTIN a0) ⇒ NEQ.
feed NEQ; first by (rewrite in_cons; apply/orP; left).
by rewrite NEQ Bool.andb_true_r.
Qed.
(* Trivial identity: any sum of zeros is zero. *)
Lemma sum0 m n:
\sum_(m ≤ i < n) 0 = 0.
Proof.
by rewrite big_const_nat iter_addn mul0n addn0 //.
Qed.
(* 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).
Proof.
split.
- rewrite /index_iota ⇒ /eqP.
rewrite -sum_nat_eq0_nat ⇒ /allP ZERO i.
rewrite -mem_index_iota /index_iota ⇒ IN.
by apply/eqP; apply ZERO.
- move⇒ ZERO.
have ->: \sum_(m ≤ i < n) F i = \sum_(m ≤ i < n) 0
by apply eq_big_nat ⇒ //.
by apply sum0.
Qed.
(* 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]).
Proof.
clear; intros.
induction r; first by rewrite big_nil.
feed IHr.
{ intros; apply H.
- by rewrite in_cons; apply/orP; right.
- by done. }
rewrite big_cons.
destruct (P a) eqn:EQ.
{ rewrite -cat1s filter_cat size_cat.
rewrite mulnDr.
apply leq_add; last by done.
rewrite size_filter.
simpl; rewrite addn0.
rewrite EQ muln1.
apply H; last by done.
by rewrite in_cons; apply/orP; left.
}
{ apply leq_trans with (const × size [seq j <- r | P j]); first by done.
rewrite leq_mul2l; apply/orP; right.
rewrite -cat1s filter_cat size_cat.
by rewrite leq_addl.
}
Qed.
(* 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).
Proof.
intros T xs F1 F2 P H1 H2 x IN PX.
induction xs; first by done.
have Fact: \sum_(j <- xs | P j) F1 j ≤ \sum_(j <- xs | P j) F2 j.
{ rewrite [in X in X ≤ _]big_seq_cond [in X in _ ≤ X]big_seq_cond leq_sum //.
move ⇒ y /andP [INy PY].
apply: H1; last by done.
by rewrite in_cons; apply/orP; right. }
feed IHxs.
{ intros x' IN' PX'.
apply H1; last by done.
by rewrite in_cons; apply/orP; right. }
rewrite big_cons [RHS]big_cons in H2.
have EqLeq: ∀ a b c d, a + b = c + d → a ≤ c → b ≥ d.
{ clear; intros; ssromega. }
move: IN; rewrite in_cons; move ⇒ /orP [/eqP EQ | IN].
{ subst a.
rewrite PX in H2.
specialize (H1 x).
feed_n 2 H1; [ by rewrite in_cons; apply/orP; left | by done | ].
move: (EqLeq
(F1 x) (\sum_(j <- xs | P j) F1 j)
(F2 x) (\sum_(j <- xs | P j) F2 j) H2 H1) ⇒ Q.
have EQ: \sum_(j <- xs | P j) F1 j = \sum_(j <- xs | P j) F2 j.
{ by apply/eqP; rewrite eqn_leq; apply/andP; split. }
by move: H2 ⇒ /eqP; rewrite EQ eqn_add2r; move ⇒ /eqP EQ'.
}
{ destruct (P a) eqn:PA; last by apply IHxs.
apply: IHxs; last by done.
specialize (H1 a).
feed_n 2 (H1); [ by rewrite in_cons; apply/orP; left | by done | ].
move: (EqLeq
(F1 a) (\sum_(j <- xs | P j) F1 j)
(F2 a) (\sum_(j <- xs | P j) F2 j) H2 H1) ⇒ Q.
by apply/eqP; rewrite eqn_leq; apply/andP; split.
}
Qed.
(* We prove that the sum of Δ ones is equal to Δ. *)
Lemma sum_of_ones:
∀ t Δ,
\sum_(t ≤ x < t + Δ) 1 = Δ.
Proof.
intros.
rewrite big_const_nat iter_addn_0 mul1n.
rewrite addnC -addnBA; last by done.
by rewrite subnn addn0.
Qed.
(* 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.
Proof.
induction Δ; intros; first by rewrite ltn0 in H.
destruct (f (t + Δ)) eqn: EQ.
{ ∃ (t + Δ); split; last by done.
by apply/andP; split; [rewrite leq_addr | rewrite addnS ltnS].
}
{ move: H; rewrite addnS big_nat_recr //= ?leq_addr // EQ addnS ltnS; move ⇒ H.
feed IHΔ.
{ by apply leq_ltn_trans with (\sum_(t ≤ i < t + Δ) f i + n); first rewrite leq_addr. }
move: IHΔ ⇒ [z [/andP [LE GE] ZERO]].
∃ z; split; last by done.
apply/andP; split; first by done.
by rewrite ltnS ltnW.
}
Qed.
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.
Proof.
intros.
induction rs; first by rewrite !big_nil subn0.
rewrite !big_cons subh2.
- apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHrs.
by intros; apply H; rewrite in_cons; apply/orP; right.
- by apply H; rewrite in_cons; apply/orP; left.
- rewrite big_seq_cond [in X in _ ≤ X]big_seq_cond.
rewrite leq_sum //; move ⇒ i /andP [IN _].
by apply H; rewrite in_cons; apply/orP; right.
Qed.
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)).
Proof.
intros n F G ALL.
rewrite sum_seq_diff; first by done.
move ⇒ i; rewrite mem_index_iota; move ⇒ /andP [_ LT].
by apply ALL.
Qed.
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.
Proof.
clear; intros.
induction rs; first by rewrite !big_nil subn0.
rewrite !big_cons !IHrs; clear IHrs.
case (P a); simpl; last by rewrite subnDl.
rewrite addnBA; first by done.
rewrite big_mkcond leq_sum //.
intros t _.
by case (P t).
Qed.
End SumArithmetic.