Agda中命题相等性函数实现问题：通用测试与函数相等性判定

1. Agda中相等测试的实现方式 #

Agda没有内置的通用布尔相等判定函数，必须为每个数据类型单独定义对应的判定逻辑——这是因为相等测试依赖于数据类型的构造子结构，不同类型的遍历、匹配规则完全不同。

比如自然数的相等测试，就像你在标准库中看到的那样，通过递归匹配构造子实现：

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

除了布尔值结果的判定函数，Agda标准库还提供了可判定相等的类型Dec (_≡_ a b)，它同时返回布尔结果和对应的证明：若相等则携带refl证明，若不等则携带不等的证明。比如自然数的_≟_：

_≟_ : (m n : ℕ) → Dec (m ≡ n)
zero  ≟ zero  = yes refl
suc n ≟ suc m with n ≟ m
... | yes p = yes (cong suc p)
... | no ¬p = no (λ ())
zero  ≟ suc n = no (λ ())
suc n ≟ zero  = no (λ ())

这种可判定相等比单纯的布尔函数更实用，因为它能在证明中复用。

2. 函数间的相等性测试是否可行 #

直接定义函数相等的布尔判定函数，或者像你描述的“判断_op_ ≡ _+_返回42”，在Agda核心语言中是不可行的，原因如下：

• Agda默认的命题相等_≡_是内涵相等：要求两个函数的定义在语法上（或通过β-归约等转换后）完全一致，但函数没有像数据类型那样的构造子可以遍历匹配，无法通过递归或模式匹配来判定这种相等。
• 即使使用外延相等（即两个函数对所有输入的结果都相等则视为相等），这需要引入公理（比如Function.Extensionality），但依然无法构造布尔判定函数——因为要验证所有输入的结果相等，这对于无限类型（比如ℕ）来说是不可能有限完成的。

如果一定要实现类似的逻辑，只能通过将函数编码为数据类型的方式间接实现。比如预先把需要判断的算子定义为数据构造子，再映射到对应的函数：

data ArithOp : Set where
  Add : ArithOp
  Mul : ArithOp
  Sub : ArithOp

opToFun : ArithOp → ℕ → ℕ → ℕ
opToFun Add = _+_
opToFun Mul = _*_
opToFun Sub = λ m n → m ∸ n

test : ArithOp → ℕ
test Add = 42
test op = 3 `opToFun` 4

但这本质上是对数据类型构造子的判断，不是直接对函数本身的相等性测试。

内容的提问来源于stack exchange，提问作者Sam_W