From 948dec69615691de382278609a5b130ad5a485d3 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 4 Jul 2018 17:34:17 +0200 Subject: Improving fintype and bigop ### Added - Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`, `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`. - Bigop theorems: `big_rmcond`, `bigD1_seq`, `reindex_enum_val_cond`, `reindex_enum_rank_cond`, `reindex_enum_val`, `reindex_enum_rank`, `big_set`. --- CHANGELOG.md | 7 +++++++ mathcomp/ssreflect/bigop.v | 45 ++++++++++++++++++++++++++++++++++++++++++++ mathcomp/ssreflect/finset.v | 4 ++++ mathcomp/ssreflect/fintype.v | 43 ++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 99 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index f8c3221..1cdf035 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -29,6 +29,13 @@ versions may be dropped. - computing (efficiently) (item, multiplicity) tallies of sequences over an `eqType`: `tally s`, `incr_tally bs x`, `bs \is a wf_tally`, `tally_seq bs`. +- 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 - definition of `PredType` which now takes only a `P -> pred T` function; diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 67e9c4b..dc6be74 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 reindex_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 reindex_enum_val_cond [I A] P F. + +Lemma reindex_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 reindex_enum_val_cond {}/h. +by apply: eq_big => [i|i Pi]; rewrite ?enum_valK_in. +Qed. +Arguments reindex_enum_rank_cond [I A x] xA P F. + +Lemma reindex_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 -(reindex_enum_val_cond predT) big_mkcondr. Qed. +Arguments reindex_enum_val [I A] F. + +Lemma reindex_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 (reindex_enum_rank_cond xA) big_mkcondr. Qed. +Arguments reindex_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 reindex_enum_val_cond [R idx op I A] P F. +Arguments reindex_enum_rank_cond [R idx op I A x] xA P F. +Arguments reindex_enum_val [R idx op I A] F. +Arguments reindex_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}. -- cgit v1.2.3 From 115a253d125015e7622f94c92fbf3d00f5f77e20 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 23 May 2019 17:33:43 +0200 Subject: renaming new `reindex_` lemmas with prefix `big_` --- mathcomp/ssreflect/bigop.v | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index dc6be74..adb4094 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1433,7 +1433,7 @@ 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 reindex_enum_val_cond (I : finType) (A : pred I) (P : pred I) 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. @@ -1444,27 +1444,27 @@ 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 reindex_enum_val_cond [I A] P F. +Arguments big_enum_val_cond [I A] P F. -Lemma reindex_enum_rank_cond (I : finType) (A : pred I) x (xA : x \in 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 reindex_enum_val_cond {}/h. +rewrite big_enum_val_cond {}/h. by apply: eq_big => [i|i Pi]; rewrite ?enum_valK_in. Qed. -Arguments reindex_enum_rank_cond [I A x] xA P F. +Arguments big_enum_rank_cond [I A x] xA P F. -Lemma reindex_enum_val (I : finType) (A : pred I) 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 -(reindex_enum_val_cond predT) big_mkcondr. Qed. -Arguments reindex_enum_val [I A] F. +Proof. by rewrite -(big_enum_val_cond predT) big_mkcondr. Qed. +Arguments big_enum_val [I A] F. -Lemma reindex_enum_rank (I : finType) (A : pred I) x (xA : x \in 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 (reindex_enum_rank_cond xA) big_mkcondr. Qed. -Arguments reindex_enum_rank [I A x] xA F. +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 @@ -1588,10 +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 reindex_enum_val_cond [R idx op I A] P F. -Arguments reindex_enum_rank_cond [R idx op I A x] xA P F. -Arguments reindex_enum_val [R idx op I A] F. -Arguments reindex_enum_rank [R idx op I A x] xA 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]. -- cgit v1.2.3 From 530a208ba37e9b333a1bf9196e883657599d2917 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 16 Oct 2019 11:33:49 +0200 Subject: shifting to CHANGELOG_UNRELEASED --- CHANGELOG.md | 7 ------- CHANGELOG_UNRELEASED.md | 7 +++++++ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1cdf035..f8c3221 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -29,13 +29,6 @@ versions may be dropped. - computing (efficiently) (item, multiplicity) tallies of sequences over an `eqType`: `tally s`, `incr_tally bs x`, `bs \is a wf_tally`, `tally_seq bs`. -- 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 - definition of `PredType` which now takes only a `P -> pred T` function; 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 -- cgit v1.2.3