Advent of Code 2024 - Day 1

Stream: general

[James Sully]

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

import Batteries.Data.HashMap

def String.lines (s : String) : List String := s.split (· == '\n')

structure Input where
  l1 : List Nat
  l2 : List Nat

def parseLine (s : String) : Option (Nat × Nat) := do
  let ns : List Nat ← s.splitOn "   " |>.mapM (·.toNat?)
  match ns with
  | [n1, n2] => .some (n1, n2)
  | _ => .none

def parseInput (input : String) : Option Input := do
  let pairs ← input.lines.mapM parseLine
  let (l1, l2) := pairs.unzip
  .some ⟨l1, l2⟩

def part1 (input : Input) : Nat :=
  let (sortedl1, sortedl2) := (input.l1.mergeSort, input.l2.mergeSort)
  let differences := List.zipWith Int.subNatNat sortedl1 sortedl2
    |>.map Int.natAbs
  differences.sum

-- definitely missing haskell's Map.alter or rust's entry api
open Batteries (HashMap)
def counts (ns : List Nat) : HashMap Nat Nat :=
  ns.foldl (init := ∅) λ map n ↦ match map.find? n with
  | .some count => map.insert n (count + 1)
  | .none => map.insert n 1

def part2 (input : Input) : Nat :=
  let l2_counts := counts input.l2
  input.l1.map (λ n ↦ n * l2_counts.findD n 0) |>.sum

def Day01.main : IO Unit := do
  let input ← IO.FS.readFile "input.txt"
  let .some parsed := parseInput input | do
    IO.println "error parsing input"

  let result1 := part1 parsed
  let result2 := part2 parsed
  IO.println s!"Part 1: {result1}"
  IO.println s!"Part 2: {result2}"

[Kim Morrison]

docs#Std.HashMap.alter and docs#Std.HashMap.modify

[Kim Morrison]

(more generally, I'd advise using Std.HashMap instead of Batteries.HashMap now.)

[James Sully]

Nice, thanks. I thought Batteries was a renaming of Std, is this something different?

[Kim Morrison]

Std was renamed to Batteries to make room for the new Std, which is packaged as part of the language distribution.

[James Sully]

Gotcha. Awesome

[James Sully]

slightly nicer counts:

open Std (HashMap)
def counts (ns : List Nat) : HashMap Nat Nat :=
  ns.foldl (init := ∅) λ map n ↦ map.alter n λ
  | .none => .some 1
  | .some count => .some <| count + 1

[Jared Corduan]

does anything have to be added to the lake config files in order to use Std? I get the error:

invalid field 'mergeSort', the environment does not contain 'List.mergeSort'

when I do this:

import Std
#eval ([] : List Nat).mergeSort

(I'm using lean4:stable )

[Edward van de Meent]

what does #eval Lean.versionString say?

[Edward van de Meent]

btw, afaict List.mergeSort doesn't even live in Std, it's in Init (and therefore shouldn't need any imports, i think)

[Jared Corduan]

4.11.0

[Jared Corduan]

oh, maybe I'm behind, I'll do an update and see if being on 4.14.0 helps. thanks!

[Jared Corduan]

that was it!

[JJ]

decided to delay advent of code by a month this year to focus on finals... i'm going to try to do every day in lean this january! here's my day 1 for those interested, stylistic feedback much appreciated

def solution (input : String): String :=
  let input := input.stripSuffix "\n"|>.splitOn "\n"
  let l1 := input.map <| fun x => x.splitOn "   " |>.get! 0 |>.toInt!
  let l2 := input.map <| fun x => x.splitOn "   " |>.get! 1 |>.toInt!
  let p1 :=
    List.foldl (· + ·) 0 <|
      List.zipWith (fun a b => (a - b).natAbs) l1.mergeSort l2.mergeSort
  let p2 :=
    List.foldl (· + ·) 0 <|
      List.map (fun a => a * List.count a l2) l1
  s!"{p1}, {p2}"

[JJ]

today taught me about · simple lambda notation and a good number of list helpers. something i don't know yet is how to get! the last element of a list, and generally how to use the module system... would like to be able to run lake exe aoc Day⟨num⟩ and run different modules in my Solutions/ folder while keeping initial input parsing in Main.lean, but i haven't yet figured out how to set up that structure yet. i think i'm going to try and scoure other people's solutions for interesting syntax sugar after solving each day...

[JJ]

also important note: (· + ·) looks like a little happy face