Agda standard library - why are more properties not marked abstract?

Question

Having been working in Agda for the last few months, I've just come across the abstract block in Agda which prevents further normalisation of the term outside the scope of the block.

Using it to hide the workings of my lemmas has greatly reduced the time required to type-check my programs. Looking through the Agda Standard Library however abstract is barely used. It seems to me that almost everything within any Properties file (for instance Data.Nat.Properties) could be within an abstract block, as I can't think of a use for reasoning about, for example, how addition is proved to be commutative.

Is this a case of abstract being a new feature which hasn't made its way into the standard library? Or is there some subtlety or downside of marking proofs abstract that I'm missing?

Answer 1

abstract is for abstract things, it blocks computation, so if you place proofs in an abstract block, you won't be able to use them in subst or rewrite while still retaining canonicity:

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

I.e. an abstract block has the same effect as a postulate block.

If you replace abstract with module _ where, the file will type check.

Andreas Abel wrote:

I think this "abstract" feature is little understood. We should schedule it for removal, giving a grace period of say 5 years. If no one has a written a technical paper about it until 2020, with a proper semantics and a description of its intended interaction with metas, we drop it.