From 18edd0a87f8cc8bfd3a7c7aaaafa3d2cfdf5d165 Mon Sep 17 00:00:00 2001 From: Christian Doczkal Date: Tue, 5 May 2020 19:50:42 +0200 Subject: cardinality lemmas for #|A| <= 1 and n <= #|A| --- mathcomp/ssreflect/fintype.v | 49 ++++++++++++++++++++++++++++++++++++++++---- mathcomp/ssreflect/seq.v | 3 +++ 2 files changed, 48 insertions(+), 4 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index abed211..00823f6 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -624,13 +624,17 @@ 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). +Lemma card_le1_eqP A : + reflect {in A&, forall x, all_equal_to x} (#|A| <= 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. +apply: (iffP card_le1P) => [Ale1 x y xA yA /=|all_eq x xA y]. + by apply/eqP; rewrite -[_ == _]/(y \in pred1 x) -Ale1. +by rewrite inE; case: (altP (y =P x)) => [->//|]; exact/contra_neqF/all_eq. Qed. +Lemma fintype_le1P : reflect (forall x : T, all_equal_to x) (#|T| <= 1). +Proof. apply: (iffP (card_le1_eqP {:T})); [exact: in2T|exact: in2W]. 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. @@ -788,6 +792,39 @@ move=> eAB [C]; congr (_ && _); first exact: (eq_subset_r eAB). by rewrite (eq_subset eAB). Qed. +Lemma card_geqP {A n} : + reflect (exists s, [/\ uniq s, size s = n & {subset s <= A}]) (n <= #|A|). +Proof. +apply: (iffP idP) => [n_le_A|[s] [uniq_s size_s /subsetP subA]]; last first. + by rewrite -size_s -(card_uniqP _ uniq_s); exact: subset_leq_card. +exists (take n (enum A)); rewrite take_uniq ?enum_uniq // size_take. +split => //; last by move => x /mem_take; rewrite mem_enum. +case: (ltnP n (size (enum A))) => // size_A. +by apply/eqP; rewrite eqn_leq size_A -cardE n_le_A. +Qed. + +Lemma card_gt1P A : + reflect (exists x y, [/\ x \in A, y \in A & x != y]) (1 < #|A|). +Proof. +apply: (iffP card_geqP) => [[s] []|[x] [y] [xA yA xDy]]. +- case: s => [|a [|b [|]]] //=; rewrite inE andbT => aDb _ subD. + by exists a; exists b; rewrite aDb !subD ?inE ?eqxx ?orbT. +- exists [:: x;y]; rewrite /= !inE xDy ; split => // z. + by rewrite !inE; case/pred2P => ->. +Qed. + +Lemma card_gt2P A : + reflect (exists x y z, [/\ x \in A, y \in A & z \in A] /\ [/\ x!=y, y!=z & z!=x]) + (2 < #|A|). +Proof. +apply: (iffP card_geqP) => [[s] []|[x] [y] [z] [[xD yD zD] [xDy xDz yDz]]]. +- case: s => [|x [|y [|z [|]]]] //=; rewrite !inE !andbT negb_or -andbA. + case/and3P => xDy xDz yDz _ subA. + by exists x;exists y;exists z; rewrite xDy yDz eq_sym xDz !subA ?inE ?eqxx ?orbT. +- exists [:: x;y;z]; rewrite /= !inE negb_or xDy xDz eq_sym yDz; split => // u. + by rewrite !inE => /or3P [] /eqP->. +Qed. + Lemma disjoint_sym A B : [disjoint A & B] = [disjoint B & A]. Proof. by congr (_ == 0); apply: eq_card => x; apply: andbC. Qed. @@ -866,6 +903,7 @@ Hint Resolve subxx_hint : core. Arguments pred0P {T P}. Arguments pred0Pn {T P}. Arguments card_le1P {T A}. +Arguments card_le1_eqP {T A}. Arguments card1P {T A}. Arguments fintype_le1P {T}. Arguments fintype1P {T}. @@ -873,6 +911,9 @@ Arguments subsetP {T A B}. Arguments subsetPn {T A B}. Arguments subset_eqP {T A B}. Arguments card_uniqP {T s}. +Arguments card_geqP {T A n}. +Arguments card_gt1P {T A}. +Arguments card_gt2P {T A}. Arguments properP {T A B}. (**********************************************************************) diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 920f393..b202dd0 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -2008,6 +2008,9 @@ Proof. by rewrite -cats1 prefix_subseq. Qed. Lemma subseq_uniq s1 s2 : subseq s1 s2 -> uniq s2 -> uniq s1. Proof. by case/subseqP=> m _ -> Us2; apply: mask_uniq. Qed. +Lemma take_uniq s n : uniq s -> uniq (take n s). +Proof. exact/subseq_uniq/take_subseq. Qed. + End Subseq. Prenex Implicits subseq. -- cgit v1.2.3 From 1ac0240534077301fa837233b2a8e4bbeef119a8 Mon Sep 17 00:00:00 2001 From: Christian Doczkal Date: Wed, 13 May 2020 19:53:40 +0200 Subject: cards_eqP and cards2P --- mathcomp/ssreflect/finset.v | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index e608d2b..351c472 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -352,6 +352,9 @@ case: (pickP (mem A)) => [x Ax | A0]; [by right; exists x | left]. by apply/setP=> x; rewrite inE; apply: A0. Qed. +Lemma set_enum A : [set x | x \in enum A] = A. +Proof. by apply/setP => x; rewrite inE mem_enum. Qed. + Lemma enum_set0 : enum set0 = [::] :> seq T. Proof. by rewrite (eq_enum (in_set _)) enum0. Qed. @@ -817,11 +820,25 @@ Proof. by rewrite setDE subsetIr. Qed. Lemma sub1set A x : ([set x] \subset A) = (x \in A). Proof. by rewrite -subset_pred1; apply: eq_subset=> y; rewrite !inE. Qed. +Variant cards_eq_spec A : seq T -> {set T} -> nat -> Type := +| CardEq (s : seq T) & uniq s : cards_eq_spec A s [set x | x \in s] (size s). + +Lemma cards_eqP A : cards_eq_spec A (enum A) A #|A|. +Proof. +by move: (enum A) (cardE A) (set_enum A) (enum_uniq A) => s -> <-; constructor. +Qed. + Lemma cards1P A : reflect (exists x, A = [set x]) (#|A| == 1). Proof. apply: (iffP idP) => [|[x ->]]; last by rewrite cards1. -rewrite eq_sym eqn_leq card_gt0 => /andP[/set0Pn[x Ax] leA1]. -by exists x; apply/eqP; rewrite eq_sym eqEcard sub1set Ax cards1 leA1. +by have [[|x []]// _] := cards_eqP; exists x; apply/setP => y; rewrite !inE. +Qed. + +Lemma cards2P A : reflect (exists x y : T, x != y /\ A = [set x; y]) (#|A| == 2). +Proof. +apply: (iffP idP) => [|[x] [y] [xy ->]]; last by rewrite cards2 xy. +have [[|x [|y []]]//=] := cards_eqP; rewrite !inE andbT => neq_xy. +by exists x, y; split=> //; apply/setP => z; rewrite !inE. Qed. Lemma subset1 A x : (A \subset [set x]) = (A == [set x]) || (A == set0). -- cgit v1.2.3 From 5b4b9ad71794cc68f9c94520e91fd8ab56a5b577 Mon Sep 17 00:00:00 2001 From: Christian Doczkal Date: Tue, 26 May 2020 12:01:50 +0200 Subject: add fcard_gt?P lemmas found in fourcolor --- mathcomp/ssreflect/fingraph.v | 20 ++++++++++++++++++++ mathcomp/ssreflect/fintype.v | 1 + 2 files changed, 21 insertions(+) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index 9fb79a2..b8231ac 100644 --- a/mathcomp/ssreflect/fingraph.v +++ b/mathcomp/ssreflect/fingraph.v @@ -608,6 +608,26 @@ Proof. by apply: same_connect1 => /=. Qed. Lemma same_fconnect1_r x y : fconnect f x y = fconnect f x (f y). Proof. by apply: same_connect1r x => /=. Qed. +Lemma fcard_gt0P (a : {pred T}) : + fclosed f a -> reflect (exists x, x \in a) (0 < fcard f a). +Proof. +move => clfA; apply: (iffP card_gt0P) => [[x /andP[]]|[x xA]]; first by exists x. +exists (froot f x); rewrite inE roots_root /=; last exact: fconnect_sym. +by rewrite -(closed_connect clfA (connect_root _ x)). +Qed. + +Lemma fcard_gt1P (A : {pred T}) : + fclosed f A -> + reflect (exists2 x, x \in A & exists2 y, y \in A & ~~ fconnect f x y) + (1 < fcard f A). +Proof. +move=> clAf; apply: (iffP card_gt1P) => [|[x] [xA [y yA not_xfy]]]. + move => [x] [y] [/andP [/= rfx xA]] [/andP[/= rfy yA] xDy]. + by exists x; try exists y; rewrite // -root_connect // (eqP rfx) (eqP rfy). +exists (froot f x), (froot f y); rewrite !inE !roots_root ?root_connect //=. +by split => //; rewrite -(closed_connect clAf (connect_root _ _)). +Qed. + End orbit_inj. Hint Resolve orbit_uniq : core. diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 00823f6..05c5547 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -912,6 +912,7 @@ Arguments subsetPn {T A B}. Arguments subset_eqP {T A B}. Arguments card_uniqP {T s}. Arguments card_geqP {T A n}. +Arguments card_gt0P {T A}. Arguments card_gt1P {T A}. Arguments card_gt2P {T A}. Arguments properP {T A B}. -- cgit v1.2.3 From 96efc4fa2a3b643c6c4ea19047c3e633c5af145f Mon Sep 17 00:00:00 2001 From: Christian Doczkal Date: Sun, 7 Jun 2020 11:17:14 +0200 Subject: drop_uniq / CHANGELOG --- mathcomp/ssreflect/seq.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index b202dd0..dec68a3 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -2011,6 +2011,9 @@ Proof. by case/subseqP=> m _ -> Us2; apply: mask_uniq. Qed. Lemma take_uniq s n : uniq s -> uniq (take n s). Proof. exact/subseq_uniq/take_subseq. Qed. +Lemma drop_uniq s n : uniq s -> uniq (drop n s). +Proof. exact/subseq_uniq/drop_subseq. Qed. + End Subseq. Prenex Implicits subseq. -- cgit v1.2.3 From 555655f227c4d154f72b352b3437a1c275be2920 Mon Sep 17 00:00:00 2001 From: Christian Doczkal Date: Sun, 7 Jun 2020 11:08:38 +0200 Subject: Apply suggestions from code review Co-authored-by: Cyril Cohen --- mathcomp/ssreflect/fingraph.v | 4 ++-- mathcomp/ssreflect/fintype.v | 20 ++++++++++---------- 2 files changed, 12 insertions(+), 12 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index b8231ac..d1376d0 100644 --- a/mathcomp/ssreflect/fingraph.v +++ b/mathcomp/ssreflect/fingraph.v @@ -611,7 +611,7 @@ Proof. by apply: same_connect1r x => /=. Qed. Lemma fcard_gt0P (a : {pred T}) : fclosed f a -> reflect (exists x, x \in a) (0 < fcard f a). Proof. -move => clfA; apply: (iffP card_gt0P) => [[x /andP[]]|[x xA]]; first by exists x. +move=> clfA; apply: (iffP card_gt0P) => [[x /andP[]]|[x xA]]; first by exists x. exists (froot f x); rewrite inE roots_root /=; last exact: fconnect_sym. by rewrite -(closed_connect clfA (connect_root _ x)). Qed. @@ -622,7 +622,7 @@ Lemma fcard_gt1P (A : {pred T}) : (1 < fcard f A). Proof. move=> clAf; apply: (iffP card_gt1P) => [|[x] [xA [y yA not_xfy]]]. - move => [x] [y] [/andP [/= rfx xA]] [/andP[/= rfy yA] xDy]. + move=> [x] [y] [/andP [/= rfx xA]] [/andP[/= rfy yA] xDy]. by exists x; try exists y; rewrite // -root_connect // (eqP rfx) (eqP rfy). exists (froot f x), (froot f y); rewrite !inE !roots_root ?root_connect //=. by split => //; rewrite -(closed_connect clAf (connect_root _ _)). diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 05c5547..986d9fd 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -625,7 +625,7 @@ by apply: (iffP idP) => [/eqP/mem_card1[x inA]|[x /eq_card1/eqP//]]; exists x. Qed. Lemma card_le1_eqP A : - reflect {in A&, forall x, all_equal_to x} (#|A| <= 1). + reflect {in A &, forall x, all_equal_to x} (#|A| <= 1). Proof. apply: (iffP card_le1P) => [Ale1 x y xA yA /=|all_eq x xA y]. by apply/eqP; rewrite -[_ == _]/(y \in pred1 x) -Ale1. @@ -633,7 +633,7 @@ by rewrite inE; case: (altP (y =P x)) => [->//|]; exact/contra_neqF/all_eq. Qed. Lemma fintype_le1P : reflect (forall x : T, all_equal_to x) (#|T| <= 1). -Proof. apply: (iffP (card_le1_eqP {:T})); [exact: in2T|exact: in2W]. Qed. +Proof. apply: (iffP (card_le1_eqP {:T})); [exact: in2T | exact: in2W]. Qed. Lemma fintype1 : #|T| = 1 -> {x : T | all_equal_to x}. Proof. @@ -807,10 +807,10 @@ Lemma card_gt1P A : reflect (exists x y, [/\ x \in A, y \in A & x != y]) (1 < #|A|). Proof. apply: (iffP card_geqP) => [[s] []|[x] [y] [xA yA xDy]]. -- case: s => [|a [|b [|]]] //=; rewrite inE andbT => aDb _ subD. - by exists a; exists b; rewrite aDb !subD ?inE ?eqxx ?orbT. -- exists [:: x;y]; rewrite /= !inE xDy ; split => // z. - by rewrite !inE; case/pred2P => ->. + case: s => [|a [|b []]]//=; rewrite inE andbT => aDb _ subD. + by exists a, b; rewrite aDb !subD ?inE ?eqxx ?orbT. +exists [:: x; y]; rewrite /= !inE xDy. +by split=> // z; rewrite !inE => /pred2P[]->. Qed. Lemma card_gt2P A : @@ -818,11 +818,11 @@ Lemma card_gt2P A : (2 < #|A|). Proof. apply: (iffP card_geqP) => [[s] []|[x] [y] [z] [[xD yD zD] [xDy xDz yDz]]]. -- case: s => [|x [|y [|z [|]]]] //=; rewrite !inE !andbT negb_or -andbA. + case: s => [|x [|y [|z []]]]//=; rewrite !inE !andbT negb_or -andbA. case/and3P => xDy xDz yDz _ subA. - by exists x;exists y;exists z; rewrite xDy yDz eq_sym xDz !subA ?inE ?eqxx ?orbT. -- exists [:: x;y;z]; rewrite /= !inE negb_or xDy xDz eq_sym yDz; split => // u. - by rewrite !inE => /or3P [] /eqP->. + by exists x, y, z; rewrite xDy yDz eq_sym xDz !subA ?inE ?eqxx ?orbT. +exists [:: x; y; z]; rewrite /= !inE negb_or xDy xDz eq_sym yDz; split=> // u. +by rewrite !inE => /or3P [] /eqP->. Qed. Lemma disjoint_sym A B : [disjoint A & B] = [disjoint B & A]. -- cgit v1.2.3 From c5008933e4f17c122a0b23e6e6cfe8d198423214 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Jun 2020 14:09:03 +0200 Subject: fixup spacing --- mathcomp/ssreflect/fintype.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 986d9fd..3705530 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -814,7 +814,7 @@ by split=> // z; rewrite !inE => /pred2P[]->. Qed. Lemma card_gt2P A : - reflect (exists x y z, [/\ x \in A, y \in A & z \in A] /\ [/\ x!=y, y!=z & z!=x]) + reflect (exists x y z, [/\ x \in A, y \in A & z \in A] /\ [/\ x != y, y != z & z != x]) (2 < #|A|). Proof. apply: (iffP card_geqP) => [[s] []|[x] [y] [z] [[xD yD zD] [xDy xDz yDz]]]. -- cgit v1.2.3 From 7fd6f9ba051ecc7be7bd95ca3e31bb1a798598ba Mon Sep 17 00:00:00 2001 From: Christian Doczkal Date: Thu, 18 Jun 2020 11:19:03 +0200 Subject: conform to 80 chars limit --- mathcomp/ssreflect/finset.v | 3 ++- mathcomp/ssreflect/fintype.v | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 351c472..f4c1dd5 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -834,7 +834,8 @@ apply: (iffP idP) => [|[x ->]]; last by rewrite cards1. by have [[|x []]// _] := cards_eqP; exists x; apply/setP => y; rewrite !inE. Qed. -Lemma cards2P A : reflect (exists x y : T, x != y /\ A = [set x; y]) (#|A| == 2). +Lemma cards2P A : reflect (exists x y : T, x != y /\ A = [set x; y]) + (#|A| == 2). Proof. apply: (iffP idP) => [|[x] [y] [xy ->]]; last by rewrite cards2 xy. have [[|x [|y []]]//=] := cards_eqP; rewrite !inE andbT => neq_xy. diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 3705530..7e440ab 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -814,7 +814,8 @@ by split=> // z; rewrite !inE => /pred2P[]->. Qed. Lemma card_gt2P A : - reflect (exists x y z, [/\ x \in A, y \in A & z \in A] /\ [/\ x != y, y != z & z != x]) + reflect (exists x y z, + [/\ x \in A, y \in A & z \in A] /\ [/\ x != y, y != z & z != x]) (2 < #|A|). Proof. apply: (iffP card_geqP) => [[s] []|[x] [y] [z] [[xD yD zD] [xDy xDz yDz]]]. -- cgit v1.2.3