Advent of Code 2024 - Day 5

Stream: general

[Marcelo Fornet]

Here's my solution. Please post your own solution!

https://github.com/mfornet/advent-of-code-2024/blob/main/Aoc2024/Day05.lean

The solution finds the topological sort of the given graph, but this was not necessary (it was only clear in hindsight, I don't think the text gives any hint about the structure of the test cases).

[Marcelo Fornet]

Cross-posting from discord

I want to prove topological sort always terminate, i.e remove the partial modifier from here: https://github.com/mfornet/advent-of-code-2024/blob/main/Aoc2024/Day05.lean#L68-L76

The condition that this always decrease is the pair <sum of indegrees, size of the queue>. Can anyone help me get started on how do I indicate Lean that this is the decreasing relationship, I'll provide the proof myself, it is just about how to get the statement.

I can't fully grasp how to do it by seeing examples of termination_by.

[Matt Russell]

https://github.com/mdr/aoc-2024/blob/main/Aoc2024/Day05/Solve.lean

[Ayhon]

Ok, this time it took me a bit longer than usual. I missunderstood the problem statement and programmed something more complicated than needed. It's still not the cleanest, but it definitely works

import Std.Internal.Parsec
import Std.Internal.Parsec.String

namespace Day5
open Std.Internal.Parsec
open Std.Internal.Parsec.String

structure Input where
  edges: List (Nat × Nat)
  reports: Array (Array Nat)
  deriving Repr, Inhabited

def p_order := do
  let lesser <- digits
  skipChar '|'
  let greater <- digits
  return (lesser, greater)

def p_report := do
  let p_optional_comma := attempt (skipChar ',') <|> pure ()
  let list <- many (digits <* p_optional_comma)
  return list

def parse_input(content: String): Option (Input) :=
  let parser := do
    let orders <- many (p_order <* skipChar '\n')
    skipChar '\n'
    let reports <- many (p_report <* skipChar '\n')
    eof
    return {
      edges := orders.toList,
      reports := reports.filter (not ∘ Array.isEmpty)
    : Input}

  match parser content.iter with
  | .success _ res => some res
  | .error _ _ => none

namespace Part1
  def Array.toSlidingWindow[Inhabited α](width: Nat)(ls: Array α): Array (Vector α width) :=
    if ls.size < width then
      #[]
    else
      let n := ls.size + 1 - width
      Array.ofFn fun (⟨start, _⟩: Fin n) =>
        Vector.ofFn fun (⟨offset, _⟩: Fin width) =>
            ls[start + offset]

  def valid(edges: List (Nat × Nat))(report: Array Nat): Bool :=
    open Part1 in
    report.toSlidingWindow 2
      |>.all fun
        | #v[u,v] => ¬ edges.contains (v,u)
        | _ => false

  def middle(report: Array Nat): Nat := report[report.size/2]!

  def solve'(info: Input): Int :=
    info.reports
      |>.toList
      |>.filter (valid info.edges ·)
      |>.map middle
      |>.sum

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


namespace Part2
  def fix(edges: List (Nat × Nat))(report: Array Nat): Array Nat := Id.run do
    let mut res := report
    for i in [1:report.size] do
      for j in [0:i] do
        if edges.contains (res[j]!, res[i]!) then
          res := res.swapIfInBounds i j
    return res

  def solve'(info: Input): Int :=
    info.reports
      |>.filter (¬ Part1.valid info.edges ·)
      |>.map (Part1.middle ∘ fix info.edges)
      |>.toList
      |>.sum

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

[Ayhon]

I do have some questions on how to simplify my Part1.valid function. I would assume that Lean can assume that a Vector a 2 has only 2 entries, why do I need to specify the other branch though?

  def valid(edges: List (Nat × Nat))(report: Array Nat): Bool :=
    open Part1 in
    report.toSlidingWindow 2
      |>.all fun
        | #v[u,v] => ¬ edges.contains (v,u)
        | _ => false

At least I couldn't manage to make it work without