Mercurial > hg > Members > Moririn
comparison hoareBinaryTree.agda @ 648:6c3d50b30bea
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 19 Nov 2021 20:07:09 +0900 |
| parents | 7b24e17e1441 |
| children | cc62eb4758b0 |
comparison
equal
deleted
inserted
replaced
| 647:7b24e17e1441 | 648:6c3d50b30bea |
|---|---|
| 241 → (next : ℕ → A → {tree0 tree1 : bt A } (repl : bt A) → (stack1 : List (bt A)) | 241 → (next : ℕ → A → {tree0 tree1 : bt A } (repl : bt A) → (stack1 : List (bt A)) |
| 242 → treeInvariant tree0 ∧ stackInvariant key tree1 tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t) | 242 → treeInvariant tree0 ∧ stackInvariant key tree1 tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t) |
| 243 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t | 243 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t |
| 244 replaceP key value {tree0} {tree} repl [] Pre next exit with proj1 (proj2 Pre) | 244 replaceP key value {tree0} {tree} repl [] Pre next exit with proj1 (proj2 Pre) |
| 245 ... | () | 245 ... | () |
| 246 replaceP key value {tree0} {tree} repl (leaf ∷ []) Pre next exit = exit tree0 (node key value leaf leaf) ⟪ {!!} , {!!} ⟫ | 246 replaceP {_} {_} {A} key value {tree0} {tree} repl (leaf ∷ []) Pre next exit = |
| 247 exit tree0 repl ⟪ proj1 Pre , subst (λ k → replacedTree key value k repl ) (repl4 (proj1 (proj2 Pre))) (proj2 (proj2 Pre)) ⟫ where | |
| 248 repl4 : stackInvariant key tree tree0 (leaf ∷ []) → tree ≡ tree0 | |
| 249 repl4 (s-single .leaf) = refl | |
| 247 replaceP key value {tree0} {tree} repl (leaf ∷ leaf ∷ st) Pre next exit = {!!} -- can't happen | 250 replaceP key value {tree0} {tree} repl (leaf ∷ leaf ∷ st) Pre next exit = {!!} -- can't happen |
| 248 replaceP key value {tree0} {tree} repl (leaf ∷ node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ | 251 replaceP key value {tree0} {tree} repl (leaf ∷ node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ |
| 249 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ left {!!} ) st {!!} ? | 252 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ left repl ) st {!!} {!!} |
| 250 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right) st {!!} {!!} | 253 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right) st {!!} {!!} |
| 251 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ {!!} right) st {!!} {!!} | 254 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right) st {!!} {!!} |
| 252 replaceP key value {tree0} {tree} repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ | 255 replaceP key value {tree0} {tree} repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ |
| 253 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right ) st {!!} ≤-refl | 256 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right ) st {!!} ≤-refl |
| 254 ... | tri≈ ¬a b ¬c = next key value (node key value left right ) st {!!} ≤-refl where -- this case won't happen | 257 ... | tri≈ ¬a b ¬c = next key value (node key value left right ) st {!!} ≤-refl where -- this case won't happen |
| 255 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ left repl) st ⟪ proj1 Pre , ⟪ {!!} , r-right a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl where | 258 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ left repl) st ⟪ proj1 Pre , ⟪ {!!} , r-right a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl where |
| 256 repl2 : stackInvariant key tree tree0 (node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ left tree) tree0 st | 259 repl2 : stackInvariant key tree tree0 (node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ left tree) tree0 st |
| 257 repl2 (s-single .(node key₁ value₁ left right)) = {!!} | 260 repl2 (s-single .(node key₁ value₁ left right)) = {!!} |
| 258 repl2 (s-right _ si) = {!!} | 261 repl2 (s-right _ si) = {!!} |
| 259 repl2 (s-left _ si) = {!!} | 262 repl2 (s-left _ si) = {!!} |
| 260 | 263 |
| 261 | |
| 262 --- ... next key value (node key₁ value₁ left tree ) (node key₁ value₁ left repl ) st ≤-refl where | |
| 263 | 264 |
| 264 open import Relation.Binary.Definitions | 265 open import Relation.Binary.Definitions |
| 265 | 266 |
| 266 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ | 267 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ |
| 267 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x | 268 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x |