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.

We declare the precedence of equality as follows:
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  =  refl
Congruence 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  =  refl
Equality 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 = refl
Equality 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

A predicate is a proposition over values of some type A, and since we model propositions as types, a predicate is a type parameterized in A. As an example, even : ℕ → Set and odd : ℕ → Set from Chapter Relations are predicates on natural numbers ℕ. (We will compare representing predicates as data types A → Set versus functions to booleans A → Bool in Chapter Decidable.)

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 step-≡-∣ step-≡-⟩
  infix  3 _∎

  begin_ : ∀ {x y : A} → x ≡ y → x ≡ y
  begin x≡y  =  x≡y

  step-≡-∣ : ∀ (x : A) {y : A} → x ≡ y → x ≡ y
  step-≡-∣ x x≡y  =  x≡y

  step-≡-⟩ : ∀ (x : A) {y z : A} → y ≡ z → x ≡ y → x ≡ z
  step-≡-⟩ x y≡z x≡y  =  trans x≡y y≡z

  syntax step-≡-∣ x x≡y      =  x ≡⟨⟩ x≡y
  syntax step-≡-⟩ x y≡z x≡y  =  x ≡⟨  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, and the keyword where; this is followed by the contents of the module, which must be 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.

This is also our first use of a syntax declaration, which specifies that the term on the left may be written with the syntax on the right. The syntax x ≡⟨ x≡y ⟩ y≡z inherits the fixity infixr 2 declared for step-≡-⟩, and the special syntax is available when the identifier step-≡-⟩ is imported. Similarly for step-≡-∣.

Rather than introducing step-≡ with special syntax, we might have declared _≡⟨_⟩′_ directly:
_≡⟨_⟩′_ : ∀ {A : Set} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
x ≡⟨ x≡y ⟩′ y≡z  =  trans x≡y y≡z

The reason for indirection is that step-≡-⟩ reverses the order of the arguments, which happens to allow Agda to perform type inference more efficiently. We will encounter some long chains in Chapter Lambda, so efficiency can be important.

Let’s look at a proof of transitivity as a chain of equations:
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 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 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.

(That trick might seem inefficient, since trans e refl and e both prove the same equality. But that inefficiency is key to our nice notation for chains of equalities. One shouldn’t fear inefficiency if it improves readability!)

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.

We then repeat the proof of commutativity:
+-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.

Agda includes special notation to support just this kind of reasoning, the 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!)

In this case, we can avoid rewrite by simply applying the substitution function defined earlier:
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.

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

Leibniz equality is reflexive and transitive, where the first follows by a variant of the identity function and the second by a variant of function composition:
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.

We now show that Martin-Löf equality implies Leibniz equality, and vice versa. In the forward direction, if we know 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 ℓ?

The answer is 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 ≡′ x
Similarly, 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 ℓ.

Most other functions in the standard library are also generalised to arbitrary levels. For instance, here is the definition of composition.
_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : 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)