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

Question

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

我从中获取了 Subset 的定义并建立在它之上。这是我到目前为止得到的：

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 类型的函数作为输入，并且必须 return 函数 B → Bool 使得值 B为真当且仅当存在一个值 A × B 在初始函数中为真。基本上，我需要遍历 A 的所有值才能知道 B 是否在关系的范围内。不可能做到的事情，不是吗？

肯定有更好的方法来实现 Range，不是吗？

Answer 1

这是我建议的实施方式：

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

将 Subset 的定义更改为 Set 而不是 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 在 R 范围内，如果它们存在 a 例如 R 或 a 并且b 成立。

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

我还冒昧的补充了相应的属性关于union

_⋃_ : ∀ {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 ⟩

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

How to define the range function on a relation in Agda (set theory)

relation

agda

set-theory