module Data.Sets where
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.OrderMorphism
open import Data.Function
open import Data.List as L using (List)
open import Data.Product using (∃; _×_)
open import Level
module Sets₁ (dto : DecTotalOrder zero zero zero) where
open DecTotalOrder dto public using (_≈_)
open DecTotalOrder dto hiding (_≈_)
infixr 6 _∪_
infix 5 _∈?_
infix 4 _∈_ _|≈|_
abstract postulate decSetoid : DecSetoid _ _
<Set> : Set
<Set> = DecSetoid.Carrier decSetoid
_|≈|_ : Rel <Set> zero
_|≈|_ = DecSetoid._≈_ decSetoid
abstract
postulate
empty : <Set>
insert : Carrier → <Set> → <Set>
_∪_ : <Set> → <Set> → <Set>
_∈_ : Carrier → <Set> → Set
_∈?_ : (x : Carrier) → (s : <Set>) → Dec (x ∈ s)
toList : <Set> → List Carrier
postulate
prop-∈-insert₁ : ∀ {x y s} → x ≈ y → x ∈ insert y s
prop-∈-insert₂ : ∀ {x y s} → x ∈ s → x ∈ insert y s
prop-∈-insert₃ : ∀ {x y s} → ¬ x ≈ y → x ∈ insert y s → x ∈ s
prop-∈-empty : ∀ {x} → ¬ x ∈ empty
prop-∈-∪ : ∀ {x s₁ s₂} → x ∈ s₁ → x ∈ s₁ ∪ s₂
prop-∪₁ : ∀ {s₁ s₂} → s₁ ∪ s₂ |≈| s₂ ∪ s₁
prop-∪₂ : ∀ {s₁ s₂ s₃} → s₁ ∪ (s₂ ∪ s₃) |≈| (s₁ ∪ s₂) ∪ s₃
prop-∈-|≈| : ∀ {x} → (λ s → x ∈ s) Respects _|≈|_
prop-∈-≈ : ∀ {s} → (λ x → x ∈ s) Respects _≈_
singleton : Carrier → <Set>
singleton x = insert x empty
⋃_ : List <Set> → <Set>
⋃_ = L.foldr _∪_ empty
fromList : List Carrier → <Set>
fromList = L.foldr insert empty
_⊆_ : <Set> → <Set> → Set
s₁ ⊆ s₂ = ∀ x → x ∈ s₁ → x ∈ s₂
open Sets₁ public
open DecTotalOrder hiding (_≈_)
open _⇒-Poset_
abstract
postulate
map : ∀ {do₁ do₂} → do₁ ⇒-DTO do₂ → <Set> do₁ → <Set> do₂
mapToSet : ∀ {do₁ do₂} →
(Carrier do₁ → <Set> do₂) →
<Set> do₁ → <Set> do₂
prop-map-∈₁ : ∀ {do₁ do₂ f x s} →
x ⟨ _∈_ do₁ ⟩ s →
fun f x ⟨ _∈_ do₂ ⟩ map f s
prop-map-∈₂ : ∀ {do₁ do₂ f y s} →
y ⟨ _∈_ do₂ ⟩ map f s →
∃ λ x → (fun f x ⟨ _≈_ do₂ ⟩ y) ×
( x ⟨ _∈_ do₁ ⟩ s)
prop-mapToSet₁ : ∀ {do₁ do₂ f x s} →
x ⟨ _∈_ do₁ ⟩ s →
f x ⟨ _⊆_ do₂ ⟩ mapToSet f s
prop-mapToSet₂ : ∀ {do₁ do₂ f y s} →
y ⟨ _∈_ do₂ ⟩ mapToSet f s →
∃ λ x → (y ⟨ _∈_ do₂ ⟩ f x) ×
(x ⟨ _∈_ do₁ ⟩ s)