sum.v 9.4 KB
Newer Older
1 2
Require Export rt.util.notation.
Require Export rt.util.nat.
3

4
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
5

Sergey Bozhko's avatar
Sergey Bozhko committed
6
(* Lemmas about sum. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
7 8 9 10 11 12 13 14
Section ExtraLemmas.

  Lemma leq_sum_seq (I: eqType) (r: seq I) (P : pred I) (E1 E2 : I -> nat) :
    (forall i, i \in r -> P i -> E1 i <= E2 i) ->
    \sum_(i <- r | P i) E1 i <= \sum_(i <- r | P i) E2 i.
  Proof.
    intros LE.
    rewrite big_seq_cond [\sum_(_ <- _| P _)_]big_seq_cond.
Sergey Bozhko's avatar
Sergey Bozhko committed
15
      by apply leq_sum; move => j /andP [IN H]; apply LE.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
16 17
  Qed.

Sergey Bozhko's avatar
Sergey Bozhko committed
18 19 20 21 22 23 24 25 26 27
  Lemma eq_sum_seq: forall (I: eqType) (r: seq I) (P: pred I) (E1 E2 : I -> nat), 
      (forall i, i \in r -> P i -> E1 i == E2 i) ->
      \sum_(i <- r | P i) E1 i == \sum_(i <- r | P i) E2 i.
  Proof.
    intros; rewrite eqn_leq; apply/andP; split.
    - apply leq_sum_seq; intros.
        by move: (H i H0 H1) => /eqP EQ; rewrite EQ.
    - apply leq_sum_seq; intros.
        by move: (H i H0 H1) => /eqP EQ; rewrite EQ.
  Qed.  
28

Felipe Cerqueira's avatar
Felipe Cerqueira committed
29 30 31 32
  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).
  Proof.
    destruct (all (fun x => F x == 0) r) eqn:ZERO.
Sergey Bozhko's avatar
Sergey Bozhko committed
33
    - move: ZERO => /allP ZERO; rewrite -leqn0.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
34 35 36 37
      rewrite big_seq_cond (eq_bigr (fun x => 0));
        first by rewrite big_const_seq iter_addn mul0n addn0 leqnn.
      intro i; rewrite andbT; intros IN.
      specialize (ZERO i); rewrite IN in ZERO.
Sergey Bozhko's avatar
Sergey Bozhko committed
38
        by move: ZERO => /implyP ZERO; apply/eqP; apply ZERO.
Sergey Bozhko's avatar
Sergey Bozhko committed
39
    - apply negbT in ZERO; rewrite -has_predC in ZERO.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
40 41 42 43
      move: ZERO => /hasP ZERO; destruct ZERO as [x IN NEQ]; simpl in NEQ.
      rewrite (big_rem x) /=; last by done.
      symmetry; apply negbTE; rewrite neq_ltn; apply/orP; right.
      apply leq_trans with (n := F x); last by apply leq_addr.
Sergey Bozhko's avatar
Sergey Bozhko committed
44
        by rewrite lt0n.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
45
  Qed.
46

Sergey Bozhko's avatar
Sergey Bozhko committed
47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68

  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.

69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
  Lemma sum_notin_rem_eqn:
    forall (T:eqType) (a: T) xs P F,
      a \notin xs ->
      \sum_(x <- xs | P x && (x != a)) F x = \sum_(x <- xs | P x) F x.
  Proof.
    intros ? ? ? ? ? NOTIN.
    induction xs; first by rewrite !big_nil.
    rewrite !big_cons.
    rewrite IHxs; clear IHxs; last first.
    { apply/memPn; intros y IN.
      move: NOTIN => /memPn NOTIN.
        by apply NOTIN; rewrite in_cons; apply/orP; right.
    }
    move: NOTIN => /memPn NOTIN. 
    move: (NOTIN a0) => NEQ.
    feed NEQ; first by (rewrite in_cons; apply/orP; left).
      by rewrite NEQ Bool.andb_true_r.
  Qed.
  
88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109
  (* Trivial identity: any sum of zeros is zero. *)
  Lemma sum0 m n:
    \sum_(m <= i < n) 0 = 0.
  Proof.
    by rewrite big_const_nat iter_addn mul0n addn0 //.
  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 <-> (forall i, m <= i < n -> F i = 0).
  Proof.
    split.
    - rewrite /index_iota => /eqP.
      rewrite -sum_nat_eq0_nat => /allP ZERO i.
      rewrite -mem_index_iota /index_iota => IN.
      by apply/eqP; apply ZERO.
    - move=> ZERO.
      have ->: \sum_(m <= i < n) F i = \sum_(m <= i < n) 0
        by apply eq_big_nat => //.
      by apply sum0.
  Qed.

110
  (* We prove that if any element of a set r is bounded by constant [const], 
Sergey Bozhko's avatar
Sergey Bozhko committed
111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140
     then the sum of the whole set is bounded by [const * size r]. *)
  Lemma sum_majorant_constant:
    forall (T: eqType) (r: seq T) (P: pred T) F const,
      (forall a,  a \in r -> P a -> F a <= const) -> 
      \sum_(j <- r | P j) F j <= const * (size [seq j <- r | P j]).
  Proof.
    clear; intros.
    induction r; first by rewrite big_nil.
    feed IHr.
    { intros; apply H.
      - by rewrite in_cons; apply/orP; right.
      - by done. } 
    rewrite big_cons.
    destruct (P a) eqn:EQ.
    { rewrite -cat1s filter_cat size_cat.
      rewrite mulnDr.
      apply leq_add; last by done.
      rewrite size_filter.
      simpl; rewrite addn0.
      rewrite EQ muln1.
      apply H; last by done. 
        by rewrite in_cons; apply/orP; left. 
    }
    { apply leq_trans with (const * size [seq j <- r | P j]); first by done.
      rewrite leq_mul2l; apply/orP; right.
      rewrite -cat1s filter_cat size_cat.
        by rewrite leq_addl.
    }
  Qed.

141
  (* We prove that if for any element x of a set [xs] the following two statements hold 
Sergey Bozhko's avatar
Sergey Bozhko committed
142 143
     (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 
144
     any element x of [xs]. *)
Sergey Bozhko's avatar
Sergey Bozhko committed
145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163
  Lemma sum_majorant_eqn:
    forall (T: eqType) xs F1 F2 (P: pred T),
      (forall x, x \in xs -> P x -> F1 x <= F2 x) -> 
      \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
      (forall x, x \in xs -> P x -> F1 x = F2 x).
  Proof.
    intros T xs F1 F2 P H1 H2 x IN PX.
    induction xs; first by done.
    have Fact: \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j.
    { rewrite [in X in X <= _]big_seq_cond [in X in _ <= X]big_seq_cond leq_sum //.
      move => y /andP [INy PY].
      apply: H1; last by done. 
        by rewrite in_cons; apply/orP; right. }
    feed IHxs.
    { intros x' IN' PX'.
      apply H1; last by done.
        by rewrite in_cons; apply/orP; right. }
    rewrite big_cons [RHS]big_cons in H2.
    have EqLeq: forall a b c d, a + b = c + d -> a <= c -> b >= d.
Sergey Bozhko's avatar
Sergey Bozhko committed
164
    { clear; intros; ssromega. } 
Sergey Bozhko's avatar
Sergey Bozhko committed
165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193
    move: IN; rewrite in_cons; move => /orP [/eqP EQ | IN]. 
    { subst a.
      rewrite PX in H2.
      specialize (H1 x).
      feed_n 2 H1; [ by rewrite in_cons; apply/orP; left | by done | ].
      move: (EqLeq
               (F1 x) (\sum_(j <- xs | P j) F1 j)
               (F2 x) (\sum_(j <- xs | P j) F2 j) H2 H1) => Q.
      have EQ: \sum_(j <- xs | P j) F1 j = \sum_(j <- xs | P j) F2 j. 
      { by apply/eqP; rewrite eqn_leq; apply/andP; split. }
        by move: H2 => /eqP; rewrite EQ eqn_add2r; move => /eqP EQ'.
    }
    { destruct (P a) eqn:PA; last by apply IHxs.
      apply: IHxs; last by done.
      specialize (H1 a).
      feed_n 2 (H1); [ by rewrite in_cons; apply/orP; left | by done | ].
      move: (EqLeq
               (F1 a) (\sum_(j <- xs | P j) F1 j)
               (F2 a) (\sum_(j <- xs | P j) F2 j) H2 H1) => Q.
        by apply/eqP; rewrite eqn_leq; apply/andP; split.
    }
  Qed.

  (* We prove that the sum of Δ ones is equal to Δ. *)
  Lemma sum_of_ones:
    forall t Δ,
      \sum_(t <= x < t + Δ) 1 = Δ. 
  Proof.
    intros.
194
    rewrite big_const_nat iter_addn_0 mul1n.
Sergey Bozhko's avatar
Sergey Bozhko committed
195 196 197
    rewrite addnC -addnBA; last by done.
      by rewrite subnn addn0.  
  Qed.
198

199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219
  (* 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 :
    forall f t Δ,
      \sum_(t <= x < t + Δ) f x < Δ ->
      exists x, t <= x < t + Δ /\ f x = 0.
  Proof.
    induction Δ; intros; first by rewrite ltn0 in H.
    destruct (f (t + Δ)) eqn: EQ.
    { exists (t + Δ); split; last by done.
        by apply/andP; split; [rewrite leq_addr | rewrite addnS ltnS].
    }
    { move: H; rewrite addnS big_nat_recr //= ?leq_addr // EQ addnS ltnS; move => H.
      feed IHΔ.
      { by apply leq_ltn_trans with (\sum_(t <= i < t + Δ) f i + n); first rewrite leq_addr. }
      move: IHΔ => [z [/andP [LE GE] ZERO]].
      exists z; split; last by done.
      apply/andP; split; first by done.
        by rewrite ltnS ltnW.
    }
  Qed.
Sergey Bozhko's avatar
Sergey Bozhko committed
220 221
  
End ExtraLemmas.
Sergey Bozhko's avatar
Sergey Bozhko committed
222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269

(* Lemmas about arithmetic with sums. *)
Section SumArithmetic.

  Lemma sum_seq_diff:
    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.
    induction rs; first by rewrite !big_nil subn0. 
    rewrite !big_cons subh2.
    - apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHrs.
        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 sum_pred_diff:
    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.
    induction rs; first by rewrite !big_nil subn0.
    rewrite !big_cons !IHrs; clear IHrs.
    case (P a); simpl; last by rewrite subnDl.
    rewrite addnBA; first by done.
    rewrite big_mkcond leq_sum //.
    intros t _.
      by case (P t).
  Qed.
  
End SumArithmetic.