Stream: math-comp users

Topic: `perm_eq` for swap


view this post on Zulip 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))

view this post on Zulip Pierre Roux (Apr 24 2022 at 15:39):

Maybe using set_nth?

view this post on Zulip Pierre Jouvelot (Apr 24 2022 at 16:24):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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