Multiset of fixed cardinality

Stream: mathlib4

[Martin Dvořák]

I would like to work with multisets of fixed cardinality.
MWE:

import Mathlib.Data.List.OfFn
open scoped List

-- `n`-ary operation on `α`
abbrev MyOperation (α : Type) (n : ℕ) : Type := (Fin n → α) → α

-- permuting the input does not change the output
def MyOperation.IsSymmetric {α : Type} {n : ℕ} (g : MyOperation α n) : Prop :=
  ∀ x y : Fin n → α, List.ofFn x ~ List.ofFn y → g x = g y

For those operations that happen to be symmetric, I would like to convert them to a function Multiset α → α but only on multisets of cardinality n. The motivation is that I do a lot of summations later. Working with Multiset.sum should be easier than with List.sum since I already have Finset.sum elsewhere and they will have to be compared.

Do we have such a notion in Mathlib? I could use a subtype, but it wouldn't be very convenient.

[Eric Wieser]

docs#Sym is that notion.

[Martin Dvořák]

Thanks a lot!

[Martin Dvořák]

Eric Wieser said:

docs#Sym is that notion.

Should
https://github.com/leanprover-community/mathlib4/blob/c671da20f0a9c6375a329f6b4a723ba9e0d8eb5a/Mathlib/Combinatorics/Optimization/ValuedCSP.lean#L120
be refactored to

∀ g ∈ ω, some_existing_Mathlib_notion g

for better compatibility with Sym please?

I would like to know if there is more API that I could (and indeed should) reüse.

[Eric Wieser]

I would have gone with

def FractionalOperation.IsSymmetric (ω : FractionalOperation D m) : Prop :=
  ∀ (σ : Equiv.Perm (Fin m)), ∀ g ∈ ω, g ∘  σ = g

[Eric Wieser]

But that's probably less not more compatible with Sym

[Martin Dvořák]

Is there a canonical way to "require symmetry" before converting an operation to Sym please?

[Eric Wieser]

What do you mean by "converting to Sym"?

[Martin Dvořák]

Eric Wieser said:

What do you mean by "converting to Sym"?

def FractionalOperation.IsSymmetric.toSym {ω : FractionalOperation D m} (hω : ω.IsSymmetric) :
    Multiset (Sym D m → D) := sorry

[Martin Dvořák]

In particular, I want to convert every term of the (Fin m → D) → D type to a term of the Sym D m → D type.

[Martin Dvořák]

Which also brings up a question whether there is a canonical conversion from Sym D m to Fin m → D.

[Martin Dvořák]

This is not a usual conversion, is it? I guess it is up to me how I do it and then I have to write the API myself?

[Martin Dvořák]

Perhaps I should build on top of docs#Sym.ofVector ...

[Eric Wieser]

Martin Dvořák said:

Which also brings up a question whether there is a canonical conversion from Sym D m to Fin m → D.

No, this direction cannot be canonical (unless you can sort D or similar)

[Martin Dvořák]

Sorry, I misused the word "canonical". I meant standard.

[Martin Dvořák]

Martin Dvořák said:

Perhaps I should build on top of docs#Sym.ofVector ...

Together with docs#Vector.ofFn should work.

[Martin Dvořák]

Well, I am the other way around...

[Martin Dvořák]

I manage to put together this conversion

import Mathlib.Data.Sym.Basic

noncomputable def Function.ofSym {D : Type*} {m : ℕ}
    (x : Sym D m) (i : Fin m) : D := by
  refine (x.attach.toMultiset.toList.get (Fin.cast ?_ i)).1
  rw [Sym.coe_attach, Multiset.length_toList, Multiset.attach, Multiset.card_pmap]
  exact x.property.symm

but it feels very very very wrong.

[Martin Dvořák]

Don't get me wrong — the noncomputable is not the problem — I will end up having noncomputable in one place or the other either way. The "body" of the definition is horrendous!

[Antoine Chambert-Loir]

Then just prove that the map you see is surjective and take a right inverse for the one you want, using docs#Function.surjInv

[Eric Wieser]

I think that's probably a worse approach here, because you lose the ability to translate to toList

[Eric Wieser]

I don't see why you needed the attach; why not just x.toMultiset.toList.get (Fin.cast ?_ i)?

[Martin Dvořák]

You are completely right! I thought I was losing the property, but I was wrong, fortunately.
This works:

import Mathlib.Data.Sym.Basic

noncomputable def Function.ofSym (x : Sym D m) (i : Fin m) : D := by
  refine x.toMultiset.toList.get (Fin.cast ?_ i)
  rw [Multiset.length_toList]
  exact x.property.symm

[Martin Dvořák]

Better:

import Mathlib.Data.Sym.Basic

lemma Sym.toMultiset_toList_length (x : Sym D m) : x.toMultiset.toList.length = m := by
  rw [Multiset.length_toList]
  exact x.property

noncomputable def Function.ofSym (x : Sym D m) (i : Fin m) : D :=
  x.toMultiset.toList.get (Fin.cast x.toMultiset_toList_length.symm i)