Agda-Standardbibliothek - Warum werden mehr Eigenschaften nicht als abstrakt markiert?

Question

Nachdem ich in den letzten Monaten in Agda gearbeitet habe, bin ich gerade auf den Block abstract in Agda gestoßen, der eine weitere Normalisierung des Begriffs außerhalb des Bereichs des Blocks verhindert.

Verwenden, um die Funktionsweise meiner Lemmas zu verbergen hat stark reduziert die Zeit erforderlich, um meine Programme zu überprüfen. Wenn man durch die Agda Standard Library schaut, wird abstract kaum benutzt. Es scheint mir, dass fast alles innerhalb einer Properties Datei (zum Beispiel Data.Nat.Properties) innerhalb eines abstract Blocks sein könnte, da ich nicht an eine Verwendung denken kann, zum Beispiel darüber, wie sich die Addition als kommutativ erweist.

Ist das ein Fall, in dem Abstrakt ein neues Feature ist, das nicht in die Standardbibliothek gelangt ist? Oder gibt es eine gewisse Subtilität oder einen Nachteil bei der Markierung von Beweisen abstract, die ich vermisse?

Answer 1

abstract ist für abstrakte Dinge, blockiert es Berechnung, also wenn Sie Beweise in einem abstract Block platzieren, Sie werden sie nicht noch in subst oder rewrite der Lage sein, zu verwenden, während canonicity Halte:

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 

D.h. Ein abstract Block hat die gleiche Wirkung wie ein postulate Block. Wenn Sie abstract durch module _ where ersetzen, wird die Datei die Überprüfung durchführen.

Andreas Abel wrote:

Ich denke, das "abstrakt" Funktion ist nur wenig verstanden. Wir sollten Zeitplan für die Entfernung, mit einer Nachfrist von etwa 5 Jahren. Wenn man bis 2020 ein technisches Papier darüber geschrieben hat, mit einer richtigen Semantik und einer Beschreibung der beabsichtigten Interaktion mit Metas, wir lassen es fallen.