Mercurial > hg > Papers > 2021 > soto-prosym

comparison Paper/src/redBlackTreeTest.agda.replaced @ 5:339fb67b4375

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
INIT rbt.agda
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 07 Nov 2021 00:51:16 +0900
parents c59202657321
children
comparison
equal deleted inserted replaced
4:72667e8198e2 5:339fb67b4375
11 open RedBlackTree.RedBlackTree 11 open RedBlackTree.RedBlackTree
12 open Stack 12 open Stack
13 13
14 -- tests 14 -- tests
15 15
16 putTree1 : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t 16 putTree1 : {n m : Level } {a k : Set n} {t : Set m} !$\rightarrow$! RedBlackTree {n} {m} {t} a k !$\rightarrow$! k !$\rightarrow$! a !$\rightarrow$! (RedBlackTree {n} {m} {t} a k !$\rightarrow$! t) !$\rightarrow$! t
17 putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree) 17 putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree)
18 ... | Nothing = next (record tree {root = Just (leafNode k1 value) }) 18 ... | Nothing = next (record tree {root = Just (leafNode k1 value) })
19 ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s @$\rightarrow$@ findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 @$\rightarrow$@ replaceNode tree1 s n1 next)) 19 ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s !$\rightarrow$! findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 !$\rightarrow$! replaceNode tree1 s n1 next))
20 20
21 open import Relation.Binary.PropositionalEquality 21 open import Relation.Binary.PropositionalEquality
22 open import Relation.Binary.Core 22 open import Relation.Binary.Core
23 open import Function 23 open import Function
24 24
25 25
26 check1 : {m : Level } (n : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@)) @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Bool {m} 26 check1 : {m : Level } (n : Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!)) !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! Bool {m}
27 check1 Nothing _ = False 27 check1 Nothing _ = False
28 check1 (Just n) x with Data.Nat.compare (value n) x 28 check1 (Just n) x with Data.Nat.compare (value n) x
29 ... | equal _ = True 29 ... | equal _ = True
30 ... | _ = False 30 ... | _ = False
31 31
32 check2 : {m : Level } (n : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@)) @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Bool {m} 32 check2 : {m : Level } (n : Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!)) !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! Bool {m}
33 check2 Nothing _ = False 33 check2 Nothing _ = False
34 check2 (Just n) x with compare2 (value n) x 34 check2 (Just n) x with compare2 (value n) x
35 ... | EQ = True 35 ... | EQ = True
36 ... | _ = False 36 ... | _ = False
37 37
38 test1 : putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ {Set Level.zero} ) 1 1 ( \t @$\rightarrow$@ getRedBlackTree t 1 ( \t x @$\rightarrow$@ check2 x 1 @$\equiv$@ True )) 38 test1 : putTree1 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$! {Set Level.zero} ) 1 1 ( \t !$\rightarrow$! getRedBlackTree t 1 ( \t x !$\rightarrow$! check2 x 1 !$\equiv$! True ))
39 test1 = refl 39 test1 = refl
40 40
41 test2 : putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ {Set Level.zero} ) 1 1 ( 41 test2 : putTree1 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$! {Set Level.zero} ) 1 1 (
42 \t @$\rightarrow$@ putTree1 t 2 2 ( 42 \t !$\rightarrow$! putTree1 t 2 2 (
43 \t @$\rightarrow$@ getRedBlackTree t 1 ( 43 \t !$\rightarrow$! getRedBlackTree t 1 (
44 \t x @$\rightarrow$@ check2 x 1 @$\equiv$@ True ))) 44 \t x !$\rightarrow$! check2 x 1 !$\equiv$! True )))
45 test2 = refl 45 test2 = refl
46 46
47 open @$\equiv$@-Reasoning 47 open !$\equiv$!-Reasoning
48 test3 : putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ {Set Level.zero}) 1 1 48 test3 : putTree1 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$! {Set Level.zero}) 1 1
49 $ \t @$\rightarrow$@ putTree1 t 2 2 49 $ \t !$\rightarrow$! putTree1 t 2 2
50 $ \t @$\rightarrow$@ putTree1 t 3 3 50 $ \t !$\rightarrow$! putTree1 t 3 3
51 $ \t @$\rightarrow$@ putTree1 t 4 4 51 $ \t !$\rightarrow$! putTree1 t 4 4
52 $ \t @$\rightarrow$@ getRedBlackTree t 1 52 $ \t !$\rightarrow$! getRedBlackTree t 1
53 $ \t x @$\rightarrow$@ check2 x 1 @$\equiv$@ True 53 $ \t x !$\rightarrow$! check2 x 1 !$\equiv$! True
54 test3 = begin 54 test3 = begin
55 check2 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1 55 check2 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1
56 @$\equiv$@@$\langle$@ refl @$\rangle$@ 56 !$\equiv$!!$\langle$! refl !$\rangle$!
57 True 57 True
58 @$\blacksquare$@ 58 !$\blacksquare$!
59 59
60 test31 = putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ ) 1 1 60 test31 = putTree1 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$! ) 1 1
61 $ \t @$\rightarrow$@ putTree1 t 2 2 61 $ \t !$\rightarrow$! putTree1 t 2 2
62 $ \t @$\rightarrow$@ putTree1 t 3 3 62 $ \t !$\rightarrow$! putTree1 t 3 3
63 $ \t @$\rightarrow$@ putTree1 t 4 4 63 $ \t !$\rightarrow$! putTree1 t 4 4
64 $ \t @$\rightarrow$@ getRedBlackTree t 4 64 $ \t !$\rightarrow$! getRedBlackTree t 4
65 $ \t x @$\rightarrow$@ x 65 $ \t x !$\rightarrow$! x
66 66
67 -- test5 : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@) 67 -- test5 : Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!)
68 test5 = putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ ) 4 4 68 test5 = putTree1 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$! ) 4 4
69 $ \t @$\rightarrow$@ putTree1 t 6 6 69 $ \t !$\rightarrow$! putTree1 t 6 6
70 $ \t0 @$\rightarrow$@ clearSingleLinkedStack (nodeStack t0) 70 $ \t0 !$\rightarrow$! clearSingleLinkedStack (nodeStack t0)
71 $ \s @$\rightarrow$@ findNode1 t0 s (leafNode 3 3) ( root t0 ) 71 $ \s !$\rightarrow$! findNode1 t0 s (leafNode 3 3) ( root t0 )
72 $ \t1 s n1 @$\rightarrow$@ replaceNode t1 s n1 72 $ \t1 s n1 !$\rightarrow$! replaceNode t1 s n1
73 $ \t @$\rightarrow$@ getRedBlackTree t 3 73 $ \t !$\rightarrow$! getRedBlackTree t 3
74 -- $ \t x @$\rightarrow$@ SingleLinkedStack.top (stack s) 74 -- $ \t x !$\rightarrow$! SingleLinkedStack.top (stack s)
75 -- $ \t x @$\rightarrow$@ n1 75 -- $ \t x !$\rightarrow$! n1
76 $ \t x @$\rightarrow$@ root t 76 $ \t x !$\rightarrow$! root t
77 where 77 where
78 findNode1 : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ (Node a k) @$\rightarrow$@ (Maybe (Node a k)) @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Node a k @$\rightarrow$@ t) @$\rightarrow$@ t 78 findNode1 : {n m : Level } {a k : Set n} {t : Set m} !$\rightarrow$! RedBlackTree {n} {m} {t} a k !$\rightarrow$! SingleLinkedStack (Node a k) !$\rightarrow$! (Node a k) !$\rightarrow$! (Maybe (Node a k)) !$\rightarrow$! (RedBlackTree {n} {m} {t} a k !$\rightarrow$! SingleLinkedStack (Node a k) !$\rightarrow$! Node a k !$\rightarrow$! t) !$\rightarrow$! t
79 findNode1 t s n1 Nothing next = next t s n1 79 findNode1 t s n1 Nothing next = next t s n1
80 findNode1 t s n1 ( Just n2 ) next = findNode t s n1 n2 next 80 findNode1 t s n1 ( Just n2 ) next = findNode t s n1 n2 next
81 81
82 -- test51 : putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {_} {Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@)} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ {Set Level.zero} ) 1 1 $ \t @$\rightarrow$@ 82 -- test51 : putTree1 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} {_} {Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!)} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$! {Set Level.zero} ) 1 1 $ \t !$\rightarrow$!
83 -- putTree1 t 2 2 $ \t @$\rightarrow$@ putTree1 t 3 3 $ \t @$\rightarrow$@ root t @$\equiv$@ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} ) 83 -- putTree1 t 2 2 $ \t !$\rightarrow$! putTree1 t 3 3 $ \t !$\rightarrow$! root t !$\equiv$! Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )
84 -- test51 = refl 84 -- test51 = refl
85 85
86 test6 : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@) 86 test6 : Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!)
87 test6 = root (createEmptyRedBlackTree@$\mathbb{N}$@ {_} @$\mathbb{N}$@ {Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@)}) 87 test6 = root (createEmptyRedBlackTree!$\mathbb{N}$! {_} !$\mathbb{N}$! {Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!)})
88 88
89 89
90 test7 : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@) 90 test7 : Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!)
91 test7 = clearSingleLinkedStack (nodeStack tree2) (\ s @$\rightarrow$@ replaceNode tree2 s n2 (\ t @$\rightarrow$@ root t)) 91 test7 = clearSingleLinkedStack (nodeStack tree2) (\ s !$\rightarrow$! replaceNode tree2 s n2 (\ t !$\rightarrow$! root t))
92 where 92 where
93 tree2 = createEmptyRedBlackTree@$\mathbb{N}$@ {_} @$\mathbb{N}$@ {Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@)} 93 tree2 = createEmptyRedBlackTree!$\mathbb{N}$! {_} !$\mathbb{N}$! {Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!)}
94 k1 = 1 94 k1 = 1
95 n2 = leafNode 0 0 95 n2 = leafNode 0 0
96 value1 = 1 96 value1 = 1
97 97
98 test8 : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@) 98 test8 : Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!)
99 test8 = putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@) 1 1 99 test8 = putTree1 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$!) 1 1
100 $ \t @$\rightarrow$@ putTree1 t 2 2 (\ t @$\rightarrow$@ root t) 100 $ \t !$\rightarrow$! putTree1 t 2 2 (\ t !$\rightarrow$! root t)
101 101
102 102
103 test9 : putRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ {Set Level.zero} ) 1 1 ( \t @$\rightarrow$@ getRedBlackTree t 1 ( \t x @$\rightarrow$@ check2 x 1 @$\equiv$@ True )) 103 test9 : putRedBlackTree {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$! {Set Level.zero} ) 1 1 ( \t !$\rightarrow$! getRedBlackTree t 1 ( \t x !$\rightarrow$! check2 x 1 !$\equiv$! True ))
104 test9 = refl 104 test9 = refl
105 105
106 test10 : putRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ {Set Level.zero} ) 1 1 ( 106 test10 : putRedBlackTree {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$! {Set Level.zero} ) 1 1 (
107 \t @$\rightarrow$@ putRedBlackTree t 2 2 ( 107 \t !$\rightarrow$! putRedBlackTree t 2 2 (
108 \t @$\rightarrow$@ getRedBlackTree t 1 ( 108 \t !$\rightarrow$! getRedBlackTree t 1 (
109 \t x @$\rightarrow$@ check2 x 1 @$\equiv$@ True ))) 109 \t x !$\rightarrow$! check2 x 1 !$\equiv$! True )))
110 test10 = refl 110 test10 = refl
111 111
112 test11 = putRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@) 1 1 112 test11 = putRedBlackTree {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (createEmptyRedBlackTree!$\mathbb{N}$! !$\mathbb{N}$!) 1 1
113 $ \t @$\rightarrow$@ putRedBlackTree t 2 2 113 $ \t !$\rightarrow$! putRedBlackTree t 2 2
114 $ \t @$\rightarrow$@ putRedBlackTree t 3 3 114 $ \t !$\rightarrow$! putRedBlackTree t 3 3
115 $ \t @$\rightarrow$@ getRedBlackTree t 2 115 $ \t !$\rightarrow$! getRedBlackTree t 2
116 $ \t x @$\rightarrow$@ root t 116 $ \t x !$\rightarrow$! root t
117 117
118 118
119 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}$@ 119 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}$!
120 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 } 120 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }
121 121
122 -- compare2 : (x y : @$\mathbb{N}$@ ) @$\rightarrow$@ compareresult 122 -- compare2 : (x y : !$\mathbb{N}$! ) !$\rightarrow$! compareresult
123 -- compare2 zero zero = eq 123 -- compare2 zero zero = eq
124 -- compare2 (suc _) zero = gt 124 -- compare2 (suc _) zero = gt
125 -- compare2 zero (suc _) = lt 125 -- compare2 zero (suc _) = lt
126 -- compare2 (suc x) (suc y) = compare2 x y 126 -- compare2 (suc x) (suc y) = compare2 x y
127 127
128 putTest1Lemma2 : (k : @$\mathbb{N}$@) @$\rightarrow$@ compare2 k k @$\equiv$@ EQ 128 putTest1Lemma2 : (k : !$\mathbb{N}$!) !$\rightarrow$! compare2 k k !$\equiv$! EQ
129 putTest1Lemma2 zero = refl 129 putTest1Lemma2 zero = refl
130 putTest1Lemma2 (suc k) = putTest1Lemma2 k 130 putTest1Lemma2 (suc k) = putTest1Lemma2 k
131 131
132 putTest1Lemma1 : (x y : @$\mathbb{N}$@) @$\rightarrow$@ compare@$\mathbb{N}$@ x y @$\equiv$@ compare2 x y 132 putTest1Lemma1 : (x y : !$\mathbb{N}$!) !$\rightarrow$! compare!$\mathbb{N}$! x y !$\equiv$! compare2 x y
133 putTest1Lemma1 zero zero = refl 133 putTest1Lemma1 zero zero = refl
134 putTest1Lemma1 (suc m) zero = refl 134 putTest1Lemma1 (suc m) zero = refl
135 putTest1Lemma1 zero (suc n) = refl 135 putTest1Lemma1 zero (suc n) = refl
136 putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n 136 putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n
137 putTest1Lemma1 (suc .m) (suc .(Data.Nat.suc m + k)) | less m k = lemma1 m 137 putTest1Lemma1 (suc .m) (suc .(Data.Nat.suc m + k)) | less m k = lemma1 m
138 where 138 where
139 lemma1 : (m : @$\mathbb{N}$@) @$\rightarrow$@ LT @$\equiv$@ compare2 m (@$\mathbb{N}$@.suc (m + k)) 139 lemma1 : (m : !$\mathbb{N}$!) !$\rightarrow$! LT !$\equiv$! compare2 m (!$\mathbb{N}$!.suc (m + k))
140 lemma1 zero = refl 140 lemma1 zero = refl
141 lemma1 (suc y) = lemma1 y 141 lemma1 (suc y) = lemma1 y
142 putTest1Lemma1 (suc .m) (suc .m) | equal m = lemma1 m 142 putTest1Lemma1 (suc .m) (suc .m) | equal m = lemma1 m
143 where 143 where
144 lemma1 : (m : @$\mathbb{N}$@) @$\rightarrow$@ EQ @$\equiv$@ compare2 m m 144 lemma1 : (m : !$\mathbb{N}$!) !$\rightarrow$! EQ !$\equiv$! compare2 m m
145 lemma1 zero = refl 145 lemma1 zero = refl
146 lemma1 (suc y) = lemma1 y 146 lemma1 (suc y) = lemma1 y
147 putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m) | greater m k = lemma1 m 147 putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m) | greater m k = lemma1 m
148 where 148 where
149 lemma1 : (m : @$\mathbb{N}$@) @$\rightarrow$@ GT @$\equiv$@ compare2 (@$\mathbb{N}$@.suc (m + k)) m 149 lemma1 : (m : !$\mathbb{N}$!) !$\rightarrow$! GT !$\equiv$! compare2 (!$\mathbb{N}$!.suc (m + k)) m
150 lemma1 zero = refl 150 lemma1 zero = refl
151 lemma1 (suc y) = lemma1 y 151 lemma1 (suc y) = lemma1 y
152 152
153 putTest1Lemma3 : (k : @$\mathbb{N}$@) @$\rightarrow$@ compare@$\mathbb{N}$@ k k @$\equiv$@ EQ 153 putTest1Lemma3 : (k : !$\mathbb{N}$!) !$\rightarrow$! compare!$\mathbb{N}$! k k !$\equiv$! EQ
154 putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k ) 154 putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k )
155 155
156 compareLemma1 : {x y : @$\mathbb{N}$@} @$\rightarrow$@ compare2 x y @$\equiv$@ EQ @$\rightarrow$@ x @$\equiv$@ y 156 compareLemma1 : {x y : !$\mathbb{N}$!} !$\rightarrow$! compare2 x y !$\equiv$! EQ !$\rightarrow$! x !$\equiv$! y
157 compareLemma1 {zero} {zero} refl = refl 157 compareLemma1 {zero} {zero} refl = refl
158 compareLemma1 {zero} {suc _} () 158 compareLemma1 {zero} {suc _} ()
159 compareLemma1 {suc _} {zero} () 159 compareLemma1 {suc _} {zero} ()
160 compareLemma1 {suc x} {suc y} eq = cong ( \z @$\rightarrow$@ @$\mathbb{N}$@.suc z ) ( compareLemma1 ( trans lemma2 eq ) ) 160 compareLemma1 {suc x} {suc y} eq = cong ( \z !$\rightarrow$! !$\mathbb{N}$!.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
161 where 161 where
162 lemma2 : compare2 (@$\mathbb{N}$@.suc x) (@$\mathbb{N}$@.suc y) @$\equiv$@ compare2 x y 162 lemma2 : compare2 (!$\mathbb{N}$!.suc x) (!$\mathbb{N}$!.suc y) !$\equiv$! compare2 x y
163 lemma2 = refl 163 lemma2 = refl
164 164
165 165
166 putTest1 :{ m : Level } (n : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@)) 166 putTest1 :{ m : Level } (n : Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!))
167 @$\rightarrow$@ (k : @$\mathbb{N}$@) (x : @$\mathbb{N}$@) 167 !$\rightarrow$! (k : !$\mathbb{N}$!) (x : !$\mathbb{N}$!)
168 @$\rightarrow$@ putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (redBlackInSomeState {_} @$\mathbb{N}$@ n {Set Level.zero}) k x 168 !$\rightarrow$! putTree1 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (redBlackInSomeState {_} !$\mathbb{N}$! n {Set Level.zero}) k x
169 (\ t @$\rightarrow$@ getRedBlackTree t k (\ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True)) 169 (\ t !$\rightarrow$! getRedBlackTree t k (\ t x1 !$\rightarrow$! check2 x1 x !$\equiv$! True))
170 putTest1 n k x with n 170 putTest1 n k x with n
171 ... | Just n1 = lemma2 ( record { top = Nothing } ) 171 ... | Just n1 = lemma2 ( record { top = Nothing } )
172 where 172 where
173 lemma2 : (s : SingleLinkedStack (Node @$\mathbb{N}$@ @$\mathbb{N}$@) ) @$\rightarrow$@ putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (@$\lambda$@ t @$\rightarrow$@ 173 lemma2 : (s : SingleLinkedStack (Node !$\mathbb{N}$! !$\mathbb{N}$!) ) !$\rightarrow$! putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (!$\lambda$! t !$\rightarrow$!
174 GetRedBlackTree.checkNode t k (@$\lambda$@ t@$\_{1}$@ x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) (root t)) 174 GetRedBlackTree.checkNode t k (!$\lambda$! t!$\_{1}$! x1 !$\rightarrow$! check2 x1 x !$\equiv$! True) (root t))
175 lemma2 s with compare2 k (key n1) 175 lemma2 s with compare2 k (key n1)
176 ... | EQ = lemma3 {!!} 176 ... | EQ = lemma3 {!!}
177 where 177 where
178 lemma3 : compare2 k (key n1) @$\equiv$@ EQ @$\rightarrow$@ getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record { root = Just ( record { 178 lemma3 : compare2 k (key n1) !$\equiv$! EQ !$\rightarrow$! getRedBlackTree {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} {Set Level.zero} ( record { root = Just ( record {
179 key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black 179 key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black
180 } ) ; nodeStack = s ; compare = @$\lambda$@ x@$\_{1}$@ y @$\rightarrow$@ compare2 x@$\_{1}$@ y } ) k ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) 180 } ) ; nodeStack = s ; compare = !$\lambda$! x!$\_{1}$! y !$\rightarrow$! compare2 x!$\_{1}$! y } ) k ( \ t x1 !$\rightarrow$! check2 x1 x !$\equiv$! True)
181 lemma3 eq with compare2 x x | putTest1Lemma2 x 181 lemma3 eq with compare2 x x | putTest1Lemma2 x
182 ... | EQ | refl with compare2 k (key n1) | eq 182 ... | EQ | refl with compare2 k (key n1) | eq
183 ... | EQ | refl with compare2 x x | putTest1Lemma2 x 183 ... | EQ | refl with compare2 x x | putTest1Lemma2 x
184 ... | EQ | refl = refl 184 ... | EQ | refl = refl
185 ... | GT = {!!} 185 ... | GT = {!!}
186 ... | LT = {!!} 186 ... | LT = {!!}
187 187
188 ... | Nothing = lemma1 188 ... | Nothing = lemma1
189 where 189 where
190 lemma1 : getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record { root = Just ( record { 190 lemma1 : getRedBlackTree {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} {Set Level.zero} ( record { root = Just ( record {
191 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red 191 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red
192 } ) ; nodeStack = record { top = Nothing } ; compare = @$\lambda$@ x@$\_{1}$@ y @$\rightarrow$@ compare2 x@$\_{1}$@ y } ) k 192 } ) ; nodeStack = record { top = Nothing } ; compare = !$\lambda$! x!$\_{1}$! y !$\rightarrow$! compare2 x!$\_{1}$! y } ) k
193 ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) 193 ( \ t x1 !$\rightarrow$! check2 x1 x !$\equiv$! True)
194 lemma1 with compare2 k k | putTest1Lemma2 k 194 lemma1 with compare2 k k | putTest1Lemma2 k
195 ... | EQ | refl with compare2 x x | putTest1Lemma2 x 195 ... | EQ | refl with compare2 x x | putTest1Lemma2 x
196 ... | EQ | refl = refl 196 ... | EQ | refl = refl