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:
hammerto 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:
Feedback and contributions are greatly appreciated, since this is one of the first developments I've written myself.
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)
hammer tactic call generally will not be reproducible - only the suggested replacement tactics will be stable, and those only require
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
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)
see https://coq.inria.fr/refman/practical-tools/coq-commands.html#by-resource-file for how to "globally locally" enable the hammer
@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
@Ben Siraphob but you're using Nix, right? Just set up your Nix configuration so it has the following in
.coqrc the Nix user's HOME directory:
From Hammer Require Import Hammer.
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
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)
I also advise to follow the general project structure here (e.g., a
theories directory): https://github.com/coq-community/jmlcoq
Last updated: Feb 06 2023 at 12:04 UTC