diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/fingraph.v | 20 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 22 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 51 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 6 |
4 files changed, 93 insertions, 6 deletions
diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index 9fb79a2..d1376d0 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/finset.v b/mathcomp/ssreflect/finset.v index e608d2b..f4c1dd5 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,26 @@ 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). diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index abed211..7e440ab 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,40 @@ 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, b; rewrite aDb !subD ?inE ?eqxx ?orbT. +exists [:: x; y]; rewrite /= !inE xDy. +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]) + (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, 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]. Proof. by congr (_ == 0); apply: eq_card => x; apply: andbC. Qed. @@ -866,6 +904,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 +912,10 @@ 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_gt0P {T A}. +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..dec68a3 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -2008,6 +2008,12 @@ 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. + +Lemma drop_uniq s n : uniq s -> uniq (drop n s). +Proof. exact/subseq_uniq/drop_subseq. Qed. + End Subseq. Prenex Implicits subseq. |