Joonatan Saarhelo (Sep 09 2021 at 15:12): 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.
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).
@YAMAMOTO Mitsuharu Thanks, that helps a lot. I was looking for things like 'S_n but only looked in seq.v
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: Sep 30 2023 at 07:01 UTC