Completeness for Boolean models formalised in Coq

The formal proofs are inside this directory. You can also browse the generated documentation as colored HTML code here.

In order to compile the sources, you need the Coq proof assistant version 8.2, a recent version (as of August 2025).

If you are on a Unix-like system, and the executable coqc is in your PATH variable, you can just run the command make from inside a terminal window. If coqc is not in your path, you can either set it, or open the Coq IDE and run Make from the Compile menu.

If you are on a Windows system, you do not have make, and coqc is not in your PATH, the simplest solution is to open Coq IDE and compile one by one file, making sure to do it in the following order: filters.v, classcomp.v.

Note: The formalisation is not complete, sorting of lists in lists.v remains to be finished.

Note (August 2025): The formalisation is now complete, sorry for the delay. If you want to see the changes, you can use git on this zip file: boolean_completeness.zip.