Infinite multisets

Stream: Is there code for X?

[Daniel Weber]

Are there infinite multisets in Mathlib? I'm thinking of something like the quotient of Σ α : Type u, α → β by equivalence of α

[Ruben Van de Velde]

Is that not just a function to Nat?

[Daniel Weber]

No, an element may appear infinitely many times (in general my elements are types, so I want to avoid comparing them)

[Daniel Weber]

Actually this might be an #xy, give me a few minutes to write my actual problem

[Kevin Buzzard]

The short answer is "no" I guess -- a multiset is defined to be a list modulo forgetting the order of the elements (and lists are finite).

[Daniel Weber]

Thinking about this a lot more, I think I'm just missing some operations on multisets as types, I'll working on PR-ing this to Mathlib

import Mathlib

variable {α β : Type*} [DecidableEq α] [DecidableEq β]

instance : IsEmpty (0 : Multiset α) := Fintype.card_eq_zero_iff.mp (by simp)

def Multiset.consEquiv {s : Multiset α} {v : α} : (v ::ₘ s) ≃ Option s where
  toFun x := if h : x.1 = v ∧ x.2.val = s.count v then none else some ⟨x.1, ⟨x.2, by
    by_cases hv : x.1 = v
    · simp only [hv, true_and] at h ⊢
      apply lt_of_le_of_ne (Nat.le_of_lt_add_one _) h
      convert x.2.2 using 1
      simp [hv]
    · convert x.2.2 using 1
      exact (count_cons_of_ne hv _).symm
    ⟩⟩
  invFun x := x.elim ⟨v, ⟨s.count v, by simp⟩⟩ (fun x ↦ ⟨x.1, x.2.castLE (count_le_count_cons ..)⟩)
  left_inv := by
    rintro ⟨x, hx⟩
    dsimp only
    split
    · rename_i h
      obtain ⟨rfl, h2⟩ := h
      simp [← h2]
    · simp
  right_inv := by
    rintro (_ | x)
    · simp
    · simp only [Option.elim_some, Nat.zero_eq, Fin.coe_castLE, Fin.eta, Sigma.eta, dite_eq_ite,
      ite_eq_right_iff, reduceCtorEq, imp_false, not_and]
      apply ne_of_lt ∘ (· ▸ x.2.2)

@[simps]
def Multiset.cast {s t : Multiset α} (h : s = t) : s ≃ t where
  toFun x := ⟨x.1, x.2.cast (by simp [h])⟩
  invFun x := ⟨x.1, x.2.cast (by simp [h])⟩
  left_inv x := rfl
  right_inv x := rfl

private theorem Multiset.mapEquiv_aux (s : Multiset α) (f : α → β) : ∃ v : s ≃ s.map f, ∀ a : s, v a = f a := by
  induction s using Multiset.induction with
  | empty =>
    simp only [map_zero, count_zero, Multiset.forall_coe, IsEmpty.forall_iff, implies_true]
    use Equiv.equivOfIsEmpty _ _
  | cons a s ih =>
    obtain ⟨v, hv⟩ := ih
    use Multiset.consEquiv.trans v.optionCongr |>.trans Multiset.consEquiv.symm |>.trans <| (Multiset.cast (map_cons f a s)).symm
    intro x
    simp only [consEquiv, Equiv.trans_apply, Equiv.coe_fn_mk, Equiv.optionCongr_apply,
      Equiv.coe_fn_symm_mk, cast_apply_fst]
    split <;> simp_all

noncomputable def Multiset.mapEquiv (s : Multiset α) (f : α → β) : s ≃ s.map f := (Multiset.mapEquiv_aux s f).choose

theorem Multiset.mapEquiv_apply (s : Multiset α) (f : α → β) (v : s) : s.mapEquiv f v = f v := (Multiset.mapEquiv_aux s f).choose_spec v

[Violeta Hernández]

Daniel Weber said:

No, an element may appear infinitely many times (in general my elements are types, so I want to avoid comparing them)

What kind of infinity? An ordinal? A cardinal? An extended natural?

[Violeta Hernández]

All of those notions can be implemented as α → β for the appropriate type β

[Daniel Weber]

I want something which is equivalent to the quotient of Σ α : Type u, α → β, so I think that's a cardinal