Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 677:681577b60c35

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
child-replaced
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 29 Nov 2021 09:06:31 +0900
parents 49f1c24842cb
children 8dd9b11aa358
comparison
equal deleted inserted replaced
676:49f1c24842cb 677:681577b60c35
112 s-right : {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 112 s-right : {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
113 → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree tree0 (tree ∷ st) 113 → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
114 s-left : {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 114 s-left : {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
115 → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree₁ tree0 (tree₁ ∷ st) 115 → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree₁ tree0 (tree₁ ∷ st)
116 116
117 data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree tree1 : bt A ) → Set n where 117 data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt A ) → Set n where
118 r-leaf : replacedTree key value leaf (node key value leaf leaf) 118 r-leaf : replacedTree key value leaf (node key value leaf leaf)
119 r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁) 119 r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁)
120 r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A} 120 r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
121 → k < key → replacedTree key value t t2 → replacedTree key value (node k v1 t1 t) t 121 → k < key → replacedTree key value t2 t → replacedTree key value (node k v1 t1 t2) (node k v1 t1 t)
122 r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A} 122 r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
123 → k > key → replacedTree key value t t2 → replacedTree key value (node k v1 t t1) t 123 → k > key → replacedTree key value t1 t → replacedTree key value (node k v1 t1 t2) (node k v1 t t2)
124 124
125 add< : { i : ℕ } (j : ℕ ) → i < suc i + j 125 add< : { i : ℕ } (j : ℕ ) → i < suc i + j
126 add< {i} j = begin 126 add< {i} j = begin
127 suc i ≤⟨ m≤m+n (suc i) j ⟩ 127 suc i ≤⟨ m≤m+n (suc i) j ⟩
128 suc i + j ∎ where open ≤-Reasoning 128 suc i + j ∎ where open ≤-Reasoning
189 si2 {tree₁ } {key₁ } {v1 } si = stackTreeInvariant key (node key₁ v1 sub tree₁ ) tree st ti si 189 si2 {tree₁ } {key₁ } {v1 } si = stackTreeInvariant key (node key₁ v1 sub tree₁ ) tree st ti si
190 190
191 rt-property1 : {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf ) 191 rt-property1 : {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
192 rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf () 192 rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf ()
193 rt-property1 {n} {A} key value .(node key _ _ _) .(node key value _ _) r-node () 193 rt-property1 {n} {A} key value .(node key _ _ _) .(node key value _ _) r-node ()
194 rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-right x rt) = ? 194 rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-right x rt) = λ ()
195 rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-left x rt) = ? 195 rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-left x rt) = λ ()
196 196
197 depth-1< : {i j : ℕ} → suc i ≤ suc (i Data.Nat.⊔ j ) 197 depth-1< : {i j : ℕ} → suc i ≤ suc (i Data.Nat.⊔ j )
198 depth-1< {i} {j} = s≤s (m≤m⊔n _ j) 198 depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
199 199
200 depth-2< : {i j : ℕ} → suc i ≤ suc (j Data.Nat.⊔ i ) 200 depth-2< : {i j : ℕ} → suc i ≤ suc (j Data.Nat.⊔ i )
253 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥ 253 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥
254 lemma3 refl () 254 lemma3 refl ()
255 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥ 255 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
256 lemma5 (s≤s z≤n) () 256 lemma5 (s≤s z≤n) ()
257 257
258 child-replaced : {n : Level} {A : Set n} (key : ℕ) (value : A) (stack : List (bt A)) (tree tree0 : bt A) → stackInvariant key tree tree0 stack → bt A
259 child-replaced key value .(tree ∷ []) tree .tree s-single = tree
260 child-replaced key value .(leaf ∷ _) leaf tree0 (s-right x si) = leaf
261 child-replaced key value .(node key₁ value₁ tree tree₁ ∷ _) (node key₁ value₁ tree tree₁) tree0 (s-right x si) = tree
262 child-replaced key value .(leaf ∷ _) leaf tree0 (s-left x si) = leaf
263 child-replaced key value .(node key₁ value₁ tree tree₁ ∷ _) (node key₁ value₁ tree tree₁) tree0 (s-left x si) = tree₁
264
258 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 265 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
259 field 266 field
260 tree0 : bt A 267 tree0 : bt A
261 ti : treeInvariant tree0 268 ti : treeInvariant tree0
262 si : stackInvariant key tree tree0 stack 269 si : stackInvariant key tree tree0 stack
263 ri : replacedTree key value tree repl 270 ri : replacedTree key value (child-replaced key value stack tree tree0 si) repl
264 ci : C tree repl stack -- data continuation 271 ci : C tree repl stack -- data continuation
265 272
266 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) 273 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
267 → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) 274 → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key )
268 → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value tree tree1 → t) → t 275 → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value tree tree1 → t) → t
275 → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A)) 282 → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A))
276 → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t) 283 → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t)
277 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t 284 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
278 replaceP key value {tree} repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen 285 replaceP key value {tree} repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen
279 replaceP key value {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ (replacePR.si Pre)-- tree0 ≡ leaf 286 replaceP key value {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ (replacePR.si Pre)-- tree0 ≡ leaf
280 ... | eq = exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ replacePR.ti Pre , {!!} ⟫ 287 ... | refl = exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ replacePR.ti Pre , r-leaf ⟫
281 replaceP key value {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁ 288 replaceP key value {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁
282 ... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) (node key₁ value₁ repl right ) ⟪ replacePR.ti Pre , {!!} ⟫ where 289 ... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) repl ⟪ replacePR.ti Pre , repl01 ⟫ where
283 repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ repl right) 290 repl01 : replacedTree key value (replacePR.tree0 Pre) repl
284 repl01 = {!!} 291 repl01 = subst (λ k → replacedTree key value k _) {!!} ( replacePR.ri Pre )
285 ... | tri≈ ¬a b ¬c = exit {!!} (node key₁ value left right ) ⟪ {!!} , {!!} ⟫ -- can't happen 292 ... | tri≈ ¬a b ¬c = exit {!!} (node key₁ value left right ) ⟪ {!!} , {!!} ⟫ -- can't happen
286 ... | tri> ¬a ¬b c = exit {!!} (node key₁ value₁ left repl ) ⟪ {!!} , {!!} ⟫ 293 ... | tri> ¬a ¬b c = exit {!!} (node key₁ value₁ left repl ) ⟪ {!!} , {!!} ⟫
287 replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen 294 replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen
288 replaceP {n} {_} {A} key value {tree} repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁ | si-property1 (replacePR.si Pre) 295 replaceP {n} {_} {A} key value {tree} repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁ | si-property1 (replacePR.si Pre)
289 ... | tri< a ¬b ¬c | refl = next key value {{!!}} (node key₁ value₁ repl right ) st Post ≤-refl where 296 ... | tri< a ¬b ¬c | refl = next key value {{!!}} (node key₁ value₁ repl right ) st Post ≤-refl where