From 1b64ec084566c4ec3248d37d1c3c70d25eb2616b Mon Sep 17 00:00:00 2001
From: Sergey Bozhko <sbozhko@sws-mpi.org>
Date: Thu, 20 Sep 2018 16:04:41 +0200
Subject: [PATCH] Update util files
---
util/all.v | 3 +-
util/minmax.v | 55 ++++++++++++--
util/sum.v | 202 +++++++++++++++++++++++++++++---------------------
3 files changed, 169 insertions(+), 91 deletions(-)
diff --git a/util/all.v b/util/all.v
index 25acc36ba..892aad02c 100644
--- a/util/all.v
+++ b/util/all.v
@@ -1,6 +1,7 @@
Require Export rt.util.tactics.
Require Export rt.util.notation.
Require Export rt.util.bigcat.
+Require Export rt.util.pick.
Require Export rt.util.bigord.
Require Export rt.util.counting.
Require Export rt.util.div_mod.
@@ -16,4 +17,4 @@ Require Export rt.util.sum.
Require Export rt.util.minmax.
Require Export rt.util.seqset.
Require Export rt.util.step_function.
-Require Export rt.util.pick.
\ No newline at end of file
+Require Export rt.util.epsilon.
diff --git a/util/minmax.v b/util/minmax.v
index ea69b93b3..5d8e673ee 100644
--- a/util/minmax.v
+++ b/util/minmax.v
@@ -514,14 +514,55 @@ End MinMaxSeq.
(* Additional lemmas about max. *)
Section ExtraLemmas.
-
- Lemma leq_big_max I r (P : pred I) (E1 E2 : I -> nat) :
- (forall i, P i -> E1 i <= E2 i) ->
- \max_(i <- r | P i) E1 i <= \max_(i <- r | P i) E2 i.
+
+ Lemma leq_bigmax_cond_seq (T : eqType) (P : pred T) (r : seq T) F i0 :
+ i0 \in r -> P i0 -> F i0 <= \max_(i <- r | P i) F i.
+ Proof.
+ intros IN0 Pi0; by rewrite (big_rem i0) //= Pi0 leq_maxl.
+ Qed.
+
+ Lemma bigmax_sup_seq:
+ forall (T: eqType) (i: T) r (P: pred T) m F,
+ i \in r -> P i -> m <= F i -> m <= \max_(i <- r| P i) F i.
+ Proof.
+ intros.
+ induction r.
+ - by rewrite in_nil in H.
+ move: H; rewrite in_cons; move => /orP [/eqP EQA | IN].
+ {
+ clear IHr; subst a.
+ rewrite (big_rem i) //=; last by rewrite in_cons; apply/orP; left.
+ apply leq_trans with (F i); first by done.
+ by rewrite H0 leq_maxl.
+ }
+ {
+ apply leq_trans with (\max_(i0 <- r | P i0) F i0); first by apply IHr.
+ rewrite [in X in _ <= X](big_rem a) //=; last by rewrite in_cons; apply/orP; left.
+
+ have Ob: a == a; first by done.
+ by rewrite Ob leq_maxr.
+ }
+ Qed.
+
+ Lemma bigmax_leq_seqP (T : eqType) (P : pred T) (r : seq T) F m :
+ reflect (forall i, i \in r -> P i -> F i <= m)
+ (\max_(i <- r | P i) F i <= m).
+ Proof.
+ apply: (iffP idP) => leFm => [i IINR Pi|];
+ first by apply: leq_trans leFm; apply leq_bigmax_cond_seq.
+ rewrite big_seq_cond; elim/big_ind: _ => // m1 m2.
+ by intros; rewrite geq_max; apply/andP; split.
+ by move: m2 => /andP [M1IN Pm1]; apply: leFm.
+ Qed.
+
+ Lemma leq_big_max (T : eqType) (P : pred T) (r : seq T) F1 F2 :
+ (forall i, i \in r -> P i -> F1 i <= F2 i) ->
+ \max_(i <- r | P i) F1 i <= \max_(i <- r | P i) F2 i.
Proof.
- move => leE12; elim/big_ind2 : _ => // m1 m2 n1 n2.
- intros LE1 LE2; rewrite leq_max; unfold maxn.
- by destruct (m2 < n2) eqn:LT; [by apply/orP; right | by apply/orP; left].
+ intros; apply /bigmax_leq_seqP; intros.
+ specialize (H i); feed_n 2 H; try(done).
+ rewrite (big_rem i) //=; rewrite H1.
+ by apply leq_trans with (F2 i); [ | rewrite leq_maxl].
Qed.
Lemma bigmax_ord_ltn_identity n :
diff --git a/util/sum.v b/util/sum.v
index 7980bd4c2..af03f4b52 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -1,88 +1,7 @@
Require Import rt.util.tactics rt.util.notation rt.util.sorting rt.util.nat.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
-(* Lemmas about arithmetic with sums. *)
-Section SumArithmetic.
-
- (* Inequality with sums is monotonic with their functions. *)
- Lemma sum_diff_monotonic :
- forall n G F,
- (forall i : nat, i < n -> G i <= F i) ->
- (\sum_(0 <= i < n) (G i)) <= (\sum_(0 <= i < n) (F i)).
- Proof.
- intros n G F ALL.
- rewrite big_nat_cond [\sum_(0 <= i < n) F i]big_nat_cond.
- apply leq_sum; intros i LT; rewrite andbT in LT.
- move: LT => /andP LT; des.
- by apply ALL, leq_trans with (n := n); ins.
- Qed.
-
- Lemma sum_diff :
- forall n F G,
- (forall i (LT: i < n), F i >= G i) ->
- \sum_(0 <= i < n) (F i - G i) =
- (\sum_(0 <= i < n) (F i)) - (\sum_(0 <= i < n) (G i)).
- Proof.
- intros n F G ALL.
- induction n; ins; first by rewrite 3?big_geq.
- assert (ALL': forall i, i < n -> G i <= F i).
- by ins; apply ALL, leq_trans with (n := n); ins.
- rewrite 3?big_nat_recr // IHn //; simpl.
- rewrite subh1; last by apply sum_diff_monotonic.
- rewrite subh2 //; try apply sum_diff_monotonic; ins.
- rewrite subh1; ins; apply sum_diff_monotonic; ins.
- by apply ALL; rewrite ltnS leqnn.
- Qed.
-
- Lemma telescoping_sum :
- forall (T: Type) (F: T->nat) r (x0: T),
- (forall i, i < (size r).-1 -> F (nth x0 r i) <= F (nth x0 r i.+1)) ->
- F (nth x0 r (size r).-1) - F (nth x0 r 0) =
- \sum_(0 <= i < (size r).-1) (F (nth x0 r (i.+1)) - F (nth x0 r i)).
- Proof.
- intros T F r x0 ALL.
- have ADD1 := big_add1.
- have RECL := big_nat_recl.
- specialize (ADD1 nat 0 addn 0 (size r) (fun x => true) (fun i => F (nth x0 r i))).
- specialize (RECL nat 0 addn (size r).-1 0 (fun i => F (nth x0 r i))).
- rewrite sum_diff; last by ins.
- rewrite addmovr; last by rewrite -[_.-1]add0n; apply prev_le_next; try rewrite add0n leqnn.
- rewrite subh1; last by apply sum_diff_monotonic.
- rewrite addnC -RECL //.
- rewrite addmovl; last by rewrite big_nat_recr // -{1}[\sum_(_ <= _ < _) _]addn0; apply leq_add.
- by rewrite addnC -big_nat_recr.
- Qed.
-
- Lemma leq_sum_sub_uniq :
- forall (T: eqType) (r1 r2: seq T) F,
- uniq r1 ->
- {subset r1 <= r2} ->
- \sum_(i <- r1) F i <= \sum_(i <- r2) F i.
- Proof.
- intros T r1 r2 F UNIQ SUB; generalize dependent r2.
- induction r1 as [| x r1' IH]; first by ins; rewrite big_nil.
- {
- intros r2 SUB.
- assert (IN: x \in r2).
- by apply SUB; rewrite in_cons eq_refl orTb.
- simpl in UNIQ; move: UNIQ => /andP [NOTIN UNIQ]; specialize (IH UNIQ).
- destruct (splitPr IN).
- rewrite big_cat 2!big_cons /= addnA [_ + F x]addnC -addnA leq_add2l.
- rewrite mem_cat in_cons eq_refl in IN.
- rewrite -big_cat /=.
- apply IH; red; intros x0 IN0.
- rewrite mem_cat.
- feed (SUB x0); first by rewrite in_cons IN0 orbT.
- rewrite mem_cat in_cons in SUB.
- move: SUB => /orP [SUB1 | /orP [/eqP EQx | SUB2]];
- [by rewrite SUB1 | | by rewrite SUB2 orbT].
- by rewrite -EQx IN0 in NOTIN.
- }
- Qed.
-
-End SumArithmetic.
-
-(* Additional lemmas about sum. *)
+(* Lemmas about sum. *)
Section ExtraLemmas.
Lemma extend_sum :
@@ -170,4 +89,121 @@ Section ExtraLemmas.
}
Qed.
-End ExtraLemmas.
\ No newline at end of file
+ Lemma sum_seq_gt0P:
+ forall (T:eqType) (r: seq T) (F: T -> nat),
+ reflect (exists i, i \in r /\ 0 < F i) (0 < \sum_(i <- r) F i).
+ Proof.
+ intros; apply: (iffP idP); intros.
+ {
+ induction r; first by rewrite big_nil in H.
+ destruct (F a > 0) eqn:POS.
+ exists a; split; [by rewrite in_cons; apply/orP; left | by done].
+ apply negbT in POS; rewrite -leqNgt leqn0 in POS; move: POS => /eqP POS.
+ rewrite big_cons POS add0n in H. clear POS.
+ feed IHr; first by done. move: IHr => [i [IN POS]].
+ exists i; split; [by rewrite in_cons; apply/orP;right | by done].
+ }
+ {
+ move: H => [i [IN POS]].
+ rewrite (big_rem i) //=.
+ apply leq_trans with (F i); [by done | by rewrite leq_addr].
+ }
+ Qed.
+
+ Lemma leq_pred_sum:
+ forall (T:eqType) (r: seq T) (P1 P2: pred T) F,
+ (forall i, P1 i -> P2 i) ->
+ \sum_(i <- r | P1 i) F i <=
+ \sum_(i <- r | P2 i) F i.
+ Proof.
+ intros.
+ rewrite big_mkcond [in X in _ <= X]big_mkcond//= leq_sum //.
+ intros i _.
+ destruct P1 eqn:P1a; destruct P2 eqn:P2a; [by done | | by done | by done].
+ exfalso.
+ move: P1a P2a => /eqP P1a /eqP P2a.
+ rewrite eqb_id in P1a; rewrite eqbF_neg in P2a.
+ move: P2a => /negP P2a.
+ by apply P2a; apply H.
+ Qed.
+
+End ExtraLemmas.
+
+(* Lemmas about arithmetic with sums. *)
+Section SumArithmetic.
+
+ Lemma sum_seq_diff:
+ forall (T:eqType) (r: seq T) (F G : T -> nat),
+ (forall i : T, i \in r -> G i <= F i) ->
+ \sum_(i <- r) (F i - G i) = \sum_(i <- r) F i - \sum_(i <- r) G i.
+ Proof.
+ intros.
+ induction r; first by rewrite !big_nil subn0.
+ rewrite !big_cons subh2.
+ - apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHr.
+ by intros; apply H; rewrite in_cons; apply/orP; right.
+ - by apply H; rewrite in_cons; apply/orP; left.
+ - rewrite big_seq_cond [in X in _ <= X]big_seq_cond.
+ rewrite leq_sum //; move => i /andP [IN _].
+ by apply H; rewrite in_cons; apply/orP; right.
+ Qed.
+
+ Lemma sum_diff:
+ forall n F G,
+ (forall i (LT: i < n), F i >= G i) ->
+ \sum_(0 <= i < n) (F i - G i) =
+ (\sum_(0 <= i < n) (F i)) - (\sum_(0 <= i < n) (G i)).
+ Proof.
+ intros n F G ALL.
+ rewrite sum_seq_diff; first by done.
+ move => i; rewrite mem_index_iota; move => /andP [_ LT].
+ by apply ALL.
+ Qed.
+
+ Lemma telescoping_sum :
+ forall (T: Type) (F: T->nat) r (x0: T),
+ (forall i, i < (size r).-1 -> F (nth x0 r i) <= F (nth x0 r i.+1)) ->
+ F (nth x0 r (size r).-1) - F (nth x0 r 0) =
+ \sum_(0 <= i < (size r).-1) (F (nth x0 r (i.+1)) - F (nth x0 r i)).
+ Proof.
+ intros T F r x0 ALL.
+ have ADD1 := big_add1.
+ have RECL := big_nat_recl.
+ specialize (ADD1 nat 0 addn 0 (size r) (fun x => true) (fun i => F (nth x0 r i))).
+ specialize (RECL nat 0 addn (size r).-1 0 (fun i => F (nth x0 r i))).
+ rewrite sum_diff; last by ins.
+ rewrite addmovr; last by rewrite -[_.-1]add0n; apply prev_le_next; try rewrite add0n leqnn.
+ rewrite subh1; last by apply leq_sum_nat; move => i /andP [_ LT] _; apply ALL.
+ rewrite addnC -RECL //.
+ rewrite addmovl; last by rewrite big_nat_recr // -{1}[\sum_(_ <= _ < _) _]addn0; apply leq_add.
+ by rewrite addnC -big_nat_recr.
+ Qed.
+
+ Lemma leq_sum_sub_uniq :
+ forall (T: eqType) (r1 r2: seq T) F,
+ uniq r1 ->
+ {subset r1 <= r2} ->
+ \sum_(i <- r1) F i <= \sum_(i <- r2) F i.
+ Proof.
+ intros T r1 r2 F UNIQ SUB; generalize dependent r2.
+ induction r1 as [| x r1' IH]; first by ins; rewrite big_nil.
+ {
+ intros r2 SUB.
+ assert (IN: x \in r2).
+ by apply SUB; rewrite in_cons eq_refl orTb.
+ simpl in UNIQ; move: UNIQ => /andP [NOTIN UNIQ]; specialize (IH UNIQ).
+ destruct (splitPr IN).
+ rewrite big_cat 2!big_cons /= addnA [_ + F x]addnC -addnA leq_add2l.
+ rewrite mem_cat in_cons eq_refl in IN.
+ rewrite -big_cat /=.
+ apply IH; red; intros x0 IN0.
+ rewrite mem_cat.
+ feed (SUB x0); first by rewrite in_cons IN0 orbT.
+ rewrite mem_cat in_cons in SUB.
+ move: SUB => /orP [SUB1 | /orP [/eqP EQx | SUB2]];
+ [by rewrite SUB1 | | by rewrite SUB2 orbT].
+ by rewrite -EQx IN0 in NOTIN.
+ }
+ Qed.
+
+End SumArithmetic.
\ No newline at end of file
--
GitLab