Stream: Coq users

Topic: Working with permutations in math-comp


view this post on Zulip Joonatan Saarhelo (Sep 09 2021 at 15:12):

To complete a proof I need to show that perm_eq s s' -> perm_eq (zip ?cs' s') (zip cs s) but I have no idea how to go about it, as perm_eq doesn't tell me how to turn s into s', just that there is a way to permute it.

I am using perm_eq and tuples to model fixed-size multisets, which is maybe not the best way. Ideally I'd like to say that a \in b if there is a perfect matching such that for each pair (a0, b0) a0 \in b0. The only easy way I could think of was to say that there is a permutation a' that satisfies the condition when zipped with b.

view this post on Zulip YAMAMOTO Mitsuharu (Sep 09 2021 at 23:47):

Probably some lemmas (such as tuple_permP below) in perm.v would be useful.

Lemma tuple_permP {T : eqType} {n} {s : seq T} {t : n.-tuple T} :
  reflect (exists p : 'S_n, s = [tuple tnth t (p i) | i < n]) (perm_eq s t).

view this post on Zulip Joonatan Saarhelo (Sep 10 2021 at 11:31):

@YAMAMOTO Mitsuharu Thanks, that helps a lot. I was looking for things like 'S_n but only looked in seq.v

view this post on Zulip Joonatan Saarhelo (Sep 10 2021 at 12:53):

I found all2, which makes things a bit nicer. I think it is a bit weird that there is that but no map2/zipWith.


Last updated: Feb 01 2023 at 13:03 UTC