Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 639:5fe23f540726

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
replacedTree
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 15 Nov 2021 17:04:13 +0900
parents be6bd51c3f05
children e0bea7a2bb4d
comparison
equal deleted inserted replaced
638:be6bd51c3f05 639:5fe23f540726
95 t-node : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂) 95 t-node : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂)
96 → treeInvariant (node key value t₁ t₂) 96 → treeInvariant (node key value t₁ t₂)
97 → treeInvariant (node key₂ value₂ t₃ t₄) 97 → treeInvariant (node key₂ value₂ t₃ t₄)
98 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) 98 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄))
99 99
100 add< : { i : ℕ } (j : ℕ ) → i < suc i + j
101 add< {i} j = begin
102 suc i ≤⟨ m≤m+n (suc i) j ⟩
103 suc i + j ∎ where open ≤-Reasoning
104
105 treeTest1 : bt ℕ
106 treeTest1 = node 1 0 leaf (node 3 1 (node 2 5 (node 4 7 leaf leaf ) leaf) (node 5 5 leaf leaf))
107 treeTest2 : bt ℕ
108 treeTest2 = node 3 1 (node 2 5 (node 4 7 leaf leaf ) leaf) (node 5 5 leaf leaf)
109
110 treeInvariantTest1 : treeInvariant treeTest1
111 treeInvariantTest1 = t-right (m≤m+n _ 1) (t-node (add< 0) (add< 1) (t-left (add< 1) (t-single 4 7)) (t-single 5 5) )
112
113 data stackInvariant {n : Level} {A : Set n} : (tree tree0 : bt A) → (stack : List (bt A)) → Set n where 100 data stackInvariant {n : Level} {A : Set n} : (tree tree0 : bt A) → (stack : List (bt A)) → Set n where
114 s-nil : stackInvariant leaf leaf []
115 s-single : (tree : bt A) → stackInvariant tree tree (tree ∷ [] ) 101 s-single : (tree : bt A) → stackInvariant tree tree (tree ∷ [] )
116 s-right : {tree0 tree tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 102 s-right : {tree0 tree tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
117 → stackInvariant (node key₁ v1 tree tree₁) tree0 st → stackInvariant tree₁ tree0 (tree₁ ∷ st) 103 → stackInvariant (node key₁ v1 tree tree₁) tree0 st → stackInvariant tree₁ tree0 (tree₁ ∷ st)
118 s-left : {tree0 tree tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 104 s-left : {tree0 tree tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
119 → stackInvariant (node key₁ v1 tree tree₁) tree0 st → stackInvariant tree tree0 (tree ∷ st) 105 → stackInvariant (node key₁ v1 tree tree₁) tree0 st → stackInvariant tree tree0 (tree ∷ st)
120
121 stackInvariantTest0 : stackInvariant {_} {ℕ} leaf leaf []
122 stackInvariantTest0 = s-nil
123
124 stackInvariantTest1 : stackInvariant treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
125 stackInvariantTest1 = s-right (s-single treeTest1 )
126 106
127 data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree tree1 : bt A ) → Set n where 107 data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree tree1 : bt A ) → Set n where
128 r-leaf : replacedTree key value leaf (node key value leaf leaf) 108 r-leaf : replacedTree key value leaf (node key value leaf leaf)
129 r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁) 109 r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁)
130 r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A} 110 r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
131 → k > key → replacedTree key value t1 t2 → replacedTree key value (node k v1 t t1) (node k v1 t t2) 111 → k > key → replacedTree key value t1 t2 → replacedTree key value (node k v1 t t1) (node k v1 t t2)
132 r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A} 112 r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
133 → k < key → replacedTree key value t1 t2 → replacedTree key value (node k v1 t1 t) (node k v1 t2 t) 113 → k < key → replacedTree key value t1 t2 → replacedTree key value (node k v1 t1 t) (node k v1 t2 t)
114
115 add< : { i : ℕ } (j : ℕ ) → i < suc i + j
116 add< {i} j = begin
117 suc i ≤⟨ m≤m+n (suc i) j ⟩
118 suc i + j ∎ where open ≤-Reasoning
119
120 treeTest1 : bt ℕ
121 treeTest1 = node 1 0 leaf (node 3 1 (node 2 5 (node 4 7 leaf leaf ) leaf) (node 5 5 leaf leaf))
122 treeTest2 : bt ℕ
123 treeTest2 = node 3 1 (node 2 5 (node 4 7 leaf leaf ) leaf) (node 5 5 leaf leaf)
124
125 treeInvariantTest1 : treeInvariant treeTest1
126 treeInvariantTest1 = t-right (m≤m+n _ 1) (t-node (add< 0) (add< 1) (t-left (add< 1) (t-single 4 7)) (t-single 5 5) )
127
128 stack-top : {n : Level} {A : Set n} (stack : List (bt A)) → Maybe (bt A)
129 stack-top [] = nothing
130 stack-top (x ∷ s) = just x
131
132 stack-last : {n : Level} {A : Set n} (stack : List (bt A)) → Maybe (bt A)
133 stack-last [] = nothing
134 stack-last (x ∷ []) = just x
135 stack-last (x ∷ s) = stack-last s
136
137 stackInvariantTest1 : stackInvariant treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
138 stackInvariantTest1 = s-right (s-single treeTest1 )
139
140 si-property1 : {n : Level} {A : Set n} (tree tree0 : bt A) → (stack : List (bt A)) → stackInvariant tree tree0 stack
141 → stack-top stack ≡ just tree
142 si-property1 t t0 (x ∷ .[]) (s-single .x) = refl
143 si-property1 t t0 (t ∷ st) (s-right si) = refl
144 si-property1 t t0 (t ∷ st) (s-left si) = refl
145
146 si-property-last : {n : Level} {A : Set n} (tree tree0 : bt A) → (stack : List (bt A)) → stackInvariant tree tree0 stack
147 → stack-last stack ≡ just tree0
148 si-property-last t t0 (x ∷ []) (s-single .x) = refl
149 si-property-last t t0 (.t ∷ x ∷ st) (s-right si) with si-property1 _ _ (x ∷ st) si
150 ... | refl = si-property-last x t0 (x ∷ st) si
151 si-property-last t t0 (.t ∷ x ∷ st) (s-left si) with si-property1 _ _ (x ∷ st) si
152 ... | refl = si-property-last x t0 (x ∷ st) si
153
154 rt-property1 : {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
155 rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf ()
156 rt-property1 {n} {A} key value .(node key _ _ _) .(node key value _ _) r-node ()
157 rt-property1 {n} {A} key value .(node _ _ _ _) .(node _ _ _ _) (r-right x rt) ()
158 rt-property1 {n} {A} key value .(node _ _ _ _) .(node _ _ _ _) (r-left x rt) ()
159
134 depth-1< : {i j : ℕ} → suc i ≤ suc (i Data.Nat.⊔ j ) 160 depth-1< : {i j : ℕ} → suc i ≤ suc (i Data.Nat.⊔ j )
135 depth-1< {i} {j} = s≤s (m≤m⊔n _ j) 161 depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
136 162
137 depth-2< : {i j : ℕ} → suc i ≤ suc (j Data.Nat.⊔ i ) 163 depth-2< : {i j : ℕ} → suc i ≤ suc (j Data.Nat.⊔ i )
138 depth-2< {i} {j} = s≤s (m≤n⊔m _ i) 164 depth-2< {i} {j} = s≤s (m≤n⊔m _ i)
151 treeRightDown {n} {A} {_} {v1} .leaf .leaf (t-single _ .v1) = t-leaf 177 treeRightDown {n} {A} {_} {v1} .leaf .leaf (t-single _ .v1) = t-leaf
152 treeRightDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right x ti) = ti 178 treeRightDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right x ti) = ti
153 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left x ti) = t-leaf 179 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left x ti) = t-leaf
154 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node x x₁ ti ti₁) = ti₁ 180 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node x x₁ ti ti₁) = ti₁
155 181
156 -- stackInvariant key (node key₁ v1 tree tree₁) tree0 st
157 -- → stackInvariant key tree tree0 (node key₁ v1 tree tree₁ ∷ st)
158 182
159 open _∧_ 183 open _∧_
160 184
161 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A)) 185 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
162 → treeInvariant tree ∧ stackInvariant tree tree0 stack 186 → treeInvariant tree ∧ stackInvariant tree tree0 stack
184 replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 ) r-leaf 208 replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 ) r-leaf
185 replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P) r-node 209 replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P) r-node
186 210
187 replaceP : {n m : Level} {A : Set n} {t : Set m} 211 replaceP : {n m : Level} {A : Set n} {t : Set m}
188 → (key : ℕ) → (value : A) → (tree repl : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant repl tree stack ∧ replacedTree key value tree repl 212 → (key : ℕ) → (value : A) → (tree repl : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant repl tree stack ∧ replacedTree key value tree repl
189 → (next : ℕ → A → (tree1 repl : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant repl tree1 stack ∧ replacedTree key value tree1 repl → bt-depth tree1 < bt-depth tree → t ) 213 → (next : ℕ → A → (tree1 repl : bt A) → (stack1 : List (bt A))
214 → treeInvariant tree1 ∧ stackInvariant repl tree1 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t)
190 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t 215 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
191 replaceP key value tree repl [] Pre next exit = exit tree repl {!!} 216 replaceP key value tree repl [] Pre next exit = exit tree repl ⟪ proj1 Pre , proj2 (proj2 Pre) ⟫
192 replaceP key value tree repl (leaf ∷ st) Pre next exit = next key value tree {!!} st {!!} {!!} 217 replaceP key value tree repl (leaf ∷ st) Pre next exit with si-property1 _ _ _ (proj1 (proj2 Pre)) | rt-property1 _ _ _ _ (proj2 (proj2 Pre))
218 ... | refl | t1 = ⊥-elim ( t1 refl )
193 replaceP key value tree repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ 219 replaceP key value tree repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
194 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) {!!} st {!!} {!!} 220 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) (node key₁ value₁ repl right ) st {!!} ≤-refl
195 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) {!!} st {!!} {!!} 221 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right )(node key₁ value₁ left right ) st {!!} ≤-refl
196 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) {!!} st {!!} {!!} 222 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) (node key₁ value₁ left repl )st {!!} ≤-refl
197 223
198 open import Relation.Binary.Definitions 224 open import Relation.Binary.Definitions
199 225
200 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ 226 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
201 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x 227 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
233 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ ⟪ P , {!!} ⟫ 259 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ ⟪ P , {!!} ⟫
234 $ λ p P loop → findP key (proj1 p) tree (proj2 p) {!!} (λ t _ s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) 260 $ λ p P loop → findP key (proj1 p) tree (proj2 p) {!!} (λ t _ s P1 lt → loop ⟪ t , s ⟫ {!!} lt )
235 $ λ t _ s P C → replaceNodeP key value t C (proj1 P) 261 $ λ t _ s P C → replaceNodeP key value t C (proj1 P)
236 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A )) 262 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A ))
237 {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) tree (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) } 263 {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) tree (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) }
238 (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ proj1 P , ⟪ {!!} , R ⟫ ⟫ 264 (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ proj1 P , ⟪ {!!} , R ⟫ ⟫
239 $ λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) {!!} 265 $ λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) {!!}
240 (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ {!!} lt ) exit 266 (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ {!!} lt ) exit
241 267
242 top-value : {n : Level} {A : Set n} → (tree : bt A) → Maybe A 268 top-value : {n : Level} {A : Set n} → (tree : bt A) → Maybe A
243 top-value leaf = nothing 269 top-value leaf = nothing
278 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR key (proj1 p) (proj2 p) (λ t s → Lift n ⊤) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ {!!} 304 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR key (proj1 p) (proj2 p) (λ t s → Lift n ⊤) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ {!!}
279 $ λ p P loop → findPP key (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt ) 305 $ λ p P loop → findPP key (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )
280 $ λ t s _ P → replaceNodeP key value t {!!} {!!} 306 $ λ t s _ P → replaceNodeP key value t {!!} {!!}
281 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A )) 307 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A ))
282 {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) tree (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) } 308 {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant (proj1 (proj2 p)) tree (proj1 p) ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) }
283 (λ p → bt-depth (proj1 (proj2 p))) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!} , R ⟫ ⟫ 309 (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫　⟪ {!!} , ⟪ {!!} , R ⟫ ⟫
284 $ λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) {!!} 310 $ λ p P1 loop → replaceP key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) {!!}
285 (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ {!!} lt ) exit 311 (λ key value tree1 repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ {!!} lt ) exit
286 312
287 record findPC {n : Level} {A : Set n} (key1 : ℕ) (value1 : A) (tree : bt A ) (stack : List (bt A)) : Set n where 313 record findPC {n : Level} {A : Set n} (key1 : ℕ) (value1 : A) (tree : bt A ) (stack : List (bt A)) : Set n where
288 field 314 field