1

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?

1 Answer 1

1

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 ⟩
4
  • Thank you. It took me an hour to go through your solution trying to understand every detail, but I was finally able to prove two other properties over ranges and domains. I must to say that working with dependent types is both exciting and exhausting. Do you know where to read more about sets, subsets and their operations, and how are they implemented in the standard library?
    – helq
    Apr 5, 2020 at 15:22
  • You're welcome, feel free to ask if you need further explanation about this code or the one you're writing. Getting into programming / proving using a dependently typed language is indeed very confusing and fascination, but is definitely worth the journey. In my opinion, it does not matter how much material you read, you have to practice to start really feel how things are working, and it looks like this is what you did here. About subsets, you should definitely check out the file I pointed out in the std lib, it is definitely readable and understandable.
    – MrO
    Apr 5, 2020 at 22:08
  • Thank you for your encouraging comments. Until now I have just used Agda as a black box, and once in a while, when playing with it, I learn something a little bit more of how it behaves under the curtains, but I do not yet understand the rules under which it works. Where should I go to to understand better the theory behind Dependent Types? What means "dependent typed" in the world of lambda calculus? Thanks!
    – helq
    Apr 6, 2020 at 0:14
  • Your questions are quite vague to me, maybe you should start by learning what Curry-Howard correspondence is - maybe you do know that already - and understand what dependent types are - types that can depend on values - and why they are so important when coupled to said correspondence. If you are more precise about what you are looking for, maybe I could point you in the right direction. About lambda calculus for instance I know a very good conference which you could enjoy if, by any chance, you happen to speak french.
    – MrO
    Apr 8, 2020 at 12:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.