Equality of functions in Agda

A student fairly new to Agda recently asked me:

We've discussed that addition is defined by two properties;

• zero + n = n, and
• (suc n) + m = suc (n + m).

In Agda, can we prove a function is equal to addition if it satisfies these properties?

More generally, without knowledge of such properties, can we prove one function is equal to another?

Let's explore this topic a little bit. For simplicity, we'll restrict our attention to just unary and binary functions between natural numbers.

An important first step is deciding: what do we mean by “equal” when we say that “one function is equal to another”?

We will use the Agda standard library definitions of the natural numbers, addition, and propositional equality in this discussion, along with equational reasoning for proofs.

open import Data.Nat using (ℕ ; zero ; suc ; _+_)

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_ ; refl)
open Eq.≡-Reasoning using (begin_ ; _≡⟨⟩_ ; _≡⟨_⟩_ ; _∎)

Here we make use of the following definitions from the standard library.

open import Data.Nat using (ℕ ; zero ; suc ; _+_)
open import Data.Nat.Properties using (+-identityʳ)

open import Relation.Nullary using (¬_)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_ ; refl ; sym ; cong)
open Eq.≡-Reasoning using (begin_ ; _≡⟨⟩_ ; _≡⟨_⟩_ ; _∎)

For the purposes of this thought experiment, we will work with this Agda record.

record PseudoAddition : Set where
  field
    _⊕_ : ℕ → ℕ → ℕ
    z⊕n≡n : (n : ℕ) → zero ⊕ n ≡ n
    [suc-m]⊕n≡suc-[m⊕n] : (m n : ℕ) → (suc m) ⊕ n ≡ suc (m ⊕ n)

We call the record PseudoAddition, since we are claiming that the ⊕ operator is, in fact, addition, even though we do not have its definition. Practically speaking, this means we have as assumptions the existence of this ⊕ operator and the two properties describing its behaviour.

We could equivalently have made the fields parameters to this Agda module; in Agda, records define a module, so there's not much difference.

It's relatively simple to prove that our assumed ⊕ operator is extensionally equal to addition, given the properties zero ⊕ n ≡ n and m ⊕ n ≡ m + n. Enough so that we leave this as exercise to the reader. Make use of cong in the induction step; you'll probably need just two steps.

record PseudoAddition : Set where
  field
    _⊕_ : ℕ → ℕ → ℕ
    z⊕n≡n : (n : ℕ) → zero ⊕ n ≡ n
    [suc-m]⊕n≡suc-[m⊕n] : (m n : ℕ) → (suc m) ⊕ n ≡ suc (m ⊕ n)

  m⊕n≡m+n : (m n : ℕ) →  m ⊕ n ≡ m + n
  m⊕n≡m+n zero n = z⊕n≡n n
  m⊕n≡m+n (suc m) n =
    begin
      (suc m ⊕ n)
    ≡⟨ ??? ⟩
      suc (m + n)
    ∎

Let's take a short break here to see an actual use of our record; we can define an operator similar, but not quite equal to addition, and by providing proofs that it satisfies the two properties defining plus, the record provides us with a proof that our operator is extensionally equal to addition. (Note the connection between Agda records and Haskell-style typeclasses).

_+₀_ : ℕ → ℕ → ℕ
m +₀ n = m + n + 0

+₀-is-PseudoAddition : PseudoAddition
+₀-is-PseudoAddition =
  record { _⊕_ = _+₀_
         ; z⊕n≡n = +-identityʳ
         ; [suc-m]⊕n≡suc-[m⊕n] = λ _ _ → refl }

m+₀n≡m+n : (m n : ℕ) → m +₀ n ≡ m + n
m+₀n≡m+n = PseudoAddition.m⊕n≡m+n +₀-is-PseudoAddition

So, we can show prove that our operation is extensionally equal to addition. However, if we try to prove

  ⊕≡+ : _⊕_ ≡ _+_
  ⊕≡+ = ???

we will find we cannot. (Note we cannot disprove it either).

In fact, even if we know the definition of the operator, and that definition is exactly the same as that of addition, as in

_plus_ : ℕ → ℕ → ℕ
zero  plus n = n
suc m plus n = suc (m plus n)

we still cannot prove it is intensionally equal to addition.

Why not!?

A post by Peter Selinger on the Agda mailing list sheds some light on the situation. Specifically, he sums up the situation as

…function equality in Agda is definitional equality, i.e., two functions are equal if and only if they are internally represented as pointers to the same closure.

Given what we've seen above with ⊕ and addition, we can conclude this about checking equality of functions in Agda:

• We can, given enough information, prove that two functions are extensionally equal to each other (x : A → f x ≡ g x).
• Only in special cases can we say that two functions are intensionally equal (f ≡ g).
  • Specifically, when both are actually the same (f ≡ f) or when one is an abbreviation of the other (defined without pattern matching).

To round out this discussion, let's consider the negative case; when can we say, in Agda, that two functions are not equal? And can we prove they are not intensionally equal, or only that they are not extensionally equal?

Actually, we can do both. And in general, whenever we prove that two functions are not extensionally equal, we can prove that they are not intensionally equal. We prove this easily as a lemma.

disagree : {A B : Set} → {f g : A → B}
         → (witness : A) → ¬ (f witness ≡ g witness)
         → ¬ (f ≡ g)
disagree witness fw≢gw refl = fw≢gw refl

Now let us examine this specific instance dealing with pseudo-addition by considering two records, covering the two cases:

1. ⊕ does not satisfy zero ⊕ n ≡ n, for some witness n, and
2. ⊕ does not satisfy (suc m) ⊕ n ≡ suc (m ⊕ n), for some witnesses m and n.

In either case, we can prove by contradiction both

• that ⊕ is not extensionally equal to addition, and
• that ⊕ is not intensionally equal to addition.
  • Note: we prove these cases manually, not using disagree, because our assumptions reason only about ⊕, so are not of the correct shape (¬ m ⊕ n ≡ m + n) for disagree.

First, let's assume that zero ⊕ n is not n.

record NotAddition-zero : Set where
  field
    _⊕_ : ℕ → ℕ → ℕ
    nʷ : ℕ   -- witness
    ¬z⊕nʷ≡nʷ : ¬ (zero ⊕ nʷ ≡ nʷ)

  ¬a⊕b≡a+b : ¬ ((a b : ℕ) → a ⊕ b ≡ a + b)
  ¬a⊕b≡a+b a⊕b≡a+b = ¬z⊕nʷ≡nʷ (a⊕b≡a+b zero nʷ)

  ¬⊕≡+ : ¬ _⊕_ ≡ _+_
  ¬⊕≡+ ⊕≡+ = ¬z⊕nʷ≡nʷ z⊕n≡n
    where
      z⊕n≡n : zero ⊕ nʷ ≡ nʷ
      z⊕n≡n =
        begin
          zero ⊕ nʷ
        ≡⟨ cong (λ op → op zero nʷ) ⊕≡+ ⟩
          zero + nʷ
        ≡⟨⟩
          nʷ
        ∎

Now, let us assume that for some m and n, (suc m) ⊕ n is not suc (m ⊕ n).

record NotAddition-suc : Set where
  field
    _⊕_ : ℕ → ℕ → ℕ
    mʷ nʷ : ℕ   -- witnesses
    ¬[suc-mʷ]⊕nʷ≡suc-[mʷ⊕nʷ] : ¬ ((suc mʷ) ⊕ nʷ ≡ suc (mʷ ⊕ nʷ))

  ¬a⊕b≡a+b : ¬ ((a b : ℕ) → a ⊕ b ≡ a + b)
  ¬a⊕b≡a+b a⊕b≡a+b = ¬[suc-mʷ]⊕nʷ≡suc-[mʷ⊕nʷ] [suc-mʷ]⊕nʷ≡suc-[mʷ⊕nʷ]
    where
      [suc-mʷ]⊕nʷ≡suc-[mʷ⊕nʷ] : (suc mʷ) ⊕ nʷ ≡ suc (mʷ ⊕ nʷ)
      [suc-mʷ]⊕nʷ≡suc-[mʷ⊕nʷ] =
        begin
          (suc mʷ) ⊕ nʷ
        ≡⟨ a⊕b≡a+b (suc mʷ) nʷ ⟩
          (suc mʷ) + nʷ
        ≡⟨⟩
          suc (mʷ + nʷ)
        ≡⟨ cong suc (sym (a⊕b≡a+b mʷ nʷ)) ⟩
          suc (mʷ ⊕ nʷ)
        ∎

  ¬⊕≡+ : ¬ _⊕_ ≡ _+_
  ¬⊕≡+ ⊕≡+ = ¬[suc-mʷ]⊕nʷ≡suc-[mʷ⊕nʷ] [suc-mʷ]⊕nʷ≡suc-[mʷ⊕nʷ]
    where
      [suc-mʷ]⊕nʷ≡suc-[mʷ⊕nʷ] : (suc mʷ) ⊕ nʷ ≡ suc (mʷ ⊕ nʷ)
      [suc-mʷ]⊕nʷ≡suc-[mʷ⊕nʷ] =
        begin
          (suc mʷ) ⊕ nʷ
        ≡⟨⟩
          suc mʷ ⊕ nʷ
        ≡⟨ cong (λ op → op (suc mʷ)  nʷ) ⊕≡+ ⟩
          suc mʷ + nʷ
        ≡⟨⟩
          suc (mʷ + nʷ)
        ≡⟨ cong (λ op → suc (op mʷ nʷ)) (sym ⊕≡+) ⟩
          suc (mʷ ⊕ nʷ)
        ≡⟨⟩
          suc (mʷ ⊕ nʷ)
        ∎

The chapter on isomorphisms in Programming Language Foundations in Agda includes a discussion on adding the axiom of extensionality to Agda.

This document was written as a literate Agda file using Org mode, from which it was exported to (potentially several) formats. The original Org source code, with Agda code between the #+begin_src agda2 and #+end_src blocks, can be found here, along with the pure Agda code tangled from this file.