{-# OPTIONS --universe-polymorphism #-}

module FSets where

open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

open import Data.Nat hiding (equal;_≟_;_≤?_;fold)
open import Data.Product
open import Data.Bool hiding (_≟_)
open import Data.List hiding (filter; partition)
open import Data.Maybe

open import Level

record FSet (setoid : DecSetoid zero zero) : Set₁ where
  open DecSetoid setoid renaming (Carrier to elt)

  field 
    t   : Set 
    _[∈]_ : elt → t → Set

  _[∉]_ : elt → t → Set
  _[∉]_ a s = ¬ (a [∈] s)

  _[=]_ : t → t → Set
  _[=]_ s1 s2 = (a : elt) → (a [∈] s1 → a [∈] s2) × (a [∈] s2 → a [∈] s1)

  _[⊆]_ : t → t → Set
  _[⊆]_ s1 s2 = (a : elt) → a [∈] s1 → a [∈] s2

  Empty : t → Set
  Empty s = (a : elt) → a [∉] s

  Forall : (P : elt → Set) → t → Set
  Forall P s = (a : elt) → a [∈] s → P a
  
  Exists : (P : elt → Set) → t → Set
  Exists P s = Σ elt (\a → a [∈] s × P a)
  
  field
    empty     : t
    empty?    : t → Bool
    mem?      : elt → t → Bool

    add       : elt → t → t
    singleton : elt → t
    remove    : elt → t → t
    _[∪]_     : t → t → t
    _[∩]_     : t → t → t
    diff      : t → t → t

    filter    : (elt → Bool) → t → t
    partition : (elt → Bool) → t → t × t
    fold      : ∀ {A : Set} → (elt → A → A) → t → A → A

    cardinal  : t → ℕ
    elements  : t → List elt
    choose    : t → Maybe elt

    equal?    : t → t → Bool
    subset?   : t → t → Bool
    forall?   : (elt → Bool) → t → Bool
    exists?   : (elt → Bool) → t → Bool

    -- Now the specification of things
    -- Spec for _[∈]_
    [∈]-1 : ∀ {s} → (\a → a [∈] s) Respects _≈_
    
    -- Spec for _[=]_
    [=]-equiv : IsDecEquivalence _[=]_
    
    -- Spec for mem?
    mem?-1 : ∀ {a s} → a [∈] s → mem? a s ≡ true
    mem?-2 : ∀ {a s} → mem? a s ≡ true → a [∈] s
  
    -- Spec for equal?
    equal?-1 : ∀ {s₁ s₂} → s₁ [=] s₂ → equal? s₁ s₂ ≡ true
    equal?-2 : ∀ {s₁ s₂} → equal? s₁ s₂ ≡ true → s₁ [=] s₂
  
    -- Spec for subset?
    subset?-1 : ∀ {s₁ s₂} → s₁ [⊆] s₂ → subset? s₁ s₂ ≡ true
    subset?-2 : ∀ {s₁ s₂} → subset? s₁ s₂ ≡ true → s₁ [⊆] s₂
  
    -- Spec for empty
    empty-1 : Empty empty
  
    -- Spec for empty?
    empty?-1 : ∀ {s} → Empty s → empty? s ≡ true
    empty?-2 : ∀ {s} → empty? s ≡ true → Empty s
  
    -- Spec for add
    add-1 : ∀ {a b s} → a ≈ b                      → b [∈] (add a s)
    add-2 : ∀ {a b s} → b [∈] s                    → b [∈] (add a s)
    add-3 : ∀ {a b s} → ¬(a ≈ b) → b [∈] (add a s) → b [∈] s
  
    -- Spec for remove
    remove-1 : ∀ {a b s} → a ≈ b               → ¬ b [∈] remove a s
    remove-2 : ∀ {a b s} → ¬ (a ≈ b) → b [∈] s → b [∈] remove a s
    remove-3 : ∀ {a b s} → b [∈] remove a s    → b [∈] s