### Bag Equality via a Proof-Relevant Membership Relation

Tuesday, March 16th, 2010 by Nils Anders DanielssonLast 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).