证明Agda中子集的可判定性 [英] Proving decidability of subset in Agda

问题描述

假设我在Agda中具有这个子集的定义

Suppose I have this definition of Subset in Agda

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

我有一套

data Q : Set where
 a : Q
 b : Q

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

Is it possible to prove that all subset of q is decidable and why?

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

可定义项在这里定义:

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

推荐答案

不适用于子集的定义，因为可确定性要求检查"p a"是否有人居住，即排除中间.

Not for that definition of Subset, since decidability would require to check whether "p a" is inhabited or not, i.e. excluded middle.

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

Decidable subsets would exactly be maps into Bool:

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

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

但是，如果您希望在成员资格证明的形状上具有更大的灵活性，可以使用Subset的定义并携带一个可确定的证明.

But if you want more flexibility on the shape of the membership proofs you could use your definition of Subset and carry around a proof that it is Decidable.

这篇关于证明Agda中子集的可判定性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！