If I need two lists to be the same size, which approach is more idiomatic?

- Take a proof of equal lengths
- Have the second list be a function from Fin len(l1)
- Take a list of pairs
- Use vectors

It depends and people don't agree. Fin (length l1) sounds tricky to deal with, and proving two functions equal requires extra axioms or setoids

For vectors, the stdlib theory isn't all that complete, plus you're dealing with the extra trickiness of dependent pattern matching; most Coq users advocate for using them as little as possible.

1 seems more general; lists of pairs seems clever if it works well for you. I'd maybe make sure to have lemmas available converting between the two, I wouldn't be surprised if those lemmas existed in std++ and/or were easy to prove.

mathcomp's tuple work fine

but it's none of the approaches you mentioned

@Shea Levy I think it depends a lot on what you want to do. It you need to manipulate collections of more than two lists that have the same (known) length, I would suggest to use tuples/vectors. An example would be a "tape" where every "character" is a bitvector or length k.

If you want to prove a lemma involving two lists by induction, I strongly recommend using `size s1 = size s2`

as an additional assumption. Mathcomp even has an induction principle for simultaneous induction on same-length lists. So it really depends :shrug:

Last updated: Jan 31 2023 at 13:02 UTC