Tactics for Sudoku

Stream: metaprogramming / tactics

[shortc1rcuit]

(Question copied from #Is there code for X? )

I'm creating a project that lets you solve Sudokus in Lean 4 while proving each step of the solution. It is inspired by @Markus Himmel's Lean 3 sudoku project and @David Renshaw's Lean 4 chess puzzles. I want to create some tactics to reduce repetitive code. I've done a couple using macro_rules but I think this one will need elab.

Proving the value of a cell looks like this

--This tracks the current progress of the sudoku
def four_by_four_test : Progress := [[none,   some 1, some 3, none  ],
                                     [some 2, none,   none,   none  ],
                                     [none,   none,   none,   some 3],
                                     [none,   some 2, some 1, none  ]]

/-
Grid is a function from Fin 4 × Fin 4 to ℕ.
We have this alongside the progress object as it's easier to reason about ℕ than Option ℕ
-/
theorem four_by_four_test_solve (g : Grid) (hg : SudokuRules g)
    (hg_0_1 : g (0, 1) = 1) (hg_0_2 : g (0, 2) = 3) (hg_1_0 : g (1, 0) = 2)
    (hg_2_3 : g (2, 3) = 3) (hg_3_1 : g (3, 1) = 2) (hg_3_2 : g (3, 2) = 1)
    : Solvable g four_by_four_test := by
  unfold four_by_four_test
  have hg_1_3 : g (1, 3) = 1 := by
    --Turns the goal into proving that all the other cells in row 1 can't be equal to 1
    elimination row_elim
    --Can't be 1 as there's a 2 here
    · simp [hg_1_0]
    --Can't be 1 as there's a one in the column
    · exact col_conflict (by decide) hg_0_1
    --Can't be 1 as there's a one in the column
    · exact col_conflict (by decide) hg_3_2
  --Updates the progress of the sudoku to include the value we just proved
  apply Solvable.Set _ _ _ _ (by decide) hg_1_3
  dsimp [Progress.set', List.get!, List.set]
  sorry

I want this to instead look something like

def four_by_four_test : Progress := [[none,   some 1, some 3, none  ],
                                     [some 2, none,   none,   none  ],
                                     [none,   none,   none,   some 3],
                                     [none,   some 2, some 1, none  ]]

theorem four_by_four_test_solve (g : Grid) (hg : SudokuRules g)
    (hg_0_1 : g (0, 1) = 1) (hg_0_2 : g (0, 2) = 3) (hg_1_0 : g (1, 0) = 2)
    (hg_2_3 : g (2, 3) = 3) (hg_3_1 : g (3, 1) = 2) (hg_3_2 : g (3, 2) = 1)
    : Solvable g four_by_four_test := by
  unfold four_by_four_test
  set_cell (1, 3) 1
  --set_cell should create the goal "g (1, 3) = 1"...
  · elimination row_elim
    · simp [hg_1_0]
    · exact col_conflict (by decide) hg_0_1
    · exact col_conflict (by decide) hg_3_2
  --...add it as a hypothesis with a generated name and apply it to the sudoku progress
  sorry

The name format should be something like "h[GRIDNAME]_[COORDINATES]".

My main questions are:

1. How do you add in the new goal?
2. How do you add the proven statement to the list of the hypotheses?
3. How do you generate the name of the hypothesis?

(Sorry that this isn't a proper mwe; if I tried to make that I would have to send most of the project in this message. I've linked the github repository of the project if you want to look at the definitions.)

[Thomas Murrills]

Here are a couple of things that might help:

• You can make a new metavariable with sideGoal ← mkFreshExprMVar <side goal type>. (Make sure you’re using withMainContext around everything first to carry over the context from the main goal!) (This doesn’t update the goal list you see in the infoview yet; it just gives you a metavariable you can carry around.)
• To assert this goal as a hypothesis on the main goal g ← getMainGoal, you can write let (_,newMainGoal) ← g.assertHypotheses #[{ userName := <your custom name>, type := <side goal type>, value := sideGoal }]. Note that the side goal doesn’t have to be proven yet.
• Then you can update the goal list to put the side goal first, with replaceMainGoal [sideGoal.mvarId!, newMainGoal]
• To construct the custom hypothesis name from before, you might find Name.appendIndexAfter and getNat (for extracting numbers from syntax) useful.