如何在 Agda 中证明`定理：¬ ⊤ ≡ ⊥`？

Question

遵循Haskell逻辑、数学和编程之路，可以找到第 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 = {!!}

当然没有解，因为我们不能构造⊥，所以我想需要反证法？另外，我是否正确认为这假定了排中律，因此需要将其作为附加假设？

阿格达说：

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

Answer 2

如果 ¬ ⊤ ≡ ⊥ 是 ¬ (⊤ ≡ ⊥)，那么@Andras Kovacs 对 ¬ ⊤ ≡ ⊥ 和 ¬ ⊥ ≡ ⊤ 都适用。如果 ¬ ⊤ ≡ ⊥ 是 (¬ ⊤) ≡ ⊥，则证明需要类型相等。通常你应该对 ¬ ⊤ 和 ⊥.

之间存在同构的证明没问题

(¬ ⊤) ≡ ⊥ 的证据表明 ¬ ⊤ 无人居住。

(¬ ⊥) ≡ ⊤ 的证明基本上确立了 ¬ ⊥ 只有一个函数 id 的事实（因此与包含单个元素的所有类型同构）。

以下所有内容都可以使用一些标准的 Agda 函数构造，但这里需要大量自给自足的定义来证明此类同构的存在。注意 False 和 True 是类型，不是布尔值。此外，需要外延性公理才能证明第二定理，因为 ¬ ⊥ 是一个函数。

data False : Set where

data True : Set where
  tt : True

data _==_ {A : Set} (x : A) : A -> Set where
   refl : x == x

false-elim : {A : Set} -> False -> A
false-elim ()

id : {A : Set} -> A -> A
id x = x

const : {A B : Set} -> B -> A -> B
const x _ = x

ap : {A B : Set} -> (A -> B) -> A -> B
ap = id

ap' : {A B : Set} -> A -> (A -> B) -> B
ap' x f = f x

infixl 4 _==_

data Isomorphism {A B : Set} (f : A -> B) (g : B -> A) : Set where
   iso : ((x : B) -> f (g x) == id x) ->
         ((x : A) -> g (f x) == id x) -> Isomorphism f g

Not : Set -> Set
Not A = A -> False

not-True-iso-False : Isomorphism (ap' tt) false-elim
not-True-iso-False = iso (\x -> false-elim {ap' tt (false-elim x) == id x} x)
                         \not-true -> false-elim (not-true tt)

-- extensionality: if functions produce equal results for all inputs, then the functions are equal
postulate ext : {A B : Set} -> (f g : A -> B) -> ((x : A) -> f x == g x) -> f == g

not-False-iso-True : Isomorphism {Not False} {True} (const tt) (const id)
not-False-iso-True = iso is-true is-not-false where
   is-true : (x : True) -> const tt (const {True} (id {Not False})) == id x
   is-true tt = refl
   is-not-false : (x : Not False) -> const id (const {Not False} tt) == id x
   is-not-false x = ext (const id (const {Not False} tt)) x \()

现在，如果我们定义_==_任何层次的类型宇宙，那么我们就可以引入关于类型相等性的公理：如果两个类型具有同构性，那么它们是相等的。

open import Agda.Primitive
data _==_ {a : Level} {A : Set a} (x : A) : A -> Set a where
   refl : x == x

postulate iso-is-eq : {A B : Set} {f : A -> B} {g : B -> A} ->
                      Isomorphism f g -> A == B

not-True-is-False : (Not True) == False
not-True-is-False = iso-is-eq not-True-iso-False

not-False-is-True : (Not False) == True
not-False-is-True = iso-is-eq not-False-iso-True

如何在 Agda 中证明`定理：¬ ⊤ ≡ ⊥`？

How to prove `theorem : ¬ ⊤ ≡ ⊥` in Agda?

logic

proof

agda