Merge pull request #203 from CohenCyril/improving_fintype_bigop

Improving fintype and bigop

4 files changed, 99 insertions, 0 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index ee236d9..c03b4f8 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -23,6 +23,13 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 - Added theorems `flatten_map1` and `allpairs_consr` in `seq.v`.
 
+- Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`,
+  `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`.
+
+- Bigop theorems: `big_rmcond`, `bigD1_seq`,
+  `big_enum_val_cond`, `big_enum_rank_cond`,
+  `big_enum_val`, `big_enum_rank`, `big_set`.
+
 ### Changed
 
 - `eqVneq` lemma is changed from `{x = y} + {x != y}` to
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 67e9c4b..adb4094 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -1182,6 +1182,14 @@ Lemma big_mkcondl I r (P Q : pred I) F :
      \big[*%M/1]_(i <- r | Q i) (if P i then F i else 1).
 Proof. by rewrite big_andbC big_mkcondr. Qed.
 
+Lemma big_rmcond (I : eqType) (r : seq I) (P : pred I) F :
+  (forall i, i \in r -> ~~ P i -> F i = 1) ->
+  \big[*%M/1]_(i <- r | P i) F i = \big[*%M/1]_(i <- r) F i.
+Proof.
+move=> Fidx; rewrite big_mkcond big_seq_cond [in RHS]big_seq_cond ?big_mkcondr.
+by apply: eq_bigr => i /Fidx {Fidx}; case: (P i) => // ->.
+Qed.
+
 Lemma big_cat I r1 r2 (P : pred I) F :
   \big[*%M/1]_(i <- r1 ++ r2 | P i) F i =
      \big[*%M/1]_(i <- r1 | P i) F i * \big[*%M/1]_(i <- r2 | P i) F i.
@@ -1425,6 +1433,39 @@ Lemma reindex_inj (I : finType) (h : I -> I) (P : pred I) F :
 Proof. by move=> injh; apply: reindex (onW_bij _ (injF_bij injh)). Qed.
 Arguments reindex_inj [I h P F].
 
+Lemma big_enum_val_cond (I : finType) (A : pred I) (P : pred I) F :
+  \big[op/idx]_(x in A | P x) F x =
+  \big[op/idx]_(i < #|A| | P (enum_val i)) F (enum_val i).
+Proof.
+have [A_eq0|/card_gt0P[x0 x0A]] := posnP #|A|.
+  rewrite !big_pred0 // => i; last by rewrite card0_eq.
+  by have: false by move: i => []; rewrite A_eq0.
+rewrite (reindex (enum_val : 'I_#|A| -> I)).
+  by apply: eq_big => [x|x Px]; rewrite ?enum_valP.
+by apply: subon_bij (enum_val_bij_in x0A) => y /andP[].
+Qed.
+Arguments big_enum_val_cond [I A] P F.
+
+Lemma big_enum_rank_cond (I : finType) (A : pred I) x (xA : x \in A) P F
+  (h := enum_rank_in xA) :
+  \big[op/idx]_(i < #|A| | P i) F i = \big[op/idx]_(s in A | P (h s)) F (h s).
+Proof.
+rewrite big_enum_val_cond {}/h.
+by apply: eq_big => [i|i Pi]; rewrite ?enum_valK_in.
+Qed.
+Arguments big_enum_rank_cond [I A x] xA P F.
+
+Lemma big_enum_val (I : finType) (A : pred I) F :
+  \big[op/idx]_(x in A) F x = \big[op/idx]_(i < #|A|) F (enum_val i).
+Proof. by rewrite -(big_enum_val_cond predT) big_mkcondr. Qed.
+Arguments big_enum_val [I A] F.
+
+Lemma big_enum_rank (I : finType) (A : pred I) x (xA : x \in A) F
+  (h := enum_rank_in xA) :
+  \big[op/idx]_(i < #|A|) F i = \big[op/idx]_(s in A) F (h s).
+Proof. by rewrite (big_enum_rank_cond xA) big_mkcondr. Qed.
+Arguments big_enum_rank [I A x] xA F.
+
 Lemma big_nat_rev m n P F :
   \big[*%M/1]_(m <= i < n | P i) F i
      = \big[*%M/1]_(m <= i < n | P (m + n - i.+1)) F (m + n - i.+1).
@@ -1547,6 +1588,10 @@ Arguments partition_big [R idx op I J P] p Q [F].
 Arguments reindex_onto [R idx op I J] h h' [P F].
 Arguments reindex [R idx op I J] h [P F].
 Arguments reindex_inj [R idx op I h P F].
+Arguments big_enum_val_cond [R idx op I A] P F.
+Arguments big_enum_rank_cond [R idx op I A x] xA P F.
+Arguments big_enum_val [R idx op I A] F.
+Arguments big_enum_rank [R idx op I A x] xA F.
 Arguments pair_big_dep [R idx op I J].
 Arguments pair_big [R idx op I J].
 Arguments big_allpairs_dep [R idx op I1 I2 J h r1 r2 F].
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index beac009..fe85e35 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -1392,6 +1392,10 @@ 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_set (A : pred I) F :
+   \big[op/idx]_(i in [set i | A i]) (F i) = \big[op/idx]_(i in A) (F i).
+Proof. by apply: eq_bigl => i; rewrite inE. 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)
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index e58ae61..fdaf98f 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -590,6 +590,8 @@ Qed.
 Lemma card0_eq A : #|A| = 0 -> A =i pred0.
 Proof. by move=> A0 x; apply/idP => Ax; rewrite (cardD1 x) Ax in A0. Qed.
 
+Lemma fintype0 : T -> #|T| <> 0. Proof. by move=> x /card0_eq/(_ x). Qed.
+
 Lemma pred0P P : reflect (P =1 pred0) (pred0b P).
 Proof. by apply: (iffP eqP); [apply: card0_eq | apply: eq_card0]. Qed.
 
@@ -603,6 +605,43 @@ Qed.
 Lemma card_gt0P A : reflect (exists i, i \in A) (#|A| > 0).
 Proof. by rewrite lt0n; apply: pred0Pn. Qed.
 
+Lemma card_le1P {A} : reflect {in A, forall x, A =i pred1 x} (#|A| <= 1).
+Proof.
+apply: (iffP idP) => [A1 x xA y|]; last first.
+  by have [/= x xA /(_ _ xA)/eq_card1->|/eq_card0->//] := pickP (mem A).
+move: A1; rewrite (cardD1 x) xA ltnS leqn0 => /eqP/card0_eq/(_ y).
+by rewrite !inE; have [->|]:= eqP.
+Qed.
+
+Lemma mem_card1 A : #|A| = 1 -> {x | A =i pred1 x}.
+Proof.
+move=> A1; have /card_gt0P/sigW[x xA]: #|A| > 0 by rewrite A1.
+by exists x; apply/card_le1P; rewrite ?A1.
+Qed.
+
+Lemma card1P A : reflect (exists x, A =i pred1 x) (#|A| == 1).
+Proof.
+by apply: (iffP idP) => [/eqP/mem_card1[x inA]|[x /eq_card1/eqP//]]; exists x.
+Qed.
+
+Lemma fintype_le1P : reflect (forall x, all_equal_to x) (#|T| <= 1).
+Proof.
+apply: (iffP card_le1P)=> [inT x y|all_eq x _ y]; last first.
+  by rewrite (all_eq x) !inE eqxx.
+by suff: y \in T by rewrite (inT x)// => /eqP.
+Qed.
+
+Lemma fintype1 : #|T| = 1 -> {x : T | all_equal_to x}.
+Proof.
+by move=> /mem_card1[x ex]; exists x => y; suff: y \in T by rewrite ex => /eqP.
+Qed.
+
+Lemma fintype1P : reflect (exists x, all_equal_to x) (#|T| == 1).
+Proof.
+apply: (iffP idP) => [/eqP/fintype1|] [x eqx]; first by exists x.
+by apply/card1P; exists x => y; rewrite eqx !inE eqxx.
+Qed.
+
 Lemma subsetE A B : (A \subset B) = pred0b [predD A & B].
 Proof. by rewrite unlock. Qed.
 
@@ -828,6 +867,10 @@ Hint Resolve subxx_hint : core.
 
 Arguments pred0P {T P}.
 Arguments pred0Pn {T P}.
+Arguments card_le1P {T A}.
+Arguments card1P {T A}.
+Arguments fintype_le1P {T}.
+Arguments fintype1P {T}.
 Arguments subsetP {T A B}.
 Arguments subsetPn {T A B}.
 Arguments subset_eqP {T A B}.