如何定義單例集？

假設我有一個值x : A，我想定義一個只包含x的集合。如何定義單例集？

這是我的嘗試：

open import Data.Product 
open import Relation.Binary.PropositionalEquality 

-- Singleton x is the set that only contains x. Its values are tuples containing 
-- a value of type A and a proof that this value is equal to x. 
Singleton : ∀ {ℓ} {A : Set ℓ} → (x : A) → Set ℓ 
Singleton {A = A} x = Σ[ y ∈ A ] (y ≡ x) 

-- injection 
singleton : ∀ {ℓ} {A : Set ℓ} → (x : A) → Singleton x 
singleton x = x , refl 

-- projection 
fromSingleton : ∀ {ℓ} {A : Set ℓ} {x : A} → Singleton x → A 
fromSingleton s = proj₁ s

有沒有更好的辦法做到這一點？

爲什麼我要這樣的一個例子：如果你有過一些集合A幺半羣，那麼你就可以形成一個作爲唯一對象的類別。爲了在Agda中表達你的想法，你需要寫一個「只包含A的集合」。

來源

2014-01-25 Tobias Brandt

我認爲這是一個很好的方法來做到這一點。通常情況下，當你想創建一個類型的「子集」，它看起來像：

postulate 
    A : Set 
    P : A → Set 

record Subset : Set where 
    field 
    value : A 
    prop : P value

然而，這可能不是在這個意義上，它實際上可以包含比原來的類型更多的元素的子集。這是因爲prop可能有更多的命題上不同的值。例如：

open import Data.Nat 

data ℕ-prop : ℕ → Set where 
    c1 : ∀ n → ℕ-prop n 
    c2 : ∀ n → ℕ-prop n 

record ℕ-Subset : Set where 
    field 
    value : ℕ 
    prop : ℕ-prop value

突然間，該子集的元素數與原始類型相比增加了兩倍。我同意這個例子有點做作，但是可以想象，你在集合上有一個子集關係（來自集合論的集合）。這樣的事情其實是相當可能的：

sub₁ : {1, 2} ⊆ {1, 2, 3, 4} 
sub₁ = drop 3 (drop 4 same) 

sub₂ : {1, 2} ⊆ {1, 2, 3, 4} 
sub₂ = drop 4 (drop 3 same)

通常的方法解決這個問題是使用不相關的參數：

record Subset : Set where 
    field 
    value : A 
    .prop : P value

這意味着Subset類型的兩個值是相等的，如果他們有value，prop字段是無關到平等。事實上：

record Subset : Set where 
    constructor sub 
    field 
    value : A 
    .prop : P value 

prop-irr : ∀ {a b} {p : P a} {q : P b} → 
    a ≡ b → sub a p ≡ sub b q 
prop-irr refl = refl

但是，這更多的是一種指導，因爲你表示不存在這個問題。這是因爲在模式匹配阿格達的實施意味着公理ķ：

K : ∀ {a p} {A : Set a} (x : A) (P : x ≡ x → Set p) (h : x ≡ x) → 
    P refl → P h 
K x P refl p = p

那麼，這並不能告訴你太多。幸運的是，還有另一種屬性，它等同於公理K：

uip : ∀ {a} {A : Set a} {x y : A} (p q : x ≡ y) → p ≡ q 
uip refl refl = refl

這告訴我們，只有一個辦法，其中兩個元素可以是相等的，即refl（uip意味着獨特身份的樣張）。

這意味着當您使用命題相等來創建子集時，您將獲得一個真正的子集。

讓我們更加明確：

isSingleton : ∀ {ℓ} → Set ℓ → Set _ 
isSingleton A = Σ[ x ∈ A ] (∀ y → x ≡ y)

isSingleton A表達了A僅包含一個元素，最多propositonal平等的事實。事實上，Singleton x是一個單：

Singleton-isSingleton : ∀ {ℓ} {A : Set ℓ} (x : A) → 
    isSingleton (Singleton x) 
Singleton-isSingleton x = (x , refl) , λ {(.x , refl) → refl}

有趣的是，如果你把{-# OPTIONS --without-K #-}編譯你的文件的頂部，這也適用無公理K.，它仍然會編譯。

來源

2014-01-25 23:01:21 Vitus

您可以定義一個記錄凸出：

record Singleton {α} {A : Set α} (x : A) : Set α where 

fromSingleton : ∀ {α} {A : Set α} {x : A} -> Singleton x -> A 
fromSingleton {x = x} _ = x 

singleton : ∀ {α} {A : Set α} -> (x : A) -> Singleton x 
singleton _ = _

或者equalently

record Singleton {α} {A : Set α} (x : A) : Set α where 

    fromSingleton = x 
open Singleton public 

singleton : ∀ {α} {A : Set α} -> (x : A) -> Singleton x 
singleton _ = _

現在你可以使用這樣的：

open import Relation.Binary.PropositionalEquality 
open import Data.Nat 

f : Singleton 5 -> ℕ 
f x = fromSingleton x 

test : f (singleton 5) ≡ 5 
test = refl 

test' : f _ ≡ 5 
test' = refl

，這是拒絕：

fail : f (singleton 4) ≡ 4 
fail = ?

錯誤：

4 != 5 of type ℕ 
when checking that the expression singleton 4 has type Singleton 5

來源

2014-11-09 19:31:10 user3237465

它可以被定義爲indexed datatype：

data Singleton {ℓ : _} {A : Set ℓ} : A -> Set where 
    singleton : (a : A) -> Singleton a

這類似於如何命題平等a ≡ b由兩個特定元件索引a和b，或如何Vector X n是索引由一個特定的n ∈ ℕ。

來源

2017-11-01 00:54:17

如何定義單例集？

回答

相關問題