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 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.

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: Oct 13 2024 at 01:02 UTC