Mercurial > hg > Gears > GearsAgda
changeset 556:69fc15bb4e82
add some lemma
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 27 Mar 2018 09:30:49 +0900 |
| parents | e8c9a492b578 |
| children | 90999865d7f3 |
| files | redBlackTreeTest.agda |
| diffstat | 1 files changed, 19 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/redBlackTreeTest.agda Mon Mar 26 23:44:02 2018 +0900 +++ b/redBlackTreeTest.agda Tue Mar 27 09:30:49 2018 +0900 @@ -132,22 +132,35 @@ compareTri1 zero = ≤′-refl compareTri1 (suc n) = ≤′-step ( compareTri1 n ) -compareTri2 : (n m : ℕ) -> (suc n) ≤′ m -> suc (suc n) ≤′ suc m +compareTri2 : (n m : ℕ) -> n ≤′ m -> suc n ≤′ suc m compareTri2 _ _ ≤′-refl = ≤′-refl -compareTri2 n (suc m) ( ≤′-step p ) = ≤′-step { suc (suc n) } ( compareTri2 n m p ) +compareTri2 n (suc m) ( ≤′-step p ) = ≤′-step { suc n } ( compareTri2 n m p ) + +compareTri3 : ∀ m {n} → ¬ m ≡ suc (m + n) +compareTri3 zero () +compareTri3 (suc m) eq = compareTri3 m (cong pred eq) + +compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m +compareTri4 zero neq = {!!} +compareTri4 (suc m) neq = {!!} + +compareTri5 : ∀ m {n} → ¬ m ≤′ n → ¬ suc m ≤′ suc n +compareTri5 zero neq = {!!} +compareTri5 (suc m) neq = {!!} + compareTri : Trichotomous _≡_ _<′_ compareTri zero zero = tri≈ ( λ ()) refl ( λ ()) compareTri zero (suc n) = tri< ( compareTri1 n ) ( λ ()) ( λ ()) compareTri (suc n) zero = tri> ( λ ()) ( λ ()) ( compareTri1 n ) compareTri (suc n) (suc m) with compareTri n m -... | tri≈ p refl r = tri≈ {!!} refl {!!} -... | tri< p q r = tri< (compareTri2 n m p ) {!!} {!!} -... | tri> p q r = tri> {!!} {!!} (compareTri2 m n r ) +... | tri< p q r = tri< (compareTri2 (suc n) m p ) (compareTri4 _ q) ( compareTri5 _ r ) +... | tri≈ p refl r = tri≈ (compareTri5 _ p) refl ( compareTri5 _ r ) +... | tri> p q r = tri> ( compareTri5 _ p ) (compareTri4 _ q) (compareTri2 (suc m) n r ) compareDecTest : (n n1 : Node ℕ ℕ) -> ( key n ≡ key n1 ) ∨ ( ¬ key n ≡ key n1 ) compareDecTest n n1 with (key n) ≟ (key n1) -... | yes p = pi1 p +... | yes p = pi1 p ... | no ¬p = pi2 ¬p