------------------------------------------------------------------------ -- 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