|
781
|
1 module btree where
|
|
|
2
|
|
|
3 open import Level hiding (suc ; zero ; _⊔_ )
|
|
|
4
|
|
|
5 open import Data.Nat hiding (compare)
|
|
|
6 open import Data.Nat.Properties as NatProp
|
|
|
7 open import Data.Maybe
|
|
|
8 open import Data.Maybe.Properties
|
|
|
9 open import Data.Empty
|
|
|
10 open import Data.List
|
|
|
11 open import Data.Product
|
|
|
12
|
|
|
13 open import Function as F hiding (const)
|
|
|
14
|
|
|
15 open import Relation.Binary
|
|
|
16 open import Relation.Binary.PropositionalEquality
|
|
|
17 open import Relation.Nullary
|
|
|
18 open import logic
|
|
|
19
|
|
|
20
|
|
|
21 --
|
|
|
22 --
|
|
|
23 -- no children , having left node , having right node , having both
|
|
|
24 --
|
|
|
25 data bt {n : Level} (A : Set n) : Set n where
|
|
|
26 leaf : bt A
|
|
|
27 node : (key : ℕ) → (value : A) →
|
|
|
28 (left : bt A ) → (right : bt A ) → bt A
|
|
|
29
|
|
|
30 node-key : {n : Level} {A : Set n} → bt A → Maybe ℕ
|
|
|
31 node-key (node key _ _ _) = just key
|
|
|
32 node-key _ = nothing
|
|
|
33
|
|
|
34 node-value : {n : Level} {A : Set n} → bt A → Maybe A
|
|
|
35 node-value (node _ value _ _) = just value
|
|
|
36 node-value _ = nothing
|
|
|
37
|
|
|
38 bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ
|
|
|
39 bt-depth leaf = 0
|
|
|
40 bt-depth (node key value t t₁) = suc (bt-depth t ⊔ bt-depth t₁ )
|
|
|
41
|
|
|
42 open import Data.Unit hiding ( _≟_ ; _≤?_ ; _≤_)
|
|
|
43
|
|
|
44 data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
|
|
|
45 t-leaf : treeInvariant leaf
|
|
|
46 t-single : (key : ℕ) → (value : A) → treeInvariant (node key value leaf leaf)
|
|
|
47 t-right : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁ → treeInvariant (node key₁ value₁ t₁ t₂)
|
|
|
48 → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂))
|
|
|
49 t-left : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁ → treeInvariant (node key value t₁ t₂)
|
|
|
50 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf )
|
|
|
51 t-node : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → key < key₁ → key₁ < key₂
|
|
|
52 → treeInvariant (node key value t₁ t₂)
|
|
|
53 → treeInvariant (node key₂ value₂ t₃ t₄)
|
|
|
54 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄))
|
|
|
55
|
|
|
56 --
|
|
|
57 -- stack always contains original top at end (path of the tree)
|
|
|
58 --
|
|
|
59 data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (top orig : bt A) → (stack : List (bt A)) → Set n where
|
|
|
60 s-nil : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [])
|
|
|
61 s-right : {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
|
|
|
62 → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
|
|
|
63 s-left : {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
|
|
|
64 → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree₁ tree0 (tree₁ ∷ st)
|
|
|
65
|
|
|
66 data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt A ) → Set n where
|
|
|
67 r-leaf : replacedTree key value leaf (node key value leaf leaf)
|
|
|
68 r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁)
|
|
|
69 r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
|
|
|
70 → k < key → replacedTree key value t2 t → replacedTree key value (node k v1 t1 t2) (node k v1 t1 t)
|
|
|
71 r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
|
|
|
72 → key < k → replacedTree key value t1 t → replacedTree key value (node k v1 t1 t2) (node k v1 t t2)
|
|
|
73
|
|
|
74 add< : { i : ℕ } (j : ℕ ) → i < suc i + j
|
|
|
75 add< {i} j = begin
|
|
|
76 suc i ≤⟨ m≤m+n (suc i) j ⟩
|
|
|
77 suc i + j ∎ where open ≤-Reasoning
|
|
|
78
|
|
|
79 treeTest1 : bt ℕ
|
|
|
80 treeTest1 = node 0 0 leaf (node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf))
|
|
|
81 treeTest2 : bt ℕ
|
|
|
82 treeTest2 = node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf)
|
|
|
83 treeTest3 : bt ℕ
|
|
|
84 treeTest3 = node 2 5 (node 1 7 leaf leaf ) leaf
|
|
|
85 treeTest4 : bt ℕ
|
|
|
86 treeTest4 = node 5 5 leaf leaf
|
|
|
87 treeTest5 : bt ℕ
|
|
|
88 treeTest5 = node 1 7 leaf leaf
|
|
|
89
|
|
|
90
|
|
|
91 treeInvariantTest1 : treeInvariant treeTest1
|
|
|
92 treeInvariantTest1 = t-right (m≤m+n _ 2) (t-node (add< 0) (add< 1) (t-left (add< 0) (t-single 1 7)) (t-single 5 5) )
|
|
|
93
|
|
|
94 treeInvariantTest2 : treeInvariant treeTest2
|
|
|
95 treeInvariantTest2 = t-node (add< 0) (add< 1) (t-left (add< 0) (t-single 1 7)) (t-single 5 5)
|
|
|
96
|
|
|
97 stack-top : {n : Level} {A : Set n} (stack : List (bt A)) → Maybe (bt A)
|
|
|
98 stack-top [] = nothing
|
|
|
99 stack-top (x ∷ s) = just x
|
|
|
100
|
|
|
101 stack-last : {n : Level} {A : Set n} (stack : List (bt A)) → Maybe (bt A)
|
|
|
102 stack-last [] = nothing
|
|
|
103 stack-last (x ∷ []) = just x
|
|
|
104 stack-last (x ∷ s) = stack-last s
|
|
|
105
|
|
|
106 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
|
|
|
107 stackInvariantTest1 = s-right (add< 3) (s-nil)
|
|
|
108
|
|
|
109 stackInvariantTest111 : stackInvariant 4 treeTest4 treeTest1 ( treeTest4 ∷ treeTest2 ∷ treeTest1 ∷ [] )
|
|
|
110 stackInvariantTest111 = s-right (add< 0) (s-right (add< 3) (s-nil))
|
|
|
111
|
|
|
112 stackInvariantTest11 : stackInvariant 4 treeTest4 treeTest1 ( treeTest4 ∷ treeTest2 ∷ treeTest1 ∷ [] )
|
|
|
113 stackInvariantTest11 = s-right (add< 0) (s-right (add< 3) (s-nil)) --treeTest4から見てみぎ、みぎnil
|
|
|
114
|
|
|
115
|
|
|
116 stackInvariantTest2' : stackInvariant 2 treeTest3 treeTest1 (treeTest3 ∷ treeTest2 ∷ treeTest1 ∷ [] )
|
|
|
117 stackInvariantTest2' = s-left (add< 0) (s-right (add< 1) (s-nil))
|
|
|
118
|
|
|
119 --stackInvariantTest121 : stackInvariant 2 treeTest5 treeTest1 ( treeTest5 ∷ treeTest3 ∷ treeTest2 ∷ treeTest1 ∷ [] )
|
|
|
120 --stackInvariantTest121 = s-left (_) (s-left (add< 0) (s-right (add< 1) (s-nil))) -- 2<2が示せない
|
|
|
121
|
|
|
122 si-property0 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → {stack : List (bt A)} → stackInvariant key tree tree0 stack → ¬ ( stack ≡ [] )
|
|
|
123
|
|
|
124 si-property0 (s-nil ) ()
|
|
|
125 si-property0 (s-right x si) ()
|
|
|
126 si-property0 (s-left x si) ()
|
|
|
127
|
|
|
128 si-property1 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 tree1 : bt A} → {stack : List (bt A)} → stackInvariant key tree tree0 (tree1 ∷ stack)
|
|
|
129 → tree1 ≡ tree
|
|
|
130 si-property1 (s-nil ) = refl
|
|
|
131 si-property1 (s-right _ si) = refl
|
|
|
132 si-property1 (s-left _ si) = refl
|
|
|
133
|
|
|
134 si-property-last : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → stackInvariant key tree tree0 stack
|
|
|
135 → stack-last stack ≡ just tree0
|
|
|
136 si-property-last key t t0 (t ∷ []) (s-nil ) = refl
|
|
|
137 si-property-last key t t0 (.t ∷ x ∷ st) (s-right _ si ) with si-property1 si
|
|
|
138 ... | refl = si-property-last key x t0 (x ∷ st) si
|
|
|
139 si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ si ) with si-property1 si
|
|
|
140 ... | refl = si-property-last key x t0 (x ∷ st) si
|
|
|
141
|
|
|
142 rt-property1 : {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
|
|
|
143 rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf ()
|
|
|
144 rt-property1 {n} {A} key value .(node key _ _ _) .(node key value _ _) r-node ()
|
|
|
145 rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-right x rt) = λ ()
|
|
|
146 rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-left x rt) = λ ()
|
|
|
147
|
|
|
148 rt-property-leaf : {n : Level} {A : Set n} {key : ℕ} {value : A} {repl : bt A} → replacedTree key value leaf repl → repl ≡ node key value leaf leaf
|
|
|
149 rt-property-leaf r-leaf = refl
|
|
|
150
|
|
|
151 rt-property-¬leaf : {n : Level} {A : Set n} {key : ℕ} {value : A} {tree : bt A} → ¬ replacedTree key value tree leaf
|
|
|
152 rt-property-¬leaf ()
|
|
|
153
|
|
|
154 rt-property-key : {n : Level} {A : Set n} {key key₂ key₃ : ℕ} {value value₂ value₃ : A} {left left₁ right₂ right₃ : bt A}
|
|
|
155 → replacedTree key value (node key₂ value₂ left right₂) (node key₃ value₃ left₁ right₃) → key₂ ≡ key₃
|
|
|
156 rt-property-key r-node = refl
|
|
|
157 rt-property-key (r-right x ri) = refl
|
|
|
158 rt-property-key (r-left x ri) = refl
|
|
|
159
|
|
|
160 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
|
|
|
161 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
|
|
|
162 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
|
|
|
163 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
|
|
|
164
|
|
|
165 open _∧_
|
|
|
166
|
|
|
167
|
|
|
168 depth-1< : {i j : ℕ} → suc i ≤ suc (i Data.Nat.⊔ j )
|
|
|
169 depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
|
|
|
170
|
|
|
171 depth-2< : {i j : ℕ} → suc i ≤ suc (j Data.Nat.⊔ i )
|
|
|
172 depth-2< {i} {j} = s≤s
|
|
|
173
|
|
|
174 depth-3< : {i : ℕ } → suc i ≤ suc (suc i)
|
|
|
175 depth-3< {zero} = s≤s ( z≤n )
|
|
|
176 depth-3< {suc i} = s≤s (depth-3< {i} )
|
|
|
177
|
|
|
178
|
|
|
179 treeLeftDown : {n : Level} {A : Set n} {k : ℕ} {v1 : A} → (tree tree₁ : bt A )
|
|
|
180 → treeInvariant (node k v1 tree tree₁)
|
|
|
181 → treeInvariant tree
|
|
|
182 treeLeftDown {n} {A} {_} {v1} leaf leaf (t-single k1 v1) = t-leaf
|
|
|
183 treeLeftDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right x ti) = t-leaf
|
|
|
184 treeLeftDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left x ti) = ti
|
|
|
185 treeLeftDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node x x₁ ti ti₁) = ti
|
|
|
186
|
|
|
187 treeRightDown : {n : Level} {A : Set n} {k : ℕ} {v1 : A} → (tree tree₁ : bt A )
|
|
|
188 → treeInvariant (node k v1 tree tree₁)
|
|
|
189 → treeInvariant tree₁
|
|
|
190 treeRightDown {n} {A} {_} {v1} .leaf .leaf (t-single _ .v1) = t-leaf
|
|
|
191 treeRightDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right x ti) = ti
|
|
|
192 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left x ti) = t-leaf
|
|
|
193 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node x x₁ ti ti₁) = ti₁
|
|
|
194
|
|
|
195
|
|
|
196
|
|
|
197 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
|
|
|
198 → treeInvariant tree ∧ stackInvariant key tree tree0 stack
|
|
|
199 → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t )
|
|
|
200 → (exit : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
|
|
|
201 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t
|
|
|
202 findP key leaf tree0 st Pre _ exit = exit leaf st Pre (case1 refl) --leafである
|
|
|
203 findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁
|
|
|
204 findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl) --探しているkeyと一致
|
|
|
205 findP {n} {_} {A} key (node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree (tree ∷ st) --keyが求めているkey1より小さい。今いるツリーの左側をstackに積む。
|
|
|
206 -- ⟪ treeLeftDown tree tree₁ (proj1 Pre) , s-left a (proj2 Pre)⟫ depth-1< --これでも通った。
|
|
|
207 ⟪ treeLeftDown tree tree₁ (proj1 Pre) , findP1 a st (proj2 Pre) ⟫ depth-1< where
|
|
|
208 findP1 : key < key₁ → (st : List (bt A)) → stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
|
|
|
209 findP1 a (x ∷ st) si = s-left a si
|
|
|
210 findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right c (proj2 Pre) ⟫ depth-2<
|
|
|
211
|
|
|
212 replaceTree1 : {n : Level} {A : Set n} {t t₁ : bt A } → ( k : ℕ ) → (v1 value : A ) → treeInvariant (node k v1 t t₁) → treeInvariant (node k value t t₁)
|
|
|
213 replaceTree1 k v1 value (t-single .k .v1) = t-single k value
|
|
|
214 replaceTree1 k v1 value (t-right x t) = t-right x t
|
|
|
215 replaceTree1 k v1 value (t-left x t) = t-left x t
|
|
|
216 replaceTree1 k v1 value (t-node x x₁ t t₁) = t-node x x₁ t t₁
|
|
|
217
|
|
|
218 open import Relation.Binary.Definitions
|
|
|
219
|
|
|
220 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥
|
|
|
221 lemma3 refl ()
|
|
|
222 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
|
|
|
223 lemma5 (s≤s z≤n) ()
|
|
|
224 ¬x<x : {x : ℕ} → ¬ (x < x)
|
|
|
225 ¬x<x (s≤s lt) = ¬x<x lt
|
|
|
226
|
|
|
227 child-replaced : {n : Level} {A : Set n} (key : ℕ) (tree : bt A) → bt A
|
|
|
228 child-replaced key leaf = leaf
|
|
|
229 child-replaced key (node key₁ value left right) with <-cmp key key₁
|
|
|
230 ... | tri< a ¬b ¬c = left --問答無用で置き換えている。
|
|
|
231 ... | tri≈ ¬a b ¬c = node key₁ value left right
|
|
|
232 ... | tri> ¬a ¬b c = right
|
|
|
233
|
|
|
234 record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where
|
|
|
235 field
|
|
|
236 tree0 : bt A
|
|
|
237 ti : treeInvariant tree0
|
|
|
238 si : stackInvariant key tree tree0 stack
|
|
|
239 ri : replacedTree key value (child-replaced key tree ) repl
|
|
|
240 ci : C tree repl stack -- data continuation
|
|
|
241
|
|
|
242 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
|
|
|
243 → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key )
|
|
|
244 → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value (child-replaced key tree) tree1 → t) → t
|
|
|
245 replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 ) r-leaf
|
|
|
246 replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P)
|
|
|
247 (subst (λ j → replacedTree k v1 j (node k v1 t t₁) ) repl00 r-node) where
|
|
|
248 repl00 : node k value t t₁ ≡ child-replaced k (node k value t t₁)
|
|
|
249 repl00 with <-cmp k k
|
|
|
250 ... | tri< a ¬b ¬c = ⊥-elim (¬b refl)
|
|
|
251 ... | tri≈ ¬a b ¬c = refl
|
|
|
252 ... | tri> ¬a ¬b c = ⊥-elim (¬b refl)
|
|
|
253
|
|
|
254 replaceP : {n m : Level} {A : Set n} {t : Set m}
|
|
|
255 → (key : ℕ) → (value : A) → {tree : bt A} ( repl : bt A)
|
|
|
256 → (stack : List (bt A)) → replacePR key value tree repl stack (λ _ _ _ → Lift n ⊤)
|
|
|
257 → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A))
|
|
|
258 → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t)
|
|
|
259 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
|
|
|
260 replaceP key value {tree} repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen
|
|
|
261 replaceP key value {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ (replacePR.si Pre)-- tree0 ≡ leaf
|
|
|
262 ... | refl = exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ replacePR.ti Pre , r-leaf ⟫
|
|
|
263 replaceP key value {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁
|
|
|
264 ... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) (node key₁ value₁ repl right ) ⟪ replacePR.ti Pre , repl01 ⟫ where
|
|
|
265 repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ repl right )
|
|
|
266 repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre)
|
|
|
267 repl01 | refl | refl = subst (λ k → replacedTree key value (node key₁ value₁ k right ) (node key₁ value₁ repl right )) repl02 (r-left a repl03) where
|
|
|
268 repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl
|
|
|
269 repl03 = replacePR.ri Pre
|
|
|
270 repl02 : child-replaced key (node key₁ value₁ left right) ≡ left
|
|
|
271 repl02 with <-cmp key key₁
|
|
|
272 ... | tri< a ¬b ¬c = refl
|
|
|
273 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a a)
|
|
|
274 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a a)
|
|
|
275 ... | tri≈ ¬a b ¬c = exit (replacePR.tree0 Pre) repl ⟪ replacePR.ti Pre , repl01 ⟫ where
|
|
|
276 repl01 : replacedTree key value (replacePR.tree0 Pre) repl
|
|
|
277 repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre)
|
|
|
278 repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl02 (replacePR.ri Pre) where
|
|
|
279 repl02 : child-replaced key (node key₁ value₁ left right) ≡ node key₁ value₁ left right
|
|
|
280 repl02 with <-cmp key key₁
|
|
|
281 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b b)
|
|
|
282 ... | tri≈ ¬a b ¬c = refl
|
|
|
283 ... | tri> ¬a ¬b c = ⊥-elim ( ¬b b)
|
|
|
284 ... | tri> ¬a ¬b c = exit (replacePR.tree0 Pre) (node key₁ value₁ left repl ) ⟪ replacePR.ti Pre , repl01 ⟫ where
|
|
|
285 repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ left repl )
|
|
|
286 repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre)
|
|
|
287 repl01 | refl | refl = subst (λ k → replacedTree key value (node key₁ value₁ left k ) (node key₁ value₁ left repl )) repl02 (r-right c repl03) where
|
|
|
288 repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl
|
|
|
289 repl03 = replacePR.ri Pre
|
|
|
290 repl02 : child-replaced key (node key₁ value₁ left right) ≡ right
|
|
|
291 repl02 with <-cmp key key₁
|
|
|
292 ... | tri< a ¬b ¬c = ⊥-elim ( ¬c c)
|
|
|
293 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c c)
|
|
|
294 ... | tri> ¬a ¬b c = refl
|
|
|
295 replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(tree1 ∷ st1)) Pre next exit = next key value repl st Post ≤-refl where
|
|
|
296 Post : replacePR key value tree1 repl (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤)
|
|
|
297 Post with replacePR.si Pre
|
|
|
298 ... | s-right {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
|
|
|
299 repl09 : tree1 ≡ node key₂ v1 tree₁ leaf
|
|
|
300 repl09 = si-property1 si
|
|
|
301 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
|
|
|
302 repl10 with si-property1 si
|
|
|
303 ... | refl = si
|
|
|
304 repl07 : child-replaced key (node key₂ v1 tree₁ leaf) ≡ leaf
|
|
|
305 repl07 with <-cmp key key₂
|
|
|
306 ... | tri< a ¬b ¬c = ⊥-elim (¬c x)
|
|
|
307 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x)
|
|
|
308 ... | tri> ¬a ¬b c = refl
|
|
|
309 repl12 : replacedTree key value (child-replaced key tree1 ) repl
|
|
|
310 repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07 ) ) (sym (rt-property-leaf (replacePR.ri Pre))) r-leaf
|
|
|
311 ... | s-left {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
|
|
|
312 repl09 : tree1 ≡ node key₂ v1 leaf tree₁
|
|
|
313 repl09 = si-property1 si
|
|
|
314 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
|
|
|
315 repl10 with si-property1 si
|
|
|
316 ... | refl = si
|
|
|
317 repl07 : child-replaced key (node key₂ v1 leaf tree₁ ) ≡ leaf
|
|
|
318 repl07 with <-cmp key key₂
|
|
|
319 ... | tri< a ¬b ¬c = refl
|
|
|
320 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a x)
|
|
|
321 ... | tri> ¬a ¬b c = ⊥-elim (¬a x)
|
|
|
322 repl12 : replacedTree key value (child-replaced key tree1 ) repl
|
|
|
323 repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07 ) ) (sym (rt-property-leaf (replacePR.ri Pre))) r-leaf
|
|
|
324 replaceP {n} {_} {A} key value {tree} repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁
|
|
|
325 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st Post ≤-refl where
|
|
|
326 Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤)
|
|
|
327 Post with replacePR.si Pre
|
|
|
328 ... | s-right {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
|
|
|
329 repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right)
|
|
|
330 repl09 = si-property1 si
|
|
|
331 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
|
|
|
332 repl10 with si-property1 si
|
|
|
333 ... | refl = si
|
|
|
334 repl03 : child-replaced key (node key₁ value₁ left right) ≡ left
|
|
|
335 repl03 with <-cmp key key₁
|
|
|
336 ... | tri< a1 ¬b ¬c = refl
|
|
|
337 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a)
|
|
|
338 ... | tri> ¬a ¬b c = ⊥-elim (¬a a)
|
|
|
339 repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right
|
|
|
340 repl02 with repl09 | <-cmp key key₂
|
|
|
341 ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt)
|
|
|
342 ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt)
|
|
|
343 ... | refl | tri> ¬a ¬b c = refl
|
|
|
344 repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1
|
|
|
345 repl04 = begin
|
|
|
346 node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03 ⟩
|
|
|
347 node key₁ value₁ left right ≡⟨ sym repl02 ⟩
|
|
|
348 child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
|
|
|
349 child-replaced key tree1 ∎ where open ≡-Reasoning
|
|
|
350 repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ repl right)
|
|
|
351 repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) repl04 (r-left a (replacePR.ri Pre))
|
|
|
352 ... | s-left {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
|
|
|
353 repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁
|
|
|
354 repl09 = si-property1 si
|
|
|
355 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
|
|
|
356 repl10 with si-property1 si
|
|
|
357 ... | refl = si
|
|
|
358 repl03 : child-replaced key (node key₁ value₁ left right) ≡ left
|
|
|
359 repl03 with <-cmp key key₁
|
|
|
360 ... | tri< a1 ¬b ¬c = refl
|
|
|
361 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a)
|
|
|
362 ... | tri> ¬a ¬b c = ⊥-elim (¬a a)
|
|
|
363 repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right
|
|
|
364 repl02 with repl09 | <-cmp key key₂
|
|
|
365 ... | refl | tri< a ¬b ¬c = refl
|
|
|
366 ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt)
|
|
|
367 ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt)
|
|
|
368 repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1
|
|
|
369 repl04 = begin
|
|
|
370 node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03 ⟩
|
|
|
371 node key₁ value₁ left right ≡⟨ sym repl02 ⟩
|
|
|
372 child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
|
|
|
373 child-replaced key tree1 ∎ where open ≡-Reasoning
|
|
|
374 repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ repl right)
|
|
|
375 repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) repl04 (r-left a (replacePR.ri Pre))
|
|
|
376 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st Post ≤-refl where
|
|
|
377 Post : replacePR key value tree1 (node key₁ value left right ) (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤)
|
|
|
378 Post with replacePR.si Pre
|
|
|
379 ... | s-right {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where
|
|
|
380 repl09 : tree1 ≡ node key₂ v1 tree₁ tree -- (node key₁ value₁ left right)
|
|
|
381 repl09 = si-property1 si
|
|
|
382 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
|
|
|
383 repl10 with si-property1 si
|
|
|
384 ... | refl = si
|
|
|
385 repl07 : child-replaced key (node key₂ v1 tree₁ tree) ≡ tree
|
|
|
386 repl07 with <-cmp key key₂
|
|
|
387 ... | tri< a ¬b ¬c = ⊥-elim (¬c x)
|
|
|
388 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x)
|
|
|
389 ... | tri> ¬a ¬b c = refl
|
|
|
390 repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key tree1 ) (node key₁ value left right )
|
|
|
391 repl12 refl with repl09
|
|
|
392 ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node
|
|
|
393 ... | s-left {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where
|
|
|
394 repl09 : tree1 ≡ node key₂ v1 tree tree₁
|
|
|
395 repl09 = si-property1 si
|
|
|
396 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
|
|
|
397 repl10 with si-property1 si
|
|
|
398 ... | refl = si
|
|
|
399 repl07 : child-replaced key (node key₂ v1 tree tree₁ ) ≡ tree
|
|
|
400 repl07 with <-cmp key key₂
|
|
|
401 ... | tri< a ¬b ¬c = refl
|
|
|
402 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a x)
|
|
|
403 ... | tri> ¬a ¬b c = ⊥-elim (¬a x)
|
|
|
404 repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key tree1 ) (node key₁ value left right )
|
|
|
405 repl12 refl with repl09
|
|
|
406 ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node
|
|
|
407 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st Post ≤-refl where
|
|
|
408 Post : replacePR key value tree1 (node key₁ value₁ left repl ) st (λ _ _ _ → Lift n ⊤)
|
|
|
409 Post with replacePR.si Pre
|
|
|
410 ... | s-right {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
|
|
|
411 repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right)
|
|
|
412 repl09 = si-property1 si
|
|
|
413 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
|
|
|
414 repl10 with si-property1 si
|
|
|
415 ... | refl = si
|
|
|
416 repl03 : child-replaced key (node key₁ value₁ left right) ≡ right
|
|
|
417 repl03 with <-cmp key key₁
|
|
|
418 ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c)
|
|
|
419 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c)
|
|
|
420 ... | tri> ¬a ¬b c = refl
|
|
|
421 repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right
|
|
|
422 repl02 with repl09 | <-cmp key key₂
|
|
|
423 ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt)
|
|
|
424 ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt)
|
|
|
425 ... | refl | tri> ¬a ¬b c = refl
|
|
|
426 repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1
|
|
|
427 repl04 = begin
|
|
|
428 node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩
|
|
|
429 node key₁ value₁ left right ≡⟨ sym repl02 ⟩
|
|
|
430 child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
|
|
|
431 child-replaced key tree1 ∎ where open ≡-Reasoning
|
|
|
432 repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ left repl)
|
|
|
433 repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl) ) repl04 (r-right c (replacePR.ri Pre))
|
|
|
434 ... | s-left {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
|
|
|
435 repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁
|
|
|
436 repl09 = si-property1 si
|
|
|
437 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
|
|
|
438 repl10 with si-property1 si
|
|
|
439 ... | refl = si
|
|
|
440 repl03 : child-replaced key (node key₁ value₁ left right) ≡ right
|
|
|
441 repl03 with <-cmp key key₁
|
|
|
442 ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c)
|
|
|
443 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c)
|
|
|
444 ... | tri> ¬a ¬b c = refl
|
|
|
445 repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right
|
|
|
446 repl02 with repl09 | <-cmp key key₂
|
|
|
447 ... | refl | tri< a ¬b ¬c = refl
|
|
|
448 ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt)
|
|
|
449 ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt)
|
|
|
450 repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1
|
|
|
451 repl04 = begin
|
|
|
452 node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩
|
|
|
453 node key₁ value₁ left right ≡⟨ sym repl02 ⟩
|
|
|
454 child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
|
|
|
455 child-replaced key tree1 ∎ where open ≡-Reasoning
|
|
|
456 repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ left repl)
|
|
|
457 repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl) ) repl04 (r-right c (replacePR.ri Pre))
|
|
|
458
|
|
|
459 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
|
|
|
460 → (r : Index) → (p : Invraiant r)
|
|
|
461 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t
|
|
|
462 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r)
|
|
|
463 ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) )
|
|
|
464 ... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where
|
|
|
465 TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t
|
|
|
466 TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1))
|
|
|
467 TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j)
|
|
|
468 ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt
|
|
|
469 ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 )
|
|
|
470 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j )
|
|
|
471 {-
|
|
|
472 open _∧_
|
|
|
473
|
|
|
474 RTtoTI0 : {n : Level} {A : Set n} → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
|
|
|
475 → replacedTree key value tree repl → treeInvariant repl
|
|
|
476 RTtoTI0 .leaf .(node key value leaf leaf) key value ti r-leaf = t-single key value
|
|
|
477 RTtoTI0 .(node key _ leaf leaf) .(node key value leaf leaf) key value (t-single .key _) r-node = t-single key value
|
|
|
478 RTtoTI0 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right x ti) r-node = t-right x ti
|
|
|
479 RTtoTI0 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x ti) r-node = t-left x ti
|
|
|
480 RTtoTI0 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ ti ti₁) r-node = t-node x x₁ ti ti₁
|
|
|
481 -- r-right case
|
|
|
482 RTtoTI0 (node _ _ leaf leaf) (node _ _ leaf .(node key value leaf leaf)) key value (t-single _ _) (r-right x r-leaf) = t-right x (t-single key value)
|
|
|
483 RTtoTI0 (node _ _ leaf right@(node _ _ _ _)) (node key₁ value₁ leaf leaf) key value (t-right x₁ ti) (r-right x ri) = t-single key₁ value₁
|
|
|
484 RTtoTI0 (node key₁ _ leaf right@(node key₂ _ _ _)) (node key₁ value₁ leaf right₁@(node key₃ _ _ _)) key value (t-right x₁ ti) (r-right x ri) =
|
|
|
485 t-right (subst (λ k → key₁ < k ) (rt-property-key ri) x₁) (RTtoTI0 _ _ key value ti ri)
|
|
|
486 RTtoTI0 (node key₁ _ (node _ _ _ _) leaf) (node key₁ _ (node key₃ value left right) leaf) key value₁ (t-left x₁ ti) (r-right x ())
|
|
|
487 RTtoTI0 (node key₁ _ (node key₃ _ _ _) leaf) (node key₁ _ (node key₃ value₃ _ _) (node key value leaf leaf)) key value (t-left x₁ ti) (r-right x r-leaf) =
|
|
|
488 t-node x₁ x ti (t-single key value)
|
|
|
489 RTtoTI0 (node key₁ _ (node _ _ _ _) (node key₂ _ _ _)) (node key₁ _ (node _ _ _ _) (node key₃ _ _ _)) key value (t-node x₁ x₂ ti ti₁) (r-right x ri) =
|
|
|
490 t-node x₁ (subst (λ k → key₁ < k) (rt-property-key ri) x₂) ti (RTtoTI0 _ _ key value ti₁ ri)
|
|
|
491 -- r-left case
|
|
|
492 RTtoTI0 .(node _ _ leaf leaf) .(node _ _ (node key value leaf leaf) leaf) key value (t-single _ _) (r-left x r-leaf) = t-left x (t-single _ _ )
|
|
|
493 RTtoTI0 .(node _ _ leaf (node _ _ _ _)) (node key₁ value₁ (node key value leaf leaf) (node _ _ _ _)) key value (t-right x₁ ti) (r-left x r-leaf) = t-node x x₁ (t-single key value) ti
|
|
|
494 RTtoTI0 (node key₃ _ (node key₂ _ _ _) leaf) (node key₃ _ (node key₁ value₁ left left₁) leaf) key value (t-left x₁ ti) (r-left x ri) =
|
|
|
495 t-left (subst (λ k → k < key₃ ) (rt-property-key ri) x₁) (RTtoTI0 _ _ key value ti ri) -- key₁ < key₃
|
|
|
496 RTtoTI0 (node key₁ _ (node key₂ _ _ _) (node _ _ _ _)) (node key₁ _ (node key₃ _ _ _) (node _ _ _ _)) key value (t-node x₁ x₂ ti ti₁) (r-left x ri) = t-node (subst (λ k → k < key₁ ) (rt-property-key ri) x₁) x₂ (RTtoTI0 _ _ key value ti ri) ti₁
|
|
|
497
|
|
|
498 RTtoTI1 : {n : Level} {A : Set n} → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant repl
|
|
|
499 → replacedTree key value tree repl → treeInvariant tree
|
|
|
500 RTtoTI1 .leaf .(node key value leaf leaf) key value ti r-leaf = t-leaf
|
|
|
501 RTtoTI1 (node key value₁ leaf leaf) .(node key value leaf leaf) key value (t-single .key .value) r-node = t-single key value₁
|
|
|
502 RTtoTI1 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right x ti) r-node = t-right x ti
|
|
|
503 RTtoTI1 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x ti) r-node = t-left x ti
|
|
|
504 RTtoTI1 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ ti ti₁) r-node = t-node x x₁ ti ti₁
|
|
|
505 -- r-right case
|
|
|
506 RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ leaf (node _ _ _ _)) key value (t-right x₁ ti) (r-right x r-leaf) = t-single key₁ value₁
|
|
|
507 RTtoTI1 (node key₁ value₁ leaf (node key₂ value₂ t2 t3)) (node key₁ _ leaf (node key₃ _ _ _)) key value (t-right x₁ ti) (r-right x ri) =
|
|
|
508 t-right (subst (λ k → key₁ < k ) (sym (rt-property-key ri)) x₁) (RTtoTI1 _ _ key value ti ri) -- key₁ < key₂
|
|
|
509 RTtoTI1 (node _ _ (node _ _ _ _) leaf) (node _ _ (node _ _ _ _) (node key value _ _)) key value (t-node x₁ x₂ ti ti₁) (r-right x r-leaf) =
|
|
|
510 t-left x₁ ti
|
|
|
511 RTtoTI1 (node key₄ _ (node key₃ _ _ _) (node key₁ value₁ n n₁)) (node key₄ _ (node key₃ _ _ _) (node key₂ _ _ _)) key value (t-node x₁ x₂ ti ti₁) (r-right x ri) = t-node x₁ (subst (λ k → key₄ < k ) (sym (rt-property-key ri)) x₂) ti (RTtoTI1 _ _ key value ti₁ ri) -- key₄ < key₁
|
|
|
512 -- r-left case
|
|
|
513 RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ _ leaf) key value (t-left x₁ ti) (r-left x ri) = t-single key₁ value₁
|
|
|
514 RTtoTI1 (node key₁ _ (node key₂ value₁ n n₁) leaf) (node key₁ _ (node key₃ _ _ _) leaf) key value (t-left x₁ ti) (r-left x ri) =
|
|
|
515 t-left (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) (RTtoTI1 _ _ key value ti ri) -- key₂ < key₁
|
|
|
516 RTtoTI1 (node key₁ value₁ leaf _) (node key₁ _ _ _) key value (t-node x₁ x₂ ti ti₁) (r-left x r-leaf) = t-right x₂ ti₁
|
|
|
517 RTtoTI1 (node key₁ value₁ (node key₂ value₂ n n₁) _) (node key₁ _ _ _) key value (t-node x₁ x₂ ti ti₁) (r-left x ri) =
|
|
|
518 t-node (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) x₂ (RTtoTI1 _ _ key value ti ri) ti₁ -- key₂ < key₁
|
|
|
519
|
|
|
520 insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
|
|
|
521 → (exit : (tree repl : bt A) → treeInvariant repl ∧ replacedTree key value tree repl → t ) → t
|
|
|
522 insertTreeP {n} {m} {A} {t} tree key value P0 exit =
|
|
|
523 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , tree ∷ [] ⟫ ⟪ P0 , s-nil ⟫
|
|
|
524 $ λ p P loop → findP key (proj1 p) tree (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )
|
|
|
525 $ λ t s P C → replaceNodeP key value t C (proj1 P)
|
|
|
526 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ bt A ∧ bt A )
|
|
|
527 {λ p → replacePR key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) (λ _ _ _ → Lift n ⊤ ) }
|
|
|
528 (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = P0 ; si = proj2 P ; ri = R ; ci = lift tt }
|
|
|
529 $ λ p P1 loop → replaceP key value (proj2 (proj2 p)) (proj1 p) P1
|
|
|
530 (λ key value {tree1} repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ P2 lt )
|
|
|
531 $ λ tree repl P → exit tree repl ⟪ RTtoTI0 _ _ _ _ (proj1 P) (proj2 P) , proj2 P ⟫
|
|
|
532
|
|
|
533 insertTestP1 = insertTreeP leaf 1 1 t-leaf
|
|
|
534 $ λ _ x0 P0 → insertTreeP x0 2 1 (proj1 P0)
|
|
|
535 $ λ _ x1 P1 → insertTreeP x1 3 2 (proj1 P1)
|
|
|
536 $ λ _ x2 P2 → insertTreeP x2 2 2 (proj1 P2) (λ _ x P → x )
|
|
|
537
|
|
|
538 top-value : {n : Level} {A : Set n} → (tree : bt A) → Maybe A
|
|
|
539 top-value leaf = nothing
|
|
|
540 top-value (node key value tree tree₁) = just value
|
|
|
541 -} |
