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

comments powered by Disqus