Stream: Coq users

Topic: formalizing graph coloring a la Wigderson

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(\sqrt{n})$ colors. However in my development I'm running into several issues.

• it is very tedious to work with maps and sets, how can I try to automate rewrites with coqhammer?
• the algorithm repeatedly 2-colors the neighbors of vertices of high degree, how can I show that this process terminates and uses at most $2\sqrt k$ colors?
• but to prove the above I need to show that the neighborhood of any vertex in a 3-colorable graph is 2-colorable. Here I am stuck because I don't know how I can reason about an arbitrary graph (which is represented a map of sets) whose only assertion is 3-colorability (do I induct on the size of the graph?)
• how can I reason about the number of colors used asymptotically? In fact the exact number of colors used is $3\sqrt{n}$, but AFAIK there isn't a library for reasoning about asymptotic notation.

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.

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

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 < 3\sqrt{n} \iff d^2 < 9n$. But FYI there is also a library for asymptotic reasoning: https://gitlab.inria.fr/agueneau/coq-bigO/

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)

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.

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

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.

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.

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

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

Karl Palmskog (Apr 14 2022 at 20:47):

also: itauto set_solver

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: Oct 13 2024 at 01:02 UTC