Stream: Coq users

Topic: formalization of graph coloring in Coq


view this post on Zulip 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:

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:

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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: Mar 28 2024 at 14:01 UTC