agda - 证明Agda中的爆炸原理

Question

由于 Agda 是直觉的，因此必须假设排中律。但据我所知，直觉逻辑接受ex falso quodlibet 或爆炸原理(一切都源于荒谬的定理)。如何证明这一假设:

  data ⊥ : Set where

  postulate exp : ∀ {n} {x : Set n} → ⊥ → x

Answer 1

可以证明爆炸的原理如下

  data ⊥ : Set where

  exp : ∀ {n} {x : Set n} → ⊥ → x
  exp ()

如果不知道如何证明这一点，可以从一个洞开始:

  data ⊥ : Set where

  exp : ∀ {n} {x : Set n} → ⊥ → x
  exp absurd = {! !}

然后，在 emacs agda2-mode 中，可以按 C-c C-l 进行类型检查，这样孔就会被替换，emacs 就会显示目标。在这种情况下，目标是 .x 类型。然后可以单击该孔并按 C-c C-c 并键入 absurd 以将此函数拆分为变量 absurd。 Emacs 将产生上面给出的最终结果。