# Unary Relation Examples

Lately I’ve been learning the dependently typed programming language Agda. While it’s a joy to learn, learning materials for the Agda standard library are sparse. In this post, I give examples using of the stdlib’s Relation.Unary module to do elementary set theory. The logical propositions I prove herein are rather trivial, but for newbies to dependently-typed languages like me, even the trivial can seem hard.

## Preliminaries

You can read this post without knowing any Agda. If nothing else, you can get a hint of the kinds of things you can do with the concept and an implementation of propositions as types.

I make reference to the Programming Language Foundations in Agda (PLFA) online book, and I highly recommend (at least chapter 1) for learning the basics of Agda.

### Basic Structure

_ : Proposition
_ = Proof

To the right of the : is a claim, a proposition. To the right of the = is a proof of that claim. The _ on both lines just means I haven’t given this expression a name.

## Predicates

Prior to learning Agda/type theory/etc, I understood the term predicate to mean a unary function (function of one argument) that returns a boolean (i.e. true or false): A → Bool. This view of predicates as indicator functions turns out to be rather limited understanding. Another, richer, understanding sees predicates as unary functions to Set (the collection of all types): A → Set. Here’s a hint at what this is all about. and here’s a description from the Relation.Unary docs:

-- Unary relations are known as predicates and Pred A ℓ can be viewed
-- as some property that elements of type A might satisfy.

-- Consequently P : Pred A ℓ can also be seen as a subset of A
-- containing all the elements of A that satisfy property P. This view
-- informs much of the notation used below.

## Setup

Show module setup and imports.

First, create a module. The name of the top-level module of in a file should match the filename.

module index where

By importing Relation.Unary module, we get access to its contents. The open statement brings the module’s content into scope as if the names were define within the current module. Without the open statement, we’d have to qualify all the names to use them, as in Relation.Unary._∈_.

open import Relation.Unary

Other imports we’ll need:

open import Data.Unit using ( tt )
open import Level
open import Relation.Binary.PropositionalEquality using ( refl )
open import Relation.Nullary using ( ¬_  )
open import Relation.Nullary.Negation using ( contradiction )
open import Data.Product
open import Data.Sum.Base using (_⊎_; inj₁ ; inj₂ ; [_,_]′ )

## Example Set

Here’s the three element set I’ll work with in the examples:

$\{ Orange, Apple, Banana \}$

This set can be defined in adga as a simple datatype:

data Fruit : Set where
Orange Apple Banana : Fruit

## Example Propositions/Proofs

In each of the examples below, I show how to one can prove the proposition in the header. So for example, the first proposition is that $$Orange \in \{ Orange \}$$, i.e. $$Orange$$ is in the singleton set containing $$Orange$$. This should hopefully be easy to prove.

### Set inclusion

#### $$Orange \in \{ Orange \}$$

Indeed, to prove the proposition, we state refl, which stands for reflexity.

_ : Orange ∈ ｛ Orange ｝
_ = refl

Inlining ∈ and ｛_｝ step by step might make it easier to see what’s going on:

    Orange ∈ ｛ Orange ｝
== ｛ Orange ｝ Orange    ( x ∈ P = P x )
==  Orange = Orange      ( ｛ x ｝ = x ≡_) 

Proof of the statement Orange = Orange is refl.

#### $$\neg ( Banana \in \{ Orange \} )$$

The claim $$Banana \in \{ Orange \}$$ should not hold; i.e., we should be able to construct a proof of the negation of the claim.

_ : ¬ ( Banana ∈ ｛ Orange ｝ )
_ = λ()

In this case, we can use an absurd pattern:

Absurd patterns can be used when none of the constructors for a particular argument would be valid.

This is indeed the case here, as we cannot construct a proof that Banana = Orange. For more on negation in constructive logic and Agda, see the negation chapter in PLFA.

I’ll note that the proposition above is equivalent to the following by definition of _∉_:

_ :  Banana ∉ ｛ Orange ｝
_ = λ()

#### $$Orange \in \{ Orange, Apple \}$$

Now I move beyond singleton sets and define a subset containing both $$Orange$$ and $$Apple$$. This is straighforward with the union _∪_ operator:

O∪A : Pred Fruit _
O∪A = ｛ Orange ｝ ∪ ｛ Apple ｝

The union operator constructs a Sum type, which I think of as the proposition that either the ｛ Orange ｝ claim or the ｛ Apple ｝ claim holds. Hence to prove the claim, we give a proof of $$Orange \in \{ Orange \}$$ to the first (inj₁) position in the sum.

_ : Orange ∈ O∪A
_ = inj₁ refl

For more on the sum type, see the Disjunction as Sum section in PLFA.

#### $$Orange \in \{ Orange, Apple, Banana \}$$

The U symbol represents the univeral set for a type. I find that symbol hard to distinguish from the union operator and infinitary union, so I’ll give the set $$\{ Orange, Apple, Banana \}$$ a name.

allFruit : Pred Fruit _
allFruit = U

The examples holds trivially because allFruit is the universal set of Fruit.

_ :  Orange ∈ allFruit
_ = tt

I’ll inline the proposition again to see what is needed of the proof.

    Orange ∈ allFruit
== allFruit Orange  ( by definition )
== U Orange         ( by definition )
== (λ _ → ⊤) Orange ( by definition )
== ⊤                ( function application )

So we need a term of type ⊤, for which tt is the only constructor for the ⊤ (unit) type.

### Subset relations

I’ll switch from proofs about set inclusion to proofs on subset relations.

The subset relation states that a proof P is a subset of Q is evidence that for all x in P, x is also in Q. Or in agda:

_⊆_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊆ Q = ∀ {x} → x ∈ P → x ∈ Q

#### $$\{ Orange, Apple \} \subseteq \{ Orange, Apple, Banana \}$$

The first one is simple:

_ : O∪A ⊆ allFruit
_ = λ _  → tt 

#### $$\{ Orange \} \cap \{ Orange, Apple \} \subseteq \{ Orange \}$$

_ : ( ｛ Orange ｝ ∩ O∪A ) ⊆ ｛ Orange ｝
_ = λ ｛O｝∩O∪A → proj₁ ｛O｝∩O∪A

Again inlining the claim might it more clear why the evidence I provided is proof of the claim.

   ∀ {x} → x ∈ ( ｛ Orange ｝ ∩ O∪A ) → x ∈ ｛ Orange ｝  (definition of _⊆_)
== ∀ {x} → (λ y → y ∈ ｛ Orange ｝ × y ∈ O∪A ) x → x ∈ ｛ Orange ｝ (definition of  _∩_)
== ∀ {x} → x ∈ ｛ Orange ｝ × x ∈ O∪A → x ∈ ｛ Orange ｝      (function application )

Ignoring the ∀ {x}, the claim states that proof is a function that take the product of x ∈ ｛ Orange ｝ and x ∈ O∪A and returns x ∈ ｛ Orange ｝, which is exactly what I wrote. Note that I could just as well have written: λ x → proj₁ x. The name of lambda variable is irrelevant, but I used the name ｛O｝∩O∪A to give a visual cue what type is being passed.

#### $$\{ Banana \} \not\subseteq \{ Orange, Apple \}$$

This one is little trickier:

_ : ｛ Banana ｝ ⊈ O∪A
_ = λ b⊆O∪A → [ ( λ () ) , ( λ () ) ]′ (b⊆O∪A refl) 

I used the [_,_]′ function. to produce a term of ¬ (｛ Banana ｝ ⊆ O∪A ).

### Equality of Pred

Now that we have an idea how to prove subset relations; I’ll demonstrate proofs for equality of predicates. Predicate equality is defined in recent versions of Relation.Unary, but for some reason, it’s not in the version I’m using, so I define it here:

_≐_ : ∀ {  ℓ₁ ℓ₂ : Level } { C : Set } → Pred C ℓ₁ → Pred C ℓ₂ → Set _
P ≐ Q = (P ⊆ Q) × (Q ⊆ P)

I won’t go through these in detail. I will reiterate that proof in each case involves producing a pair proofs, one for P ⊆ Q and another for Q ⊆ P.

#### $$\{ Orange \} \cap \{ Orange, Apple, Banana \} = \{ Orange \}$$

_ : ( ｛ Orange ｝ ∩ allFruit ) ≐ ( ｛ Orange ｝ )
_ =   (λ ( o∈O , _ ) → o∈O )
, ( λ o∈O →  o∈O , tt )  

#### $$\{ Orange \} \cap \{ Apple \} = \emptyset$$

_ :  ( ｛ Orange ｝ ∩ ｛ Apple ｝ ) ≐ ∅
_ =   ( λ { (refl , ())})
, ( λ () )

#### $$\{ Orange \} \cup \{ Apple \} \cup \{ Banana \} = \bigcup$$

_ :  ( ｛ Orange ｝ ∪ ｛ Apple ｝ ∪ ｛ Banana ｝ ) ≐ allFruit
_ =  ( λ _ → tt )
, λ { {Orange} _ →  inj₁ refl
; {Apple} _ → inj₂ (inj₁ refl)
; {Banana} _ → inj₂ (inj₂ refl)
} 

## Fin

I hope to share more of my Agda learnings in the coming weeks.