Mercurial > hg > Members > Moririn

comparison hoareBinaryTree.agda @ 660:712e2998c76b

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 Sun, 21 Nov 2021 19:03:22 +0900
parents afcccfaea264
children 323533798054
comparison
equal deleted inserted replaced
659:afcccfaea264 660:712e2998c76b
101 → treeInvariant (node key value t₁ t₂) 101 → treeInvariant (node key value t₁ t₂)
102 → treeInvariant (node key₂ value₂ t₃ t₄) 102 → treeInvariant (node key₂ value₂ t₃ t₄)
103 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) 103 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄))
104 104
105 data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (top orig : bt A) → (stack : List (bt A)) → Set n where 105 data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (top orig : bt A) → (stack : List (bt A)) → Set n where
106 s-nil : {tree : bt A} → stackInvariant key tree tree [] 106 s-nil : {tree tree0 : bt A} → stackInvariant key tree tree0 []
107 s-single : {tree tree0 : bt A} → stackInvariant key tree tree0 [] → stackInvariant key tree tree0 (tree ∷ []) 107 s-single : {tree tree0 : bt A} → stackInvariant key tree tree0 [] → stackInvariant key tree0 tree0 (tree0 ∷ [])
108 s-right : {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 108 s-right : {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
109 → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → ¬ (st ≡ []) → stackInvariant key tree tree0 (tree ∷ st) 109 → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → ¬ (st ≡ []) → stackInvariant key tree tree0 (tree ∷ st)
110 s-left : {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 110 s-left : {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
111 → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → ¬ (st ≡ []) → stackInvariant key tree₁ tree0 (tree₁ ∷ st) 111 → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → ¬ (st ≡ []) → stackInvariant key tree₁ tree0 (tree₁ ∷ st)
112 112
146 stack-last (x ∷ []) = just x 146 stack-last (x ∷ []) = just x
147 stack-last (x ∷ s) = stack-last s 147 stack-last (x ∷ s) = stack-last s
148 148
149 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] ) 149 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
150 stackInvariantTest1 = s-right (add< 2) (s-single s-nil) (λ ()) 150 stackInvariantTest1 = s-right (add< 2) (s-single s-nil) (λ ())
151
152 si-nil : {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → (si : stackInvariant key tree tree0 []) → tree ≡ tree0
153 si-nil s-nil = refl
154 151
155 si-property1 : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → ¬ (stack ≡ []) → stackInvariant key tree tree0 stack 152 si-property1 : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → ¬ (stack ≡ []) → stackInvariant key tree tree0 stack
156 → stack-top stack ≡ just tree 153 → stack-top stack ≡ just tree
157 si-property1 key t t0 [] ne (s-nil ) = ⊥-elim ( ne refl ) 154 si-property1 key t t0 [] ne (s-nil ) = ⊥-elim ( ne refl )
158 si-property1 key t t0 (t ∷ []) ne (s-single _) = refl 155 si-property1 key t t0 (t ∷ []) ne (s-single _) = refl
181 ti-left {_} {_} {_} {_} {key₁} {v1} (t-right x ti) = t-leaf 178 ti-left {_} {_} {_} {_} {key₁} {v1} (t-right x ti) = t-leaf
182 ti-left {_} {_} {_} {_} {key₁} {v1} (t-left x ti) = ti 179 ti-left {_} {_} {_} {_} {key₁} {v1} (t-left x ti) = ti
183 ti-left {_} {_} {.(node _ _ _ _)} {_} {key₁} {v1} (t-node x x₁ ti ti₁) = ti 180 ti-left {_} {_} {.(node _ _ _ _)} {_} {key₁} {v1} (t-node x x₁ ti ti₁) = ti
184 181
185 stackTreeInvariant : {n : Level} {A : Set n} (key : ℕ) (sub tree : bt A) → (stack : List (bt A)) 182 stackTreeInvariant : {n : Level} {A : Set n} (key : ℕ) (sub tree : bt A) → (stack : List (bt A))
186 → treeInvariant tree → stackInvariant key sub tree stack → treeInvariant sub 183 → treeInvariant tree → stackInvariant key sub tree stack → ¬ (stack ≡ []) → treeInvariant sub
187 stackTreeInvariant {_} {A} key sub tree [] ti s-nil = ti 184 stackTreeInvariant {_} {A} key sub tree [] ti s-nil ne = ⊥-elim ( ne refl )
188 stackTreeInvariant {_} {A} key sub tree (sub ∷ []) ti (s-single s-nil ) = ti 185 stackTreeInvariant {_} {A} key sub tree (sub ∷ []) ti (s-single s-nil ) _ = ti
189 stackTreeInvariant {_} {A} key sub tree (sub ∷ st) ti (s-right _ si _) = ti-right (si1 si) where 186 stackTreeInvariant {_} {A} key sub tree (sub ∷ st) ti (s-right _ si ne) _ = ti-right (si1 si) where
190 si1 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant key (node key₁ v1 tree₁ sub ) tree st → treeInvariant (node key₁ v1 tree₁ sub ) 187 si1 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant key (node key₁ v1 tree₁ sub ) tree st → treeInvariant (node key₁ v1 tree₁ sub )
191 si1 {tree₁ } {key₁ } {v1 } si = stackTreeInvariant key (node key₁ v1 tree₁ sub ) tree st ti si 188 si1 {tree₁ } {key₁ } {v1 } si = stackTreeInvariant key (node key₁ v1 tree₁ sub ) tree st ti si ne
192 stackTreeInvariant {_} {A} key sub tree (sub ∷ st) ti (s-left _ si _) = ti-left ( si2 si) where 189 stackTreeInvariant {_} {A} key sub tree (sub ∷ st) ti (s-left _ si ne) _ = ti-left ( si2 si) where
193 si2 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant key (node key₁ v1 sub tree₁ ) tree st → treeInvariant (node key₁ v1 sub tree₁ ) 190 si2 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant key (node key₁ v1 sub tree₁ ) tree st → treeInvariant (node key₁ v1 sub tree₁ )
194 si2 {tree₁ } {key₁ } {v1 } si = stackTreeInvariant key (node key₁ v1 sub tree₁ ) tree st ti si 191 si2 {tree₁ } {key₁ } {v1 } si = stackTreeInvariant key (node key₁ v1 sub tree₁ ) tree st ti si ne
195 192
196 rt-property1 : {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf ) 193 rt-property1 : {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
197 rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf () 194 rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf ()
198 rt-property1 {n} {A} key value .(node key _ _ _) .(node key value _ _) r-node () 195 rt-property1 {n} {A} key value .(node key _ _ _) .(node key value _ _) r-node ()
199 rt-property1 {n} {A} key value .(node _ _ _ _) .(node _ _ _ _) (r-right x rt) () 196 rt-property1 {n} {A} key value .(node _ _ _ _) .(node _ _ _ _) (r-right x rt) ()
228 225
229 226
230 open _∧_ 227 open _∧_
231 228
232 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A)) 229 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
233 → treeInvariant tree ∧ stackInvariant key tree tree0 stack 230 → treeInvariant tree ∧ ((¬ (stack ≡ []) → stackInvariant key tree tree0 stack ))
234 → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t ) 231 → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ ((¬ (stack ≡ []) → stackInvariant key tree1 tree0 stack)) → bt-depth tree1 < bt-depth tree → t )
235 → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack 232 → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ ((¬ (stack ≡ []) → stackInvariant key tree1 tree0 stack))
236 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t 233 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t
237 findP key leaf tree0 st Pre _ exit = exit leaf tree0 st Pre (case1 refl) 234 findP key leaf tree0 st Pre _ exit = exit leaf tree0 st Pre (case1 refl)
238 findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁ 235 findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁
239 findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n tree0 st Pre (case2 refl) 236 findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n tree0 st Pre (case2 refl)
240 findP {n} {_} {A} key (node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (tree ∷ st) 237 findP {n} {_} {A} key (node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (tree ∷ st)
241 ⟪ treeLeftDown tree tree₁ (proj1 Pre) , ? ⟫ depth-1< where 238 ⟪ treeLeftDown tree tree₁ (proj1 Pre) , (λ ne → findP1 a st (proj2 Pre )) ⟫ depth-1< where
242 findP0 : key < key₁ → (st : List (bt A)) → stackInvariant key (node key₁ v1 tree tree₁) tree0 st → Set n 239 findP1 : key < key₁ → (st : List (bt A)) → ( ¬ (st ≡ [] ) → stackInvariant key (node key₁ v1 tree tree₁) tree0 st ) → stackInvariant key tree tree0 (tree ∷ st)
243 findP0 a [] si = stackInvariant key tree0 tree0 (tree0 ∷ []) 240 findP1 a [] si = {!!} -- s-single s-nil
244 findP0 a (x ∷ st) si = stackInvariant key tree tree0 (tree ∷ x ∷ st) 241 findP1 a (x ∷ st) si with si {!!}
245 findP1 : (a : key < key₁ ) → (st : List (bt A)) → (si : stackInvariant key (node key₁ v1 tree tree₁) tree0 st) → findP0 a st si 242 ... | t = s-left a t {!!}
246 findP1 a (x ∷ st) si = s-left a si (λ ()) 243 findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , {!!} ⟫ depth-2<
247 findP1 a [] s-nil = s-single s-nil
248 findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right c (proj2 Pre) {!!} ⟫ depth-2<
249 244
250 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₁) 245 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₁)
251 replaceTree1 k v1 value (t-single .k .v1) = t-single k value 246 replaceTree1 k v1 value (t-single .k .v1) = t-single k value
252 replaceTree1 k v1 value (t-right x t) = t-right x t 247 replaceTree1 k v1 value (t-right x t) = t-right x t
253 replaceTree1 k v1 value (t-left x t) = t-left x t 248 replaceTree1 k v1 value (t-left x t) = t-left x t