------------------------------------------------------------------------
-- The Agda standard library
--
-- Subsets of finite sets
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Fin.Subset where
open import Algebra.Core using (Op₁; Op₂)
open import Data.Bool using (not; _∧_; _∨_; _≟_)
open import Data.Fin.Base using (Fin; zero; suc)
open import Data.List.Base using (List; foldr; foldl)
open import Data.Nat.Base using (ℕ)
open import Data.Product.Base using (∃; _×_)
open import Data.Vec.Base hiding (foldr; foldl)
open import Function.Base using (flip)
open import Relation.Nullary
private
variable
n : ℕ
------------------------------------------------------------------------
-- Definitions
-- Partitions a finite set into two parts, the inside and the outside.
-- Note that it would be great to shorten these to `in` and `out` but
-- `in` is a keyword (e.g. let ... in ...)
-- Sides.
open import Data.Bool.Base public
using () renaming (Bool to Side; true to inside; false to outside)
-- Subset
Subset : ℕ → Set
Subset = Vec Side
------------------------------------------------------------------------
-- Special subsets
-- The empty subset
⊥ : Subset n
⊥ = replicate _ outside
-- The full subset
⊤ : Subset n
⊤ = replicate _ inside
-- A singleton subset, containing just the given element.
⁅_⁆ : Fin n → Subset n
⁅ zero ⁆ = inside ∷ ⊥
⁅ suc i ⁆ = outside ∷ ⁅ i ⁆
------------------------------------------------------------------------
-- Membership and subset predicates
infix 4 _∈_ _∉_ _⊆_ _⊈_ _⊂_ _⊄_
_∈_ : Fin n → Subset n → Set
x ∈ p = p [ x ]= inside
_∉_ : Fin n → Subset n → Set
x ∉ p = ¬ (x ∈ p)
_⊆_ : Subset n → Subset n → Set
p ⊆ q = ∀ {x} → x ∈ p → x ∈ q
_⊈_ : Subset n → Subset n → Set
p ⊈ q = ¬ (p ⊆ q)
_⊂_ : Subset n → Subset n → Set
p ⊂ q = p ⊆ q × ∃ (λ x → x ∈ q × x ∉ p)
_⊄_ : Subset n → Subset n → Set
p ⊄ q = ¬ (p ⊂ q)
_⊇_ : Subset n → Subset n → Set
_⊇_ = flip _⊆_
_⊉_ : Subset n → Subset n → Set
_⊉_ = flip _⊈_
_⊃_ : Subset n → Subset n → Set
_⊃_ = flip _⊂_
_⊅_ : Subset n → Subset n → Set
_⊅_ = flip _⊄_
------------------------------------------------------------------------
-- Set operations
infixr 7 _∩_
infixr 6 _∪_
infixl 5 _─_ _-_
-- Complement
∁ : Op₁ (Subset n)
∁ p = map not p
-- Intersection
_∩_ : Op₂ (Subset n)
p ∩ q = zipWith _∧_ p q
-- Union
_∪_ : Op₂ (Subset n)
p ∪ q = zipWith _∨_ p q
-- Difference
_─_ : Op₂ (Subset n)
p ─ q = zipWith diff p q
where
diff : Side → Side → Side
diff x inside = outside
diff x outside = x
-- N-ary union
⋃ : List (Subset n) → Subset n
⋃ = foldr _∪_ ⊥
-- N-ary intersection
⋂ : List (Subset n) → Subset n
⋂ = foldr _∩_ ⊤
-- Element removal
_-_ : Subset n → Fin n → Subset n
p - x = p ─ ⁅ x ⁆
-- Size
∣_∣ : Subset n → ℕ
∣ p ∣ = count (_≟ inside) p
------------------------------------------------------------------------
-- Properties
Nonempty : ∀ (p : Subset n) → Set
Nonempty p = ∃ λ f → f ∈ p
Empty : ∀ (p : Subset n) → Set
Empty p = ¬ Nonempty p
Lift : ∀ {ℓ} → (Fin n → Set ℓ) → (Subset n → Set ℓ)
Lift P p = ∀ {x} → x ∈ p → P x
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4