Stream: Coq users

Topic: Idiomatic same-sized lists


view this post on Zulip Shea Levy (Oct 21 2020 at 19:14):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Maxime Dénès (Oct 21 2020 at 20:46):

mathcomp's tuple work fine

view this post on Zulip Maxime Dénès (Oct 21 2020 at 20:47):

but it's none of the approaches you mentioned

view this post on Zulip 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: Jan 31 2023 at 13:02 UTC