Mercurial > hg > Gears > GearsAgda

comparison redBlackTreeTest.agda @ 550:2476f7123dc3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
root = Nothing case passed on putTest1
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 17 Jan 2018 17:31:41 +0900
parents bc3208d510cd
children 8bc39f95c961
comparison
equal deleted inserted replaced
549:bc3208d510cd 550:2476f7123dc3
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 : ℕ) -> compareℕ x y ≡ EQ -> x ≡ y 156 compareLemma1 : (x y : ℕ) -> compare2 x y ≡ EQ -> x ≡ y
157 compareLemma1 x y eq with compareℕ x y | eq 157 compareLemma1 zero zero refl = refl
158 ... | EQ | refl = ? 158 compareLemma1 zero (suc _) ()
159 compareLemma1 (suc _) zero ()
160 compareLemma1 (suc x) (suc y) eq = cong ( \z -> ℕ.suc z ) ( compareLemma1 x y ( trans lemma2 eq ) )
161 where
162 lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
163 lemma2 = refl
159 164
160 165
161 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ)) 166 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
162 -> (k : ℕ) (x : ℕ) 167 -> (k : ℕ) (x : ℕ)
163 -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x 168 -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
168 where 173 where
169 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { 174 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {
170 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red 175 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red
171 } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y } ) k 176 } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y } ) k
172 ( \ t x1 -> check2 x1 x ≡ True) 177 ( \ t x1 -> check2 x1 x ≡ True)
173 lemma1 = {!!} 178 lemma1 with compare2 k k | putTest1Lemma2 k
174 179 ... | EQ | refl with compare2 x x | putTest1Lemma2 x
175 180 ... | EQ | refl = refl
176