## Stream: math-comp users

### Topic: `perm_eq` for swap

#### Pierre Jouvelot (Apr 24 2022 at 15:15):

I can see a way to try to prove this by cutting `s` into pieces, using `i1` and `i2` as boundaries, but before diving into this, I wonder whether there is more elegant way to prove this:

``````  lt1s : i1 < size s
lt2s : i2 < size s
============================
perm_eq [seq (if i == i2 then i1 else if i == i1 then i2 else i) | i <- iota 0 (size s)]
(iota 0 (size s))
``````

#### Pierre Roux (Apr 24 2022 at 15:39):

Maybe using `set_nth`?

#### Pierre Jouvelot (Apr 24 2022 at 16:24):

Ah, I hadn't considered this approach. Thanks for the idea :smile:

#### Kazuhiko Sakaguchi (Apr 24 2022 at 17:09):

I think that relying on the definition of `perm_eq` or using `permP` is the easiest way to prove that. https://math-comp.github.io/htmldoc/mathcomp.ssreflect.seq.html#perm_eq

#### Pierre Roux (Apr 24 2022 at 18:18):

Indeed, and if you use `set_nth`, this PR may be useful: https://github.com/math-comp/math-comp/pull/877

#### Pierre Jouvelot (May 01 2022 at 19:00):

While thinking about all these interesting suggestions, I also figured out that using `uniq_perm` led to a somewhat short proof, using `map_uniq` and the fact that a transposition is an involution to prove the unicity of the transposed `iota`.

Last updated: Jul 15 2024 at 21:02 UTC