Agda標準ライブラリ - より多くのプロパティが抽象的なマークされていないのはなぜですか？

Question

ここ数ヶ月間Agdaで働いていたので、Agdaのabstractブロックを訪れ、ブロックの範囲外の用語の正規化をさらに防止しました。

私の補題の動作を隠すためにそれを使用すると、が大幅に私のプログラムのタイプチェックに必要な時間が短縮されました。しかし、Agda標準ライブラリを見ると、abstractはほとんど使用されていません。 Propertiesファイル（たとえばData.Nat.Properties）内のほぼすべてが、abstractブロック内にある可能性があります。たとえば、加算が可換性であることが証明されているなど、推論の用途を考えることはできません。

これは、抽象概念が標準ライブラリに移行していない新しい機能であるケースですか？それとも、私が紛失している証拠を捺印することの微妙な点や弱点がありますか？abstractあなたはabstractブロック内の証明を配置する場合、あなたはまだ規範性を保持しつつ、substまたはrewriteでそれらを使用することができなくなりますので

Answer 1

abstractは、抽象的なもの、それはブロックの計算のためのものです：

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をに置き換えると、ファイルにチェックが入力されます。

アンドレアス・アベルwrote：

私は、この "抽象" 機能が少し理解されていると思います。我々は を5年間の猶予期間を与えて削除するようにスケジュールする必要があります。 に、2020年までの技術論文があり、 の適切なセマンティクスと メタとの意図した相互作用の説明がある場合は、それを削除します。