If I need two lists to be the same size, which approach is more idiomatic?
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