From 1c1a8bf97e2816b4c086e7e0f8d96e759838ee10 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre@roux01.fr>
Date: Sat, 19 Feb 2022 22:48:37 +0100
Subject: [PATCH] Simplify proof of {l,}eq_sum_seq
---
util/sum.v | 14 +++++---------
1 file changed, 5 insertions(+), 9 deletions(-)
diff --git a/util/sum.v b/util/sum.v
index 1cc6575a3..783cd15dd 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -117,9 +117,8 @@ Section SumsOverSequences.
(forall 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.
+ move=> le; rewrite big_seq_cond [X in _ <= X]big_seq_cond.
+ apply: leq_sum => i /andP[]; exact: le.
Qed.
(** In the same way, if [E1] equals [E2] in all the points considered above, then also the two
@@ -128,13 +127,10 @@ Section SumsOverSequences.
(forall 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.
- move=> EQ.
- rewrite big_seq_cond [\sum_(_ <- _| P _)_]big_seq_cond.
- rewrite eqn_leq; apply /andP; split.
- all: apply leq_sum; move => j /andP [IN H].
- all: by move:(EQ j IN H) => LEQ; lia.
+ move=> eqE; apply/eqP; rewrite -big_filter -[RHS]big_filter.
+ apply: eq_big_seq => x; rewrite mem_filter => /andP[Px xr]; exact/eqP/eqE.
Qed.
-
+
(** 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
--
GitLab