Add properties that characterize Data.Tree.AVL.Indexed.delete.

src/Data/Tree/AVL/Indexed/Relation/Unary/Any/AnyLookup.agda

@@ -0,0 +1,50 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties related to Any.lookup
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (StrictTotalOrder)
+
+module Data.Tree.AVL.Indexed.Relation.Unary.Any.AnyLookup
+  {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
+  where
+
+open import Data.Nat.Base using (ℕ)
+open import Data.Product.Base as Prod using (_,_)
+open import Function.Base using (flip)
+open import Level using (Level)
+open import Relation.Unary using (Pred; _∩_)
+
+open import Data.Tree.AVL.Indexed sto
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
+
+private
+  variable
+    v p : Level
+    V : Value v
+    l u : Key⁺
+    n : ℕ
+    P Q : Pred (K& V) p
+
+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)

src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Cast.agda

@@ -0,0 +1,37 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of castʳ related to Any
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (StrictTotalOrder)
+
+module Data.Tree.AVL.Indexed.Relation.Unary.Any.Cast
+  {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
+  where
+
+open import Level using (Level)
+open import Relation.Unary using (Pred)
+
+open import Data.Tree.AVL.Indexed sto
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
+
+private
+  variable
+    v p : Level
+    V : Value v
+    P : Pred (K& V) p
+
+castʳ⁺ : ∀ {l m u h} {lm : Tree V l m h} {m<u : m <⁺ u} →
+         Any P lm → Any P (castʳ lm m<u)
+castʳ⁺ (here p) = here p
+castʳ⁺ (left p) = left p
+castʳ⁺ (right p) = right (castʳ⁺ p)
+
+castʳ⁻ : ∀ {l m u h} {lm : Tree V l m h} {m<u : m <⁺ u} →
+         Any P (castʳ lm m<u) → Any P lm
+castʳ⁻ {lm = node _ _ _ _} (here p) = here p
+castʳ⁻ {lm = node _ _ _ _} (left p) = left p
+castʳ⁻ {lm = node _ _ _ _} (right p) = right (castʳ⁻ p)

src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Delete.agda

@@ -0,0 +1,160 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of delete related to Any
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (StrictTotalOrder)
+
+module Data.Tree.AVL.Indexed.Relation.Unary.Any.Delete
+  {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
+  where
+
+open import Data.Nat.Base using (ℕ)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Data.Sum.Base using (inj₁; inj₂)
+open import Function.Base using (_∘′_)
+open import Level using (Level)
+open import Relation.Binary.Definitions using (tri<; tri≈; tri>)
+open import Relation.Nullary.Negation.Core using (contradiction)
+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 import Data.Tree.AVL.Indexed.Relation.Unary.Any.AnyLookup sto
+  using (lookup-bounded; lookup-result; lookup-rebuild)
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Join sto
+  using (join-left⁺; join-right⁺; join-node⁻; join⁻)
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any.JoinConstFuns sto
+  using (joinʳ⁻-here⁺; joinʳ⁻-left⁺; joinʳ⁻-right⁺; joinˡ⁻-here⁺;
+         joinˡ⁻-left⁺; joinˡ⁻-right⁺; joinʳ⁻⁻; joinˡ⁻⁻)
+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 : Level
+    V : Value v
+    l u : Key⁺
+    n : ℕ
+    P : Pred (K& V) p
+
+module _ {V : Value v} where
+
+  module _ (k : Key) where
+
+    delete⁺ : (t : Tree V l u n) (seg : l < k < u) →
+              (p : Any P t) → lookupKey p ≉ k →
+              Any P (proj₂ (delete k t seg))
+    delete⁺ (leaf _) _ p _ = p
+    delete⁺ (node (k′ , v) lk′ k′u bal) (l<k , k<u) p p≉k
+      with compare k′ k
+    delete⁺ (node kv@(k′ , v) lk′ k′u bal) (l<k , k<u) p p≉k
+      | tri< k′<k _ _ with p
+    ... | here pk =
+      joinʳ⁻-here⁺ kv lk′ (delete k k′u ([ k′<k ]ᴿ , k<u)) bal pk
+    ... | left pl =
+      joinʳ⁻-left⁺ kv lk′ (delete k k′u ([ k′<k ]ᴿ , k<u)) bal pl
+    ... | right pr =
+      joinʳ⁻-right⁺ kv lk′ (delete k k′u ([ k′<k ]ᴿ , k<u)) bal
+        (delete⁺ k′u ([ k′<k ]ᴿ , k<u) pr p≉k)
+    delete⁺ (node kv@(k′ , v) lk′ k′u bal) (l<k , k<u) p p≉k
+      | tri> _ _ k′>k with p
+    ... | here pk =
+      joinˡ⁻-here⁺ kv (delete k lk′ (l<k , [ k′>k ]ᴿ)) k′u bal pk
+    ... | left pl =
+      joinˡ⁻-left⁺ kv (delete k lk′ (l<k , [ k′>k ]ᴿ)) k′u bal
+        ((delete⁺ lk′ (l<k , [ k′>k ]ᴿ)) pl p≉k)
+    ... | right pr =
+      joinˡ⁻-right⁺ kv (delete k lk′ (l<k , [ k′>k ]ᴿ)) k′u bal pr
+    delete⁺ (node (k′ , v) lk′ k′u bal) (l<k , k<u) p p≉k
+      | tri≈ _ k′≈k _ with p
+    ... | here pk = contradiction k′≈k p≉k
+    ... | left pl = join-left⁺ lk′ k′u bal pl
+    ... | right pr = join-right⁺ lk′ k′u bal pr
+
+    delete-tree⁻ : (t : Tree V l u n) (seg : l < k < u) →
+                   Any P (proj₂ (delete k t seg)) →
+                   Any P t
+    delete-tree⁻ (node (k′ , v) lk′ k′u bal) (l<k , k<u) p
+      with compare k′ k
+    delete-tree⁻ (node kv@(k′ , v) lk′ k′u bal) (l<k , k<u) p
+      | tri< k′<k _ _
+      with joinʳ⁻⁻ kv lk′ (delete k k′u ([ k′<k ]ᴿ , k<u)) bal p
+    ... | inj₁ pk = here pk
+    ... | inj₂ (inj₁ pl) = left pl
+    ... | inj₂ (inj₂ pr) = right (delete-tree⁻ k′u ([ k′<k ]ᴿ , k<u) pr)
+    delete-tree⁻ (node kv@(k′ , v) lk′ k′u bal) (l<k , k<u) p
+      | tri> _ _ k′>k
+      with joinˡ⁻⁻ kv (delete k lk′ (l<k , [ k′>k ]ᴿ)) k′u bal p
+    ... | inj₁ pk = here pk
+    ... | inj₂ (inj₁ pl) = left (delete-tree⁻ lk′ (l<k , [ k′>k ]ᴿ) pl)
+    ... | inj₂ (inj₂ pr) = right pr
+    delete-tree⁻ (node (k′ , v) lk′ k′u bal) (l<k , k<u) p
+      | tri≈ _ _ _ =
+      join-node⁻ v lk′ k′u bal p
+
+
+  module _ (k : Key) where
+
+    open <-Reasoning AVL.strictPartialOrder
+
+    delete-key-∈⁻ : (t : Tree V l u n) (seg : l < k < u) →
+                    {kp : Key} →
+                    Any ((kp ≈_) ∘′ key) (proj₂ (delete k t seg)) →
+                    kp ≉ k
+    delete-key-∈⁻ (node (k′ , v) lk′ k′u bal) (l<k , k<u) p kp≈k
+      with compare k′ k
+    delete-key-∈⁻ (node kv@(k′ , v) lk′ k′u bal) (l<k , k<u) {kp} p kp≈k
+      | tri< k′<k k′≉k _
+      with joinʳ⁻⁻ kv lk′ (delete k k′u ([ k′<k ]ᴿ , k<u)) bal p
+    ... | inj₁ kp≈k′ = contradiction (trans (sym kp≈k′) kp≈k) k′≉k
+    ... | inj₂ (inj₁ pl) = begin-contradiction
+      [ k  ]                ≈⟨ [ sym kp≈k ]ᴱ ⟩
+      [ kp ]                ≈⟨ [ lookup-result pl ]ᴱ ⟩
+      [ Any.lookupKey pl ]  <⟨ proj₂ (lookup-bounded pl) ⟩
+      [ k′ ]                <⟨ [ k′<k ]ᴿ ⟩
+      [ k  ]                ∎
+    ... | inj₂ (inj₂ pr) = delete-key-∈⁻ k′u ([ k′<k ]ᴿ , k<u) pr kp≈k
+    delete-key-∈⁻ (node kv@(k′ , v) lk′ k′u bal) (l<k , k<u) {kp} p kp≈k
+      | tri> _ k′≉k k′>k
+      with joinˡ⁻⁻ kv (delete k lk′ (l<k , [ k′>k ]ᴿ)) k′u bal p
+    ... | inj₁ kp≈k′ = contradiction (trans (sym kp≈k′) kp≈k) k′≉k
+    ... | inj₂ (inj₁ pl) = delete-key-∈⁻ lk′ (l<k , [ k′>k ]ᴿ) pl kp≈k
+    ... | inj₂ (inj₂ pr) = begin-contradiction
+      [ k  ]                <⟨ [ k′>k ]ᴿ ⟩
+      [ k′ ]                <⟨ proj₁ (lookup-bounded pr) ⟩
+      [ Any.lookupKey pr ]  ≈⟨ [ sym (lookup-result pr) ]ᴱ ⟩
+      [ kp ]                ≈⟨ [ kp≈k ]ᴱ ⟩
+      [ k  ]                ∎
+    delete-key-∈⁻ (node (k′ , v) lk′ k′u bal) (l<k , k<u) {kp} p kp≈k
+      | tri≈ k′≮k _ k′≯k
+      with join⁻ lk′ k′u bal p
+    ... | inj₁ p₁ = contradiction
+      (begin-strict
+        [ k  ]                ≈⟨ [ sym kp≈k ]ᴱ ⟩
+        [ kp ]                ≈⟨ [ lookup-result p₁ ]ᴱ ⟩
+        [ Any.lookupKey p₁ ]  <⟨ proj₂ (lookup-bounded p₁) ⟩
+        [ k′ ]                ∎)
+      (k′≯k ∘′ [<]-injective)
+    ... | inj₂ p₂ = contradiction
+      (begin-strict
+        [ k′  ]               <⟨ proj₁ (lookup-bounded p₂) ⟩
+        [ Any.lookupKey p₂ ]  ≈⟨ [ sym (lookup-result p₂) ]ᴱ ⟩
+        [ kp ]                ≈⟨ [ kp≈k ]ᴱ ⟩
+        [ k ]                 ∎)
+      (k′≮k ∘′ [<]-injective)
+
+
+  module _ (k : Key) where
+
+    delete-key⁻ : (t : Tree V l u n) (seg : l < k < u) →
+                  (p : Any P (proj₂ (delete k t seg))) →
+                  Any.lookupKey p ≉ k
+    delete-key⁻ t seg p kp≈k =
+      delete-key-∈⁻ k t seg (lookup-rebuild p Eq.refl) kp≈k

src/Data/Tree/AVL/Indexed/Relation/Unary/Any/HeadTail.agda

@@ -0,0 +1,74 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of headTail related to Any
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (StrictTotalOrder)
+
+module Data.Tree.AVL.Indexed.Relation.Unary.Any.HeadTail
+  {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
+  where
+
+open import Data.Nat.Base using (suc; _+_)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality.Core renaming (refl to ≡-refl)
+open import Relation.Unary using (Pred)
+
+open import Data.Tree.AVL.Indexed sto
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any.JoinConstFuns sto
+  using (joinˡ⁻-here⁺; joinˡ⁻-left⁺; joinˡ⁻-right⁺; joinˡ⁻⁻)
+
+private
+  variable
+    v p : Level
+    V : Value v
+    P : Pred (K& V) p
+
+headTail⁺ : ∀ {l u h} (t : Tree V l u (1 + h)) →
+            Any P t →
+            P (proj₁ (headTail t))
+            ⊎ Any P (proj₂ (proj₂ (proj₂ (headTail t))))
+headTail⁺ (node _ (leaf _) _ ∼+) (here p) = inj₁ p
+headTail⁺ (node _ (leaf _) _ ∼+) (right p) = inj₂ p
+headTail⁺ (node _ (leaf _) _ ∼0) (here p) = inj₁ p
+headTail⁺ (node {hˡ = suc _} k₃ t₁₂@(node _ _ _ _) t₄ bal) (here p)
+  with headTail t₁₂
+... | k₁ , l<k₁ , t₂ = inj₂ (joinˡ⁻-here⁺ k₃ t₂ t₄ bal p)
+headTail⁺ (node {hˡ = suc _} k₃ t₁₂@(node _ _ _ _) t₄ bal) (left p)
+  with headTail t₁₂ | headTail⁺ t₁₂ p
+... | k₁ , l<k₁ , t₂ | inj₁ ph = inj₁ ph
+... | k₁ , l<k₁ , t₂ | inj₂ pt = inj₂ (joinˡ⁻-left⁺ k₃ t₂ t₄ bal pt)
+headTail⁺ (node {hˡ = suc _} k₃ t₁₂@(node _ _ _ _) t₄ bal) (right p)
+  with headTail t₁₂
+... | k₁ , l<k₁ , t₂ = inj₂ (joinˡ⁻-right⁺ k₃ t₂ t₄ bal p)
+
+headTail-head⁻ : ∀ {l u h} → (t : Tree V l u (suc h)) →
+                 P (proj₁ (headTail t)) → Any P t
+headTail-head⁻ (node _ (leaf _) _ ∼+) p = here p
+headTail-head⁻ (node _ (leaf _) _ ∼0) p = here p
+headTail-head⁻ (node {hˡ = suc _} _ t₁₂ _ _) p
+  with headTail t₁₂
+headTail-head⁻ (node {hˡ = suc _} _ t₁₂@(node _ _ _ _) _ _) p
+  | k₁ , l<k₁ , t₂ = left (headTail-head⁻ t₁₂ p)
+
+headTail-tail⁻ : ∀ {l u h} (t : Tree V l u (1 + h)) →
+                 Any P (proj₂ (proj₂ (proj₂ (headTail t)))) →
+                 Any P t
+headTail-tail⁻ (node _ (leaf _) _ ∼+) p = right p
+headTail-tail⁻ (node _ (leaf _) _ ∼0) p = right p
+headTail-tail⁻ (node {hˡ = suc _} k₃ t₁₂@(node _ _ _ _) t₄ bal) p
+  with k₁ , l<k₁ , t₂ ← headTail t₁₂ in eq
+     -- This match on `bal` is so the termination checker sees `h`
+     -- decrease.
+     | joinˡ⁻⁻ k₃ t₂ t₄ bal p | bal | eq
+... | inj₁ pk | _ | ≡-refl = here pk
+... | inj₂ (inj₁ pl) | ∼+ | ≡-refl = left (headTail-tail⁻ t₁₂ pl)
+... | inj₂ (inj₁ pl) | ∼0 | ≡-refl = left (headTail-tail⁻ t₁₂ pl)
+... | inj₂ (inj₁ pl) | ∼- | ≡-refl = left (headTail-tail⁻ t₁₂ pl)
+... | inj₂ (inj₂ pr) | _ | ≡-refl = right pr