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

src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/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.Properties.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/Properties/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.Properties.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/Properties/Delete.agda

@@ -0,0 +1,145 @@
+------------------------------------------------------------------------
+-- 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.Properties.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 as Sum 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.Properties.AnyLookup sto
+  using (lookup-bounded; lookup-result; lookup-rebuild)
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Join sto
+  using (join-left⁺; join-right⁺; join⁻)
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.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 _ (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⁺ (node (k′ , _) _ _ bal) _ (here pk) p≉k
+    with compare k′ k
+  ... | tri< _ _ _    = joinʳ⁻-here⁺ _ _ _ bal pk
+  ... | tri> _ _ _    = joinˡ⁻-here⁺ _ _ _ bal pk
+  ... | tri≈ _ k′≈k _ = contradiction k′≈k p≉k
+  delete⁺ (node (k′ , _) lk′ k′u bal) (l<k , _) (left pl) p≉k
+    with compare k′ k
+  ... | tri< _ _ _    = joinʳ⁻-left⁺ _ _ _ bal pl
+  ... | tri> _ _ k′>k = joinˡ⁻-left⁺ _ _ _ bal
+                          (delete⁺ lk′ (l<k , [ k′>k ]ᴿ) pl p≉k)
+  ... | tri≈ _ _ _    = join-left⁺ _ k′u bal pl
+  delete⁺ (node (k′ , _) _ k′u bal) (_ , k<u) (right pr) p≉k
+    with compare k′ k
+  ... | tri< k′<k _ _ = joinʳ⁻-right⁺ _ _ _ bal
+                          (delete⁺ k′u ([ k′<k ]ᴿ , k<u) pr p≉k)
+  ... | tri> _ _ k′>k = joinˡ⁻-right⁺ _ _ _ bal pr
+  ... | tri≈ _ _ _    = join-right⁺ _ _ 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′ , _) _ _ _) _ _ with compare k′ k
+  delete-tree⁻ (node kv _ k′u bal) (_ , k<u) p | tri< k′<k _ _
+    with joinʳ⁻⁻ _ _ _ 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 lk′ _ bal) (l<k , _) p | tri> _ _ k′>k
+    with joinˡ⁻⁻ _ _ _ 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 _ lk′ k′u bal) _ p | tri≈ _ _ _ =
+    Sum.[ (λ p → left p) , (λ p → right p) ]′ (join⁻ 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′ , _) _ _ _) _ _ _
+    with compare k′ k
+  delete-key-∈⁻ (node (k′ , _) _ k′u bal) (_ , k<u) {kp} p kp≈k
+    | tri< k′<k k′≉k _
+    with joinʳ⁻⁻ _ _ _ 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 (k′ , _) lk′ _ bal) (l<k , _) {kp} p kp≈k
+    | tri> _ k′≉k k′>k
+    with joinˡ⁻⁻ _ _ _ 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′ , _) _ k′u bal) _ {kp} p kp≈k
+    | tri≈ k′≮k _ k′≯k
+    with join⁻ _ 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/Properties/HeadTail.agda

@@ -0,0 +1,71 @@
+------------------------------------------------------------------------
+-- 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.Properties.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 as Sum using (_⊎_; inj₁; inj₂)
+open import Function using (id)
+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.Properties.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)) →
+            let _ , _ , _ , t⁻ = headTail t in
+            Any P t → P (proj₁ (headTail t)) ⊎ Any P 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 k₃ t₁₂@(node _ _ _ _) t₄ bal) (here p)
+  = let _ , _ , t₂ = headTail t₁₂
+    in inj₂ (joinˡ⁻-here⁺ k₃ t₂ t₄ bal p)
+headTail⁺ (node k₃ t₁₂@(node _ _ _ _) t₄ bal) (left p)
+  = let _ , _ , t₂ = headTail t₁₂
+    in Sum.map id (joinˡ⁻-left⁺ k₃ t₂ t₄ bal) (headTail⁺ t₁₂ p)
+headTail⁺ (node k₃ t₁₂@(node _ _ _ _) t₄ bal) (right p)
+  = let _ , _ , t₂ = headTail t₁₂
+    in 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 _ t₁₂@(node _ _ _ _) _ _) p =
+  left (headTail-head⁻ t₁₂ p)
+
+headTail-tail⁻ : ∀ {l u h} (t : Tree V l u (1 + h)) →
+                 let _ , _ , _ , t⁻ = headTail t in
+                 Any P t⁻ → Any P t
+headTail-tail⁻ (node _ (leaf _) _ ∼+)              p = right p
+headTail-tail⁻ (node _ (leaf _) _ ∼0)              p = right p
+headTail-tail⁻ (node k₃ t₁₂@(node _ _ _ _) t₄ bal) p
+  using _ , _ , t₂ ← headTail t₁₂
+  with joinˡ⁻⁻ k₃ t₂ t₄ bal p
+... | inj₁ pk        = here pk
+... | inj₂ (inj₂ pr) = right pr
+... | inj₂ (inj₁ pl) using p⁻ ← headTail-tail⁻ t₁₂ pl with bal
+-- This match on `bal` shows the termination checker that `h` decreases.
+...   | ∼+ = left p⁻
+...   | ∼0 = left p⁻
+...   | ∼- = left p⁻