agda - Agda 中的非平凡否定

Question

我看到的所有否定，即 A -> Bottom in agda 形式的结论都来自荒谬的模式匹配。还有其他情况可以在agda中获得否定吗？依赖类型理论中是否还有其他可能的情况？

Answer 1

类型理论通常没有模式匹配的概念(以及扩展的荒谬模式)，但它们可以证明您所描述的那种否定。

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

消除规则看起来有点像折叠(至少对于正数类型)。例如，下面是自然数的消除规则在 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 : ∀ n → suc n ≡ zero → ⊥

但是，其中涉及到一个技巧(事实上，它非常关键；在 Martin-Löf 的没有宇宙的类型理论中，如果没有这个技巧，您将无法做到，请参阅 this paper)。我们需要构造一个函数，该函数将根据其参数返回两种不同的类型:

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 falso quodlibet)。在 Agda 中，我们显然有:

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

但事实证明，这恰恰是⊥的消除器，所以在类型论中定义这个类型的时候就给出了。