123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127-------------------------------------------------------------------------- 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.Nullaryopen import Relation.Unaryopen 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