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.

@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

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/

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)

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.

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

, I recommend itauto

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.

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

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

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

also: `itauto set_solver`

`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: Sep 23 2023 at 15:01 UTC