2018 OMA Intercolegial Level 2 Problem 1
The following board with numbers in its squares is given:$$\begin{array}{|c|c|c|} \hline 1 & 2 & 3 \\ \hline 4 & 5 & 6 \\ \hline 7 & 8 & 9 \\ \hline \end{array}$$At each step it is possible to add $1$ to each cell in a row, add $1$ to each cell in a column, subtract $1$ from each cell in a row, or subtract $1$ from each cell in a column. Show a list of steps that transform the given board into the following board:$$\begin{array}{|c|c|c|} \hline 9 & 8 & 7 \\ \hline 6 & 5 & 4 \\ \hline 3 & 2 & 1 \\ \hline \end{array}$$
Replace sorry in the template below with your solution. The Mathlib version currently used is v4.26.0.
import Mathlib.LinearAlgebra.Matrix.RowCol
-- 3 × 3 board of integers
abbrev Board := Matrix (Fin 3) (Fin 3) ℤ
inductive OpTy
| Row
| Col
open OpTy
inductive OpDir
| Inc
| Dec
open OpDir
def OpDir.delta : OpDir → ℤ
| Inc => 1
| Dec => -1
structure Step where
opType : OpTy
ix : Fin 3
direction : OpDir
def Step.delta (op : Step) : ℤ :=
op.direction.delta
def Step.app (op : Step) (b : Board) : Board :=
match op.opType with
| Row =>
b + Matrix.updateRow 0 op.ix (List.Vector.replicate 3 op.delta).get
| Col =>
b + Matrix.updateCol 0 op.ix (List.Vector.replicate 3 op.delta).get
def applySteps (ops : List Step) (b : Board) : Board :=
ops.foldl (fun acc op => op.app acc) b
def initial : Board :=
![![1, 2, 3],
![4, 5, 6],
![7, 8, 9]]
def final : Board :=
![![9, 8, 7],
![6, 5, 4],
![3, 2, 1]]
def answer : List Step := sorry
theorem solution : applySteps answer initial = final := sorry
Login to submit a solution.