Compat of sumn with bigop and renaming dep to cond when appropriate

5 files changed, 64 insertions, 17 deletions

diff --git a/ChangeLog b/ChangeLog
index 81d479a..0a5e310 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -95,6 +95,16 @@
 
 	* Corrected implicits and documentation of MatrixGenField.
 
+	* Renamed `big_setIDdep` to `big_setIDcond`
+	  and `sum_nat_dep_const` to `sum_nat_cond_const`
+
+	* Added lemmas `big_imset_cond`,`big_map_id`, `big_image_cond`
+	  `big_image`, `big_image_cond_id` and `big_image_id` for
+	  completeness purposes
+
+	* Added lemmas `foldrE`, `foldlE`, `foldl_idx` and `sumnE`
+	  to turn "seq statements" into "bigop statements"
+
 24/04/2018 - compatibility with Coq 8.8 and several small fixes - version 1.7
 
 	* Added compatibility with Coq 8.8 and lost compatibility with
diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v
index 1d8f785..65f06c4 100644
--- a/mathcomp/character/mxabelem.v
+++ b/mathcomp/character/mxabelem.v
@@ -897,7 +897,7 @@ have nb_irr: #|sS| = (p ^ n.*2 + p.-1)%N.
     rewrite ((_ ^: _ =P [set x ^ y])%g _) ?sub1set // eq_sym eqEcard.
     rewrite sub1set class_refl cards1 -index_cent1 (setIidPl _) ?indexgg //.
     by rewrite sub_cent1; apply: subsetP Zxy; apply: subsetIr.
-  rewrite sum_nat_dep_const mulnC eqn_pmul2l //; move/eqP <-.
+  rewrite sum_nat_cond_const mulnC eqn_pmul2l //; move/eqP <-.
   rewrite addSnnS prednK // -cardZcl -[card _](cardsID Zcl) /= addnC.
   by congr (_ + _)%N; apply: eq_card => t; rewrite !inE andbC // andbAC andbb.
 have fful_nlin i: i \in ~: linS -> mx_faithful (irr_repr i).
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index f108ff9..bcc1f7e 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -786,6 +786,9 @@ Section SeqExtension.
 
 Variable I : Type.
 
+Lemma foldrE r : foldr op idx r = \big[op/idx]_(x <- r) x.
+Proof. by rewrite unlock. Qed.
+
 Lemma big_filter r (P : pred I) F :
   \big[op/idx]_(i <- filter P r) F i = \big[op/idx]_(i <- r | P i) F i.
 Proof. by rewrite unlock; elim: r => //= i r <-; case (P i). Qed.
@@ -878,6 +881,11 @@ Proof. by rewrite unlock; elim: r => //= i r ->; case: (P i). Qed.
 
 End SeqExtension.
 
+Lemma big_map_id J (h : J -> R) r (P : pred R) :
+  \big[op/idx]_(i <- map h r | P i) i
+     = \big[op/idx]_(j <- r | P (h j)) h j.
+Proof. exact: big_map. Qed.
+
 (* The following lemmas can be used to localise extensionality to a specific  *)
 (* index sequence. This is done by ssreflect rewriting, before applying       *)
 (* congruence or induction lemmas.                                            *)
@@ -1085,6 +1093,24 @@ Lemma big_nseq I n a (F : I -> R):
   \big[op/idx]_(i <- nseq n a) F i = iter n (op (F a)) idx.
 Proof. exact: big_nseq_cond. Qed.
 
+Lemma big_image_cond I (J : finType) (h : J -> I) (A : pred J) (P : pred I) F :
+  \big[op/idx]_(i <- [seq h j | j in A] | P i) F i
+     = \big[op/idx]_(j in A | P (h j)) F (h j).
+Proof. by rewrite big_map big_filter_cond. Qed.
+
+Lemma big_image I (J : finType) (h : J -> I) (A : pred J) F :
+  \big[op/idx]_(i <- [seq h j | j in A]) F i = \big[op/idx]_(j in A) F (h j).
+Proof. by rewrite big_map big_filter. Qed.
+
+Lemma big_image_cond_id (J : finType) (h : J -> R) (A : pred J) (P : pred R) :
+  \big[op/idx]_(i <- [seq h j | j in A] | P i) i
+     = \big[op/idx]_(j in A | P (h j)) h j.
+Proof. exact: big_image_cond. Qed.
+
+Lemma big_image_id (J : finType) (h : J -> R) (A : pred J) :
+  \big[op/idx]_(i <- [seq h j | j in A]) i = \big[op/idx]_(j in A) h j.
+Proof. exact: big_image. Qed.
+
 End Extensionality.
 
 Section MonoidProperties.
@@ -1103,6 +1129,14 @@ Variable op : Monoid.law 1.
 Local Notation "*%M" := op (at level 0).
 Local Notation "x * y" := (op x y).
 
+Lemma foldlE x r : foldl *%M x r = \big[*%M/1]_(y <- x :: r) y.
+Proof.
+by rewrite -foldrE; elim: r => [|y r IHr]/= in x *; rewrite ?mulm1 ?mulmA ?IHr.
+Qed.
+
+Lemma foldl_idx r : foldl *%M 1 r = \big[*%M/1]_(x <- r) x.
+Proof. by rewrite foldlE big_cons mul1m. Qed.
+
 Lemma eq_big_idx_seq idx' I r (P : pred I) F :
      right_id idx' *%M -> has P r ->
    \big[*%M/idx']_(i <- r | P i) F i =\big[*%M/1]_(i <- r | P i) F i.
@@ -1327,7 +1361,7 @@ by apply: big_pred1 => i; rewrite /= andbC; case: eqP => // ->.
 Qed.
 Arguments bigD1 [I] j [P F].
 
-Lemma bigD1_seq (I : eqType) (r : seq I) j F : 
+Lemma bigD1_seq (I : eqType) (r : seq I) j F :
     j \in r -> uniq r ->
   \big[*%M/1]_(i <- r) F i = F j * \big[*%M/1]_(i <- r | i != j) F i.
 Proof. by move=> /big_rem-> /rem_filter->; rewrite big_filter. Qed.
@@ -1687,6 +1721,8 @@ Proof. by rewrite big_const_nat -Monoid.iteropE. Qed.
 
 End NatConst.
 
+Lemma sumnE r : sumn r = \sum_(i <- r) i. Proof. exact: foldrE. Qed.
+
 Lemma leqif_sum (I : finType) (P C : pred I) (E1 E2 : I -> nat) :
     (forall i, P i -> E1 i <= E2 i ?= iff C i) ->
   \sum_(i | P i) E1 i <= \sum_(i | P i) E2 i ?= iff [forall (i | P i), C i].
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v
index 98ee64e..1f0ae16 100644
--- a/mathcomp/ssreflect/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
@@ -387,7 +387,7 @@ have [ltTk | lekT] := ltnP #|B| k.
   have [AsubB /=|//] := boolP (A \subset B).
   by rewrite (leq_ltn_trans (subset_leq_card AsubB)) ?andbF.
 apply/eqP; rewrite -(eqn_pmul2r (fact_gt0 k)) bin_ffact // eq_sym.
-rewrite -sum_nat_dep_const -{1 3}(card_ord k).
+rewrite -sum_nat_cond_const -{1 3}(card_ord k).
 rewrite -card_inj_ffuns_on -sum1dep_card.
 pose imIk (f : {ffun 'I_k -> T}) := f @: 'I_k.
 rewrite (partition_big imIk (fun A => (A \subset B) && (#|A| == k))) /=
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 87d5da4..8e174c0 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -717,7 +717,7 @@ Proof. exact/eq_card/in_set. Qed.
 Lemma sum1dep_card pA : \sum_(x | pA x) 1 = #|[set x | pA x]|.
 Proof. by rewrite sum1_card cardsE. Qed.
 
-Lemma sum_nat_dep_const pA n : \sum_(x | pA x) n = #|[set x | pA x]| * n.
+Lemma sum_nat_cond_const pA n : \sum_(x | pA x) n = #|[set x | pA x]| * n.
 Proof. by rewrite sum_nat_const cardsE. Qed.
 
 Lemma cards0 : #|@set0 T| = 0.
@@ -1380,24 +1380,21 @@ Proof. by apply: big_pred0 => i; rewrite inE. Qed.
 Lemma big_set1 a F : \big[op/idx]_(i in [set a]) F i = F a.
 Proof. by apply: big_pred1 => i; rewrite !inE. Qed.
 
-Lemma big_setIDdep A B P F :
-  \big[aop/idx]_(i in A | P i) F i =
-     aop (\big[aop/idx]_(i in A :&: B | P i) F i)
-         (\big[aop/idx]_(i in A :\: B | P i) F i).
-Proof.
-rewrite (bigID (mem B)) setDE.
-by congr (aop _ _); apply: eq_bigl => i; rewrite !inE andbAC.
-Qed.
-
 Lemma big_setID A B F :
   \big[aop/idx]_(i in A) F i =
      aop (\big[aop/idx]_(i in A :&: B) F i)
          (\big[aop/idx]_(i in A :\: B) F i).
 Proof.
-rewrite (bigID (mem B)) !(eq_bigl _ _ (in_set _)) //=.
-by congr (aop _); apply: eq_bigl => i; rewrite andbC.
+rewrite (bigID (mem B)) setDE.
+by congr (aop _ _); apply: eq_bigl => i; rewrite !inE.
 Qed.
 
+Lemma big_setIDcond A B P F :
+  \big[aop/idx]_(i in A | P i) F i =
+     aop (\big[aop/idx]_(i in A :&: B | P i) F i)
+         (\big[aop/idx]_(i in A :\: B | P i) F i).
+Proof. by rewrite !big_mkcondr; apply: big_setID. Qed.
+
 Lemma big_setD1 a A F : a \in A ->
   \big[aop/idx]_(i in A) F i = aop (F a) (\big[aop/idx]_(i in A :\ a) F i).
 Proof.
@@ -1409,8 +1406,7 @@ Lemma big_setU1 a A F : a \notin A ->
   \big[aop/idx]_(i in a |: A) F i = aop (F a) (\big[aop/idx]_(i in A) F i).
 Proof. by move=> notAa; rewrite (@big_setD1 a) ?setU11 //= setU1K. Qed.
 
-Lemma big_imset h (A : pred I) G :
-     {in A &, injective h} ->
+Lemma big_imset h (A : pred I) G : {in A &, injective h} ->
   \big[aop/idx]_(j in h @: A) G j = \big[aop/idx]_(i in A) G (h i).
 Proof.
 move=> injh; pose hA := mem (image h A).
@@ -1427,6 +1423,11 @@ symmetry; rewrite (negbTE nhAhi); apply/idP=> Ai.
 by case/imageP: nhAhi; exists i.
 Qed.
 
+Lemma big_imset_cond h (A : pred I) (P : pred J) G : {in A &, injective h} ->
+  \big[aop/idx]_(j in h @: A | P j) G j =
+    \big[aop/idx]_(i in A | P (h i)) G (h i).
+Proof. by move=> h_inj; rewrite 2!big_mkcondr big_imset. Qed.
+
 Lemma partition_big_imset h (A : pred I) F :
   \big[aop/idx]_(i in A) F i =
      \big[aop/idx]_(j in h @: A) \big[aop/idx]_(i in A | h i == j) F i.