Commit 5e400eaf authored by Felipe Cerqueira's avatar Felipe Cerqueira

Add a new lemma about summation

parent c46823da
Require Import rt.util.tactics rt.util.notation rt.util.sorting rt.util.nat. Require Import rt.util.tactics rt.util.notation rt.util.sorting rt.util.nat.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop. From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
(* Lemmas about arithmetic with sums. *) (* Lemmas about arithmetic with sums. *)
Section SumArithmetic. Section SumArithmetic.
...@@ -53,6 +53,33 @@ Section SumArithmetic. ...@@ -53,6 +53,33 @@ Section SumArithmetic.
by rewrite addnC -big_nat_recr. by rewrite addnC -big_nat_recr.
Qed. Qed.
Lemma leq_sum_sub_uniq :
forall (T: eqType) (r1 r2: seq T) F,
uniq r1 ->
{subset r1 <= r2} ->
\sum_(i <- r1) F i <= \sum_(i <- r2) F i.
Proof.
intros T r1 r2 F UNIQ SUB; generalize dependent r2.
induction r1 as [| x r1' IH]; first by ins; rewrite big_nil.
{
intros r2 SUB.
assert (IN: x \in r2).
by apply SUB; rewrite in_cons eq_refl orTb.
simpl in UNIQ; move: UNIQ => /andP [NOTIN UNIQ]; specialize (IH UNIQ).
destruct (splitPr IN).
rewrite big_cat 2!big_cons /= addnA [_ + F x]addnC -addnA leq_add2l.
rewrite mem_cat in_cons eq_refl in IN.
rewrite -big_cat /=.
apply IH; red; intros x0 IN0.
rewrite mem_cat.
feed (SUB x0); first by rewrite in_cons IN0 orbT.
rewrite mem_cat in_cons in SUB.
move: SUB => /orP [SUB1 | /orP [/eqP EQx | SUB2]];
[by rewrite SUB1 | | by rewrite SUB2 orbT].
by rewrite -EQx IN0 in NOTIN.
}
Qed.
End SumArithmetic. End SumArithmetic.
(* Additional lemmas about sum and max big operators. *) (* Additional lemmas about sum and max big operators. *)
...@@ -121,5 +148,5 @@ Section ExtraLemmasSumMax. ...@@ -121,5 +148,5 @@ Section ExtraLemmasSumMax.
rewrite big_seq_cond [\sum_(_ <- _| P _)_]big_seq_cond. rewrite big_seq_cond [\sum_(_ <- _| P _)_]big_seq_cond.
by apply leq_sum; move => j /andP [IN H]; apply LE. by apply leq_sum; move => j /andP [IN H]; apply LE.
Qed. Qed.
End ExtraLemmasSumMax. End ExtraLemmasSumMax.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment