Mercurial > hg > Members > Moririn

comparison redBlackTreeTest.agda @ 553:7d9af1d4b5af

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add compareTri
author ryokka
date Mon, 26 Mar 2018 17:50:04 +0900
parents 5f4c5a663219
children 988c12d7f887
comparison
equal deleted inserted replaced
552:5f4c5a663219 553:7d9af1d4b5af
2 2
3 open import RedBlackTree 3 open import RedBlackTree
4 open import stack 4 open import stack
5 open import Level hiding (zero) 5 open import Level hiding (zero)
6 6
7 open import Data.Empty
8
7 open import Data.Nat 9 open import Data.Nat
10 open import Relation.Nullary
8 11
9 open Tree 12 open Tree
10 open Node 13 open Node
11 open RedBlackTree.RedBlackTree 14 open RedBlackTree.RedBlackTree
12 open Stack 15 open Stack
122 -- compare2 : (x y : ℕ ) -> CompareResult {Level.zero} 125 -- compare2 : (x y : ℕ ) -> CompareResult {Level.zero}
123 -- compare2 zero zero = EQ 126 -- compare2 zero zero = EQ
124 -- compare2 (suc _) zero = GT 127 -- compare2 (suc _) zero = GT
125 -- compare2 zero (suc _) = LT 128 -- compare2 zero (suc _) = LT
126 -- compare2 (suc x) (suc y) = compare2 x y 129 -- compare2 (suc x) (suc y) = compare2 x y
130
131 compareTri1 : (n : ℕ) -> zero < ℕ.suc n
132 compareTri1 zero = {!!}
133 compareTri1 (suc n) = {!!}
134
135 compareTri : Trichotomous _≡_ _<_
136 compareTri zero zero = tri≈ (\()) refl (\())
137 compareTri zero (suc n) = tri< {!!} (\()) (\())
138 compareTri (suc n) zero = tri> (\()) (\()) {!!}
139 compareTri (suc n) (suc m) with compareTri n m
140 ... | tri≈ p q r = tri≈ {!!} (cong (\x -> ℕ.suc x) q) {!!}
141 ... | tri< p q r = tri< {!!} {!!} {!!}
142 ... | tri> p q r = tri> {!!} {!!} {!!}
143
144 compareDecTest : (n n1 : Node ℕ ℕ) -> key n ≡ key n1
145 compareDecTest n n1 with (key n) ≟ (key n1)
146 ... | yes p = p
147 ... | no ¬p = {!!}
148
149
127 150
128 putTest1Lemma2 : (k : ℕ) -> compare2 k k ≡ EQ 151 putTest1Lemma2 : (k : ℕ) -> compare2 k k ≡ EQ
129 putTest1Lemma2 zero = refl 152 putTest1Lemma2 zero = refl
130 putTest1Lemma2 (suc k) = putTest1Lemma2 k 153 putTest1Lemma2 (suc k) = putTest1Lemma2 k
131 154
171 ... | Just n1 = lemma2 ( record { top = Nothing } ) 194 ... | Just n1 = lemma2 ( record { top = Nothing } )
172 where 195 where
173 lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) -> putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t → 196 lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) -> putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
174 GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t)) 197 GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t))
175 lemma2 s with compare2 k (key n1) 198 lemma2 s with compare2 k (key n1)
176 ... | EQ = lemma3 ? 199 ... | EQ = lemma3 {!!}
177 where 200 where
178 lemma3 : compare2 k (key n1) ≡ EQ -> getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { 201 lemma3 : compare2 k (key n1) ≡ EQ -> getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {
179 key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black 202 key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black
180 } ) ; nodeStack = s ; compare = λ x₁ y → compare2 x₁ y } ) k ( \ t x1 -> check2 x1 x ≡ True) 203 } ) ; nodeStack = s ; compare = λ x₁ y → compare2 x₁ y } ) k ( \ t x1 -> check2 x1 x ≡ True)
181 lemma3 eq with compare2 x x | putTest1Lemma2 x 204 lemma3 eq with compare2 x x | putTest1Lemma2 x