It’s December again, and time for a new round of Advent of Code. I will be doing it in Lean 4 again this year, as I really enjoyed doing (most of) AoC in Lean last year.
Today’s problem was relatively simple, but it’s been a long time since I last wrote Lean, so it was mostly about re-learning the syntax. I wrote this on my iPad while sleep-deprived at Charles de Gaulle airport in Paris, so it took a while!
I have a small utility
library and I ended
up adding a
scanl
method on String, since I couldn’t find one in the standard library:
def List.scanl {α β : Type} (f : α → β → α) (init : α) : List β → List α
| [] => [init]
| b :: bs => init :: scanl f (f init b) bsNot really any fancy Lean stuff today, except for the fact that the type
representing the safe’s dial ensure that its state is in the range [1, 100) by
using the
Fin
type which ensures it’s a natural number less than 100. When rotating the dial
we therefore need to supply a proof of newVal < 100, which the
omega
tactic is able to just…figure out here, since we’re doing a modulo 100.1
Things I (re-)learned today
- I can for the most part just write Haskell and then follow the error messages.
- The behaviour of the pipe operator can be really subtle/confusing.
(43 : Int) |>.toNatworks, as does(43 : Int) |> Int.toNat, but not(43 : Int) |> .toNat2. I think I’ll stick to explicitly resolving these in the future. - I really quite like the syntax for anonymous functions (
(·.dial == 0)is the same as(fun s => s.dial == 0)).
Solution
import Aoc
open Aoc
structure DialState where
dial : Fin 100
instance : ToString DialState where
toString state := s!"DialState(dial = {state.dial})"
def parseRotationInstruction (line : String) : Int :=
match line.front with
| 'R' => line.drop 1 |>.toInt!
| 'L' => line.drop 1 |>.toInt! |>.neg
| invalid => panic! s!"Invalid instruction: {invalid}"
def DialState.rotate (state : DialState) (steps : Int) : DialState :=
let newVal := (state.dial + steps) % 100 |>.toNat
{ dial := ⟨newVal, (by omega : newVal < 100)⟩ }
def DialState.zeroCount (state : DialState) (steps : Int) : Nat :=
let distance := if steps < 0 && state.dial != 0
then 100 - state.dial -- we're (100 - [current value]) steps away from zero
else state.dial
(steps.natAbs + distance) / 100
def main : IO Unit := do
let lines ← readNonEmptyLines "Day01/input.txt"
let instructions := lines.map parseRotationInstruction |>.toList
-- part 1
let states : List DialState := List.scanl .rotate (DialState.mk 50) instructions
let zeroStates := states.filter (·.dial == 0)
IO.println s!"Part 1: {zeroStates.length}"
-- part 2
let (_, zerosCount) : DialState × Nat := List.foldl (fun ⟨state, numZeros⟩ steps =>
(state.rotate steps, numZeros + state.zeroCount steps)
) (DialState.mk 50, 0) instructions
IO.println s!"Part 2: {zerosCount}"