------------------------------------------------------------------------
-- The Agda standard library
--
-- AVL trees where at least one element satisfies a given property
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (StrictTotalOrder)
module Data.Tree.AVL.Relation.Unary.Any
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
where
open import Data.Product.Base as Product using (∃)
open import Function.Base using (_∘_; _$_)
open import Level using (Level; _⊔_)
open import Relation.Nullary.Decidable using (map′)
open import Relation.Unary
open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
open import Data.Tree.AVL.Indexed strictTotalOrder as Indexed using (K&_; _,_)
open import Data.Tree.AVL strictTotalOrder using (Tree; tree; Value)
import Data.Tree.AVL.Indexed.Relation.Unary.Any strictTotalOrder as AVLₚ
private
variable
v p q : Level
V : Value v
t : Tree V
P : Pred (K& V) p
Q : Pred (K& V) q
------------------------------------------------------------------------
-- Definition
-- Given a predicate P, Any P t describes a path in t to an element that
-- satisfies P. There may be others.
-- See `Relation.Unary` for an explanation of predicates.
data Any {V : Value v} (P : Pred (K& V) p) :
Tree V → Set (p ⊔ a ⊔ v ⊔ ℓ₂) where
tree : ∀ {h t} → AVLₚ.Any P t → Any P (tree {h = h} t)
------------------------------------------------------------------------
-- Operations on Any
map : P ⊆ Q → Any P t → Any Q t
map f (tree p) = tree (AVLₚ.map f p)
lookup : Any {V = V} P t → K& V
lookup (tree p) = AVLₚ.lookup p
lookupKey : Any P t → Key
lookupKey (tree p) = AVLₚ.lookupKey p
-- If any element satisfies P, then P is satisfied.
satisfied : Any P t → ∃ P
satisfied (tree p) = AVLₚ.satisfied p
------------------------------------------------------------------------
-- Properties of predicates preserved by Any
any? : Decidable P → Decidable (Any {V = V} P)
any? P? (tree p) = map′ tree (λ where (tree p) → p) (AVLₚ.any? P? p)
satisfiable : (k : Key) → Satisfiable (P ∘ (k ,_)) → Satisfiable (Any {V = V} P)
satisfiable k sat = Product.map tree tree
$ AVLₚ.satisfiable Indexed.⊥⁺<[ k ] Indexed.[ k ]<⊤⁺ sat
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