Стандартная библиотека Agda - почему больше свойств не отмечено абстрактными?

Question

Работая в Agda в течение последних нескольких месяцев, я просто столкнулся с блоком abstract в Агда, который предотвращает дальнейшую нормализацию термина за пределами области действия блока.

Использование его для скрытия выработок моих лемм имеет значительно сократило время, необходимое для проверки типов моих программ. Просматривая стандартную библиотеку 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, файл напечатает чек.

Андреас Абель wrote:

Я думаю, что это "абстрактный" особенность малопонятным. Мы должны планировать его для удаления, предоставляя льготный период, например, 5 лет. Если нет , у вас есть письменная техническая документация об этом до 2020 года с правильной семантикой и описанием ее предполагаемого взаимодействия с metas, мы ее отбрасываем.