fix notations for 8.20

[Alizter]

I've updated my local Coq version to 8.20 and have finally been able to address the outstanding warnings.

Many warnings were about various notations having the wrong levels. If two notations exist and one can be factored into the other, then they have to be in the same level. Otherwise, Coq just doesn't parse things correctly.

An example of this happening in practice was the infix ^ notation which was being used for powers by BinInt. Having this notation around broke ^ as a postfix path inversion operator. The solution was to remove this notation, which wasn't being used anyway.

The notation {{ _ | _ // _ }} used for the surreal numbers was causing quite a few problems due to how // was being factored. I didn't really know the best way to fix this, so I opted to just add another / to make it {{ _ | _ /// _ }}. This is a bit clunky, but doesn't appear to make readability worse. We might be able to choose something more sensible in the future.

[Alizter]

cc @proux01 who might be interested in these warnings appearing in practice.

[Alizter]

Hmm there appears to be a limitation in 8.19 where _ $== _ and _ $== _ :> _ cannot coexist without problems. In 8.20 this limitation appears to be lifted.

I guess we either wait for the 8.20 minimal version bump for this PR to be merged or comment out the problematic notation until 8.20.

[proux01]

Sounds strange, I thought we had that kind of thing everywhere.

[Alizter]

We have a similar set up with _ = _ and _ = _ :> _ that appears to work without problem. I'm not sure what is different in 8.19 that was changed in 8.20. FTR, the problematic file here is theories/WildCat/Monoidal.v.

[proux01]

That's indeed what I had in mind, strange.

[jdchristensen]

I'd like to keep the minimal Coq version at 8.19 for a little while, as I've just started teaching a class in which students will be using the library, and they currently have 8.19.x installed. (Also, one student mentioned that VSCode doesn't yet support 8.20.)

This could be merged without the problematic bit.

It would also be nice if the surreal number notation didn't need to change, just to keep the diff small, but if that's not possible then no worries.

[Alizter]

8.20 was released a few days ago, so it might be some time for VSCoq to catch up. On the other hand, coq-lsp seems to be working fine.

I agree that we shouldn't bump the minimum version this early. I'm inclined to remove the _ $== _ :> _ notation temporarily and add a note for reinclusion in 8.20.

[Alizter]

I've made the changes even more conservative by disabling a warning about postfix notations being recommended to be put at level 1 for a few notations that factor few an infix notation. This means we don't have to change levels in various places unnecessarily and importantly fixes the annoying warnings in 8.20 without changing the behaviour of the library.

[jdchristensen]

Great, that seems like a good way to handle it. BTW, the only remaining warnings github shows me are:

"From Coq" has been replaced by "From Stdlib".

Can we just change From Coq to From Stdlib to silence these?

[Alizter]

@jdchristensen Those are new warnings from 8.21+alpha that are not backwards compatible. They will be warnings until From Coq ceases to work, by that time switching to From Stdlib will be doable. For now, I will just disable those warnings so that they don't appear in the PRs.

I think this is part of the splitting of the stdlib / renaming of Coq project.