Advent of Code 2023

Stream: general

[Gareth Ma]

I wrote a program that should solve AoC2023 Day 1, but it is way too slow. Any suggestions on how to optimise part 2? I don't even know what's slow about this. It took 16 seconds to run on twovgtprdzcjjzkq3ffsbcblnpq and there are 1000 lines in the input file, and I would like to get it to under a minute :) Is it because I am using recursive definitions?

import Mathlib.Tactic

open String Tactic

def parseDigit (c : Char) : ℕ := if '0' ≤ c ∧ c ≤ '9' then c.val.toNat - 0x30 else 0

def parseNatAux : List Char → ℕ
| [] => 0
| x :: xs => (parseNatAux xs) * 10 + parseDigit x

def parseNat : String → ℕ := fun s ↦ parseNatAux (s.toList.reverse)

def getInput : IO (Array String) := do
  let dir := "<cwd>"
  return ←IO.FS.lines (dir ++ "/in")

def words : List String := [
  "zero", "one", "two", "three", "four", "five", "six", "seven", "eight", "nine",
  "0", "1", "2", "3", "4", "5", "6", "7", "8", "9"
]

def List.getSuffix : List α → List (List α)
| [] => [[]]
| x :: xs => (x :: xs) :: getSuffix xs

def String.getSuffix (s : String) : List String := (List.getSuffix s.toList).map List.asString

def List.enumerate (l : List α) : List (ℕ × α) := (List.range l.length).zip l

def List.IsPrefix' : List α → List α → Prop
| [], _ => True
| _, [] => False
| (x::xs), (y::ys) => (x = y) ∧ List.IsPrefix' xs ys

def String.IsPrefix' : String → String → Prop
  | ⟨d1⟩, ⟨d2⟩ => List.IsPrefix' d1 d2

instance [DecidableEq α] {s t : List α} : Decidable (List.IsPrefix' s t) := by
  induction' s with s s' hs generalizing t
  <;> induction' t with t t' _
  <;> try simp only [IsPrefix', List.IsPrefix']
  · exact decidableTrue
  · exact decidableTrue
  · exact decidableFalse
  · apply And.decidable (dq := ?_)
    exact hs

instance {s t : String} : Decidable (IsPrefix' s t) := by unfold IsPrefix' ; infer_instance

def part1 : IO ℤ := do
  let mut res := 0
  for line in ←getInput do
    let chars := line.toList.filter Char.isDigit
    let val := [chars.head!, chars.getLast!].asString
    res := res + parseNat val
  return res

def part2 : IO ℤ := do
  let mut res := 0
  let input ← getInput
  let words' := List.enumerate words
  for line in input.toList.take 1 do
    let lineSuffix' := List.enumerate (getSuffix line)
    let mut tmp : List (ℕ × ℕ) := []
    for (i, suf) in lineSuffix' do
      for (j, num) in words' do
        if num.IsPrefix' suf then
          tmp := (i, j % 10) :: tmp
    res := res + tmp.getLast!.snd * 10 + tmp.head!.snd
  return res

set_option profiler true
set_option trace.profiler true

/- #eval part1 -/
#eval part2
/- #print part2 -/

[Gareth Ma]

Also if any of these are in Lean / Mathlib already that will be nice. In particular, String.IsSuffix exists but they write it with an $\exists$ which isn't decidable.

[Mauricio Collares]

I wonder if we should have a separate stream for AoC, if only to avoid spoilers.

[Eric Wieser]

Compiling it to C will likely make it faster

[Gareth Ma]

I have waited 6 hours before posting, but if creating a new thread is possible that'll be great too :)

[Gareth Ma]

Eric Wieser said:

Compiling it to C will likely make it faster

How can I do that?

[Eric Wieser]

You should be able to add it as an exe in the lakefile

[Damiano Testa]

Gareth, I did not look carefully at your code, but

• docs#String.isPrefixOf exists and is likely more optimised than yours;
• I reversed the strings and used the same function twice (and reversed the English words, of course!) -- not sure about the net effect of reversal vs scanning from the back.

And this is the running time of my solution:

$ time lake env lean Advents/day01.lean

[Part 1 answer]
[Part 2 answer]

real    0m0,725s
user    0m0,635s
sys 0m0,090s

[Damiano Testa]

(My project only depend on Std, in case it matters.)

[Damiano Testa]

Mauricio Collares said:

I wonder if we should have a separate stream for AoC, if only to avoid spoilers.

I like the idea of a new thread: waiting some time may not be enough, due to timezones/other commitments that someone might have! :smile:

[Damiano Testa]

Header

Gareth, I think that your input data not will contain either "zero" or "0" as a substring, so you can ditch those.

I doubt that this will improve substantially the running time, though!

[Gareth Ma]

Thanks for the comments, I rewrote it based on your code and Arthur's (from another server) and got it down to 225ms :)

[Jujian Zhang]

there is also a simpler solution just by pattern matching

pattern-matching

def processStringLastHelper (s : String) : Nat :=
match s with
| ⟨[]⟩ => panic s!"wrong {s}"
| ⟨'0':: _⟩ => 0
| ⟨'1':: _⟩ => 1
| ⟨'2':: _⟩ => 2
| ⟨'3':: _⟩ => 3
| ⟨'4':: _⟩ => 4
| ⟨'5':: _⟩ => 5
| ⟨'6':: _⟩ => 6
| ⟨'7':: _⟩ => 7
| ⟨'8':: _⟩ => 8
| ⟨'9':: _⟩ => 9
| ⟨'o' :: 'r' :: 'e' :: 'z' :: _⟩ => 0
| ⟨'e' :: 'n' :: 'o' :: _⟩ => 1
| ⟨'o' :: 'w' :: 't' :: _⟩ => 2
| ⟨'e' :: 'e' :: 'r' :: 'h' :: 't' :: _⟩ => 3
| ⟨'r' :: 'u' :: 'o' :: 'f'  :: _⟩ => 4
| ⟨'e' :: 'v' :: 'i' :: 'f'  :: _⟩ => 5
| ⟨'x' :: 'i' :: 's' :: _⟩ => 6
| ⟨'n' :: 'e' :: 'v' :: 'e' :: 's' :: _⟩ => 7
| ⟨'t' :: 'h' :: 'g' :: 'i' :: 'e' :: _⟩ => 8
| ⟨'e' :: 'n' :: 'i' :: 'n' :: _⟩ => 9
| ⟨_::rest⟩ => processStringLastHelper <| .mk rest

def processStringLast := processStringLastHelper ∘ .reverse

[Shubham Kumar 🦀 (he/him)]

I had a question, while I was trying to run day1 I ran into a type inference problem
So my day1.lean file looks like this

def isDigit (ch : Char) : Bool := Char.isDigit ch

def CharToNat (ch : Char) : Nat :=
  Char.toNat ch - Char.toNat ' ' - 16

def filterNumbers (s : String) : List Nat :=
  String.toList s
  |> List.filter isDigit
  |> List.map CharToNat

but when I try to print the list (my Main.lean)

import Aoc2023

def numbers :=
  List.map filterNumbers ["1abc2", "pqr3stu8vwx", "a1b2c3d4e5f", "treb7uchet"]

def main : IO Unit :=
  let n := List.map List.head numbers
  IO.println s!"{n}"

The type infered for filterNumbers is String -> String instead of String -> List Nat

What am I doing wrong?

[Kyle Miller]

Where are you seeing String -> String?

I'm seeing that filterNumbers is String -> List Nat and numbers is List (List Nat)

[Kyle Miller]

Maybe you're looking for List.head! instead of List.head?

This fixes the type error: let n := List.map List.head! numbers

[Shubham Kumar 🦀 (he/him)]

so lake build gives the following error

❯ lake build
Building Main
error: > LEAN_PATH=./build/lib LD_LIBRARY_PATH=./build/lib /home/sk/.elan/toolchains/leanprover--lean4---nightly-2022-10-18/bin/lean ./././Main.lean -R ././. -o ./build/lib/Main.olean -i ./build/lib/Main.ilean -c ./build/ir/Main.c
error: stdout:
./././Main.lean:8:13: error: typeclass instance problem is stuck, it is often due to metavariables
  ToString (List ?m.64)
error: external command `/home/sk/.elan/toolchains/leanprover--lean4---nightly-2022-10-18/bin/lean` exited with code 1

but the lsp is showing the type signature in numbers as String -> String I cannot screenshot it because as soon as I try to screenshot it vanishes

[Shubham Kumar 🦀 (he/him)]

I'll try List.head!

[Shubham Kumar 🦀 (he/him)]

The lsp shows a problem even though the lake build commands compiles it without any issues
Screenshot-from-2023-12-05-11-28-24.png

[Kyle Miller]

I'm not sure how that can be -- have you pasted exactly the code you have?

[Shubham Kumar 🦀 (he/him)]

❯ lake build
Building Main
Compiling Main
Linking aoc_2023

aoc_2023_lean on  main [?] on ☁  (ap-southeast-2)
❯ ./build/bin/aoc_2023
[1, 3, 1, 7]

[Gareth Ma]

Have you tried restarting the lsp or just reopening the file

[Shubham Kumar 🦀 (he/him)]

I'm trying to keep it all in a structure
Screenshot-from-2023-12-05-11-30-08.png

[Shubham Kumar 🦀 (he/him)]

I'll try restarting the lsp

Gareth Ma said:

Have you tried restarting the lsp or just reopening the file

[Shubham Kumar 🦀 (he/him)]

Yeah restarting the lsp fixed it, sorry

[Kyle Miller]

A useful command is "restart file" too. It reloads all the dependencies of a file. Maybe you had an older version of filterNumbers still loaded in Main.lean?

[Kyle Miller]

(on Mac, the keybinding is Cmd-shift-x)

[Shubham Kumar 🦀 (he/him)]

Thanks!

[Shubham Kumar 🦀 (he/him)]

is there a way to convert List (IO Nat) -> IO Unit?
right now I have the following code

import Aoc2023

def getNumbers lst :=
  List.map filterNumbers lst
  |> List.filter (fun lst => not (List.isEmpty lst))
  |> List.map (fun lst => List.head! lst * 10 + List.getLast! lst)
  |> List.foldr (fun n acc => acc + n) 0

def fileToNumbers (path : String) : IO Nat := do
  let input <- IO.FS.readFile path
  pure (String.splitOn input "\n" |> getNumbers)

def paths := [
 "/home/sk/aoc_2023_lean/Aoc2023/input_day1_part1.txt"
]

def main : IO Unit := do
  let result := List.map fileToNumbers paths

and I want to print result

[Mario Carneiro]

maybe use List.mapM instead to get a List Nat and then print that instead?

[Shubham Kumar 🦀 (he/him)]

oh is there a List.mapM I didn't know, thanks @Mario Carneiro !

[Shubham Kumar 🦀 (he/him)]

Hi I was having some issues with pattern matching Substring but the my question is tangential to that error.
The following error message states

❯ lake build
Building Aoc2023.Day1
error: > LEAN_PATH=./build/lib LD_LIBRARY_PATH=./build/lib /home/sk/.elan/toolchains/leanprover--lean4---nightly-2022-10-18/bin/lean ./././Aoc2023/Day1.lean -R ././. -o ./build/lib/Aoc2023/Day1.olean -i ./build/lib/Aoc2023/Day1.ilean -c ./build/ir/Aoc2023/Day1.c
error: stdout:
./././Aoc2023/Day1.lean:42:2: error: failed to compile pattern matching, stuck at
  remaining variables: [x✝:(String)]
  alternatives:
    [] |- ["one"] => h_1 ()
    [] |- ["two"] => h_2 ()
    [] |- ["six"] => h_3 ()
  examples:_

I want to know what [] |- ["one"] => h_1() means

[Shubham Kumar 🦀 (he/him)]

and the other pattern matches that are also mentioned

[Notification Bot]

2 messages were moved here from #general > Advent of Code? by Shubham Kumar 🦀 (he/him).