logic - 如何在 Agda 中证明 `theorem : ¬ ⊤ ≡ ⊥`？

Question

沿着 The Haskell Road to Logic, Maths and Programming，你可以找到第 48 页 定理 2.12.1 ¬ ⊤ ≡ ⊥和它的反面 ¬ ⊥ ≡ ⊤
本书使用 Haskell 并假设

⊥ = False

⊤ = True

这将产生 Agda 类型 theorem : (p q : Bool) → not p ≡ q通过 refl 证明这是微不足道的.

但是，不假设 1 和 2 就可以证明原始定理吗？

试

-- from software foundations (https://plfa.github.io/Negation/)
postulate
  excluded-middle : ∀ {A : Set} → A ⊎ ¬ A

theorem : ¬ ⊤ ≡ ⊥
theorem x = {!!}

当然没有解决方案，因为我们不能构造 ⊥ ，所以我猜需要一个反证法？另外，我是否正确，这假设了排中律，因此需要作为附加假设？

Agda 说:

I'm not sure if there should be a case for the constructor refl, because I get stuck when trying to solve the following unification problems (inferred index ≟ expected index): ⊤ ≟ ⊥ when checking that the expression ? has type ⊥

谢谢!

Answer 1

这在没有假设的普通 Agda 中是可以证明的。解决方案是⊤ ≡ ⊥允许我们转任何证明 ⊤成⊥的证明.

open import Data.Unit
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

theorem : ¬ (⊤ ≡ ⊥)
theorem eq = subst (λ A → A) eq tt