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.

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

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