Mercurial > hg > Members > Moririn

comparison redBlackTreeTest.agda @ 554:988c12d7f887

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use another nat comparator
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 26 Mar 2018 23:22:07 +0900
parents 7d9af1d4b5af
children e8c9a492b578
comparison
equal deleted inserted replaced
553:7d9af1d4b5af 554:988c12d7f887
1 module redBlackTreeTest where 1 module redBlackTreeTest where
2 2
3 open import RedBlackTree 3 open import RedBlackTree
4 open import stack 4 open import stack
5 open import Level hiding (zero) 5 open import Level hiding (zero) renaming ( suc to succ )
6 6
7 open import Data.Empty 7 open import Data.Empty
8 8
9 open import Data.Nat 9 open import Data.Nat
10 open import Relation.Nullary 10 open import Relation.Nullary
126 -- compare2 zero zero = EQ 126 -- compare2 zero zero = EQ
127 -- compare2 (suc _) zero = GT 127 -- compare2 (suc _) zero = GT
128 -- compare2 zero (suc _) = LT 128 -- compare2 zero (suc _) = LT
129 -- compare2 (suc x) (suc y) = compare2 x y 129 -- compare2 (suc x) (suc y) = compare2 x y
130 130
131 compareTri1 : (n : ℕ) -> zero < ℕ.suc n 131 compareTri1 : (n : ℕ) -> zero <′ suc n
132 compareTri1 zero = {!!} 132 compareTri1 zero = ≤′-refl
133 compareTri1 (suc n) = {!!} 133 compareTri1 (suc n) = ≤′-step ( compareTri1 n )
134 134
135 compareTri : Trichotomous _≡_ _<_ 135 compareTri2 : (n m : ℕ) -> (suc n) ≤′ m -> suc (suc n) ≤′ suc m
136 compareTri zero zero = tri≈ (\()) refl (\()) 136 compareTri2 _ _ ≤′-refl = ≤′-refl
137 compareTri zero (suc n) = tri< {!!} (\()) (\()) 137 compareTri2 n (suc m) ( ≤′-step p ) = ≤′-step { suc (suc n) } ( compareTri2 n m p )
138 compareTri (suc n) zero = tri> (\()) (\()) {!!} 138
139 compareTri : Trichotomous _≡_ _<′_
140 compareTri zero zero = tri≈ ( λ ()) refl ( λ ())
141 compareTri zero (suc n) = tri< ( compareTri1 n ) ( λ ()) ( λ ())
142 compareTri (suc n) zero = tri> ( λ ()) ( λ ()) ( compareTri1 n )
139 compareTri (suc n) (suc m) with compareTri n m 143 compareTri (suc n) (suc m) with compareTri n m
140 ... | tri≈ p q r = tri≈ {!!} (cong (\x -> ℕ.suc x) q) {!!} 144 ... | tri≈ p q r = tri≈ {!!} (cong ( λ x -> suc x) q) {!!}
141 ... | tri< p q r = tri< {!!} {!!} {!!} 145 ... | tri< p q r = tri< (compareTri2 n m p ) {!!} {!!}
142 ... | tri> p q r = tri> {!!} {!!} {!!} 146 ... | tri> p q r = tri> {!!} {!!} (compareTri2 m n r )
143 147
144 compareDecTest : (n n1 : Node ℕ ℕ) -> key n ≡ key n1 148 compareDecTest : (n n1 : Node ℕ ℕ) -> ( key n ≡ key n1 ) ∨ ( ¬ key n ≡ key n1 )
145 compareDecTest n n1 with (key n) ≟ (key n1) 149 compareDecTest n n1 with (key n) ≟ (key n1)
146 ... | yes p = p 150 ... | yes p = pi1 p
147 ... | no ¬p = {!!} 151 ... | no ¬p = pi2 ¬p
148
149 152
150 153
151 putTest1Lemma2 : (k : ℕ) -> compare2 k k ≡ EQ 154 putTest1Lemma2 : (k : ℕ) -> compare2 k k ≡ EQ
152 putTest1Lemma2 zero = refl 155 putTest1Lemma2 zero = refl
153 putTest1Lemma2 (suc k) = putTest1Lemma2 k 156 putTest1Lemma2 (suc k) = putTest1Lemma2 k