## WORK IN PROGRESS

**This is a work-in progress port from Markus Himmel's [https://github.com/TwoFX/sudoku](Lean3 version).**

## Playing sudoku in the Lean theorem prover

### How to start playing

Assumes that you have a C++ compiler via `g++`

. On Debian/Ubuntu,
`sudo apt install build-essential`

should do the trick.

First, we download the code.

`leanproject get TwoFx/sudoku`

Next, we compile the program that generates levels for us.

`cd sudoku`

`g++ -std=gnu++11 -O2 scripts/gen.cpp -o gen`

Next, we will use it to generate a level for us.

- Put a sudoku in a file (as 81 numbers separated by white space, 0 is blank). See
`scripts/easy1`

for an example. `./gen < your_sudoku_file > src/play.lean`

Next, we have to tell Visual Studio code to not time out our code. This is needed because I wrote very inefficient and slow code. You will notice this while playing.

`code .`

- Open the settings (Ctrl+Comma), search for Lean Time Limit, and set it to 0.

Finally, we are ready to go.

- Restart VS Code, and open
`play.lean`

.

### How to play

Please look at the screenshot for an example of how a game of sudoku can look.

Cells are zero-indexed from the top left. You place the number z in cell (x, y) by saying

```
have cxy : s.f (x, y) = z
```

but now you have to prove why this is the case. There are four main tactics for that:

`box_logic`

splits along the statement "there is a z somewhere in the box of (x, y)" and tries to find a conflict in the board for ever position other than (x, y)`row_logic`

and`col_logic`

are the same as`box_logic`

, but (you guessed it) for rows and columns rather than boxes`cell_logic`

is like the others, but splits along the statement "there is a number in (x, y)"`naked_single`

is a synonym for`cell_logic`

to conform to usual sudoku terminology

There is also support for two kinds of pencil marks: Snyder notation on the edges of cells and doubles and triples in the center of cells:

If you say

```
have p0 : s.snyder w x y z a
```

then you have to prove that there is an a in (w, x) or (y, z). You will usually use row, box or column logic for this.

If you say

```
have p1 : s.double x y a b
```

then you have to prove that there is either an a or a b in (x, y).

Doing this will give you a pencil mark. To later use such a pencil mark in a deduction, you can say things like `box_logic with p0 p1`

, which for every possible position in the box will first try to find an unconditional conflict and then splits over p0 and p1 in the cases where it gets stuck.

Finally, you can use `pencil with p0 p1`

to make case distinctions over pencil marks only.

For hard sudokus, you'll want to formalize some actual sudoku theory. I have started doing that in the file `Basic.lean`

, but that work is still in its very early stages.