Card lemmas #509

chdoc · 2020-05-14T18:11:59Z

Motivation for this change

Additional lemmas about cardinalities of predicates and sets. Mainly picking n distinct elements for an a predicate with n <= #|A|.

Things done/to do

added corresponding entries in CHANGELOG_UNRELEASED.md
~~added corresponding documentation in the headers~~

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

CohenCyril · 2020-05-14T20:22:03Z

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 :


In thought I did that one when I added fintype_le1P tomorrow. 😆 I will double check tomorrow, if I forgot to push something.

CohenCyril · 2020-05-14T20:28:17Z

mathcomp/ssreflect/finset.v

@@ -824,6 +824,16 @@ 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.
 Qed.

+Lemma cards2P A : reflect (exists x y : T, x != y /\ A = [set x;y]) (#|A| == 2).


Nice one to have indeed, I think there is a lot of refactoring to do with all the card_* lemma you added, through enum (which is uniq which size is the cardinal of the considered set). Indeed, I think card_eqP would be almost a one liner and card_geqP, and cards2P is a simple twice case analysis (the main step being something like case: (enum A) (enum_uniq A) (size_enum A) => [|x [|y []]//; exists x; exists y).
I also think it would be nice to have le/lt variants and pred variants.

I'm not sure I follow. There is no card_eqP (yet) and indeed I'm not sure that would be useful, since enum A has already good lemma support. And card_geqP is about encapsulating the picking of a subsequence of enum A, if one only has a lower bound.
Admittedly, using the _gt?P lemmas to prove cards2P may be overkill.

Here is an elaboration of what I had in mind:

Lemma set_enum A : [set x | x \in enum A] = A. Proof. by apply/setP => x; rewrite inE mem_enum. 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. 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.

and something like this for fintype...

And card_geqP is about encapsulating the picking of a subsequence of enum A, if one only has a lower bound.

Indeed, I missed that...

Okay, for {set _} what you propose is indeed more general and more direct than what I had proposed. However, I'm not sure it transfers all that well to predicates: due to the lack of extensionality, one cannot pull the [set x | x \in enum A] trick. One could instead generate s =i A as an assumption, but I'm not sure this view would be all that useful.

The same goes for lower bounds, albeit for a different reason: there one doesn't even want to replace the original predicate/set.

chdoc · 2020-05-26T10:14:05Z

I tried to incorporate the feedback from @CohenCyril , and I found two more lemmas fcard_gt0P and fcard_gt1P. The proof of the latter naturally makes use of card_gt1P. These are adapted/simplified from the fourcolor development, where one can find a specific instance for each of them (fcard0P and fcard1P).

CohenCyril

LGTM, except for minor proof style or spacing issues.
I made many code suggestions to point them out with a suggest fix, which I did not test

mathcomp/ssreflect/seq.v

mathcomp/ssreflect/fintype.v

mathcomp/ssreflect/fingraph.v

mathcomp/ssreflect/fintype.v

mathcomp/ssreflect/fingraph.v

mathcomp/ssreflect/fintype.v

chdoc · 2020-06-17T12:21:23Z

I wasn't sure about this, because the line already had 82 characters, now it gained another 6. And yes, I want a linter, too. 😄

CohenCyril · 2020-06-17T12:25:43Z

I wasn't sure about this, because the line already had 82 characters, now it gained another 6. And yes, I want a linter, too.

Oh ok, I should really checkout locally.
In the core mathcomp repo there is a strict rule about the 80 characters per line limit. So this line should be split anyway.

still some typesetting to do

chdoc · 2020-06-17T12:31:18Z

Well, running a grep -n '.\{81\}' ssreflect/*.v made me believe that the rule is not that strict.

CohenCyril · 2020-06-17T12:33:42Z

Well, running a grep -n '.\{81\}' ssreflect/*.v made me believe that the rule is not that strict.

It used to be, this is outrageous 😉
I will revive #163 ASAP.

Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>

CohenCyril

Yeay, LGTM now!

CohenCyril reviewed May 14, 2020

View reviewed changes

affeldt-aist added this to the 1.12.0 milestone May 15, 2020

CohenCyril requested changes Jun 7, 2020

View reviewed changes

coqbot added the needs: rebase PR which is not rebased: check the target is appropriate (generally master) and rebase on top of it. label Jun 7, 2020

chdoc force-pushed the card-lemmas branch from 50ac347 to 88d7045 Compare June 7, 2020 09:30

coqbot removed the needs: rebase PR which is not rebased: check the target is appropriate (generally master) and rebase on top of it. label Jun 7, 2020

chdoc requested a review from CohenCyril June 7, 2020 12:35

CohenCyril reviewed Jun 8, 2020

View reviewed changes

mathcomp/ssreflect/fingraph.v Outdated Show resolved Hide resolved

CohenCyril reviewed Jun 8, 2020

View reviewed changes

mathcomp/ssreflect/fintype.v Outdated Show resolved Hide resolved

coqbot added the needs: rebase PR which is not rebased: check the target is appropriate (generally master) and rebase on top of it. label Jun 17, 2020

chdoc force-pushed the card-lemmas branch from 4f8b8b1 to fef9904 Compare June 17, 2020 09:45

coqbot removed the needs: rebase PR which is not rebased: check the target is appropriate (generally master) and rebase on top of it. label Jun 17, 2020

CohenCyril reviewed Jun 17, 2020

View reviewed changes

mathcomp/ssreflect/fintype.v Outdated Show resolved Hide resolved

CohenCyril previously approved these changes Jun 17, 2020

View reviewed changes

CohenCyril added kind: enhancement Issue or PR about addition of features. kind: refactoring Issue or PR about a refactoring. (reorganizing the code, reusing theorems, simplifications...) labels Jun 17, 2020

coqbot added the needs: rebase PR which is not rebased: check the target is appropriate (generally master) and rebase on top of it. label Jun 18, 2020

chdoc and others added 6 commits June 18, 2020 16:45

cardinality lemmas for #|A| <= 1 and n <= #|A|

18edd0a

cards_eqP and cards2P

1ac0240

add fcard_gt?P lemmas found in fourcolor

5b4b9ad

drop_uniq / CHANGELOG

96efc4f

Apply suggestions from code review

555655f

Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>

fixup spacing

c500893

conform to 80 chars limit

7fd6f9b

chdoc force-pushed the card-lemmas branch from 58990ac to 7fd6f9b Compare June 18, 2020 14:46

coqbot removed the needs: rebase PR which is not rebased: check the target is appropriate (generally master) and rebase on top of it. label Jun 18, 2020

CohenCyril approved these changes Jun 19, 2020

View reviewed changes

CohenCyril merged commit f25ef67 into math-comp:master Jun 19, 2020

chdoc mentioned this pull request Jun 26, 2020

fix "Nothing to inject" warnings #542

Merged

2 tasks

chdoc deleted the card-lemmas branch June 30, 2020 11:43

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Card lemmas #509

Card lemmas #509

chdoc commented May 14, 2020

CohenCyril May 14, 2020

CohenCyril May 14, 2020 •

edited

chdoc May 15, 2020

CohenCyril May 15, 2020 •

edited

CohenCyril May 15, 2020

chdoc May 19, 2020

chdoc commented May 26, 2020

CohenCyril left a comment

chdoc commented Jun 17, 2020

CohenCyril commented Jun 17, 2020

chdoc commented Jun 17, 2020

CohenCyril commented Jun 17, 2020 •

edited

CohenCyril left a comment

Card lemmas #509

Card lemmas #509

Conversation

chdoc commented May 14, 2020

Motivation for this change

Things done/to do

Automatic note to reviewers

CohenCyril May 14, 2020

Choose a reason for hiding this comment

CohenCyril May 14, 2020 • edited

Choose a reason for hiding this comment

chdoc May 15, 2020

Choose a reason for hiding this comment

CohenCyril May 15, 2020 • edited

Choose a reason for hiding this comment

CohenCyril May 15, 2020

Choose a reason for hiding this comment

chdoc May 19, 2020

Choose a reason for hiding this comment

chdoc commented May 26, 2020

CohenCyril left a comment

Choose a reason for hiding this comment

chdoc commented Jun 17, 2020

CohenCyril commented Jun 17, 2020

chdoc commented Jun 17, 2020

CohenCyril commented Jun 17, 2020 • edited

CohenCyril left a comment

Choose a reason for hiding this comment

CohenCyril May 14, 2020 •

edited

CohenCyril May 15, 2020 •

edited

CohenCyril commented Jun 17, 2020 •

edited