# Equality: Equality and equational reasoning

module plfa.part1.Equality where

Much of our reasoning has involved equality. Given two terms `M`

and `N`

, both of type `A`

, we write `M ≡ N`

to assert that `M`

and `N`

are interchangeable. So far we have treated equality as a primitive, here we show how to define it as an inductive datatype.

## Imports

This chapter has no imports. Every chapter in this book, and nearly every module in the Agda standard library, imports equality. Since we define equality here, any import would create a conflict.

## Equality

We declare equality as follows:data _≡_ {A : Set} (x : A) : A → Set where refl : x ≡ x

In other words, for any type `A`

and for any `x`

of type `A`

, the constructor `refl`

provides evidence that `x ≡ x`

. Hence, every value is equal to itself, and we have no other way of showing values equal. The definition features an asymmetry, in that the first argument to `_≡_`

is given by the parameter `x : A`

, while the second is given by an index in `A → Set`

. This follows our policy of using parameters wherever possible. The first argument to `_≡_`

can be a parameter because it doesn’t vary, while the second must be an index, so it can be required to be equal to the first.

infix 4 _≡_

We set the precedence of `_≡_`

at level 4, the same as `_≤_`

, which means it binds less tightly than any arithmetic operator. It associates neither to left nor right; writing `x ≡ y ≡ z`

is illegal.

## Equality is an equivalence relation

An equivalence relation is one which is reflexive, symmetric, and transitive. Reflexivity is built-in to the definition of equality, via the constructor`refl`

. It is straightforward to show symmetry:
sym : ∀ {A : Set} {x y : A} → x ≡ y ----- → y ≡ x sym refl = refl

How does this proof work? The argument to `sym`

has type `x ≡ y`

, but on the left-hand side of the equation the argument has been instantiated to the pattern `refl`

, which requires that `x`

and `y`

are the same. Hence, for the right-hand side of the equation we need a term of type `x ≡ x`

, and `refl`

will do.

It is instructive to develop `sym`

interactively. To start, we supply a variable for the argument on the left, and a hole for the body on the right:

```
sym : ∀ {A : Set} {x y : A}
→ x ≡ y
-----
→ y ≡ x
sym e = {! !}
```

If we go into the hole and type `C-c C-,`

then Agda reports:

```
Goal: .y ≡ .x
————————————————————————————————————————————————————————————
e : .x ≡ .y
.y : .A
.x : .A
.A : Set
```

If in the hole we type `C-c C-c e`

then Agda will instantiate `e`

to all possible constructors, with one equation for each. There is only one possible constructor:

```
sym : ∀ {A : Set} {x y : A}
→ x ≡ y
-----
→ y ≡ x
sym refl = {! !}
```

If we go into the hole again and type `C-c C-,`

then Agda now reports:

```
Goal: .x ≡ .x
————————————————————————————————————————————————————————————
.x : .A
.A : Set
```

This is the key step—Agda has worked out that `x`

and `y`

must be the same to match the pattern `refl`

!

Finally, if we go back into the hole and type `C-c C-r`

it will instantiate the hole with the one constructor that yields a value of the expected type:

```
sym : ∀ {A : Set} {x y : A}
→ x ≡ y
-----
→ y ≡ x
sym refl = refl
```

This completes the definition as given above.

Transitivity is equally straightforward:trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z ----- → x ≡ z trans refl refl = refl

Again, a useful exercise is to carry out an interactive development, checking how Agda’s knowledge changes as each of the two arguments is instantiated.

## Congruence and substitution

Equality satisfies*congruence*. If two terms are equal, they remain so after the same function is applied to both:

cong : ∀ {A B : Set} (f : A → B) {x y : A} → x ≡ y --------- → f x ≡ f y cong f refl = reflCongruence of functions with two arguments is similar:

cong₂ : ∀ {A B C : Set} (f : A → B → C) {u x : A} {v y : B} → u ≡ x → v ≡ y ------------- → f u v ≡ f x y cong₂ f refl refl = reflEquality is also a congruence in the function position of an application. If two functions are equal, then applying them to the same term yields equal terms:

cong-app : ∀ {A B : Set} {f g : A → B} → f ≡ g --------------------- → ∀ (x : A) → f x ≡ g x cong-app refl x = reflEquality also satisfies

*substitution*. If two values are equal and a predicate holds of the first then it also holds of the second:

subst : ∀ {A : Set} {x y : A} (P : A → Set) → x ≡ y --------- → P x → P y subst P refl px = px

## Chains of equations

Here we show how to support reasoning with chains of equations, as used throughout the book. We package the declarations into a module, named`≡-Reasoning`

, to match the format used in Agda’s standard library:
module ≡-Reasoning {A : Set} where infix 1 begin_ infixr 2 _≡⟨⟩_ _≡⟨_⟩_ infix 3 _∎ begin_ : ∀ {x y : A} → x ≡ y ----- → x ≡ y begin x≡y = x≡y _≡⟨⟩_ : ∀ (x : A) {y : A} → x ≡ y ----- → x ≡ y x ≡⟨⟩ x≡y = x≡y _≡⟨_⟩_ : ∀ (x : A) {y z : A} → x ≡ y → y ≡ z ----- → x ≡ z x ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z _∎ : ∀ (x : A) ----- → x ≡ x x ∎ = refl open ≡-Reasoning

This is our first use of a nested module. It consists of the keyword `module`

followed by the module name and any parameters, explicit or implicit, the keyword `where`

, and the contents of the module indented. Modules may contain any sort of declaration, including other nested modules. Nested modules are similar to the top-level modules that constitute each chapter of this book, save that the body of a top-level module need not be indented. Opening the module makes all of the definitions available in the current environment.

trans′ : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z ----- → x ≡ z trans′ {A} {x} {y} {z} x≡y y≡z = begin x ≡⟨ x≡y ⟩ y ≡⟨ y≡z ⟩ z ∎

According to the fixity declarations, the body parses as follows:

`begin (x ≡⟨ x≡y ⟩ (y ≡⟨ y≡z ⟩ (z ∎)))`

The application of `begin`

is purely cosmetic, as it simply returns its argument. That argument consists of `_≡⟨_⟩_`

applied to `x`

, `x≡y`

, and `y ≡⟨ y≡z ⟩ (z ∎)`

. The first argument is a term, `x`

, while the second and third arguments are both proofs of equations, in particular proofs of `x ≡ y`

and `y ≡ z`

respectively, which are combined by `trans`

in the body of `_≡⟨_⟩_`

to yield a proof of `x ≡ z`

. The proof of `y ≡ z`

consists of `_≡⟨_⟩_`

applied to `y`

, `y≡z`

, and `z ∎`

. The first argument is a term, `y`

, while the second and third arguments are both proofs of equations, in particular proofs of `y ≡ z`

and `z ≡ z`

respectively, which are combined by `trans`

in the body of `_≡⟨_⟩_`

to yield a proof of `y ≡ z`

. Finally, the proof of `z ≡ z`

consists of `_∎`

applied to the term `z`

, which yields `refl`

. After simplification, the body is equivalent to the term:

`trans x≡y (trans y≡z refl)`

We could replace any use of a chain of equations by a chain of applications of `trans`

; the result would be more compact but harder to read. The trick behind `∎`

means that a chain of equalities simplifies to a chain of applications of `trans`

that ends in `trans e refl`

, where `e`

is a term that proves some equality, even though `e`

alone would do.

#### Exercise `trans`

and `≡-Reasoning`

(practice)

Sadly, we cannot use the definition of trans’ using ≡-Reasoning as the definition for trans. Can you see why? (Hint: look at the definition of `_≡⟨_⟩_`

)

-- Your code goes here

## Chains of equations, another example

As a second example of chains of equations, we repeat the proof that addition is commutative. We first repeat the definitions of naturals and addition. We cannot import them because (as noted at the beginning of this chapter) it would cause a conflict:data ℕ : Set where zero : ℕ suc : ℕ → ℕ _+_ : ℕ → ℕ → ℕ zero + n = n (suc m) + n = suc (m + n)To save space we postulate (rather than prove in full) two lemmas:

postulate +-identity : ∀ (m : ℕ) → m + zero ≡ m +-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)

This is our first use of a *postulate*. A postulate specifies a signature for an identifier but no definition. Here we postulate something proved earlier to save space. Postulates must be used with caution. If we postulate something false then we could use Agda to prove anything whatsoever.

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m +-comm m zero = begin m + zero ≡⟨ +-identity m ⟩ m ≡⟨⟩ zero + m ∎ +-comm m (suc n) = begin m + suc n ≡⟨ +-suc m n ⟩ suc (m + n) ≡⟨ cong suc (+-comm m n) ⟩ suc (n + m) ≡⟨⟩ suc n + m ∎

The reasoning here is similar to that in the preceding section. We use `_≡⟨⟩_`

when no justification is required. One can think of `_≡⟨⟩_`

as equivalent to `_≡⟨ refl ⟩_`

.

Agda always treats a term as equivalent to its simplified term. The reason that one can write

```
suc (n + m)
≡⟨⟩
suc n + m
```

is because Agda treats both terms as the same. This also means that one could instead interchange the lines and write

```
suc n + m
≡⟨⟩
suc (n + m)
```

and Agda would not object. Agda only checks that the terms separated by `≡⟨⟩`

have the same simplified form; it’s up to us to write them in an order that will make sense to the reader.

#### Exercise `≤-Reasoning`

(stretch)

The proof of monotonicity from Chapter Relations can be written in a more readable form by using an analogue of our notation for `≡-Reasoning`

. Define `≤-Reasoning`

analogously, and use it to write out an alternative proof that addition is monotonic with regard to inequality. Rewrite all of `+-monoˡ-≤`

, `+-monoʳ-≤`

, and `+-mono-≤`

.

-- Your code goes here

## Rewriting

Consider a property of natural numbers, such as being even. We repeat the earlier definition:data even : ℕ → Set data odd : ℕ → Set data even where even-zero : even zero even-suc : ∀ {n : ℕ} → odd n ------------ → even (suc n) data odd where odd-suc : ∀ {n : ℕ} → even n ----------- → odd (suc n)

In the previous section, we proved addition is commutative. Given evidence that `even (m + n)`

holds, we ought also to be able to take that as evidence that `even (n + m)`

holds.

`rewrite`

notation we encountered earlier. To enable this notation, we use pragmas to tell Agda which type corresponds to equality:
{-# BUILTIN EQUALITY _≡_ #-}We can then prove the desired property as follows:

even-comm : ∀ (m n : ℕ) → even (m + n) ------------ → even (n + m) even-comm m n ev rewrite +-comm n m = ev

Here `ev`

ranges over evidence that `even (m + n)`

holds, and we show that it also provides evidence that `even (n + m)`

holds. In general, the keyword `rewrite`

is followed by evidence of an equality, and that equality is used to rewrite the type of the goal and of any variable in scope.

It is instructive to develop `even-comm`

interactively. To start, we supply variables for the arguments on the left, and a hole for the body on the right:

```
even-comm : ∀ (m n : ℕ)
→ even (m + n)
------------
→ even (n + m)
even-comm m n ev = {! !}
```

If we go into the hole and type `C-c C-,`

then Agda reports:

```
Goal: even (n + m)
————————————————————————————————————————————————————————————
ev : even (m + n)
n : ℕ
m : ℕ
```

Now we add the rewrite:

```
even-comm : ∀ (m n : ℕ)
→ even (m + n)
------------
→ even (n + m)
even-comm m n ev rewrite +-comm n m = {! !}
```

If we go into the hole again and type `C-c C-,`

then Agda now reports:

```
Goal: even (m + n)
————————————————————————————————————————————————————————————
ev : even (m + n)
n : ℕ
m : ℕ
```

The arguments have been swapped in the goal. Now it is trivial to see that `ev`

satisfies the goal, and typing `C-c C-a`

in the hole causes it to be filled with `ev`

. The command `C-c C-a`

performs an automated search, including checking whether a variable in scope has the same type as the goal.

## Multiple rewrites

One may perform multiple rewrites, each separated by a vertical bar. For instance, here is a second proof that addition is commutative, relying on rewrites rather than chains of equalities:+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m +-comm′ zero n rewrite +-identity n = refl +-comm′ (suc m) n rewrite +-suc n m | +-comm′ m n = refl

This is far more compact. Among other things, whereas the previous proof required `cong suc (+-comm m n)`

as the justification to invoke the inductive hypothesis, here it is sufficient to rewrite with `+-comm m n`

, as rewriting automatically takes congruence into account. Although proofs with rewriting are shorter, proofs as chains of equalities are easier to follow, and we will stick with the latter when feasible.

## Rewriting expanded

The`rewrite`

notation is in fact shorthand for an appropriate use of `with`

abstraction:
even-comm′ : ∀ (m n : ℕ) → even (m + n) ------------ → even (n + m) even-comm′ m n ev with m + n | +-comm m n ... | .(n + m) | refl = ev

In general, one can follow `with`

by any number of expressions, separated by bars, where each following equation has the same number of patterns. We often write expressions and the corresponding patterns so they line up in columns, as above. Here the first column asserts that `m + n`

and `n + m`

are identical, and the second column justifies that assertion with evidence of the appropriate equality. Note also the use of the *dot pattern*, `.(n + m)`

. A dot pattern consists of a dot followed by an expression, and is used when other information forces the value matched to be equal to the value of the expression in the dot pattern. In this case, the identification of `m + n`

and `n + m`

is justified by the subsequent matching of `+-comm m n`

against `refl`

. One might think that the first clause is redundant as the information is inherent in the second clause, but in fact Agda is rather picky on this point: omitting the first clause or reversing the order of the clauses will cause Agda to report an error. (Try it and see!)

even-comm″ : ∀ (m n : ℕ) → even (m + n) ------------ → even (n + m) even-comm″ m n = subst even (+-comm m n)

Nonetheless, rewrite is a vital part of the Agda toolkit. We will use it sparingly, but it is occasionally essential.

## Leibniz equality

The form of asserting equality that we have used is due to Martin Löf, and was published in 1975. An older form is due to Leibniz, and was published in 1686. Leibniz asserted the *identity of indiscernibles*: two objects are equal if and only if they satisfy the same properties. This principle sometimes goes by the name Leibniz’ Law, and is closely related to Spock’s Law, “A difference that makes no difference is no difference”. Here we define Leibniz equality, and show that two terms satisfy Leibniz equality if and only if they satisfy Martin Löf equality.

Leibniz equality is usually formalised to state that `x ≐ y`

holds if every property `P`

that holds of `x`

also holds of `y`

. Perhaps surprisingly, this definition is sufficient to also ensure the converse, that every property `P`

that holds of `y`

also holds of `x`

.

`x`

and `y`

be objects of type `A`

. We say that `x ≐ y`

holds if for every predicate `P`

over type `A`

we have that `P x`

implies `P y`

:
_≐_ : ∀ {A : Set} (x y : A) → Set₁ _≐_ {A} x y = ∀ (P : A → Set) → P x → P y

We cannot write the left-hand side of the equation as `x ≐ y`

, and instead we write `_≐_ {A} x y`

to provide access to the implicit parameter `A`

which appears on the right-hand side.

This is our first use of *levels*. We cannot assign `Set`

the type `Set`

, since this would lead to contradictions such as Russell’s Paradox and Girard’s Paradox. Instead, there is a hierarchy of types, where `Set : Set₁`

, `Set₁ : Set₂`

, and so on. In fact, `Set`

itself is just an abbreviation for `Set₀`

. Since the equation defining `_≐_`

mentions `Set`

on the right-hand side, the corresponding signature must use `Set₁`

. We say a bit more about levels below.

refl-≐ : ∀ {A : Set} {x : A} → x ≐ x refl-≐ P Px = Px trans-≐ : ∀ {A : Set} {x y z : A} → x ≐ y → y ≐ z ----- → x ≐ z trans-≐ x≐y y≐z P Px = y≐z P (x≐y P Px)Symmetry is less obvious. We have to show that if

`P x`

implies `P y`

for all predicates `P`

, then the implication holds the other way round as well:
sym-≐ : ∀ {A : Set} {x y : A} → x ≐ y ----- → y ≐ x sym-≐ {A} {x} {y} x≐y P = Qy where Q : A → Set Q z = P z → P x Qx : Q x Qx = refl-≐ P Qy : Q y Qy = x≐y Q Qx

Given `x ≐ y`

, a specific `P`

, we have to construct a proof that `P y`

implies `P x`

. To do so, we instantiate the equality with a predicate `Q`

such that `Q z`

holds if `P z`

implies `P x`

. The property `Q x`

is trivial by reflexivity, and hence `Q y`

follows from `x ≐ y`

. But `Q y`

is exactly a proof of what we require, that `P y`

implies `P x`

.

`x ≡ y`

we need for any `P`

to take evidence of `P x`

to evidence of `P y`

, which is easy since equality of `x`

and `y`

implies that any proof of `P x`

is also a proof of `P y`

:
≡-implies-≐ : ∀ {A : Set} {x y : A} → x ≡ y ----- → x ≐ y ≡-implies-≐ x≡y P = subst P x≡y

This direction follows from substitution, which we showed earlier.

In the reverse direction, given that for any`P`

we can take a proof of `P x`

to a proof of `P y`

we need to show `x ≡ y`

:
≐-implies-≡ : ∀ {A : Set} {x y : A} → x ≐ y ----- → x ≡ y ≐-implies-≡ {A} {x} {y} x≐y = Qy where Q : A → Set Q z = x ≡ z Qx : Q x Qx = refl Qy : Q y Qy = x≐y Q Qx

The proof is similar to that for symmetry of Leibniz equality. We take `Q`

to be the predicate that holds of `z`

if `x ≡ z`

. Then `Q x`

is trivial by reflexivity of Martin Löf equality, and hence `Q y`

follows from `x ≐ y`

. But `Q y`

is exactly a proof of what we require, that `x ≡ y`

.

(Parts of this section are adapted from *≐≃≡: Leibniz Equality is Isomorphic to Martin-Löf Identity, Parametrically*, by Andreas Abel, Jesper Cockx, Dominique Devries, Andreas Nuyts, and Philip Wadler, draft, 2017.)

## Universe polymorphism

As we have seen, not every type belongs to `Set`

, but instead every type belongs somewhere in the hierarchy `Set₀`

, `Set₁`

, `Set₂`

, and so on, where `Set`

abbreviates `Set₀`

, and `Set₀ : Set₁`

, `Set₁ : Set₂`

, and so on. The definition of equality given above is fine if we want to compare two values of a type that belongs to `Set`

, but what if we want to compare two values of a type that belongs to `Set ℓ`

for some arbitrary level `ℓ`

?

*universe polymorphism*, where a definition is made with respect to an arbitrary level

`ℓ`

. To make use of levels, we first import the following:
open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)

We rename constructors `zero`

and `suc`

to `lzero`

and `lsuc`

to avoid confusion between levels and naturals.

Levels are isomorphic to natural numbers, and have similar constructors:

```
lzero : Level
lsuc : Level → Level
```

The names `Set₀`

, `Set₁`

, `Set₂`

, and so on, are abbreviations for

```
Set lzero
Set (lsuc lzero)
Set (lsuc (lsuc lzero))
```

and so on. There is also an operator

`_⊔_ : Level → Level → Level`

that given two levels returns the larger of the two.

Here is the definition of equality, generalised to an arbitrary level:data _≡′_ {ℓ : Level} {A : Set ℓ} (x : A) : A → Set ℓ where refl′ : x ≡′ xSimilarly, here is the generalised definition of symmetry:

sym′ : ∀ {ℓ : Level} {A : Set ℓ} {x y : A} → x ≡′ y ------ → y ≡′ x sym′ refl′ = refl′

For simplicity, we avoid universe polymorphism in the definitions given in the text, but most definitions in the standard library, including those for equality, are generalised to arbitrary levels as above.

Here is the generalised definition of Leibniz equality:_≐′_ : ∀ {ℓ : Level} {A : Set ℓ} (x y : A) → Set (lsuc ℓ) _≐′_ {ℓ} {A} x y = ∀ (P : A → Set ℓ) → P x → P y

Before the signature used `Set₁`

as the type of a term that includes `Set`

, whereas here the signature uses `Set (lsuc ℓ)`

as the type of a term that includes `Set ℓ`

.

_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃} → (B → C) → (A → B) → A → C (g ∘ f) x = g (f x)

Further information on levels can be found in the Agda docs.

## Standard library

Definitions similar to those in this chapter can be found in the standard library. The Agda standard library defines`_≡⟨_⟩_`

as `step-≡`

, which reverses the order of the arguments. The standard library also defines a syntax macro, which is automatically imported whenever you import `step-≡`

, which recovers the original argument order:
-- import Relation.Binary.PropositionalEquality as Eq -- open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst) -- open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

Here the imports are shown as comments rather than code to avoid collisions, as mentioned in the introduction.

## Unicode

This chapter uses the following unicode:

```
≡ U+2261 IDENTICAL TO (\==, \equiv)
⟨ U+27E8 MATHEMATICAL LEFT ANGLE BRACKET (\<)
⟩ U+27E9 MATHEMATICAL RIGHT ANGLE BRACKET (\>)
∎ U+220E END OF PROOF (\qed)
≐ U+2250 APPROACHES THE LIMIT (\.=)
ℓ U+2113 SCRIPT SMALL L (\ell)
⊔ U+2294 SQUARE CUP (\lub)
₀ U+2080 SUBSCRIPT ZERO (\_0)
₁ U+2081 SUBSCRIPT ONE (\_1)
₂ U+2082 SUBSCRIPT TWO (\_2)
```