Mercurial > hg > Members > Moririn
diff redBlackTreeTest.agda @ 550:2476f7123dc3
root = Nothing case passed on putTest1
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 17 Jan 2018 17:31:41 +0900 |
| parents | bc3208d510cd |
| children | 8bc39f95c961 |
line wrap: on
line diff
--- a/redBlackTreeTest.agda Tue Jan 16 17:14:29 2018 +0900 +++ b/redBlackTreeTest.agda Wed Jan 17 17:31:41 2018 +0900 @@ -153,9 +153,14 @@ putTest1Lemma3 : (k : ℕ) -> compareℕ k k ≡ EQ putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k ) -compareLemma1 : (x y : ℕ) -> compareℕ x y ≡ EQ -> x ≡ y -compareLemma1 x y eq with compareℕ x y | eq -... | EQ | refl = ? +compareLemma1 : (x y : ℕ) -> compare2 x y ≡ EQ -> x ≡ y +compareLemma1 zero zero refl = refl +compareLemma1 zero (suc _) () +compareLemma1 (suc _) zero () +compareLemma1 (suc x) (suc y) eq = cong ( \z -> ℕ.suc z ) ( compareLemma1 x y ( trans lemma2 eq ) ) + where + lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y + lemma2 = refl putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ)) @@ -170,7 +175,6 @@ key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y } ) k ( \ t x1 -> check2 x1 x ≡ True) - lemma1 = {!!} - - - + lemma1 with compare2 k k | putTest1Lemma2 k + ... | EQ | refl with compare2 x x | putTest1Lemma2 x + ... | EQ | refl = refl