Skip to content

Commit bcc0843

Browse files
mikedelorimiermikedelorimier
committed
Add properties that characterize Data.Tree.AVL.Indexed.delete.
These are properties for the core delete on AVL trees and similar to the prexisting properties of `insert`. Lemmas added for `delete` are `delete⁺`, `delete-tree⁻`, `delete-key-∈⁻` and `delete-key⁻`. Together these can be used to prove `(k′ ∈ delete k t) ⇔ (k′ ≉ k × k′ ∈ t)`, which fully characterizes `delete`. `delete⁺`, `delete-tree⁻`, and `delete-key⁻` correspond to Coq.FSets.FSetInterface's `remove_2`, `remove_3`, and `remove_1`, respectively. Just like other lemmas in this file, `delete⁺`, `delete-tree⁻`, `delete-key⁻` generalize `k′ ∈ t` to `Any P t`. `delete-key-∈⁻` is essentally a helper for `delete-key⁻`, which would be difficult to prove directly. Many more lemmas were added for AVL functions that `delete` depends on. These additional lemmas characterize the functions `castʳ`, `joinˡ⁺`, `joinʳ⁺`, `joinˡ⁻`, `joinʳ⁻`, `headTail`, and `join`. Adding all this code to Properties.agda caused `make test` to overflow past the 4096 MB default heap size. This was solved by breaking Properties.agda into multiple files, with roughly one file for each AVL function. Added proofs are a similar style the preexisting proofs in Properties.agda.
1 parent 03acec1 commit bcc0843

10 files changed

Lines changed: 1060 additions & 405 deletions

File tree

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

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Properties related to Any.lookup
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe #-}
8+
9+
open import Relation.Binary.Bundles using (StrictTotalOrder)
10+
11+
module Data.Tree.AVL.Indexed.Relation.Unary.Any.AnyLookup
12+
{a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
13+
where
14+
15+
open import Data.Nat.Base using (ℕ)
16+
open import Data.Product.Base as Prod using (_,_)
17+
open import Function.Base using (flip)
18+
open import Level using (Level)
19+
open import Relation.Unary using (Pred; _∩_)
20+
21+
open import Data.Tree.AVL.Indexed sto
22+
open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
23+
24+
private
25+
variable
26+
v p : Level
27+
V : Value v
28+
l u : Key⁺
29+
n : ℕ
30+
P Q : Pred (K& V) p
31+
32+
lookup-result : {t : Tree V l u n} (p : Any P t) → P (Any.lookup p)
33+
lookup-result (here p) = p
34+
lookup-result (left p) = lookup-result p
35+
lookup-result (right p) = lookup-result p
36+
37+
lookup-bounded : {t : Tree V l u n} (p : Any P t) → l < Any.lookup p .key < u
38+
lookup-bounded {t = node kv lk ku bal} (here p) = ordered lk , ordered ku
39+
lookup-bounded {t = node kv lk ku bal} (left p) =
40+
Prod.map₂ (flip (trans⁺ _) (ordered ku)) (lookup-bounded p)
41+
lookup-bounded {t = node kv lk ku bal} (right p) =
42+
Prod.map₁ (trans⁺ _ (ordered lk)) (lookup-bounded p)
43+
44+
lookup-rebuild : {t : Tree V l u n} (p : Any P t) → Q (Any.lookup p) → Any Q t
45+
lookup-rebuild (here _) q = here q
46+
lookup-rebuild (left p) q = left (lookup-rebuild p q)
47+
lookup-rebuild (right p) q = right (lookup-rebuild p q)
48+
49+
lookup-rebuild-accum : {t : Tree V l u n} (p : Any P t) → Q (Any.lookup p) → Any (Q ∩ P) t
50+
lookup-rebuild-accum p q = lookup-rebuild p (q , lookup-result p)

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

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Properties of castʳ related to Any
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe #-}
8+
9+
open import Relation.Binary.Bundles using (StrictTotalOrder)
10+
11+
module Data.Tree.AVL.Indexed.Relation.Unary.Any.Cast
12+
{a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
13+
where
14+
15+
open import Level using (Level)
16+
open import Relation.Unary using (Pred)
17+
18+
open import Data.Tree.AVL.Indexed sto
19+
open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
20+
21+
private
22+
variable
23+
v p : Level
24+
V : Value v
25+
P : Pred (K& V) p
26+
27+
castʳ⁺ : ∀ {l m u h} {lm : Tree V l m h} {m<u : m <⁺ u} →
28+
Any P lm → Any P (castʳ lm m<u)
29+
castʳ⁺ (here p) = here p
30+
castʳ⁺ (left p) = left p
31+
castʳ⁺ (right p) = right (castʳ⁺ p)
32+
33+
castʳ⁻ : ∀ {l m u h} {lm : Tree V l m h} {m<u : m <⁺ u} →
34+
Any P (castʳ lm m<u) → Any P lm
35+
castʳ⁻ {lm = node _ _ _ _} (here p) = here p
36+
castʳ⁻ {lm = node _ _ _ _} (left p) = left p
37+
castʳ⁻ {lm = node _ _ _ _} (right p) = right (castʳ⁻ p)

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

Lines changed: 160 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,160 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Properties of delete related to Any
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe #-}
8+
9+
open import Relation.Binary.Bundles using (StrictTotalOrder)
10+
11+
module Data.Tree.AVL.Indexed.Relation.Unary.Any.Delete
12+
{a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
13+
where
14+
15+
open import Data.Nat.Base using (ℕ)
16+
open import Data.Product.Base using (_,_; proj₁; proj₂)
17+
open import Data.Sum.Base using (inj₁; inj₂)
18+
open import Function.Base using (_∘′_)
19+
open import Level using (Level)
20+
open import Relation.Binary.Definitions using (tri<; tri≈; tri>)
21+
open import Relation.Nullary.Negation.Core using (contradiction)
22+
open import Relation.Unary using (Pred)
23+
24+
open import Data.Tree.AVL.Indexed sto as AVL
25+
open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
26+
open import Data.Tree.AVL.Indexed.Relation.Unary.Any.AnyLookup sto
27+
using (lookup-bounded; lookup-result; lookup-rebuild)
28+
open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Join sto
29+
using (join-left⁺; join-right⁺; join-node⁻; join⁻)
30+
open import Data.Tree.AVL.Indexed.Relation.Unary.Any.JoinConstFuns sto
31+
using (joinʳ⁻-here⁺; joinʳ⁻-left⁺; joinʳ⁻-right⁺; joinˡ⁻-here⁺;
32+
joinˡ⁻-left⁺; joinˡ⁻-right⁺; joinʳ⁻⁻; joinˡ⁻⁻)
33+
open StrictTotalOrder sto renaming (Carrier to Key; trans to <-trans); open Eq using (sym; trans)
34+
35+
open import Relation.Binary.Construct.Add.Extrema.Strict _<_ using ([<]-injective)
36+
37+
import Relation.Binary.Reasoning.StrictPartialOrder as <-Reasoning
38+
39+
private
40+
variable
41+
v p : Level
42+
V : Value v
43+
l u : Key⁺
44+
n : ℕ
45+
P : Pred (K& V) p
46+
47+
module _ {V : Value v} where
48+
49+
module _ (k : Key) where
50+
51+
delete⁺ : (t : Tree V l u n) (seg : l < k < u) →
52+
(p : Any P t) → lookupKey p ≉ k →
53+
Any P (proj₂ (delete k t seg))
54+
delete⁺ (leaf _) _ p _ = p
55+
delete⁺ (node (k′ , v) lk′ k′u bal) (l<k , k<u) p p≉k
56+
with compare k′ k
57+
delete⁺ (node kv@(k′ , v) lk′ k′u bal) (l<k , k<u) p p≉k
58+
| tri< k′<k _ _ with p
59+
... | here pk =
60+
joinʳ⁻-here⁺ kv lk′ (delete k k′u ([ k′<k ]ᴿ , k<u)) bal pk
61+
... | left pl =
62+
joinʳ⁻-left⁺ kv lk′ (delete k k′u ([ k′<k ]ᴿ , k<u)) bal pl
63+
... | right pr =
64+
joinʳ⁻-right⁺ kv lk′ (delete k k′u ([ k′<k ]ᴿ , k<u)) bal
65+
(delete⁺ k′u ([ k′<k ]ᴿ , k<u) pr p≉k)
66+
delete⁺ (node kv@(k′ , v) lk′ k′u bal) (l<k , k<u) p p≉k
67+
| tri> _ _ k′>k with p
68+
... | here pk =
69+
joinˡ⁻-here⁺ kv (delete k lk′ (l<k , [ k′>k ]ᴿ)) k′u bal pk
70+
... | left pl =
71+
joinˡ⁻-left⁺ kv (delete k lk′ (l<k , [ k′>k ]ᴿ)) k′u bal
72+
((delete⁺ lk′ (l<k , [ k′>k ]ᴿ)) pl p≉k)
73+
... | right pr =
74+
joinˡ⁻-right⁺ kv (delete k lk′ (l<k , [ k′>k ]ᴿ)) k′u bal pr
75+
delete⁺ (node (k′ , v) lk′ k′u bal) (l<k , k<u) p p≉k
76+
| tri≈ _ k′≈k _ with p
77+
... | here pk = contradiction k′≈k p≉k
78+
... | left pl = join-left⁺ lk′ k′u bal pl
79+
... | right pr = join-right⁺ lk′ k′u bal pr
80+
81+
delete-tree⁻ : (t : Tree V l u n) (seg : l < k < u) →
82+
Any P (proj₂ (delete k t seg)) →
83+
Any P t
84+
delete-tree⁻ (node (k′ , v) lk′ k′u bal) (l<k , k<u) p
85+
with compare k′ k
86+
delete-tree⁻ (node kv@(k′ , v) lk′ k′u bal) (l<k , k<u) p
87+
| tri< k′<k _ _
88+
with joinʳ⁻⁻ kv lk′ (delete k k′u ([ k′<k ]ᴿ , k<u)) bal p
89+
... | inj₁ pk = here pk
90+
... | inj₂ (inj₁ pl) = left pl
91+
... | inj₂ (inj₂ pr) = right (delete-tree⁻ k′u ([ k′<k ]ᴿ , k<u) pr)
92+
delete-tree⁻ (node kv@(k′ , v) lk′ k′u bal) (l<k , k<u) p
93+
| tri> _ _ k′>k
94+
with joinˡ⁻⁻ kv (delete k lk′ (l<k , [ k′>k ]ᴿ)) k′u bal p
95+
... | inj₁ pk = here pk
96+
... | inj₂ (inj₁ pl) = left (delete-tree⁻ lk′ (l<k , [ k′>k ]ᴿ) pl)
97+
... | inj₂ (inj₂ pr) = right pr
98+
delete-tree⁻ (node (k′ , v) lk′ k′u bal) (l<k , k<u) p
99+
| tri≈ _ _ _ =
100+
join-node⁻ v lk′ k′u bal p
101+
102+
103+
module _ (k : Key) where
104+
105+
open <-Reasoning AVL.strictPartialOrder
106+
107+
delete-key-∈⁻ : (t : Tree V l u n) (seg : l < k < u) →
108+
{kp : Key} →
109+
Any ((kp ≈_) ∘′ key) (proj₂ (delete k t seg)) →
110+
kp ≉ k
111+
delete-key-∈⁻ (node (k′ , v) lk′ k′u bal) (l<k , k<u) p kp≈k
112+
with compare k′ k
113+
delete-key-∈⁻ (node kv@(k′ , v) lk′ k′u bal) (l<k , k<u) {kp} p kp≈k
114+
| tri< k′<k k′≉k _
115+
with joinʳ⁻⁻ kv lk′ (delete k k′u ([ k′<k ]ᴿ , k<u)) bal p
116+
... | inj₁ kp≈k′ = contradiction (trans (sym kp≈k′) kp≈k) k′≉k
117+
... | inj₂ (inj₁ pl) = begin-contradiction
118+
[ k ] ≈⟨ [ sym kp≈k ]ᴱ ⟩
119+
[ kp ] ≈⟨ [ lookup-result pl ]ᴱ ⟩
120+
[ Any.lookupKey pl ] <⟨ proj₂ (lookup-bounded pl) ⟩
121+
[ k′ ] <⟨ [ k′<k ]ᴿ ⟩
122+
[ k ] ∎
123+
... | inj₂ (inj₂ pr) = delete-key-∈⁻ k′u ([ k′<k ]ᴿ , k<u) pr kp≈k
124+
delete-key-∈⁻ (node kv@(k′ , v) lk′ k′u bal) (l<k , k<u) {kp} p kp≈k
125+
| tri> _ k′≉k k′>k
126+
with joinˡ⁻⁻ kv (delete k lk′ (l<k , [ k′>k ]ᴿ)) k′u bal p
127+
... | inj₁ kp≈k′ = contradiction (trans (sym kp≈k′) kp≈k) k′≉k
128+
... | inj₂ (inj₁ pl) = delete-key-∈⁻ lk′ (l<k , [ k′>k ]ᴿ) pl kp≈k
129+
... | inj₂ (inj₂ pr) = begin-contradiction
130+
[ k ] <⟨ [ k′>k ]ᴿ ⟩
131+
[ k′ ] <⟨ proj₁ (lookup-bounded pr) ⟩
132+
[ Any.lookupKey pr ] ≈⟨ [ sym (lookup-result pr) ]ᴱ ⟩
133+
[ kp ] ≈⟨ [ kp≈k ]ᴱ ⟩
134+
[ k ] ∎
135+
delete-key-∈⁻ (node (k′ , v) lk′ k′u bal) (l<k , k<u) {kp} p kp≈k
136+
| tri≈ k′≮k _ k′≯k
137+
with join⁻ lk′ k′u bal p
138+
... | inj₁ p₁ = contradiction
139+
(begin-strict
140+
[ k ] ≈⟨ [ sym kp≈k ]ᴱ ⟩
141+
[ kp ] ≈⟨ [ lookup-result p₁ ]ᴱ ⟩
142+
[ Any.lookupKey p₁ ] <⟨ proj₂ (lookup-bounded p₁) ⟩
143+
[ k′ ] ∎)
144+
(k′≯k ∘′ [<]-injective)
145+
... | inj₂ p₂ = contradiction
146+
(begin-strict
147+
[ k′ ] <⟨ proj₁ (lookup-bounded p₂) ⟩
148+
[ Any.lookupKey p₂ ] ≈⟨ [ sym (lookup-result p₂) ]ᴱ ⟩
149+
[ kp ] ≈⟨ [ kp≈k ]ᴱ ⟩
150+
[ k ] ∎)
151+
(k′≮k ∘′ [<]-injective)
152+
153+
154+
module _ (k : Key) where
155+
156+
delete-key⁻ : (t : Tree V l u n) (seg : l < k < u) →
157+
(p : Any P (proj₂ (delete k t seg))) →
158+
Any.lookupKey p ≉ k
159+
delete-key⁻ t seg p kp≈k =
160+
delete-key-∈⁻ k t seg (lookup-rebuild p Eq.refl) kp≈k

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

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Properties of headTail related to Any
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe #-}
8+
9+
open import Relation.Binary.Bundles using (StrictTotalOrder)
10+
11+
module Data.Tree.AVL.Indexed.Relation.Unary.Any.HeadTail
12+
{a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
13+
where
14+
15+
open import Data.Nat.Base using (suc; _+_)
16+
open import Data.Product.Base using (_,_; proj₁; proj₂)
17+
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
18+
open import Level using (Level)
19+
open import Relation.Binary.PropositionalEquality.Core renaming (refl to ≡-refl)
20+
open import Relation.Unary using (Pred)
21+
22+
open import Data.Tree.AVL.Indexed sto
23+
open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
24+
open import Data.Tree.AVL.Indexed.Relation.Unary.Any.JoinConstFuns sto
25+
using (joinˡ⁻-here⁺; joinˡ⁻-left⁺; joinˡ⁻-right⁺; joinˡ⁻⁻)
26+
27+
private
28+
variable
29+
v p : Level
30+
V : Value v
31+
P : Pred (K& V) p
32+
33+
headTail⁺ : ∀ {l u h} (t : Tree V l u (1 + h)) →
34+
Any P t →
35+
P (proj₁ (headTail t))
36+
⊎ Any P (proj₂ (proj₂ (proj₂ (headTail t))))
37+
headTail⁺ (node _ (leaf _) _ ∼+) (here p) = inj₁ p
38+
headTail⁺ (node _ (leaf _) _ ∼+) (right p) = inj₂ p
39+
headTail⁺ (node _ (leaf _) _ ∼0) (here p) = inj₁ p
40+
headTail⁺ (node {hˡ = suc _} k₃ t₁₂@(node _ _ _ _) t₄ bal) (here p)
41+
with headTail t₁₂
42+
... | k₁ , l<k₁ , t₂ = inj₂ (joinˡ⁻-here⁺ k₃ t₂ t₄ bal p)
43+
headTail⁺ (node {hˡ = suc _} k₃ t₁₂@(node _ _ _ _) t₄ bal) (left p)
44+
with headTail t₁₂ | headTail⁺ t₁₂ p
45+
... | k₁ , l<k₁ , t₂ | inj₁ ph = inj₁ ph
46+
... | k₁ , l<k₁ , t₂ | inj₂ pt = inj₂ (joinˡ⁻-left⁺ k₃ t₂ t₄ bal pt)
47+
headTail⁺ (node {hˡ = suc _} k₃ t₁₂@(node _ _ _ _) t₄ bal) (right p)
48+
with headTail t₁₂
49+
... | k₁ , l<k₁ , t₂ = inj₂ (joinˡ⁻-right⁺ k₃ t₂ t₄ bal p)
50+
51+
headTail-head⁻ : ∀ {l u h} → (t : Tree V l u (suc h)) →
52+
P (proj₁ (headTail t)) → Any P t
53+
headTail-head⁻ (node _ (leaf _) _ ∼+) p = here p
54+
headTail-head⁻ (node _ (leaf _) _ ∼0) p = here p
55+
headTail-head⁻ (node {hˡ = suc _} _ t₁₂ _ _) p
56+
with headTail t₁₂
57+
headTail-head⁻ (node {hˡ = suc _} _ t₁₂@(node _ _ _ _) _ _) p
58+
| k₁ , l<k₁ , t₂ = left (headTail-head⁻ t₁₂ p)
59+
60+
headTail-tail⁻ : ∀ {l u h} (t : Tree V l u (1 + h)) →
61+
Any P (proj₂ (proj₂ (proj₂ (headTail t)))) →
62+
Any P t
63+
headTail-tail⁻ (node _ (leaf _) _ ∼+) p = right p
64+
headTail-tail⁻ (node _ (leaf _) _ ∼0) p = right p
65+
headTail-tail⁻ (node {hˡ = suc _} k₃ t₁₂@(node _ _ _ _) t₄ bal) p
66+
with k₁ , l<k₁ , t₂ ← headTail t₁₂ in eq
67+
-- This match on `bal` is so the termination checker sees `h`
68+
-- decrease.
69+
| joinˡ⁻⁻ k₃ t₂ t₄ bal p | bal | eq
70+
... | inj₁ pk | _ | ≡-refl = here pk
71+
... | inj₂ (inj₁ pl) | ∼+ | ≡-refl = left (headTail-tail⁻ t₁₂ pl)
72+
... | inj₂ (inj₁ pl) | ∼0 | ≡-refl = left (headTail-tail⁻ t₁₂ pl)
73+
... | inj₂ (inj₁ pl) | ∼- | ≡-refl = left (headTail-tail⁻ t₁₂ pl)
74+
... | inj₂ (inj₂ pr) | _ | ≡-refl = right pr

0 commit comments

Comments
 (0)