Day 6: Wait for It

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/ , pastebin, or github (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

  • soulsource@discuss.tchncs.de
    2·
    1 年前

    [Language: Lean4]

    This one was straightforward, especially since Lean’s Floats are 64bits. There is one interesting piece in the solution though, and that’s the function that combines two integers, which I wrote because I want to use the same parse function for both parts. This combineNumbers function is interesting, because it needs a proof of termination to make the Lean4 compiler happy. Or, in other words, the compiler needs to be told that if n is larger than 0, n/10 is a strictly smaller integer than n. That proof actually exists in Lean’s standard library, but the compiler doesn’t find it by itself. Supplying it is as easy as invoking the simp tactic with that proof, and a proof that n is larger than 0.

    As with the previous days, I won’t post the full source here, just the relevant parts. The full solution is on github, including the main function of the program, that loads the input file and runs the solution.

    Solution 
    structure Race where
  timeLimit : Nat
  recordDistance : Nat
  deriving Repr

private def parseLine (header : String) (input : String) : Except String (List Nat) := do
  if not $ input.startsWith header then
    throw s!"Unexpected line header: {header}, {input}"
  let input := input.drop header.length |> String.trim
  let numbers := input.split Char.isWhitespace
    |> List.map String.trim
    |> List.filter (not ∘ String.isEmpty)
  numbers.mapM $ Option.toExcept s!"Failed to parse input line: Not a number {input}" ∘  String.toNat?

def parse (input : String) : Except String (List Race) := do
  let lines := input.splitOn "\n"
    |> List.map String.trim
    |> List.filter (not ∘ String.isEmpty)
  let (times, distances) ← match lines with
    | [times, distances] =>
      let times ← parseLine "Time:" times
      let distances ← parseLine "Distance:" distances
      pure (times, distances)
    | _ => throw "Failed to parse: there should be exactly 2 lines of input"
  if times.length != distances.length then
    throw "Input lines need to have the same number of, well, numbers."
  let pairs := times.zip distances
  if pairs = [] then
    throw "Input does not have at least one race."
  return pairs.map $ uncurry Race.mk

-- okay, part 1 is a quadratic equation. Simple as can be
-- s = v * tMoving
-- s = tPressed * (tLimit - tPressed)
-- (tPressed - tLimit) * tPressed + s = 0
-- tPressed² - tPressed * tLimit + s = 0
-- tPressed := tLimit / 2 ± √(tLimit² / 4 - s)
-- beware: We need to _beat_ the record, so s here is the record + 1

-- Inclusive! This is the smallest number that can win, and the largest number that can win
private def Race.timeRangeToWin (input : Race) : (Nat × Nat) :=
  let tLimit  := input.timeLimit.toFloat
  let sRecord := input.recordDistance.toFloat
  let tlimitHalf := 0.5 * tLimit
  let theRoot := (tlimitHalf^2 - sRecord - 1.0).sqrt
  let lowerBound := tlimitHalf - theRoot
  let upperBound := tlimitHalf + theRoot
  let lowerBound := lowerBound.ceil.toUInt64.toNat
  let upperBound := upperBound.floor.toUInt64.toNat
  (lowerBound,upperBound)

def part1 (input : List Race) : Nat :=
  let limits := input.map Race.timeRangeToWin
  let counts := limits.map $ λ p ↦ p.snd - p.fst + 1 -- inclusive range
  counts.foldl (· * ·) 1

-- part2 is the same thing, but here we need to be careful.
-- namely, careful about the precision of Float. Which luckily is enough, as confirmed by pen&paper
-- but _barely_ enough.
-- If Lean's Float were an actual C float and not a C double, this would not work.

-- we need to concatenate the numbers again (because I don't want to make a separate parse for part2)
private def combineNumbers (left : Nat) (right : Nat) : Nat :=
  let rec countDigits := λ (s : Nat) (n : Nat) ↦
    if p : n > 0 then
      have : n > n / 10 := by simp[p, Nat.div_lt_self]
      countDigits (s+1) (n/10)
    else
      s
  let d := if right = 0 then 1 else countDigits 0 right
  left * (10^d) + right

def part2 (input : List Race) : Nat :=
  let timeLimits := input.map Race.timeLimit
  let timeLimit := timeLimits.foldl combineNumbers 0
  let records := input.map Race.recordDistance
  let record := records.foldl combineNumbers 0
  let limits := Race.timeRangeToWin $ {timeLimit := timeLimit, recordDistance := record}
  limits.snd - limits.fst + 1 -- inclusive range

open DayPart
instance : Parse ⟨6, by simp⟩ (ι := List Race) where
  parse := parse

instance : Part ⟨6, _⟩ Parts.One (ι := List Race) (ρ := Nat) where
  run := some ∘ part1

instance : Part ⟨6, _⟩ Parts.Two (ι := List Race) (ρ := Nat) where
  run := some ∘ part2