主页 / coding / 问题 / 77674687
Accepted
lemongyros
Asked: 2023-12-17 22:02:17 +0800 CST

Agda 证明 Bool ≢ ⊤

  • 772

所以这是我在家庭作业中遇到的问题，我必须证明 bool 不等于 top，而且我必须使用一个重新定义的等号。

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 _≡_

-- define conversion between the two 'equals'
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

-- prove properties of ≡

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))

-- types
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≠⊤ = {!!}

我尝试了类似的方法，但是我无法成功：/无法创建 Set -> Set 谓词


⊤≠⊥ : ⊤ ≢ ⊥ 
⊤≠⊥ 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) = ⊥
functional-programming

2 个回答

  1. Best Answer

    在 Agda 中证明两个集合不同的唯一方法是利用它们在基数方面的差异。

    Bool在和 的情况下⊤，这特别容易利用，因为 的每个元素⊤都等于它的每个其他元素，但对于Bool(true不等于false) 来说则不然。因此你需要的是

    Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ x with sym x (λ A -> (x y : A) -> x ≡ᵣ y) (λ _ _ -> reflᵣ) true false
... | ()
    • 1

  2. 第一步是考虑一个谓词，P : Set → Set这样它P Bool是存在的并且P ⊤是可反驳的，反之亦然。阿格达不会给你太多帮助来选择一个好的，因为它Set → Set是一种非常模糊的类型，有很多居民（其中大多数对你来说毫无用处）。我将把这个选择P主要作为练习，但给出一些提示，因为我想找到这样的 aP是这个家庭作业问题的要点。

    事实上，我发现反之亦然更容易——选择P带有P ⊤“但是”的选项P Bool → ⊥。在生成这样的 时P，您通常会使用T : Setλ 抽象。这T将被实例化为⊤并由Bool的定义进行实例化_≡_。有了这样的T，您就可以使用 来普遍量化元素(x : T) → ...。如果您已经了解了 Σ 类型（依赖对），则可以将它们用于存在量化，尽管我最终发现了一个只需要通用量化的属性。由于尺寸问题，您无法用于_≡_生产所需的产品，但您可以在其位置使用。您无法对其居民进行模式匹配，因为它们不属于或Set_≡ᵣ_Tdatarecord类型。

    我需要一个引理true≢ᵣfalse : true ≡ᵣ false → ⊥。我通过荒谬的模式匹配 ( ()) 证明了这一点，但它也应该通过untransp定义布尔值的属性来证明，该true属性的 true 和 false false。这个属性更容易定义，因为它的类型是Bool → Set，因此您可以对参数进行模式匹配Bool。

    结果证明应如下所示。我建议从 just 开始true≢ᵣfalse ?，然后填写Pand p，然后它会告诉您应该采用多少个参数sym q P p。

    Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ q = true≢ᵣfalse (sym q P p {- instantiation of universal quantifiers -})
  where
  P : Set → Set
  P T = ?

  p : P ⊤
  p = ?
    • 0

相关问题