Mercurial > hg > Gears > GearsAgda
changeset 560:f4779958ff6a
compareTri5 done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 29 Mar 2018 20:23:51 +0900 |
| parents | cca54e32d7ac |
| children | 1bbbd787472e |
| files | redBlackTreeTest.agda |
| diffstat | 1 files changed, 6 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/redBlackTreeTest.agda Thu Mar 29 19:38:49 2018 +0900 +++ b/redBlackTreeTest.agda Thu Mar 29 20:23:51 2018 +0900 @@ -154,10 +154,9 @@ compareTri21 : (n m : ℕ) -> suc n ≤′ suc m -> n ≤′ m compareTri21 _ _ ≤′-refl = ≤′-refl compareTri21 n (suc m) ( ≤′-step p ) = ≤′-step (compareTri21 _ _ p) -compareTri21 zero zero _ = ≤′-refl -compareTri21 (suc zero) zero _ = {!!} -compareTri21 (suc (suc n)) zero _ = {!!} - +compareTri21 zero zero ( ≤′-step p ) = ≤′-refl +compareTri21 (suc n1) zero = {!!} + compareTri3 : ∀ m {n} → ¬ m ≡ suc (m + n) compareTri3 zero () @@ -168,14 +167,12 @@ ... | yes refl = λ x y → x refl ... | no p = λ x y → p ( cong pred y ) -compareTri5 : ∀ m {n} → ¬ m <′ n → ¬ suc m <′ suc n -compareTri5 m {n} with (is≤′ m n) -... | yes p = {!!} -... | no p = {!!} - compareTri6 : ∀ m {n} → ¬ m ≤′ n → ¬ suc m ≤′ suc n compareTri6 m {n} = λ x y → x (compareTri21 _ _ y) +compareTri5 : ∀ m {n} → ¬ m <′ n → ¬ suc m <′ suc n +compareTri5 m {n} = compareTri6 (suc m) + compareTri : Trichotomous _≡_ _<′_ compareTri zero zero = tri≈ ( λ ()) refl ( λ ()) compareTri zero (suc n) = tri< ( compareTri1 n ) ( λ ()) ( λ ())