Advent of Code 2024 - Day 6

Stream: general

[Ayhon]

I haven't seen any thread/channel dedicated to AoC day 6 solutions and later. It's a shame, becuase I really enjoyed the discussions that happened in them and reading the code that people shared. That's why I share my version in hope others may join me in sharing theirs.

I'm not super happy with my solution, but it definitely works. I think I could simplify a bit the definitions. I'm looking forward to reading other's solutions

import Std.Internal.Parsec
import Std.Internal.Parsec.String
import Std.Data.HashSet

namespace Day6
open Std.Internal.Parsec
open Std.Internal.Parsec.String


inductive Direction where
| Up
| Right
| Down
| Left
deriving Inhabited, Repr, BEq, Hashable

def Direction.turn: Direction -> Direction
| Up => Right
| Right => Down
| Down => Left
| Left => Up

inductive Cell where
| Obstacle
| Nothing
| Guard
deriving Inhabited, Repr

abbrev Position := Nat×Nat
structure Guard where
  pos: Position
  dir: Direction
  deriving Inhabited, Repr, BEq, Hashable

abbrev Grid := Array (Array Cell)

def Grid.width(g: Grid) := if h: 0 < g.size then (g[0]'h).size else 0
def Grid.height(g: Grid) := g.size

def Grid.get!(grid: Grid)(pos: Position) := Id.run do
  let (x,y) := pos
  let some row := grid[x]? | panic s!"Tried to access out of bounds x={x}"
  let some cell := row[y]? | panic s!"Tried to access out of bounds y={y}"
  cell

structure Lab where
  grid: Grid
  guard: Guard
deriving Inhabited

instance instReprLab:  Repr Lab where
  reprPrec lab _ := lab.grid.toList
    |>.map (fun row => row.toList
      |>.map (fun
        | Cell.Nothing => "░"
        | Cell.Guard => match lab.guard.dir with
          | Direction.Up => "^"
          | Direction.Left => "<"
          | Direction.Right => ">"
          | Direction.Down => "v"
        | Cell.Obstacle => "#"
        )
      |> String.join
    )
    |> String.intercalate "\n"

def List.enum' [Inhabited α](ls: List α) :=
  if ls.isEmpty then []
  else
    let rec enumFrom(n: Nat)(s: Nat)(ls: List α)(inv: s + ls.length = n): List (Fin n  × α)
    := match ls with
      | [] => []
      | x :: xs =>
        let m := ls.length
        let index: Fin n := by
          constructor <;> try exact s
          rw [<-inv]
          have h: 0 < (x :: xs).length := by
            rw [List.length_cons]
            exact Nat.zero_lt_succ xs.length
          apply Nat.lt_add_of_pos_right h
        have inv':  s + 1 + xs.length = n := by
          rw [Nat.add_assoc, Nat.add_comm 1,<-List.length_cons x]
          exact inv
        let rest := enumFrom n (s + 1) xs inv'
        (index, x) :: rest
    enumFrom ls.length 0 ls (by simp)

def Lab.fromGrid(grid: Grid): Option Lab := do
  let guard <- grid.toList
      |>.enum
      |>.findSome? (fun (i, row) =>
        row.toList
          |>.enum
          |>.findSome? fun (j, cell) =>
            match cell with
            | Cell.Guard => some ⟨(i,j), Direction.Up⟩
            | _ => none
    )
  return {grid := grid, guard := guard : Lab}


abbrev Input := Lab

def parse_input(content: String): Option (Input) := do
  let p_cell := do
    pchar '.' *> pure Cell.Nothing <|>
    pchar '#' *> pure Cell.Obstacle <|>
    pchar '^' *> pure Cell.Guard
  let parser := many ((many p_cell) <* skipChar '\n')
  let .success _ grid := parser content.iter | failure
  (<- Lab.fromGrid grid)

def andThen(a: α)(b: Prop)[Decidable b]: Option α := if b then some a else none
def Grid.ahead (grid: Grid)(guard: Guard): Option Position := do
    let (w,h) := (grid.width, grid.height)
    let (x,y) := guard.pos
    match guard.dir with
      | Direction.Up    => (x  > 0)  |> andThen (x-1, y)
      | Direction.Right => (y+1 < w) |> andThen (x, y+1)
      | Direction.Down  => (x+1 < h) |> andThen (x+1, y)
      | Direction.Left  => (y  > 0)  |> andThen (x, y-1)

def Lab.toString (lab: Lab)(positions: Std.HashSet Position) := List.range lab.grid.height
  |>.map (fun i =>
  List.range lab.grid.width
    |>.map (fun j => if positions.contains (i,j) then "X" else "░")
    |> String.join
  )
  |> String.intercalate "\n"

def Lab.newGuardPosition(lab: Lab): Option Guard := getPosition lab 4 where
  getPosition lab
  | 0 => none
  | limit+1 => do
    let (nx,ny) <- lab.grid.ahead lab.guard
    let cell <- (<- lab.grid[nx]?)[ny]?
    match cell with
    | Cell.Obstacle =>
      getPosition {lab with guard := {lab.guard with dir := lab.guard.dir.turn}} limit
    | _ => some {lab.guard with pos := (nx,ny)}

def Lab.simulate(lab: Lab): Option Lab := do
  let newGuard <- Lab.newGuardPosition lab
  let (x,y) := lab.guard.pos
  let (nx,ny) := newGuard.pos
  return {lab with
    grid := lab.grid
      |>.modify x (·.set! y Cell.Nothing)
      |>.modify nx (·.set! ny (Cell.Guard))
    guard := newGuard
  }

namespace Part1
  def solve'(lab: Lab): Int :=  go (4*lab.grid.width*lab.grid.height) {lab.guard.pos} lab where
    go: Nat -> Std.HashSet Position -> Lab -> Int
    | 0, _, _ => -1
    | fuel+1, positions, lab =>
      match Lab.simulate lab with
      | some newLab =>
        go fuel (positions.insert newLab.guard.pos) newLab
      | none => Id.run do
        Int.ofNat positions.size

  partial def solve: Option (Input) -> Int
  | .some input => solve' input
  | .none => -1
end Part1

namespace Part2
  partial def hasCycle(lab: Lab): Bool := go {lab.guard} lab where
    go : Std.HashSet Guard -> Lab -> Bool
    | seenConfigurations, lab => Id.run do
      let some newLab := lab.simulate | false
      let hasCycle := seenConfigurations.contains newLab.guard
      hasCycle || go (seenConfigurations.insert newLab.guard) newLab

  partial def solve'(lab: Lab): Int :=
    lab.grid.toList
      |> List.enum'
      |>.map (fun (i, row) =>
        row.toList
          |> List.enum'
          |>.countP fun (j, c) => match c with
            | Cell.Nothing =>
              let modLab := {lab with grid := lab.grid.set i (row.set j Cell.Obstacle)}
              let res := hasCycle modLab
              res
            | _ => false
      )
      |>.sum

  partial def solve: Option (Input) -> Int
  | .some input => solve' input
  | .none => -1
end Part2

[Ayhon]

I'm a bit behind on AoC problems, but once I've solved day 7 and day 8 I'm thinking of posting my solutions. If someone wants to beat me to it, please, feel free to do so!

[Matt Russell]

Thanks for posting! I wasn't super happy with my Day 6 - https://github.com/mdr/aoc-2024/blob/main/Aoc2024/Day06/Solve.lean
I thought I'd mess around with the state monad, but I think it just made it more complex than a more direct approach in the end.
Also needing to pass around the right size fuel felt silly, I think I need to start learning about how to prove termination to Lean (I need to learn about proving things in Lean full stop really!)

[Ayhon]

Actually, I found your solution from the link you posted for Day 5! I saw it had some wip as the commit message that introduced it so I assumed that it wasn't finished yet.

I liked the idea of having a set of obstacles and bounds and doing away with the grid, I believe it makes things clearer. I also share your opinion on fuel. My prior solution was to add partial all over the place, but while the code is more readable, I do think it's against Lean's spirit, so to say.

I imagine there could be a monad though, in order not to have to pass fuel directly all the time. Something like

inductive StepBound (a: Type): Nat -> Type where
| TimedOut : StepBound a 0
| Finished (val: a): StepBound a steps
| StillRunning(n: Nat)(cont : Unit => StepBound a n): StepBound a n

That might be a cool exercise for monads and monad transformers, I'll try to formalize it a bit more once I find the time!

[Greg Shuflin]

Ayhon said:

I haven't seen any thread/channel dedicated to AoC day 6 solutions and later. It's a shame, becuase I really enjoyed the discussions that happened in them and reading the code that people shared. That's why I share my version in hope others may join me in sharing theirs.

I'm not super happy with my solution, but it definitely works. I think I could simplify a bit the definitions. I'm looking forward to reading other's solutions

import Std.Internal.Parsec
import Std.Internal.Parsec.String
import Std.Data.HashSet

namespace Day6
open Std.Internal.Parsec
open Std.Internal.Parsec.String


inductive Direction where
| Up
| Right
| Down
| Left
deriving Inhabited, Repr, BEq, Hashable

def Direction.turn: Direction -> Direction
| Up => Right
| Right => Down
| Down => Left
| Left => Up

inductive Cell where
| Obstacle
| Nothing
| Guard
deriving Inhabited, Repr

abbrev Position := Nat×Nat
structure Guard where
  pos: Position
  dir: Direction
  deriving Inhabited, Repr, BEq, Hashable

abbrev Grid := Array (Array Cell)

def Grid.width(g: Grid) := if h: 0 < g.size then (g[0]'h).size else 0
def Grid.height(g: Grid) := g.size

def Grid.get!(grid: Grid)(pos: Position) := Id.run do
  let (x,y) := pos
  let some row := grid[x]? | panic s!"Tried to access out of bounds x={x}"
  let some cell := row[y]? | panic s!"Tried to access out of bounds y={y}"
  cell

structure Lab where
  grid: Grid
  guard: Guard
deriving Inhabited

instance instReprLab:  Repr Lab where
  reprPrec lab _ := lab.grid.toList
    |>.map (fun row => row.toList
      |>.map (fun
        | Cell.Nothing => "░"
        | Cell.Guard => match lab.guard.dir with
          | Direction.Up => "^"
          | Direction.Left => "<"
          | Direction.Right => ">"
          | Direction.Down => "v"
        | Cell.Obstacle => "#"
        )
      |> String.join
    )
    |> String.intercalate "\n"

def List.enum' [Inhabited α](ls: List α) :=
  if ls.isEmpty then []
  else
    let rec enumFrom(n: Nat)(s: Nat)(ls: List α)(inv: s + ls.length = n): List (Fin n  × α)
    := match ls with
      | [] => []
      | x :: xs =>
        let m := ls.length
        let index: Fin n := by
          constructor <;> try exact s
          rw [<-inv]
          have h: 0 < (x :: xs).length := by
            rw [List.length_cons]
            exact Nat.zero_lt_succ xs.length
          apply Nat.lt_add_of_pos_right h
        have inv':  s + 1 + xs.length = n := by
          rw [Nat.add_assoc, Nat.add_comm 1,<-List.length_cons x]
          exact inv
        let rest := enumFrom n (s + 1) xs inv'
        (index, x) :: rest
    enumFrom ls.length 0 ls (by simp)

def Lab.fromGrid(grid: Grid): Option Lab := do
  let guard <- grid.toList
      |>.enum
      |>.findSome? (fun (i, row) =>
        row.toList
          |>.enum
          |>.findSome? fun (j, cell) =>
            match cell with
            | Cell.Guard => some ⟨(i,j), Direction.Up⟩
            | _ => none
    )
  return {grid := grid, guard := guard : Lab}


abbrev Input := Lab

def parse_input(content: String): Option (Input) := do
  let p_cell := do
    pchar '.' *> pure Cell.Nothing <|>
    pchar '#' *> pure Cell.Obstacle <|>
    pchar '^' *> pure Cell.Guard
  let parser := many ((many p_cell) <* skipChar '\n')
  let .success _ grid := parser content.iter | failure
  (<- Lab.fromGrid grid)

def andThen(a: α)(b: Prop)[Decidable b]: Option α := if b then some a else none
def Grid.ahead (grid: Grid)(guard: Guard): Option Position := do
    let (w,h) := (grid.width, grid.height)
    let (x,y) := guard.pos
    match guard.dir with
      | Direction.Up    => (x  > 0)  |> andThen (x-1, y)
      | Direction.Right => (y+1 < w) |> andThen (x, y+1)
      | Direction.Down  => (x+1 < h) |> andThen (x+1, y)
      | Direction.Left  => (y  > 0)  |> andThen (x, y-1)

def Lab.toString (lab: Lab)(positions: Std.HashSet Position) := List.range lab.grid.height
  |>.map (fun i =>
  List.range lab.grid.width
    |>.map (fun j => if positions.contains (i,j) then "X" else "░")
    |> String.join
  )
  |> String.intercalate "\n"

def Lab.newGuardPosition(lab: Lab): Option Guard := getPosition lab 4 where
  getPosition lab
  | 0 => none
  | limit+1 => do
    let (nx,ny) <- lab.grid.ahead lab.guard
    let cell <- (<- lab.grid[nx]?)[ny]?
    match cell with
    | Cell.Obstacle =>
      getPosition {lab with guard := {lab.guard with dir := lab.guard.dir.turn}} limit
    | _ => some {lab.guard with pos := (nx,ny)}

def Lab.simulate(lab: Lab): Option Lab := do
  let newGuard <- Lab.newGuardPosition lab
  let (x,y) := lab.guard.pos
  let (nx,ny) := newGuard.pos
  return {lab with
    grid := lab.grid
      |>.modify x (·.set! y Cell.Nothing)
      |>.modify nx (·.set! ny (Cell.Guard))
    guard := newGuard
  }

namespace Part1
  def solve'(lab: Lab): Int :=  go (4*lab.grid.width*lab.grid.height) {lab.guard.pos} lab where
    go: Nat -> Std.HashSet Position -> Lab -> Int
    | 0, _, _ => -1
    | fuel+1, positions, lab =>
      match Lab.simulate lab with
      | some newLab =>
        go fuel (positions.insert newLab.guard.pos) newLab
      | none => Id.run do
        Int.ofNat positions.size

  partial def solve: Option (Input) -> Int
  | .some input => solve' input
  | .none => -1
end Part1

namespace Part2
  partial def hasCycle(lab: Lab): Bool := go {lab.guard} lab where
    go : Std.HashSet Guard -> Lab -> Bool
    | seenConfigurations, lab => Id.run do
      let some newLab := lab.simulate | false
      let hasCycle := seenConfigurations.contains newLab.guard
      hasCycle || go (seenConfigurations.insert newLab.guard) newLab

  partial def solve'(lab: Lab): Int :=
    lab.grid.toList
      |> List.enum'
      |>.map (fun (i, row) =>
        row.toList
          |> List.enum'
          |>.countP fun (j, c) => match c with
            | Cell.Nothing =>
              let modLab := {lab with grid := lab.grid.set i (row.set j Cell.Obstacle)}
              let res := hasCycle modLab
              res
            | _ => false
      )
      |>.sum

  partial def solve: Option (Input) -> Int
  | .some input => solve' input
  | .none => -1
end Part2

is there a reason you defined andThen instead of just using the built-in >>= operator?

[Ayhon]

If I understood correctly, >>= is the same as the monadic bind. But then, my andThen doesn't have the same signature, since its first parameter is a Bool and not Option a. I was more thinking of Rust's bool::then, and since I couldn't find something that fit the signature in Loogle I coded my own

[Ayhon]

@Greg Shuflin, does this answer your question? I haven't actually tested whether >>= can be used in this case, but assumed it wouldn't type check

[Greg Shuflin]

Ayhon said:

Greg Shuflin, does this answer your question? I haven't actually tested whether >>= can be used in this case, but assumed it wouldn't type check

ah yeah, I misunderstood at first glance how your andThen was different from >>=

[Paul Nelson]

@Ayhon How long does your code take on the actual 101*103 input for Part 2? When I try your code (or my own) on that part, it takes several minutes.

[Ayhon]

This is what I get when I run time lake exe aoc24 for day 6

➜  aoc24 git:(main) ✗ time lake exe aoc24
Part 1: 5318
Part 2: 1831
lake exe aoc24  7,89s user 0,22s system 100% cpu 8,049 total

[Ayhon]

It may be that I have a reasonably new laptop. I'm using an AMD Ryzen 7 7840U CPU

[Paul Nelson]

Thanks, good tip -- I didn't know about lake exe and hadn't thought to look into compiling :). Runs fast on mine now too

[Paul Nelson]

Here's mine

import Lean.Data.HashSet

inductive Direction where
  | Up | Right | Down | Left
  deriving BEq, Hashable, Repr

instance : Inhabited Direction where
  default := Direction.Up

def Direction.next (d : Direction) : Direction :=
  let dirs := #[Up, Right, Down, Left]
  let i := (dirs.findIdx? (· == d)).get!
  dirs[(i + 1) % 4]!

abbrev Point := Nat × Nat

def step (x_max y_max : Nat) (pos : Point) (dir : Direction) : Option Point :=
  match dir, pos with
  | .Up,    ⟨x, y⟩ => if x > 0 then some ⟨x - 1, y⟩ else none
  | .Down,  ⟨x, y⟩ => if x < x_max then some ⟨x + 1, y⟩ else none
  | .Left,  ⟨x, y⟩ => if y > 0 then some ⟨x, y - 1⟩ else none
  | .Right, ⟨x, y⟩ => if y < y_max then some ⟨x, y + 1⟩ else none

abbrev Grid := Array (Array Char)

structure Input where
  grid : Grid
  start : Point

def Array.enum (ar : Array α) : Array (Nat × α) :=
  Array.mapIdx (fun i x => (i, x)) ar

def findInGrid (grid : Grid) (char : Char) : Option Point :=
  grid.enum.findSome? fun (i, row) =>
    row.enum.findSome? fun (j, c) =>
      if c == char then some ⟨i, j⟩ else none

def parse (input : String) : Input :=
  let grid := input.splitOn "\n"
    |>.filter (·.length > 0)
    |>.map String.toList
    |>.map List.toArray
    |>.toArray
  let start := findInGrid grid '^' |>.get!
  ⟨ grid, start ⟩

structure State where
  pos : Point
  dir : Direction
  deriving BEq, Hashable, Repr, Inhabited

def facingObstacle (grid : Grid) (pos : Point) (dir : Direction) : Bool :=
  let next_pos := step (grid.size - 1) (grid[0]!.size - 1) pos dir
  match next_pos with
  | none => false
  | some next_pos => grid[next_pos.1]![next_pos.2]! == '#'

def State.next (grid : Grid) (state : State) : Option State :=
  let ⟨pos, dir⟩ := state
  if facingObstacle grid pos dir then
    some ⟨pos, dir.next⟩
  else
    step (grid.size - 1) (grid[0]!.size - 1) pos dir
      |>.map (fun p => ⟨p, dir⟩)

def exitPath (grid : Grid) (start : State) : Option (Array State) :=
  let max_states := 4 * grid.size * grid[0]!.size
  let rec go (fuel : Nat) (seen : Std.HashSet State) (path : Array State)
      (current : State) : Option (Array State) :=
    match fuel with
    | 0 => panic! "Exceeded maximum possible states"
    | fuel+1 =>
      if seen.contains current then
        none
      else
        let path := path.push current
        match current.next grid with
        | none => some path
        | some next => go fuel (seen.insert current) path next
  go max_states Std.HashSet.empty #[] start

def part1 (input : Input) : Nat :=
  exitPath input.grid ⟨input.start, Direction.Up⟩
  |>.getD (panic! "Unexpected cycle detected")
  |>.map (·.pos)
  |>.foldl (·.insert ·) Std.HashSet.empty
  |>.size

def windows2 {α : Type} (xs : List α) : List (α × α) :=
  xs.zip xs.tail

def part2 (input : Input) : Nat :=
  let path := match exitPath input.grid ⟨input.start, Direction.Up⟩ with
    | none => panic! "Unexpected cycle detected"
    | some path => path
  -- Collect (state, position) pairs where position obstructs state.
  let trials :=
    let rec go (pairs : List (State × State))
        (seen : Std.HashSet Point) : List (State × Point) :=
      match pairs with
      | [] => []
      | (before, after) :: rest =>
        if seen.contains after.pos || after.pos == input.start then
          go rest seen
        else
          (before, after.pos) :: go rest (seen.insert after.pos)
    go (windows2 path.toList) Std.HashSet.empty
  trials |>.filter (fun (start, barrier) =>
      let grid := input.grid.modify barrier.1 (fun a => a.set! barrier.2 '#')
        match exitPath grid start with
        | none => true
        | _ => false)
    |>.length