Agda标准库 - 为什么更多属性没有标记为抽象？

Question

在过去的几个月里,我一直在Agda工作,我刚刚遇到了abstractAgda的这个区块,这阻止了该区域范围之外的进一步规范化.

使用它来隐藏我的引理的工作方式大大减少了对我的程序进行类型检查所需的时间.然而,浏览Agda标准库abstract几乎没有使用.在我看来,几乎所有Properties文件中的所有内容(例如Data.Nat.Properties)都可以在一个abstract块内,因为我无法想到用于推理的用法,例如,如何证明加法是可交换的.

这是一个抽象的案例,是一个尚未进入标准库的新功能吗？或者是否有一些abstract我遗漏的标记证明的微妙或缺点？

Answer 1

abstract是抽象的东西,它的块计算,因此,如果你把证据在abstract块,你将无法在使用它们subst或rewrite同时仍然保持正典:

module _ where

open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Base
open import Data.Fin hiding (_+_)

abstract
  +0 : ? n -> n + 0 ? n
  +0  0      = refl
  +0 (suc n) = cong suc (+0 n)

zero? : ? n -> Fin (suc n + 0)
zero? n = subst (Fin ? suc) (sym (+0 n)) zero

fail : zero? 2 ? zero
fail = refl

-- subst ((? {.x} ? Fin) ? suc) (sym (+0 2)) zero != zero of type Fin (suc 2 + 0)
-- when checking that the expression refl has type zero? 2 ? zero

即abstract块具有与块相同的效果postulate.

如果替换abstract为module _ where,则文件将键入check.

Andreas Abel 写道:

我认为这个"抽象"特征很少被理解.我们应该安排它去除,给予5年的宽限期.如果直到2020年没有人写过关于它的技术论文,并且有适当的语义和对与metas的预期交互的描述,我们放弃它.