------------------------------------------------------------------------
-- The Agda standard library
--
-- Some code related to indexed AVL trees that relies on the K rule
------------------------------------------------------------------------
{-# OPTIONS --with-K --safe #-}
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Structures using (IsStrictTotalOrder)
open import Relation.Binary.Bundles using (StrictTotalOrder)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; subst)
module Data.Tree.AVL.Indexed.WithK
{k r} (Key : Set k) {_<_ : Rel Key r}
(isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where
strictTotalOrder : StrictTotalOrder _ _ _
strictTotalOrder = record { isStrictTotalOrder = isStrictTotalOrder }
open import Data.Tree.AVL.Indexed strictTotalOrder as AVL hiding (Value)
module _ {v} {V′ : Key → Set v} where
private
V : AVL.Value v
V = AVL.MkValue V′ (subst V′)
node-injectiveˡ : ∀ {hˡ hʳ h l u k}
{lk₁ : Tree V l [ k .key ] hˡ} {lk₂ : Tree V l [ k .key ] hˡ}
{ku₁ : Tree V [ k .key ] u hʳ} {ku₂ : Tree V [ k .key ] u hʳ}
{bal₁ bal₂ : hˡ ∼ hʳ ⊔ h} →
node k lk₁ ku₁ bal₁ ≡ node k lk₂ ku₂ bal₂ → lk₁ ≡ lk₂
node-injectiveˡ refl = refl
node-injectiveʳ : ∀ {hˡ hʳ h l u k}
{lk₁ : Tree V l [ k .key ] hˡ} {lk₂ : Tree V l [ k .key ] hˡ}
{ku₁ : Tree V [ k .key ] u hʳ} {ku₂ : Tree V [ k .key ] u hʳ}
{bal₁ bal₂ : hˡ ∼ hʳ ⊔ h} →
node k lk₁ ku₁ bal₁ ≡ node k lk₂ ku₂ bal₂ → ku₁ ≡ ku₂
node-injectiveʳ refl = refl
node-injective-bal : ∀ {hˡ hʳ h l u k}
{lk₁ : Tree V l [ k .key ] hˡ} {lk₂ : Tree V l [ k .key ] hˡ}
{ku₁ : Tree V [ k .key ] u hʳ} {ku₂ : Tree V [ k .key ] u hʳ}
{bal₁ bal₂ : hˡ ∼ hʳ ⊔ h} →
node k lk₁ ku₁ bal₁ ≡ node k lk₂ ku₂ bal₂ → bal₁ ≡ bal₂
node-injective-bal refl = refl
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