Tactics for Array/List simplification in lean4

Question

Because there are both Arrays and Lists in Lean4, sometimes you end up with code that has a mixture of Lists and Arrays interspersed with basic operations and conversions between the two. For example, I needed to prove something like this as part of a larger theorem:

lemma foo (a b: Array _): { data := Array.data a ++ (Array.data b ++ [Array.data c]) : Array (List _)} = a ++ (b ++ [Array.data c])

How should I approach proving these sorts of lemmas? Are there tactics or library lemmas I should be aware of?

Answer 1

Many of the tools for working with programming-like objects (Arrays and such) can be found in either core Lean (Init which is imported automatically) or in the standard (programming) library Std. You can find a lot of useful lemmas in Std. For Arrays they are stored in Std.Data.Array.Lemmas.

Further, to prove that two structures are equal, it is enough to use the congr tactic. (Note from a theorem-proving perspective Arrays are just defined as structures wrapping a list data. Of course that is not actually the internal implementation.) So in the end you get a short proof of your lemma:

import Std.Data.Array.Init.Lemmas

theorem foo (a b: Array (List α)) (c : Array α) :
    { data := a.data ++ (b.data ++ [c.data]) : Array (List _)}
    = a ++ (b ++ [c.data]) := by
  congr -- useful for proving two structures are equal
        -- new goal: a.data ++ (b.data ++ [c.data]) = (a ++ (b ++ [c.data])).data
  simp  -- uses simp lemmas from Std.Data.Array.Init.Lemmas

Note, simp looks up "simp lemmas" from other parts of the code, so you have to import Std.Data.Array.Lemmas to access the simp lemmas for Array.

Lean 4 is still under development, and even moreso Std. So if you find lemmas for Array or List or other standard objects that would be useful to have, either ask about it on the Lean Zulip, approach one of the maintainers of https://github.com/leanprover/std4, make an issue on that repo, or make a PR to that repo with your new lemmas.

---

Update: As you noted in the comment, this two line proof may not always work, and I should be more clear that it likely won't work for many applications. Here are a few observations:

• Theorem proving is in general challenging. While Lean and other proof assistants strive to make powerful automation that make the job of the user easier, this itself is no easy task.
• If you plan to prove a lot about Array, you may find it useful to look through the proofs in Std.Data.Array.Lemmas in more detail to see how they are done.
• As for searching for theorems and lemmas, the three best approaches I know in Lean 4 are library_search (example below), the search feature in the docs, and asking around (on here or the Lean Zulip).
• I notice that the Array lemmas are often stated as <expression for an array>.data = ... and I think if you state your lemmas in that format then you would find that simp tactic works much of the time for simple equations. As for getting your lemma in that format, let me mention how I was able to solve your new example (found in the comments).

I want a way to turn x = {data := y} into x.data = y. I don't know the name of the theorem or even where to look, but I suspect there is a theorem similar to the following and I use the library_search tactic to find it.

import Std.Data.Array.Init.Lemmas
import Mathlib.Tactic.LibrarySearch

example (r: Array α): r.data = x -> r = { data := x } := by
  library_search  -- exact fun a ↦ Array.ext' a

While that exact fact wasn't in the library, library_search gives me a proof of my fact, and I see that Array.ext' is what I basically need. So then I apply Array.ext' and it is now in the form I can use simp:

import Std.Data.Array.Init.Lemmas

theorem bar (r: Array α) (b: List α): r ++ b = { data := r.data ++ b } := by
  apply Array.ext'
  simp