I'm trying to find a way to prove a couple of set theory-based problems in Agda, but I'm having a hard time defining the function range.
I took the definition of Subset from Proving decidability of subset in Agda and built on top of it. This is what I got so far:
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 = ?
The problem is that Range takes as an input a function of type A × B → Bool and must return a function B → Bool such that a value B is true iff there exists a value A × B which is true in the initial function. Basically, I would need to iterate through all values of A to know whether B is in the range of the relation. Something impossible to do, isn't it?
There must be surely a better way to implement Range, doesn't it?
Here is the implementation I suggest :
open import Data.Unit
open import Data.Product renaming (_,_ to ⟨_,_⟩)
open import Data.Sum
open import Function
Change the definition of Subset to go to Set instead of Bool. I know this might be controversial, but in my experience this has always been the way to go, and also this is how subsets are implemented in the standard library. (By the way, if you are interested to see the implementation in the standard library, it is in the file Relation/Unary.agda). I also removed the levels of universe since you didn't use them in your later definitions, which led me to clean up the types of the module.
Subset : Set → Set₁
Subset A = A → Set
The definition of membership is changed accordingly.
_∈_ : ∀ {A} → A → Subset A → Set
a ∈ P = P a
Relation : ∀ A B → Set₁
Relation A B = Subset (A × B)
The range becomes then very natural : b is in the range of R if their exists an a such as R of a and b holds.
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
Not much to say about the wholeset
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
The proof of range inclusion is done very naturally with this definition.
⊆-range-∩ : ∀ {A B} {F G : Relation A B} → Range (F ∩ G) ⊆ (Range F ∩ Range G)
⊆-range-∩ _ ⟨ a , ⟨ Fab , Gab ⟩ ⟩ = ⟨ ⟨ a , Fab ⟩ , ⟨ a , Gab ⟩ ⟩
I also took the liberty to add the corresponding property about 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 ⟩