Stream: Coq users

Topic: Replacement for (some of) Ndist to be deprecated?

view this post on Zulip Jerome Hugues (Mar 20 2024 at 11:20):

I saw that Coq 8.19 deprecated Ndist. I am using natinf (natural numbers + infinity), ni_min, and a couple of associated lemmas. I also extended this library with other trivial lemmas and a definition for ni_max (see ).

I understand the rationale for , and agree the interface is rather old and could benefits from an update.

Do you know a replacement for this capability? I was hoping to find a library that would have (natural numbers + infinity), min, max, and + in math comp but this does not seem to be covered.

The deprecation notice mentions maintaining this package as an alternative. Does it mean creating a separate package coq-ndist for these definitions?


view this post on Zulip Pierre Roux (Mar 20 2024 at 12:00):

Pinging @Andres Erbsen . About mathcomp, I indeed don't think we have that. It would probably be relatively easy to do, taking inspiration of extended reals (it would likely be much simpler as you won't have the duality question and all the operations on reals). A pull request would certainly be welcome.

view this post on Zulip Jerome Hugues (Mar 20 2024 at 18:37):

Thanks for the pointer, it seems a big departure from the original Ndist. Should we go in that direction, or instead define this as an actual (min, +) algebra with corresponding type classes defining axioms for algebra, which I presume should be defined somewhere in either math comp or other libraries.

Last updated: Jun 22 2024 at 15:01 UTC