------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to Any
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (StrictTotalOrder)
module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties
{a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
where
open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′)
open import Data.Maybe.Properties using (just-injective)
open import Data.Maybe.Relation.Unary.All as Maybe using (nothing; just)
open import Data.Nat.Base using (ℕ)
open import Data.Product.Base as Prod using (∃; ∃-syntax; _×_; _,_; proj₁; proj₂)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
open import Function.Base as F using (const; _∘_; id; flip; _∘′_)
open import Level using (Level)
open import Relation.Binary.Definitions using (_Respects_; tri<; tri≈; tri>)
open import Relation.Binary.PropositionalEquality.Core using (_≡_) renaming (refl to ≡-refl)
open import Relation.Nullary.Negation.Core using (¬_; contradiction)
open import Relation.Nullary.Decidable.Core as Dec using (Dec; yes; no)
open import Relation.Unary using (Pred; _∩_)
open import Data.Tree.AVL.Indexed sto as AVL
open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
open StrictTotalOrder sto renaming (Carrier to Key; trans to <-trans); open Eq using (sym; trans)
open import Relation.Binary.Construct.Add.Extrema.Strict _<_ using ([<]-injective)
import Relation.Binary.Reasoning.StrictPartialOrder as <-Reasoning
private
variable
v p q : Level
k : Key
V : Value v
l u : Key⁺
n : ℕ
P Q : Pred (K& V) p
------------------------------------------------------------------------
-- Any.lookup
lookup-result : {t : Tree V l u n} (p : Any P t) → P (Any.lookup p)
lookup-result (here p) = p
lookup-result (left p) = lookup-result p
lookup-result (right p) = lookup-result p
lookup-bounded : {t : Tree V l u n} (p : Any P t) → l < Any.lookup p .key < u
lookup-bounded {t = node kv lk ku bal} (here p) = ordered lk , ordered ku
lookup-bounded {t = node kv lk ku bal} (left p) =
Prod.map₂ (flip (trans⁺ _) (ordered ku)) (lookup-bounded p)
lookup-bounded {t = node kv lk ku bal} (right p) =
Prod.map₁ (trans⁺ _ (ordered lk)) (lookup-bounded p)
lookup-rebuild : {t : Tree V l u n} (p : Any P t) → Q (Any.lookup p) → Any Q t
lookup-rebuild (here _) q = here q
lookup-rebuild (left p) q = left (lookup-rebuild p q)
lookup-rebuild (right p) q = right (lookup-rebuild p q)
lookup-rebuild-accum : {t : Tree V l u n} (p : Any P t) → Q (Any.lookup p) → Any (Q ∩ P) t
lookup-rebuild-accum p q = lookup-rebuild p (q , lookup-result p)
joinˡ⁺-here⁺ : ∀ {l u hˡ hʳ h} →
(kv : K& V) →
(l : ∃ λ i → Tree V l [ kv .key ] (i ⊕ hˡ)) →
(r : Tree V [ kv .key ] u hʳ) →
(bal : hˡ ∼ hʳ ⊔ h) →
P kv → Any P (proj₂ (joinˡ⁺ kv l r bal))
joinˡ⁺-here⁺ k₂ (0# , t₁) t₃ bal p = here p
joinˡ⁺-here⁺ k₂ (1# , t₁) t₃ ∼0 p = here p
joinˡ⁺-here⁺ k₂ (1# , t₁) t₃ ∼+ p = here p
joinˡ⁺-here⁺ k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼- p = right (here p)
joinˡ⁺-here⁺ k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼- p = right (here p)
joinˡ⁺-here⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼- p = right (here p)
joinˡ⁺-left⁺ : ∀ {l u hˡ hʳ h} →
(k : K& V) →
(l : ∃ λ i → Tree V l [ k .key ] (i ⊕ hˡ)) →
(r : Tree V [ k .key ] u hʳ) →
(bal : hˡ ∼ hʳ ⊔ h) →
Any P (proj₂ l) → Any P (proj₂ (joinˡ⁺ k l r bal))
joinˡ⁺-left⁺ k₂ (0# , t₁) t₃ bal p = left p
joinˡ⁺-left⁺ k₂ (1# , t₁) t₃ ∼0 p = left p
joinˡ⁺-left⁺ k₂ (1# , t₁) t₃ ∼+ p = left p
joinˡ⁺-left⁺ k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼- (here p) = here p
joinˡ⁺-left⁺ k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼- (left p) = left p
joinˡ⁺-left⁺ k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼- (right p) = right (left p)
joinˡ⁺-left⁺ k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼- (here p) = here p
joinˡ⁺-left⁺ k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼- (left p) = left p
joinˡ⁺-left⁺ k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼- (right p) = right (left p)
joinˡ⁺-left⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼- (here p) = left (here p)
joinˡ⁺-left⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼- (left p) = left (left p)
joinˡ⁺-left⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼- (right (here p)) = here p
joinˡ⁺-left⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼- (right (left p)) = left (right p)
joinˡ⁺-left⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼- (right (right p)) = right (left p)
joinˡ⁺-right⁺ : ∀ {l u hˡ hʳ h} →
(kv@(k , v) : K& V) →
(l : ∃ λ i → Tree V l [ k ] (i ⊕ hˡ)) →
(r : Tree V [ k ] u hʳ) →
(bal : hˡ ∼ hʳ ⊔ h) →
Any P r → Any P (proj₂ (joinˡ⁺ kv l r bal))
joinˡ⁺-right⁺ k₂ (0# , t₁) t₃ bal p = right p
joinˡ⁺-right⁺ k₂ (1# , t₁) t₃ ∼0 p = right p
joinˡ⁺-right⁺ k₂ (1# , t₁) t₃ ∼+ p = right p
joinˡ⁺-right⁺ k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼- p = right (right p)
joinˡ⁺-right⁺ k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼- p = right (right p)
joinˡ⁺-right⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼- p = right (right p)
joinʳ⁺-here⁺ : ∀ {l u hˡ hʳ h} →
(kv : K& V) →
(l : Tree V l [ kv .key ] hˡ) →
(r : ∃ λ i → Tree V [ kv .key ] u (i ⊕ hʳ)) →
(bal : hˡ ∼ hʳ ⊔ h) →
P kv → Any P (proj₂ (joinʳ⁺ kv l r bal))
joinʳ⁺-here⁺ k₂ t₁ (0# , t₃) bal p = here p
joinʳ⁺-here⁺ k₂ t₁ (1# , t₃) ∼0 p = here p
joinʳ⁺-here⁺ k₂ t₁ (1# , t₃) ∼- p = here p
joinʳ⁺-here⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+) ∼+ p = left (here p)
joinʳ⁺-here⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0) ∼+ p = left (here p)
joinʳ⁺-here⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+ p = left (here p)
joinʳ⁺-left⁺ : ∀ {l u hˡ hʳ h} →
(kv : K& V) →
(l : Tree V l [ kv .key ] hˡ) →
(r : ∃ λ i → Tree V [ kv .key ] u (i ⊕ hʳ)) →
(bal : hˡ ∼ hʳ ⊔ h) →
Any P l → Any P (proj₂ (joinʳ⁺ kv l r bal))
joinʳ⁺-left⁺ k₂ t₁ (0# , t₃) bal p = left p
joinʳ⁺-left⁺ k₂ t₁ (1# , t₃) ∼0 p = left p
joinʳ⁺-left⁺ k₂ t₁ (1# , t₃) ∼- p = left p
joinʳ⁺-left⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+) ∼+ p = left (left p)
joinʳ⁺-left⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0) ∼+ p = left (left p)
joinʳ⁺-left⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+ p = left (left p)
joinʳ⁺-right⁺ : ∀ {l u hˡ hʳ h} →
(kv : K& V) →
(l : Tree V l [ kv .key ] hˡ) →
(r : ∃ λ i → Tree V [ kv .key ] u (i ⊕ hʳ)) →
(bal : hˡ ∼ hʳ ⊔ h) →
Any P (proj₂ r) → Any P (proj₂ (joinʳ⁺ kv l r bal))
joinʳ⁺-right⁺ k₂ t₁ (0# , t₃) bal p = right p
joinʳ⁺-right⁺ k₂ t₁ (1# , t₃) ∼0 p = right p
joinʳ⁺-right⁺ k₂ t₁ (1# , t₃) ∼- p = right p
joinʳ⁺-right⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+) ∼+ (here p) = here p
joinʳ⁺-right⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+) ∼+ (left p) = left (right p)
joinʳ⁺-right⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+) ∼+ (right p) = right p
joinʳ⁺-right⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0) ∼+ (here p) = here p
joinʳ⁺-right⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0) ∼+ (left p) = left (right p)
joinʳ⁺-right⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0) ∼+ (right p) = right p
joinʳ⁺-right⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+ (here p) = right (here p)
joinʳ⁺-right⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+ (left (here p)) = here p
joinʳ⁺-right⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+ (left (left p)) = left (right p)
joinʳ⁺-right⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+ (left (right p)) = right (left p)
joinʳ⁺-right⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+ (right p) = right (right p)
joinˡ⁺⁻ : ∀ {l u hˡ hʳ h} →
(kv@(k , v) : K& V) →
(l : ∃ λ i → Tree V l [ k ] (i ⊕ hˡ)) →
(r : Tree V [ k ] u hʳ) →
(bal : hˡ ∼ hʳ ⊔ h) →
Any P (proj₂ (joinˡ⁺ kv l r bal)) →
P kv ⊎ Any P (proj₂ l) ⊎ Any P r
joinˡ⁺⁻ k₂ (0# , t₁) t₃ ba = Any.toSum
joinˡ⁺⁻ k₂ (1# , t₁) t₃ ∼0 = Any.toSum
joinˡ⁺⁻ k₂ (1# , t₁) t₃ ∼+ = Any.toSum
joinˡ⁺⁻ k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼- = λ where
(left p) → inj₂ (inj₁ (left p))
(here p) → inj₂ (inj₁ (here p))
(right (left p)) → inj₂ (inj₁ (right p))
(right (here p)) → inj₁ p
(right (right p)) → inj₂ (inj₂ p)
joinˡ⁺⁻ k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼- = λ where
(left p) → inj₂ (inj₁ (left p))
(here p) → inj₂ (inj₁ (here p))
(right (left p)) → inj₂ (inj₁ (right p))
(right (here p)) → inj₁ p
(right (right p)) → inj₂ (inj₂ p)
joinˡ⁺⁻ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼- = λ where
(left (left p)) → inj₂ (inj₁ (left p))
(left (here p)) → inj₂ (inj₁ (here p))
(left (right p)) → inj₂ (inj₁ (right (left p)))
(here p) → inj₂ (inj₁ (right (here p)))
(right (left p)) → inj₂ (inj₁ (right (right p)))
(right (here p)) → inj₁ p
(right (right p)) → inj₂ (inj₂ p)
joinʳ⁺⁻ : ∀ {l u hˡ hʳ h} →
(kv : K& V) →
(l : Tree V l [ kv .key ] hˡ) →
(r : ∃ λ i → Tree V [ kv .key ] u (i ⊕ hʳ)) →
(bal : hˡ ∼ hʳ ⊔ h) →
Any P (proj₂ (joinʳ⁺ kv l r bal)) →
P kv ⊎ Any P l ⊎ Any P (proj₂ r)
joinʳ⁺⁻ k₂ t₁ (0# , t₃) bal = Any.toSum
joinʳ⁺⁻ k₂ t₁ (1# , t₃) ∼0 = Any.toSum
joinʳ⁺⁻ k₂ t₁ (1# , t₃) ∼- = Any.toSum
joinʳ⁺⁻ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+) ∼+ = λ where
(left (left p)) → inj₂ (inj₁ p)
(left (here p)) → inj₁ p
(left (right p)) → inj₂ (inj₂ (left p))
(here p) → inj₂ (inj₂ (here p))
(right p) → inj₂ (inj₂ (right p))
joinʳ⁺⁻ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0) ∼+ = λ where
(left (left p)) → inj₂ (inj₁ p)
(left (here p)) → inj₁ p
(left (right p)) → inj₂ (inj₂ (left p))
(here p) → inj₂ (inj₂ (here p))
(right p) → inj₂ (inj₂ (right p))
joinʳ⁺⁻ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+ = λ where
(left (left p)) → inj₂ (inj₁ p)
(left (here p)) → inj₁ p
(left (right p)) → inj₂ (inj₂ (left (left p)))
(here p) → inj₂ (inj₂ (left (here p)))
(right (left p)) → inj₂ (inj₂ (left (right p)))
(right (here p)) → inj₂ (inj₂ (here p))
(right (right p)) → inj₂ (inj₂ (right p))
module _ {V : Value v} where
private
Val = Value.family V
Val≈ = Value.respects V
singleton⁺ : {P : Pred (K& V) p} →
(k : Key) →
(v : Val k) →
(l<k<u : l < k < u) →
P (k , v) → Any P (singleton k v l<k<u)
singleton⁺ k v l<k<u Pkv = here Pkv
singleton⁻ : {P : Pred (K& V) p} →
(k : Key) →
(v : Val k) →
(l<k<u : l < k < u) →
Any P (singleton k v l<k<u) → P (k , v)
singleton⁻ k v l<k<u (here Pkv) = Pkv
----------------------------------------------------------------------
-- insert
module _ (k : Key) (f : Maybe (Val k) → Val k) where
open <-Reasoning AVL.strictPartialOrder
Any-insertWith-nothing : (t : Tree V l u n) (seg : l < k < u) →
P (k , f nothing) →
¬ (Any ((k ≈_) ∘′ key) t) → Any P (proj₂ (insertWith k f t seg))
Any-insertWith-nothing (leaf l<u) seg pr ¬p = here pr
Any-insertWith-nothing (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr ¬p
with compare k k′
... | tri≈ _ k≈k′ _ = contradiction (here k≈k′) ¬p
... | tri< k<k′ _ _ = let seg′ = l<k , [ k<k′ ]ᴿ; lk′ = insertWith k f lk seg′
ih = Any-insertWith-nothing lk seg′ pr (λ p → ¬p (left p))
in joinˡ⁺-left⁺ kv lk′ ku bal ih
... | tri> _ _ k>k′ = let seg′ = [ k>k′ ]ᴿ , k<u; ku′ = insertWith k f ku seg′
ih = Any-insertWith-nothing ku seg′ pr (λ p → ¬p (right p))
in joinʳ⁺-right⁺ kv lk ku′ bal ih
Any-insertWith-just : (t : Tree V l u n) (seg : l < k < u) →
(pr : ∀ k′ v → (eq : k ≈ k′) → P (k′ , Val≈ eq (f (just (Val≈ (sym eq) v))))) →
Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insertWith k f t seg))
Any-insertWith-just (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr p
with p | compare k k′
-- happy paths
... | here _ | tri≈ _ k≈k′ _ = here (pr k′ v k≈k′)
... | left lp | tri< k<k′ _ _ = let seg′ = l<k , [ k<k′ ]ᴿ; lk′ = insertWith k f lk seg′ in
joinˡ⁺-left⁺ kv lk′ ku bal (Any-insertWith-just lk seg′ pr lp)
... | right rp | tri> _ _ k>k′ = let seg′ = [ k>k′ ]ᴿ , k<u; ku′ = insertWith k f ku seg′ in
joinʳ⁺-right⁺ kv lk ku′ bal (Any-insertWith-just ku seg′ pr rp)
-- impossible cases
... | here eq | tri< k<k′ _ _ = begin-contradiction
[ k ] <⟨ [ k<k′ ]ᴿ ⟩
[ k′ ] ≈⟨ [ sym eq ]ᴱ ⟩
[ k ] ∎
... | here eq | tri> _ _ k>k′ = begin-contradiction
[ k ] ≈⟨ [ eq ]ᴱ ⟩
[ k′ ] <⟨ [ k>k′ ]ᴿ ⟩
[ k ] ∎
... | left lp | tri≈ _ k≈k′ _ = begin-contradiction
let k″ = Any.lookup lp .key; k≈k″ = lookup-result lp; (_ , k″<k′) = lookup-bounded lp in
[ k ] ≈⟨ [ k≈k″ ]ᴱ ⟩
[ k″ ] <⟨ k″<k′ ⟩
[ k′ ] ≈⟨ [ sym k≈k′ ]ᴱ ⟩
[ k ] ∎
... | left lp | tri> _ _ k>k′ = begin-contradiction
let k″ = Any.lookup lp .key; k≈k″ = lookup-result lp; (_ , k″<k′) = lookup-bounded lp in
[ k ] ≈⟨ [ k≈k″ ]ᴱ ⟩
[ k″ ] <⟨ k″<k′ ⟩
[ k′ ] <⟨ [ k>k′ ]ᴿ ⟩
[ k ] ∎
... | right rp | tri< k<k′ _ _ = begin-contradiction
let k″ = Any.lookup rp .key; k≈k″ = lookup-result rp; (k′<k″ , _) = lookup-bounded rp in
[ k ] <⟨ [ k<k′ ]ᴿ ⟩
[ k′ ] <⟨ k′<k″ ⟩
[ k″ ] ≈⟨ [ sym k≈k″ ]ᴱ ⟩
[ k ] ∎
... | right rp | tri≈ _ k≈k′ _ = begin-contradiction
let k″ = Any.lookup rp .key; k≈k″ = lookup-result rp; (k′<k″ , _) = lookup-bounded rp in
[ k ] ≈⟨ [ k≈k′ ]ᴱ ⟩
[ k′ ] <⟨ k′<k″ ⟩
[ k″ ] ≈⟨ [ sym k≈k″ ]ᴱ ⟩
[ k ] ∎
module _ (k : Key) (v : Val k) (t : Tree V l u n) (seg : l < k < u) where
Any-insert-nothing : P (k , v) → ¬ (Any ((k ≈_) ∘′ key) t) → Any P (proj₂ (insert k v t seg))
Any-insert-nothing = Any-insertWith-nothing k (F.const v) t seg
Any-insert-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , Val≈ eq v)) →
Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insert k v t seg))
Any-insert-just pr = Any-insertWith-just k (F.const v) t seg (λ k′ _ eq → pr k′ eq)
module _ (k : Key) (f : Maybe (Val k) → Val k) where
insertWith⁺ : (t : Tree V l u n) (seg : l < k < u) →
(p : Any P t) → k ≉ Any.lookupKey p →
Any P (proj₂ (insertWith k f t seg))
insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (here p) k≉
with compare k k′
... | tri< k<k′ _ _ = let l′ = insertWith k f l (l<k , [ k<k′ ]ᴿ)
in joinˡ⁺-here⁺ kv l′ r bal p
... | tri≈ _ k≈k′ _ = contradiction k≈k′ k≉
... | tri> _ _ k′<k = let r′ = insertWith k f r ([ k′<k ]ᴿ , k<u)
in joinʳ⁺-here⁺ kv l r′ bal p
insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (left p) k≉
with compare k k′
... | tri< k<k′ _ _ = let l′ = insertWith k f l (l<k , [ k<k′ ]ᴿ)
ih = insertWith⁺ l (l<k , [ k<k′ ]ᴿ) p k≉
in joinˡ⁺-left⁺ kv l′ r bal ih
... | tri≈ _ k≈k′ _ = left p
... | tri> _ _ k′<k = let r′ = insertWith k f r ([ k′<k ]ᴿ , k<u)
in joinʳ⁺-left⁺ kv l r′ bal p
insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (right p) k≉
with compare k k′
... | tri< k<k′ _ _ = let l′ = insertWith k f l (l<k , [ k<k′ ]ᴿ)
in joinˡ⁺-right⁺ kv l′ r bal p
... | tri≈ _ k≈k′ _ = right p
... | tri> _ _ k′<k = let r′ = insertWith k f r ([ k′<k ]ᴿ , k<u)
ih = insertWith⁺ r ([ k′<k ]ᴿ , k<u) p k≉
in joinʳ⁺-right⁺ kv l r′ bal ih
insert⁺ : (k : Key) (v : Val k) (t : Tree V l u n) (seg : l < k < u) →
(p : Any P t) → k ≉ Any.lookupKey p →
Any P (proj₂ (insert k v t seg))
insert⁺ k v = insertWith⁺ k (F.const v)
module _
{P : Pred (K& V) p}
(P-Resp : ∀ {k k′ v} → (k≈k′ : k ≈ k′) → P (k′ , Val≈ k≈k′ v) → P (k , v))
(k : Key) (v : Val k)
where
insert⁻ : (t : Tree V l u n) (seg : l < k < u) →
Any P (proj₂ (insert k v t seg)) →
P (k , v) ⊎ Any (λ{ (k′ , v′) → k ≉ k′ × P (k′ , v′)}) t
insert⁻ (leaf l<u) seg (here p) = inj₁ p
insert⁻ (node kv′@(k′ , v′) l r bal) (l<k , k<u) p with compare k k′
insert⁻ (node kv′@(k′ , v′) l r bal) (l<k , k<u) p | tri< k<k′ k≉k′ _
with joinˡ⁺⁻ kv′ (insert k v l (l<k , [ k<k′ ]ᴿ)) r bal p
... | inj₁ p = inj₂ (here (k≉k′ , p))
... | inj₂ (inj₂ p) = inj₂ (right (lookup-rebuild-accum p k≉p))
where
k′<p = [<]-injective (proj₁ (lookup-bounded p))
k≉p = λ k≈p → irrefl k≈p (<-trans k<k′ k′<p)
... | inj₂ (inj₁ p) = Sum.map₂ (λ q → left q) (insert⁻ l (l<k , [ k<k′ ]ᴿ) p)
insert⁻ (node kv′@(k′ , v′) l r bal) (l<k , k<u) p | tri> _ k≉k′ k′<k
with joinʳ⁺⁻ kv′ l (insert k v r ([ k′<k ]ᴿ , k<u)) bal p
... | inj₁ p = inj₂ (here (k≉k′ , p))
... | inj₂ (inj₁ p) = inj₂ (left (lookup-rebuild-accum p k≉p))
where
p<k′ = [<]-injective (proj₂ (lookup-bounded p))
k≉p = λ k≈p → irrefl (sym k≈p) (<-trans p<k′ k′<k)
... | inj₂ (inj₂ p) = Sum.map₂ (λ q → right q) (insert⁻ r ([ k′<k ]ᴿ , k<u) p)
insert⁻ (node kv′@(k′ , v′) l r bal) (l<k , k<u) p | tri≈ _ k≈k′ _
with p
... | left p = inj₂ (left (lookup-rebuild-accum p k≉p))
where
p<k′ = [<]-injective (proj₂ (lookup-bounded p))
k≉p = λ k≈p → irrefl (trans (sym k≈p) k≈k′) p<k′
... | here p = inj₁ (P-Resp k≈k′ p)
... | right p = inj₂ (right (lookup-rebuild-accum p k≉p))
where
k′<p = [<]-injective (proj₁ (lookup-bounded p))
k≉p = λ k≈p → irrefl (trans (sym k≈k′) k≈p) k′<p
lookup⁺ : (t : Tree V l u n) (k : Key) (seg : l < k < u) →
(p : Any P t) →
key (Any.lookup p) ≉ k ⊎ ∃[ p≈k ] AVL.lookup t k seg ≡ just (Val≈ p≈k (value (Any.lookup p)))
lookup⁺ (node (k′ , v′) l r bal) k (l<k , k<u) p
with compare k′ k | p
... | tri< k′<k _ _ | right p = lookup⁺ r k ([ k′<k ]ᴿ , k<u) p
... | tri≈ _ k′≈k _ | here p = inj₂ (k′≈k , ≡-refl)
... | tri> _ _ k<k′ | left p = lookup⁺ l k (l<k , [ k<k′ ]ᴿ) p
... | tri< k′<k _ _ | left p = inj₁ (λ p≈k → irrefl p≈k (<-trans p<k′ k′<k))
where p<k′ = [<]-injective (proj₂ (lookup-bounded p))
... | tri< k′<k _ _ | here p = inj₁ (λ p≈k → irrefl p≈k k′<k)
... | tri≈ _ k′≈k _ | left p = inj₁ (λ p≈k → irrefl (trans p≈k (sym k′≈k)) p<k′)
where p<k′ = [<]-injective (proj₂ (lookup-bounded p))
... | tri≈ _ k′≈k _ | right p = inj₁ (λ p≈k → irrefl (trans k′≈k (sym p≈k)) k′<p)
where k′<p = [<]-injective (proj₁ (lookup-bounded p))
... | tri> _ _ k<k′ | here p = inj₁ (λ p≈k → irrefl (sym p≈k) k<k′)
... | tri> _ _ k<k′ | right p = inj₁ (λ p≈k → irrefl (sym p≈k) (<-trans k<k′ k′<p))
where k′<p = [<]-injective (proj₁ (lookup-bounded p))
lookup⁻ : (t : Tree V l u n) (k : Key) (v : Val k) (seg : l < k < u) →
AVL.lookup t k seg ≡ just v →
Any (λ{ (k′ , v′) → ∃ λ k′≈k → Val≈ k′≈k v′ ≡ v}) t
lookup⁻ (node (k′ , v′) l r bal) k v (l<k , k<u) eq with compare k′ k
... | tri< k′<k _ _ = right (lookup⁻ r k v ([ k′<k ]ᴿ , k<u) eq)
... | tri≈ _ k′≈k _ = here (k′≈k , just-injective eq)
... | tri> _ _ k<k′ = left (lookup⁻ l k v (l<k , [ k<k′ ]ᴿ) eq)
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