沿着 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 ⊥
谢谢!
最佳答案
这在没有假设的普通 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
关于logic - 如何在 Agda 中证明 `theorem : ¬ ⊤ ≡ ⊥`?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/58906691/