Advent of Code?

Stream: general

[Omri Schwarz]

Is anyone trying to do Advent of Code in Lean this year?

[Damiano Testa]

I am.
(Not polished yet, but it should work!)

I plan to polish at least the first day or two, since I am planning to "Christmas" lecture on Lean as a programming language for my students.

[Gareth Ma]

Hi, I missed this thread. I’m also doing it in Lean (as well as a billion other languages, probably)

[Gareth Ma]

My terrible first attempt is at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Advent.20of.20Code.202023 but it takes couple hours, I think

[Omri Schwarz]

First night of the advent and I missed how a misclick gave me the 1st day puzzle from 2015. ..

[Gareth Ma]

Also, the author has asked people not to publish their input data publicly: https://twitter.com/ericwastl/status/1465805354214830081

[Omri Schwarz]

And I am stuck because of what happens when digit words overlap, I think.

[Gareth Ma]

Yeah, a lot of people did

[Arthur Adjedj]

I will also be trying to do the Advent of Code here

[Kyle Miller]

I'm not sure how long I'll keep it up, but I have my solutions here

[Wojciech Nawrocki]

There is also an Advent of Proof!

[Adam Topaz]

Wojciech Nawrocki said:

There is also an Advent of Proof!

Is this supposed to just be a discord invite?

[Wojciech Nawrocki]

Adam Topaz said:

Wojciech Nawrocki said:

There is also an Advent of Proof!

Is this supposed to just be a discord invite?

There is a webpage, but it appears to ask for access to a Discord account to use as your submission account.

[Gareth Ma]

How hard is it? I will try tonight but I feel kind of nervous (???)

[Gareth Ma]

Okay it's not hard at all, at least D1

[Frédéric Dupuis]

I'm also doing it, at least for the first few days. Repository here.

[Scott Morrison]

Is anyone considering writing formal specs and proofs? :-)

I did day 1, and will probably do as many (in lean) as my kid does (in python). I didn't attempt to verify it, but looking at the code here are some basic facts that I would have wanted:

proof_wanted String.intercalate_splitOn {sep s : String} :
    sep.intercalate (s.splitOn sep) = s

proof_wanted List.insertionSort_sorted {l : List α} [DecidableRel r] :
    (l.insertionSort r).Sorted r

proof_wanted String.mem_findAllSubstr_iff {s : String} {p} :
    t ∈ s.findAllSubstr p ↔ t.str = s ∧ t.toString = p

/-- `String.findAllSubstr` returns results in order. -/
proof_wanted String.findAllSubstr_sorted {s : String} {p} :
    (s.findAllSubstr p).map (Substring.startPos) |>.toList |>.Sorted (· < ·)

We really need to add the String instances for slim_check so we can sanity check statement like these; I bet at least one is wrong! :-)

[Arthur Adjedj]

The AOC might be a great opportunity to find missing functions/theorems currently missing in Lean. I found myself being limited in my options when writing my code. For example, manipulating Substring isn't so easy, since the functions aren't documented. Furthermore, I don't feel like the str[a:b] notation should give an Array as it does now, I feel like it would make sense for it to return a Substring, in the same way that arr[a:b] returns a Subarray for a given Array.

[Frédéric Dupuis]

Here's a problem that came up for me: how do we prove termination of a monadic parser, such as

partial def getFirstNum : Parsec Nat :=
  parseNumberForwards <|> (do let _ ← anyChar; getFirstNum)

where getFirstNum is another parser that tries to get a digit at the current position either as an actual digit or spelled out as a word. Here termination should be guaranteed by the fact that the string being parsed gets strictly shorter with every recursive call, but this is all hidden under monadic code.

[Mario Carneiro]

You can't, at least not written that way. One way you could do it is to have a Parsec.fix : (Parsec A -> Parsec A) -> Parsec A parser, which calls the passed function with a parser that acts like the one under construction except it fails if called from the same or lower string position

[Mario Carneiro]

Arthur Adjedj said:

The AOC might be a great opportunity to find missing functions/theorems currently missing in Lean.

I think this every year. Maybe what we should do is have a wiki page so that people can jot down their pain points or missing theorems as they come up. Or just post here on zulip

[Frédéric Dupuis]

Yeah, also I guess there's always the "fuel" trick:

def getFirstNum (fuel : Nat) : Parsec Nat :=
  parseNumberForwards <|> do
    if fuel = 0 then fail "end of string"
    else
      let _ ← anyChar
      getFirstNum (fuel-1)

[Mario Carneiro]

It's important to catch people in the moment though, because even a few hours later going back over the code you may already have forgotten what lemma you were missing and worked around

[Mario Carneiro]

@Frédéric Dupuis the downside of that version is that every recursive parser needs an if statement

[Mario Carneiro]

and you have to set the fuel correctly and prove that it is large enough etc

[Frédéric Dupuis]

Yeah, in this case it's not a big problem but it's definitely a downside.

[Frédéric Dupuis]

As for missing lemmas, would you welcome PRs to Std for functions like String.reverse or is this just going to get annoying?

[Mario Carneiro]

Yes certainly we want such theorems

[Mario Carneiro]

I think it's probably better to get the proof_wanted version of the theorems first though, the proofs can come later

[Frédéric Dupuis]

Right. (Though in this case it's just the function that reverses a string.)

[Mario Carneiro]

oh you mean the function itself, not the lemmas

[Scott Morrison]

We'd prefer lemmas over functions for now. :-)

[Frédéric Dupuis]

Alright, makes sense!

[Mario Carneiro]

rust std doesn't have a String::reverse so I'm a bit meh

[Scott Morrison]

I think PRs with new functions for Std are okay, but perhaps they could come with a fair bit of effort to include all the lemmas, at least as proof_wanted.

[Scott Morrison]

We would really like to get to the point where we know what is missing in terms of adding API, i.e. where we can post a graph of the number of proof_wanted statements and feel like getting it to zero will be a meaningful milestone.

[Mario Carneiro]

In fact I think we should push people to use proof_wanted more aggressively in those PRs, that way they can be focused on the API design rather than adding a bunch of work which may need to be discarded in response to definition changes

[Frédéric Dupuis]

So I guess this is what you had in mind, Mario?

def Parsec.fix (p : Parsec α → Parsec α) : Parsec α := fun it =>
  let p' : Parsec α := fun it' =>
    if h : it.s.endPos - it.i ≤ it'.s.endPos - it'.i then
      .error it' "recursive call going backwards in the string"
    else
      have : it'.s.endPos - it'.i < it.s.endPos - it.i := by
        have h'' : ¬(it.s.endPos - it.i).byteIdx ≤ (it'.s.endPos - it'.i).byteIdx := h
        rwa [Nat.not_le] at h''
      fix p it'
  p p' it
termination_by fix p it => it

def getFirstNum : Parsec Nat := fix fun p =>
  parseNumberForwards <|> do let _ ← anyChar; p

[Frédéric Dupuis]

Very nice, I expected this to be more painful.

[Mario Carneiro]

or more simply

def Parsec.fix (p : Parsec α → Parsec α) : Parsec α := fun it =>
  let p' : Parsec α := fun it' =>
    if it'.s.endPos - it'.i < it.s.endPos - it.i then
      fix p it'
    else
      .error it' "recursive call going backwards in the string"
  p p' it

[Adomas Baliuka]

What is parseNumberForwards? Loogle gives no hits.
(by the way, my AoC is here but I probably won't be using Parsec because I couldn't find a tutorial yet and it feels I'm doing it very wrong).

[Adomas Baliuka]

(deleted)

[Frédéric Dupuis]

@Adomas Baliuka You can find my full solutions here. This code is in Aoc2023/Day01.lean, and the functions I use there that are not in core or Std are in Aoc2023/Utils.lean.

[Antanas Kalkauskas]

I am also participating, here are my solutions. Hoping to go through the whole event.

[Antanas Kalkauskas]

Is anyone hosting a private Advent of Code leaderboard for lean4 solutions?

[Yakov Pechersky]

Mario Carneiro said:

or more simply

def Parsec.fix (p : Parsec α → Parsec α) : Parsec α := fun it =>
  let p' : Parsec α := fun it' =>
    if it'.s.endPos - it'.i < it.s.endPos - it.i then
      fix p it'
    else
      .error it' "recursive call going backwards in the string"
  p p' it

Can we reuse the parser propositions I developed for the lean3 parser here?

[Mario Carneiro]

quite possibly. I think they all have to be rewritten since the underlying types and operations have changed but the ideas should still work

[Yakov Pechersky]

Agree on the rewrite. There might be a need for special support in the termination checker for parsecs to look for a docs3#parser.prog

[Liam O'Connor]

Wojciech Nawrocki said:

There is also an Advent of Proof!

this is meant as a competition for beginners/intermediate lean users associated with the university of edinburgh's TypeSig and related student societies, not really for general admission. If this works well perhaps we will expand the scope next year.

[Phil Nguyen]

I am also using AoC to learn more about practical programming in Lean. Here are my solutions

For input processing, I'm either doing naive parsing using String.splitOn, or emacs's macros to massage the input. Are there tutorials/examples out there for using Lean's parser library? Thanks!

[Frédéric Dupuis]

I don't think there are any tutorials, but if you want a more extended example, I wrote a bibtex parser here. It's probably not great code though, this was my first attempt at using monadic parsers.

[Adomas Baliuka]

Can we make a "blessed" solution of AoC that shows best practices (while remaining concise so people can easily read all of it)? Which of the solutions referenced here so far (certainly not mine) might be candidates?

[21eleven]

Just joined this Zulip. I am using Advent of Code to learn Lean . Found this thread while searching for documentation on parsers :p

[Mario Carneiro]

@Adomas Baliuka Of the examples linked so far, I think Kyle's solutions are the most best-practice looking. It's a lot more work to write this kind of teaching material every day compared to just solving the problem though

[Adomas Baliuka]

I wonder, why are some definitions marked partial there? I removed it at two random examples and it seemed the keyword was not necessary. Why does one mark definitions partial when it's not needed to make Lean accept them?

[Mario Carneiro]

probably just copy pasta

[Mario Carneiro]

It's possibly a bit faster to compile if you don't have to do the termination proof? But for most functions this is barely noticeable

[Kyle Miller]

If you're talking about the partials in day 1 part 2, I just forgot to remove them. I started by writing a state machine to process characters one at a time, but then I realized there was docs#String.findAllSubstr (which uses a KMP matcher by the way) and went with that.

[Kyle Miller]

@Phil Nguyen I've been using Lean's Parsec library here and there. It's a bit anemic as a parser library, but it has just enough to be able to write what you need. Here is a parser for today's format. I put the ws whitespace parser probably in more places than I needed, which is harmless, but one gotcha is that because Parsec commits to a parse, I needed to write many (nat <* ws) instead of many (ws *> nat), since in the latter matching whitespace causes it to think there ought to be another nat.

I had to define the nat parser myself, and it's here.

[Kyle Miller]

I should have written a general sepBy parser, but instead in day 2 I wrote specialized versions. I'll probably factor it out when it's needed in a future day.

[Adam Layne]

My solutions are here. First time using Lean. Using it as an opportunity to get better at monads/applicatives.

[Adam Layne]

AoC23 seems pretty heavy on text parsing, so I should probably learn the parser library as well.

[tristanC]

Also using AoC to learn some Lean (coming from Haskell/Rust). I got to use Parsec for day 2. My solutions are here if that helps. It's a lot of fun, cheers :)

[James Dabbs]

Hey y'all :wave: Late to the party here, but I'm getting started as well. Similarly, just wrapped up my first non-trivial bit of parsing for day 2.

[Notification Bot]

Stuart Presnell has marked this topic as resolved.

[Notification Bot]

Stuart Presnell has marked this topic as unresolved.

[Stuart Presnell]

Sorry, misclicked the "mark as resolved" button

[Phil Nguyen]

Kind of silly, but is there a standard library function for sorting a list? I couldn't find it for day 7 so ended up implementing a basic one today. I tried autocompletion in emacs, and searching for {a : Type} -> [Ord a] -> List a -> List a on Loogle but couldn't find anything :upside_down:

[Henrik Böving]

I can offer you docs#Array.qsort but I think nobody bothered to implement list sorting yet

[tristanC]

For what it's worth, I propose this:

-- From https://codereview.stackexchange.com/questions/197868/bubble-sort-in-haskell
def swapTill [Min α] [Max α] (x : α) : List α -> List α
  | [] => [x]
  | y :: xs => min x y :: swapTill (max x y) xs
def List.bubbleSort [Min α] [Max α]: List α -> List α := List.foldr swapTill []

[Frédéric Dupuis]

docs#List.insertionSort

[Kalle Kytölä]

or docs#List.mergeSort.

[ohhaimark]

Doing AoC and find myself wanting to use Lean's builtin parser, perhaps naively. Is there an easy interface to it along the lines of parse : Parser -> String -> Option Syntax? I guess it is specialized to Lean enough to make this a chore and not a good idea.

[Kyle Miller]

You could use docs#Lean.Parser.runParserCategory for a parser category that you define, or here's some code for running a parser for a named syntax: https://github.com/nomeata/loogle/blob/master/Loogle.lean#L18

[Steve Dunham]

For sorting, I converted to an Array (.toArray.qsort). I suspect it's the fastest way, since it can mutate in place.

[tristanC]

Kyle Miller said:

You could use docs#Lean.Parser.runParserCategory for a parser category that you define

Thanks, that looks very useful. Though I can't find how to create the Lean.Environment, do we need to setup a CoreM for that? Is there an example that demonstrates using runParserCategory from the main IO Unit?

[Alok Singh (S1'17)]

would anyone like to pair on advent? i live in the bay area and i just started aoc. i'm on part 1b (writing a parser combinator to handle it, or figuring out Lean.Data.Parsec). i'm familiar with functional programming.

[Shubham Kumar 🦀 (he/him)]

Alok Singh (S1'17) said:

would anyone like to pair on advent? i live in the bay area and i just started aoc. i'm on part 1b (writing a parser combinator to handle it, or figuring out Lean.Data.Parsec). i'm familiar with functional programming.

https://github.com/leanprover-community/lean4-samples/blob/main/CSVParser/README.md

I was also thinking the same and I saw this one is archived but maybe can help in understanding Parsec.

[Shubham Kumar 🦀 (he/him)]

Steve Dunham said:

For sorting, I converted to an Array (.toArray.qsort). I suspect it's the fastest way, since it can mutate in place.

I did the same didn't know how to add Mathlib to the project, maybe need to have a look at FPIL

[Mac Malone]

ohhaimark said:

Doing AoC and find myself wanting to use Lean's builtin parser, perhaps naively. Is there an easy interface to it along the lines of parse : Parser -> String -> Option Syntax? I guess it is specialized to Lean enough to make this a chore and not a good idea.

tristanC said:

Kyle Miller said:

You could use docs#Lean.Parser.runParserCategory for a parser category that you define

Thanks, that looks very useful. Though I can't find how to create the Lean.Environment, do we need to setup a CoreM for that? Is there an example that demonstrates using runParserCategory from the main IO Unit?

The Partax library provides an interface for converting Lean syntax / parsers into simpler functions that can be easily run without a full Lean.Enviroment. (Sorry for the shameless self-plug!)

[Kyle Miller]

That also avoids what Loogle needs to do, which is to embed Lean (using supportInterpreter := true in the lakefile) and then set up CoreM by importing modules: https://github.com/nomeata/loogle/blob/master/Loogle.lean#L142

If you're not attached to doing runParserCategory from the command line, then you can use #eval, which can run CoreM using the current environment at that point.

[Kyle Miller]

Today's part 2 was mathematically interesting, though yesterday task was a classic.

It involves finding the area of the interior of a closed loop in the plane. The curve is made of segments between integer coordinates, and to figure out which cells are in the interior you can use Z/2Z intersection numbers between the curve and a ray that goes to infinity -- the count is 1 iff it's an interior cell.

My solution: https://github.com/kmill/kmill-aoc2023/blob/main/AoC2023/Day10/Part2.lean

I'm curious what other approaches anyone took with this part.

[Frédéric Dupuis]

I just went with the first thing that popped into my head, namely:

"Puffing" up the grid by adding a filler character so that a DFS search on the inside of the curve can get between the pipes. Also I didn't even bother figuring out where the inside was; I just started four searches at the NW, NE, SW and SE corners of the starting position. Definitely not a clean as your solution! :-)

[Kyle Miller]

@Frédéric Dupuis I like that idea to manipulate the data. It makes it conceptually clear what's being calculated. Mine takes an arbitrary choice (a direction) which is a bit inelegant.

[Frédéric Dupuis]

I also spent an embarrassing amount of time playing with this sort of pattern for verification, which looked quite promising:

structure PropWrapper (p : Prop) where
  pf : p

def checkThat {α : Type _} (x : α) (p : α → Prop) [∀ a, Decidable (p a)] :
    Option (PropWrapper (p x)) :=
  if h : p x then some ⟨h⟩
  else none

def Array.checkThatAll {α : Type _} (xs : Array α) (p : α → Prop) [∀ a, Decidable (p a)] :
    Option (PropWrapper (∀ i, (h : i < xs.size) → p xs[i])) :=
  match h : xs.all p with
  | false => none
  | true =>
      have hmain : ∀ (i : Fin xs.size), p xs[i] := by
        have htmp := (xs.all_eq_true _).mp h
        simpa [decide_eq_true_iff] using htmp
      some ⟨fun i hi => hmain ⟨i, hi⟩⟩

def toyExample (input : FilePath) : IO Unit := do
  let data := (← IO.FS.lines input).map String.toCharArray
  let some ⟨hdata⟩ := checkThat data fun as => 0 < as.size | panic! "no input"
  -- here I have `hdata : 0 < as.size` in context
  let firstrow := data[0]   -- which lets me access the first element without using `data[0]!`
  let some ⟨hdata'⟩ :=
    data.checkThatAll fun as => as.size = data[0].size | panic! "Rows not all the same size!"
  -- here I have `hdata' : ∀ i < data.size, data[i].size = data[0].size` in context

[Frédéric Dupuis]

It seems like a clean way to get proofs of facts we want asserted, and that we can then use later in the code to e.g. check array bounds.

[Kyle Miller]

docs#PLift is the core Lean structure for PropWrapper btw. That pattern seems to be similar to this one, which came up when someone was asking about this recently.

[Frédéric Dupuis]

Thanks! I figured something like this had to exist...

[Damiano Testa]

spoiler

I simply assigned a "counterclockwise rotation of the next step along the path", then moved along each row until I hit the path and depending on where the outward normal was pointing, I decided if it was inside or not.

My very messy code is https://github.com/adomani/advents/blob/master/Advents/day10.lean

[ohhaimark]

Getting a stack overflow but no stack trace. I'm running a built executable through lake exe, so I'm not sure if running it interpreted would get a stack trace. Is there a debug flag I can set for executable targets or an easy way to run a lake exe on the interpreter with stack traces?

Getting used to strict evaluation and having foldr be a no no.
EDIT: tried buildType := BuildType.debug, still no stack trace

[Henrik Böving]

@ohhaimark does your binary coredump? If so you can easily get a stacktrace from that using any reasonably good C debugger.

[ohhaimark]

Henrik Böving said:

ohhaimark does your binary coredump? If so you can easily get a stacktrace from that using any reasonably good C debugger.

Ah, running it through lean exe didn't print that it core dumped, but running the binary directly did.

Now to remember the systemd incantation to find it.

[Henrik Böving]

coredumpctl debug if you have a somewhat recent distro @ohhaimark

[ohhaimark]

Ah, it seems the foldl in the parser library I'm using (https://github.com/fgdorais/lean4-parser) isn't tail recursive.

[Kyle Miller]

@Damiano Testa

Nice, so it seems like you did something like the winding number algorithm and I did something like the even-odd algorithm: https://en.wikipedia.org/wiki/Point_in_polygon

[ohhaimark]

@[specialize f]
private partial def foldAux (f : γ → β → γ) (y : γ) (p : ParserT ε σ α m β) : ParserT ε σ α m γ :=
  let rec rest (y : γ) : ParserT ε σ α m γ :=
    try
      let x ← withBacktracking p
      rest (f y x)
    catch _ => return y
  rest y

Or maybe it's specialized to my f that is screwing things, but that doesn't explain the repeated foldAux in the backtrace.

[ohhaimark]

I guess the try-catch could muddy the waters, haven't thought too deeply about how that translates. Or just the parser monad in general. I use the SimpleParserT with StateT ... ExceptT ... Id, so maybe in SimpleParser it is tail recursive.

[ohhaimark]

Using parser combinators at the stage I'm on (Day 3) is overkill anyway, but now I stubbornly want to get this to work. This is why I never get anything done.

[Damiano Testa]

@Kyle Miller

spoiler

Indeed! I hadn't seen the wikipedia page that you linked, my first thought was counting parity of intersections, but got stuck trying to convince myself how to deal efficiently with a ray sharing several steps with the path (i.e. non-transverse intersections). I convinced myself more quickly that the first hitting points was enough and I coded that. I was definitely thinking of winding numbers!

[Kyle Miller]

@Damiano Testa

I was used to dealing with transversality problems because of some algorithms in low-dimensional topology, so I jumped at that. The trick here is that the loop has tangent vectors that lie only in cardinal directions, so you can displace the loop by an epsilon amount in a non-cardinal direction. There's some ascii art in my solution as I worked out the combinatorics from there.

[Damiano Testa]

@Kyle Miller

spoiler

Ah, good point! I eventually convinced that it worked as well, by carrying around the two vectors until the first time that the path changes direction. But that is mostly because I was walking around the path in the first place!

[Mario Carneiro]

@ohhaimark Your foldAux is not tail-recursive, it calls rest inside a tryCatch which means it builds up a stack of tryCatches

[ohhaimark]

Mario Carneiro said:

ohhaimark Your foldAux is not tail-recursive, it calls rest inside a tryCatch which means it builds up a stack of tryCatches

It's the library's. I've filed an issue https://github.com/fgdorais/lean4-parser/issues/5.

From the issue:
In the process of trying to come up with a minimal example for, I caused an internal panic instead :sob:.

import Parser
import Parser.Char

open Parser Parser.Char Std

abbrev P := SimpleParser Substring Char

def test : IO Unit := do
  let x := Parser.run (Parser.foldl (fun _ _ => ()) (pure ()) (pure ()) : P Unit) ""
  match x with
  | .ok _ res => pure res
  | .error err => IO.println err
def main : IO Unit := test

stdout/stderr

INTERNAL PANIC: unreachable code has been reached

Where do I report upstream?

[Mario Carneiro]

looks like it's already fixed upstream

[Mario Carneiro]

Actually can you make a lean4-parser-free MWE for the INTERNAL PANIC issue?

[ohhaimark]

Mario Carneiro said:

looks like it's already fixed upstream

I tried, but I don't know enough about the cause to understand how to repro without it.

[Mario Carneiro]

I mean can you just inline what you need and remove things as long as the problem persists

[Mario Carneiro]

You presumably only need the Parser type, Parser.run and Parser.foldl to make this (mis)compile

[Mario Carneiro]

you should pull up the Output panel so that you can see when the panic occurs, since only the first panic in a session gets a popup

[Alok Singh (S1'17)]

I'm livestreaming day 2 at https://www.youtube.com/watch?v=IgeXFbOG_Nc

[Steve Dunham]

For day 10 part 2,

I vaguely remembered the even-odd thing and came up with scanning each row toggling inside/outside for vertical lines (and using the flag for above/below on a horizontal line segment).

https://github.com/dunhamsteve/aoc2023/blob/main/day10/day10.lean

[Steve Dunham]

To show totality in day12, I needed to tell lean that List.drop returned something the same or smaller than its argument. I ended up coming up with this, but I'm somewhat new to proofs in Lean 4. Is there a better way to do this:

theorem drop_le (r : Nat) (cs : List Char) :  sizeOf (cs.drop r) <= sizeOf cs := by
  revert cs
  induction r
  intro cs
  apply Nat.le_of_eq; rfl
  intro cs
  cases cs
  apply Nat.le_of_eq; rfl
  rename_i n ih head tail
  apply Nat.le_trans (ih tail)
  simp [Nat.le_add_left]

Full code, but spoilers, at https://github.com/dunhamsteve/aoc2023/blob/main/day12/day12.lean

[Steve Dunham]

Working from phone:
IMG_4478.PNG

[Phil Nguyen]

Is there a library function for parsing a hex string to a Nat? Thanks! (I figure it's straightforward but just wonder if the library already has it)

[Phil Nguyen]

Day 19 was pretty fun. What I did was writing a monadic interpreter for the language, then by swapping out the monad, we obtain the standard semantics for q1, and symbolic execution for q2. I found out Lean doesn't really have something like ListT in Haskell (probably because it's not practical in an eager language?). Also I think I need to learn more about Parsec to write less verbose parsers...