Stream: math-comp users

Topic: topological sorting in mathcomp


view this post on Zulip Evgeniy Moiseenko (Oct 21 2021 at 19:33):

Hi folks.
In my project, I need a lemma stating that any finite partial order can be extended to a total order, which boils down to the topological sorting of a finite graph. I was hoping to find a ready-to-go solution, preferably in mathcomp-style.
I was looking for the required lemma in ssreflect/fingraph.v https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/fingraph.v but haven't found it.
I was also searching in graph-theory library https://github.com/coq-community/graph-theory, also unsuccessfully.
But perhaps I just overlooked it? Topological sorting seems to be quite a basic thing, so expect someone already did it in Coq/mathcomp.

view this post on Zulip Karl Palmskog (Oct 21 2021 at 19:39):

there are a couple of implementations of topological sorting out there, originally by Cyril Cohen and Laurent Théry. I have adapted their solutions a bit for my purposes of analyzing dependency graphs in code that is extractable to OCaml. See here, in particular topos.v (proofs of topological sorting) and kosaraju.v (topological sorting function tseq): https://github.com/palmskog/chip/blob/master/core

This is the original development I adapted: https://github.com/CohenCyril/tarjan

This is Cyril and Laurent's paper on the general graph algorithm formalizations of which topological sorting is one part: http://drops.dagstuhl.de/opus/volltexte/2019/11068/pdf/LIPIcs-ITP-2019-13.pdf
This is the paper I co-authored on dependency graph analysis where we used parts of Cyril & Laurent's work: https://link.springer.com/content/pdf/10.1007%2F978-3-030-45237-7_9.pdf
Laurent's tech report on the original formalization of Kosaraju's algorithm, which uses topological sorting: http://www-sop.inria.fr/marelle/Laurent.Thery/Kosaraju/Kosaraju.pdf

I guess the main drawback is that this code is currently for MathComp 1.7, so would need some porting to recent MathComp (both Cyril's tarjan repo and my repo)

view this post on Zulip Evgeniy Moiseenko (Oct 21 2021 at 19:48):

Thank you, looks very useful indeed.
The restriction on version 1.7 of math comp is a bit problematic, since I currently use some features from the dev version.
Do you have plans to upgrade your developments to recent versions of mathcomp?

view this post on Zulip Karl Palmskog (Oct 21 2021 at 19:49):

well, I could take a look at in the near future to port my repo if you can confirm it has what you need

view this post on Zulip Karl Palmskog (Oct 21 2021 at 19:58):

ah, for completeness I should mention also a quite different non-MathComp topological sorting implementation (using the stdpp library), could likely be adapted to MathComp quite easily: https://github.com/runtimeverification/casper-cbc-proofs/blob/master/Lib/TopSort.v

view this post on Zulip Evgeniy Moiseenko (Oct 21 2021 at 20:01):

Karl Palmskog said:

well, I could take a look at in the near future to port my repo if you can confirm it has what you need

I am studying the source code.
I guess this is the lemma I need?
https://github.com/palmskog/chip/blob/072de78e61de5ed8a5891da5db3f9e267d063a0b/core/kosaraju.v#L348

I wonder why there is no precondition on graph/relation r being acyclic? (or I just don't see it)

view this post on Zulip Karl Palmskog (Oct 21 2021 at 20:02):

@Evgeniy Moiseenko this is what Laurent didn't have and which I added, you have two variations here:

view this post on Zulip Evgeniy Moiseenko (Oct 21 2021 at 20:04):

Oh, I see, very cool, thank you

view this post on Zulip Karl Palmskog (Oct 21 2021 at 20:04):

it turns out that the correctness of Kosaraju for strong connectedness needs topological sorting, but does not use the acyclicity. We needed acyclicity.

view this post on Zulip Karl Palmskog (Oct 21 2021 at 20:08):

if you think you can reuse kosaraju.v/acyclic.v/topos.v, please open an issue about the port to mathcomp-dev and we can take it from there: https://github.com/palmskog/chip/issues

view this post on Zulip Evgeniy Moiseenko (Oct 21 2021 at 20:19):

[Quoting…]
done

view this post on Zulip Evgeniy Moiseenko (Oct 21 2021 at 20:20):

would you expect it to be hard to update chip to latest mathcomp?
I can have a try by myself in coming days. In case there would be no significant problems I can just do it by myself.

view this post on Zulip Karl Palmskog (Oct 21 2021 at 20:22):

quite a lot has happened over the last few years in terms of lemmas changing name and so on. It shouldn't take too much work, and I might have time this weekend, but you can also jump into the port yourself if you want (then please fork and submit a pull request if you succeed)

Note that you need both coq-mathcomp-ssreflect and coq-mathcomp-fingroup at least.

I would then also recommend looking at the dependencies between files and ignore everything that doesn't have anything to do with topos.v (remove from _CoqProject)

view this post on Zulip Evgeniy Moiseenko (Oct 21 2021 at 20:32):

Karl Palmskog said:

I would then also recommend looking at the dependencies between files and ignore everything that doesn't have anything to do with topos.v (remove from _CoqProject)

I was hoping to get a working version of the whole library and then just add it to my opam as a dependency :sweat_smile:

view this post on Zulip Karl Palmskog (Oct 21 2021 at 20:33):

ah OK, I see. But why I think we should port those files first is because I copied other files from other places, and they have been maintained upstream, so one might copy them over again from there.

view this post on Zulip Evgeniy Moiseenko (Oct 21 2021 at 20:34):

ok, I see :)

view this post on Zulip Karl Palmskog (Oct 21 2021 at 20:35):

it's not clear that the best thing here is to put out a conglomeration of files not-all-so-related to graphs as an opam package. Ideally we would put together a graph algorithms package which also includes Tarjan's algorithm with the work by Cyril and Laurent.

view this post on Zulip Evgeniy Moiseenko (Oct 21 2021 at 20:38):

Maybe then promote some graph theory to fingraph.v? I think topological sorting at least would be very useful.

view this post on Zulip Karl Palmskog (Oct 21 2021 at 20:38):

this could take more time and a bit of communication, so that's why it may be a good idea to vendor the topsort files you need (put them in your repo) when they are first ported to mathcomp-dev, and then switch to using the imagined graph-algorithms package via opam later

view this post on Zulip Evgeniy Moiseenko (Oct 21 2021 at 20:39):

ok, I see, thank you. I'll have a look.

view this post on Zulip Karl Palmskog (Oct 21 2021 at 20:39):

the standards for getting code into the mathcomp repo alongside fingraph.v are super strict. If one creates a coq-graph-algorithms package/project, then eventually parts of that repository may be accepted into MathComp proper

view this post on Zulip Evgeniy Moiseenko (Oct 21 2021 at 20:41):

I am a bit uncomfortable with copying other people code to my repo (because in my opinion, it blurs the contributions of the community).
That is why I am proposing to update chip, or move to ssreflect, etc

view this post on Zulip Karl Palmskog (Oct 21 2021 at 20:42):

yes, we are trying to coordinate those kinds of projects, where people set up new repos with code to maintain to not have divergence, in coq-community: https://github.com/coq-community/manifesto/

view this post on Zulip Karl Palmskog (Oct 21 2021 at 20:43):

in the short term though, it's probably hard to avoid some vendoring

view this post on Zulip Evgeniy Moiseenko (Oct 21 2021 at 20:43):

Ok, hypothetical coq-graph-algorithms package looks like the best solution to me.
But as a first step, I would try to just fork chip and fix things in-place.

view this post on Zulip Evgeniy Moiseenko (Oct 21 2021 at 20:45):

Also, there is https://github.com/coq-community/graph-theory
Looks like it also overlaps with the theme of graph algorithms
Are you familiar with that library?

view this post on Zulip Karl Palmskog (Oct 21 2021 at 20:46):

yes, the maintainer said he prefers not to have algorithms like what is in chip and the tarjan repo in that project

view this post on Zulip Evgeniy Moiseenko (Oct 21 2021 at 20:46):

ok, I see

view this post on Zulip Karl Palmskog (Oct 21 2021 at 20:47):

it also has different notions/definitions of graphs than fingraph.v (although I guess they are convertible)

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 21:24):

I am a bit uncomfortable with copying other people code to my repo (because in my opinion, it blurs the contributions of the community).

And clear attribution/copyright notices (maybe a separate folder) should address this concern, and you probably need that to fulfill licensing requirements :-)

view this post on Zulip Evgeniy Moiseenko (Oct 22 2021 at 07:49):

Paolo Giarrusso said:

I am a bit uncomfortable with copying other people code to my repo (because in my opinion, it blurs the contributions of the community).

And clear attribution/copyright notices (maybe a separate folder) should address this concern, and you probably need that to fulfill licensing requirements :-)

Yes, for sure I would put license and credentials, but still ))

view this post on Zulip Karl Palmskog (Oct 22 2021 at 08:06):

maybe @Cyril Cohen could move this topic to the MathComp stream - and also possibly comment on what he thinks about consolidating MathComp graph algorithm results into some GitHub repo, for example his tarjan repo (or other repo where we adopt the tarjan code)

view this post on Zulip Notification Bot (Oct 22 2021 at 08:23):

This topic was moved here from #Coq users > topological sorting in mathcomp by Cyril Cohen

view this post on Zulip Cyril Cohen (Oct 22 2021 at 08:38):

I'm in favor of submitting PRs to mathcomp whenever some stuff are used by more than one user. We can converge by discussing in PR threads.

view this post on Zulip Karl Palmskog (Oct 22 2021 at 10:48):

OK, I'm reading this as that we could submit the topological sorting + lemmas about it as PR to MathComp proper. Will think about this when we get things ported to MathComp master.

view this post on Zulip Karl Palmskog (Oct 23 2021 at 13:48):

I ported my repo to MathComp master (compatibility with 1.12): https://github.com/palmskog/chip

With Laurent's encouragement I will also revive my old PR to the tarjan repo with changes to topological sorting and acyclicity from chip: https://github.com/CohenCyril/tarjan/pull/10

If this PR is merged, I will probably change chip to depend on the tarjan repo/package.

view this post on Zulip Karl Palmskog (Oct 24 2021 at 14:01):

PR was revived now: https://github.com/CohenCyril/tarjan/pull/10

view this post on Zulip Evgeniy Moiseenko (Oct 25 2021 at 09:06):

@Karl Palmskog awesome, thank you so much

view this post on Zulip Karl Palmskog (Oct 27 2021 at 16:19):

many thanks to Laurent who did great proof script improvements in my PR branch! I try to learn better MC/SSR style over time, and this is great for that. I didn't catch up to the boolP predicate until now.

view this post on Zulip Evgeniy Moiseenko (Oct 28 2021 at 13:24):

@Karl Palmskog thank you for your contributions!
Should I now use chip as my opam dependency?
Or should I use tarjan repo after your PR will be merged?
tarjan currently has no opam package, but I could PR basic .opam file for the library, if the contributors are okay with that.

view this post on Zulip Karl Palmskog (Oct 28 2021 at 14:11):

Cyril just did a PR against my PR about an hour ago, he has a much more math-compy way of handling acyclicity that I think looks good, I will review and merge his PR soon. Probably you should depend on tarjan after my PR + Cyril's improvements are merged

view this post on Zulip Cyril Cohen (Oct 28 2021 at 15:27):

I think the next steps to do are actually

  1. review and merge PR CohenCyril/tarjan#10
  2. move the repo to the math-comp organization
  3. move all .v files to theories directory
  4. add a meta.yml package (and generate metadata from it)
  5. publish an opam package and a nix package (note that it suffices to add this file to https://github.com/nixos/nixpkgs.
  6. backport the stuff to mathcomp master

view this post on Zulip Karl Palmskog (Oct 28 2021 at 15:46):

@Cyril Cohen can/should I generate a basic meta.yml and do a PR with that? Or I guess we wait until after the move, OK.

view this post on Zulip Cyril Cohen (Oct 28 2021 at 17:27):

Step 2. is done and Step 3. is math-comp/tarjan#13 and merged
@Karl Palmskog you could prepare step 4. in parallel

view this post on Zulip Karl Palmskog (Oct 28 2021 at 17:43):

OK, working on the meta.yml file now, should be done in the next hour

view this post on Zulip Karl Palmskog (Oct 28 2021 at 17:46):

@Cyril Cohen is the MIT license OK, or do your prefer some CECILL one?

view this post on Zulip Cyril Cohen (Oct 28 2021 at 17:46):

Cecill please

view this post on Zulip Karl Palmskog (Oct 28 2021 at 22:42):

OK, the MathComp Tarjan and Kosaraju opam package, version 1.0.0, is now out in the Coq opam archive:

opam install coq-mathcomp-tarjan

It has definitions of graph acyclicity and verified topological sorting, as well as variants of strongly connected components algorithms.

view this post on Zulip Evgeniy Moiseenko (Oct 29 2021 at 08:08):

Thank you so much to all people involved @Karl Palmskog @Cyril Cohen @Laurent Théry .
I want to say that mathcomp community is just awesome.

view this post on Zulip Karl Palmskog (Oct 30 2021 at 18:25):

just saw this other piece of graph algorithm formalization using fingraph, flavor feels familiar to the Kosaraju formalization: https://github.com/fetburner/coq-dijkstra


Last updated: Mar 29 2024 at 01:40 UTC