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:

- https://github.com/palmskog/chip/blob/master/core/topos.v#L174
- https://github.com/palmskog/chip/blob/master/core/topos.v#L194

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

- review and merge PR CohenCyril/tarjan#10
- move the repo to the
`math-comp`

organization - move all
`.v`

files to`theories`

directory - add a
`meta.yml`

package (and generate metadata from it) - publish an opam package and a nix package (note that it suffices to add this file to https://github.com/nixos/nixpkgs.
- backport the stuff to mathcomp
`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: Jul 25 2024 at 16:02 UTC