Mercurial > hg > Members > Moririn

comparison hoareBinaryTree.agda @ 666:f344e6b254d8

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, 22 Nov 2021 14:50:09 +0900
parents 1708fe988ac5
children eb3721179793
comparison
equal deleted inserted replaced
665:1708fe988ac5 666:f344e6b254d8
148 stack-last (x ∷ s) = stack-last s 148 stack-last (x ∷ s) = stack-last s
149 149
150 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] ) 150 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
151 stackInvariantTest1 = s-right (add< 2) s-single 151 stackInvariantTest1 = s-right (add< 2) s-single
152 152
153 si-property0 : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → stackInvariant key tree tree0 stack → ¬ ( stack ≡ [] ) 153 si-property0 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → {stack : List (bt A)} → stackInvariant key tree tree0 stack → ¬ ( stack ≡ [] )
154 si-property0 key tree .tree .(tree ∷ []) s-single () 154 si-property0 s-single ()
155 si-property0 key tree tree0 .(tree ∷ _) (s-right x si) () 155 si-property0 (s-right x si) ()
156 si-property0 key tree tree0 .(tree ∷ _) (s-left x si) () 156 si-property0 (s-left x si) ()
157 157
158 si-property1 : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → stackInvariant key tree tree0 stack 158 si-property1 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 tree1 : bt A} → {stack : List (bt A)} → stackInvariant key tree tree0 (tree1 ∷ stack)
159 → stack-top stack ≡ just tree 159 → tree1 ≡ tree
160 si-property1 key t t0 (t ∷ []) s-single = refl 160 si-property1 s-single = refl
161 si-property1 key t t0 (t ∷ st) (s-right _ si) = refl 161 si-property1 (s-right _ si) = refl
162 si-property1 key t t0 (t ∷ st) (s-left _ si) = refl 162 si-property1 (s-left _ si) = refl
163 163
164 si-property-last : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → stackInvariant key tree tree0 stack 164 si-property-last : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → stackInvariant key tree tree0 stack
165 → stack-last stack ≡ just tree0 165 → stack-last stack ≡ just tree0
166 si-property-last key t t0 (t ∷ []) s-single = refl 166 si-property-last key t t0 (t ∷ []) s-single = refl
167 si-property-last key t t0 (.t ∷ x ∷ st) (s-right _ si ) with si-property1 key _ _ (x ∷ st) si 167 si-property-last key t t0 (.t ∷ x ∷ st) (s-right _ si ) with si-property1 si
168 ... | refl = si-property-last key x t0 (x ∷ st) si 168 ... | refl = si-property-last key x t0 (x ∷ st) si
169 si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ si ) with si-property1 key _ _ (x ∷ st) si 169 si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ si ) with si-property1 si
170 ... | refl = si-property-last key x t0 (x ∷ st) si 170 ... | refl = si-property-last key x t0 (x ∷ st) si
171 171
172 ti-right : {n : Level} {A : Set n} {tree₁ repl : bt A} → {key₁ : ℕ} → {v1 : A} → treeInvariant (node key₁ v1 tree₁ repl) → treeInvariant repl 172 ti-right : {n : Level} {A : Set n} {tree₁ repl : bt A} → {key₁ : ℕ} → {v1 : A} → treeInvariant (node key₁ v1 tree₁ repl) → treeInvariant repl
173 ti-right {_} {_} {.leaf} {_} {key₁} {v1} (t-single .key₁ .v1) = t-leaf 173 ti-right {_} {_} {.leaf} {_} {key₁} {v1} (t-single .key₁ .v1) = t-leaf
174 ti-right {_} {_} {.leaf} {_} {key₁} {v1} (t-right x ti) = ti 174 ti-right {_} {_} {.leaf} {_} {key₁} {v1} (t-right x ti) = ti
268 → (key : ℕ) → (value : A) → {tree0 tree tree-st : bt A} ( repl : bt A) 268 → (key : ℕ) → (value : A) → {tree0 tree tree-st : bt A} ( repl : bt A)
269 → (stack : List (bt A)) → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack ∧ replacedTree key value tree repl 269 → (stack : List (bt A)) → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack ∧ replacedTree key value tree repl
270 → (next : ℕ → A → {tree0 tree1 tree-st : bt A } (repl : bt A) → (stack1 : List (bt A)) 270 → (next : ℕ → A → {tree0 tree1 tree-st : bt A } (repl : bt A) → (stack1 : List (bt A))
271 → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t) 271 → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t)
272 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t 272 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
273 replaceP key value {tree0} {tree} {tree-st} repl [] Pre next exit = ⊥-elim ( si-property0 _ _ _ _ (proj1 (proj2 Pre)) refl ) -- can't happen 273 replaceP key value {tree0} {tree} {tree-st} repl [] Pre next exit = ⊥-elim ( si-property0 (proj1 (proj2 Pre)) refl ) -- can't happen
274 replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ []) Pre next exit = 274 replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ []) Pre next exit =
275 exit tree0 (node key value leaf leaf) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} r-leaf ⟫ 275 exit tree0 (node key value leaf leaf) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} r-leaf ⟫
276 replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁ 276 replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁
277 ... | tri< a ¬b ¬c = exit tree0 (node key₁ value₁ tree right ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫ 277 ... | tri< a ¬b ¬c = exit tree0 (node key₁ value₁ tree right ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} (r-left a (proj2 (proj2 Pre)) ) ⟫
278 ... | tri≈ ¬a b ¬c = exit tree0 (node key₁ value left right ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫ 278 ... | tri≈ ¬a refl ¬c = exit tree0 (node key₁ value left right ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} r-node ⟫
279 ... | tri> ¬a ¬b c = exit tree0 (node key₁ value₁ left tree ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫ 279 ... | tri> ¬a ¬b c = exit tree0 (node key₁ value₁ left tree ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫
280 replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ st@(_ ∷ _)) Pre next exit = 280 replaceP {n} {_} {A} key value {tree0} {tree} {tree-st} repl (leaf ∷ st@(_ ∷ _)) Pre next exit =
281 next key value {tree0} (node key value leaf leaf) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫ ⟫ ≤-refl 281 next key value {tree0} (node key value leaf leaf) st
282 ⟪ proj1 Pre , ⟪ repl01 (sym (si-property1 (proj1 (proj2 Pre)))) (proj1 (proj2 Pre))
283 , subst (λ k → replacedTree key value k (node key value leaf leaf) ) (si-property1 (proj1 (proj2 Pre))) r-leaf ⟫ ⟫ ≤-refl where
284 repl01 : {x : bt A} → { xs : List (bt A)} → tree-st ≡ leaf → stackInvariant key tree-st tree0 (leaf ∷ x ∷ xs) → stackInvariant key x tree0 (x ∷ xs)
285 repl01 {x} {xs} refl (s-right lt si) = subst (λ k → stackInvariant key k tree0 (x ∷ xs) ) (sym (si-property1 si)) si
286 repl01 {x} {xs} refl (s-left lt si) = subst (λ k → stackInvariant key k tree0 (x ∷ xs) ) (sym (si-property1 si)) si
282 replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ st@(_ ∷ _)) Pre next exit with <-cmp key key₁ 287 replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ st@(_ ∷ _)) Pre next exit with <-cmp key key₁
283 ... | tri< a ¬b ¬c = next key value {tree0} (node key₁ value₁ tree right ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫ ⟫ ≤-refl 288 ... | tri< a ¬b ¬c = next key value {tree0} (node key₁ value₁ tree right ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫ ⟫ ≤-refl
284 ... | tri≈ ¬a b ¬c = next key value {tree0} (node key₁ value left right ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫ ⟫ ≤-refl 289 ... | tri≈ ¬a b ¬c = next key value {tree0} (node key₁ value left right ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫ ⟫ ≤-refl
285 ... | tri> ¬a ¬b c = next key value {tree0} (node key₁ value₁ left tree ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫ ⟫ ≤-refl 290 ... | tri> ¬a ¬b c = next key value {tree0} (node key₁ value₁ left tree ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫ ⟫ ≤-refl
286 291