## Bag Equality via a Proof-Relevant Membership Relation

March 16th, 2010 by Nils Anders Danielsson

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).

### One Response to “Bag Equality via a Proof-Relevant Membership Relation”

1. Conor Says:

Hi Nisse

Just to remark that this use of membership is highly reminiscent of the Backhouse-Hoogendijk notion of container. Membership is being-equal-to-what’s-at-some-position-in, so it all works out the same, if you’re sufficiently blasé about what “being equal” means…

Cheers

Conor