5
$\begingroup$

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?

$\endgroup$

1 Answer 1

4
$\begingroup$

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
$\endgroup$
4
  • $\begingroup$ Thanks, this solves my example, but it seems to struggle with a simpler lemma of this sort: lemma bar (r: Array α) (b: List α): r ++ b = { data := r.data ++ b } Even when importing Std.Data.List.Init.Lemmas as well. Is this the result of a missing lemma, or are there more tricks needed for these sorts of proofs? $\endgroup$ Dec 12, 2022 at 17:58
  • $\begingroup$ I was able to solve it using rw [← Array.appendList_data], but is there an easier way that doesn't require me manually searching for lemmas? $\endgroup$ Dec 12, 2022 at 18:19
  • $\begingroup$ @JeremySalwen See my edits. $\endgroup$
    – Jason Rute
    Dec 12, 2022 at 22:07
  • $\begingroup$ @JeremySalwen Also the congr proof seems to work with the symmetric goal, { data := r.data ++ b } = r ++ b. That is a bit annoying, but good to know. $\endgroup$
    – Jason Rute
    Dec 12, 2022 at 22:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.