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
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 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
[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 thesimp
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