Many of the tools for working with programming-like objects (Array
s 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 Array
s 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 Array
s 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.