Mercurial > hg > Gears > GearsAgda

comparison btree.agda @ 781:68904fdaab71

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
te
author Moririn < Moririn@cr.ie.u-ryukyu.ac.jp>
date Mon, 10 Jul 2023 19:59:14 +0900
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 781:68904fdaab71
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 {! !} --(m≤n⊔m j i)
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
262 replaceP key value {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ (replacePR.si Pre)-- tree0 ≡ leaf
263 ... | refl = exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ replacePR.ti Pre , r-leaf ⟫
264 replaceP key value {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁
265 ... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) (node key₁ value₁ repl right ) ⟪ replacePR.ti Pre , repl01 ⟫ where
266 repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ repl right )
267 repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre)
268 repl01 | refl | refl = subst (λ k → replacedTree key value (node key₁ value₁ k right ) (node key₁ value₁ repl right )) repl02 (r-left a repl03) where
269 repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl
270 repl03 = replacePR.ri Pre
271 repl02 : child-replaced key (node key₁ value₁ left right) ≡ left
272 repl02 with <-cmp key key₁
273 ... | tri< a ¬b ¬c = refl
274 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a a)
275 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a a)
276 ... | tri≈ ¬a b ¬c = exit (replacePR.tree0 Pre) repl ⟪ replacePR.ti Pre , repl01 ⟫ where
277 repl01 : replacedTree key value (replacePR.tree0 Pre) repl
278 repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre)
279 repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl02 (replacePR.ri Pre) where
280 repl02 : child-replaced key (node key₁ value₁ left right) ≡ node key₁ value₁ left right
281 repl02 with <-cmp key key₁
282 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b b)
283 ... | tri≈ ¬a b ¬c = refl
284 ... | tri> ¬a ¬b c = ⊥-elim ( ¬b b)
285 ... | tri> ¬a ¬b c = exit (replacePR.tree0 Pre) (node key₁ value₁ left repl ) ⟪ replacePR.ti Pre , repl01 ⟫ where
286 repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ left repl )
287 repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre)
288 repl01 | refl | refl = subst (λ k → replacedTree key value (node key₁ value₁ left k ) (node key₁ value₁ left repl )) repl02 (r-right c repl03) where
289 repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl
290 repl03 = replacePR.ri Pre
291 repl02 : child-replaced key (node key₁ value₁ left right) ≡ right
292 repl02 with <-cmp key key₁
293 ... | tri< a ¬b ¬c = ⊥-elim ( ¬c c)
294 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c c)
295 ... | tri> ¬a ¬b c = refl
296
297
298 replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(tree1 ∷ st1)) Pre next exit = next key value repl st Post ≤-refl where
299 Post : replacePR key value tree1 repl (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤)
300 --Post (replacePR)を定める必要があるが、siの値のよって影響されるため、場合分けをする。
301 --siとriが変化するから、（nextとすると）場合分けで定義し直す必要がある。
302 Post with replacePR.si Pre
303 ... | s-right {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
304 repl09 : tree1 ≡ node key₂ v1 tree₁ leaf
305 repl09 = si-property1 si
306 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
307 repl10 with si-property1 si
308 ... | refl = si
309 repl07 : child-replaced key (node key₂ v1 tree₁ leaf) ≡ leaf
310 repl07 with <-cmp key key₂
311 ... | tri< a ¬b ¬c = ⊥-elim (¬c x)
312 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x)
313 ... | tri> ¬a ¬b c = refl
314 repl12 : replacedTree key value (child-replaced key tree1 ) repl
315 -- repl12 = subst₂ {!!} {!!} {!!} {!!}
316 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
317 ... | s-left {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
318 repl09 : tree1 ≡ node key₂ v1 leaf tree₁
319 repl09 = si-property1 si
320 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
321 repl10 with si-property1 si
322 ... | refl = si
323 repl07 : child-replaced key (node key₂ v1 leaf tree₁ ) ≡ leaf
324 repl07 with <-cmp key key₂
325 ... | tri< a ¬b ¬c = refl
326 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a x)
327 ... | tri> ¬a ¬b c = ⊥-elim (¬a x)
328 repl12 : replacedTree key value (child-replaced key tree1 ) repl
329 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
330 replaceP {n} {_} {A} key value {tree} repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁
331 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st Post ≤-refl where
332 Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤)
333 Post with replacePR.si Pre
334 ... | s-right {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
335 repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right)
336 repl09 = si-property1 si
337 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
338 repl10 with si-property1 si
339 ... | refl = si
340 repl03 : child-replaced key (node key₁ value₁ left right) ≡ left
341 repl03 with <-cmp key key₁
342 ... | tri< a1 ¬b ¬c = refl
343 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a)
344 ... | tri> ¬a ¬b c = ⊥-elim (¬a a)
345 repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right
346 repl02 with repl09 | <-cmp key key₂
347 ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt)
348 ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt)
349 ... | refl | tri> ¬a ¬b c = refl
350 repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1
351 repl04 = begin
352 node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03 ⟩
353 node key₁ value₁ left right ≡⟨ sym repl02 ⟩
354 child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
355 child-replaced key tree1 ∎ where open ≡-Reasoning
356 repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ repl right)
357 repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) repl04 (r-left a (replacePR.ri Pre))
358 ... | s-left {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
359 repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁
360 repl09 = si-property1 si
361 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
362 repl10 with si-property1 si
363 ... | refl = si
364 repl03 : child-replaced key (node key₁ value₁ left right) ≡ left
365 repl03 with <-cmp key key₁
366 ... | tri< a1 ¬b ¬c = refl
367 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a)
368 ... | tri> ¬a ¬b c = ⊥-elim (¬a a)
369 repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right
370 repl02 with repl09 | <-cmp key key₂
371 ... | refl | tri< a ¬b ¬c = refl
372 ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt)
373 ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt)
374 repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1
375 repl04 = begin
376 node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03 ⟩
377 node key₁ value₁ left right ≡⟨ sym repl02 ⟩
378 child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
379 child-replaced key tree1 ∎ where open ≡-Reasoning
380 repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ repl right)
381 repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) repl04 (r-left a (replacePR.ri Pre))
382 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st Post ≤-refl where
383 Post : replacePR key value tree1 (node key₁ value left right ) (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤)
384 Post with replacePR.si Pre
385 ... | 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
386 repl09 : tree1 ≡ node key₂ v1 tree₁ tree -- (node key₁ value₁ left right)
387 repl09 = si-property1 si
388 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
389 repl10 with si-property1 si
390 ... | refl = si
391 repl07 : child-replaced key (node key₂ v1 tree₁ tree) ≡ tree
392 repl07 with <-cmp key key₂
393 ... | tri< a ¬b ¬c = ⊥-elim (¬c x)
394 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x)
395 ... | tri> ¬a ¬b c = refl
396 repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key tree1 ) (node key₁ value left right )
397 repl12 refl with repl09
398 ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node
399 ... | 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
400 repl09 : tree1 ≡ node key₂ v1 tree tree₁
401 repl09 = si-property1 si
402 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
403 repl10 with si-property1 si
404 ... | refl = si
405 repl07 : child-replaced key (node key₂ v1 tree tree₁ ) ≡ tree
406 repl07 with <-cmp key key₂
407 ... | tri< a ¬b ¬c = refl
408 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a x)
409 ... | tri> ¬a ¬b c = ⊥-elim (¬a x)
410 repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key tree1 ) (node key₁ value left right )
411 repl12 refl with repl09
412 ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node
413 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st Post ≤-refl where
414 Post : replacePR key value tree1 (node key₁ value₁ left repl ) st (λ _ _ _ → Lift n ⊤)
415 Post with replacePR.si Pre
416 ... | s-right {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
417 repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right)
418 repl09 = si-property1 si
419 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
420 repl10 with si-property1 si
421 ... | refl = si
422 repl03 : child-replaced key (node key₁ value₁ left right) ≡ right
423 repl03 with <-cmp key key₁
424 ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c)
425 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c)
426 ... | tri> ¬a ¬b c = refl
427 repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right
428 repl02 with repl09 | <-cmp key key₂
429 ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt)
430 ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt)
431 ... | refl | tri> ¬a ¬b c = refl
432 repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1
433 repl04 = begin
434 node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩
435 node key₁ value₁ left right ≡⟨ sym repl02 ⟩
436 child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
437 child-replaced key tree1 ∎ where open ≡-Reasoning
438 repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ left repl)
439 repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl) ) repl04 (r-right c (replacePR.ri Pre))
440 ... | s-left {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
441 repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁
442 repl09 = si-property1 si
443 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
444 repl10 with si-property1 si
445 ... | refl = si
446 repl03 : child-replaced key (node key₁ value₁ left right) ≡ right
447 repl03 with <-cmp key key₁
448 ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c)
449 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c)
450 ... | tri> ¬a ¬b c = refl
451 repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right
452 repl02 with repl09 | <-cmp key key₂
453 ... | refl | tri< a ¬b ¬c = refl
454 ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt)
455 ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt)
456 repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1
457 repl04 = begin
458 node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩
459 node key₁ value₁ left right ≡⟨ sym repl02 ⟩
460 child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
461 child-replaced key tree1 ∎ where open ≡-Reasoning
462 repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ left repl)
463 repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl) ) repl04 (r-right c (replacePR.ri Pre))
464
465 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
466 → (r : Index) → (p : Invraiant r)
467 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t
468 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r)
469 ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) )
470 ... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where
471 TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t
472 TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1))
473 TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j)
474 ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt
475 ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 )
476 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j )
477 {-
478 open _∧_
479
480 RTtoTI0 : {n : Level} {A : Set n} → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
481 → replacedTree key value tree repl → treeInvariant repl
482 RTtoTI0 .leaf .(node key value leaf leaf) key value ti r-leaf = t-single key value
483 RTtoTI0 .(node key _ leaf leaf) .(node key value leaf leaf) key value (t-single .key _) r-node = t-single key value
484 RTtoTI0 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right x ti) r-node = t-right x ti
485 RTtoTI0 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x ti) r-node = t-left x ti
486 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₁
487 -- r-right case
488 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)
489 RTtoTI0 (node _ _ leaf right@(node _ _ _ _)) (node key₁ value₁ leaf leaf) key value (t-right x₁ ti) (r-right x ri) = t-single key₁ value₁
490 RTtoTI0 (node key₁ _ leaf right@(node key₂ _ _ _)) (node key₁ value₁ leaf right₁@(node key₃ _ _ _)) key value (t-right x₁ ti) (r-right x ri) =
491 t-right (subst (λ k → key₁ < k ) (rt-property-key ri) x₁) (RTtoTI0 _ _ key value ti ri)
492 RTtoTI0 (node key₁ _ (node _ _ _ _) leaf) (node key₁ _ (node key₃ value left right) leaf) key value₁ (t-left x₁ ti) (r-right x ())
493 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) =
494 t-node x₁ x ti (t-single key value)
495 RTtoTI0 (node key₁ _ (node _ _ _ _) (node key₂ _ _ _)) (node key₁ _ (node _ _ _ _) (node key₃ _ _ _)) key value (t-node x₁ x₂ ti ti₁) (r-right x ri) =
496 t-node x₁ (subst (λ k → key₁ < k) (rt-property-key ri) x₂) ti (RTtoTI0 _ _ key value ti₁ ri)
497 -- r-left case
498 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 _ _ )
499 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
500 RTtoTI0 (node key₃ _ (node key₂ _ _ _) leaf) (node key₃ _ (node key₁ value₁ left left₁) leaf) key value (t-left x₁ ti) (r-left x ri) =
501 t-left (subst (λ k → k < key₃ ) (rt-property-key ri) x₁) (RTtoTI0 _ _ key value ti ri) -- key₁ < key₃
502 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₁
503
504 RTtoTI1 : {n : Level} {A : Set n} → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant repl
505 → replacedTree key value tree repl → treeInvariant tree
506 RTtoTI1 .leaf .(node key value leaf leaf) key value ti r-leaf = t-leaf
507 RTtoTI1 (node key value₁ leaf leaf) .(node key value leaf leaf) key value (t-single .key .value) r-node = t-single key value₁
508 RTtoTI1 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right x ti) r-node = t-right x ti
509 RTtoTI1 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x ti) r-node = t-left x ti
510 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₁
511 -- r-right case
512 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₁
513 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) =
514 t-right (subst (λ k → key₁ < k ) (sym (rt-property-key ri)) x₁) (RTtoTI1 _ _ key value ti ri) -- key₁ < key₂
515 RTtoTI1 (node _ _ (node _ _ _ _) leaf) (node _ _ (node _ _ _ _) (node key value _ _)) key value (t-node x₁ x₂ ti ti₁) (r-right x r-leaf) =
516 t-left x₁ ti
517 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₁
518 -- r-left case
519 RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ _ leaf) key value (t-left x₁ ti) (r-left x ri) = t-single key₁ value₁
520 RTtoTI1 (node key₁ _ (node key₂ value₁ n n₁) leaf) (node key₁ _ (node key₃ _ _ _) leaf) key value (t-left x₁ ti) (r-left x ri) =
521 t-left (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) (RTtoTI1 _ _ key value ti ri) -- key₂ < key₁
522 RTtoTI1 (node key₁ value₁ leaf _) (node key₁ _ _ _) key value (t-node x₁ x₂ ti ti₁) (r-left x r-leaf) = t-right x₂ ti₁
523 RTtoTI1 (node key₁ value₁ (node key₂ value₂ n n₁) _) (node key₁ _ _ _) key value (t-node x₁ x₂ ti ti₁) (r-left x ri) =
524 t-node (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) x₂ (RTtoTI1 _ _ key value ti ri) ti₁ -- key₂ < key₁
525
526 insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
527 → (exit : (tree repl : bt A) → treeInvariant repl ∧ replacedTree key value tree repl → t ) → t
528 insertTreeP {n} {m} {A} {t} tree key value P0 exit =
529 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 ⟫
530 $ λ p P loop → findP key (proj1 p) tree (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )
531 $ λ t s P C → replaceNodeP key value t C (proj1 P)
532 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ bt A ∧ bt A )
533 {λ p → replacePR key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) (λ _ _ _ → Lift n ⊤ ) }
534 (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = P0 ; si = proj2 P ; ri = R ; ci = lift tt }
535 $ λ p P1 loop → replaceP key value (proj2 (proj2 p)) (proj1 p) P1
536 (λ key value {tree1} repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ P2 lt )
537 $ λ tree repl P → exit tree repl ⟪ RTtoTI0 _ _ _ _ (proj1 P) (proj2 P) , proj2 P ⟫
538
539 insertTestP1 = insertTreeP leaf 1 1 t-leaf
540 $ λ _ x0 P0 → insertTreeP x0 2 1 (proj1 P0)
541 $ λ _ x1 P1 → insertTreeP x1 3 2 (proj1 P1)
542 $ λ _ x2 P2 → insertTreeP x2 2 2 (proj1 P2) (λ _ x P → x )
543
544 top-value : {n : Level} {A : Set n} → (tree : bt A) → Maybe A
545 top-value leaf = nothing
546 top-value (node key value tree tree₁) = just value
547 -}