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

Question

是否有可能定义一个简单的相等的句法概念(类似于GHC可能自动派生为EqHaskell 98类型的实例),而无需明确证明每个数据构造函数是单射的,或者做类似的事情,例如定义撤销每个构造函数和使用cong？

换句话说,是否有可能更直接地利用数据构造函数的注入性,而不是必须为每个构造函数引入一个辅助函数？

以下以自然数为例.

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 的Agda 前奏包含一种自动导出给定数据类型的可判定相等性的机制。该代码基于Agda的反射机制，并自动生成扩展lambda来证明构造函数的单射性。我建议看一下代码，尽管它并不总是那么简单。