Takeaways from proving Advent of Code solutions

Stream: lean4

[Jeremy Salwen]

A month ago, I started working on a project to write provably correct solutions to the 2022 Advent of Code. At this point I had no experience with any theorem prover besides working through the first two volumes of Software Foundations in Coq a few years ago. Today I just finished proving the correctness of my solution to the first part of the first problem of Advent of Code. I have been taking notes about what I found difficult or confusing, as well as missing pieces of Std or Mathlib that I needed to implement myself. Some of these things may be rehashing questions that I asked on the Zulip chat (THANK YOU everyone who answered all my questions!), but I'm listing everything here for completeness.

1. The library docs were incredibly useful, but I only found the link by asking on Zulip. Google "lean4 docs" brings me to this page which doesn't link the library docs.
2. There are two searches on the library docs, the autocomplete search, and the google site search. I rarely found the google site search helpful, but I often wished that I could see the complete list of autocomplete possibilities. It also would be nice to be able to search for theorems vs defs, since a huge number of matching theorems can make it hard to search for a function.
3. #find and library_search are also essential for newbies, but aren't mentioned in the theorem proving tutorial
4. I ended up relying on #find mostly, because library_searchpopulates the results with spam that can drown out legitimate results. (see this discussion).
5. library_search also often fails because of the heartbeat limit, but setting the heartbeat limit option mentioned in the error message does not seem to have any effect.
6. List and Array conversions were sometimes tricky for me, because I often ended up with expressions mixing Array and List operations. I found that using simp [Array.ext_iff]as suggested by Eric was the best technique, but was still not perfect. Further discussion of the general problem of translating between isomorphic theories is discussed here
7. I loved using simp, but then it would slow down my proofs. The best way I found to combat this was to use simp? and replace simp with simp only. However, the list of lemmas is generally pretty large, creating clutter in my proofs. It also is pretty tedious. I wonder if it would be possible to automate this?
8. I spent a lot of time manually doing Nat arithmetic, because it felt like the automated tactics didn't really help. For example, s + (d+ t) - (d- 1) - (s + d) = t - (d- 1) Is true over the Nats, but no combination of arithmetic automation solves it (ring, ring_nf, zify, linarith). I wish there were a tactic that solved equations over Z and generated goals for the inequalities that were necessary to make the equality hold over Nat. (earlier discussion here)
9. This is likely more an issue with the VSCode extension (maybe not), but when you start a new tactic block, e.g. after by, case _ =>, etc, the Lean Infoview will not update with the new tactics state until after you have put the first tactic in the block. So I'm basically forced to put in a dummy tactic at the start of every block that I delete later, so that I can see the goal state.
10. When rewriting under binders or with dependent types, rw will fail, but simp only will succeed. However, rw gives a nice error message when it fails to rewrite, but simp doesn't. The error messages are very helpful for newbies like me. rw also only rewrites a single expression, but simp will rewrite multiple expressions, even with singlePass := true, which makes it less convenient to work with. (discussed here)
11. if and match in conv mode were important for me, but I had to copy and paste the code from this discussion to get them to work.
12. partial functions blocked me from proving anything about my program, so I had to avoid the partial library functions that I would otherwise want to use. Because of this, I avoided using String altogether and did everything as a List Char. For Nat and Int, I was forced to implement a non-partial version of the following functions: Int.repr, String.toInt, along with appropriate lemmas.
13. There were also a few functions that I felt were "missing" from the library, which I implemented myself: Nat.digit List.lastN List.splitOnList Array.modifyHead Array.modifyLast List.isInfixOf, along with appropriate lemmas.
14. I had to prove many lemmas about my new functions, but also a large number of lemmas about the existing functions. They generally fell into the following categories:

• Lemmas about Nat.toDigits, and round tripping of Int->List Char->Int
• Lemmas about List isInfix``isPrefix and isSuffix, including their relations to each-other, simp lemmas, decidability, and case splitting lemmas.
• Lemmas about the relationship of isInfix and mem to string manipulation functions like intercalate, intersperse, join,count, etc.
• Lemmas about second tier list manipulation functions, like modifyNth, modifyLast, dropLast, getLast?, get?, getD, and getRest.
• Commutators of List modifyNth, set, and get
• Basic lemmas about splitOnP and splitOn
• Basic WithTop lemmas
• This lemma: lemma Nat.sub_sub_eq_add_sub_of_le {a b c:ℕ} (h:c≤ b): a - (b-c) = a + c - b which I still believe is hiding somewhere in the library I just haven't found it. :sweat_smile:

You can see the full implementation here: https://github.com/jeremysalwen/advent_of_lean_2022/blob/master/one.lean
I would like to contribute back as much as possible! Are there any areas where my contributions would be valuable?

[James Gallicchio]

I'm pretty sure Std would happily add the List and Array lemmas you described. Super cool work!

[Yaël Dillies]

Here are some partial answers:

1. Unfortunately it's not clear to people at first that Lean and mathlib are separate things. We sure could ask the Lean devs to link back to Zulip, but they really are different projects
2. Separating defs and lemmas seems very useful, yes!
3. Dummy line
4. Dummy line
5. Dummy line
6. Dummy line
7. The automation on finding the list generated by simp? is... simp. If it significantly slowed down your proof, it's probably that you were either calling it on not such a simpable goal, or it tried to use bad simp lemmas that you added.
8. This problem should be solved once someone has reimplemented omega, but in the meantime zify i indeed what you want to use and maintain.
9. Dummy line
10. Do you know about simp_rw? It's a call to simp configured to feel like rw.
11. Dummy line
12. Dummy line
13. Is your Nat.digit docs#nat.digits? It hasn't been ported yet.

14. More specific feedback:

    • Lemmas about IsInfix/IsPrefix/IsSuffix are in file4#Mathlib/Data/List/Infix. They might not have been ported when you looked for them.
    • What basic WithTop lemmas?
    • Weirdly enough, we seem not to have your Nat.sub_sub_eq_add_sub_of_le. It should be called tsub_tsub_eq_add_tsub, and the closest I could find is docs#tsub_tsub_le_tsub_add

[Yaël Dillies]

Ugh, it renumbered everything :upside_down:

[Damiano Testa]

Regarding your item 9, I usually put a _ to see what the tactic state really is.

[Jeremy Salwen]

1 I don't see any place besides https://leanprover-community.github.io/mathlib4_docs/ where Std is documented. The lean documentation page links the Zulip chat, but doesn't link the mathlib4_docs page, which I think it should, regardless of the organizational separateness of lean and mathlib.
....
7 I didn't mean automating the simplification, but automating the textual replacement. I was thinking of llike a vscode shortcut that would replace simp with the simp only form. I will experiment more to see what is actually causing the slowdown, because I was seeing simps of over a second, and I don't think I was doing anything pathological.
...
10 I have tried simp_rw, but it behaves too much like simp in the ways I didn't like (repeated rewriting, no error messages).
...
13 I think nat.digits is already ported to Nat.toDigits. My Nat.digit is just def Nat.digit (base:ℕ) (n:ℕ) (index:ℕ): ℕ := (n / base^index) % base
...
14 Ahh, I may have also missed some lemmas due to the two names used for the same relation (isInfix and infix). Is there a reason why it's this way?

The WithTop lemmas were lemma WithTop.untop'_min_left [LinearOrder α] (x: α) (y: WithTop α): untop' d (min ↑x y) = min x (untop' x y) and the symmetric one.

More generally, how should I go about contributing to Mathlib4/Std4? What's the next step, just opening a PR with all the lemmas I think would be useful?

[Kevin Buzzard]

Right now mathlib4 isn't seeking new contributions (unless you want to also backport them to mathlib3) -- we're trying to keep mathlib3 and mathlib4 completely in sync during the porting process.

[Jireh Loreaux]

I think Std4 is available for contributing though, right?

[Dan Velleman]

Another solution for item 9 is to put done after by, and then write your proof between by and done. There will be a red squiggle under done until the proof is complete, at which point the red squiggle will disappear.

[Sebastian Ullrich]

Please provide an example for 9), there have been various bug fixes regarding that

[Jeremy Salwen]

Sebastian Ullrich said:

Please provide an example for 9), there have been various bug fixes regarding that

I could have sworn that like yesterday this was happening to me every time, but now I can't even get it to happen once. Was there a recent bugfix?

[Sebastian Ullrich]

Not in the last month or so