------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of constructions over unary relations
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Relation.Unary.Properties where

open import Data.Product using (_×_; _,_; swap; proj₁)
open import Data.Sum.Base using (inj₁; inj₂)
open import Data.Unit.Base using (tt)
open import Level
open import Relation.Binary.Core
open import Relation.Binary.Definitions hiding (Decidable; Universal)
open import Relation.Unary
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Nullary.Sum using (_⊎-dec_)
open import Relation.Nullary.Negation.Core using (¬?)
open import Function.Base using (_$_; _∘_)

private
  variable
    a b ℓ ℓ₁ ℓ₂ : Level
    A : Set a
    B : Set b

----------------------------------------------------------------------
-- The empty set

∅? : Decidable {A = A} ∅
∅? _ = no λ()

∅-Empty : Empty {A = A} ∅
∅-Empty x ()

∁∅-Universal : Universal {A = A} (∁ ∅)
∁∅-Universal = λ x x∈∅ → x∈∅

----------------------------------------------------------------------
-- The universe

U? : Decidable {A = A} U
U? _ = yes tt

U-Universal : Universal {A = A} U
U-Universal = λ _ → _

∁U-Empty : Empty {A = A} (∁ U)
∁U-Empty = λ x x∈∁U → x∈∁U _

----------------------------------------------------------------------
-- Subset properties

∅-⊆ : (P : Pred A ℓ) → ∅ ⊆ P
∅-⊆ P ()

⊆-U : (P : Pred A ℓ) → P ⊆ U
⊆-U P _ = _

⊆-refl : Reflexive (_⊆_ {A = A} {ℓ})
⊆-refl x∈P = x∈P

⊆-trans : Transitive (_⊆_ {A = A} {ℓ})
⊆-trans P⊆Q Q⊆R x∈P = Q⊆R (P⊆Q x∈P)

⊂-asym : Asymmetric (_⊂_ {A = A} {ℓ})
⊂-asym (_ , Q⊈P) = Q⊈P ∘ proj₁

----------------------------------------------------------------------
-- Decidability properties

∁? : {P : Pred A ℓ} → Decidable P → Decidable (∁ P)
∁? P? x = ¬? (P? x)

_∪?_ : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} →
       Decidable P → Decidable Q → Decidable (P ∪ Q)
_∪?_ P? Q? x = (P? x) ⊎-dec (Q? x)

_∩?_ : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} →
       Decidable P → Decidable Q → Decidable (P ∩ Q)
_∩?_ P? Q? x = (P? x) ×-dec (Q? x)

_×?_ : {P : Pred A ℓ₁} {Q : Pred B ℓ₂} →
       Decidable P → Decidable Q → Decidable (P ⟨×⟩ Q)
_×?_ P? Q? (a , b) = (P? a) ×-dec (Q? b)

_⊙?_ : {P : Pred A ℓ₁} {Q : Pred B ℓ₂} →
       Decidable P → Decidable Q → Decidable (P ⟨⊙⟩ Q)
_⊙?_ P? Q? (a , b) = (P? a) ⊎-dec (Q? b)

_⊎?_ : {P : Pred A ℓ} {Q : Pred B ℓ} →
       Decidable P → Decidable Q → Decidable (P ⟨⊎⟩ Q)
_⊎?_ P? Q? (inj₁ a) = P? a
_⊎?_ P? Q? (inj₂ b) = Q? b

_~? : {P : Pred (A × B) ℓ} → Decidable P → Decidable (P ~)
_~? P? = P? ∘ swap