CODEWITHSUNDEEP
agda
Patrick Stevens
Patrick Stevens

Reputation: 579

Agda: separate declaration from definition

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.

Upvotes: 2

Views: 154

Answers (1)

gallais
gallais

Reputation: 12133

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 = {!!}

Upvotes: 2

Related Questions