A formalisation of Sudoku in Coq. It implements a naive Davis-Putnam procedure to solve Sudokus.
- Author(s):
- Laurent Théry (initial)
- Coq-community maintainer(s):
- License: GNU Lesser General Public License v2.1 or later
- Compatible Coq versions: 8.12 or later
- Additional dependencies: none
- Coq namespace:
Sudoku
- Related publication(s):
The easiest way to install the latest released version of Sudoku is via OPAM:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-sudoku
To instead build and install manually, do:
git clone https://github.com/coq-community/sudoku.git
cd sudoku
make # or make -j <number-of-cores-on-your-machine>
make install
A Sudoku is represented as a mono-dimensional list of natural numbers. Zeros are used to represent empty cells. For example, the 3x3 Sudoku:
-------------------------------------
| | | 8 | 1 | 6 | | 9 | | |
-------------------------------------
| | | 4 | | 5 | | 2 | | |
-------------------------------------
| 9 | 7 | | | | 8 | | 4 | 5 |
-------------------------------------
| | | 5 | | | | | | 6 |
-------------------------------------
| 8 | 9 | | | | | | 3 | 7 |
-------------------------------------
| 1 | | | | | | 4 | | |
-------------------------------------
| 3 | 6 | | 5 | | | | 8 | 4 |
-------------------------------------
| | | 2 | | 7 | | 5 | | |
-------------------------------------
| | | 7 | | 4 | 9 | 3 | | |
-------------------------------------
is represented as
0 :: 0 :: 8 :: 1 :: 6 :: 0 :: 9 :: 0 :: 0 ::
0 :: 0 :: 4 :: 0 :: 5 :: 0 :: 2 :: 0 :: 0 ::
9 :: 7 :: 0 :: 0 :: 0 :: 8 :: 0 :: 4 :: 5 ::
0 :: 0 :: 5 :: 0 :: 0 :: 0 :: 0 :: 0 :: 6 ::
8 :: 9 :: 0 :: 0 :: 0 :: 0 :: 0 :: 3 :: 7 ::
1 :: 0 :: 0 :: 0 :: 0 :: 0 :: 4 :: 0 :: 0 ::
3 :: 6 :: 0 :: 5 :: 0 :: 0 :: 0 :: 8 :: 4 ::
0 :: 0 :: 2 :: 0 :: 7 :: 0 :: 5 :: 0 :: 0 ::
0 :: 0 :: 7 :: 0 :: 4 :: 9 :: 3 :: 0 :: 0 :: nil
All functions are parametrized by the height and width of a Sudoku's subrectangles. For example, for a 3x3 Sudoku:
sudoku 3 3: list nat -> Prop
check 3 3: forall l, {sudoku 3 3 l} + {~ sudoku 3 3 l}
find_one 3 3: list nat -> option (list nat)
find_all 3 3: list nat -> list (list nat)
See Test.v
.
Corresponding correctness theorems are:
find_one_correct 3 3
: forall s,
length s = 81 ->
match find_one 3 3 s with
| Some s1 => refine 3 3 s s1 /\ sudoku 3 3 s1
| None =>
forall s, refine 3 3 s s1 -> ~ sudoku 3 3 s1
end
find_all_correct 3 3
: forall s s1, refine 3 3 s s1 -> (sudoku 3 3 s1 <-> In s1 (find_all 3 3 s))
See Sudoku.v
.
More about the formalisation can be found in a note.
The following files are included:
ListOp.v
some basic functions on listSudoku.v
main fileTest.v
test fileTactic.v
contradict tacticDiv.v
division and modulo for natPermutation.v
permutationUList.v
unique listListAux.v
auxillary facts on listsOrderedList.v
ordered list
The Sudoku code can be extracted to JavaScript using js_of_ocaml:
make Sudoku.js
Then, point your browser at Sudoku.html
.