Advent of Code 2024 - Day 2

Stream: general

[James Sully]

Here's my solution. Feedback appreciated, and please post your own solution!

import Utils

abbrev Report := List Nat
abbrev Input := List Report

namespace Day02

def parseNatList (line : String) : Option (List Nat) :=
  line.split (Char.isWhitespace)
  |>.mapM String.toNat?

def parseInput (s : String) : Option Input :=
  s.lines.mapM parseNatList

def reportSafe (report : Report) : Bool :=
  let differences : List Int :=
    List.zipWith Int.subNatNat report report.tail
  differences.all (·.natAbs ≤ 3) &&
    (differences.all (· > 0) || differences.all (· < 0))

def part1 : Input → Nat := List.countP reportSafe

def removals (l : List α) : List (List α) :=
  List.range l.length
  |>.map (l.eraseIdx ·)

def reportSafeDampener (report : Report) : Bool :=
  reportSafe report || (removals report).any reportSafe

def part2 := List.countP reportSafeDampener

[Ayhon]

Here's my solution for day 2, minus the runner

import Lean.Data.RBMap
import Batteries.Data.List

namespace Day2

abbrev Input := List (List Int)

def parse_input(ls: List String): Input :=
  let ls := ls.filter (not ∘ String.isEmpty)
  let tokens := ls.map
    (·.split Char.isWhitespace |> List.filter (not ∘ String.isEmpty))
  tokens.map (·.map (String.toInt!))


namespace Part1
  def List.window[Inhabited α](width: Nat)(ls: List α): List (List α) :=
    let n := ls.length - width + 1
    List.range n
      |>.map (fun start =>
        List.range width
          |>.map (fun i => ls[start + i]!)
      )

  def valid (ls: List Int): Bool :=
    let inc := compare ls[0]! ls[1]!
    open Part1 in
    ls.window 2
      |>.all (fun row =>
        /- dbg_trace s!"row={row}" -/
        let diff := (row[0]! - row[1]!).natAbs
        compare row[0]! row[1]! == inc && 1 <= diff && diff <= 3)

  def solve(board: Input): Int := board.filter valid |>.length
end Part1

namespace Part2
  def valid (ls: List Int): Bool :=
    let n := ls.length
    List.range n
      |>.any (fun i =>
        Part1.valid (ls.eraseIdx i)
      )

  def solve(board: Input): Int :=
    board.filter valid |>.length
end Part2

[James Sully]

nice, I bet the general sliding windows function will come in handy

[Ayhon]

Yes, I was looking for that functionality in Batteries. I found List.toChunks, which seems to almost be what I want, but not quite. Perhaps we could add it to Batteries? If people would be interested I don't mind researching what's the necessary process to do so.

[Edward van de Meent]

docs#List.groupBy ?

[Ayhon]

Edward van de Meent said:

docs#List.groupBy ?

That seems to be more like List.toChunks. I was looking for something that allows me to access each element of a list, together with the next element in the sequence

[Ayhon]

splitBy (·==·) [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [2, 2, 2], [3], [2]]
withWindow 2 [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [1, 2], [2, 2], [2, 2], [2, 3], [3, 2]]
withWindow 3 [1, 1, 2, 2, 2, 3, 2] = [[1, 1, 2], [1, 2, 2], [2, 2, 2], [2, 2, 3], [2, 3, 2]]

[James Sully]

It's unfortunate List doesn't have a monad instance for perf reasons. I miss list comprehensions and do notation, I find my

def removals (l : List α) : List (List α) :=
  List.range l.length
  |>.map (l.eraseIdx ·)

much less readable than something like

[l.eraseIdx i | i <- List.range l.length]

[Jannis Limperg]

You can add a local instance if you don't mind the questionable performance.

[James Sully]

for sure. that would go against my aesthetic sensibilities a little though. I think it's good to work with the standard idioms of a language, rather than fighting it

[Mario Carneiro]

it is a functor, so you can use <$> notation instead of .map... not sure if that is any better though

[James Sully]

yeah

[James Sully]

I think one issue is building the list List.range l.length, rather than iterating over a range [0:l.length] directly somehow

[Mario Carneiro]

you can use List.enum to get access to the index

[James Sully]

I don't think that's quite doing what I want in this case, since I don't want the element at the same time, I just want to delete there

[James Sully]

Nat.foldM is certainly enough power, but probably unwieldy

[Mario Carneiro]

if you are going for clear code this is probably fine, if you want maximum performance you probably shouldn't be using lists to begin with

[James Sully]

yeah obviously maximum bikeshedding here

[Mario Carneiro]

and if you want to prove properties this is probably also the easiest to reason about

[James Sully]

would be cool to be able to write [:l.length].map (l.eraseIdx ·) though

[Ayhon]

Idk about implicit conversions, but a .toList or similar for Std.Range would be nice. List.range doesn't handle start and step.

[Kyle Miller]

https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/List.20Nat.20versus.20.22List.20Nat.3A.20.20Type.20.28max.20o.20m.2E2332.29.20.3F/near/485505008 has some up-to-date code for list comprehension notation if you want. With it you could write [l.eraseIdx i | for i in List.range l.length]

[Kim Morrison]

You could also write window as

def List.window [Inhabited α] (width: Nat) (ls: List α) : List (List α) :=
  if h : ls.length < width then
    []
  else
    let n := ls.length - width + 1
    List.ofFn fun (start : Fin n) =>
      List.ofFn fun (i : Fin width) => ls[start.1 + i.1]

Notice there is no runtime bounds check here anymore. This will also make proving easier.

[Kim Morrison]

There's probably a good trick to avoid the if statement.

[Kim Morrison]

If you really cared about keeping track of sizes you would define Vector.window : (k : Nat) → Vector n α → Vector (n + 1 - k) (Vector α k).

[JJ]

wrote some kind of horrifically imperative code for today

def safe (report : List Nat) : Bool :=
  (increasing_safely report) || (increasing_safely report.reverse)

where increasing_safely (report : List Nat) : Bool := Id.run do
    let mut prev := report.head!
    for i in report.tail! do
      if (i < prev + 1) || (prev + 3 < i) then
        return false
      else
        prev <- i
    true

def dampen (report : List Nat) : List (List Nat) := Id.run do
  let mut (head, tail, result) := ([], report, [report])
  for elem in report do
    tail <- tail.tail
    result <- result.concat (head.append tail)
    head <- head.concat elem
  result

def solution (input : String) : String := Id.run do
  let reports :=
    input.stripSuffix "\n" |>.splitOn "\n"
    |>.map (·.splitOn |>.map String.toNat!)
  let mut (p1, p2) := (0, 0)
  for report in reports do
    p1 <- p1 + (if safe report then 1 else 0)
    p2 <- p2 + (if (dampen report).any safe then 1 else 0)
  s!"{p1}, {p2}"

[Patrick Massot]

There is nothing horrific with Lean code written in imperative style using do. Lean itself is mostly written like this.

[Kyle Miller]

Here's a bit of manual pretty printing on my part. Note that the performance of List.concat is linear. If you are always concatenating, it's probably better to use Array, which has (amortized) constant-time pushing to the end.

def safe (report : Array Nat) : Bool :=
  increasing_safely report || increasing_safely report.reverse
where
  increasing_safely (report : Array Nat) : Bool := Id.run do
    let mut prev := report[0]!
    for i in report[1:] do
      if i < prev + 1 || prev + 3 < i then
        return false
      else
        prev <- i
    true

def dampen (report : Array Nat) : Array (Array Nat) := Id.run do
  let mut head := #[]
  let mut result := #[report]
  for h : i in [0:report.size] do
    let elem := report[i]
    result <- result.push (head ++ report[i:].toArray)
    head <- head.push elem
  result

def solution (input : String) : String := Id.run do
  let reports :=
    input.stripSuffix "\n" |>.splitOn "\n"
    |>.map (·.splitOn |>.map String.toNat! |>.toArray)
  let mut p1 := 0
  let mut p2 := 0
  for report in reports do
    if safe report then
      p1 <- p1 + 1
    if (dampen report).any safe then
      p2 <- p2 + 1
  s!"{p1}, {p2}"

(This is completely untested! I'm just editing directly in Zulip.)