## Stream: Coq users

### Topic: Idiomatic same-sized lists

#### Shea Levy (Oct 21 2020 at 19:14):

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

#### Paolo Giarrusso (Oct 21 2020 at 19:26):

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

#### Paolo Giarrusso (Oct 21 2020 at 19:27):

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.

#### Paolo Giarrusso (Oct 21 2020 at 19:31):

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.

#### Maxime Dénès (Oct 21 2020 at 20:46):

mathcomp's tuple work fine

#### Maxime Dénès (Oct 21 2020 at 20:47):

but it's none of the approaches you mentioned

#### Christian Doczkal (Oct 22 2020 at 09:09):

@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: Jun 24 2024 at 13:02 UTC