multiset α is the quotient of list α by list permutation. The result is a type of finite sets with duplicates allowed.

0 : multiset α is the empty set

cons a s is the multiset which contains s plus one more instance of a.

Dependent recursor on multisets.

TODO: should be @[recursor 6], but then the definition of multiset.pi failes with a stack overflow in whnf.

a ∈ s means that a has nonzero multiplicity in s.

s ⊆ t is the lift of the list subset relation. It means that any element with nonzero multiplicity in s has nonzero multiplicity in t, but it does not imply that the multiplicity of a in s is less or equal than in t; see s ≤ t for this relation.

s ≤ t means that s is a sublist of t (up to permutation). Equivalently, s ≤ t means that count a s ≤ count a t for all a.

The cardinality of a multiset is the sum of the multiplicities of all its elements, or simply the length of the underlying list.

The sum of two multisets is the lift of the list append operation. This adds the multiplicities of each element, i.e. count a (s + t) = count a s + count a t.

repeat a n is the multiset containing only a with multiplicity n.

range n is the multiset lifted from the list range n, that is, the set {0, 1, ..., n-1}.

erase s a is the multiset that subtracts 1 from the multiplicity of a.

map f s is the lift of the list map operation. The multiplicity of b in map f s is the number of a ∈ s (counting multiplicity) such that f a = b.

foldl f H b s is the lift of the list operation foldl f b l, which folds f over the multiset. It is well defined when f is right-commutative, that is, f (f b a₁) a₂ = f (f b a₂) a₁.

foldr f H b s is the lift of the list operation foldr f b l, which folds f over the multiset. It is well defined when f is left-commutative, that is, f a₁ (f a₂ b) = f a₂ (f a₁ b).

Product of a multiset given a commutative monoid structure on α. prod {a, b, c} = a * b * c

join S, where S is a multiset of multisets, is the lift of the list join operation, that is, the union of all the sets.

join {{1, 2}, {1, 2}, {0, 1}} = {0, 1, 1, 1, 2, 2}

bind s f is the monad bind operation, defined as join (map f s). It is the union of f a as a ranges over s.

The multiplicity of (a, b) in product s t is the product of the multiplicity of a in s and b in t.

sigma s t is the dependent version of product. It is the sum of (a, b) as a ranges over s and b ranges over t a.

Lift of the list pmap operation. Map a partial function f over a multiset s whose elements are all in the domain of f.

"Attach" a proof that a ∈ s to each element a in s to produce a multiset on {x // x ∈ s}.

decidable equality for functions whose domain is bounded by multisets

s - t is the multiset such that count a (s - t) = count a s - count a t for all a.

s ∪ t is the lattice join operation with respect to the multiset ≤. The multiplicity of a in s ∪ t is the maximum of the multiplicities in s and t.

s ∩ t is the lattice meet operation with respect to the multiset ≤. The multiplicity of a in s ∩ t is the minimum of the multiplicities in s and t.

filter p s returns the elements in s (with the same multiplicities) which satisfy p, and removes the rest.

filter_map f s is a combination filter/map operation on s. The function f : α → option β is applied to each element of s; if f a is some b then b is added to the result, otherwise a is removed from the resulting multiset.

The antidiagonal of a multiset s consists of all pairs (t₁, t₂) such that t₁ + t₂ = s. These pairs are counted with multiplicities.

A pair (t₁, t₂) of multisets is contained in antidiagonal s if and only if t₁ + t₂ = s.

countp p s counts the number of elements of s (with multiplicity) that satisfy p.

count a s is the multiplicity of a in s.

rel r s t -- lift the relation r between two elements to a relation between s and t, s.t. there is a one-to-one mapping betweem elements in s and t following r.

disjoint s t means that s and t have no elements in common.

pairwise r m states that there exists a list of the elements s.t. r holds pairwise on this list.

nodup s means that s has no duplicates, i.e. the multiplicity of any element is at most 1.

erase_dup s removes duplicates from s, yielding a nodup multiset.

ndinsert a s is the lift of the list insert operation. This operation does not respect multiplicities, unlike cons, but it is suitable as an insert operation on finset.

ndunion s t is the lift of the list union operation. This operation does not respect multiplicities, unlike s ∪ t, but it is suitable as a union operation on finset. (s ∪ t would also work as a union operation on finset, but this is more efficient.)

ndinter s t is the lift of the list ∩ operation. This operation does not respect multiplicities, unlike s ∩ t, but it is suitable as an intersection operation on finset. (s ∩ t would also work as a union operation on finset, but this is more efficient.)

fold op b s folds a commutative associative operation op over the multiset s.

Supremum of a multiset: sup {a, b, c} = a ⊔ b ⊔ c

Infimum of a multiset: inf {a, b, c} = a ⊓ b ⊓ c

sort s constructs a sorted list from the multiset s. (Uses merge sort algorithm.)

pi m t constructs the Cartesian product over t indexed by m.

Ico n m is the multiset lifted from the list Ico n m, e.g. the set {n, n+1, ..., m-1}.

The antidiagonal of a natural number n is the multiset of pairs (i,j) such that i+j = n.

A pair (i,j) is contained in the antidiagonal of n if and only if i+j=n.

The cardinality of the antidiagonal of n is n+1.

The antidiagonal of 0 is the list [(0,0)]

The antidiagonal of n does not contain duplicate entries.