Hi,

I am looking for a data structure which is effectively a map, but its key is ordered, so we can do things like `find_ge`

which finds a binding for the smallest key that is greater than or equal to the input, as well as `find_le`

for the symmetric direction. The standard library does expose `FMapFullAVL`

, but it seems does not expose the interface I want. is there any way I can get this data structure? It does not have to be in stdlib if other libraries provide it.

you may want to look at this: https://github.com/xavierleroy/coq-mmaps

the RBT version likely has the invariant you want, per https://www.cs.princeton.edu/~appel/papers/redblack.pdf

now if we only could get this PR merged and an opam package: https://github.com/letouzey/coq-mmaps/pull/2

Is the problem that Avl trees don't have that invariant, or they just don't expose it? I'd have expected the latter?

@Karl Palmskog is this a candidate for coq-community? Not that I have energy to contribute sadly :-|

@Paolo Giarrusso I would personally like coq-mmaps to join Coq-community. But we would need permission from Pierre Letouzey, who I think has not been active on GitHub for a while. You are welcome to propose adding coq-mmaps to Coq-community though and ping in Pierre (or even email him beforehand): https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md#proposing-a-new-package

The proposer of a package doesn't have to volunteer to be maintainer.

Note that "we need permission" is a bit too strong. Our process is to ask permission from the original author and to proceed (e.g., with a fork) in case we don't hear back. That being said, it would be preferable to be able to transfer the repo instead of creating a fork, so I can also ask Pierre Letouzey (who is in my lab) directly (but probably after the summer).

But there is not much point in doing this effort if we do not find a volunteer maintainer to start with.

I guess I could step in as an interim maintainer, since I would at least like to see this package have Xavier's changes and put it on opam. Then I will do the minimum to keep it compatible until someone takes over. But it all depends on what Pierre says (if he likes the idea)

I recently ported Andrew's RBT to CakeML, so I know the codebase

I've recently implemented a bunch of search tree structures with SSReflect here https://github.com/clayrat/fav-ssr

@Alexander Gryzlov any plans to package those in some way? Ideally, this would become part of some official MathComp project (cc: @Enrico Tassi )

Yeah I was planning to finish part 4 first, then propose some of the auxilliary theories (e.g. division with ceiling) for core mathcomp, and maybe the repo itself as some sort of mathcomp project

The only problem is that part 4 is the hardest one and the ratio of actual code to the stuff they describe in the book is much higher than in the other chapters :D

we already have https://github.com/thery/mathcomp-extra which is a bit similar, and also deserves more highlighting

it's definitely a cliche, but "perfect" or "complete" may sometimes be the enemy of good (enough to publish)

Yeah, I know of mathcomp-extra, I used its logarithm ceiling for this project for a while and then @Laurent Théry even upstreamed it to mathcomp core

@Karl Palmskog it is a bit unclear what you mean, or better I don't know what "official MC project" is. For example we are moving (with your help) some projects to coq-community. If you mean "being integrated in the main MC repo" then the thing is about maintenance and the code quality is going to be examined carefully. (and I agree totally with "perfect is enemy of good")

@Enrico Tassi well, this was just me checking in what you think the process should be. If indeed you think Coq-community should be the home for MathComp-related projects by default, then that's great, and we can just ask Alexander to follow the process here when ready.

But to me, "official" MathComp has meant the project being part of the `math-comp`

GitHub org.

When we created that, coq-community was not even there, and we were kind of proposing the same "services", eg we test against you. Today we do that with nix, no matter where you place your project... Visibility is also different, you can opam search mathcomp, in the past you could not...

This is why we started moving some projects to coq-community

OK, sounds great to me. Then I guess the only "official" thing left will be the `coq-math-comp-`

prefix in package names?

We can try to define this precisely. To me a user of MC shall not use that prefix. But a library which adds some theory to MC should, even if it is not hosted in MC/

Example: if you add a structure to the hierarchy (today hard, starting from MC 2.0 easier) or provide instances of general interest, then the prefix makes sense to me

If you follow similar style

if it would make sense to merge your library in MC, eventually...

We don't have that written up, this is what looks reasonable to me (on the top of my head)

clearly a thing called "mathcomp-extra" has that trajectory in mind

@Alexander Gryzlov didn't know your work. Great!!. If you need some manpower to progress in chapter 4, don't hesitate to ask.

If people need not permission from the math comp team to get the math comp prefix, this should indeed be documented. And if they need it but there is a process to apply, it should be documented as well :wink:

somewhat counterintuitively, the rules around the `coq-math-comp-`

prefix should probably be documented in the Coq opam archive, and be enforced by opam archive maintainers

Re the invariant on stdlib’s fmaps/fsets, I think there is an additional functor in the stdlib that shows that folding over a set/map is order-preserving (assuming the keys are ordered) so you could implement it I think

Last updated: Sep 23 2023 at 07:01 UTC