Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 630:24bec7639079

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, 09 Nov 2021 09:44:23 +0900
parents 7a19d4b43795
children 956ee8ae42b9
comparison
equal deleted inserted replaced
629:7a19d4b43795 630:24bec7639079
99 treeInvariantTest1 = {!!} 99 treeInvariantTest1 = {!!}
100 100
101 data stackInvariant {n : Level} {A : Set n} (key0 : ℕ) : (tree tree0 : bt A) → (stack : List (bt A)) → Set n where 101 data stackInvariant {n : Level} {A : Set n} (key0 : ℕ) : (tree tree0 : bt A) → (stack : List (bt A)) → Set n where
102 s-nil : stackInvariant key0 leaf leaf [] 102 s-nil : stackInvariant key0 leaf leaf []
103 s-single : (tree : bt A) → stackInvariant key0 tree tree (tree ∷ [] ) 103 s-single : (tree : bt A) → stackInvariant key0 tree tree (tree ∷ [] )
104 s-< : (tree0 tree : bt A) → {key : ℕ } → {value : A } { left : bt A} → {st : List (bt A)} 104 s-right : (tree0 tree : bt A) → {key : ℕ } → {value : A } { left : bt A} → {st : List (bt A)}
105 → key < key0 → stackInvariant key0(node key value left tree ) tree0 (node key value left tree ∷ st ) → stackInvariant key0 tree tree0 (tree ∷ node key value left tree ∷ st ) 105 → key < key0 → stackInvariant key0(node key value left tree ) tree0 (node key value left tree ∷ st ) → stackInvariant key0 tree tree0 (tree ∷ node key value left tree ∷ st )
106 s-> : (tree0 tree : bt A) → {key : ℕ } → {value : A } { right : bt A} → {st : List (bt A)} 106 s-left : (tree0 tree : bt A) → {key : ℕ } → {value : A } { right : bt A} → {st : List (bt A)}
107 → key0 < key → stackInvariant key0(node key value tree right ) tree0 (node key value tree right ∷ st ) → stackInvariant key0 tree tree0 (tree ∷ node key value tree right ∷ st ) 107 → key0 < key → stackInvariant key0(node key value tree right ) tree0 (node key value tree right ∷ st ) → stackInvariant key0 tree tree0 (tree ∷ node key value tree right ∷ st )
108 108
109 data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree tree1 : bt A ) → Set n where 109 data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree tree1 : bt A ) → Set n where
110 r-leaf : replacedTree key value leaf (node key value leaf leaf) 110 r-leaf : replacedTree key value leaf (node key value leaf leaf)
111 r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁) 111 r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁)
116 116
117 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A)) 117 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
118 → treeInvariant tree ∧ stackInvariant key tree tree0 stack 118 → treeInvariant tree ∧ stackInvariant key tree tree0 stack
119 → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t ) 119 → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t )
120 → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → t ) → t 120 → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → t ) → t
121 findP key leaf tree0 st Pre _ exit = exit leaf tree0 st {!!} 121 findP key leaf tree0 st Pre _ exit = exit leaf tree0 st Pre
122 findP key (node key₁ v tree tree₁) tree0 st Pre next exit with <-cmp key key₁ 122 findP key (node key₁ v tree tree₁) tree0 st Pre next exit with <-cmp key key₁
123 findP key n tree0 st Pre _ exit | tri≈ ¬a b ¬c = exit n tree0 st {!!} 123 findP key n tree0 st Pre _ exit | tri≈ ¬a b ¬c = exit n tree0 st Pre
124 findP key n@(node key₁ v tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (n ∷ st) {!!} {!!} 124 findP key n@(node key₁ v tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (n ∷ st) {!!} {!!}
125 findP key n@(node key₁ v tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (n ∷ st) {!!} {!!} 125 findP key n@(node key₁ v tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (n ∷ st) {!!} {!!}
126 126
127 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) → (treeInvariant tree ) 127 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) → (treeInvariant tree )
128 → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value tree tree1 → t) → t 128 → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value tree tree1 → t) → t
219 219
220 insertTreePP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree 220 insertTreePP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
221 → (exit : (tree repl : bt A) → treeInvariant tree ∧ replacedTree key value tree repl → t ) → t 221 → (exit : (tree repl : bt A) → treeInvariant tree ∧ replacedTree key value tree repl → t ) → t
222 insertTreePP {n} {m} {A} {t} tree key value P exit = 222 insertTreePP {n} {m} {A} {t} tree key value P exit =
223 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR key (proj1 p) (proj2 p) (λ t s → Lift n ⊤) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ {!!} 223 TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR key (proj1 p) (proj2 p) (λ t s → Lift n ⊤) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ {!!}
224 $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) 224 $ λ p P loop → findPP key (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )
225 $ λ t s _ P → replaceNodeP key value t {!!} 225 $ λ t s _ P → replaceNodeP key value t {!!}
226 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A )) 226 $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A ))
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) {!!}
249 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 : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤
250 containsTree {n} {m} {A} {t} tree tree1 key value P RT = 250 containsTree {n} {m} {A} {t} tree tree1 key value P RT =
251 TerminatingLoopS (bt A ∧ List (bt A) ) 251 TerminatingLoopS (bt A ∧ List (bt A) )
252 {λ p → findPR key (proj1 p) (proj2 p) (findPC key value ) } (λ p → bt-depth (proj1 p)) 252 {λ p → findPR key (proj1 p) (proj2 p) (findPC key value ) } (λ p → bt-depth (proj1 p))
253 ⟪ tree1 , [] ⟫ {!!} 253 ⟪ tree1 , [] ⟫ {!!}
254 $ λ p P loop → findPPC key value (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt ) 254 $ λ p P loop → findPPC key value (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )
255 $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value (lemma6 t1 s1 found? P2) where 255 $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value (lemma6 t1 s1 found? P2) where
256 lemma6 : (t1 : bt A) (s1 : List (bt A)) (found? : (t1 ≡ leaf) ∨ (node-key t1 ≡ just key)) (P2 : findPR key t1 s1 (findPC key value)) → top-value t1 ≡ just value 256 lemma6 : (t1 : bt A) (s1 : List (bt A)) (found? : (t1 ≡ leaf) ∨ (node-key t1 ≡ just key)) (P2 : findPR key t1 s1 (findPC key value)) → top-value t1 ≡ just value
257 lemma6 t1 s1 found? P2 = lemma7 t1 s1 (findPR.tree0 P2) ( findPC.tree1 (findPR.ci P2)) ( findPC.ci (findPR.ci P2)) (findPR.si P2) found? where 257 lemma6 t1 s1 found? P2 = lemma7 t1 s1 (findPR.tree0 P2) ( findPC.tree1 (findPR.ci P2)) ( findPC.ci (findPR.ci P2)) (findPR.si P2) found? where
258 lemma7 : (t1 : bt A) ( s1 : List (bt A) ) (tree0 tree1 : bt A) → 258 lemma7 : (t1 : bt A) ( s1 : List (bt A) ) (tree0 tree1 : bt A) →
259 replacedTree key value t1 tree1 → stackInvariant key t1 tree0 s1 → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key) → top-value t1 ≡ just value 259 replacedTree key value t1 tree1 → stackInvariant key t1 tree0 s1 → ( t1 ≡ leaf ) ∨ ( node-key t1 ≡ just key) → top-value t1 ≡ just value