Add [in A] notation.

Add [in A] notation for fun x => x \in A, the natural applicative equivalent of a collective predicate A. Replace (mem A) and [mem A], which had a similar purpose but require an explicit /= or inE to turn mem A x to x \in A, which is sometimes awkward. Remove the Coq 8.10 compatibility code from ssrbool.v, which is actually incompatible with Coq < 8.13. Add lemmas for all and map: allT, all_mapT, inj_in_map, mapK_in.

Motivation for this change

The existing notation for passing a collective predicate A (e.g., a seq or finest) where an applicative one is expected (e.g, as arguments of all, filter or eq_bigl), namely [mem A] or (mem A), require an explicit simplification step to convert an application mem A x to the expected statement x \in A. This simplification step may be awkward when a simple /= would cause other unwanted simplification in the goal; indeed this is the reason for including a rule for expanding simpl_pred in the inE multi-rule. The new definition avoids this as [in A] x simply beta-reduces to x \in A. In addition, using the in keyword is more natural and meshes well with mathcomp functionals, e.g. all [in A] s or pick [in A]. Use of the new notation has been propagated to the whole library, including in ssrbool.v and eqtype.v notation such as [predD A & B] or [predU1 x & A]. Possible regression: non-? rewriting with inE intended to expand mem A x instances are now errors. There were only a few instances of this in all of mathcomp. An easy backward compatible fix in client libraries would be be to make such rewrites optional (i.e.,, rewrite ?inE). This PR also adds a few useful lemmas to seq.v, whose use had motivated the introduction of the [in A] notation:

• allT and all_mapT help prove instances of all with a predicate that always holds, on a possibly empty non-eqType.
• inj_in_map and mapK_in are localized versions of inj_map and mapK. Finally, this PR removes the Coq 8.10 compatibility code in ssrbool.v, which is outdated: it uses the name attribute in notations, which only works for Coq >= 8.13. The only use of that code in the mathcomp library was to provide the simp_rel >-> rel coercion under the alternative name rel_of_simpl_rel. This was fixed by replacing this with the rel_of_simpl name actually provided by ssr.ssrbool in the two instances (in eqtype.v and gseries.v) where it was used.

The[in A] notation should eventually be pushed to the Coq ssr library, but it seems prudent to see how often inE regressions occur in clients before doing so.

Things done/to do

• [X] added corresponding entries in CHANGELOG_UNRELEASED.md (do not edit former entries)
• [X] added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

Am I right that this is a backward compatible change? As long as client code does not start using [in A] and keep using mem A, they will not be impacted in anyway. If that's the case I do not see why not push the changes to Coq's ssrbool straight away.

As it stands, part of the change is not backward compatible : adding the new [in A] notation obviously is, but using it in the [predU A & B], [predI A & B], etc. notation is not. It breaks various fragile scripts that rely on rewrite inE of such notation exposing a mem A x (really pred_of_simpl (simpl_of_mem (mem A)) x) subterm, as explained the rationale. The PR fixes this in mathcomp proper, as do math-comp/odd-order#40 and coq-community/fourcolor#42 for odd-order and foucolor, respectively (in a backward compatible way), but CI also indicates a similar failure in graph-theory, for which I've yet to propose a fix (I'm not set up to compile it right now). It thus seems prudent to fix the clients before pushing the full PR to coq/ssrbool, though of course the definition of [in A] could be pushed immediately.

but CI also indicates a similar failure in graph-theory, for which I've yet to propose a fix (I'm not set up to compile it right now).

If needed, I can try to investigate and fix this next week, but I'm out of office until Tuesday.

This PR looks good to me except for the above minor suggestion and CI, but I have an impression that I don't understand Boolean predicates of MathComp deep enough. It is probably better if someone else can review it.

BTW, do we still want to keep [mem A]? When should we consider using it?

Is there some nix command that would allow me to quickly get to the context the CI will be in when trying to build graph-theory on top of this PR?

Is there some nix command that would allow me to quickly get to the context the CI will be in when trying to build graph-theory on top of this PR?

Run this in the current branch

nix-shell --no-out-link --argstr bundle "coq-8.14" --argstr job "graph-theory"

Then cd to your graph-theory workdir

It appears that in the part of graph-theory that is checked by the MathComp CI there is only one line that breaks.

I noticed that the Nix package used in the CI does not build the part that depends on fourcolor. In the opam package, fourcolor is an optional dependency (i.e., Wagner's theorem is only checked and installed if fourcolor is available).

What do I have to add to the nix-shell invocation in order to add the (cached) fourcolor run on PR #42 (the overlay for this PR)?

@ggonthier could you please rebase so that we could merge?

As discussed during the last meeting, we are planning to merge this PR. Before we merge, @chdoc could you test that graph-theory still compiles with this PR? (Since graph-theory requires the Four color theorem, the default CI test is only partial.)

@affeldt-aist in fact, since https://github.com/math-comp/math-comp/pull/956 we have a Nix CI overlay that tests it (long story short: they moved to dune in graph-theory master, which made make build unconditionally with fourcolor and broke the dev Nix derivation). So if CI is green, it's fine.

@affeldt-aist in fact, since #956 we have a Nix CI overlay that tests it (long story short: they moved to dune in graph-theory master, which made make build unconditionally with fourcolor and broke the dev Nix derivation). So if CI is green, it's fine.

Thanks for information. I missed it.

@affeldt-aist in fact, since #956 we have a Nix CI overlay that tests it (long story short: they moved to dune in graph-theory master, which made make build unconditionally with fourcolor and broke the dev Nix derivation). So if CI is green, it's fine.

~~AFAIU they released a 0.9.1 version with a separation between two packages graph-theory and graph-theory-planar, only the latter depends on fourcolor, I added it as a PR to nixpkgs and I started a job at https://github.com/coq-community/coq-nix-toolbox/pull/130 to test it... However there is an independent failure (about smtcoq) that might delay the integration here. We might either trust 0.9 results or make an overlay using my PR https://github.com/NixOS/nixpkgs/pull/211137~~

EDIT: I got it wrong about 0.9.1. So I restored the previous version but testing 0.9.1 with Coq >= 8.14

EDIT: I got it wrong about 0.9.1. So I restored the previous version but testing 0.9.1 with Coq >= 8.14

My understanding of .nix/config.nix is that the tested version is master.

Multinomials is failing now and I do not understand why, it didn't change since 2 days ago @proux01 @strub any hints?

@CohenCyril no idea, I'll have a look tomorrow.

@CohenCyril : so, the PR is changing the names of a few implicit arguments in seq.v. Here is an overlay for multinomials: https://github.com/math-comp/multinomials/pull/68 , I also updated the CHANGELOG to indicate the renamings. CI is now green.