equal lists can be permuted

Stream: new members

[Monica Omar]

I want to show that there exists some Equiv.Perm for any two equal finite lists. No clue how to go about this tbh, any help would be appreciated:

import Mathlib.Logic.Equiv.Defs
import Mathlib.Algebra.BigOperators.Basic

example {R : Type _} {n : ℕ} [DecidableEq R] (A₁ A₂ : Fin n → R)
  (h : ∀ (x : R), (∃ (i : Fin n), A₁ i = x) ↔ ∃ (i : Fin n), A₂ i = x) :
  ∃ (U : Equiv.Perm (Fin n)), ∀ (i : Fin n), A₂ i = A₁ ((Equiv.symm U) i) :=

[Martin Dvořák]

I don't think it holds. Consider A₁ = !['a', 'a', 'b'] and A₂ = !['a', 'b', 'b'].

[Monica Omar]

Oh right, we'd need to probably say something about uniqueness for it to hold and the lists to actually be equal (up to permutation)?

[Martin Dvořák]

Depends on what kind of characterization you want and what type you want to apply it to. You may want to talk about ~ on Lists, you may want to talk about = on Multisets...

[Martin Dvořák]

You may want to have Finset which is Multiset without duplicates.

[Richard Copley]

(~ is notation for docs#List.Perm which is the thing you seemed to be asking for at first)

[Richard Copley]

docs#List.isPerm_iff might be useful too

[Monica Omar]

Let's stick with Fin n -> R for now.

So what I wanted to say is that both vectors are equal, and also that they have the same multiplicities. So if A₁ has two 'a''s then so should A₂. Then there should exist a permutation Equiv.Perm that permutes one to the other.

How do I say this in Lean though, my mind is drawing a blank at the moment.

[Martin Dvořák]

It seems to me that you have a weird notion of "both vectors are equal".

[Martin Dvořák]

Do you want to say, as you assumption, that converting both vectors to a multisets gives equal multisets?

[Monica Omar]

Yeah, actually, you're right, it does seem weird.

Okay, let's go for Set R then? And say that both sets are equal with equal multiplicities?

[Martin Dvořák]

I didn't offer Set for a reason — it doesn't track multiplicities.

[Monica Omar]

Martin Dvořák said:

Do you want to say, as you assumption, that converting both vectors to a multisets gives equal multisets?

Perhaps, perhaps. You know, I kind of lost track of what I was trying to even prove in the first place lmao

[Monica Omar]

Lemme have a rethink of all this, and get back on this tomorrow

[Monica Omar]

Okay, what's a nice way to describe that every entry of A₁ and A₂ are equal with the same multiplicity?

[Richard Copley]

It's hard to know how to answer. If this is an exercise you've set yourself, it would be a shame to spoil it for you. If it's something you think you need as part of the solution to a broader problem, the best advice would depend on the details of that problem (but would probably be "you should rephrase the problem in terms of multisets").

[Monica Omar]

Naw, naw, it's ok. Please spoil it haha

[Richard Copley]

Well, no, because while it won't be difficult, it will take a long time and it will be boring, and it will serve no useful purpose. The good ways to do this already exist.

[Monica Omar]

What are the good ways? How do I transform (A₁ A₂ : Fin n -> R) to multisets?

[Richard Copley]

Multiset.ofList (List.ofFn f) is one way. There might be a direct conversion.

[Matt Diamond]

Monica Omar said:

Okay, what's a nice way to describe that every entry of A₁ and A₂ are equal with the same multiplicity?

Richard already mentioned docs#List.Perm... would that work? That seems like a pretty direct statement of what you're asking.

[Martin Dvořák]

Richard Copley said:

Multiset.ofList (List.ofFn f) is one way. There might be a direct conversion.

I believe that Finset.univ.val.map A₁ should also produce the multiset.

[Kyle Miller]

For Fin n -> R functions, you could say that for each element of R that the preimages have the same cardinality. You could write a preimage cardinality as (Finset.filter (fun i => A₁ i = r)).card.

I'm not sure if this is any good in practice, but at least it's a simple definition.

[Matt Diamond]

on a side note, @Monica Omar was asking for proof that an Equiv.Perm exists but that doesn't actually make sense in the context of lists, right? Equiv.Perm only works for types or sets coerced to types

[Kyle Miller]

At least you could ask for an Equiv.Perm for the type of indices for a list, so that when you reindex according to it you get the other list.