Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 675:7421e5c7e56c

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 Tue, 23 Nov 2021 15:11:56 +0900
parents b5fde9727830
children 49f1c24842cb
comparison
equal deleted inserted replaced
671:b5fde9727830 675:7421e5c7e56c
106 106
107 -- 107 --
108 -- stack always contains original top at end 108 -- stack always contains original top at end
109 -- 109 --
110 data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (top orig : bt A) → (stack : List (bt A)) → Set n where 110 data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (top orig : bt A) → (stack : List (bt A)) → Set n where
111 s-single : {tree0 : bt A} → ¬ ( tree0 ≡ leaf ) → stackInvariant key tree0 tree0 (tree0 ∷ []) 111 s-single : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [])
112 s-right : {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 112 s-right : {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
113 → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree tree0 (tree ∷ st) 113 → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
114 s-left : {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 114 s-left : {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
115 → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree₁ tree0 (tree₁ ∷ st) 115 → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree₁ tree0 (tree₁ ∷ st)
116 116
121 → k < key → replacedTree key value t1 t2 → replacedTree key value (node k v1 t t1) (node k v1 t t2) 121 → k < key → replacedTree key value t1 t2 → replacedTree key value (node k v1 t t1) (node k v1 t t2)
122 r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A} 122 r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
123 → k > key → replacedTree key value t1 t2 → replacedTree key value (node k v1 t1 t) (node k v1 t2 t) 123 → k > key → replacedTree key value t1 t2 → replacedTree key value (node k v1 t1 t) (node k v1 t2 t)
124 124
125 replFromStack : {n : Level} {A : Set n} {key : ℕ} {top orig : bt A} → {stack : List (bt A)} → stackInvariant key top orig stack → bt A 125 replFromStack : {n : Level} {A : Set n} {key : ℕ} {top orig : bt A} → {stack : List (bt A)} → stackInvariant key top orig stack → bt A
126 replFromStack (s-single {tree} _ ) = tree 126 replFromStack (s-single {tree} ) = tree
127 replFromStack (s-right {tree} x st) = tree 127 replFromStack (s-right {tree} x st) = tree
128 replFromStack (s-left {tree} x st) = tree 128 replFromStack (s-left {tree} x st) = tree
129 129
130 add< : { i : ℕ } (j : ℕ ) → i < suc i + j 130 add< : { i : ℕ } (j : ℕ ) → i < suc i + j
131 add< {i} j = begin 131 add< {i} j = begin
148 stack-last [] = nothing 148 stack-last [] = nothing
149 stack-last (x ∷ []) = just x 149 stack-last (x ∷ []) = just x
150 stack-last (x ∷ s) = stack-last s 150 stack-last (x ∷ s) = stack-last s
151 151
152 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] ) 152 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
153 stackInvariantTest1 = s-right (add< 2) (s-single (λ ())) 153 stackInvariantTest1 = s-right (add< 2) (s-single )
154 154
155 si-property0 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → {stack : List (bt A)} → stackInvariant key tree tree0 stack → ¬ ( stack ≡ [] ) 155 si-property0 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → {stack : List (bt A)} → stackInvariant key tree tree0 stack → ¬ ( stack ≡ [] )
156 si-property0 (s-single _ ) () 156 si-property0 (s-single ) ()
157 si-property0 (s-right x si) () 157 si-property0 (s-right x si) ()
158 si-property0 (s-left x si) () 158 si-property0 (s-left x si) ()
159 159
160 si-property1 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 tree1 : bt A} → {stack : List (bt A)} → stackInvariant key tree tree0 (tree1 ∷ stack) 160 si-property1 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 tree1 : bt A} → {stack : List (bt A)} → stackInvariant key tree tree0 (tree1 ∷ stack)
161 → tree1 ≡ tree 161 → tree1 ≡ tree
162 si-property1 (s-single _ ) = refl 162 si-property1 (s-single ) = refl
163 si-property1 (s-right _ si) = refl 163 si-property1 (s-right _ si) = refl
164 si-property1 (s-left _ si) = refl 164 si-property1 (s-left _ si) = refl
165 165
166 si-property-last : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → stackInvariant key tree tree0 stack 166 si-property-last : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → stackInvariant key tree tree0 stack
167 → stack-last stack ≡ just tree0 167 → stack-last stack ≡ just tree0
168 si-property-last key t t0 (t ∷ []) (s-single _) = refl 168 si-property-last key t t0 (t ∷ []) (s-single ) = refl
169 si-property-last key t t0 (.t ∷ x ∷ st) (s-right _ si ) with si-property1 si 169 si-property-last key t t0 (.t ∷ x ∷ st) (s-right _ 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 si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ si ) with si-property1 si 171 si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ si ) with si-property1 si
172 ... | refl = si-property-last key x t0 (x ∷ st) si 172 ... | refl = si-property-last key x t0 (x ∷ st) si
173 173
183 ti-left {_} {_} {_} {_} {key₁} {v1} (t-left x ti) = ti 183 ti-left {_} {_} {_} {_} {key₁} {v1} (t-left x ti) = ti
184 ti-left {_} {_} {.(node _ _ _ _)} {_} {key₁} {v1} (t-node x x₁ ti ti₁) = ti 184 ti-left {_} {_} {.(node _ _ _ _)} {_} {key₁} {v1} (t-node x x₁ ti ti₁) = ti
185 185
186 stackTreeInvariant : {n : Level} {A : Set n} (key : ℕ) (sub tree : bt A) → (stack : List (bt A)) 186 stackTreeInvariant : {n : Level} {A : Set n} (key : ℕ) (sub tree : bt A) → (stack : List (bt A))
187 → treeInvariant tree → stackInvariant key sub tree stack → treeInvariant sub 187 → treeInvariant tree → stackInvariant key sub tree stack → treeInvariant sub
188 stackTreeInvariant {_} {A} key sub tree (sub ∷ []) ti (s-single _) = ti 188 stackTreeInvariant {_} {A} key sub tree (sub ∷ []) ti (s-single ) = ti
189 stackTreeInvariant {_} {A} key sub tree (sub ∷ st) ti (s-right _ si ) = ti-right (si1 si) where 189 stackTreeInvariant {_} {A} key sub tree (sub ∷ st) ti (s-right _ si ) = 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 ) 190 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 191 si1 {tree₁ } {key₁ } {v1 } si = stackTreeInvariant key (node key₁ v1 tree₁ sub ) tree st ti si
192 stackTreeInvariant {_} {A} key sub tree (sub ∷ st) ti (s-left _ si ) = ti-left ( si2 si) where 192 stackTreeInvariant {_} {A} key sub tree (sub ∷ st) ti (s-left _ si ) = 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₁ ) 193 si2 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant key (node key₁ v1 sub tree₁ ) tree st → treeInvariant (node key₁ v1 sub tree₁ )
278 → (key : ℕ) → (value : A) → {tree : bt A} ( repl : bt A) 278 → (key : ℕ) → (value : A) → {tree : bt A} ( repl : bt A)
279 → (stack : List (bt A)) → replacePR key value tree repl stack (λ _ _ _ → Lift n ⊤) 279 → (stack : List (bt A)) → replacePR key value tree repl stack (λ _ _ _ → Lift n ⊤)
280 → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A)) 280 → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A))
281 → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t) 281 → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t)
282 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t 282 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
283 replaceP key value {tree} repl [] Pre next exit = ⊥-elim ( si-property0 {!!} refl ) -- can't happen 283 replaceP key value {tree} repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen
284 replaceP key value {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ {!!} -- tree0 ≡ leaf 284 replaceP key value {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ (replacePR.si Pre)-- tree0 ≡ leaf
285 ... | eq = exit {!!} (node key value leaf leaf) ⟪ {!!} , r-leaf ⟫ 285 ... | eq = exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ replacePR.ti Pre , {!!} ⟫
286 replaceP key value {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁ 286 replaceP key value {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁
287 ... | tri< a ¬b ¬c = exit {!!} (node key₁ value₁ repl right ) {!!} where 287 ... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) (node key₁ value₁ repl right ) ⟪ replacePR.ti Pre , {!!} ⟫ where
288 repl01 : node key₁ value₁ tree right ≡ {!!} 288 repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ repl right)
289 repl01 with si-property-last _ _ _ _ {!!} 289 repl01 = ?
290 ... | eq = {!!}
291 ... | tri≈ ¬a b ¬c = exit {!!} (node key₁ value left right ) ⟪ {!!} , {!!} ⟫ -- can't happen 290 ... | tri≈ ¬a b ¬c = exit {!!} (node key₁ value left right ) ⟪ {!!} , {!!} ⟫ -- can't happen
292 ... | tri> ¬a ¬b c = exit {!!} (node key₁ value₁ left repl ) ⟪ {!!} , {!!} ⟫ 291 ... | tri> ¬a ¬b c = exit {!!} (node key₁ value₁ left repl ) ⟪ {!!} , {!!} ⟫
293 replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen 292 replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen
294 replaceP key value {tree} repl (node key₁ value₁ left right ∷ st@(_ ∷ _)) Pre next exit with <-cmp key key₁ 293 replaceP {n} {_} {A} key value {tree} repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁ | si-property1 (replacePR.si Pre)
295 ... | tri< a ¬b ¬c = next key value {{!!}} (node key₁ value₁ tree right ) st {!!} ≤-refl 294 ... | tri< a ¬b ¬c | refl = next key value {{!!}} (node key₁ value₁ repl right ) st Post ≤-refl where
296 ... | tri≈ ¬a b ¬c = next key value {{!!}} (node key₁ value left right ) st {!!} ≤-refl 295 Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤)
297 ... | tri> ¬a ¬b c = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl 296 Post with replacePR.si Pre
297 ... | s-right x t = {!!}
298 ... | s-left lt si with si-property1 si
299 ... | refl = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = si ; ri = {!!} ; ci = lift tt } where
300 repl02 : replacedTree key value (replFromStack si) (node key₁ value₁ repl right)
301 repl02 = {!!}
302 ... | tri≈ ¬a b ¬c | refl = next key value {{!!}} (node key₁ value left right ) st {!!} ≤-refl -- can't happen
303 ... | tri> ¬a ¬b c | refl = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl
298 304
299 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) 305 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
300 → (r : Index) → (p : Invraiant r) 306 → (r : Index) → (p : Invraiant r)
301 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t 307 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t
302 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r) 308 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r)