Add new lemma about sums

util/minmax.v

@@ -157,8 +157,8 @@ Section MinMaxSeq.
   
 End MinMaxSeq.
 
-(* Additional lemmas about sum and max big operators. *)
-Section ExtraLemmasSumMax.
+(* 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) ->
@@ -236,152 +236,5 @@ Section ExtraLemmasSumMax.
       by rewrite (IHn (Ordinal LT)).
     }
   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).
-  Proof.
-    destruct (all (fun x => F x == 0) r) eqn:ZERO.
-    {
-      move: ZERO => /allP ZERO; rewrite -leqn0.
-      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.
-      by move: ZERO => /implyP ZERO; apply/eqP; apply ZERO.
-    }
-    {
-      apply negbT in ZERO; rewrite -has_predC in ZERO.
-      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.
-      by rewrite lt0n.
-    }
-  Qed.
-  
-  Lemma extend_sum :
-    forall t1 t2 t1' t2' F,
-      t1' <= t1 ->
-      t2 <= t2' ->
-      \sum_(t1 <= t < t2) F t <= \sum_(t1' <= t < t2') F t.
-  Proof.
-    intros t1 t2 t1' t2' F LE1 LE2.
-    destruct (t1 <= t2) eqn:LE12;
-      last by apply negbT in LE12; rewrite -ltnNge in LE12; rewrite big_geq // ltnW.
-    rewrite -> big_cat_nat with (m := t1') (n := t1); try (by done); simpl;
-      last by apply leq_trans with (n := t2).
-    rewrite -> big_cat_nat with (p := t2') (n := t2); try (by done); simpl.
-    by rewrite addnC -addnA; apply leq_addr.
-  Qed.
-
-  Lemma leq_sum_nat m n (P : pred nat) (E1 E2 : nat -> nat) :
-    (forall i, m <= i < n -> P i -> E1 i <= E2 i) ->
-    \sum_(m <= i < n | P i) E1 i <= \sum_(m <= i < n | P i) E2 i.
-  Proof.
-    intros LE.
-    rewrite big_nat_cond [\sum_(_ <= _ < _| P _)_]big_nat_cond.
-    by apply leq_sum; move => j /andP [IN H]; apply LE.
-  Qed.
-
-  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.
-    by apply leq_sum; move => j /andP [IN H]; apply LE.
-  Qed.
-
-  Lemma leq_sum1_smaller_range m n (P Q: pred nat) a b:
-    (forall i, m <= i < n /\ P i -> a <= i < b /\ Q i) ->
-    \sum_(m <= i < n | P i) 1 <= \sum_(a <= i < b | Q i) 1.
-  Proof.
-    intros REDUCE.
-    rewrite big_mkcond.
-    apply leq_trans with (n := \sum_(a <= i < b | Q i) \sum_(m <= i' < n | i' == i) 1).
-    {
-      rewrite (exchange_big_dep (fun x => true)); [simpl | by done].
-      apply leq_sum_nat; intros i LE _.
-      case TRUE: (P i); last by done.
-      move: (REDUCE i (conj LE TRUE)) => [LE' TRUE'].
-      rewrite (big_rem i); last by rewrite mem_index_iota.
-      by rewrite TRUE' eq_refl.
-    }
-    {
-      apply leq_sum_nat; intros i LE TRUE.
-      rewrite big_mkcond /=.
-      destruct (m <= i < n) eqn:LE'; last first.
-      {
-        rewrite big_nat_cond big1; first by done.
-        move => i' /andP [LE'' _]; case EQ: (_ == _); last by done.
-        by move: EQ => /eqP EQ; subst; rewrite LE'' in LE'.
-      }
-      rewrite (bigD1_seq i) /=; [ | by rewrite mem_index_iota | by rewrite iota_uniq ].
-      rewrite eq_refl big1; first by done.
-      by move => i' /negbTE NEQ; rewrite NEQ.
-    }
-  Qed.
-
-End ExtraLemmasSumMax.
-
-(*Section ProvingFinType.
-    
-    Lemma seq_sub_choiceMixin : choiceMixin (seq_sub l).
-    Proof.
-      destruct (seq_sub_enum l) eqn:SUB.
-      {
-        set f := fun (P: pred (seq_sub l)) (x: nat) => @None (seq_sub l).
-                 exists f; last by done.
-                 {
-                   intros P n x.
-                   have IN := mem_seq_sub_enum x.
-                     by rewrite SUB in_nil in IN.
-                 }
-                 {
-                   move => P [x PROP].
-                   have IN := mem_seq_sub_enum x.
-                     by rewrite SUB in_nil in IN.
-                 }
-      }
-      {
-        set NTH := nth s (seq_sub_enum l).
-        set f := fun (P: pred (seq_sub l)) (x: nat) => if P (NTH x) then Some (NTH x) else None.
-        exists f.
-        {
-          unfold f; intros P n x.
-          by case: ifP => [PROP | //]; case => <-.
-        }
-        {
-          move => P [x PROP].
-          exists (index x (seq_sub_enum l)).
-          by rewrite /f /NTH nth_index ?PROP; last by apply mem_seq_sub_enum.
-        }
-        {
-          by intros P Q EQ x; rewrite /f -EQ.
-        }
-      }
-    Qed.
-
-    Canonical seq_sub_choiceType :=
-      Eval hnf in ChoiceType (seq_sub l) (seq_sub_choiceMixin).  
     
-
-    Definition seq_sub_countMixin' := CountMixin (@seq_sub_pickleK T l).
-
-    Canonical seq_sub_countType := @Countable.pack _ seq_sub_countMixin' seq_sub_choiceType _ id.
-
-
-    Lemma seq_sub_enumP: Finite.axiom (seq_sub_enum l).
-    Proof.
-      intros x.
-      rewrite count_uniq_mem ?undup_uniq //.
-      by apply/eqP; rewrite eqb1; apply mem_seq_sub_enum.
-    Qed.
-  
-    Definition seq_sub_finMixin := @FinMixin seq_sub_countType (seq_sub_enum l) seq_sub_enumP.
-
-    Canonical seq_sub_finType :=
-      @Finite.pack (seq_sub l) [eqMixin of (seq_sub l)] seq_sub_finMixin seq_sub_choiceType _ id _ id. 
-
-  End ProvingFinType.*)
-
+End ExtraLemmas.
\ No newline at end of file

util/sum.v

@@ -81,3 +81,93 @@ Section SumArithmetic.
   Qed.
     
 End SumArithmetic.
+
+(* Additional lemmas about sum. *)
+Section ExtraLemmas.
+  
+  Lemma extend_sum :
+    forall t1 t2 t1' t2' F,
+      t1' <= t1 ->
+      t2 <= t2' ->
+      \sum_(t1 <= t < t2) F t <= \sum_(t1' <= t < t2') F t.
+  Proof.
+    intros t1 t2 t1' t2' F LE1 LE2.
+    destruct (t1 <= t2) eqn:LE12;
+      last by apply negbT in LE12; rewrite -ltnNge in LE12; rewrite big_geq // ltnW.
+    rewrite -> big_cat_nat with (m := t1') (n := t1); try (by done); simpl;
+      last by apply leq_trans with (n := t2).
+    rewrite -> big_cat_nat with (p := t2') (n := t2); try (by done); simpl.
+    by rewrite addnC -addnA; apply leq_addr.
+  Qed.
+
+  Lemma leq_sum_nat m n (P : pred nat) (E1 E2 : nat -> nat) :
+    (forall i, m <= i < n -> P i -> E1 i <= E2 i) ->
+    \sum_(m <= i < n | P i) E1 i <= \sum_(m <= i < n | P i) E2 i.
+  Proof.
+    intros LE.
+    rewrite big_nat_cond [\sum_(_ <= _ < _| P _)_]big_nat_cond.
+    by apply leq_sum; move => j /andP [IN H]; apply LE.
+  Qed.
+
+  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.
+    by apply leq_sum; move => j /andP [IN H]; apply LE.
+  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).
+  Proof.
+    destruct (all (fun x => F x == 0) r) eqn:ZERO.
+    {
+      move: ZERO => /allP ZERO; rewrite -leqn0.
+      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.
+      by move: ZERO => /implyP ZERO; apply/eqP; apply ZERO.
+    }
+    {
+      apply negbT in ZERO; rewrite -has_predC in ZERO.
+      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.
+      by rewrite lt0n.
+    }
+  Qed.
+  
+  Lemma leq_sum1_smaller_range m n (P Q: pred nat) a b:
+    (forall i, m <= i < n /\ P i -> a <= i < b /\ Q i) ->
+    \sum_(m <= i < n | P i) 1 <= \sum_(a <= i < b | Q i) 1.
+  Proof.
+    intros REDUCE.
+    rewrite big_mkcond.
+    apply leq_trans with (n := \sum_(a <= i < b | Q i) \sum_(m <= i' < n | i' == i) 1).
+    {
+      rewrite (exchange_big_dep (fun x => true)); [simpl | by done].
+      apply leq_sum_nat; intros i LE _.
+      case TRUE: (P i); last by done.
+      move: (REDUCE i (conj LE TRUE)) => [LE' TRUE'].
+      rewrite (big_rem i); last by rewrite mem_index_iota.
+      by rewrite TRUE' eq_refl.
+    }
+    {
+      apply leq_sum_nat; intros i LE TRUE.
+      rewrite big_mkcond /=.
+      destruct (m <= i < n) eqn:LE'; last first.
+      {
+        rewrite big_nat_cond big1; first by done.
+        move => i' /andP [LE'' _]; case EQ: (_ == _); last by done.
+        by move: EQ => /eqP EQ; subst; rewrite LE'' in LE'.
+      }
+      rewrite (bigD1_seq i) /=; [ | by rewrite mem_index_iota | by rewrite iota_uniq ].
+      rewrite eq_refl big1; first by done.
+      by move => i' /negbTE NEQ; rewrite NEQ.
+    }
+  Qed.
+
+End ExtraLemmas.
\ No newline at end of file