Agda: separate declaration from definition

Question

I'm proving stuff in Agda, and some of my files are starting to get a bit long and cluttered (even after I refactored into smaller modules). Is it possible to have two files, one of which contains type signatures of theorems only, and another which contains those theorems and proofs? I looked at the abstract keyword, but that doesn't quite seem to do the right thing.

Of course, I can put all the type signatures at the top of the file, and have all the proofs at the bottom of the file; but it seems cleaner if I could have the statements in a file to themselves.

Abstract definitions just behave as postulates to usually improve type-checking speed. You can just have all proofs in one file and add again the signatures in another file and set the proof to the proof synonym. This way you'll have one liner proofs. You can't skip the definition of a function in a file. — white_wolf

gallais gallais · Accepted Answer · 2018-06-16T15:26:48

You could give names to the types of your lemmas. E.g. in file Statement.agda:

module Statement where

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

+-sym : Set
+-sym = ∀ m n → m + n ≡ n + m

And in file Proof.agda:

module Proof where

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
import Statement

+-sym : Statement.+-sym
+-sym m n = {!!}

In case your definition is level-polymorphic, Agda unfortunately doesn't have a (surface) name for types of the form ∀ {ℓ : Level} → .... You will have to take the levels as arguments in Statement and quantify over them universally when using the statement in Proof. This would give you something like this:

In Statement.agda:

open import Agda.Primitive

data ⊥ : Set where

⊥-elim : (ℓ : Level) → Set (lsuc ℓ)
⊥-elim ℓ = ∀ {A : Set ℓ} → ⊥ → A

In Proof.agda:

⊥-elim : ∀ {ℓ} → Statement.⊥-elim ℓ
⊥-elim = {!!}

Agda: separate declaration from definition

1 Answers