Agda：将声明与定义分开

Question

我正在 Agda 中证明一些东西，我的一些文件开始变得有点长和混乱（即使在我重构为更小的模块之后）。是否可以有两个文件，其中一个只包含定理的类型签名，另一个包含那些定理和证明？我查看了 abstract 关键字，但这似乎不太正确。

当然，我可以把所有的类型签名放在文件的顶部，把所有的证明放在文件的底部；但如果我可以将文件中的语句单独保存起来似乎更干净。

Answer 1

您可以为引理的类型命名。例如。在文件 Statement.agda:

module Statement where

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

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

并且在文件 Proof.agda 中：

module Proof where

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

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

如果您的定义是多态的，很遗憾，Agda 没有 ∀ {ℓ : Level} → ... 形式的类型的（表面）名称。当使用 Proof 中的语句时，您必须将级别作为 Statement 中的参数并对其进行普遍量化。这会给你这样的东西：

在Statement.agda中：

open import Agda.Primitive

data ⊥ : Set where

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

在Proof.agda中：

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

Agda: separate declaration from definition