Day 4: Scratchcards

Megathread guidelines

  • Keep top level comments as only solutions, if you want to say something other than a solution put it in a new post. (replies to comments can be whatever)
  • Code block support is not fully rolled out yet but likely will be in the middle of the event. Try to share solutions as both code blocks and using something such as https://topaz.github.io/paste/ or pastebin (code blocks to future proof it for when 0.19 comes out and since code blocks currently function in some apps and some instances as well if they are running a 0.19 beta)

FAQ

  • What is this?: Here is a post with a large amount of details: https://programming.dev/post/6637268
  • Where do I participate?: https://adventofcode.com/
  • Is there a leaderboard for the community?: We have a programming.dev leaderboard with the info on how to join in this post: https://programming.dev/post/6631465

🔒This post will be unlocked when there is a decent amount of submissions on the leaderboard to avoid cheating for top spots

🔓 Unlocked after 8 mins

  • soulsource@discuss.tchncs.de
    ·
    10 months ago

    [Language: Lean4]

    I'll only post the actual parsing and solution. I have written some helpers which are in other files, as is the main function. For the full code, please see my github repo.

    I'm pretty sure that implementing part 2 in a naive way would cause Lean to demand a proof of termination, what might not be that easy to supply in this case... Luckily there's a way more elegant and way faster solution than the naive one, that can use structural recursion and therefore doesn't need an extra proof of termination.

    Solution 
    structure Card where
  id : Nat
  winningNumbers : List Nat
  haveNumbers : List Nat
  deriving Repr

private def Card.matches (c : Card) : Nat :=
  flip c.haveNumbers.foldl 0 λo n ↦
    if c.winningNumbers.contains n then o + 1 else o

private def Card.score : Card → Nat :=
  (· / 2) ∘ (2^·) ∘ Card.matches

abbrev Deck := List Card

private def Deck.score : Deck → Nat :=
  List.foldl (· + ·.score) 0

def parse (input : String) : Option Deck := do
  let mut cards : Deck := []
  for line in input.splitOn "\n" do
    if line.isEmpty then
      continue
    let cs := line.splitOn ":"
    if p : cs.length = 2 then
      let f := String.trim $ cs[0]'(by simp[p])
      let g := String.trim $ cs[1]'(by simp[p])
      if not $ f.startsWith "Card " then
        failure
      let f := f.drop 5 |> String.trim
      let f ← f.toNat?
      let g := g.splitOn "|"
      if q : g.length = 2 then
        let winners := String.trim $ g[0]'(by simp[q])
        let draws := String.trim $ g[1]'(by simp[q])
        let toNumbers := λ(s : String) ↦
          s.split (·.isWhitespace)
          |> List.filter (not ∘ String.isEmpty)
          |> List.mapM String.toNat?
        let winners ← toNumbers winners
        let draws ← toNumbers draws
        cards := {id := f, winningNumbers := winners, haveNumbers := draws : Card} :: cards
      else
        failure
    else
      failure
  return cards -- cards is **reversed**, that's intentional. It doesn't affect part 1, but makes part 2 easier.

def part1 : Deck → Nat := Deck.score

def part2 (input : Deck) : Nat :=
  -- Okay, doing this brute-force is dumb.
  -- Instead let's compute how many cards each original card is worth, and sum that up.
  -- This relies on parse outputting the cards in **reverse** order.
  let multipliers := input.map Card.matches
  let sumNextN : Nat → List Nat → Nat := λn l ↦ (l.take n).foldl (· + ·) 0
  let rec helper : List Nat → List Nat → List Nat := λ input output ↦ match input with
    | [] => output
    | a :: as => helper as $ (1 + (sumNextN a output)) :: output
  let worths := helper multipliers []
  worths.foldl (· + ·) 0