|
7
|
1 redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a @$\mathbb{N}$@)) {t : Set m} @$\rightarrow$@ RedBlackTree {Level.zero} {m} {t} a @$\mathbb{N}$@
|
|
|
2 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }
|
|
|
3
|
|
|
4 putTest1 :{ m : Level } (n : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@))
|
|
|
5 @$\rightarrow$@ (k : @$\mathbb{N}$@) (x : @$\mathbb{N}$@)
|
|
|
6 @$\rightarrow$@ putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (redBlackInSomeState {_} @$\mathbb{N}$@ n {Set Level.zero}) k x
|
|
|
7 (\ t @$\rightarrow$@ getRedBlackTree t k (\ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True))
|
|
|
8 putTest1 n k x with n
|
|
|
9 ... | Just n1 = lemma2 ( record { top = Nothing } )
|
|
|
10 where
|
|
|
11 lemma2 : (s : SingleLinkedStack (Node @$\mathbb{N}$@ @$\mathbb{N}$@) ) @$\rightarrow$@ putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
|
|
|
12 GetRedBlackTree.checkNode t k (λ t@$\text{1}$@ x1 → check2 x1 x @$\equiv$@ True) (root t))
|
|
|
13 lemma2 s with compare2 k (key n1)
|
|
|
14 ... | EQ = lemma3 {!!}
|
|
|
15 where
|
|
|
16 lemma3 : compare2 k (key n1) @$\equiv$@ EQ @$\rightarrow$@ getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record { root = Just ( record {
|
|
|
17 key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black
|
|
|
18 } ) ; nodeStack = s ; compare = λ x@$\text{1}$@ y → compare2 x@$\text{1}$@ y } ) k ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True)
|
|
|
19 lemma3 eq with compare2 x x | putTest1Lemma2 x
|
|
|
20 ... | EQ | refl with compare2 k (key n1) | eq
|
|
|
21 ... | EQ | refl with compare2 x x | putTest1Lemma2 x
|
|
|
22 ... | EQ | refl = refl
|
|
|
23 ... | GT = {!!}
|
|
|
24 ... | LT = {!!}
|
|
|
25
|
|
|
26 ... | Nothing = lemma1
|
|
|
27 where
|
|
|
28 lemma1 : getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record { root = Just ( record {
|
|
|
29 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red
|
|
|
30 } ) ; nodeStack = record { top = Nothing } ; compare = λ x@$\text{1}$@ y → compare2 x@$\text{1}$@ y } ) k
|
|
|
31 ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True)
|
|
|
32 lemma1 with compare2 k k | putTest1Lemma2 k
|
|
|
33 ... | EQ | refl with compare2 x x | putTest1Lemma2 x
|
|
|
34 ... | EQ | refl = refl
|
