Stream: Coq devs & plugin devs

Topic: odd vs. Odd

Karl Palmskog (Dec 29 2021 at 14:17):

In current master, Arith.Even is deprecated. OK, we switch to Nat.Odd and friends. However, there isn't a proper decision procedure for even-odd-ness in Nat! Are we supposed to regress to using booleans everywhere, or is everyone who for some reason wants parity forced to roll their own (non-deprecated) decision procedure?

Olivier Laurent (Dec 29 2021 at 15:54):

I am not sure I understand what you mean. Do you refer to some decision procedure which becomes deprecated?

Karl Palmskog (Dec 29 2021 at 15:56):

OK, let me be more specific: where is the Nat.* equivalent of the now-deprecated Even.even_odd_dec?

Karl Palmskog (Dec 29 2021 at 15:58):

but in general, the even-odd theory in Nat.* is poor compared to Even.*. So weird to me to deprecate Even.* before most definitions/lemmas even have Nat.* equivalents.

Karl Palmskog (Dec 29 2021 at 16:01):

to be extremely specific, I consider the warnings here unfeasible to fix, since they require a near-complete refactoring of the affected file: https://github.com/coq-community/qarith-stern-brocot/runs/4659633467?check_suite_focus=true#step:4:381

Olivier Laurent (Dec 29 2021 at 16:27):

The short answer is that the purpose of deprecating those Arith files was to generate deprecation warnings where so far it was just a comment in the files. No big changes for users, just more warnings. This is considered as a first step in cleaning Arith (some discussions in coq/coq#11356).
The question of integrating all deprecated statements (and how and where) is indeed important! I have somehow tried to open the discussion:
https://github.com/coq/coq/pull/14736#issuecomment-894196996
But I do not think there was many reactions.
I think that we could either put them (or some of them) in the Nat module of Arith.PeanoNat, or in Arith.Arith_base as additional statements on top of PeanoNat.Nat. This is also correlated with the idea of merging Arith.Arith_base and Arith.Arith.
I'll try to have a look at the precise problems you are facing, sorry for the inconvenience...

Karl Palmskog (Dec 29 2021 at 16:29):

I'm supportive of the whole effort of modernizing the Arith part of stdlib, but I think it's a good rule to not deprecate until the alternative is nearly-as-good-as (or better than) the obsoleted. This was the case with omega vs. lia in the past.

Karl Palmskog (Dec 29 2021 at 16:32):

if you want to replicate my problems, you can use this commit using Coq master: https://github.com/coq-community/qarith-stern-brocot/tree/8ab631a26cf1ea77d37abb203e76533ddf59db01

Karl Palmskog (Dec 29 2021 at 16:32):

also, the port of the rest was actually quite a lot of effort, since many of the suggested new lemmas in deprecation warnings are not the same: https://github.com/coq-community/qarith-stern-brocot/commit/923f0aaeea3ef8e6a525b3472d5ce2887f2b2d19

Karl Palmskog (Dec 29 2021 at 16:37):

I do not think there was many reactions.

In the Coq ecosystem, there are few Coq project maintainers that follow Coq issues and PRs. At most, they read release notes. The reason I flag this stuff up is that I have nearly all my projects build with Coq master Docker images, and I usually fix deprecation warnings if it can be done in a backwards-compatible way. The real reactions will come when a release candidate or release is rolled out.

Karl Palmskog (Dec 29 2021 at 16:39):

finally, one very specific problem I discovered. The deprecation warning for le_antisym suggests Nat.le_antisym, which doesn't exist. It's supposed to be Nat.le_antisymm (arguably bad name)

Gaëtan Gilbert (Dec 29 2021 at 18:02):

we can undeprecate, especially if noone remembers what the purpose of the deprecation was

Karl Palmskog (Dec 29 2021 at 18:09):

I think the purpose of the deprecation is clear (moving towards removing Arith.Min, Arith.Le, etc.), but in the case of Arith.Div2 and Arith.Even there are often no good equivalents in the Nat module, and the definition of even-ness and odd-ness is completely different - Inductive vs. exists x, ....

Karl Palmskog (Dec 29 2021 at 18:21):

so my recommendation would be to undeprecate Arith.Div2/Arith.Even xor bring the corresponding Nat definitions/results for Arith.Div2 and Arith.Even up to par (ideally including the Inductive definitions of odd-ness and even-ness)

Olivier Laurent (Dec 29 2021 at 18:37):

I think it is a good thing to incorporate deprecated results in the PeanotNat.Nat < Arith_base < Arith hierarchy. I would say in PeanoNat.Nat by default.
Concerning deprecated definitions (e.g. Even.even), I would suggest moving the missing results to PeanoNat.Nat as properties of PeanoNat.Nat.Even and introducing the inductive definitions as alternative ones with equivalence proofs w.r.t. the existing ones. This means developments relying on the inductive construction of the predicates (not only their properties) could require to go through these equivalences.
I can start building a PR along the lines above.
One major issue behind all this is naming. For example here, I would consider Nat.even a more natural name for the current Nat.Even, which would require to rename the current Nat.even as Nat.evenb. Finally the inductive one could be Nat.Even or Nat.even_alt for example. However this would probably break a lot of development. So should a first step be to move Nat.even into Nat.evenb with Nat.even becoming deprecated for a while before it could be used for the current Nat.Even?

Karl Palmskog (Dec 29 2021 at 18:42):

yeah I agree with that naming (e.g., Nat.Even becomes the new Nat.even, and then we also get Nat.evenb)

Karl Palmskog (Dec 29 2021 at 18:43):

I don't personally care so much if it breaks something, but there may be a breakage policy somewhere...

Karl Palmskog (Dec 29 2021 at 18:45):

aren't inductive proofs of even-ness and odd-ness unique by the way? I think that would be one advantage of the inductive definitions...

Olivier Laurent (Dec 29 2021 at 18:58):

I would really prefer to avoid modifying the core definition of Nat.Even since its seems to be hard coded in Numbers.NatInt.NZParity.

Karl Palmskog (Dec 29 2021 at 19:02):

fine by me if current Nat.Even is provided somehow, but I think users should be able to choose an alternative without getting deprecations

Olivier Laurent (Dec 29 2021 at 19:12):

If we agree on this:

I think it is a good thing to incorporate deprecated results in the PeanotNat.Nat < Arith_base < Arith hierarchy. I would say in PeanoNat.Nat by default.
Concerning deprecated definitions (e.g. Even.even), I would suggest moving the missing results to PeanoNat.Nat as properties of PeanoNat.Nat.Even and introducing the inductive definitions as alternative ones with equivalence proofs w.r.t. the existing ones. This means developments relying on the inductive construction of the predicates (not only their properties) could require to go through these equivalences.

I'm committing to doing this before the 8.16 release process starts.
Again I am really sorry for the inconvenience. The model I had in mind was more of generating now the deprecation warnings which were implicit for a long time to encourage users to move to PeanoNat.Nat or Arith, and considering clean substitutes only before deleting the old files. I perfectly understand the idea of considering deprecation as requiring a ready alternative, and I will try to move to this as fast as possible.

Karl Palmskog (Dec 29 2021 at 19:17):

sure, that sounds good, you can ping me in any PRs (@palmskog) if you want opinions from a Coq project maintenance viewpoint.

Karl Palmskog (Dec 29 2021 at 21:16):

let's also be real about the inconvenience caused by a general deprecation like deprecated-syntactic-definition. I can either suppress the warning at the project level in _CoqProject or dune. But this then suppresses not just Arith.* warnings, but any other such deprecations as well. The alternative is to add clunky Set commands in all the affected files in my project. And if I don't suppress warnings, every build is overfull of warning messages.

Last updated: Jun 05 2023 at 09:01 UTC