Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 628:ec2506b532ba

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 08 Nov 2021 23:44:24 +0900
parents 967547859521
children 7a19d4b43795
comparison
equal deleted inserted replaced
627:967547859521 628:ec2506b532ba
227 {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant key (proj1 (proj2 p)) tree (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) } 227 {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant key (proj1 (proj2 p)) tree (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) }
228 (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!} , R ⟫ ⟫ 228 (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!} , R ⟫ ⟫
229 $ λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) {!!} 229 $ λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) {!!}
230 (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ {!!} lt ) exit 230 (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ {!!} lt ) exit
231 231
232 -- findP key tree stack = findPP key tree stack {findPR} → record { ti = tree-invariant tree ; si stack-invariant tree stack } → 232 record findP-contains {n : Level} {A : Set n} (key1 : ℕ) (value1 : A) (tree : bt A ) (stack : List (bt A)) : Set n where
233
234 record findP-contains {n : Level} {A : Set n} (tree : bt A ) (stack : List (bt A)) : Set n where
235 field 233 field
236 key1 : ℕ
237 value1 : A
238 tree1 : bt A 234 tree1 : bt A
239 ci : replacedTree key1 value1 tree tree1 235 ci : replacedTree key1 value1 tree tree1
240 236
241 findPPC : {n m : Level} {A : Set n} {t : Set m} 237 findPPC : {n m : Level} {A : Set n} {t : Set m}
242 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A)) 238 → (key : ℕ) → (value : A) → (tree : bt A ) → (stack : List (bt A))
243 → (Pre : findPR key tree stack findP-contains) 239 → (Pre : findPR key tree stack (findP-contains key value))
244 → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR key tree1 stack1 findP-contains → bt-depth tree1 < bt-depth tree → t ) 240 → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR key tree1 stack1 (findP-contains key value) → bt-depth tree1 < bt-depth tree → t )
245 → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key) → findPR key tree1 stack1 findP-contains → t) → t 241 → (exit : (tree1 : bt A) → (stack1 : List (bt A)) → ( tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key) → findPR key tree1 stack1 (findP-contains key value) → t) → t
246 findPPC = {!!} 242 findPPC = {!!}
247 243
248 containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤ 244 containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤
249 containsTree {n} {m} {A} {t} tree tree1 key value P RT = 245 containsTree {n} {m} {A} {t} tree tree1 key value P RT =
250 TerminatingLoopS (bt A ∧ List (bt A) ) 246 TerminatingLoopS (bt A ∧ List (bt A) )
251 {λ p → findPR key (proj1 p) (proj2 p) findP-contains } (λ p → bt-depth (proj1 p)) 247 {λ p → findPR key (proj1 p) (proj2 p) (findP-contains key value ) } (λ p → bt-depth (proj1 p))
252 ⟪ tree1 , [] ⟫ {!!} 248 ⟪ tree1 , [] ⟫ {!!}
253 $ λ p P loop → findPPC key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) 249 $ λ p P loop → findPPC key value (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt )
254 $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value (lemma7 {!!} {!!} found? ) where 250 $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value (lemma7 {!!} (findPR.si P2 ) found? ) where
255 lemma7 : {key : ℕ } {value1 : A } {t1 tree : bt A } { s1 : List (bt A) } → 251 lemma7 : {key : ℕ } {value1 : A } {t1 tree : bt A } { s1 : List (bt A) } →
256 replacedTree key value1 tree t1 → stackInvariant key t1 tree s1 → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key) → top-value t1 ≡ just value 252 replacedTree key value1 tree t1 → stackInvariant key t1 tree s1 → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key) → top-value t1 ≡ just value
257 lemma7 = ? 253 lemma7 = {!!}
258 254