Agda: Function for Propositional Equality

Question

I have been working my way through Programming Language Foundations in Agda, and currently I'm up to "Decidable: Booleans and decision procedures". It seems that, at least for the example given in detail, a function for deciding if something is true is similar in structure to a proof object that demonstrates why it is true. Specifically the proof type

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n : ℕ} → zero ≤ n
  s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n

has the same structure as the decision function

_≤ᵇ_ : ℕ → ℕ → Bool
zero ≤ᵇ n       =  true
suc m ≤ᵇ zero   =  false
suc m ≤ᵇ suc n  =  m ≤ᵇ n

except that the latter has an additional case because it needs to work when the answer is false while the former only needs to work when the answer is true.

But this similarity seems not to hold in the case of propositional equality. The proof that a value is equal to itself is written refl for any type whatsoever -- as I understand it the difficult work is done for us by the type checker which reduces everything to canonical form on our behalf. However as far as I can tell (please correct me if I'm wrong) a function

_≡ᵇ_ : {A : Set} → A → A → Bool

that decides equality for values of an arbitrary type is not definable in Agda.

My question is twofold:

1. How is testing for equality generally implemented? Is a separate function defined for each datatype?
2. In particular is there any way to define a test for equality between functions? Say I want to define a function that takes as an argument a binary operator _op_ : ℕ → ℕ → ℕ and returns 42 if _op_ ≡ _+_ and 3 op 4 otherwise. This would seem to require a way to test for equality of functions but I can't work out how to do so. Is such a thing possible?

Checking the standard library I notice that equality testing for ℕ is defined as

_==_ : Nat → Nat → Bool
zero  == zero  = true
suc n == suc m = n == m
_     == _     = false

which suggests that the answer to my first question is that a separate equality function is indeed defined for each datatype as I thought. I haven't found anything that suggests an answer to my second question.

Answer 1

In the chapter on Isomorphism in the PLFA book, equality of function is postulated via extensionality: Two functions can be considered equal, if they produce the same result for all inputs. Using extensionality, to prove the equality of two functions (or not), you can only invoke one of the following to obtain the desired result:

open import Data.Nat.Base using (ℕ; _+_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
open import Data.Sum using (_⊎_; inj₁; inj₂)

foo : (op : ℕ → ℕ → ℕ) → {(op ≡ _+_) ⊎ (op ≢ _+_)} → ℕ
foo _op_ {inj₁  eq} = 42
foo _op_ {inj₂ neq} = 3 op 4

-- Test call with +
foo+ : foo _+_ {inj₁ refl} ≡ 42
foo+ = refl

So function foo takes such a binary operator as input as well as either a proof of equality to _+_ or inequality to _+_. I made the proof an implicit argument here so Agda might be able to infer a value by itself. However, this did not work when I tried it with foo+ above.

I do not think that it is possible to write this function without taking proofs as a parameter because then the proofs would have to be computed within the function itself, probably during runtime which is hardly automatable.

I hope this helps. :)