Today’sYesterday’s problem was a
not-very-hidden linear algebra problem. So, finally time to start playing with
mathlib, right?
Wrong!
❯ lake exec day10
info: mathlib: checking out revision '1ccd71f89cbbd82ae7d097723ce1722ca7b01c33'
[tonnes of errors]
info: Mathlib/Algebra/BigOperators/Group/List/Defs.lean:95:0: PANIC at Lean.Meta…
backtrace:
0 libleanshared.dylib 0x000000011154997c _ZN4leanL15lean_panic_implEPKcmb + 264
1 libleanshared.dylib 0x0000000111549e48 lean_panic_fn + 40
2 libleanshared.dylib 0x000000010aa5ba38 l___private_Lean_MetavarContext_0__Lea…
3 libleanshared.dylib 0x000000010aa5a76c l___private_Lean_MetavarContext_0__Lea…
4 libleanshared.dylib 0x000000010aa5af5c l___private_Lean_MetavarContext_0__Lea…
5 libleanshared.dylib 0x000000010aa5b730 l___private_Init_Data_Array_Basic_0__A…
6 libleanshared.dylib 0x000000010aa5a884 l___private_Lean_MetavarContext_0__Lea…
7 libleanshared.dylib 0x000000010aa630ac l_Lean_MetavarContext_MkBinding_elimMV…
8 libleanshared.dylib 0x000000010aa656c0 l_Lean_MetavarContext_MkBinding_mkBind…
9 libleanshared.dylib 0x000000010ae418b0 l_Lean_Meta_mkLambdaFVars + 704
…
error: Lean exited with code 1
Some required targets logged failures:
- proofwidgets/widgetJsAll
- Mathlib.Algebra.BigOperators.Group.List.Defs
error: build failedOh, well.
Let’s just use the Vector type in the standard library, then:
structure Machine {n : Nat} where
lightDiagram : Vector (Fin 2) n
buttons : List (Vector (Fin 2) n)
joltageReqs: Vector Nat n
deriving ReprThis is pretty cool! Each machine is parameterized over the number of lights it
has, and the fact that that buttons toggle lights can be represented as vectors
of Fin 2s (i.e. a Nat guaranteed to be either 0 or 1).
This, together with the fact that • (scalar multiplication) and + (vector
addition) just…works means that once I represent a button list as a vector of
Fin 2s (i.e. representing #[1,3] as the vector (0, 1, 0, 1)), I can apply a list of button presses by multiplying by 0 or
1 and summing (mod 2):
def applyButtonPresses {n : Nat} (buttons : List (Vector (Fin 2) n)) (presses : List (Fin 2)) : Vector (Fin 2) n :=
let pairs := buttons.zip presses
pairs.foldl (λ acc (button, press) =>
acc + press • button
) (Vector.replicate n 0)Since each set of buttons is used either zero or one time1, I can then simply generate all combinations of the button sets and filter those that match the given light diagram.
Plenty fast enough!
For part 2, no such luck. For that part we no longer work mod 2, and a brute-force solution would be slow.
To make long, tragic story short2, I called my old friend Z3 for help.
Because with Z3 I could simply describe one of the problems like this (the clue
being the minimize goal) and have it solved:
(declare-const x0 Int)
(declare-const x1 Int)
(declare-const x2 Int)
(declare-const x3 Int)
(assert (>= x0 0))
(assert (>= x1 0))
(assert (>= x2 0))
(assert (>= x3 0))
(assert (= (+ x0 x1 x2) 10))
(assert (= (+ x0 x2 x3) 11))
(assert (= (+ x0 x1) 5))
(assert (= (+ x0 x1 x2) 10))
(assert (= x2 5))
(minimize (+ x0 x1 x2 x3))
(check-sat)
(get-value (x0 x1 x2 x3))So that’s exactly what I did! I generate such a Z3 program, then call whatever’s
called “z3” in $PATH and parse its result. Yolo.
I would love to revisit this and do it in Lean, but at least I got to really use “real programming” side of Lean today and do some file IO.
Things I (re-)learned today
- Using length-indexed vectors to ensure length invariants are preserved.
- Doing simple vector maths.
- Parsing using parser combinators.
- File system operations
- Calling an external program
Solution
import Parser
import Aoc
open Aoc
namespace Parser
open Parser Char ASCII
def parseSat : SimpleParser Substring Char Unit := do
_ ← string "sat"
_ ← char '\n'
return ()
def parseVarValuePair : SimpleParser Substring Char (String × Nat) := do
_ ← char '('
let varName ← takeMany1 alphanum
_ ← char ' '
let value ← parseNat
_ ← char ')'
return (String.mk varName.toList, value)
def parseVars : SimpleParser Substring Char (Std.HashMap String Nat) := do
_ ← char '('
let pairs ← sepBy (takeMany1 (whitespace <|> eol)) parseVarValuePair
_ ← char ')'
return Std.HashMap.ofList pairs.toList
def parseZ3Output : SimpleParser Substring Char (Std.HashMap String Nat) :=
parseSat *> parseVars
end Parser
structure Machine {n : Nat} where
lightDiagram : Vector (Fin 2) n
buttons : List (Vector (Fin 2) n)
joltageReqs: Vector Nat n
deriving Repr
def String.unbracket (s : String) : String :=
s.drop 1 |>.dropRight 1
def Machine.parse (s : String) : Except String (Σ n, Machine (n := n)) :=
match s.words with
| (goalStr :: rest) =>
let (buttonsStr, joltageReqsStr) := rest.splitAt (rest.length - 1)
let goalChars := goalStr.unbracket.toList.map (match · with
| '#' => 1
| '.' => 0
| c => panic! s!"Invalid goal character {c}"
)
let goal := goalChars.toArray
let n := goal.size
let buttonPositions := buttonsStr.toArray.map (·.unbracket.splitOn "," |> Array.mk ∘ List.map (·.toNat!))
let buttons := buttonPositions.toList.map (λ positions =>
Vector.ofFn λ i => if positions.contains i.val then 1 else 0
)
let joltageReqsArray :=
joltageReqsStr.head!.unbracket.splitOn "," |> Array.mk ∘ List.map (·.toNat!)
if joltageReqsArray.size = n then
let goalVec := Vector.ofFn (goal[·]!)
let joltageVec := Vector.ofFn (joltageReqsArray[·]!)
Except.ok ⟨n, Machine.mk goalVec buttons joltageVec⟩
else
Except.error s!"Length mismatch"
| _ => Except.error s!"Invalid Machine: {s}"
def allButtonCombinations (numButtons : Nat) : List (List (Fin 2)) :=
if numButtons = 0 then [[]]
else
let rest := allButtonCombinations (numButtons - 1)
rest.flatMap (λ bs => [0 :: bs, 1 :: bs])
def applyButtonPresses {n : Nat} (buttons : List (Vector (Fin 2) n)) (presses : List (Fin 2)) : Vector (Fin 2) n :=
let pairs := buttons.zip presses
pairs.foldl (λ acc (button, press) =>
acc + press • button
) (Vector.replicate n 0)
def Part1.solve {n : Nat} (m : Machine (n := n)) :=
let combinations := allButtonCombinations m.buttons.length
let valid := combinations.filter (applyButtonPresses m.buttons · = m.lightDiagram)
valid.map (λ x => x.filter (· = 1) |>.length) |>.min?
def generatez3Code {n : Nat} (m : Machine (n := n)) : String :=
let numButtons := m.buttons.length
let vars := (List.range numButtons).map (s!"x{·}")
let varList := String.intercalate " " vars
let varDecls := vars.map (s!"(declare-const {·} Int)")
let nonNegConstraints := vars.map (s!"(assert (>= {·} 0))")
-- (assert (= (+ x1 x3) 43))
let sumConstraints := List.ofFn (λ pos =>
let terms := m.buttons.mapIdx (λ idx button =>
if button[pos] == 0 then
none
else
some s!"x{idx}"
)
let validTerms := terms.filterMap id
let lhs := s!"(+ {String.intercalate " " validTerms})"
let rhs := toString (m.joltageReqs.get pos)
s!"(assert (= {lhs} {rhs}))"
)
let objective := s!"(minimize (+ {varList}))"
String.intercalate "\n" (
varDecls ++
nonNegConstraints ++
sumConstraints ++
[objective, "(check-sat)", s!"(get-value ({varList}))"]
)
def Part2.solve {n : Nat} (m : Machine (n := n)) : IO (Option Nat) := do
let z3Code := generatez3Code m
IO.FS.withTempFile (λ _ tmpFile =>
try
IO.FS.writeFile tmpFile z3Code
let result ← IO.Process.output {cmd := "z3", args := #[tmpFile.toString]}
if result.exitCode = 0 then
match Parser.parseZ3Output.run result.stdout with
| .ok _ m => return some m.values.sum
| .error _ errMsg =>
IO.println s!"Failed to parse z3 output: {errMsg}"
return none
else
IO.println s!"z3 error: {result.stderr}"
return none
catch e =>
IO.println s!"Failed to run z3: {e}"
return none
)
def main : IO Unit := do
let lines <- readLines "Day10/input.txt"
let machines ← lines.mapM Machine.parse |> IO.ofExcept
-- part 1
let presses := machines.map (λ ⟨_, m⟩ => Part1.solve m)
|>.map (·.get!)
|>.sum
IO.println s!"Part 1: {presses}"
-- part 2
let part2Results ← machines.mapM (λ ⟨_, m⟩ => Part2.solve m)
let part2Sum := part2Results.filterMap id |>.sum
IO.println s!"Part 2: {part2Sum}"