Logic puzzles in Lean

Stream: Is there code for X?

[shortc1rcuit]

Ive been looking into the soduku widget for lean and I'm interested in maybe furthering the idea. However, there does seem to be a big issue. For you to solve the soduku, you need to give the solution in the goal, which kind of defeats the purpose. Is there a way to structure a goal so this isn't needed (i.e: your arguments are the clues and the goal is "find the solution to the puzzle")?

[Damiano Testa]

These examples make me suspect that Lean should be able to also find a solution to a sudoku puzzle:

import Mathlib.Data.Finset.Basic

example {n : Nat} (hn : n ∈ ({0, 1, 2} : Finset Nat)) (hn' : n ∉ ({0, 2} : Finset Nat)) : n = 1 := by
  revert n
  decide

open Finset in
example {n : Nat} (hn : n ∈ range 9) (hn' : n ∉ range 8) : n = 8 := by
  revert n
  decide

[shortc1rcuit]

Maybe? I'm worried it may get caught on more complex logic. Either way, that would still involve having to give the solution in the goal before solving it.

[Kim Morrison]

We really should fix decide so you don't need the revert here!

[Damiano Testa]

shortc1rcuit said:

Either way, that would still involve having to give the solution in the goal before solving it.

Not necessarily: since decide will only work on one choice, you can write a tactic that tries out all values in 0...9 and only use the one where decide was successful.

[shortc1rcuit]

I'm confused, wouldn't you still have to put n = 8 in the goal?

[Damiano Testa]

What I am suggesting is that you can get a metaprogram to figure out what the answer is and then either add a declaration automatically to the environment or produce a Try this output with the solution.

[Alex Meiburg]

I think a good 'fix' would be instead of saying "prove that X is the answer", having "prove that there exists an answer". This is a similar problem to what they run into with IMO problem formalization -- you don't want to give away the answer.

[Alex Meiburg]

Even better if you say "show that there exists a unique solution", which is true for many logic puzzles :)