由于 Agda 是直觉的,因此必须假设排中律。但据我所知,直觉逻辑接受ex falso quodlibet 或爆炸原理(一切都源于荒谬的定理)。如何证明这一假设:
data ⊥ : Set where
postulate exp : ∀ {n} {x : Set n} → ⊥ → x
最佳答案
可以证明爆炸的原理如下
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 将产生上面给出的最终结果。
关于agda - 证明Agda中的爆炸原理,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/48030607/