comparison redBlackTreeTest.agda @ 552:5f4c5a663219

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 18 Jan 2018 10:38:55 +0900 (2018-01-18)
parents 8bc39f95c961
children 7d9af1d4b5af
comparison
equal deleted inserted replaced
551:8bc39f95c961 552:5f4c5a663219
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 = lemma2 171 ... | Just n1 = lemma2 ( record { top = Nothing } )
172 where 172 where
173 lemma2 : putTree1 (record { root = Just n1 ; nodeStack = record { top = Nothing } ; compare = compare2 }) k x (λ t → 173 lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) -> putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
174 GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t)) 174 GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t))
175 lemma2 with compare2 k (key n1) 175 lemma2 s with compare2 k (key n1)
176 ... | EQ = {!!} 176 ... | EQ = lemma3 ?
177 where 177 where
178 lemma3 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { 178 lemma3 : compare2 k (key n1) ≡ EQ -> getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {
179 key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black 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) 180 } ) ; nodeStack = s ; compare = λ x₁ y → compare2 x₁ y } ) k ( \ t x1 -> check2 x1 x ≡ True)
181 lemma3 with compare2 x x | putTest1Lemma2 x 181 lemma3 eq with compare2 x x | putTest1Lemma2 x
182 ... | EQ | refl = {!!} 182 ... | EQ | refl with compare2 k (key n1) | eq
183 ... | EQ | refl with compare2 x x | putTest1Lemma2 x
184 ... | EQ | refl = refl
183 ... | GT = {!!} 185 ... | GT = {!!}
184 ... | LT = {!!} 186 ... | LT = {!!}
185 ... | Nothing = lemma1 187 ... | Nothing = lemma1
186 where 188 where
187 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { 189 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {