Agda中的非平凡否定

类型理论通常没有模式匹配的概念（并且扩展到荒谬的模式），但是它们可以证明您所描述的类型的否定。

首先，我们必须查看数据类型。如果没有模式匹配，则可以通过引入和消除规则来表征它们。引入规则基本上是构造函数，它们告诉您如何构造该类型的值。另一方面，消除规则告诉您如何使用该类型的值。也有相关的计算规则（β约简，有时是η约简），但是我们现在不需要处理这些规则。

消除规则看上去有点像褶皱（至少对于正数类型）。例如，以下是自然数的消除规则在Agda中的样子：

ℕ-elim : ∀ {p} (P : ℕ → Set p)
  (s : ∀ {n} → P n → P (suc n))
  (z : P 0) →
  ∀ n → P n
ℕ-elim P s z zero    = z
ℕ-elim P s z (suc n) = s (ℕ-elim P s z n)

尽管Agda确实有介绍规则（构造函数），但没有淘汰规则。相反，它具有模式匹配，并且如您在上面所看到的，我们可以使用它来恢复消除规则。但是，我们也可以相反：我们可以使用消除规则来模拟模式匹配。实话实说，这通常会更加不便，但是可以做到-上面提到的消除规则基本上是在最外层构造函数上进行模式匹配，如果需要更深入的研究，我们可以再次应用消除规则。

因此，我们可以模拟模式匹配。那荒谬的模式呢？例如，我们将采用第四个Peano公理：

peano : ∀ n → suc n ≡ zero → ⊥

但是，这涉及到一个技巧（实际上，这非常关键；在没有宇宙的马丁·洛夫类型理论中，没有技巧就无法做到这一点，请参见本文）。我们需要构造一个函数，该函数将根据其参数返回两种不同的类型：

Nope : (m n : ℕ) → Set
Nope (suc _) zero = ⊥
Nope _    _       = ⊤

如果为m ≡ n，我们应该能够证明Nope m n持有（有人居住）。确实，这很容易：

nope : ∀ m n → m ≡ n → Nope m n
nope zero    ._ refl = _
nope (suc m) ._ refl = _

现在，您可以看到前进的方向。如果我们将应用于nope的“不良”证明suc n ≡ zero，Nope (suc n) zero则将减少为⊥，我们将获得所需的功能：

peano : ∀ n → suc n ≡ zero → ⊥
peano _ p = nope _ _ p

现在，您可能会注意到我有点作弊。我使用过模式匹配，即使我之前说过这些类型理论都不是模式匹配附带的。我将在下一个示例中对此进行补救，但是我建议您尝试证明peano数字上没有模式匹配（使用ℕ-elim上面给出的）；如果您真的想要一个硬核版本，则也不要在相等性上进行模式匹配，而应使用此消除器：

J : ∀ {a p} {A : Set a} (P : ∀ (x : A) y → x ≡ y → Set p)
  (f : ∀ x → P x x refl) → ∀ x y → (p : x ≡ y) → P x y p
J P f x .x refl = f x

另一个流行的荒谬模式是某种类型的Fin 0（从此示例中，您将了解如何模拟其他此类荒谬的匹配）。因此，首先，我们需要消除Fin。

Fin-elim : ∀ {p} (P : ∀ n → Fin n → Set p)
  (s : ∀ {n} {fn : Fin n} → P n fn → P (suc n) (fsuc fn))
  (z : ∀ {n} → P (suc n) fzero) →
  ∀ {n} (fn : Fin n) → P n fn
Fin-elim P s z fzero    = z
Fin-elim P s z (fsuc x) = s (Fin-elim P s z x)

是的，类型真的很丑。无论如何，我们将使用相同的技巧，但是这次，我们只需要依赖一个数字即可：

Nope : ℕ → Set
Nope = ℕ-elim (λ _ → Set) (λ _ → ⊤) ⊥

请注意，这等效于：

Nope zero    = ⊥
Nope (suc _) = ⊤

现在，请注意，这两种情况对上述消除（即s和z的情况下）一些回报型的P (suc n) _。如果选择P = λ n _ → Nope n，则⊤两种情况下都必须返回某种类型的东西-但这很简单！确实，这很容易：

bad : Fin 0 → ⊥
bad = Fin-elim (λ n _ → Nope n) (λ _ → _) _

您可能想知道的最后一件事是我们如何从中获取任何类型的值⊥（在逻辑上称为ex quodlibet）。在阿格达，我们显然有：

⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
⊥-elim ()

但是事实证明，这恰恰是的消除器⊥，因此在类型理论中定义此类型时会给出它。