没有明确证明数据构造函数是单射的平等测试

Question

是否可以定义一个简单的相等句法概念(类似于 GHC 可能自动派生为 Haskell 98 类型的 Eq 实例)，而无需明确证明每个数据构造函数是单射的，或做类似的事情，例如定义每个构造函数的撤回并使用 cong ?

换句话说，是否可以更直接地利用数据构造函数的注入(inject)性，而不是为每个构造函数引入一个辅助函数？

下面以自然数为例。

module Eq where

   open import Function
   open import Relation.Binary
   open import Relation.Binary.PropositionalEquality
   open import Relation.Nullary

   data ℕ : Set where
      zero : ℕ
      suc : ℕ → ℕ

   -- How to eliminate these injectivity proofs?
   suc-injective : ∀ {n m} → suc n ≡ suc m → n ≡ m
   suc-injective refl = refl

   _≟_ : Decidable {A = ℕ} _≡_
   zero ≟ suc _ = no (λ ())
   suc _ ≟ zero = no (λ ())
   zero ≟ zero = yes refl
   suc n ≟ suc m with n ≟ m
   suc n ≟ suc .n | yes refl = yes refl
   ... | no n≢m = no (n≢m ∘ suc-injective)

可以替换 suc-injective通过 cong (λ { zero → zero ; (suc x) → x }) ，即通过定义一个反转 suc 的函数，但这仍然需要每个构造函数的一个辅助函数的样板，并且由于需要全部，因此定义这些函数有些难看。

(通常需要注意的是缺少一些明显的东西。)

Answer 1

Ulf Norell 的 prelude for Agda包含一种为给定数据类型自动推导可判定相等性的机制。该代码基于 Agda 的反射机制，并自动生成扩展的 lambda，用于证明构造函数的注入(inject)性。我建议看一下代码，尽管它并不总是尽可能简单。