Mercurial > hg > Gears > GearsAgda
changeset 548:c304869ac439
compareN x x = EQ
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 14 Jan 2018 17:57:38 +0900 |
| parents | d6a2b812b056 |
| children | bc3208d510cd |
| files | redBlackTreeTest.agda |
| diffstat | 1 files changed, 26 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/redBlackTreeTest.agda Sun Jan 14 08:38:46 2018 +0900 +++ b/redBlackTreeTest.agda Sun Jan 14 17:57:38 2018 +0900 @@ -119,15 +119,33 @@ compare2 zero (suc _) = LT compare2 (suc x) (suc y) = compare2 x y -putTest1Lemma1 : (k : ℕ) -> compare2 k k ≡ EQ -putTest1Lemma1 zero = refl -putTest1Lemma1 (suc k) = putTest1Lemma1 k +putTest1Lemma2 : (k : ℕ) -> compare2 k k ≡ EQ +putTest1Lemma2 zero = refl +putTest1Lemma2 (suc k) = putTest1Lemma2 k --- begin --- Data.Nat.compare k (key (leafNode k x)) --- ≡⟨ {!!} ⟩ --- Data.Nat.equal _ --- ∎ +putTest1Lemma1 : (x y : ℕ) -> compareℕ x y ≡ compare2 x y +putTest1Lemma1 zero zero = refl +putTest1Lemma1 (suc m) zero = refl +putTest1Lemma1 zero (suc n) = refl +putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n +putTest1Lemma1 (suc .m) (suc .(Data.Nat.suc m + k)) | less m k = lemma1 m + where + lemma1 : (m : ℕ) -> LT ≡ compare2 m (ℕ.suc (m + k)) + lemma1 zero = refl + lemma1 (suc y) = lemma1 y +putTest1Lemma1 (suc .m) (suc .m) | equal m = lemma1 m + where + lemma1 : (m : ℕ) -> EQ ≡ compare2 m m + lemma1 zero = refl + lemma1 (suc y) = lemma1 y +putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m) | greater m k = lemma1 m + where + lemma1 : (m : ℕ) -> GT ≡ compare2 (ℕ.suc (m + k)) m + lemma1 zero = refl + lemma1 (suc y) = lemma1 y + +putTest1Lemma3 : (k : ℕ) -> compareℕ k k ≡ EQ +putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k ) putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))