Stream: Coq users

Topic: formalizing graph coloring a la Wigderson


view this post on Zulip Ben Siraphob (Apr 11 2022 at 17:33):

I'm working on formalizing properties of Wigderson's algorithm, using a similar development outlined in Software Foundations. Wigderson's algorithm colors a 3-colorable graph using O(n)O(\sqrt{n}) colors. However in my development I'm running into several issues.

I did see that there is a graph theory development in math-comp but I am not fluent enough in ssreflect to be able to use the code. Any suggestions welcome on how I should go about tackling this development.

view this post on Zulip Karl Palmskog (Apr 11 2022 at 18:05):

@Ben Siraphob how are you representing graphs? The state of the art in graph representations for ease of proofs is likely: https://github.com/coq-community/graph-theory

view this post on Zulip Li-yao (Apr 11 2022 at 18:06):

how can I show that this process terminates

Every iteration colors at least one vertex -> the number of iterations is bounded by the number of vertices -> you can define the color function by recursion on the number of vertices.

how can I reason about the number of colors used asymptotically? In fact the exact number of colors used is 3n3\sqrt{n}3n
​, but AFAIK there isn't a library for reasoning about asymptotic notation.

It's probably simplest to just reason about the exact number of colors here. Inequalities with square roots can be rewritten as quadratic inequalities, e.g., d<3n    d2<9nd < 3\sqrt{n} \iff d^2 < 9n. But FYI there is also a library for asymptotic reasoning: https://gitlab.inria.fr/agueneau/coq-bigO/

view this post on Zulip Karl Palmskog (Apr 11 2022 at 18:08):

if you want to reason about complexity down to a model of computation, there is a heavyweight library here: https://github.com/uds-psl/coq-library-complexity

(Li-yao's suggestion is likely a better starting point)

view this post on Zulip Karl Palmskog (Apr 11 2022 at 18:10):

CoqHammer is most likely to help when you have a big library of graph theory facts, like there is in the graph-theory project. However, CoqHammer currently does not play all that well with the MathComp library and boolean reflection.

view this post on Zulip Karl Palmskog (Apr 11 2022 at 18:18):

for more lightweight proof automation, e.g., SAT + arithmetic/auto with my_lemma_collection, I recommend itauto

view this post on Zulip Ben Siraphob (Apr 14 2022 at 20:04):

Thanks for the suggestions. Yeah, I'll probably use the concrete color bound and show that the function terminates by arguing about the number of vertices. @Karl Palmskog doesn't CoqHammer have built-in reasoning about boolean reflection? I'll check out itauto.

view this post on Zulip Karl Palmskog (Apr 14 2022 at 20:06):

there is some basic built-in support for reflection in CoqHammer, but it doesn't work well on complex MathComp developments.

view this post on Zulip Paolo Giarrusso (Apr 14 2022 at 20:45):

For maps and sets, I use the support in stdpp and it’s better than the stdlib, but it’s not the case that every appropriate lemma exists there

view this post on Zulip Paolo Giarrusso (Apr 14 2022 at 20:47):

OTOH, set_solver can be rather nice. And it probably could be combined with coq-hammer’s first-order logic tactic

view this post on Zulip Karl Palmskog (Apr 14 2022 at 20:47):

also: itauto set_solver

view this post on Zulip Karl Palmskog (Apr 14 2022 at 20:49):

sauto in CoqHammer can do a ton, of course, it even has fine-grained support for unfolding, which gives an experience like the first-order solvers in HOL, like Metis


Last updated: Feb 06 2023 at 13:03 UTC