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 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'mathcomp/ssreflect/fingraph.v') 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. -- 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 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mathcomp/ssreflect/fingraph.v') 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 _ _)). -- cgit v1.2.3