Как определить функцию диапазона для отношения в 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, не так ли?

Answer 1

Вот реализация, которую я предлагаю:

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

Измените определение Subset на go на Set вместо Bool. Я знаю, что это может быть спорным, но в моем опыте это всегда путь к go, а также это как подмножества реализованы в стандартной библиотеке. (Кстати, если вам интересно увидеть реализацию в стандартной библиотеке, она находится в файле Relation / Unary.agda). Я также удалил уровни вселенной, поскольку вы не использовали их в своих более поздних определениях, что привело меня к очистке типов модуля.

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, если они существуют, например, 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 ⟩ ⟩

Я также взял свобода добавлять соответствующие свойства о союзе.

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