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.
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)
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?
well, I could take a look at in the near future to port my repo if you can confirm it has what you need
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
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)
@Evgeniy Moiseenko this is what Laurent didn't have and which I added, you have two variations here:
Oh, I see, very cool, thank you
it turns out that the correctness of Kosaraju for strong connectedness needs topological sorting, but does not use the acyclicity. We needed acyclicity.
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
[Quoting…]
done
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.
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
)
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:
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.
ok, I see :)
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.
Maybe then promote some graph theory to fingraph.v
? I think topological sorting at least would be very useful.
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
ok, I see, thank you. I'll have a look.
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
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
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/
in the short term though, it's probably hard to avoid some vendoring
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.
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?
yes, the maintainer said he prefers not to have algorithms like what is in chip and the tarjan repo in that project
ok, I see
it also has different notions/definitions of graphs than fingraph.v
(although I guess they are convertible)
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 :-)
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 ))
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)
This topic was moved here from #Coq users > topological sorting in mathcomp by Cyril Cohen
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.
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
.
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.
PR was revived now: https://github.com/CohenCyril/tarjan/pull/10
@Karl Palmskog awesome, thank you so much
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.
@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.
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
I think the next steps to do are actually
math-comp
organization.v
files to theories
directorymeta.yml
package (and generate metadata from it)master
@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.
Step 2. is done and Step 3. is math-comp/tarjan#13 and merged
@Karl Palmskog you could prepare step 4. in parallel
OK, working on the meta.yml
file now, should be done in the next hour
@Cyril Cohen is the MIT license OK, or do your prefer some CECILL one?
Cecill please
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.
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.
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