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

Question

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

我从Proving decidability of subset in 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的更好的方法，不是吗？

Answer 1

这是我建议的实现：

open import Data.Unit using (⊤; tt)
open import Data.Product using (_×_ ; ∃) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum 
open import Function

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

Subset : (A : Set) -> Set _
Subset A = A → Set

成员资格的定义已相应更改。

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

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

然后范围变得很自然：b是R的范围，如果它们存在a，例如R的a和b成立。

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

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

关于整体没什么可说的

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

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

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

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

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

我还自由地添加了有关union的类似属性。

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

⋃-range-⊆ : ∀ {A B : Set} {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 ⟩