在 Agda 中证明子集的可判定性答案

【问题标题】：Proving decidability of subset in Agda在 Agda 中证明子集的可判定性
【发布时间】：2015-12-09 16:00:27
【问题描述】：

假设我在 Agda 中有这个 Subset 的定义

Subset : ∀ {α} → Set α → {ℓ : Level} → Set (α ⊔ suc ℓ)
Subset A {ℓ} = A → Set ℓ

我有一套

data Q : Set where
 a : Q
 b : Q

是否有可能证明 q 的所有子集都是可判定的，为什么？

Qs? : (qs : Subset Q {zero}) → Decidable qs

Decidable 在这里定义：

-- Membership
infix 10 _∈_
_∈_ : ∀ {α ℓ}{A : Set α} → A → Subset A → Set ℓ
a ∈ p = p a

-- Decidable
Decidable : ∀ {α ℓ}{A : Set α} → Subset A {ℓ} → Set (α ⊔ ℓ)
Decidable as = ∀ a → Dec (a ∈ as)

【问题讨论】：

这个子集定义不允许这样做。对于一些无法确定的t，您可以只使用const t : Subset Q。

标签： subset agda decidable

【解决方案1】：

不适用于子集的定义，因为可判定性需要检查“p a”是否有人居住，即排除中间。

可确定的子集将完全映射到 Bool：

Subset : ∀ {α} (A : Set α) -> Set
Subset A = A → Bool 

_∈_ : ∀ {α}{A : Set α} → A → Subset A → Set
a ∈ p = T (p a)

但是，如果您希望成员证明的形式更加灵活，您可以使用您对子集的定义并携带证明它是可判定的。

【讨论】：