backport ssrbool to Coq

[affeldt-aist]

Backport to Coq new contents from ssrbool.v (as introduced by PR #513 PR #519 PR #499 ).

https://github.com/affeldt-aist/coq/tree/ssrbool_backport_MathComp1.11
already contains an ssrbool.v file with an integration of PR #513, PR #519, and PR #499
and is ready to be PRed.

@CohenCyril @ybertot

(NB: this issue has been edited, it was mentioning ssrfun.v but its contents have already made their way to Coq)

[chdoc]

Note that PR #499, which is hopefully going to be merged soon, also includes additions to ssrbool.v. So you may want to hold off on this for a few more days.

[chdoc]

PR #499 has been merged.

[affeldt-aist]

PR #499 has been merged.

Thank you for letting me know. I have updated the tentative backport accordingly.

[chdoc]

Maybe the contra lemmas should be integrated with the other contra lemmas already present in that file, i.e., somewhere around this line. Possibly the whole set of lemmas could be wrapped in a section with the appropriate Implicit Types ... command.

[pi8027]

I hope this will be done before the feature freeze of Coq 8.13, which is 15 Nov. (see coq/coq#12334)

[CohenCyril]

Wasn't this fixed in coq/coq#12898?

[pi8027]

I was not aware of that, but it does not seem to include #552.

[CohenCyril]

I was not aware of that, but it does not seem to include #552.

I think it doesn't need to, it was a problem specific to ssrbool.v on mathcomp side, @chdoc looked at this more closely than I did, am I right @chdoc?

[chdoc]

Yes, the problem was/is that recent versions of ssr.ssrbool.v declare a reserved notation for [rel _ _ : _ | _] (rel with explicit typing) with a particular printing format. Prior to the fix, mathcomp was redeclaring this notation in ssreflect.ssrbool.v. However, one needs to give level information to please old versions of Coq that don't yet provide the reserved notation. This invalidates the preexisting format. Moreover, one cannot provide an equivalent format string at this point, because only parsing notations don't take format strings. Thus, mathcomp needs to repeat the Reserved Notation command for the time being, as this is the only way to declare only parsing notations with a particular format 😁

[pi8027]

I see. So shall we close here?

[affeldt-aist]

I think we can close. I forgot to do so when the backport was merged (coq/coq@40140bf, coq/coq@bfd384e, coq/coq@3405ab8).