diff --git a/math/examples/sudoku.lurch b/math/examples/sudoku.lurch new file mode 100644 index 00000000..a1700e35 --- /dev/null +++ b/math/examples/sudoku.lurch @@ -0,0 +1,393 @@ + +
+ + +The following conditions hold for any size Sudoku grid. Let value(x,y,z) denote the value of the square in the grid that is in row x, column y, and quadrant z. To keep things simple we do not specify how the quadrant, z is a function of the pair [x,y]. This has the added advantage that the same proofs will work no matter how you define the four 'quadrants'.
+Row condition: If value(x,y,z)=value(w,y,z) then w=x.
+Column condition: If value(x,y,z)=value(x,w,z) then w=y.
+Quadrant condition: If value(x,y,z)=value(x,y,w) then w=z.
+Example:
+TODO: The challenge here is the combinatorial part: how to handle things like value(x,y,z) must be from a certain finite set, so that e.g. if a row contains 1,2,3 the remaining value must be 4 and not something else. Pigeonhole stuff.