module Data.Fin.Subset where
open import Algebra
import Algebra.Properties.BooleanAlgebra as BoolAlgProp
import Algebra.Properties.BooleanAlgebra.Expression as BAExpr
open import Data.Bool.Properties using (∨-∧-booleanAlgebra)
open import Data.Fin
open import Data.List.Base using (List; foldr; foldl)
open import Data.Nat
open import Data.Product
open import Data.Vec using (Vec; _∷_; _[_]=_)
import Data.Vec.Relation.Pointwise.Extensional as Pointwise
open import Relation.Nullary
open import Data.Bool.Base public
using () renaming (Bool to Side; true to inside; false to outside)
Subset : ℕ → Set
Subset = Vec Side
infix 4 _∈_ _∉_ _⊆_ _⊈_
_∈_ : ∀ {n} → Fin n → Subset n → Set
x ∈ p = p [ x ]= inside
_∉_ : ∀ {n} → Fin n → Subset n → Set
x ∉ p = ¬ (x ∈ p)
_⊆_ : ∀ {n} → Subset n → Subset n → Set
p₁ ⊆ p₂ = ∀ {x} → x ∈ p₁ → x ∈ p₂
_⊈_ : ∀ {n} → Subset n → Subset n → Set
p₁ ⊈ p₂ = ¬ (p₁ ⊆ p₂)
booleanAlgebra : ℕ → BooleanAlgebra _ _
booleanAlgebra n =
BoolAlgProp.replace-equality
(BAExpr.lift ∨-∧-booleanAlgebra n)
Pointwise.Pointwise-≡
private
open module BA {n} = BooleanAlgebra (booleanAlgebra n) public
using
( ⊥
; ⊤
)
renaming
( _∨_ to _∪_
; _∧_ to _∩_
; ¬_ to ∁
)
⁅_⁆ : ∀ {n} → Fin n → Subset n
⁅ zero ⁆ = inside ∷ ⊥
⁅ suc i ⁆ = outside ∷ ⁅ i ⁆
⋃ : ∀ {n} → List (Subset n) → Subset n
⋃ = foldr _∪_ ⊥
⋂ : ∀ {n} → List (Subset n) → Subset n
⋂ = foldr _∩_ ⊤
Nonempty : ∀ {n} (p : Subset n) → Set
Nonempty p = ∃ λ f → f ∈ p
Empty : ∀ {n} (p : Subset n) → Set
Empty p = ¬ Nonempty p
Lift : ∀ {n} → (Fin n → Set) → (Subset n → Set)
Lift P p = ∀ {x} → x ∈ p → P x