------------------------------------------------------------------------
-- The Agda standard library
--
-- Predicate transformers
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Relation.Unary.PredicateTransformer where

open import Data.Product.Base using (∃)
open import Function.Base using (_∘_)
open import Level hiding (_⊔_)
open import Relation.Nullary
open import Relation.Unary
open import Relation.Binary.Core using (REL)

private
  variable
    a b c i ℓ ℓ₁ ℓ₂ ℓ₃ : Level
    A : Set a
    B : Set b
    C : Set c

------------------------------------------------------------------------
-- Heterogeneous and homogeneous predicate transformers

PT : Set a → Set b → (ℓ₁ ℓ₂ : Level) → Set _
PT A B ℓ₁ ℓ₂ = Pred A ℓ₁ → Pred B ℓ₂

Pt : Set a → (ℓ : Level) → Set _
Pt A ℓ = PT A A ℓ ℓ

------------------------------------------------------------------------
-- Composition and identity

infixr 9 _⍮_

_⍮_ : PT B C ℓ₂ ℓ₃ → PT A B ℓ₁ ℓ₂ → PT A C ℓ₁ _
S ⍮ T = S ∘ T

skip : PT A A ℓ ℓ
skip P = P

------------------------------------------------------------------------
-- Operations on predicates extend pointwise to predicate transformers

-- The bottom and the top of the predicate transformer lattice.

abort : PT A B 0ℓ 0ℓ
abort = λ _ → ∅

magic : PT A B 0ℓ 0ℓ
magic = λ _ → U

-- Negation.

infix 8 ∼_

∼_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂
∼ T = ∁ ∘ T

-- Refinement.

infix 4 _⊑_ _⊒_ _⊑′_ _⊒′_

_⊑_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → Set _
S ⊑ T = ∀ {X} → S X ⊆ T X

_⊑′_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → Set _
S ⊑′ T = ∀ X → S X ⊆ T X

_⊒_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → Set _
T ⊒ S = T ⊑ S

_⊒′_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → Set _
T ⊒′ S = S ⊑′ T

-- The dual of refinement.

infix 4 _⋢_

_⋢_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → Set _
S ⋢ T = ∃ λ X → S X ≬ T X

-- Union.

infixl 6 _⊓_

_⊓_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂
S ⊓ T = λ X → S X ∪ T X

-- Intersection.

infixl 7 _⊔_

_⊔_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂
S ⊔ T = λ X → S X ∩ T X

-- Implication.

infixl 8 _⇛_

_⇛_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂
S ⇛ T = λ X → S X ⇒ T X

-- Infinitary union and intersection.

infix 9 ⨆ ⨅

⨆ : ∀ (I : Set i) → (I → PT A B ℓ₁ ℓ₂) → PT A B ℓ₁ _
⨆ I T = λ X → ⋃[ i ∶ I ] T i X

syntax ⨆ I (λ i → T) = ⨆[ i ∶ I ] T

⨅ : ∀ (I : Set i) → (I → PT A B ℓ₁ ℓ₂) → PT A B ℓ₁ _
⨅ I T = λ X → ⋂[ i ∶ I ] T i X

syntax ⨅ I (λ i → T) = ⨅[ i ∶ I ] T

-- Angelic and demonic update.

⟨_⟩ : REL A B ℓ → PT B A ℓ _
⟨ R ⟩ P = λ x → R x ≬ P

[_] : REL A B ℓ → PT B A ℓ _
[ R ] P = λ x → R x ⊆ P