# Nottingham FP Lab Blog

## Bag Equality via a Proof-Relevant Membership Relation

by Nils Anders Danielsson on March 16, 2010.
Tagged as: Lunches.

Last week I talked about a definition of bag equality—equality up to permutation—which I have used recently. The definition works for arbitrary containers, but for simplicity I will focus on lists.

The predicate transformer Any can be defined as follows (in Agda):

  data Any {A : Set} (P : A → Set) : List A → Set where
here  : ∀ {x xs} → P x      → Any P (x ∷ xs)
there : ∀ {x xs} → Any P xs → Any P (x ∷ xs)

Any P xs means that any element in xs satisfies P. Using Any and an equality relation it is easy to define the membership relation:

  _∈_ : {A : Set} → A → List A → Set
x ∈ xs = Any (_≡_ x) xs

Finally bag equality can be defined:

  _≈_ : {A : Set} → List A → List A → Set
xs ≈ ys = ∀ x → x ∈ xs ⇿ x ∈ ys

Here A ⇿ B is the set of invertible functions between A and B. Two lists xs and ys are equal when viewed as bags if, for every element x, the two sets x ∈ xs and x ∈ ys are equipotent; note that if x occurs a certain number of times in xs, then there will be a corresponding number of distinct elements in x ∈ xs.

The definition above has some nice properties:

• If _⇿_ is replaced by equivalence (coinhabitance), then we get set equality instead of bag equality. This uniformity can be exploited; one can for instance prove that map preserves bag and set equality using a single, uniform proof.
• The definition generalises to other containers, including types with infinite values (like streams).
• The use of Any can give some convenient wiggle room in proofs.

Let me illustrate the last point by proving that bind distributes from the left over append:

  xs >>= (λ x → f x ++ g x) ≈ (xs >>= f) ++ (xs >>= g)

This property does not hold for ordinary list equality (one way to see this is to let xs be true ∷ false ∷ [] and f and g both be return). I will make use of the following properties:

  (∀ x → P₁ x ⇿ P₂ x) → xs₁ ≈ xs₂ → Any P₁ xs₁ ⇿ Any P₂ xs₂
A ⇿ B → C ⇿ D → (A ⊎ C) ⇿ (B ⊎ D)

Any P (xs ++ ys)          ⇿  Any P xs ⊎ Any P ys
Any (λ x → P x ⊎ Q x) xs  ⇿  Any P xs ⊎ Any Q xs
Any P (map f xs)          ⇿  Any (P ∘ f) xs
Any P (concat xss)        ⇿  Any (Any P) xss

From the last two properties we get a derived property for bind:

  Any P (xs >>= f)           ⇿
Any P (concat (map f xs))  ⇿
Any (Any P) (map f xs)     ⇿
Any (Any P ∘ f) xs

Using these properties we can prove left distributivity. The proof is a simple calculation:

  y ∈ (xs >>= λ x → f x ++ g x)                    ⇿
Any (λ x → y ∈ f x ++ g x) xs                    ⇿
Any (λ x → y ∈ f x ⊎ y ∈ g x) xs                 ⇿
Any (λ x → y ∈ f x) xs ⊎ Any (λ x → y ∈ g x) xs  ⇿
y ∈ (xs >>= f) ⊎ y ∈ (xs >>= g)                  ⇿
y ∈ (xs >>= f) ++ (xs >>= g)

The “wiggle room” I mentioned above is visible in the calculation: the proof does not refer solely to _∈_ y, i.e. Any (_≡_ y), but also to Any P for other predicates P.

The definitions of Any and bag and set equality are available in Agda’s standard library (Data.List.Any), along with the proof of left distributivity (Data.List.Any.BagAndSetEquality).