Pierre Jouvelot (Apr 24 2022 at 15:15): 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))
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: Feb 08 2023 at 08:02 UTC