Merge pull request #509 from chdoc/card-lemmas

Card lemmas

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.