Agda作业：证明Bool ≢ ⊤（使用自定义等价关系）

问题说明 #

需证明Bool类型与⊤类型不等价（即Bool ≢ ⊤），且必须使用代码中自定义的_≡_等价关系（命题外延性风格的等价定义）。核心难点是构造合适的Set→Set谓词，通过等价关系的替换性导出矛盾。

完整代码框架 #

module TranspEq where

open import Agda.Primitive
open import Agda.Builtin.Equality renaming (_≡_ to _≡ᵣ_ ; refl to reflᵣ)
open import Agda.Builtin.Nat renaming (Nat to ℕ)

_≡_ : ∀{ℓ}{A : Set ℓ} → A → A → Setω
_≡_ {A = A} a b = ∀{κ}(P : A → Set κ) → P a → P b

infix 4 _≡_

-- 自定义等价与内置等价的转换
transp : ∀{ℓ}{A : Set ℓ}(a b : A) → a ≡ b → a ≡ᵣ b
transp a b x = x (_≡ᵣ_ a) reflᵣ

untransp : ∀{ℓ}{A : Set ℓ}(a b : A) → a ≡ᵣ b → a ≡ b
untransp a .a reflᵣ P y = y

-- 自定义等价的性质证明
refl : ∀{ℓ}{A : Set ℓ}{a : A} → a ≡ a
refl P a = a

sym : ∀{ℓ}{A : Set ℓ}{a b : A} → a ≡ b → b ≡ a
sym {l} {A} {a} {b} = λ z P → z (λ z₁ → (x : P z₁) → P a) (λ x → x)

trans : ∀{ℓ}{A : Set ℓ}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans = λ a b P c → b P (a P c)

cong : ∀{ℓ κ}{A : Set ℓ}{B : Set κ}(f : A → B){a b : A} → a ≡ b → f a ≡ f b
cong = λ f a P → a (λ b → P (f b))

-- 基础类型定义
record ⊤ : Set where
  instance constructor tt

data Bool : Set where
  true : Bool
  false : Bool

data ⊥ : Set where

_≢_ : ∀{ℓ}{A : Set ℓ} → A → A → Setω
a ≢ b = a ≡ b → ⊥

-- 需要完成的证明
Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ = {!!}

用户尝试片段 #

⊤≠⊥ : ⊤ ≢ ⊥ 
⊤≠⊥ x = x (λ x → x) tt
 

Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ x = ⊤≠⊥ λ P y → {!   !}
--Bool≠⊤ : Bool ≢ ⊤
--Bool≠⊤ x = x (λ y → y tt) p
--    where
--    p : {Set : (Bool ≡ ⊤)}→ ⊥
--    p (true ≡ tt) = ⊥
--    p (false ≡ tt) = ⊥

解决方案 #

核心思路是构造一个区分Bool和⊤的谓词：利用Bool存在两个不同元素、而⊤仅含唯一元素的特性，通过等价关系的替换性导出矛盾。

补充完整的证明代码如下：

-- 先证明Bool的两个元素不等价
true≢false : true ≡ᵣ false → ⊥
true≢false ()

-- 定义谓词：类型X是否存在两个不同的元素
has-two-distinct : Set → Set
has-two-distinct X = Σ X (λ x → Σ X (λ y → x ≡ᵣ y → ⊥))

-- Bool满足该谓词
Bool-has-two : has-two-distinct Bool
Bool-has-two = true , false , true≢false

-- ⊤不满足该谓词（导出矛盾）
⊤-no-two : has-two-distinct ⊤ → ⊥
⊤-no-two (tt , tt , contra) = contra reflᵣ

-- 最终证明Bool ≢ ⊤
Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ eq = ⊤-no-two (eq has-two-distinct Bool-has-two)

证明逻辑：

1. 若Bool ≡ ⊤（即eq成立），根据自定义等价的定义，eq has-two-distinct会将has-two-distinct Bool转换为has-two-distinct ⊤。
2. 我们已知Bool-has-two是has-two-distinct Bool的实例，代入后得到has-two-distinct ⊤的实例。
3. 但⊤-no-two证明了has-two-distinct ⊤必然导出⊥，由此矛盾得证Bool ≢ ⊤。

内容的提问来源于stack exchange，提问作者lemongyros