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 https://github.com/Oqarina/oqarina/blob/main/src/formalisms/FaultTrees/NatInfMinMax.v ).

I understand the rationale for https://github.com/coq/coq/pull/17732 , 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?

Thanks

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 https://github.com/math-comp/analysis/blob/master/theories/constructive_ereal.v (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.

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