------------------------------------------------------------------------
-- The Agda standard library
--
-- AVL trees whose elements satisfy a given property
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (StrictTotalOrder)
module Data.Tree.AVL.Indexed.Relation.Unary.All
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
where
open import Data.Nat.Base using (ℕ)
open import Data.Product.Base using (_,_; _×_)
open import Data.Product.Nary.NonDependent using (uncurryₙ)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Function.Base using (flip; _∘_; const)
open import Function.Nary.NonDependent using (congₙ)
open import Level using (Level; _⊔_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
open import Relation.Nullary.Decidable.Core using (Dec; yes; map′; _×-dec_)
open import Relation.Unary using (Pred; Decidable; Universal; Irrelevant; _⊆_; _∪_)
open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
open import Data.Tree.AVL.Indexed strictTotalOrder
using (Tree; Value; Key⁺; [_]; _<⁺_; K&_; key; _∼_⊔_; ∼0; leaf; node)
open import Data.Tree.AVL.Indexed.Relation.Unary.Any strictTotalOrder
using (Any; here; left; right)
private
variable
v p q : Level
V : Value v
P : Pred (K& V) p
Q : Pred (K& V) q
l u : Key⁺
n : ℕ
t : Tree V l u n
------------------------------------------------------------------------
-- Definition
-- Given a predicate P, All P t is a proof that all of the elements in t
-- satisfy P.
-- See `Relation.Unary` for an explanation of predicates.
data All {V : Value v} (P : Pred (K& V) p) {l u}
: ∀ {n} → Tree V l u n → Set (p ⊔ a ⊔ v ⊔ ℓ₂) where
leaf : {p : l <⁺ u} → All P (leaf p)
node : ∀ {hˡ hʳ h} {kv : K& V}
{lk : Tree V l [ kv .key ] hˡ}
{ku : Tree V [ kv .key ] u hʳ} →
{bal : hˡ ∼ hʳ ⊔ h} →
P kv → All P lk → All P ku → All P (node kv lk ku bal)
------------------------------------------------------------------------
-- Operations on All
map : P ⊆ Q → All P t → All Q t
map f leaf = leaf
map f (node p l r) = node (f p) (map f l) (map f r)
decide : Π[ P ∪ Q ] → (t : Tree V l u n) → All P t ⊎ Any Q t
decide p⊎q (leaf l<u) = inj₁ leaf
decide p⊎q (node kv l r bal) with p⊎q kv | decide p⊎q l | decide p⊎q r
... | inj₂ q | _ | _ = inj₂ (here q)
... | _ | inj₂ q | _ = inj₂ (left q)
... | _ | _ | inj₂ q = inj₂ (right q)
... | inj₁ pv | inj₁ pl | inj₁ pr = inj₁ (node pv pl pr)
unnode : ∀ {hˡ hʳ h} {kv : K& V}
{lk : Tree V l [ kv .key ] hˡ}
{ku : Tree V [ kv .key ] u hʳ}
{bal : hˡ ∼ hʳ ⊔ h} →
All P (node kv lk ku bal) → P kv × All P lk × All P ku
unnode (node p l r) = p , l , r
all? : Decidable P → ∀ (t : Tree V l u n) → Dec (All P t)
all? p? (leaf l<u) = yes leaf
all? p? (node kv l r bal) = map′ (uncurryₙ 3 node) unnode
(p? kv ×-dec all? p? l ×-dec all? p? r)
universal : Universal P → (t : Tree V l u n) → All P t
universal u (leaf l<u) = leaf
universal u (node kv l r bal) = node (u kv) (universal u l) (universal u r)
irrelevant : Irrelevant P → (p q : All P t) → p ≡ q
irrelevant irr leaf leaf = refl
irrelevant irr (node p l₁ r₁) (node q l₂ r₂) =
congₙ 3 node (irr p q) (irrelevant irr l₁ l₂) (irrelevant irr r₁ r₂)
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