Mercurial > hg > Members > Moririn

comparison redBlackTreeTest.agda @ 569:f24a73245f36

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate trichotomos exercise
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 17 Apr 2018 10:14:16 +0900
parents a5ba292e4081
children a6aa2ff5fea4
comparison
equal deleted inserted replaced
568:a5ba292e4081 569:f24a73245f36
124 124
125 125
126 redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} → RedBlackTree {Level.zero} {m} {t} a ℕ 126 redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} → RedBlackTree {Level.zero} {m} {t} a ℕ
127 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compareT } 127 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compareT }
128 128
129 -- compare2 : (x y : ℕ ) → CompareResult {Level.zero}
130 -- compare2 zero zero = EQ
131 -- compare2 (suc _) zero = GT
132 -- compare2 zero (suc _) = LT
133 -- compare2 (suc x) (suc y) = compare2 x y
134
135 contraposition : {m : Level } {A B : Set m} → (B → A) → (¬ A → ¬ B)
136 contraposition f = λ x y → x (f y)
137
138 compareTri1 : (n : ℕ) → zero <′ suc n
139 compareTri1 zero = ≤′-refl
140 compareTri1 (suc n) = ≤′-step ( compareTri1 n )
141
142 compareTri2 : (n m : ℕ) → n ≤′ m → suc n ≤′ suc m
143 compareTri2 _ _ ≤′-refl = ≤′-refl
144 compareTri2 n (suc m) ( ≤′-step p ) = ≤′-step { suc n } ( compareTri2 n m p )
145
146 <′dec : Set
147 <′dec = ∀ m n → Dec ( m ≤′ n )
148
149 compareTri6 : ∀ m {n} → ¬ m ≤′ n → ¬ suc m ≤′ suc n
150
151 is≤′ : <′dec
152 is≤′ zero zero = yes ≤′-refl
153 is≤′ zero (suc n) = yes (lemma n)
154 where
155 lemma : (n : ℕ) → zero ≤′ suc n
156 lemma zero = ≤′-step ≤′-refl
157 lemma (suc n) = ≤′-step (lemma n)
158 is≤′ (suc m) (zero) = no ( λ () )
159 is≤′ (suc m) (suc n) with is≤′ m n
160 ... | yes p = yes ( compareTri2 _ _ p )
161 ... | no p = no ( compareTri6 _ p )
162
163 compareTri20 : {n : ℕ} → ¬ suc n ≤′ zero
164 compareTri20 ()
165
166
167 compareTri21 : (n m : ℕ) → suc n ≤′ suc m → n ≤′ m
168 compareTri21 _ _ ≤′-refl = ≤′-refl
169 compareTri21 (suc n) zero ( ≤′-step p ) = compareTri23 (suc n) ( ≤′-step p ) p
170 where
171 compareTri23 : (n : ℕ) → suc n ≤′ suc zero → suc n ≤′ zero → n ≤′ zero
172 compareTri23 zero ( ≤′-step p ) _ = ≤′-refl
173 compareTri23 zero ≤′-refl _ = ≤′-refl
174 compareTri23 (suc n1) ( ≤′-step p ) ()
175 compareTri21 n (suc m) ( ≤′-step p ) = ≤′-step (compareTri21 _ _ p)
176 compareTri21 zero zero ( ≤′-step p ) = ≤′-refl
177
178
179 compareTri3 : ∀ m {n} → ¬ m ≡ suc (m + n)
180 compareTri3 zero ()
181 compareTri3 (suc m) eq = compareTri3 m (cong pred eq)
182
183 compareTri4' : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
184 compareTri4' m {n} with n ≟ m
185 ... | yes refl = λ x y → x refl
186 ... | no p = λ x y → p ( cong pred y )
187
188 compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
189 compareTri4 m = contraposition ( λ x → cong pred x )
190
191 -- compareTri6 : ∀ m {n} → ¬ m ≤′ n → ¬ suc m ≤′ suc n
192 compareTri6 m {n} = λ x y → x (compareTri21 _ _ y)
193
194 compareTri5 : ∀ m {n} → ¬ m <′ n → ¬ suc m <′ suc n
195 compareTri5 m {n} = compareTri6 (suc m)
196
197 compareTri : Trichotomous _≡_ _<′_
198 compareTri zero zero = tri≈ ( λ ()) refl ( λ ())
199 compareTri zero (suc n) = tri< ( compareTri1 n ) ( λ ()) ( λ ())
200 compareTri (suc n) zero = tri> ( λ ()) ( λ ()) ( compareTri1 n )
201 compareTri (suc n) (suc m) with compareTri n m
202 ... | tri< p q r = tri< (compareTri2 (suc n) m p ) (compareTri4 _ q) ( compareTri5 _ r )
203 ... | tri≈ p refl r = tri≈ (compareTri5 _ p) refl ( compareTri5 _ r )
204 ... | tri> p q r = tri> ( compareTri5 _ p ) (compareTri4 _ q) (compareTri2 (suc m) n r )
205
206 compareDecTest : (n n1 : Node ℕ ℕ) → ( key n ≡ key n1 ) ∨ ( ¬ key n ≡ key n1 )
207 compareDecTest n n1 with (key n) ≟ (key n1)
208 ... | yes p = pi1 p
209 ... | no ¬p = pi2 ¬p
210
211
212 putTest1Lemma2 : (k : ℕ) → compare2 k k ≡ EQ
213 putTest1Lemma2 zero = refl
214 putTest1Lemma2 (suc k) = putTest1Lemma2 k
215
216 putTest1Lemma1 : (x y : ℕ) → compareℕ x y ≡ compare2 x y
217 putTest1Lemma1 zero zero = refl
218 putTest1Lemma1 (suc m) zero = refl
219 putTest1Lemma1 zero (suc n) = refl
220 putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n
221 putTest1Lemma1 (suc .m) (suc .(Data.Nat.suc m + k)) | less m k = lemma1 m
222 where
223 lemma1 : (m : ℕ) → LT ≡ compare2 m (ℕ.suc (m + k))
224 lemma1 zero = refl
225 lemma1 (suc y) = lemma1 y
226 putTest1Lemma1 (suc .m) (suc .m) | equal m = lemma1 m
227 where
228 lemma1 : (m : ℕ) → EQ ≡ compare2 m m
229 lemma1 zero = refl
230 lemma1 (suc y) = lemma1 y
231 putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m) | greater m k = lemma1 m
232 where
233 lemma1 : (m : ℕ) → GT ≡ compare2 (ℕ.suc (m + k)) m
234 lemma1 zero = refl
235 lemma1 (suc y) = lemma1 y
236
237 putTest1Lemma3 : (k : ℕ) → compareℕ k k ≡ EQ
238 putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k )
239
240 compareLemma1 : {x y : ℕ} → compare2 x y ≡ EQ → x ≡ y
241 compareLemma1 {zero} {zero} refl = refl
242 compareLemma1 {zero} {suc _} ()
243 compareLemma1 {suc _} {zero} ()
244 compareLemma1 {suc x} {suc y} eq = cong ( λ z → ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
245 where
246 lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
247 lemma2 = refl
248
249 129
250 compTri : ( x y : ℕ ) -> Tri (x < y) ( x ≡ y ) ( x > y ) 130 compTri : ( x y : ℕ ) -> Tri (x < y) ( x ≡ y ) ( x > y )
251 compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder) 131 compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder)
252 where open import Relation.Binary 132 where open import Relation.Binary
253 133