Library prosa.util.sum
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 39)
I : eqType
r : seq I
P : pred I
E1, E2 : I -> nat
============================
(forall i : 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 40)
I : eqType
r : seq I
P : pred I
E1, E2 : I -> nat
LE : forall i : I, i \in r -> P i -> E1 i <= E2 i
============================
\sum_(i <- r | P i) E1 i <= \sum_(i <- r | P i) E2 i
----------------------------------------------------------------------------- *)
rewrite big_seq_cond [\sum_(_ <- _| P _)_]big_seq_cond.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 67)
I : eqType
r : seq I
P : pred I
E1, E2 : I -> nat
LE : forall i : I, i \in r -> P i -> E1 i <= E2 i
============================
\sum_(i <- r | (i \in r) && P i) E1 i <=
\sum_(i <- r | (i \in r) && P i) E2 i
----------------------------------------------------------------------------- *)
by apply leq_sum; move ⇒ j /andP [IN H]; apply LE.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
============================
forall (I : eqType) (r : seq I) (P : pred I) (E1 E2 : I -> nat),
(forall i : 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.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 94)
I : eqType
r : seq I
P : pred I
E1, E2 : I -> nat
H : forall i : I, i \in r -> P i -> E1 i == E2 i
============================
\sum_(i <- r | P i) E1 i <= \sum_(i <- r | P i) E2 i
subgoal 2 (ID 95) is:
\sum_(i <- r | P i) E2 i <= \sum_(i <- r | P i) E1 i
----------------------------------------------------------------------------- *)
- apply leq_sum_seq; intros.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 99)
I : eqType
r : seq I
P : pred I
E1, E2 : I -> nat
H : forall i : I, i \in r -> P i -> E1 i == E2 i
i : I
H0 : i \in r
H1 : P i
============================
E1 i <= E2 i
subgoal 2 (ID 95) is:
\sum_(i <- r | P i) E2 i <= \sum_(i <- r | P i) E1 i
----------------------------------------------------------------------------- *)
by move: (H i H0 H1) ⇒ /eqP EQ; rewrite EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 95)
I : eqType
r : seq I
P : pred I
E1, E2 : I -> nat
H : forall i : I, i \in r -> P i -> E1 i == E2 i
============================
\sum_(i <- r | P i) E2 i <= \sum_(i <- r | P i) E1 i
----------------------------------------------------------------------------- *)
- apply leq_sum_seq; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 140)
I : eqType
r : seq I
P : pred I
E1, E2 : I -> nat
H : forall i : I, i \in r -> P i -> E1 i == E2 i
i : I
H0 : i \in r
H1 : P i
============================
E2 i <= E1 i
----------------------------------------------------------------------------- *)
by move: (H i H0 H1) ⇒ /eqP EQ; rewrite EQ.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 73)
T : eqType
F : T -> nat
r : seq T
============================
all (fun x : T => F x == 0) r = (\sum_(i <- r) F i == 0)
----------------------------------------------------------------------------- *)
Proof.
destruct (all (fun x ⇒ F x == 0) r) eqn:ZERO.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 88)
T : eqType
F : T -> nat
r : seq T
ZERO : all (fun x : T => F x == 0) r = true
============================
true = (\sum_(i <- r) F i == 0)
subgoal 2 (ID 89) is:
false = (\sum_(i <- r) F i == 0)
----------------------------------------------------------------------------- *)
- move: ZERO ⇒ /allP ZERO; rewrite -leqn0.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 128)
T : eqType
F : T -> nat
r : seq T
ZERO : {in r, forall x : T, F x == 0}
============================
true = (\sum_(i <- r) F i <= 0)
subgoal 2 (ID 89) is:
false = (\sum_(i <- r) F i == 0)
----------------------------------------------------------------------------- *)
rewrite big_seq_cond (eq_bigr (fun x ⇒ 0));
first by rewrite big_const_seq iter_addn mul0n addn0 leqnn.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 157)
T : eqType
F : T -> nat
r : seq T
ZERO : {in r, forall x : T, F x == 0}
============================
forall i : T, (i \in r) && true -> F i = 0
subgoal 2 (ID 89) is:
false = (\sum_(i <- r) F i == 0)
----------------------------------------------------------------------------- *)
intro i; rewrite andbT; intros IN.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 191)
T : eqType
F : T -> nat
r : seq T
ZERO : {in r, forall x : T, F x == 0}
i : T
IN : i \in r
============================
F i = 0
subgoal 2 (ID 89) is:
false = (\sum_(i <- r) F i == 0)
----------------------------------------------------------------------------- *)
specialize (ZERO i); rewrite IN in ZERO.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 208)
T : eqType
F : T -> nat
r : seq T
i : T
IN : i \in r
ZERO : true -> F i == 0
============================
F i = 0
subgoal 2 (ID 89) is:
false = (\sum_(i <- r) F i == 0)
----------------------------------------------------------------------------- *)
by move: ZERO ⇒ /implyP ZERO; apply/eqP; apply ZERO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 89)
T : eqType
F : T -> nat
r : seq T
ZERO : all (fun x : T => F x == 0) r = false
============================
false = (\sum_(i <- r) F i == 0)
----------------------------------------------------------------------------- *)
- apply negbT in ZERO; rewrite -has_predC in ZERO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 335)
T : eqType
F : T -> nat
r : seq T
ZERO : has (predC (fun x : T => F x == 0)) r
============================
false = (\sum_(i <- r) F i == 0)
----------------------------------------------------------------------------- *)
move: ZERO ⇒ /hasP ZERO; destruct ZERO as [x IN NEQ]; simpl in NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 378)
T : eqType
F : T -> nat
r : seq T
x : T
IN : x \in r
NEQ : F x != 0
============================
false = (\sum_(i <- r) F i == 0)
----------------------------------------------------------------------------- *)
rewrite (big_rem x) /=; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 395)
T : eqType
F : T -> nat
r : seq T
x : T
IN : x \in r
NEQ : F x != 0
============================
false = (F x + \sum_(y <- rem (T:=T) x r) F y == 0)
----------------------------------------------------------------------------- *)
symmetry; apply negbTE; rewrite neq_ltn; apply/orP; right.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 429)
T : eqType
F : T -> nat
r : seq T
x : T
IN : x \in r
NEQ : F x != 0
============================
0 < F x + \sum_(y <- rem (T:=T) x r) F y
----------------------------------------------------------------------------- *)
apply leq_trans with (n := F x); last by apply leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 430)
T : eqType
F : T -> nat
r : seq T
x : T
IN : x \in r
NEQ : F x != 0
============================
0 < F x
----------------------------------------------------------------------------- *)
by rewrite lt0n.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 86)
============================
forall (T : eqType) (r : seq T) (F : T -> nat),
reflect (exists i : T, i \in r /\ 0 < F i) (0 < \sum_(i <- r) F i)
----------------------------------------------------------------------------- *)
Proof.
intros; apply: (iffP idP); intros.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 123)
T : eqType
r : seq T
F : T -> nat
H : 0 < \sum_(i <- r) F i
============================
exists i : T, i \in r /\ 0 < F i
subgoal 2 (ID 124) is:
0 < \sum_(i <- r) F i
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 123)
T : eqType
r : seq T
F : T -> nat
H : 0 < \sum_(i <- r) F i
============================
exists i : T, i \in r /\ 0 < F i
----------------------------------------------------------------------------- *)
induction r; first by rewrite big_nil in H.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 140)
T : eqType
a : T
r : seq T
F : T -> nat
H : 0 < \sum_(i <- (a :: r)) F i
IHr : 0 < \sum_(i <- r) F i -> exists i : T, i \in r /\ 0 < F i
============================
exists i : T, i \in a :: r /\ 0 < F i
----------------------------------------------------------------------------- *)
destruct (F a > 0) eqn:POS.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 195)
T : eqType
a : T
r : seq T
F : T -> nat
H : 0 < \sum_(i <- (a :: r)) F i
IHr : 0 < \sum_(i <- r) F i -> exists i : T, i \in r /\ 0 < F i
POS : (0 < F a) = true
============================
exists i : T, i \in a :: r /\ 0 < F i
subgoal 2 (ID 196) is:
exists i : T, i \in a :: r /\ 0 < F i
----------------------------------------------------------------------------- *)
∃ a; split; [by rewrite in_cons; apply/orP; left | by done].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 196)
T : eqType
a : T
r : seq T
F : T -> nat
H : 0 < \sum_(i <- (a :: r)) F i
IHr : 0 < \sum_(i <- r) F i -> exists i : T, i \in r /\ 0 < F i
POS : (0 < F a) = false
============================
exists i : T, i \in a :: r /\ 0 < F i
----------------------------------------------------------------------------- *)
apply negbT in POS; rewrite -leqNgt leqn0 in POS; move: POS ⇒ /eqP POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 292)
T : eqType
a : T
r : seq T
F : T -> nat
H : 0 < \sum_(i <- (a :: r)) F i
IHr : 0 < \sum_(i <- r) F i -> exists i : T, i \in r /\ 0 < F i
POS : F a = 0
============================
exists i : T, i \in a :: r /\ 0 < F i
----------------------------------------------------------------------------- *)
rewrite big_cons POS add0n in H.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 323)
T : eqType
a : T
r : seq T
F : T -> nat
IHr : 0 < \sum_(i <- r) F i -> exists i : T, i \in r /\ 0 < F i
POS : F a = 0
H : 0 < \sum_(j <- r) F j
============================
exists i : T, i \in a :: r /\ 0 < F i
----------------------------------------------------------------------------- *)
clear POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 324)
T : eqType
a : T
r : seq T
F : T -> nat
IHr : 0 < \sum_(i <- r) F i -> exists i : T, i \in r /\ 0 < F i
H : 0 < \sum_(j <- r) F j
============================
exists i : T, i \in a :: r /\ 0 < F i
----------------------------------------------------------------------------- *)
feed IHr; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 330)
T : eqType
a : T
r : seq T
F : T -> nat
IHr : exists i : T, i \in r /\ 0 < F i
H : 0 < \sum_(j <- r) F j
============================
exists i : T, i \in a :: r /\ 0 < F i
----------------------------------------------------------------------------- *)
move: IHr ⇒ [i [IN POS]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 353)
T : eqType
a : T
r : seq T
F : T -> nat
H : 0 < \sum_(j <- r) F j
i : T
IN : i \in r
POS : 0 < F i
============================
exists i0 : T, i0 \in a :: r /\ 0 < F i0
----------------------------------------------------------------------------- *)
∃ i; split; [by rewrite in_cons; apply/orP;right | by done].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 124)
subgoal 1 (ID 124) is:
0 < \sum_(i <- r) F i
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 124)
T : eqType
r : seq T
F : T -> nat
H : exists i : T, i \in r /\ 0 < F i
============================
0 < \sum_(i <- r) F i
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 124)
T : eqType
r : seq T
F : T -> nat
H : exists i : T, i \in r /\ 0 < F i
============================
0 < \sum_(i <- r) F i
----------------------------------------------------------------------------- *)
move: H ⇒ [i [IN POS]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 413)
T : eqType
r : seq T
F : T -> nat
i : T
IN : i \in r
POS : 0 < F i
============================
0 < \sum_(i0 <- r) F i0
----------------------------------------------------------------------------- *)
rewrite (big_rem i) //=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 430)
T : eqType
r : seq T
F : T -> nat
i : T
IN : i \in r
POS : 0 < F i
============================
0 < F i + \sum_(y <- rem (T:=T) i r) F y
----------------------------------------------------------------------------- *)
apply leq_trans with (F i); [by done | by rewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 114)
============================
forall (T : eqType) (a : T) (xs : seq_predType T)
(P : T -> bool) (F : T -> nat),
a \notin xs ->
\sum_(x <- xs | P x && (x != a)) F x = \sum_(x <- xs | P x) F x
----------------------------------------------------------------------------- *)
Proof.
intros ? ? ? ? ? NOTIN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 120)
T : eqType
a : T
xs : seq_predType T
P : T -> bool
F : T -> nat
NOTIN : a \notin xs
============================
\sum_(x <- xs | P x && (x != a)) F x = \sum_(x <- xs | P x) F x
----------------------------------------------------------------------------- *)
induction xs; first by rewrite !big_nil.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 136)
T : eqType
a, a0 : T
xs : seq T
P : T -> bool
F : T -> nat
NOTIN : a \notin a0 :: xs
IHxs : a \notin xs ->
\sum_(x <- xs | P x && (x != a)) F x = \sum_(x <- xs | P x) F x
============================
\sum_(x <- (a0 :: xs) | P x && (x != a)) F x =
\sum_(x <- (a0 :: xs) | P x) F x
----------------------------------------------------------------------------- *)
rewrite !big_cons.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 178)
T : eqType
a, a0 : T
xs : seq T
P : T -> bool
F : T -> nat
NOTIN : a \notin a0 :: xs
IHxs : a \notin xs ->
\sum_(x <- xs | P x && (x != a)) F x = \sum_(x <- xs | P x) F x
============================
(if P a0 && (a0 != a)
then F a0 + \sum_(j <- xs | P j && (j != a)) F j
else \sum_(j <- xs | P j && (j != a)) F j) =
(if P a0 then F a0 + \sum_(j <- xs | P j) F j else \sum_(j <- xs | P j) F j)
----------------------------------------------------------------------------- *)
rewrite IHxs; clear IHxs; last first.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 192)
T : eqType
a, a0 : T
xs : seq T
P : T -> bool
F : T -> nat
NOTIN : a \notin a0 :: xs
============================
a \notin xs
subgoal 2 (ID 191) is:
(if P a0 && (a0 != a)
then F a0 + \sum_(x <- xs | P x) F x
else \sum_(x <- xs | P x) F x) =
(if P a0 then F a0 + \sum_(j <- xs | P j) F j else \sum_(j <- xs | P j) F j)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 192)
T : eqType
a, a0 : T
xs : seq T
P : T -> bool
F : T -> nat
NOTIN : a \notin a0 :: xs
============================
a \notin xs
----------------------------------------------------------------------------- *)
apply/memPn; intros y IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 223)
T : eqType
a, a0 : T
xs : seq T
P : T -> bool
F : T -> nat
NOTIN : a \notin a0 :: xs
y : T
IN : y \in xs
============================
y != a
----------------------------------------------------------------------------- *)
move: NOTIN ⇒ /memPn NOTIN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 259)
T : eqType
a, a0 : T
xs : seq T
P : T -> bool
F : T -> nat
y : T
IN : y \in xs
NOTIN : {in a0 :: xs, forall y : T, y != a}
============================
y != a
----------------------------------------------------------------------------- *)
by apply NOTIN; rewrite in_cons; apply/orP; right.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 191)
subgoal 1 (ID 191) is:
(if P a0 && (a0 != a)
then F a0 + \sum_(x <- xs | P x) F x
else \sum_(x <- xs | P x) F x) =
(if P a0 then F a0 + \sum_(j <- xs | P j) F j else \sum_(j <- xs | P j) F j)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 191)
T : eqType
a, a0 : T
xs : seq T
P : T -> bool
F : T -> nat
NOTIN : a \notin a0 :: xs
============================
(if P a0 && (a0 != a)
then F a0 + \sum_(x <- xs | P x) F x
else \sum_(x <- xs | P x) F x) =
(if P a0 then F a0 + \sum_(j <- xs | P j) F j else \sum_(j <- xs | P j) F j)
----------------------------------------------------------------------------- *)
move: NOTIN ⇒ /memPn NOTIN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 328)
T : eqType
a, a0 : T
xs : seq T
P : T -> bool
F : T -> nat
NOTIN : {in a0 :: xs, forall y : T, y != a}
============================
(if P a0 && (a0 != a)
then F a0 + \sum_(x <- xs | P x) F x
else \sum_(x <- xs | P x) F x) =
(if P a0 then F a0 + \sum_(j <- xs | P j) F j else \sum_(j <- xs | P j) F j)
----------------------------------------------------------------------------- *)
move: (NOTIN a0) ⇒ NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 330)
T : eqType
a, a0 : T
xs : seq T
P : T -> bool
F : T -> nat
NOTIN : {in a0 :: xs, forall y : T, y != a}
NEQ : a0 \in a0 :: xs -> a0 != a
============================
(if P a0 && (a0 != a)
then F a0 + \sum_(x <- xs | P x) F x
else \sum_(x <- xs | P x) F x) =
(if P a0 then F a0 + \sum_(j <- xs | P j) F j else \sum_(j <- xs | P j) F j)
----------------------------------------------------------------------------- *)
feed NEQ; first by (rewrite in_cons; apply/orP; left).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 336)
T : eqType
a, a0 : T
xs : seq T
P : T -> bool
F : T -> nat
NOTIN : {in a0 :: xs, forall y : T, y != a}
NEQ : a0 != a
============================
(if P a0 && (a0 != a)
then F a0 + \sum_(x <- xs | P x) F x
else \sum_(x <- xs | P x) F x) =
(if P a0 then F a0 + \sum_(j <- xs | P j) F j else \sum_(j <- xs | P j) F j)
----------------------------------------------------------------------------- *)
by rewrite NEQ Bool.andb_true_r.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(* Trivial identity: any sum of zeros is zero. *)
Lemma sum0 m n:
\sum_(m ≤ i < n) 0 = 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 125)
m, n : nat
============================
\sum_(m <= i < n) 0 = 0
----------------------------------------------------------------------------- *)
Proof.
by rewrite big_const_nat iter_addn mul0n addn0 //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 143)
m, n : nat
F : nat -> nat
============================
\sum_(m <= i < n) F i = 0 <-> (forall i : nat, m <= i < n -> F i = 0)
----------------------------------------------------------------------------- *)
Proof.
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 145)
m, n : nat
F : nat -> nat
============================
\sum_(m <= i < n) F i = 0 -> forall i : nat, m <= i < n -> F i = 0
subgoal 2 (ID 146) is:
(forall i : nat, m <= i < n -> F i = 0) -> \sum_(m <= i < n) F i = 0
----------------------------------------------------------------------------- *)
- rewrite /index_iota ⇒ /eqP.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 205)
m, n : nat
F : nat -> nat
============================
\sum_(i <- iota m (n - m)) F i == 0 ->
forall i : nat, m <= i < n -> F i = 0
subgoal 2 (ID 146) is:
(forall i : nat, m <= i < n -> F i = 0) -> \sum_(m <= i < n) F i = 0
----------------------------------------------------------------------------- *)
rewrite -sum_nat_eq0_nat ⇒ /allP ZERO i.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 245)
m, n : nat
F : nat -> nat
ZERO : {in iota m (n - m), forall x : nat_eqType, F x == 0}
i : nat
============================
m <= i < n -> F i = 0
subgoal 2 (ID 146) is:
(forall i : nat, m <= i < n -> F i = 0) -> \sum_(m <= i < n) F i = 0
----------------------------------------------------------------------------- *)
rewrite -mem_index_iota /index_iota ⇒ IN.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 252)
m, n : nat
F : nat -> nat
ZERO : {in iota m (n - m), forall x : nat_eqType, F x == 0}
i : nat
IN : i \in iota m (n - m)
============================
F i = 0
subgoal 2 (ID 146) is:
(forall i : nat, m <= i < n -> F i = 0) -> \sum_(m <= i < n) F i = 0
----------------------------------------------------------------------------- *)
by apply/eqP; apply ZERO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 146)
m, n : nat
F : nat -> nat
============================
(forall i : nat, m <= i < n -> F i = 0) -> \sum_(m <= i < n) F i = 0
----------------------------------------------------------------------------- *)
- move⇒ ZERO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 309)
m, n : nat
F : nat -> nat
ZERO : forall i : nat, m <= i < n -> F i = 0
============================
\sum_(m <= i < n) F i = 0
----------------------------------------------------------------------------- *)
have ->: \sum_(m ≤ i < n) F i = \sum_(m ≤ i < n) 0
by apply eq_big_nat ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 326)
m, n : nat
F : nat -> nat
ZERO : forall i : nat, m <= i < n -> F i = 0
============================
\sum_(m <= i < n) 0 = 0
----------------------------------------------------------------------------- *)
by apply sum0.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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]).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 162)
============================
forall (T : eqType) (r : seq T) (P : pred T) (F : T -> nat) (const : nat),
(forall a : T, 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 168)
T : eqType
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a : T, a \in r -> P a -> F a <= const
============================
\sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
----------------------------------------------------------------------------- *)
induction r; first by rewrite big_nil.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 184)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : (forall a : T, a \in r -> P a -> F a <= const) ->
\sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
============================
\sum_(j <- (a :: r) | P j) F j <= const * size [seq j <- a :: r | P j]
----------------------------------------------------------------------------- *)
feed IHr.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 193)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : (forall a : T, a \in r -> P a -> F a <= const) ->
\sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
============================
forall a0 : T, a0 \in r -> P a0 -> F a0 <= const
subgoal 2 (ID 198) is:
\sum_(j <- (a :: r) | P j) F j <= const * size [seq j <- a :: r | P j]
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 193)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : (forall a : T, a \in r -> P a -> F a <= const) ->
\sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
============================
forall a0 : T, a0 \in r -> P a0 -> F a0 <= const
----------------------------------------------------------------------------- *)
intros; apply H.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 202)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : (forall a : T, a \in r -> P a -> F a <= const) ->
\sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
a0 : T
H0 : a0 \in r
H1 : P a0
============================
a0 \in a :: r
subgoal 2 (ID 203) is:
P a0
----------------------------------------------------------------------------- *)
- by rewrite in_cons; apply/orP; right.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 203)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : (forall a : T, a \in r -> P a -> F a <= const) ->
\sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
a0 : T
H0 : a0 \in r
H1 : P a0
============================
P a0
----------------------------------------------------------------------------- *)
- by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 198)
subgoal 1 (ID 198) is:
\sum_(j <- (a :: r) | P j) F j <= const * size [seq j <- a :: r | P j]
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 198)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : \sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
============================
\sum_(j <- (a :: r) | P j) F j <= const * size [seq j <- a :: r | P j]
----------------------------------------------------------------------------- *)
rewrite big_cons.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 245)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : \sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
============================
(if P a then F a + \sum_(j <- r | P j) F j else \sum_(j <- r | P j) F j) <=
const * size [seq j <- a :: r | P j]
----------------------------------------------------------------------------- *)
destruct (P a) eqn:EQ.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 257)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : \sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
EQ : P a = true
============================
F a + \sum_(j <- r | P j) F j <= const * size [seq j <- a :: r | P j]
subgoal 2 (ID 258) is:
\sum_(j <- r | P j) F j <= const * size [seq j <- a :: r | P j]
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 257)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : \sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
EQ : P a = true
============================
F a + \sum_(j <- r | P j) F j <= const * size [seq j <- a :: r | P j]
----------------------------------------------------------------------------- *)
rewrite -cat1s filter_cat size_cat.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 274)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : \sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
EQ : P a = true
============================
F a + \sum_(j <- r | P j) F j <=
const * (size [seq j <- [:: a] | P j] + size [seq j <- r | P j])
----------------------------------------------------------------------------- *)
rewrite mulnDr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 282)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : \sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
EQ : P a = true
============================
F a + \sum_(j <- r | P j) F j <=
const * size [seq j <- [:: a] | P j] + const * size [seq j <- r | P j]
----------------------------------------------------------------------------- *)
apply leq_add; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 283)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : \sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
EQ : P a = true
============================
F a <= const * size [seq j <- [:: a] | P j]
----------------------------------------------------------------------------- *)
rewrite size_filter.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 289)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : \sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
EQ : P a = true
============================
F a <= const * count (fun j : T => P j) [:: a]
----------------------------------------------------------------------------- *)
simpl; rewrite addn0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 298)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : \sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
EQ : P a = true
============================
F a <= const * P a
----------------------------------------------------------------------------- *)
rewrite EQ muln1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 305)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : \sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
EQ : P a = true
============================
F a <= const
----------------------------------------------------------------------------- *)
apply H; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 306)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : \sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
EQ : P a = true
============================
a \in a :: r
----------------------------------------------------------------------------- *)
by rewrite in_cons; apply/orP; left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 258)
subgoal 1 (ID 258) is:
\sum_(j <- r | P j) F j <= const * size [seq j <- a :: r | P j]
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 258)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : \sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
EQ : P a = false
============================
\sum_(j <- r | P j) F j <= const * size [seq j <- a :: r | P j]
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 258)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : \sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
EQ : P a = false
============================
\sum_(j <- r | P j) F j <= const * size [seq j <- a :: r | P j]
----------------------------------------------------------------------------- *)
apply leq_trans with (const × size [seq j <- r | P j]); first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 344)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : \sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
EQ : P a = false
============================
const * size [seq j <- r | P j] <= const * size [seq j <- a :: r | P j]
----------------------------------------------------------------------------- *)
rewrite leq_mul2l; apply/orP; right.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 375)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : \sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
EQ : P a = false
============================
size [seq j <- r | P j] <= size [seq j <- a :: r | P j]
----------------------------------------------------------------------------- *)
rewrite -cat1s filter_cat size_cat.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 391)
T : eqType
a : T
r : seq T
P : pred T
F : T -> nat
const : nat
H : forall a0 : T, a0 \in a :: r -> P a0 -> F a0 <= const
IHr : \sum_(j <- r | P j) F j <= const * size [seq j <- r | P j]
EQ : P a = false
============================
size [seq j <- r | P j] <=
size [seq j <- [:: a] | P j] + size [seq j <- r | P j]
----------------------------------------------------------------------------- *)
by rewrite leq_addl.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 200)
============================
forall (T : eqType) (xs : seq_predType T) (F1 F2 : T -> nat) (P : pred T),
(forall x : T, 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 : T, x \in xs -> P x -> F1 x = F2 x
----------------------------------------------------------------------------- *)
Proof.
intros T xs F1 F2 P H1 H2 x IN PX.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 210)
T : eqType
xs : seq_predType T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in xs -> P x -> F1 x <= F2 x
H2 : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x
x : T
IN : x \in xs
PX : P x
============================
F1 x = F2 x
----------------------------------------------------------------------------- *)
induction xs; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 239)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
H2 : \sum_(x <- (a :: xs) | P x) F1 x = \sum_(x <- (a :: xs) | P x) F2 x
x : T
IN : x \in a :: xs
PX : P x
IHxs : (forall x : T, x \in xs -> P x -> F1 x <= F2 x) ->
\sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
============================
F1 x = F2 x
----------------------------------------------------------------------------- *)
have Fact: \sum_(j <- xs | P j) F1 j ≤ \sum_(j <- xs | P j) F2 j.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 272)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
H2 : \sum_(x <- (a :: xs) | P x) F1 x = \sum_(x <- (a :: xs) | P x) F2 x
x : T
IN : x \in a :: xs
PX : P x
IHxs : (forall x : T, x \in xs -> P x -> F1 x <= F2 x) ->
\sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
============================
\sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
subgoal 2 (ID 274) is:
F1 x = F2 x
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 272)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
H2 : \sum_(x <- (a :: xs) | P x) F1 x = \sum_(x <- (a :: xs) | P x) F2 x
x : T
IN : x \in a :: xs
PX : P x
IHxs : (forall x : T, x \in xs -> P x -> F1 x <= F2 x) ->
\sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
============================
\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 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 311)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
H2 : \sum_(x <- (a :: xs) | P x) F1 x = \sum_(x <- (a :: xs) | P x) F2 x
x : T
IN : x \in a :: xs
PX : P x
IHxs : (forall x : T, x \in xs -> P x -> F1 x <= F2 x) ->
\sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
============================
forall i : T, (i \in xs) && P i -> F1 i <= F2 i
----------------------------------------------------------------------------- *)
move ⇒ y /andP [INy PY].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 378)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
H2 : \sum_(x <- (a :: xs) | P x) F1 x = \sum_(x <- (a :: xs) | P x) F2 x
x : T
IN : x \in a :: xs
PX : P x
IHxs : (forall x : T, x \in xs -> P x -> F1 x <= F2 x) ->
\sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
y : T
INy : y \in xs
PY : P y
============================
F1 y <= F2 y
----------------------------------------------------------------------------- *)
apply: H1; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 392)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H2 : \sum_(x <- (a :: xs) | P x) F1 x = \sum_(x <- (a :: xs) | P x) F2 x
x : T
IN : x \in a :: xs
PX : P x
IHxs : (forall x : T, x \in xs -> P x -> F1 x <= F2 x) ->
\sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
y : T
INy : y \in xs
PY : P y
============================
y \in a :: xs
----------------------------------------------------------------------------- *)
by rewrite in_cons; apply/orP; right.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 274)
subgoal 1 (ID 274) is:
F1 x = F2 x
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 274)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
H2 : \sum_(x <- (a :: xs) | P x) F1 x = \sum_(x <- (a :: xs) | P x) F2 x
x : T
IN : x \in a :: xs
PX : P x
IHxs : (forall x : T, x \in xs -> P x -> F1 x <= F2 x) ->
\sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
============================
F1 x = F2 x
----------------------------------------------------------------------------- *)
feed IHxs.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 426)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
H2 : \sum_(x <- (a :: xs) | P x) F1 x = \sum_(x <- (a :: xs) | P x) F2 x
x : T
IN : x \in a :: xs
PX : P x
IHxs : (forall x : T, x \in xs -> P x -> F1 x <= F2 x) ->
\sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
============================
forall x0 : T, x0 \in xs -> P x0 -> F1 x0 <= F2 x0
subgoal 2 (ID 431) is:
F1 x = F2 x
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 426)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
H2 : \sum_(x <- (a :: xs) | P x) F1 x = \sum_(x <- (a :: xs) | P x) F2 x
x : T
IN : x \in a :: xs
PX : P x
IHxs : (forall x : T, x \in xs -> P x -> F1 x <= F2 x) ->
\sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
============================
forall x0 : T, x0 \in xs -> P x0 -> F1 x0 <= F2 x0
----------------------------------------------------------------------------- *)
intros x' IN' PX'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 434)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
H2 : \sum_(x <- (a :: xs) | P x) F1 x = \sum_(x <- (a :: xs) | P x) F2 x
x : T
IN : x \in a :: xs
PX : P x
IHxs : (forall x : T, x \in xs -> P x -> F1 x <= F2 x) ->
\sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
x' : T
IN' : x' \in xs
PX' : P x'
============================
F1 x' <= F2 x'
----------------------------------------------------------------------------- *)
apply H1; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 435)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
H2 : \sum_(x <- (a :: xs) | P x) F1 x = \sum_(x <- (a :: xs) | P x) F2 x
x : T
IN : x \in a :: xs
PX : P x
IHxs : (forall x : T, x \in xs -> P x -> F1 x <= F2 x) ->
\sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
x' : T
IN' : x' \in xs
PX' : P x'
============================
x' \in a :: xs
----------------------------------------------------------------------------- *)
by rewrite in_cons; apply/orP; right.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 431)
subgoal 1 (ID 431) is:
F1 x = F2 x
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 431)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
H2 : \sum_(x <- (a :: xs) | P x) F1 x = \sum_(x <- (a :: xs) | P x) F2 x
x : T
IN : x \in a :: xs
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
============================
F1 x = F2 x
----------------------------------------------------------------------------- *)
rewrite big_cons [RHS]big_cons in H2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 516)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
x : T
IN : x \in a :: xs
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
H2 : (if P a
then F1 a + \sum_(j <- xs | P j) F1 j
else \sum_(j <- xs | P j) F1 j) =
(if P a
then F2 a + \sum_(j <- xs | P j) F2 j
else \sum_(j <- xs | P j) F2 j)
============================
F1 x = F2 x
----------------------------------------------------------------------------- *)
have EqLeq: ∀ a b c d, a + b = c + d → a ≤ c → b ≥ d.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 523)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
x : T
IN : x \in a :: xs
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
H2 : (if P a
then F1 a + \sum_(j <- xs | P j) F1 j
else \sum_(j <- xs | P j) F1 j) =
(if P a
then F2 a + \sum_(j <- xs | P j) F2 j
else \sum_(j <- xs | P j) F2 j)
============================
forall a0 b c d : nat, a0 + b = c + d -> a0 <= c -> d <= b
subgoal 2 (ID 525) is:
F1 x = F2 x
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 523)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
x : T
IN : x \in a :: xs
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
H2 : (if P a
then F1 a + \sum_(j <- xs | P j) F1 j
else \sum_(j <- xs | P j) F1 j) =
(if P a
then F2 a + \sum_(j <- xs | P j) F2 j
else \sum_(j <- xs | P j) F2 j)
============================
forall a0 b c d : nat, a0 + b = c + d -> a0 <= c -> d <= b
----------------------------------------------------------------------------- *)
clear; intros; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 525)
subgoal 1 (ID 525) is:
F1 x = F2 x
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 525)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
x : T
IN : x \in a :: xs
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
H2 : (if P a
then F1 a + \sum_(j <- xs | P j) F1 j
else \sum_(j <- xs | P j) F1 j) =
(if P a
then F2 a + \sum_(j <- xs | P j) F2 j
else \sum_(j <- xs | P j) F2 j)
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
============================
F1 x = F2 x
----------------------------------------------------------------------------- *)
move: IN; rewrite in_cons; move ⇒ /orP [/eqP EQ | IN].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 788)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
x : T
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
H2 : (if P a
then F1 a + \sum_(j <- xs | P j) F1 j
else \sum_(j <- xs | P j) F1 j) =
(if P a
then F2 a + \sum_(j <- xs | P j) F2 j
else \sum_(j <- xs | P j) F2 j)
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
EQ : x = a
============================
F1 x = F2 x
subgoal 2 (ID 789) is:
F1 x = F2 x
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 788)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
x : T
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
H2 : (if P a
then F1 a + \sum_(j <- xs | P j) F1 j
else \sum_(j <- xs | P j) F1 j) =
(if P a
then F2 a + \sum_(j <- xs | P j) F2 j
else \sum_(j <- xs | P j) F2 j)
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
EQ : x = a
============================
F1 x = F2 x
----------------------------------------------------------------------------- *)
subst a.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 797)
T : eqType
xs : seq T
F1, F2 : T -> nat
P : pred T
x : T
H1 : forall x0 : T, x0 \in x :: xs -> P x0 -> F1 x0 <= F2 x0
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
H2 : (if P x
then F1 x + \sum_(j <- xs | P j) F1 j
else \sum_(j <- xs | P j) F1 j) =
(if P x
then F2 x + \sum_(j <- xs | P j) F2 j
else \sum_(j <- xs | P j) F2 j)
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
============================
F1 x = F2 x
----------------------------------------------------------------------------- *)
rewrite PX in H2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 818)
T : eqType
xs : seq T
F1, F2 : T -> nat
P : pred T
x : T
H1 : forall x0 : T, x0 \in x :: xs -> P x0 -> F1 x0 <= F2 x0
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
H2 : F1 x + \sum_(j <- xs | P j) F1 j = F2 x + \sum_(j <- xs | P j) F2 j
============================
F1 x = F2 x
----------------------------------------------------------------------------- *)
specialize (H1 x).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 820)
T : eqType
xs : seq T
F1, F2 : T -> nat
P : pred T
x : T
H1 : x \in x :: xs -> P x -> F1 x <= F2 x
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
H2 : F1 x + \sum_(j <- xs | P j) F1 j = F2 x + \sum_(j <- xs | P j) F2 j
============================
F1 x = F2 x
----------------------------------------------------------------------------- *)
feed_n 2 H1; [ by rewrite in_cons; apply/orP; left | by done | ].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 832)
T : eqType
xs : seq T
F1, F2 : T -> nat
P : pred T
x : T
H1 : F1 x <= F2 x
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
H2 : F1 x + \sum_(j <- xs | P j) F1 j = F2 x + \sum_(j <- xs | P j) F2 j
============================
F1 x = F2 x
----------------------------------------------------------------------------- *)
move: (EqLeq
(F1 x) (\sum_(j <- xs | P j) F1 j)
(F2 x) (\sum_(j <- xs | P j) F2 j) H2 H1) ⇒ Q.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 876)
T : eqType
xs : seq T
F1, F2 : T -> nat
P : pred T
x : T
H1 : F1 x <= F2 x
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
H2 : F1 x + \sum_(j <- xs | P j) F1 j = F2 x + \sum_(j <- xs | P j) F2 j
Q : \sum_(j <- xs | P j) F2 j <= \sum_(j <- xs | P j) F1 j
============================
F1 x = F2 x
----------------------------------------------------------------------------- *)
have EQ: \sum_(j <- xs | P j) F1 j = \sum_(j <- xs | P j) F2 j.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 889)
T : eqType
xs : seq T
F1, F2 : T -> nat
P : pred T
x : T
H1 : F1 x <= F2 x
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
H2 : F1 x + \sum_(j <- xs | P j) F1 j = F2 x + \sum_(j <- xs | P j) F2 j
Q : \sum_(j <- xs | P j) F2 j <= \sum_(j <- xs | P j) F1 j
============================
\sum_(j <- xs | P j) F1 j = \sum_(j <- xs | P j) F2 j
subgoal 2 (ID 891) is:
F1 x = F2 x
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 889)
T : eqType
xs : seq T
F1, F2 : T -> nat
P : pred T
x : T
H1 : F1 x <= F2 x
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
H2 : F1 x + \sum_(j <- xs | P j) F1 j = F2 x + \sum_(j <- xs | P j) F2 j
Q : \sum_(j <- xs | P j) F2 j <= \sum_(j <- xs | P j) F1 j
============================
\sum_(j <- xs | P j) F1 j = \sum_(j <- xs | P j) F2 j
----------------------------------------------------------------------------- *)
by apply/eqP; rewrite eqn_leq; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 891)
subgoal 1 (ID 891) is:
F1 x = F2 x
subgoal 2 (ID 789) is:
F1 x = F2 x
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 891)
T : eqType
xs : seq T
F1, F2 : T -> nat
P : pred T
x : T
H1 : F1 x <= F2 x
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
H2 : F1 x + \sum_(j <- xs | P j) F1 j = F2 x + \sum_(j <- xs | P j) F2 j
Q : \sum_(j <- xs | P j) F2 j <= \sum_(j <- xs | P j) F1 j
EQ : \sum_(j <- xs | P j) F1 j = \sum_(j <- xs | P j) F2 j
============================
F1 x = F2 x
----------------------------------------------------------------------------- *)
by move: H2 ⇒ /eqP; rewrite EQ eqn_add2r; move ⇒ /eqP EQ'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 789)
subgoal 1 (ID 789) is:
F1 x = F2 x
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 789)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
x : T
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
H2 : (if P a
then F1 a + \sum_(j <- xs | P j) F1 j
else \sum_(j <- xs | P j) F1 j) =
(if P a
then F2 a + \sum_(j <- xs | P j) F2 j
else \sum_(j <- xs | P j) F2 j)
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
IN : x \in xs
============================
F1 x = F2 x
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 789)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
x : T
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
H2 : (if P a
then F1 a + \sum_(j <- xs | P j) F1 j
else \sum_(j <- xs | P j) F1 j) =
(if P a
then F2 a + \sum_(j <- xs | P j) F2 j
else \sum_(j <- xs | P j) F2 j)
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
IN : x \in xs
============================
F1 x = F2 x
----------------------------------------------------------------------------- *)
destruct (P a) eqn:PA; last by apply IHxs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1099)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
x : T
PX : P x
IHxs : \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
x \in xs -> F1 x = F2 x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
PA : P a = true
H2 : F1 a + \sum_(j <- xs | P j) F1 j = F2 a + \sum_(j <- xs | P j) F2 j
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
IN : x \in xs
============================
F1 x = F2 x
----------------------------------------------------------------------------- *)
apply: IHxs; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1115)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : forall x : T, x \in a :: xs -> P x -> F1 x <= F2 x
x : T
PX : P x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
PA : P a = true
H2 : F1 a + \sum_(j <- xs | P j) F1 j = F2 a + \sum_(j <- xs | P j) F2 j
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
IN : x \in xs
============================
\sum_(x0 <- xs | P x0) F1 x0 = \sum_(x0 <- xs | P x0) F2 x0
----------------------------------------------------------------------------- *)
specialize (H1 a).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1118)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : a \in a :: xs -> P a -> F1 a <= F2 a
x : T
PX : P x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
PA : P a = true
H2 : F1 a + \sum_(j <- xs | P j) F1 j = F2 a + \sum_(j <- xs | P j) F2 j
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
IN : x \in xs
============================
\sum_(x0 <- xs | P x0) F1 x0 = \sum_(x0 <- xs | P x0) F2 x0
----------------------------------------------------------------------------- *)
feed_n 2 (H1); [ by rewrite in_cons; apply/orP; left | by done | ].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1130)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : F1 a <= F2 a
x : T
PX : P x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
PA : P a = true
H2 : F1 a + \sum_(j <- xs | P j) F1 j = F2 a + \sum_(j <- xs | P j) F2 j
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
IN : x \in xs
============================
\sum_(x0 <- xs | P x0) F1 x0 = \sum_(x0 <- xs | P x0) F2 x0
----------------------------------------------------------------------------- *)
move: (EqLeq
(F1 a) (\sum_(j <- xs | P j) F1 j)
(F2 a) (\sum_(j <- xs | P j) F2 j) H2 H1) ⇒ Q.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1174)
T : eqType
a : T
xs : seq T
F1, F2 : T -> nat
P : pred T
H1 : F1 a <= F2 a
x : T
PX : P x
Fact : \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j
PA : P a = true
H2 : F1 a + \sum_(j <- xs | P j) F1 j = F2 a + \sum_(j <- xs | P j) F2 j
EqLeq : forall a b c d : nat, a + b = c + d -> a <= c -> d <= b
IN : x \in xs
Q : \sum_(j <- xs | P j) F2 j <= \sum_(j <- xs | P j) F1 j
============================
\sum_(x0 <- xs | P x0) F1 x0 = \sum_(x0 <- xs | P x0) F2 x0
----------------------------------------------------------------------------- *)
by apply/eqP; rewrite eqn_leq; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(* We prove that the sum of Δ ones is equal to Δ. *)
Lemma sum_of_ones:
∀ t Δ,
\sum_(t ≤ x < t + Δ) 1 = Δ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 209)
============================
forall t Δ : nat, \sum_(t <= x < t + Δ) 1 = Δ
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 211)
t, Δ : nat
============================
\sum_(t <= x < t + Δ) 1 = Δ
----------------------------------------------------------------------------- *)
rewrite big_const_nat iter_addn_0 mul1n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 228)
t, Δ : nat
============================
t + Δ - t = Δ
----------------------------------------------------------------------------- *)
rewrite addnC -addnBA; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 240)
t, Δ : nat
============================
Δ + (t - t) = Δ
----------------------------------------------------------------------------- *)
by rewrite subnn addn0.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 223)
============================
forall (f : nat -> nat) (t Δ : nat),
\sum_(t <= x < t + Δ) f x < Δ -> exists x : nat, t <= x < t + Δ /\ f x = 0
----------------------------------------------------------------------------- *)
Proof.
induction Δ; intros; first by rewrite ltn0 in H.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 235)
f : nat -> nat
t, Δ : nat
IHΔ : \sum_(t <= x < t + Δ) f x < Δ ->
exists x : nat, t <= x < t + Δ /\ f x = 0
H : \sum_(t <= x < t + Δ.+1) f x < Δ.+1
============================
exists x : nat, t <= x < t + Δ.+1 /\ f x = 0
----------------------------------------------------------------------------- *)
destruct (f (t + Δ)) eqn: EQ.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 285)
f : nat -> nat
t, Δ : nat
IHΔ : \sum_(t <= x < t + Δ) f x < Δ ->
exists x : nat, t <= x < t + Δ /\ f x = 0
H : \sum_(t <= x < t + Δ.+1) f x < Δ.+1
EQ : f (t + Δ) = 0
============================
exists x : nat, t <= x < t + Δ.+1 /\ f x = 0
subgoal 2 (ID 287) is:
exists x : nat, t <= x < t + Δ.+1 /\ f x = 0
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 285)
f : nat -> nat
t, Δ : nat
IHΔ : \sum_(t <= x < t + Δ) f x < Δ ->
exists x : nat, t <= x < t + Δ /\ f x = 0
H : \sum_(t <= x < t + Δ.+1) f x < Δ.+1
EQ : f (t + Δ) = 0
============================
exists x : nat, t <= x < t + Δ.+1 /\ f x = 0
----------------------------------------------------------------------------- *)
∃ (t + Δ); split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 291)
f : nat -> nat
t, Δ : nat
IHΔ : \sum_(t <= x < t + Δ) f x < Δ ->
exists x : nat, t <= x < t + Δ /\ f x = 0
H : \sum_(t <= x < t + Δ.+1) f x < Δ.+1
EQ : f (t + Δ) = 0
============================
t <= t + Δ < t + Δ.+1
----------------------------------------------------------------------------- *)
by apply/andP; split; [rewrite leq_addr | rewrite addnS ltnS].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 287)
subgoal 1 (ID 287) is:
exists x : nat, t <= x < t + Δ.+1 /\ f x = 0
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 287)
f : nat -> nat
t, Δ : nat
IHΔ : \sum_(t <= x < t + Δ) f x < Δ ->
exists x : nat, t <= x < t + Δ /\ f x = 0
H : \sum_(t <= x < t + Δ.+1) f x < Δ.+1
n : nat
EQ : f (t + Δ) = n.+1
============================
exists x : nat, t <= x < t + Δ.+1 /\ f x = 0
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 287)
f : nat -> nat
t, Δ : nat
IHΔ : \sum_(t <= x < t + Δ) f x < Δ ->
exists x : nat, t <= x < t + Δ /\ f x = 0
H : \sum_(t <= x < t + Δ.+1) f x < Δ.+1
n : nat
EQ : f (t + Δ) = n.+1
============================
exists x : nat, t <= x < t + Δ.+1 /\ f x = 0
----------------------------------------------------------------------------- *)
move: H; rewrite addnS big_nat_recr //= ?leq_addr // EQ addnS ltnS; move ⇒ H.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 448)
f : nat -> nat
t, Δ : nat
IHΔ : \sum_(t <= x < t + Δ) f x < Δ ->
exists x : nat, t <= x < t + Δ /\ f x = 0
n : nat
EQ : f (t + Δ) = n.+1
H : \sum_(t <= i < t + Δ) f i + n < Δ
============================
exists x : nat, t <= x < (t + Δ).+1 /\ f x = 0
----------------------------------------------------------------------------- *)
feed IHΔ.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 449)
f : nat -> nat
t, Δ : nat
IHΔ : \sum_(t <= x < t + Δ) f x < Δ ->
exists x : nat, t <= x < t + Δ /\ f x = 0
n : nat
EQ : f (t + Δ) = n.+1
H : \sum_(t <= i < t + Δ) f i + n < Δ
============================
\sum_(t <= x < t + Δ) f x < Δ
subgoal 2 (ID 454) is:
exists x : nat, t <= x < (t + Δ).+1 /\ f x = 0
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 449)
f : nat -> nat
t, Δ : nat
IHΔ : \sum_(t <= x < t + Δ) f x < Δ ->
exists x : nat, t <= x < t + Δ /\ f x = 0
n : nat
EQ : f (t + Δ) = n.+1
H : \sum_(t <= i < t + Δ) f i + n < Δ
============================
\sum_(t <= x < t + Δ) f x < Δ
----------------------------------------------------------------------------- *)
by apply leq_ltn_trans with (\sum_(t ≤ i < t + Δ) f i + n); first rewrite leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 454)
subgoal 1 (ID 454) is:
exists x : nat, t <= x < (t + Δ).+1 /\ f x = 0
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 454)
f : nat -> nat
t, Δ : nat
IHΔ : exists x : nat, t <= x < t + Δ /\ f x = 0
n : nat
EQ : f (t + Δ) = n.+1
H : \sum_(t <= i < t + Δ) f i + n < Δ
============================
exists x : nat, t <= x < (t + Δ).+1 /\ f x = 0
----------------------------------------------------------------------------- *)
move: IHΔ ⇒ [z [/andP [LE GE] ZERO]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 526)
f : nat -> nat
t, Δ, n : nat
EQ : f (t + Δ) = n.+1
H : \sum_(t <= i < t + Δ) f i + n < Δ
z : nat
LE : t <= z
GE : z < t + Δ
ZERO : f z = 0
============================
exists x : nat, t <= x < (t + Δ).+1 /\ f x = 0
----------------------------------------------------------------------------- *)
∃ z; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 530)
f : nat -> nat
t, Δ, n : nat
EQ : f (t + Δ) = n.+1
H : \sum_(t <= i < t + Δ) f i + n < Δ
z : nat
LE : t <= z
GE : z < t + Δ
ZERO : f z = 0
============================
t <= z < (t + Δ).+1
----------------------------------------------------------------------------- *)
apply/andP; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 558)
f : nat -> nat
t, Δ, n : nat
EQ : f (t + Δ) = n.+1
H : \sum_(t <= i < t + Δ) f i + n < Δ
z : nat
LE : t <= z
GE : z < t + Δ
ZERO : f z = 0
============================
z < (t + Δ).+1
----------------------------------------------------------------------------- *)
by rewrite ltnS ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 240)
============================
forall (t1 t2 d : nat) (F1 F2 : nat -> nat),
(forall g : nat, g < d -> F1 (t1 + g) = F2 (t2 + g)) ->
\sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
----------------------------------------------------------------------------- *)
Proof.
intros × P.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 246)
t1, t2, d : nat
F1, F2 : nat -> nat
P : forall g : nat, g < d -> F1 (t1 + g) = F2 (t2 + g)
============================
\sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
----------------------------------------------------------------------------- *)
induction d.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 255)
t1, t2 : nat
F1, F2 : nat -> nat
P : forall g : nat, g < 0 -> F1 (t1 + g) = F2 (t2 + g)
============================
\sum_(t1 <= t < t1 + 0) F1 t = \sum_(t2 <= t < t2 + 0) F2 t
subgoal 2 (ID 260) is:
\sum_(t1 <= t < t1 + d.+1) F1 t = \sum_(t2 <= t < t2 + d.+1) F2 t
----------------------------------------------------------------------------- *)
now rewrite !addn0 !big_geq ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 260)
t1, t2, d : nat
F1, F2 : nat -> nat
P : forall g : nat, g < d.+1 -> F1 (t1 + g) = F2 (t2 + g)
IHd : (forall g : nat, g < d -> F1 (t1 + g) = F2 (t2 + g)) ->
\sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
============================
\sum_(t1 <= t < t1 + d.+1) F1 t = \sum_(t2 <= t < t2 + d.+1) F2 t
----------------------------------------------------------------------------- *)
feed_n 1 IHd.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 320)
t1, t2, d : nat
F1, F2 : nat -> nat
P : forall g : nat, g < d.+1 -> F1 (t1 + g) = F2 (t2 + g)
IHd : (forall g : nat, g < d -> F1 (t1 + g) = F2 (t2 + g)) ->
\sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
============================
forall g : nat, g < d -> F1 (t1 + g) = F2 (t2 + g)
subgoal 2 (ID 325) is:
\sum_(t1 <= t < t1 + d.+1) F1 t = \sum_(t2 <= t < t2 + d.+1) F2 t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 320)
t1, t2, d : nat
F1, F2 : nat -> nat
P : forall g : nat, g < d.+1 -> F1 (t1 + g) = F2 (t2 + g)
IHd : (forall g : nat, g < d -> F1 (t1 + g) = F2 (t2 + g)) ->
\sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
============================
forall g : nat, g < d -> F1 (t1 + g) = F2 (t2 + g)
----------------------------------------------------------------------------- *)
intros g G_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 327)
t1, t2, d : nat
F1, F2 : nat -> nat
P : forall g : nat, g < d.+1 -> F1 (t1 + g) = F2 (t2 + g)
IHd : (forall g : nat, g < d -> F1 (t1 + g) = F2 (t2 + g)) ->
\sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
g : nat
G_LT : g < d
============================
F1 (t1 + g) = F2 (t2 + g)
----------------------------------------------------------------------------- *)
now specialize (P g); feed_n 1 P; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 325)
subgoal 1 (ID 325) is:
\sum_(t1 <= t < t1 + d.+1) F1 t = \sum_(t2 <= t < t2 + d.+1) F2 t
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 325)
t1, t2, d : nat
F1, F2 : nat -> nat
P : forall g : nat, g < d.+1 -> F1 (t1 + g) = F2 (t2 + g)
IHd : \sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
============================
\sum_(t1 <= t < t1 + d.+1) F1 t = \sum_(t2 <= t < t2 + d.+1) F2 t
----------------------------------------------------------------------------- *)
rewrite !addnS !big_nat_recr ⇒ //; try by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1396)
t1, t2, d : nat
F1, F2 : nat -> nat
P : forall g : nat, g < d.+1 -> F1 (t1 + g) = F2 (t2 + g)
IHd : \sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
============================
addn_monoid (\big[addn_monoid/0]_(t1 <= i < t1 + d) F1 i) (F1 (t1 + d)) =
addn_monoid (\big[addn_monoid/0]_(t2 <= i < t2 + d) F2 i) (F2 (t2 + d))
----------------------------------------------------------------------------- *)
rewrite IHd.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1851)
t1, t2, d : nat
F1, F2 : nat -> nat
P : forall g : nat, g < d.+1 -> F1 (t1 + g) = F2 (t2 + g)
IHd : \sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
============================
addn_monoid (\sum_(t2 <= t < t2 + d) F2 t) (F1 (t1 + d)) =
addn_monoid (\big[addn_monoid/0]_(t2 <= i < t2 + d) F2 i) (F2 (t2 + d))
----------------------------------------------------------------------------- *)
specialize (P d); feed_n 1 P.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1854)
t1, t2, d : nat
F1, F2 : nat -> nat
P : d < d.+1 -> F1 (t1 + d) = F2 (t2 + d)
IHd : \sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
============================
d < d.+1
subgoal 2 (ID 1859) is:
addn_monoid (\sum_(t2 <= t < t2 + d) F2 t) (F1 (t1 + d)) =
addn_monoid (\big[addn_monoid/0]_(t2 <= i < t2 + d) F2 i) (F2 (t2 + d))
----------------------------------------------------------------------------- *)
ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1859)
t1, t2, d : nat
F1, F2 : nat -> nat
P : F1 (t1 + d) = F2 (t2 + d)
IHd : \sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
============================
addn_monoid (\sum_(t2 <= t < t2 + d) F2 t) (F1 (t1 + d)) =
addn_monoid (\big[addn_monoid/0]_(t2 <= i < t2 + d) F2 i) (F2 (t2 + d))
----------------------------------------------------------------------------- *)
now rewrite P.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 39)
============================
forall (T : eqType) (rs : seq T) (F G : T -> nat),
(forall 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 44)
T : eqType
rs : seq T
F, G : T -> nat
H : forall 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
----------------------------------------------------------------------------- *)
induction rs; first by rewrite !big_nil subn0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 60)
T : eqType
a : T
rs : seq T
F, G : T -> nat
H : forall i : T, i \in a :: rs -> G i <= F i
IHrs : (forall 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
============================
\sum_(i <- (a :: rs)) (F i - G i) =
\sum_(i <- (a :: rs)) F i - \sum_(i <- (a :: rs)) G i
----------------------------------------------------------------------------- *)
rewrite !big_cons subh2.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 141)
T : eqType
a : T
rs : seq T
F, G : T -> nat
H : forall i : T, i \in a :: rs -> G i <= F i
IHrs : (forall 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
============================
F a - G a + \sum_(j <- rs) (F j - G j) =
F a - G a + (\sum_(j <- rs) F j - \sum_(j <- rs) G j)
subgoal 2 (ID 142) is:
G a <= F a
subgoal 3 (ID 143) is:
\sum_(j <- rs) G j <= \sum_(j <- rs) F j
----------------------------------------------------------------------------- *)
- apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHrs.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 232)
T : eqType
a : T
rs : seq T
F, G : T -> nat
H : forall i : T, i \in a :: rs -> G i <= F i
IHrs : (forall 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
============================
forall i : T, i \in rs -> G i <= F i
subgoal 2 (ID 142) is:
G a <= F a
subgoal 3 (ID 143) is:
\sum_(j <- rs) G j <= \sum_(j <- rs) F j
----------------------------------------------------------------------------- *)
by intros; apply H; rewrite in_cons; apply/orP; right.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 142)
T : eqType
a : T
rs : seq T
F, G : T -> nat
H : forall i : T, i \in a :: rs -> G i <= F i
IHrs : (forall 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
============================
G a <= F a
subgoal 2 (ID 143) is:
\sum_(j <- rs) G j <= \sum_(j <- rs) F j
----------------------------------------------------------------------------- *)
- by apply H; rewrite in_cons; apply/orP; left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 143)
T : eqType
a : T
rs : seq T
F, G : T -> nat
H : forall i : T, i \in a :: rs -> G i <= F i
IHrs : (forall 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
============================
\sum_(j <- rs) G j <= \sum_(j <- rs) F j
----------------------------------------------------------------------------- *)
- rewrite big_seq_cond [in X in _ ≤ X]big_seq_cond.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 323)
T : eqType
a : T
rs : seq T
F, G : T -> nat
H : forall i : T, i \in a :: rs -> G i <= F i
IHrs : (forall 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
============================
\sum_(i <- rs | (i \in rs) && true) G i <=
\sum_(i <- rs | (i \in rs) && true) F i
----------------------------------------------------------------------------- *)
rewrite leq_sum //; move ⇒ i /andP [IN _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 399)
T : eqType
a : T
rs : seq T
F, G : T -> nat
H : forall i : T, i \in a :: rs -> G i <= F i
IHrs : (forall 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
i : T
IN : i \in rs
============================
G i <= F i
----------------------------------------------------------------------------- *)
by apply H; rewrite in_cons; apply/orP; right.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 62)
============================
forall (n : nat) (F G : nat -> nat),
(forall i : nat, i < n -> G i <= F 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 66)
n : nat
F, G : nat -> nat
ALL : forall i : nat, i < n -> G i <= F i
============================
\sum_(0 <= i < n) (F i - G i) =
\sum_(0 <= i < n) F i - \sum_(0 <= i < n) G i
----------------------------------------------------------------------------- *)
rewrite sum_seq_diff; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 74)
n : nat
F, G : nat -> nat
ALL : forall i : nat, i < n -> G i <= F i
============================
forall i : nat_eqType, i \in index_iota 0 n -> G i <= F i
----------------------------------------------------------------------------- *)
move ⇒ i; rewrite mem_index_iota; move ⇒ /andP [_ LT].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 120)
n : nat
F, G : nat -> nat
ALL : forall i : nat, i < n -> G i <= F i
i : nat_eqType
LT : i < n
============================
G i <= F i
----------------------------------------------------------------------------- *)
by apply ALL.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 80)
============================
forall (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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 84)
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
----------------------------------------------------------------------------- *)
induction rs; first by rewrite !big_nil subn0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 94)
T : eqType
a : T
rs : seq T
P : T -> bool
F : T -> nat
IHrs : \sum_(r <- rs | P r) F r =
\sum_(r <- rs) F r - \sum_(r <- rs | ~~ P r) F r
============================
\sum_(r <- (a :: rs) | P r) F r =
\sum_(r <- (a :: rs)) F r - \sum_(r <- (a :: rs) | ~~ P r) F r
----------------------------------------------------------------------------- *)
rewrite !big_cons !IHrs; clear IHrs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 170)
T : eqType
a : T
rs : seq T
P : T -> bool
F : T -> nat
============================
(if P a
then F a + (\sum_(r <- rs) F r - \sum_(r <- rs | ~~ P r) F r)
else \sum_(r <- rs) F r - \sum_(r <- rs | ~~ P r) F r) =
F a + \sum_(j <- rs) F j -
(if ~~ P a
then F a + \sum_(j <- rs | ~~ P j) F j
else \sum_(j <- rs | ~~ P j) F j)
----------------------------------------------------------------------------- *)
case (P a); simpl; last by rewrite subnDl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 174)
T : eqType
a : T
rs : seq T
P : T -> bool
F : T -> nat
============================
F a + (\sum_(r <- rs) F r - \sum_(r <- rs | ~~ P r) F r) =
F a + \sum_(j <- rs) F j - \sum_(j <- rs | ~~ P j) F j
----------------------------------------------------------------------------- *)
rewrite addnBA; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 188)
T : eqType
a : T
rs : seq T
P : T -> bool
F : T -> nat
============================
\sum_(r <- rs | ~~ P r) F r <= \sum_(r <- rs) F r
----------------------------------------------------------------------------- *)
rewrite big_mkcond leq_sum //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 206)
T : eqType
a : T
rs : seq T
P : T -> bool
F : T -> nat
============================
forall i : T, true -> (if ~~ P i then F i else 0) <= F i
----------------------------------------------------------------------------- *)
intros t _.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 235)
T : eqType
a : T
rs : seq T
P : T -> bool
F : T -> nat
t : T
============================
(if ~~ P t then F t else 0) <= F t
----------------------------------------------------------------------------- *)
by case (P t).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 240)
============================
forall (t1 t2 d : nat) (F1 F2 : nat -> nat),
(forall g : nat, g < d -> F1 (t1 + g) = F2 (t2 + g)) ->
\sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
----------------------------------------------------------------------------- *)
Proof.
intros × P.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 246)
t1, t2, d : nat
F1, F2 : nat -> nat
P : forall g : nat, g < d -> F1 (t1 + g) = F2 (t2 + g)
============================
\sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
----------------------------------------------------------------------------- *)
induction d.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 255)
t1, t2 : nat
F1, F2 : nat -> nat
P : forall g : nat, g < 0 -> F1 (t1 + g) = F2 (t2 + g)
============================
\sum_(t1 <= t < t1 + 0) F1 t = \sum_(t2 <= t < t2 + 0) F2 t
subgoal 2 (ID 260) is:
\sum_(t1 <= t < t1 + d.+1) F1 t = \sum_(t2 <= t < t2 + d.+1) F2 t
----------------------------------------------------------------------------- *)
now rewrite !addn0 !big_geq ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 260)
t1, t2, d : nat
F1, F2 : nat -> nat
P : forall g : nat, g < d.+1 -> F1 (t1 + g) = F2 (t2 + g)
IHd : (forall g : nat, g < d -> F1 (t1 + g) = F2 (t2 + g)) ->
\sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
============================
\sum_(t1 <= t < t1 + d.+1) F1 t = \sum_(t2 <= t < t2 + d.+1) F2 t
----------------------------------------------------------------------------- *)
feed_n 1 IHd.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 320)
t1, t2, d : nat
F1, F2 : nat -> nat
P : forall g : nat, g < d.+1 -> F1 (t1 + g) = F2 (t2 + g)
IHd : (forall g : nat, g < d -> F1 (t1 + g) = F2 (t2 + g)) ->
\sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
============================
forall g : nat, g < d -> F1 (t1 + g) = F2 (t2 + g)
subgoal 2 (ID 325) is:
\sum_(t1 <= t < t1 + d.+1) F1 t = \sum_(t2 <= t < t2 + d.+1) F2 t
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 320)
t1, t2, d : nat
F1, F2 : nat -> nat
P : forall g : nat, g < d.+1 -> F1 (t1 + g) = F2 (t2 + g)
IHd : (forall g : nat, g < d -> F1 (t1 + g) = F2 (t2 + g)) ->
\sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
============================
forall g : nat, g < d -> F1 (t1 + g) = F2 (t2 + g)
----------------------------------------------------------------------------- *)
intros g G_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 327)
t1, t2, d : nat
F1, F2 : nat -> nat
P : forall g : nat, g < d.+1 -> F1 (t1 + g) = F2 (t2 + g)
IHd : (forall g : nat, g < d -> F1 (t1 + g) = F2 (t2 + g)) ->
\sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
g : nat
G_LT : g < d
============================
F1 (t1 + g) = F2 (t2 + g)
----------------------------------------------------------------------------- *)
now specialize (P g); feed_n 1 P; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 325)
subgoal 1 (ID 325) is:
\sum_(t1 <= t < t1 + d.+1) F1 t = \sum_(t2 <= t < t2 + d.+1) F2 t
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 325)
t1, t2, d : nat
F1, F2 : nat -> nat
P : forall g : nat, g < d.+1 -> F1 (t1 + g) = F2 (t2 + g)
IHd : \sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
============================
\sum_(t1 <= t < t1 + d.+1) F1 t = \sum_(t2 <= t < t2 + d.+1) F2 t
----------------------------------------------------------------------------- *)
rewrite !addnS !big_nat_recr ⇒ //; try by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1396)
t1, t2, d : nat
F1, F2 : nat -> nat
P : forall g : nat, g < d.+1 -> F1 (t1 + g) = F2 (t2 + g)
IHd : \sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
============================
addn_monoid (\big[addn_monoid/0]_(t1 <= i < t1 + d) F1 i) (F1 (t1 + d)) =
addn_monoid (\big[addn_monoid/0]_(t2 <= i < t2 + d) F2 i) (F2 (t2 + d))
----------------------------------------------------------------------------- *)
rewrite IHd.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1851)
t1, t2, d : nat
F1, F2 : nat -> nat
P : forall g : nat, g < d.+1 -> F1 (t1 + g) = F2 (t2 + g)
IHd : \sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
============================
addn_monoid (\sum_(t2 <= t < t2 + d) F2 t) (F1 (t1 + d)) =
addn_monoid (\big[addn_monoid/0]_(t2 <= i < t2 + d) F2 i) (F2 (t2 + d))
----------------------------------------------------------------------------- *)
specialize (P d); feed_n 1 P.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1854)
t1, t2, d : nat
F1, F2 : nat -> nat
P : d < d.+1 -> F1 (t1 + d) = F2 (t2 + d)
IHd : \sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
============================
d < d.+1
subgoal 2 (ID 1859) is:
addn_monoid (\sum_(t2 <= t < t2 + d) F2 t) (F1 (t1 + d)) =
addn_monoid (\big[addn_monoid/0]_(t2 <= i < t2 + d) F2 i) (F2 (t2 + d))
----------------------------------------------------------------------------- *)
ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1859)
t1, t2, d : nat
F1, F2 : nat -> nat
P : F1 (t1 + d) = F2 (t2 + d)
IHd : \sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t
============================
addn_monoid (\sum_(t2 <= t < t2 + d) F2 t) (F1 (t1 + d)) =
addn_monoid (\big[addn_monoid/0]_(t2 <= i < t2 + d) F2 i) (F2 (t2 + d))
----------------------------------------------------------------------------- *)
now rewrite P.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 39)
============================
forall (T : eqType) (rs : seq T) (F G : T -> nat),
(forall 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 44)
T : eqType
rs : seq T
F, G : T -> nat
H : forall 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
----------------------------------------------------------------------------- *)
induction rs; first by rewrite !big_nil subn0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 60)
T : eqType
a : T
rs : seq T
F, G : T -> nat
H : forall i : T, i \in a :: rs -> G i <= F i
IHrs : (forall 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
============================
\sum_(i <- (a :: rs)) (F i - G i) =
\sum_(i <- (a :: rs)) F i - \sum_(i <- (a :: rs)) G i
----------------------------------------------------------------------------- *)
rewrite !big_cons subh2.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 141)
T : eqType
a : T
rs : seq T
F, G : T -> nat
H : forall i : T, i \in a :: rs -> G i <= F i
IHrs : (forall 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
============================
F a - G a + \sum_(j <- rs) (F j - G j) =
F a - G a + (\sum_(j <- rs) F j - \sum_(j <- rs) G j)
subgoal 2 (ID 142) is:
G a <= F a
subgoal 3 (ID 143) is:
\sum_(j <- rs) G j <= \sum_(j <- rs) F j
----------------------------------------------------------------------------- *)
- apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHrs.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 232)
T : eqType
a : T
rs : seq T
F, G : T -> nat
H : forall i : T, i \in a :: rs -> G i <= F i
IHrs : (forall 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
============================
forall i : T, i \in rs -> G i <= F i
subgoal 2 (ID 142) is:
G a <= F a
subgoal 3 (ID 143) is:
\sum_(j <- rs) G j <= \sum_(j <- rs) F j
----------------------------------------------------------------------------- *)
by intros; apply H; rewrite in_cons; apply/orP; right.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 142)
T : eqType
a : T
rs : seq T
F, G : T -> nat
H : forall i : T, i \in a :: rs -> G i <= F i
IHrs : (forall 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
============================
G a <= F a
subgoal 2 (ID 143) is:
\sum_(j <- rs) G j <= \sum_(j <- rs) F j
----------------------------------------------------------------------------- *)
- by apply H; rewrite in_cons; apply/orP; left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 143)
T : eqType
a : T
rs : seq T
F, G : T -> nat
H : forall i : T, i \in a :: rs -> G i <= F i
IHrs : (forall 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
============================
\sum_(j <- rs) G j <= \sum_(j <- rs) F j
----------------------------------------------------------------------------- *)
- rewrite big_seq_cond [in X in _ ≤ X]big_seq_cond.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 323)
T : eqType
a : T
rs : seq T
F, G : T -> nat
H : forall i : T, i \in a :: rs -> G i <= F i
IHrs : (forall 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
============================
\sum_(i <- rs | (i \in rs) && true) G i <=
\sum_(i <- rs | (i \in rs) && true) F i
----------------------------------------------------------------------------- *)
rewrite leq_sum //; move ⇒ i /andP [IN _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 399)
T : eqType
a : T
rs : seq T
F, G : T -> nat
H : forall i : T, i \in a :: rs -> G i <= F i
IHrs : (forall 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
i : T
IN : i \in rs
============================
G i <= F i
----------------------------------------------------------------------------- *)
by apply H; rewrite in_cons; apply/orP; right.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 62)
============================
forall (n : nat) (F G : nat -> nat),
(forall i : nat, i < n -> G i <= F 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 66)
n : nat
F, G : nat -> nat
ALL : forall i : nat, i < n -> G i <= F i
============================
\sum_(0 <= i < n) (F i - G i) =
\sum_(0 <= i < n) F i - \sum_(0 <= i < n) G i
----------------------------------------------------------------------------- *)
rewrite sum_seq_diff; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 74)
n : nat
F, G : nat -> nat
ALL : forall i : nat, i < n -> G i <= F i
============================
forall i : nat_eqType, i \in index_iota 0 n -> G i <= F i
----------------------------------------------------------------------------- *)
move ⇒ i; rewrite mem_index_iota; move ⇒ /andP [_ LT].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 120)
n : nat
F, G : nat -> nat
ALL : forall i : nat, i < n -> G i <= F i
i : nat_eqType
LT : i < n
============================
G i <= F i
----------------------------------------------------------------------------- *)
by apply ALL.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 80)
============================
forall (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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 84)
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
----------------------------------------------------------------------------- *)
induction rs; first by rewrite !big_nil subn0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 94)
T : eqType
a : T
rs : seq T
P : T -> bool
F : T -> nat
IHrs : \sum_(r <- rs | P r) F r =
\sum_(r <- rs) F r - \sum_(r <- rs | ~~ P r) F r
============================
\sum_(r <- (a :: rs) | P r) F r =
\sum_(r <- (a :: rs)) F r - \sum_(r <- (a :: rs) | ~~ P r) F r
----------------------------------------------------------------------------- *)
rewrite !big_cons !IHrs; clear IHrs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 170)
T : eqType
a : T
rs : seq T
P : T -> bool
F : T -> nat
============================
(if P a
then F a + (\sum_(r <- rs) F r - \sum_(r <- rs | ~~ P r) F r)
else \sum_(r <- rs) F r - \sum_(r <- rs | ~~ P r) F r) =
F a + \sum_(j <- rs) F j -
(if ~~ P a
then F a + \sum_(j <- rs | ~~ P j) F j
else \sum_(j <- rs | ~~ P j) F j)
----------------------------------------------------------------------------- *)
case (P a); simpl; last by rewrite subnDl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 174)
T : eqType
a : T
rs : seq T
P : T -> bool
F : T -> nat
============================
F a + (\sum_(r <- rs) F r - \sum_(r <- rs | ~~ P r) F r) =
F a + \sum_(j <- rs) F j - \sum_(j <- rs | ~~ P j) F j
----------------------------------------------------------------------------- *)
rewrite addnBA; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 188)
T : eqType
a : T
rs : seq T
P : T -> bool
F : T -> nat
============================
\sum_(r <- rs | ~~ P r) F r <= \sum_(r <- rs) F r
----------------------------------------------------------------------------- *)
rewrite big_mkcond leq_sum //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 206)
T : eqType
a : T
rs : seq T
P : T -> bool
F : T -> nat
============================
forall i : T, true -> (if ~~ P i then F i else 0) <= F i
----------------------------------------------------------------------------- *)
intros t _.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 235)
T : eqType
a : T
rs : seq T
P : T -> bool
F : T -> nat
t : T
============================
(if ~~ P t then F t else 0) <= F t
----------------------------------------------------------------------------- *)
by case (P t).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
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.
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 102)
============================
forall (T : eqType) (r1 r2 : seq T) (F : T -> nat),
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 110)
T : eqType
r1 : seq T
F : T -> nat
UNIQ : uniq r1
============================
forall r2 : seq T,
{subset r1 <= r2} -> \sum_(i <- r1) F i <= \sum_(i <- r2) F i
----------------------------------------------------------------------------- *)
induction r1 as [| x r1' IH]; first by ins; rewrite big_nil.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 126)
T : eqType
x : T
r1' : seq T
F : T -> nat
UNIQ : uniq (x :: r1')
IH : uniq r1' ->
forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
============================
forall r2 : seq T,
{subset x :: r1' <= r2} -> \sum_(i <- (x :: r1')) F i <= \sum_(i <- r2) F i
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 126)
T : eqType
x : T
r1' : seq T
F : T -> nat
UNIQ : uniq (x :: r1')
IH : uniq r1' ->
forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
============================
forall r2 : seq T,
{subset x :: r1' <= r2} -> \sum_(i <- (x :: r1')) F i <= \sum_(i <- r2) F i
----------------------------------------------------------------------------- *)
intros r2 SUB.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 167)
T : eqType
x : T
r1' : seq T
F : T -> nat
UNIQ : uniq (x :: r1')
IH : uniq r1' ->
forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
r2 : seq T
SUB : {subset x :: r1' <= r2}
============================
\sum_(i <- (x :: r1')) F i <= \sum_(i <- r2) F i
----------------------------------------------------------------------------- *)
assert (IN: x \in r2).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 172)
T : eqType
x : T
r1' : seq T
F : T -> nat
UNIQ : uniq (x :: r1')
IH : uniq r1' ->
forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
r2 : seq T
SUB : {subset x :: r1' <= r2}
============================
x \in r2
subgoal 2 (ID 174) is:
\sum_(i <- (x :: r1')) F i <= \sum_(i <- r2) F i
----------------------------------------------------------------------------- *)
by apply SUB; rewrite in_cons eq_refl orTb.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 174)
T : eqType
x : T
r1' : seq T
F : T -> nat
UNIQ : uniq (x :: r1')
IH : uniq r1' ->
forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
r2 : seq T
SUB : {subset x :: r1' <= r2}
IN : x \in r2
============================
\sum_(i <- (x :: r1')) F i <= \sum_(i <- r2) F i
----------------------------------------------------------------------------- *)
simpl in UNIQ; move: UNIQ ⇒ /andP [NOTIN UNIQ]; specialize (IH UNIQ).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 234)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
r2 : seq T
SUB : {subset x :: r1' <= r2}
IN : x \in r2
NOTIN : x \notin r1'
UNIQ : uniq r1'
============================
\sum_(i <- (x :: r1')) F i <= \sum_(i <- r2) F i
----------------------------------------------------------------------------- *)
destruct (splitPr IN).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 251)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
SUB : {subset x :: r1' <= p1 ++ x :: p2}
IN : x \in p1 ++ x :: p2
NOTIN : x \notin r1'
UNIQ : uniq r1'
============================
\sum_(i <- (x :: r1')) F i <= \sum_(i <- (p1 ++ x :: p2)) F i
----------------------------------------------------------------------------- *)
rewrite big_cat 2!big_cons /= addnA [_ + F x]addnC -addnA leq_add2l.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 309)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
SUB : {subset x :: r1' <= p1 ++ x :: p2}
IN : x \in p1 ++ x :: p2
NOTIN : x \notin r1'
UNIQ : uniq r1'
============================
\sum_(j <- r1') F j <= \sum_(i <- p1) F i + \sum_(j <- p2) F j
----------------------------------------------------------------------------- *)
rewrite mem_cat in_cons eq_refl in IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 343)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
SUB : {subset x :: r1' <= p1 ++ x :: p2}
NOTIN : x \notin r1'
UNIQ : uniq r1'
IN : [|| x \in p1, true | x \in p2]
============================
\sum_(j <- r1') F j <= \sum_(i <- p1) F i + \sum_(j <- p2) F j
----------------------------------------------------------------------------- *)
rewrite -big_cat /=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 354)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
SUB : {subset x :: r1' <= p1 ++ x :: p2}
NOTIN : x \notin r1'
UNIQ : uniq r1'
IN : [|| x \in p1, true | x \in p2]
============================
\sum_(j <- r1') F j <= \sum_(i <- (p1 ++ p2)) F i
----------------------------------------------------------------------------- *)
apply IH; red; intros x0 IN0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 359)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
SUB : {subset x :: r1' <= p1 ++ x :: p2}
NOTIN : x \notin r1'
UNIQ : uniq r1'
IN : [|| x \in p1, true | x \in p2]
x0 : T
IN0 : x0 \in r1'
============================
x0 \in p1 ++ p2
----------------------------------------------------------------------------- *)
rewrite mem_cat.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 365)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
SUB : {subset x :: r1' <= p1 ++ x :: p2}
NOTIN : x \notin r1'
UNIQ : uniq r1'
IN : [|| x \in p1, true | x \in p2]
x0 : T
IN0 : x0 \in r1'
============================
(x0 \in p1) || (x0 \in p2)
----------------------------------------------------------------------------- *)
feed (SUB x0); first by rewrite in_cons IN0 orbT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 371)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
x0 : T
SUB : x0 \in p1 ++ x :: p2
NOTIN : x \notin r1'
UNIQ : uniq r1'
IN : [|| x \in p1, true | x \in p2]
IN0 : x0 \in r1'
============================
(x0 \in p1) || (x0 \in p2)
----------------------------------------------------------------------------- *)
rewrite mem_cat in_cons in SUB.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 414)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
x0 : T
NOTIN : x \notin r1'
UNIQ : uniq r1'
IN : [|| x \in p1, true | x \in p2]
IN0 : x0 \in r1'
SUB : [|| x0 \in p1, x0 == x | x0 \in p2]
============================
(x0 \in p1) || (x0 \in p2)
----------------------------------------------------------------------------- *)
move: SUB ⇒ /orP [SUB1 | /orP [/eqP EQx | SUB2]];
[by rewrite SUB1 | | by rewrite SUB2 orbT].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 533)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
x0 : T
NOTIN : x \notin r1'
UNIQ : uniq r1'
IN : [|| x \in p1, true | x \in p2]
IN0 : x0 \in r1'
EQx : x0 = x
============================
(x0 \in p1) || (x0 \in p2)
----------------------------------------------------------------------------- *)
by rewrite -EQx IN0 in NOTIN.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End SumArithmetic.
∀ (T: eqType) (r1 r2: seq T) F,
uniq r1 →
{subset r1 ≤ r2} →
\sum_(i <- r1) F i ≤ \sum_(i <- r2) F i.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 102)
============================
forall (T : eqType) (r1 r2 : seq T) (F : T -> nat),
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 110)
T : eqType
r1 : seq T
F : T -> nat
UNIQ : uniq r1
============================
forall r2 : seq T,
{subset r1 <= r2} -> \sum_(i <- r1) F i <= \sum_(i <- r2) F i
----------------------------------------------------------------------------- *)
induction r1 as [| x r1' IH]; first by ins; rewrite big_nil.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 126)
T : eqType
x : T
r1' : seq T
F : T -> nat
UNIQ : uniq (x :: r1')
IH : uniq r1' ->
forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
============================
forall r2 : seq T,
{subset x :: r1' <= r2} -> \sum_(i <- (x :: r1')) F i <= \sum_(i <- r2) F i
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 126)
T : eqType
x : T
r1' : seq T
F : T -> nat
UNIQ : uniq (x :: r1')
IH : uniq r1' ->
forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
============================
forall r2 : seq T,
{subset x :: r1' <= r2} -> \sum_(i <- (x :: r1')) F i <= \sum_(i <- r2) F i
----------------------------------------------------------------------------- *)
intros r2 SUB.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 167)
T : eqType
x : T
r1' : seq T
F : T -> nat
UNIQ : uniq (x :: r1')
IH : uniq r1' ->
forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
r2 : seq T
SUB : {subset x :: r1' <= r2}
============================
\sum_(i <- (x :: r1')) F i <= \sum_(i <- r2) F i
----------------------------------------------------------------------------- *)
assert (IN: x \in r2).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 172)
T : eqType
x : T
r1' : seq T
F : T -> nat
UNIQ : uniq (x :: r1')
IH : uniq r1' ->
forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
r2 : seq T
SUB : {subset x :: r1' <= r2}
============================
x \in r2
subgoal 2 (ID 174) is:
\sum_(i <- (x :: r1')) F i <= \sum_(i <- r2) F i
----------------------------------------------------------------------------- *)
by apply SUB; rewrite in_cons eq_refl orTb.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 174)
T : eqType
x : T
r1' : seq T
F : T -> nat
UNIQ : uniq (x :: r1')
IH : uniq r1' ->
forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
r2 : seq T
SUB : {subset x :: r1' <= r2}
IN : x \in r2
============================
\sum_(i <- (x :: r1')) F i <= \sum_(i <- r2) F i
----------------------------------------------------------------------------- *)
simpl in UNIQ; move: UNIQ ⇒ /andP [NOTIN UNIQ]; specialize (IH UNIQ).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 234)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
r2 : seq T
SUB : {subset x :: r1' <= r2}
IN : x \in r2
NOTIN : x \notin r1'
UNIQ : uniq r1'
============================
\sum_(i <- (x :: r1')) F i <= \sum_(i <- r2) F i
----------------------------------------------------------------------------- *)
destruct (splitPr IN).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 251)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
SUB : {subset x :: r1' <= p1 ++ x :: p2}
IN : x \in p1 ++ x :: p2
NOTIN : x \notin r1'
UNIQ : uniq r1'
============================
\sum_(i <- (x :: r1')) F i <= \sum_(i <- (p1 ++ x :: p2)) F i
----------------------------------------------------------------------------- *)
rewrite big_cat 2!big_cons /= addnA [_ + F x]addnC -addnA leq_add2l.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 309)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
SUB : {subset x :: r1' <= p1 ++ x :: p2}
IN : x \in p1 ++ x :: p2
NOTIN : x \notin r1'
UNIQ : uniq r1'
============================
\sum_(j <- r1') F j <= \sum_(i <- p1) F i + \sum_(j <- p2) F j
----------------------------------------------------------------------------- *)
rewrite mem_cat in_cons eq_refl in IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 343)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
SUB : {subset x :: r1' <= p1 ++ x :: p2}
NOTIN : x \notin r1'
UNIQ : uniq r1'
IN : [|| x \in p1, true | x \in p2]
============================
\sum_(j <- r1') F j <= \sum_(i <- p1) F i + \sum_(j <- p2) F j
----------------------------------------------------------------------------- *)
rewrite -big_cat /=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 354)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
SUB : {subset x :: r1' <= p1 ++ x :: p2}
NOTIN : x \notin r1'
UNIQ : uniq r1'
IN : [|| x \in p1, true | x \in p2]
============================
\sum_(j <- r1') F j <= \sum_(i <- (p1 ++ p2)) F i
----------------------------------------------------------------------------- *)
apply IH; red; intros x0 IN0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 359)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
SUB : {subset x :: r1' <= p1 ++ x :: p2}
NOTIN : x \notin r1'
UNIQ : uniq r1'
IN : [|| x \in p1, true | x \in p2]
x0 : T
IN0 : x0 \in r1'
============================
x0 \in p1 ++ p2
----------------------------------------------------------------------------- *)
rewrite mem_cat.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 365)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
SUB : {subset x :: r1' <= p1 ++ x :: p2}
NOTIN : x \notin r1'
UNIQ : uniq r1'
IN : [|| x \in p1, true | x \in p2]
x0 : T
IN0 : x0 \in r1'
============================
(x0 \in p1) || (x0 \in p2)
----------------------------------------------------------------------------- *)
feed (SUB x0); first by rewrite in_cons IN0 orbT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 371)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
x0 : T
SUB : x0 \in p1 ++ x :: p2
NOTIN : x \notin r1'
UNIQ : uniq r1'
IN : [|| x \in p1, true | x \in p2]
IN0 : x0 \in r1'
============================
(x0 \in p1) || (x0 \in p2)
----------------------------------------------------------------------------- *)
rewrite mem_cat in_cons in SUB.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 414)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
x0 : T
NOTIN : x \notin r1'
UNIQ : uniq r1'
IN : [|| x \in p1, true | x \in p2]
IN0 : x0 \in r1'
SUB : [|| x0 \in p1, x0 == x | x0 \in p2]
============================
(x0 \in p1) || (x0 \in p2)
----------------------------------------------------------------------------- *)
move: SUB ⇒ /orP [SUB1 | /orP [/eqP EQx | SUB2]];
[by rewrite SUB1 | | by rewrite SUB2 orbT].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 533)
T : eqType
x : T
r1' : seq T
F : T -> nat
IH : forall r2 : seq T,
{subset r1' <= r2} -> \sum_(i <- r1') F i <= \sum_(i <- r2) F i
p1, p2 : seq T
x0 : T
NOTIN : x \notin r1'
UNIQ : uniq r1'
IN : [|| x \in p1, true | x \in p2]
IN0 : x0 \in r1'
EQx : x0 = x
============================
(x0 \in p1) || (x0 \in p2)
----------------------------------------------------------------------------- *)
by rewrite -EQx IN0 in NOTIN.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End SumArithmetic.