relation - 如何在 Agda 中定义关系的范围函数（集合论）

Question

我试图找到一种方法来证明 Agda 中的几个基于集合论的问题，但我很难定义函数范围。

我从在 Agda 中证明子集的可判定性中获取了子集的定义，并在此基础上构建。这是我到目前为止得到的：

open import Data.Bool as Bool using (Bool; true; false; T; _∨_; _∧_)
open import Data.Unit using (⊤; tt)
open import Level using (Level; _⊔_; 0ℓ) renaming (suc to lsuc)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)

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

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

Relation : ∀ {α β} (A : Set α) (B : Set β) → Set (α ⊔ β)
Relation A B = Subset (A × B)

Range : ∀ {A B : Set} → Relation A B → Subset B
Range = ?

_⊆_ : ∀ {A : Set} → Subset A → Subset A → Set
A ⊆ B = ∀ x → x ∈ A → x ∈ B

wholeSet : ∀ (A : Set) → Subset A
wholeSet _ = λ _ → true

∀subset⊆set : ∀ {A : Set} {sub : Subset A} → sub ⊆ wholeSet A
∀subset⊆set = λ _ _ → tt

_∩_ : ∀ {A : Set} → Subset A → Subset A → Subset A
A ∩ B = λ x → (A x) ∧ (B x)

⊆-range-∩ : ∀ {A B : Set}
            (F G : Relation A B)
          → Range (F ∩ G) ⊆ (Range F ∩ Range G)
⊆-range-∩ f g = ?

问题在于，Range将一个类型的函数作为输入，A × B → Bool并且必须返回一个函数B → Bool，使得如果在初始函数中B存在一个为真的值，则该值为真。A × B基本上，我需要遍历所有值A以了解是否B在关系范围内。不可能的事情，不是吗？

肯定有更好的实施方式Range，不是吗？

标签： relationagdaset-theory

Answer 1

这是我建议的实现：

open import Data.Unit
open import Data.Product renaming (_,_ to ⟨_,_⟩)
open import Data.Sum 
open import Function

将 的定义更改Subset为 go toSet而不是Bool。我知道这可能会引起争议，但根据我的经验，这一直是要走的路，这也是标准库中子集的实现方式。（顺便说一句，如果您有兴趣查看标准库中的实现，它位于文件 Relation/Unary.agda 中）。我还删除了 Universe 的级别，因为您在以后的定义中没有使用它们，这导致我清理了模块的类型。

Subset : Set → Set₁
Subset A = A → Set

成员资格的定义也相应改变。

_∈_ : ∀ {A} → A → Subset A → Set
a ∈ P = P a

Relation : ∀ A B → Set₁
Relation A B = Subset (A × B)

然后范围变得非常自然：如果它们存在，b则在范围内，例如并成立。RaRab

Range : ∀ {A B} → Relation A B → Subset B
Range R b = ∃ (R ∘ ⟨_, b ⟩)  -- equivalent to ∃ \a → R ⟨ a , b ⟩

_⊆_ : ∀ {A} → Subset A → Subset A → Set
A ⊆ B = ∀ x → x ∈ A → x ∈ B

整套话不多说

wholeSet : ∀ A → Subset A
wholeSet _ _ = ⊤

∀subset⊆set : ∀ {A sub} → sub ⊆ wholeSet A
∀subset⊆set _ _ = tt

_∩_ : ∀ {A} → Subset A → Subset A → Subset A
(A ∩ B) x = x ∈ A × x ∈ B

范围包含的证明非常自然地使用此定义完成。

⊆-range-∩ : ∀ {A B} {F G : Relation A B} → Range (F ∩ G) ⊆ (Range F ∩ Range G)
⊆-range-∩ _ ⟨ a , ⟨ Fab , Gab ⟩ ⟩ = ⟨ ⟨ a , Fab ⟩ , ⟨ a , Gab ⟩ ⟩

我还冒昧地添加了关于联合的相应属性。

_⋃_ : ∀ {A} → Subset A → Subset A → Subset A
(A ⋃ B) x = x ∈ A ⊎ x ∈ B

⋃-range-⊆ : ∀ {A B} {F G : Relation A B} → (Range F ⋃ Range G) ⊆ Range (F ⋃ G)
⋃-range-⊆ _ (inj₁ ⟨ a , Fab ⟩) = ⟨ a , inj₁ Fab ⟩
⋃-range-⊆ _ (inj₂ ⟨ a , Gab ⟩) = ⟨ a , inj₂ Gab ⟩