Mercurial > hg > Gears > GearsAgda

comparison redBlackTreeTest.agda @ 551:8bc39f95c961

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix findNode
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 17 Jan 2018 18:28:25 +0900
parents 2476f7123dc3
children 5f4c5a663219
comparison
equal deleted inserted replaced
550:2476f7123dc3 551:8bc39f95c961
151 lemma1 (suc y) = lemma1 y 151 lemma1 (suc y) = lemma1 y
152 152
153 putTest1Lemma3 : (k : ℕ) -> compareℕ k k ≡ EQ 153 putTest1Lemma3 : (k : ℕ) -> compareℕ k k ≡ EQ
154 putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k ) 154 putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k )
155 155
156 compareLemma1 : (x y : ℕ) -> compare2 x y ≡ EQ -> x ≡ y 156 compareLemma1 : {x y : ℕ} -> compare2 x y ≡ EQ -> x ≡ y
157 compareLemma1 zero zero refl = refl 157 compareLemma1 {zero} {zero} refl = refl
158 compareLemma1 zero (suc _) () 158 compareLemma1 {zero} {suc _} ()
159 compareLemma1 (suc _) zero () 159 compareLemma1 {suc _} {zero} ()
160 compareLemma1 (suc x) (suc y) eq = cong ( \z -> ℕ.suc z ) ( compareLemma1 x y ( trans lemma2 eq ) ) 160 compareLemma1 {suc x} {suc y} eq = cong ( \z -> ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
161 where 161 where
162 lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y 162 lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
163 lemma2 = refl 163 lemma2 = refl
164 164
165 165
166 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ)) 166 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
167 -> (k : ℕ) (x : ℕ) 167 -> (k : ℕ) (x : ℕ)
168 -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x 168 -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
169 (\ t -> getRedBlackTree t k (\ t x1 -> check2 x1 x ≡ True)) 169 (\ t -> getRedBlackTree t k (\ t x1 -> check2 x1 x ≡ True))
170 putTest1 n k x with n 170 putTest1 n k x with n
171 ... | Just n1 = {!!} 171 ... | Just n1 = lemma2
172 where
173 lemma2 : putTree1 (record { root = Just n1 ; nodeStack = record { top = Nothing } ; compare = compare2 }) k x (λ t →
174 GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t))
175 lemma2 with compare2 k (key n1)
176 ... | EQ = {!!}
177 where
178 lemma3 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {
179 key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black
180 } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y } ) k ( \ t x1 -> check2 x1 x ≡ True)
181 lemma3 with compare2 x x | putTest1Lemma2 x
182 ... | EQ | refl = {!!}
183 ... | GT = {!!}
184 ... | LT = {!!}
172 ... | Nothing = lemma1 185 ... | Nothing = lemma1
173 where 186 where
174 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { 187 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {
175 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red 188 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red
176 } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y } ) k 189 } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y } ) k