diff --git a/util/all.v b/util/all.v
index 25acc36ba7e9401eb2ac8d5ac29202e57bed0faa..892aad02c146e41dbe06e142bf9ee794f431c6a4 100644
--- a/util/all.v
+++ b/util/all.v
@@ -1,6 +1,7 @@
Require Export rt.util.tactics.
Require Export rt.util.notation.
Require Export rt.util.bigcat.
+Require Export rt.util.pick.
Require Export rt.util.bigord.
Require Export rt.util.counting.
Require Export rt.util.div_mod.
@@ -16,4 +17,4 @@ Require Export rt.util.sum.
Require Export rt.util.minmax.
Require Export rt.util.seqset.
Require Export rt.util.step_function.
-Require Export rt.util.pick.
\ No newline at end of file
+Require Export rt.util.epsilon.
diff --git a/util/list.v b/util/list.v
index 4f82d0aad92628075e64278fcfe0bb2aef2ef316..e822d2314b2c06a72a305aa57cdec916249ec24b 100644
--- a/util/list.v
+++ b/util/list.v
@@ -109,6 +109,52 @@ Section UniqList.
End UniqList.
+(* Additional lemmas about rem for lists. *)
+Section RemList.
+
+ (* We prove that if x lies in xs excluding y, then x also lies in xs. *)
+ Lemma rem_in:
+ forall (T: eqType) (x y: T) (xs: seq T),
+ x \in rem y xs -> x \in xs.
+ Proof.
+ clear; intros.
+ induction xs; simpl in H.
+ { by rewrite in_nil in H. }
+ { rewrite in_cons; apply/orP.
+ destruct (a == y) eqn:EQ.
+ { by move: EQ => /eqP EQ; subst a; right. }
+ { move: H; rewrite in_cons; move => /orP [/eqP H | H].
+ - by subst a; left.
+ - by right; apply IHxs.
+ }
+ }
+ Qed.
+
+ (* We prove that if we remove an element x for which P x from
+ a filter, then the size of the filter decreases by 1. *)
+ Lemma filter_size_rem:
+ forall (T: eqType) (x:T) (xs: seq T) (P: T -> bool),
+ (x \in xs) ->
+ P x ->
+ size [seq y <- xs | P y] = size [seq y <- rem x xs | P y] + 1.
+ Proof.
+ clear; intros.
+ induction xs; first by inversion H.
+ move: H; rewrite in_cons; move => /orP [/eqP H | H]; subst.
+ { by simpl; rewrite H0 -[X in X = _]addn1 eq_refl. }
+ { specialize (IHxs H); simpl in *.
+ case EQab: (a == x); simpl.
+ { move: EQab => /eqP EQab; subst.
+ by rewrite H0 addn1. }
+ { case Pa: (P a); simpl.
+ - by rewrite IHxs !addn1.
+ - by rewrite IHxs.
+ }
+ }
+ Qed.
+
+End RemList.
+
(* Additional lemmas about list zip. *)
Section Zip.
@@ -697,4 +743,89 @@ Section Order.
rel x2 x1 ->
x1 = x2.
-End Order.
\ No newline at end of file
+End Order.
+
+(* In this section we prove some additional lemmas about sequences. *)
+Section AdditionalLemmas.
+
+ (* We define a local function max over lists using foldl and maxn. *)
+ Let max := foldl maxn 0.
+
+ (* We prove that max {x, xs} is equal to max {x, max xs}. *)
+ Lemma seq_max_cons: forall x xs, max (x :: xs) = maxn x (max xs).
+ Proof.
+ have L: forall s x xs, foldl maxn s (x::xs) = maxn x (foldl maxn s xs).
+ { clear; intros.
+ generalize dependent s; generalize dependent x.
+ induction xs.
+ { by intros; rewrite maxnC. }
+ { intros; simpl in *.
+ by rewrite maxnC IHxs [maxn s a]maxnC IHxs maxnA [maxn s x]maxnC.
+ }
+ }
+ by intros; unfold max; apply L.
+ Qed.
+
+ (* We prove that for any two sequences xs and ys the fact that xs is a subsequence
+ of ys implies that the size of xs is at most the size of ys. *)
+ Lemma subseq_leq_size:
+ forall {T: eqType} (xs ys: seq T),
+ uniq xs ->
+ (forall x, x \in xs -> x \in ys) ->
+ size xs <= size ys.
+ Proof.
+ clear; intros ? ? ? UNIQ SUB.
+ have Lem:
+ forall a ys,
+ (a \in ys) ->
+ exists ysl ysr, ys = ysl ++ [::a] ++ ysr.
+ { clear; intros ? ? ? SUB.
+ induction ys; first by done.
+ move: SUB; rewrite in_cons; move => /orP [/eqP EQ|IN].
+ - by subst; exists [::], ys.
+ - feed IHys; first by done.
+ clear IN; move: IHys => [ysl [ysr EQ]].
+ by subst; exists(a0::ysl), ysr.
+ }
+ have EXm: exists m, size ys <= m.
+ { by exists (size ys). }
+ move: EXm => [m SIZEm].
+ move: SIZEm UNIQ SUB; move: xs ys.
+ induction m.
+ { intros.
+ move: SIZEm; rewrite leqn0 size_eq0; move => /eqP SIZEm; subst ys.
+ destruct xs; first by done.
+ specialize (SUB s).
+ feed SUB; first by rewrite in_cons; apply/orP; left.
+ by done.
+ }
+ { intros.
+ destruct xs as [ | x xs]; first by done.
+ specialize (@Lem _ x ys).
+ feed Lem.
+ { by apply SUB; rewrite in_cons; apply/orP; left. }
+ move: Lem => [ysl [ysr EQ]]; subst ys.
+ rewrite !size_cat; simpl; rewrite -addnC add1n addSn ltnS -size_cat.
+ eapply IHm.
+ - move: SIZEm; rewrite !size_cat; simpl; move => SIZE.
+ by rewrite add1n addnS ltnS addnC in SIZE.
+ - by move: UNIQ; rewrite cons_uniq; move => /andP [_ UNIQ].
+ - intros a IN.
+ destruct (a == x) eqn: EQ.
+ { exfalso.
+ move: EQ UNIQ; rewrite cons_uniq; move => /eqP EQ /andP [NIN UNIQ].
+ by subst; move: NIN => /negP NIN; apply: NIN.
+ }
+ { specialize (SUB a).
+ feed SUB.
+ { by rewrite in_cons; apply/orP; right. }
+ clear IN; move: SUB; rewrite !mem_cat; move => /orP [IN| /orP [IN|IN]].
+ - by apply/orP; right.
+ - exfalso.
+ by move: IN; rewrite in_cons; move => /orP [IN|IN]; [rewrite IN in EQ | ].
+ - by apply/orP; left.
+ }
+ }
+ Qed.
+
+End AdditionalLemmas.
\ No newline at end of file
diff --git a/util/minmax.v b/util/minmax.v
index ea69b93b3841ada7e6cfd4403d812a8e42ce09b2..5d8e673eead69db683195e482c4d06ccf26d50a8 100644
--- a/util/minmax.v
+++ b/util/minmax.v
@@ -514,14 +514,55 @@ End MinMaxSeq.
(* Additional lemmas about max. *)
Section ExtraLemmas.
-
- Lemma leq_big_max I r (P : pred I) (E1 E2 : I -> nat) :
- (forall i, P i -> E1 i <= E2 i) ->
- \max_(i <- r | P i) E1 i <= \max_(i <- r | P i) E2 i.
+
+ Lemma leq_bigmax_cond_seq (T : eqType) (P : pred T) (r : seq T) F i0 :
+ i0 \in r -> P i0 -> F i0 <= \max_(i <- r | P i) F i.
+ Proof.
+ intros IN0 Pi0; by rewrite (big_rem i0) //= Pi0 leq_maxl.
+ Qed.
+
+ Lemma bigmax_sup_seq:
+ forall (T: eqType) (i: T) r (P: pred T) m F,
+ i \in r -> P i -> m <= F i -> m <= \max_(i <- r| P i) F i.
+ Proof.
+ intros.
+ induction r.
+ - by rewrite in_nil in H.
+ move: H; rewrite in_cons; move => /orP [/eqP EQA | IN].
+ {
+ clear IHr; subst a.
+ rewrite (big_rem i) //=; last by rewrite in_cons; apply/orP; left.
+ apply leq_trans with (F i); first by done.
+ by rewrite H0 leq_maxl.
+ }
+ {
+ apply leq_trans with (\max_(i0 <- r | P i0) F i0); first by apply IHr.
+ rewrite [in X in _ <= X](big_rem a) //=; last by rewrite in_cons; apply/orP; left.
+
+ have Ob: a == a; first by done.
+ by rewrite Ob leq_maxr.
+ }
+ Qed.
+
+ Lemma bigmax_leq_seqP (T : eqType) (P : pred T) (r : seq T) F m :
+ reflect (forall i, i \in r -> P i -> F i <= m)
+ (\max_(i <- r | P i) F i <= m).
+ Proof.
+ apply: (iffP idP) => leFm => [i IINR Pi|];
+ first by apply: leq_trans leFm; apply leq_bigmax_cond_seq.
+ rewrite big_seq_cond; elim/big_ind: _ => // m1 m2.
+ by intros; rewrite geq_max; apply/andP; split.
+ by move: m2 => /andP [M1IN Pm1]; apply: leFm.
+ Qed.
+
+ Lemma leq_big_max (T : eqType) (P : pred T) (r : seq T) F1 F2 :
+ (forall i, i \in r -> P i -> F1 i <= F2 i) ->
+ \max_(i <- r | P i) F1 i <= \max_(i <- r | P i) F2 i.
Proof.
- move => leE12; elim/big_ind2 : _ => // m1 m2 n1 n2.
- intros LE1 LE2; rewrite leq_max; unfold maxn.
- by destruct (m2 < n2) eqn:LT; [by apply/orP; right | by apply/orP; left].
+ intros; apply /bigmax_leq_seqP; intros.
+ specialize (H i); feed_n 2 H; try(done).
+ rewrite (big_rem i) //=; rewrite H1.
+ by apply leq_trans with (F2 i); [ | rewrite leq_maxl].
Qed.
Lemma bigmax_ord_ltn_identity n :
diff --git a/util/nat.v b/util/nat.v
index 8cb1de9b36c62cb77ede8e206205e88e6b43d772..e661c533d427033d3a7e66320e7ffe6a1013bfd1 100644
--- a/util/nat.v
+++ b/util/nat.v
@@ -22,7 +22,7 @@ Section NatLemmas.
n1 >= n2 ->
(m1 + n1) - (m2 + n2) = m1 - m2 + (n1 - n2).
Proof. by ins; ssromega. Qed.
-
+
Lemma subh3 :
forall m n p,
m + p <= n ->
@@ -33,6 +33,21 @@ Section NatLemmas.
by rewrite subh1 // -addnBA // subnn addn0.
Qed.
+ (* subh3: forall m n p : nat, m + p <= n -> p <= n -> m <= n - p *)
+ (* unnecessary condition -- ^^^^^^^^^ *)
+ (* TODO: del subh3 *)
+ Lemma subh3_ext:
+ forall m n p,
+ m + p <= n ->
+ m <= n - p.
+ Proof.
+ clear.
+ intros.
+ apply subh3; first by done.
+ apply leq_trans with (m+p); last by done.
+ by rewrite leq_addl.
+ Qed.
+
Lemma subh4:
forall m n p,
m <= n ->
diff --git a/util/step_function.v b/util/step_function.v
index a1e3fcd4497bb36ab2a33d48f7c10cf49cfa6ab9..c999715f6417b7e1760892424284d0b23d341f42 100644
--- a/util/step_function.v
+++ b/util/step_function.v
@@ -85,5 +85,50 @@ Section StepFunction.
End ExistsIntermediateValue.
End Lemmas.
+
+ (* In this section, we prove an analogue of the intermediate
+ value theorem, but for predicates of natural numbers. *)
+ Section ExistsIntermediateValuePredicates.
+
+ (* Let P be any predicate on natural numbers. *)
+ Variable P: nat -> bool.
+
+ (* Consider a time interval [t1,t2] such that ... *)
+ Variables t1 t2: nat.
+ Hypothesis H_t1_le_t2: t1 <= t2.
+
+ (* ... P doesn't hold for t1 ... *)
+ Hypothesis H_not_P_at_t1: ~~ P t1.
+
+ (* ... but holds for t2. *)
+ Hypothesis H_P_at_t2: P t2.
+
+ (* Then we prove that within time interval [t1,t2] there exists time
+ instant t such that t is the first time instant when P holds. *)
+ Lemma exists_first_intermediate_point:
+ exists t, (t1 < t <= t2) /\ (forall x, t1 <= x < t -> ~~ P x) /\ P t.
+ Proof.
+ have EX: exists x, P x && (t1 < x <= t2).
+ { exists t2.
+ apply/andP; split; first by done.
+ apply/andP; split; last by done.
+ move: H_t1_le_t2; rewrite leq_eqVlt; move => /orP [/eqP EQ | NEQ1]; last by done.
+ by exfalso; subst t2; move: H_not_P_at_t1 => /negP NPt1.
+ }
+ have MIN := ex_minnP EX.
+ move: MIN => [x /andP [Px /andP [LT1 LT2]] MIN]; clear EX.
+ exists x; repeat split; [ apply/andP; split | | ]; try done.
+ move => y /andP [NEQ1 NEQ2]; apply/negPn; intros Py.
+ feed (MIN y).
+ { apply/andP; split; first by done.
+ apply/andP; split.
+ - move: NEQ1. rewrite leq_eqVlt; move => /orP [/eqP EQ | NEQ1]; last by done.
+ by exfalso; subst y; move: H_not_P_at_t1 => /negP NPt1.
+ - by apply ltnW, leq_trans with x.
+ }
+ by move: NEQ2; rewrite ltnNge; move => /negP NEQ2.
+ Qed.
+
+ End ExistsIntermediateValuePredicates.
End StepFunction.
\ No newline at end of file
diff --git a/util/sum.v b/util/sum.v
index 7980bd4c2b6fa3153400e05727efd856dc56c38f..6266d3da93ecf455aa5b10ca758477cb5e6f14fd 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -1,88 +1,7 @@
Require Import rt.util.tactics rt.util.notation rt.util.sorting rt.util.nat.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
-(* Lemmas about arithmetic with sums. *)
-Section SumArithmetic.
-
- (* Inequality with sums is monotonic with their functions. *)
- Lemma sum_diff_monotonic :
- forall n G F,
- (forall i : nat, i < n -> G i <= F i) ->
- (\sum_(0 <= i < n) (G i)) <= (\sum_(0 <= i < n) (F i)).
- Proof.
- intros n G F ALL.
- rewrite big_nat_cond [\sum_(0 <= i < n) F i]big_nat_cond.
- apply leq_sum; intros i LT; rewrite andbT in LT.
- move: LT => /andP LT; des.
- by apply ALL, leq_trans with (n := n); ins.
- Qed.
-
- Lemma sum_diff :
- forall n F G,
- (forall 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.
- induction n; ins; first by rewrite 3?big_geq.
- assert (ALL': forall i, i < n -> G i <= F i).
- by ins; apply ALL, leq_trans with (n := n); ins.
- rewrite 3?big_nat_recr // IHn //; simpl.
- rewrite subh1; last by apply sum_diff_monotonic.
- rewrite subh2 //; try apply sum_diff_monotonic; ins.
- rewrite subh1; ins; apply sum_diff_monotonic; ins.
- by apply ALL; rewrite ltnS leqnn.
- Qed.
-
- Lemma telescoping_sum :
- forall (T: Type) (F: T->nat) r (x0: T),
- (forall 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)).
- Proof.
- intros T F r x0 ALL.
- have ADD1 := big_add1.
- have RECL := big_nat_recl.
- specialize (ADD1 nat 0 addn 0 (size r) (fun x => true) (fun i => F (nth x0 r i))).
- specialize (RECL nat 0 addn (size r).-1 0 (fun i => F (nth x0 r i))).
- rewrite sum_diff; last by ins.
- rewrite addmovr; last by rewrite -[_.-1]add0n; apply prev_le_next; try rewrite add0n leqnn.
- rewrite subh1; last by apply sum_diff_monotonic.
- rewrite addnC -RECL //.
- rewrite addmovl; last by rewrite big_nat_recr // -{1}[\sum_(_ <= _ < _) _]addn0; apply leq_add.
- by rewrite addnC -big_nat_recr.
- Qed.
-
- Lemma leq_sum_sub_uniq :
- forall (T: eqType) (r1 r2: seq T) F,
- uniq r1 ->
- {subset r1 <= r2} ->
- \sum_(i <- r1) F i <= \sum_(i <- r2) F i.
- Proof.
- intros T r1 r2 F UNIQ SUB; generalize dependent r2.
- induction r1 as [| x r1' IH]; first by ins; rewrite big_nil.
- {
- intros r2 SUB.
- assert (IN: x \in r2).
- by apply SUB; rewrite in_cons eq_refl orTb.
- simpl in UNIQ; move: UNIQ => /andP [NOTIN UNIQ]; specialize (IH UNIQ).
- destruct (splitPr IN).
- rewrite big_cat 2!big_cons /= addnA [_ + F x]addnC -addnA leq_add2l.
- rewrite mem_cat in_cons eq_refl in IN.
- rewrite -big_cat /=.
- apply IH; red; intros x0 IN0.
- rewrite mem_cat.
- feed (SUB x0); first by rewrite in_cons IN0 orbT.
- rewrite mem_cat in_cons in SUB.
- move: SUB => /orP [SUB1 | /orP [/eqP EQx | SUB2]];
- [by rewrite SUB1 | | by rewrite SUB2 orbT].
- by rewrite -EQx IN0 in NOTIN.
- }
- Qed.
-
-End SumArithmetic.
-
-(* Additional lemmas about sum. *)
+(* Lemmas about sum. *)
Section ExtraLemmas.
Lemma extend_sum :
@@ -97,7 +16,7 @@ Section ExtraLemmas.
rewrite -> big_cat_nat with (m := t1') (n := t1); try (by done); simpl;
last by apply leq_trans with (n := t2).
rewrite -> big_cat_nat with (p := t2') (n := t2); try (by done); simpl.
- by rewrite addnC -addnA; apply leq_addr.
+ by rewrite addnC -addnA; apply leq_addr.
Qed.
Lemma leq_sum_nat m n (P : pred nat) (E1 E2 : nat -> nat) :
@@ -106,7 +25,7 @@ Section ExtraLemmas.
Proof.
intros LE.
rewrite big_nat_cond [\sum_(_ <= _ < _| P _)_]big_nat_cond.
- by apply leq_sum; move => j /andP [IN H]; apply LE.
+ by apply leq_sum; move => j /andP [IN H]; apply LE.
Qed.
Lemma leq_sum_seq (I: eqType) (r: seq I) (P : pred I) (E1 E2 : I -> nat) :
@@ -115,7 +34,7 @@ Section ExtraLemmas.
Proof.
intros LE.
rewrite big_seq_cond [\sum_(_ <- _| P _)_]big_seq_cond.
- by apply leq_sum; move => j /andP [IN H]; apply LE.
+ by apply leq_sum; move => j /andP [IN H]; apply LE.
Qed.
Lemma sum_nat_eq0_nat (T : eqType) (F : T -> nat) (r: seq T) :
@@ -128,7 +47,7 @@ Section ExtraLemmas.
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.
+ by move: ZERO => /implyP ZERO; apply/eqP; apply ZERO.
}
{
apply negbT in ZERO; rewrite -has_predC in ZERO.
@@ -136,7 +55,7 @@ Section ExtraLemmas.
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.
+ by rewrite lt0n.
}
Qed.
@@ -153,7 +72,7 @@ Section ExtraLemmas.
case TRUE: (P i); last by done.
move: (REDUCE i (conj LE TRUE)) => [LE' TRUE'].
rewrite (big_rem i); last by rewrite mem_index_iota.
- by rewrite TRUE' eq_refl.
+ by rewrite TRUE' eq_refl.
}
{
apply leq_sum_nat; intros i LE TRUE.
@@ -162,12 +81,242 @@ Section ExtraLemmas.
{
rewrite big_nat_cond big1; first by done.
move => i' /andP [LE'' _]; case EQ: (_ == _); last by done.
- by move: EQ => /eqP EQ; subst; rewrite LE'' in LE'.
+ by move: EQ => /eqP EQ; subst; rewrite LE'' in LE'.
}
rewrite (bigD1_seq i) /=; [ | by rewrite mem_index_iota | by rewrite iota_uniq ].
rewrite eq_refl big1; first by done.
- by move => i' /negbTE NEQ; rewrite NEQ.
+ by move => i' /negbTE NEQ; rewrite NEQ.
+ }
+ Qed.
+
+ Lemma sum_seq_gt0P:
+ forall (T:eqType) (r: seq T) (F: T -> nat),
+ reflect (exists 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.
+ exists 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]].
+ exists 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 leq_pred_sum:
+ forall (T:eqType) (r: seq T) (P1 P2: pred T) F,
+ (forall i, P1 i -> P2 i) ->
+ \sum_(i <- r | P1 i) F i <=
+ \sum_(i <- r | P2 i) F i.
+ Proof.
+ intros.
+ rewrite big_mkcond [in X in _ <= X]big_mkcond//= leq_sum //.
+ intros i _.
+ destruct P1 eqn:P1a; destruct P2 eqn:P2a; [by done | | by done | by done].
+ exfalso.
+ move: P1a P2a => /eqP P1a /eqP P2a.
+ rewrite eqb_id in P1a; rewrite eqbF_neg in P2a.
+ move: P2a => /negP P2a.
+ by apply P2a; apply H.
+ Qed.
+
+ Lemma sum_notin_rem_eqn:
+ forall (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.
-End ExtraLemmas.
\ No newline at end of file
+ (* 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:
+ forall (T: eqType) (r: seq T) (P: pred T) F const,
+ (forall 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:
+ forall (T: eqType) xs F1 F2 (P: pred T),
+ (forall x, x \in xs -> P x -> F1 x <= F2 x) ->
+ \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
+ (forall x, x \in xs -> P x -> F1 x = F2 x).
+ Proof.
+ clear.
+ 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: forall a b c d, a + b = c + d -> a <= c -> b >= d.
+ { clear; intros.
+ rewrite leqNgt; apply/negP; intros H1.
+ move: H => /eqP; rewrite eqn_leq; move => /andP [LE GE].
+ move: GE; rewrite leqNgt; move => /negP GE; apply: GE.
+ by apply leq_trans with (a + d); [rewrite ltn_add2l | rewrite leq_add2r]. }
+ 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:
+ forall t Δ,
+ \sum_(t <= x < t + Δ) 1 = Δ.
+ Proof.
+ intros.
+ simpl_sum_const.
+ rewrite addnC -addnBA; last by done.
+ by rewrite subnn addn0.
+ Qed.
+
+End ExtraLemmas.
+
+(* Lemmas about arithmetic with sums. *)
+Section SumArithmetic.
+
+ Lemma sum_seq_diff:
+ forall (T:eqType) (r: seq T) (F G : T -> nat),
+ (forall i : T, i \in r -> G i <= F i) ->
+ \sum_(i <- r) (F i - G i) = \sum_(i <- r) F i - \sum_(i <- r) G i.
+ Proof.
+ intros.
+ induction r; first by rewrite !big_nil subn0.
+ rewrite !big_cons subh2.
+ - apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHr.
+ 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:
+ forall n F G,
+ (forall 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 telescoping_sum :
+ forall (T: Type) (F: T->nat) r (x0: T),
+ (forall 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)).
+ Proof.
+ intros T F r x0 ALL.
+ have ADD1 := big_add1.
+ have RECL := big_nat_recl.
+ specialize (ADD1 nat 0 addn 0 (size r) (fun x => true) (fun i => F (nth x0 r i))).
+ specialize (RECL nat 0 addn (size r).-1 0 (fun i => F (nth x0 r i))).
+ rewrite sum_diff; last by ins.
+ rewrite addmovr; last by rewrite -[_.-1]add0n; apply prev_le_next; try rewrite add0n leqnn.
+ rewrite subh1; last by apply leq_sum_nat; move => i /andP [_ LT] _; apply ALL.
+ rewrite addnC -RECL //.
+ rewrite addmovl; last by rewrite big_nat_recr // -{1}[\sum_(_ <= _ < _) _]addn0; apply leq_add.
+ by rewrite addnC -big_nat_recr.
+ Qed.
+
+ Lemma leq_sum_sub_uniq :
+ forall (T: eqType) (r1 r2: seq T) F,
+ uniq r1 ->
+ {subset r1 <= r2} ->
+ \sum_(i <- r1) F i <= \sum_(i <- r2) F i.
+ Proof.
+ intros T r1 r2 F UNIQ SUB; generalize dependent r2.
+ induction r1 as [| x r1' IH]; first by ins; rewrite big_nil.
+ {
+ intros r2 SUB.
+ assert (IN: x \in r2).
+ by apply SUB; rewrite in_cons eq_refl orTb.
+ simpl in UNIQ; move: UNIQ => /andP [NOTIN UNIQ]; specialize (IH UNIQ).
+ destruct (splitPr IN).
+ rewrite big_cat 2!big_cons /= addnA [_ + F x]addnC -addnA leq_add2l.
+ rewrite mem_cat in_cons eq_refl in IN.
+ rewrite -big_cat /=.
+ apply IH; red; intros x0 IN0.
+ rewrite mem_cat.
+ feed (SUB x0); first by rewrite in_cons IN0 orbT.
+ rewrite mem_cat in_cons in SUB.
+ move: SUB => /orP [SUB1 | /orP [/eqP EQx | SUB2]];
+ [by rewrite SUB1 | | by rewrite SUB2 orbT].
+ by rewrite -EQx IN0 in NOTIN.
+ }
+ Qed.
+
+End SumArithmetic.
\ No newline at end of file