Is Array faster than List in proofs?

Stream: lean4

[Bolton Bailey]

My proof is taking a long time, and one suspicion I have is that I am trying to simplify expressions built out of several applications of List.modifyNth to various lists. I am considering replacing List with Array where relevant in my code. But the docs#Array says "From the point of view of proofs Array α is just a wrapper around List α." Is this statement meant to convey that the speed of proofs using List is the same as analogous proofs using Array operations, or could Array be faster?

[James Gallicchio]

This might be a complicated question to answer. It sounds like you have some expressions you want to prove something about and those expressions currently involve lists and you are asking if you make them arrays whether the proofs will elaborate/typecheck faster.

List and array have essentially the same expression representation during elaboration. So, any tactics you use to manipulate expressions about list/array will probably behave about the same.

For elaboration, a rough metric of how fast things will be is how large your expressions are. Large expressions will make most tactic calls slow because they have to traverse large expressions. If you have a big, static list expression [a, …, z], then elaboration will probably be kinda slow. And changing to #[] doesn’t really change the expression size so it’ll still be slow.

I think set_option trace.profiler is quite helpful for figuring out why elaboration is taking a lot of time.

[James Gallicchio]

(Notably, if you are using lists in some metaprograms then you may notice speed up by using arrays, because I think arrays might evaluate differently in the VM, and they definitely evaluate differently in compiled code)