module Padova2025.ProvingBasics.Equality.Base where

Definition

In blackboard mathematics, “x = y” is an assertion, a statement. For instance, this assertion might be true, or it might be false. In the Agda community, x ≡ y is a type—the type of witnesses that x and y are equal. For instance, this type could be inhabited, or it could be empty.

If in blackboard mathematics we would prove that x = y, in Agda we exhibit a value of type x ≡ y.

The following three lines set up these types:

infix  _≡_
data _≡_ {X : Set} : X → X → Set where
  refl : {a : X} → a ≡ a

Example: Our first identities

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProgrammingBasics.DependentFunctions

With the definition of equality at hand, we can state and prove that zero equals zero:

zero-equals-zero : zero ≡ zero
zero-equals-zero = refl

In exactly the same fashion, we can state and prove that two + two equals four:

grande-teorema : two + two ≡ four
-- fully parenthesized as follows: grande-teorema : ((two + two) ≡ four)
grande-teorema = refl

We can use refl in exactly those situations, where the two sides of the alleged identity are manifestly equal, i.e. equal in a way which just requires unfolding all definitions and simplifying by computation, but no actual insights, to become convinced of the equality.

For instance, as zero + b equals b by definition, refl can be used in the following proof:

trivial : (b : ℕ) → zero + b ≡ b
-- fully parenthesized: lemma : (b : ℕ) → ((zero + b) ≡ b)
trivial b = refl

This piece of code can (as all pieces of Agda code!) be both read in a logical and in a computational sense:

(logical reading)
“lemma” is the result that for every number b, zero + b equals b.

(computational reading)
“lemma” is a function which reads as input a number b, and outputs a witness that zero + b equals b.

It is also true that a + zero equals a. However, this identity does not hold by definition; instead it requires a nontrivial (inductive) argument. For this reason, Agda rejects refl in the following attempt:

nontrivial : (a : ℕ) → a + zero ≡ a
nontrivial a = refl
-- ERROR:
-- a + zero != a of type ℕ
-- when checking that the expression refl has type a + zero ≡ a

Example: One not zero

It is not the case that one equals zero. And indeed, the hole in the following piece of Agda code cannot be filled:

outrageous : one ≡ zero
outrageous = ?

It is instructive to understand why this is the case. At the end of the day, for constructing an inhabitant of the type one ≡ zero, we will need to use a constructor of this type. But the only constructor is refl. This constructor only provides us with elements of types of the for x ≡ x, where the two sides are literally the same. But succ zero is (by definition) a freshly-minted new natural number, distint from zero.

The only way to fill in this hole would be to change the definition of ≡. For instance, we could add a constructor bailout:

data _≡'_ {X : Set} : X → X → Set where
  refl    : {x   : X} → x ≡' x
  bailout : {x y : X} → x ≡' y

outrageous' : one ≡' zero
outrageous' = bailout

Exercise: Predecessor of successor

Prove that the predecessor of a successor of a number is the original number again.

lemma-pred-succ : (a : ℕ) → pred (succ a) ≡ a
lemma-pred-succ a = {!!}

Unit tests

If a definition is not used in the remainder of a development, Agda supports giving it the reusable dummy name “_”. This feature is used in the Agda community to document expected results as rigorously verified unit tests, instead of merely putting examples in comments.

_ : twice two ≡ four
_ = refl