Advent of Code 2024 - Day 11

Stream: general

[Chris Henson]

For day 11, I was pretty happy with writing memoization as a state monad, did anyone else take a similar approach? (Here's a link to my repo: https://github.com/chenson2018/advent-of-code/blob/main/2024/lean/AoC/Day11.lean)

[Ayhon]

I have been falling behind on my advent of code problems. Currently I'm at day 10, once I've come over to day 11 I'll post my solution and check out yours!

[Ayhon]

As promised, today I got to day 11 and here's my solution. I feel like it's very similar to yours, but in my case I make the Cached effect much less generic. I also defined a sequence function (which probably already exists somewhere in the standard library, but I con't manage to loogle it) because originally I wanted to do something way more complicated, storing the intermediate generated lists to store results for depths of powers of two. Not viable though :/

Anyways, here's my code

import Std.Internal.Parsec
import Std.Internal.Parsec.String
import Std.Data.HashMap

namespace Day11
open Std.Internal.Parsec.String (pchar pstring skipString skipChar Parser digits digit ws)
open Std.Internal.Parsec (skip many many1 attempt)

abbrev Input := List Nat

def parse_input(content: String): Input :=
  content.split Char.isWhitespace
    |>.filter (¬ ·.isEmpty)
    |>.map (·.toNat!)

def log10 (n : Nat) : Nat :=
  if n ≥ 10 then log10 (n / 10) + 1 else 1

namespace Part1
  def expand(x: Nat): List Nat :=
    let n := log10 x
    if x == 0 then
      [1]
    else if n % 2 == 0 then
      let mask := 10^(n/2)
      [x / mask, x % mask]
    else
      [x*2024]

  def solve(inp: Input): Int :=
    inp
      |> Nat.repeat (·.flatMap expand) 25
      |>.length

  #eval (include_str "../inputs/day11.txt")
    |> parse_input
    |> solve
end Part1


namespace Part2
  abbrev Cache := Std.HashMap (Nat × Nat) Nat
  abbrev Cached α := StateM Cache α

  def sequence(ls: List (Cached α)): Cached (List α) := do match ls with
  | [] => return []
  | x :: xs => return (<- x) :: (<- sequence xs)

  def withCached(args: Nat × Nat)(body: Nat × Nat -> Cached Nat): Cached Nat := do
    match (<- get).get? args with
      | some result => return result
      | none =>
        let result <- body args
        modify (·.insert args result)
        return result

  partial def simulate'(times: Nat)(x: Nat): Cached Nat := do
    match times with
    | 0 => return 1
    | _ => withCached (times, x) fun (times, x) =>
        Part1.expand x
          |>.map (simulate' (times-1))
          |> sequence
          |>.map List.sum

  partial def simulate(times: Nat)(x: Nat): Nat :=
    simulate' times x
      |>.run ∅
      |>.run
      |>.1

  partial def solve(inp: Input): Int := inp |>.map (simulate 75) |>.sum

  #eval (include_str "../inputs/day11.txt")
    |> parse_input
    |> solve
end Part2

[Paul Nelson]

import Std.Data.HashSet
import Mathlib.Logic.Function.Iterate

def parse (input : String) : List Nat :=
  input.splitOn "\n" |>.filter (!·.isEmpty) |>.head!
    |>.splitOn " " |>.filter (!·.isEmpty) |>.map String.toNat!

def blink : Nat → List Nat
  | 0 => [1]
  | n =>
    let str := n.repr
    match str.length % 2 with
    | 1 => [2024 * n]
    | _ =>
      let mid := String.Pos.mk (str.length / 2)
      [str.extract 0 mid, str.extract mid str.endPos].map String.toNat!

abbrev State := Std.HashMap Nat Nat

def State.init (input : List Nat) : State :=
  input.foldl (·.insert · 1) Std.HashMap.empty

def State.next (state : State) : State := Id.run do
  let mut newState := Std.HashMap.empty
  for (k, v) in state do
    for n in blink k do
      newState := newState.insert n (v + newState.getD n 0)
  newState

def numberOfStones (fuel : Nat) (input : List Nat) : Nat :=
  let finalState := Nat.iterate State.next fuel (State.init input)
  finalState.fold (fun acc _ v => acc + v) 0

def part1 : List Nat → Nat := numberOfStones 25
def part2 : List Nat → Nat := numberOfStones 75