Mercurial > hg > Gears > GearsAgda

comparison redBlackTreeTest.agda @ 559:cca54e32d7ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author ryokka
date Thu, 29 Mar 2018 19:38:49 +0900
parents 8595a7ffba8b
children f4779958ff6a
comparison
equal deleted inserted replaced
558:8595a7ffba8b 559:cca54e32d7ac
134 134
135 compareTri2 : (n m : ℕ) -> n ≤′ m -> suc n ≤′ suc m 135 compareTri2 : (n m : ℕ) -> n ≤′ m -> suc n ≤′ suc m
136 compareTri2 _ _ ≤′-refl = ≤′-refl 136 compareTri2 _ _ ≤′-refl = ≤′-refl
137 compareTri2 n (suc m) ( ≤′-step p ) = ≤′-step { suc n } ( compareTri2 n m p ) 137 compareTri2 n (suc m) ( ≤′-step p ) = ≤′-step { suc n } ( compareTri2 n m p )
138 138
139 compareTri3 : ∀ m {n} → ¬ m ≡ suc (m + n)
140 compareTri3 zero ()
141 compareTri3 (suc m) eq = compareTri3 m (cong pred eq)
142
143 compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
144 compareTri4 m {n} with n ≟ m
145 ... | yes refl = λ x y → x refl
146 ... | no p = λ x y → p ( cong pred y )
147
148 <′dec : Set 139 <′dec : Set
149 <′dec = ∀ m n → Dec ( m ≤′ n ) 140 <′dec = ∀ m n → Dec ( m ≤′ n )
150 141
151 is≤′ : <′dec 142 is≤′ : <′dec
152 is≤′ zero zero = yes ≤′-refl 143 is≤′ zero zero = yes ≤′-refl
154 is≤′ (suc m) (zero) = no ( \ () ) 145 is≤′ (suc m) (zero) = no ( \ () )
155 is≤′ (suc m) (suc n) with is≤′ m n 146 is≤′ (suc m) (suc n) with is≤′ m n
156 ... | yes p = yes {!!} 147 ... | yes p = yes {!!}
157 ... | no p = no {!!} 148 ... | no p = no {!!}
158 149
150 compareTri20 : {n : ℕ} -> ¬ suc n ≤′ zero
151 compareTri20 {zero} = {!!}
152 compareTri20 {suc n} = {!!}
153
154 compareTri21 : (n m : ℕ) -> suc n ≤′ suc m -> n ≤′ m
155 compareTri21 _ _ ≤′-refl = ≤′-refl
156 compareTri21 n (suc m) ( ≤′-step p ) = ≤′-step (compareTri21 _ _ p)
157 compareTri21 zero zero _ = ≤′-refl
158 compareTri21 (suc zero) zero _ = {!!}
159 compareTri21 (suc (suc n)) zero _ = {!!}
160
161
162 compareTri3 : ∀ m {n} → ¬ m ≡ suc (m + n)
163 compareTri3 zero ()
164 compareTri3 (suc m) eq = compareTri3 m (cong pred eq)
165
166 compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
167 compareTri4 m {n} with n ≟ m
168 ... | yes refl = λ x y → x refl
169 ... | no p = λ x y → p ( cong pred y )
170
159 compareTri5 : ∀ m {n} → ¬ m <′ n → ¬ suc m <′ suc n 171 compareTri5 : ∀ m {n} → ¬ m <′ n → ¬ suc m <′ suc n
160 compareTri5 m {n} with (is≤′ m n) 172 compareTri5 m {n} with (is≤′ m n)
161 ... | yes p = {!!} 173 ... | yes p = {!!}
162 ... | no p = {!!} 174 ... | no p = {!!}
175
176 compareTri6 : ∀ m {n} → ¬ m ≤′ n → ¬ suc m ≤′ suc n
177 compareTri6 m {n} = λ x y → x (compareTri21 _ _ y)
163 178
164 compareTri : Trichotomous _≡_ _<′_ 179 compareTri : Trichotomous _≡_ _<′_
165 compareTri zero zero = tri≈ ( λ ()) refl ( λ ()) 180 compareTri zero zero = tri≈ ( λ ()) refl ( λ ())
166 compareTri zero (suc n) = tri< ( compareTri1 n ) ( λ ()) ( λ ()) 181 compareTri zero (suc n) = tri< ( compareTri1 n ) ( λ ()) ( λ ())
167 compareTri (suc n) zero = tri> ( λ ()) ( λ ()) ( compareTri1 n ) 182 compareTri (suc n) zero = tri> ( λ ()) ( λ ()) ( compareTri1 n )