Stream: Coq users

Topic: formalization of graph coloring in Coq

Ben Siraphob (May 13 2022 at 22:46):

Hi all,

I've been working on a formalization of Wigderson's algorithm in Coq for the last month and a half now as part of a class on verification. Please see the attached paper for more details. Some notes about the formalization:

• it builds upon the representation of graphs in the graph coloring chapter in Software Foundations, but the graph theory involved is completely written from scratch
• it extensively uses CoqHammer's tactics sauto and hammer to reduce the tedium and lemma searching involved

Note that the choice to not use the graph-theory development in mathcomp is a conscious decision. I found it very difficult to work with even with some knowledge of ssreflect.

The formalization is not complete yet, but various key lemmas are proven and the main coloring loops have been defined. In particular, however, it remains to show trickier things:

• decidability of two-coloring (involves writing and proving a two-coloring algorithm correct)
• reasoning about functions whose termination criterion is based on the maximum degree of a graph, or number of uncolored vertices

Feedback and contributions are greatly appreciated, since this is one of the first developments I've written myself.

Karl Palmskog (May 13 2022 at 22:50):

I strongly recommend never leaving a From Hammer Require Import Hammer. in the source code. This means anyone who wants to use your code needs to install the coq-hammer plugin (as opposed to just the coq-hammer-tactics pure Coq library)

Karl Palmskog (May 13 2022 at 22:50):

the hammer tactic call generally will not be reproducible - only the suggested replacement tactics will be stable, and those only require coq-hammer-tactics

Ben Siraphob (May 13 2022 at 22:52):

Yes, this is purely for development purposes for now but I plan on removing the imports once the formalization is complete. Attached to the repository is a shell.nix file that also provides the ATPs invoked by CoqHammer

Karl Palmskog (May 13 2022 at 23:34):

part of my job is reviewing and requesting revisions of Coq code, and one important requirement before requesting reviews is removing all unnecessary dependencies (to allow the reviewer to run the code with minimum fuss)

Karl Palmskog (May 13 2022 at 23:35):

see https://coq.inria.fr/refman/practical-tools/coq-commands.html#by-resource-file for how to "globally locally" enable the hammer

Ben Siraphob (May 15 2022 at 18:44):

@Karl Palmskog is there a way to enable it just for my project? I have an environment that only has CoqHammer available in the project directory

Karl Palmskog (May 15 2022 at 18:54):

@Ben Siraphob but you're using Nix, right? Just set up your Nix configuration so it has the following in .coqrc in the Nix user's HOME directory:

From Hammer Require Import Hammer.

Karl Palmskog (May 15 2022 at 18:55):

then you will have hammer tactic available everywhere when using that Nix config, but you don't have to have the require-import for it in GitHub code

Karl Palmskog (May 15 2022 at 18:57):

then you can set up CI on GitHub using either opam or separate Nix to check that the project always builds without the Hammer plugin (this would be best practice, and ensure people who look at your code don't have to install the hammer)

Karl Palmskog (May 15 2022 at 18:58):

I also advise to follow the general project structure here (e.g., a theories directory): https://github.com/coq-community/jmlcoq

Last updated: Sep 28 2023 at 11:01 UTC