Mercurial > hg > Gears > GearsAgda

comparison redBlackTreeTest.agda @ 564:40ab3d39e49d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
using strict total order
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 11 Apr 2018 11:29:57 +0900
parents 8634f448e699
children ba7c5f1c2937
comparison
equal deleted inserted replaced
563:8634f448e699 564:40ab3d39e49d
6 6
7 open import Data.Empty 7 open import Data.Empty
8 8
9 open import Data.Nat 9 open import Data.Nat
10 open import Relation.Nullary 10 open import Relation.Nullary
11
12
13 open import Algebra
14 open import Relation.Binary
15 open import Data.Nat.Properties as NatProp
11 16
12 open Tree 17 open Tree
13 open Node 18 open Node
14 open RedBlackTree.RedBlackTree 19 open RedBlackTree.RedBlackTree
15 open Stack 20 open Stack
118 $ λ t → getRedBlackTree t 2 123 $ λ t → getRedBlackTree t 2
119 $ λ t x → root t 124 $ λ t x → root t
120 125
121 126
122 redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} → RedBlackTree {Level.zero} {m} {t} a ℕ 127 redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} → RedBlackTree {Level.zero} {m} {t} a ℕ
123 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 } 128 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compareT }
124 129
125 -- compare2 : (x y : ℕ ) → CompareResult {Level.zero} 130 -- compare2 : (x y : ℕ ) → CompareResult {Level.zero}
126 -- compare2 zero zero = EQ 131 -- compare2 zero zero = EQ
127 -- compare2 (suc _) zero = GT 132 -- compare2 (suc _) zero = GT
128 -- compare2 zero (suc _) = LT 133 -- compare2 zero (suc _) = LT
240 compareLemma1 {suc x} {suc y} eq = cong ( λ z → ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) ) 245 compareLemma1 {suc x} {suc y} eq = cong ( λ z → ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
241 where 246 where
242 lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y 247 lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
243 lemma2 = refl 248 lemma2 = refl
244 249
250 open IsStrictTotalOrder
251
252 compTri : ( x y : ℕ ) -> Tri (x < y) ( x ≡ y ) ( x > y )
253 compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder)
254
255 checkT : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool {m}
256 checkT Nothing _ = False
257 checkT (Just n) x with compTri (value n) x
258 ... | tri≈ _ _ _ = True
259 ... | _ = False
260
245 261
246 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ)) 262 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
247 → (k : ℕ) (x : ℕ) 263 → (k : ℕ) (x : ℕ)
248 → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x 264 → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
249 (λ t → getRedBlackTree t k (λ t x1 → check2 x1 x ≡ True)) 265 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True))
250 putTest1 n k x with n 266 putTest1 n k x with n
251 ... | Just n1 = lemma2 ( record { top = Nothing } ) 267 ... | Just n1 = lemma2 ( record { top = Nothing } )
252 where 268 where
253 lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t → 269 lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) →
254 GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t)) 270 putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compareT }) k x (λ t →
255 lemma2 s with compare2 k (key n1) 271 GetRedBlackTree.checkNode t k (λ t₁ x1 → checkT x1 x ≡ True) (root t))
256 ... | EQ = lemma3 {!!} 272 lemma2 s with compTri k (key n1)
273 ... | tri≈ le eq gt = lemma3
257 where 274 where
258 lemma3 : compare2 k (key n1) ≡ EQ → getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { 275 lemma3 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {
259 key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black 276 key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black
260 } ) ; nodeStack = s ; compare = λ x₁ y → compare2 x₁ y } ) k ( λ t x1 → check2 x1 x ≡ True) 277 } ) ; nodeStack = s ; compare = λ x₁ y → compareT x₁ y } ) k ( λ t x1 → checkT x1 x ≡ True)
261 lemma3 eq with compare2 x x | putTest1Lemma2 x 278 lemma3 = {!!}
262 ... | EQ | refl with compare2 k (key n1) | eq 279 ... | tri> le eq gt = {!!}
263 ... | EQ | refl with compare2 x x | putTest1Lemma2 x 280 ... | tri< le eq gt = {!!}
264 ... | EQ | refl = refl
265 ... | GT = {!!}
266 ... | LT = {!!}
267 ... | Nothing = lemma1 281 ... | Nothing = lemma1
268 where 282 where
269 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { 283 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {
270 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red 284 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red
271 } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y } ) k 285 } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y } ) k
272 ( λ t x1 → check2 x1 x ≡ True) 286 ( λ t x1 → checkT x1 x ≡ True)
273 lemma1 with compare2 k k | putTest1Lemma2 k 287 lemma1 = {!!}
274 ... | EQ | refl with compare2 x x | putTest1Lemma2 x
275 ... | EQ | refl = refl