Mercurial > hg > Members > Moririn
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 { |