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?
I am not sure I understand what you mean. Do you refer to some decision procedure which becomes deprecated?
OK, let me be more specific: where is the Nat.*
equivalent of the now-deprecated Even.even_odd_dec
?
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.
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
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...
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.
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
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
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.
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)
we can undeprecate, especially if noone remembers what the purpose of the deprecation was
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, ...
.
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)
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
?
yeah I agree with that naming (e.g., Nat.Even
becomes the new Nat.even
, and then we also get Nat.evenb
)
I don't personally care so much if it breaks something, but there may be a breakage policy somewhere...
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...
I would really prefer to avoid modifying the core definition of Nat.Even
since its seems to be hard coded in Numbers.NatInt.NZParity
.
fine by me if current Nat.Even
is provided somehow, but I think users should be able to choose an alternative without getting deprecations
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 inPeanoNat.Nat
by default.
Concerning deprecated definitions (e.g.Even.even
), I would suggest moving the missing results toPeanoNat.Nat
as properties ofPeanoNat.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.
sure, that sounds good, you can ping me in any PRs (@palmskog
) if you want opinions from a Coq project maintenance viewpoint.
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: Sep 26 2023 at 12:02 UTC