annotate redBlackTreeTest.agda @ 563:8634f448e699

minor fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 30 Mar 2018 11:09:06 +0900
parents 9df8103bc493
children 40ab3d39e49d
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
537
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
1 module redBlackTreeTest where
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
2
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
3 open import RedBlackTree
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
4 open import stack
554
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 553
diff changeset
5 open import Level hiding (zero) renaming ( suc to succ )
537
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
6
553
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
7 open import Data.Empty
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
8
537
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
9 open import Data.Nat
553
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
10 open import Relation.Nullary
537
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
11
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
12 open Tree
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
13 open Node
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
14 open RedBlackTree.RedBlackTree
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
15 open Stack
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
16
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
17 -- tests
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
18
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
19 putTree1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → k → a → (RedBlackTree {n} {m} {t} a k → t) → t
543
1595dd84fc3e fix use SingleLinkedStack
ryokka
parents: 542
diff changeset
20 putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree)
537
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
21 ... | Nothing = next (record tree {root = Just (leafNode k1 value) })
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
22 ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode k1 value) n2 (λ tree1 s n1 → replaceNode tree1 s n1 next))
537
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
23
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
24 open import Relation.Binary.PropositionalEquality
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
25 open import Relation.Binary.Core
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
26 open import Function
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
27
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
28
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
29 check1 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool {m}
537
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
30 check1 Nothing _ = False
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
31 check1 (Just n) x with Data.Nat.compare (value n) x
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
32 ... | equal _ = True
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
33 ... | _ = False
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
34
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
35 check2 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool {m}
549
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
36 check2 Nothing _ = False
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
37 check2 (Just n) x with compare2 (value n) x
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
38 ... | EQ = True
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
39 ... | _ = False
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
40
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
41 test1 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 x 1 ≡ True ))
537
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
42 test1 = refl
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
43
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
44 test2 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
45 λ t → putTree1 t 2 2 (
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
46 λ t → getRedBlackTree t 1 (
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
47 λ t x → check2 x 1 ≡ True )))
537
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
48 test2 = refl
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
49
545
b180dc78abcf add someTest
ryokka
parents: 544
diff changeset
50 open ≡-Reasoning
542
ee65e69c9b62 puttree1 act
ryokka
parents: 541
diff changeset
51 test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
52 $ λ t → putTree1 t 2 2
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
53 $ λ t → putTree1 t 3 3
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
54 $ λ t → putTree1 t 4 4
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
55 $ λ t → getRedBlackTree t 1
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
56 $ λ t x → check2 x 1 ≡ True
545
b180dc78abcf add someTest
ryokka
parents: 544
diff changeset
57 test3 = begin
549
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
58 check2 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1
545
b180dc78abcf add someTest
ryokka
parents: 544
diff changeset
59 ≡⟨ refl ⟩
b180dc78abcf add someTest
ryokka
parents: 544
diff changeset
60 True
b180dc78abcf add someTest
ryokka
parents: 544
diff changeset
61
542
ee65e69c9b62 puttree1 act
ryokka
parents: 541
diff changeset
62
ee65e69c9b62 puttree1 act
ryokka
parents: 541
diff changeset
63 test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
64 $ λ t → putTree1 t 2 2
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
65 $ λ t → putTree1 t 3 3
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
66 $ λ t → putTree1 t 4 4
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
67 $ λ t → getRedBlackTree t 4
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
68 $ λ t x → x
538
5c001e8ba0d5 add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents: 537
diff changeset
69
540
6a4830c5a514 testing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 539
diff changeset
70 -- test5 : Maybe (Node ℕ ℕ)
541
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 540
diff changeset
71 test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
72 $ λ t → putTree1 t 6 6
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
73 $ λ t0 → clearSingleLinkedStack (nodeStack t0)
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
74 $ λ s → findNode1 t0 s (leafNode 3 3) ( root t0 )
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
75 $ λ t1 s n1 → replaceNode t1 s n1
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
76 $ λ t → getRedBlackTree t 3
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
77 -- $ λ t x → SingleLinkedStack.top (stack s)
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
78 -- $ λ t x → n1
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
79 $ λ t x → root t
540
6a4830c5a514 testing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 539
diff changeset
80 where
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
81 findNode1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → (Node a k) → (Maybe (Node a k)) → (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → t) → t
540
6a4830c5a514 testing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 539
diff changeset
82 findNode1 t s n1 Nothing next = next t s n1
6a4830c5a514 testing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 539
diff changeset
83 findNode1 t s n1 ( Just n2 ) next = findNode t s n1 n2 next
538
5c001e8ba0d5 add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents: 537
diff changeset
84
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
85 -- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ λ t →
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
86 -- putTree1 t 2 2 $ λ t → putTree1 t 3 3 $ λ t → root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )
538
5c001e8ba0d5 add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents: 537
diff changeset
87 -- test51 = refl
539
39d465c20e5a print contant tree. C-c C-n test.
ryokka
parents: 538
diff changeset
88
39d465c20e5a print contant tree. C-c C-n test.
ryokka
parents: 538
diff changeset
89 test6 : Maybe (Node ℕ ℕ)
39d465c20e5a print contant tree. C-c C-n test.
ryokka
parents: 538
diff changeset
90 test6 = root (createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)})
39d465c20e5a print contant tree. C-c C-n test.
ryokka
parents: 538
diff changeset
91
39d465c20e5a print contant tree. C-c C-n test.
ryokka
parents: 538
diff changeset
92
39d465c20e5a print contant tree. C-c C-n test.
ryokka
parents: 538
diff changeset
93 test7 : Maybe (Node ℕ ℕ)
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
94 test7 = clearSingleLinkedStack (nodeStack tree2) (λ s → replaceNode tree2 s n2 (λ t → root t))
539
39d465c20e5a print contant tree. C-c C-n test.
ryokka
parents: 538
diff changeset
95 where
39d465c20e5a print contant tree. C-c C-n test.
ryokka
parents: 538
diff changeset
96 tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}
39d465c20e5a print contant tree. C-c C-n test.
ryokka
parents: 538
diff changeset
97 k1 = 1
39d465c20e5a print contant tree. C-c C-n test.
ryokka
parents: 538
diff changeset
98 n2 = leafNode 0 0
39d465c20e5a print contant tree. C-c C-n test.
ryokka
parents: 538
diff changeset
99 value1 = 1
39d465c20e5a print contant tree. C-c C-n test.
ryokka
parents: 538
diff changeset
100
39d465c20e5a print contant tree. C-c C-n test.
ryokka
parents: 538
diff changeset
101 test8 : Maybe (Node ℕ ℕ)
39d465c20e5a print contant tree. C-c C-n test.
ryokka
parents: 538
diff changeset
102 test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
103 $ λ t → putTree1 t 2 2 (λ t → root t)
544
4f692df9b3db add reference
ryokka
parents: 543
diff changeset
104
4f692df9b3db add reference
ryokka
parents: 543
diff changeset
105
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
106 test9 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 x 1 ≡ True ))
544
4f692df9b3db add reference
ryokka
parents: 543
diff changeset
107 test9 = refl
4f692df9b3db add reference
ryokka
parents: 543
diff changeset
108
4f692df9b3db add reference
ryokka
parents: 543
diff changeset
109 test10 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
110 λ t → putRedBlackTree t 2 2 (
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
111 λ t → getRedBlackTree t 1 (
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
112 λ t x → check2 x 1 ≡ True )))
544
4f692df9b3db add reference
ryokka
parents: 543
diff changeset
113 test10 = refl
4f692df9b3db add reference
ryokka
parents: 543
diff changeset
114
4f692df9b3db add reference
ryokka
parents: 543
diff changeset
115 test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
116 $ λ t → putRedBlackTree t 2 2
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
117 $ λ t → putRedBlackTree t 3 3
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
118 $ λ t → getRedBlackTree t 2
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
119 $ λ t x → root t
545
b180dc78abcf add someTest
ryokka
parents: 544
diff changeset
120
b180dc78abcf add someTest
ryokka
parents: 544
diff changeset
121
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
122 redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} → RedBlackTree {Level.zero} {m} {t} a ℕ
549
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
123 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }
545
b180dc78abcf add someTest
ryokka
parents: 544
diff changeset
124
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
125 -- compare2 : (x y : ℕ ) → CompareResult {Level.zero}
549
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
126 -- compare2 zero zero = EQ
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
127 -- compare2 (suc _) zero = GT
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
128 -- compare2 zero (suc _) = LT
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
129 -- compare2 (suc x) (suc y) = compare2 x y
546
b654ce34c894 add putTest1Lemma1, putTest1
ryokka
parents: 545
diff changeset
130
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
131 contraposition : {m : Level } {A B : Set m} → (B → A) → (¬ A → ¬ B)
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
132 contraposition f = λ x y → x (f y)
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
133
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
134 compareTri1 : (n : ℕ) → zero <′ suc n
554
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 553
diff changeset
135 compareTri1 zero = ≤′-refl
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 553
diff changeset
136 compareTri1 (suc n) = ≤′-step ( compareTri1 n )
553
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
137
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
138 compareTri2 : (n m : ℕ) → n ≤′ m → suc n ≤′ suc m
554
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 553
diff changeset
139 compareTri2 _ _ ≤′-refl = ≤′-refl
556
69fc15bb4e82 add some lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 555
diff changeset
140 compareTri2 n (suc m) ( ≤′-step p ) = ≤′-step { suc n } ( compareTri2 n m p )
69fc15bb4e82 add some lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 555
diff changeset
141
558
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 557
diff changeset
142 <′dec : Set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 557
diff changeset
143 <′dec = ∀ m n → Dec ( m ≤′ n )
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
144
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
145 compareTri6 : ∀ m {n} → ¬ m ≤′ n → ¬ suc m ≤′ suc n
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
146
558
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 557
diff changeset
147 is≤′ : <′dec
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 557
diff changeset
148 is≤′ zero zero = yes ≤′-refl
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
149 is≤′ zero (suc n) = yes (lemma n)
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
150 where
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
151 lemma : (n : ℕ) → zero ≤′ suc n
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
152 lemma zero = ≤′-step ≤′-refl
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
153 lemma (suc n) = ≤′-step (lemma n)
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
154 is≤′ (suc m) (zero) = no ( λ () )
558
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 557
diff changeset
155 is≤′ (suc m) (suc n) with is≤′ m n
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
156 ... | yes p = yes ( compareTri2 _ _ p )
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
157 ... | no p = no ( compareTri6 _ p )
557
90999865d7f3 some try ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 556
diff changeset
158
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
159 compareTri20 : {n : ℕ} → ¬ suc n ≤′ zero
561
1bbbd787472e trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 560
diff changeset
160 compareTri20 ()
1bbbd787472e trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 560
diff changeset
161
559
ryokka
parents: 558
diff changeset
162
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
163 compareTri21 : (n m : ℕ) → suc n ≤′ suc m → n ≤′ m
559
ryokka
parents: 558
diff changeset
164 compareTri21 _ _ ≤′-refl = ≤′-refl
561
1bbbd787472e trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 560
diff changeset
165 compareTri21 (suc n) zero ( ≤′-step p ) = compareTri23 (suc n) ( ≤′-step p ) p
1bbbd787472e trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 560
diff changeset
166 where
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
167 compareTri23 : (n : ℕ) → suc n ≤′ suc zero → suc n ≤′ zero → n ≤′ zero
561
1bbbd787472e trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 560
diff changeset
168 compareTri23 zero ( ≤′-step p ) _ = ≤′-refl
1bbbd787472e trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 560
diff changeset
169 compareTri23 zero ≤′-refl _ = ≤′-refl
1bbbd787472e trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 560
diff changeset
170 compareTri23 (suc n1) ( ≤′-step p ) ()
559
ryokka
parents: 558
diff changeset
171 compareTri21 n (suc m) ( ≤′-step p ) = ≤′-step (compareTri21 _ _ p)
560
f4779958ff6a compareTri5 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 559
diff changeset
172 compareTri21 zero zero ( ≤′-step p ) = ≤′-refl
f4779958ff6a compareTri5 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 559
diff changeset
173
559
ryokka
parents: 558
diff changeset
174
ryokka
parents: 558
diff changeset
175 compareTri3 : ∀ m {n} → ¬ m ≡ suc (m + n)
ryokka
parents: 558
diff changeset
176 compareTri3 zero ()
ryokka
parents: 558
diff changeset
177 compareTri3 (suc m) eq = compareTri3 m (cong pred eq)
ryokka
parents: 558
diff changeset
178
563
8634f448e699 minor fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 562
diff changeset
179 compareTri4' : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
8634f448e699 minor fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 562
diff changeset
180 compareTri4' m {n} with n ≟ m
559
ryokka
parents: 558
diff changeset
181 ... | yes refl = λ x y → x refl
ryokka
parents: 558
diff changeset
182 ... | no p = λ x y → p ( cong pred y )
ryokka
parents: 558
diff changeset
183
563
8634f448e699 minor fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 562
diff changeset
184 compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
8634f448e699 minor fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 562
diff changeset
185 compareTri4 m = contraposition ( λ x → cong pred x )
8634f448e699 minor fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 562
diff changeset
186
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
187 -- compareTri6 : ∀ m {n} → ¬ m ≤′ n → ¬ suc m ≤′ suc n
559
ryokka
parents: 558
diff changeset
188 compareTri6 m {n} = λ x y → x (compareTri21 _ _ y)
ryokka
parents: 558
diff changeset
189
560
f4779958ff6a compareTri5 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 559
diff changeset
190 compareTri5 : ∀ m {n} → ¬ m <′ n → ¬ suc m <′ suc n
f4779958ff6a compareTri5 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 559
diff changeset
191 compareTri5 m {n} = compareTri6 (suc m)
f4779958ff6a compareTri5 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 559
diff changeset
192
554
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 553
diff changeset
193 compareTri : Trichotomous _≡_ _<′_
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 553
diff changeset
194 compareTri zero zero = tri≈ ( λ ()) refl ( λ ())
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 553
diff changeset
195 compareTri zero (suc n) = tri< ( compareTri1 n ) ( λ ()) ( λ ())
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 553
diff changeset
196 compareTri (suc n) zero = tri> ( λ ()) ( λ ()) ( compareTri1 n )
553
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
197 compareTri (suc n) (suc m) with compareTri n m
556
69fc15bb4e82 add some lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 555
diff changeset
198 ... | tri< p q r = tri< (compareTri2 (suc n) m p ) (compareTri4 _ q) ( compareTri5 _ r )
69fc15bb4e82 add some lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 555
diff changeset
199 ... | tri≈ p refl r = tri≈ (compareTri5 _ p) refl ( compareTri5 _ r )
69fc15bb4e82 add some lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 555
diff changeset
200 ... | tri> p q r = tri> ( compareTri5 _ p ) (compareTri4 _ q) (compareTri2 (suc m) n r )
553
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
201
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
202 compareDecTest : (n n1 : Node ℕ ℕ) → ( key n ≡ key n1 ) ∨ ( ¬ key n ≡ key n1 )
553
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
203 compareDecTest n n1 with (key n) ≟ (key n1)
556
69fc15bb4e82 add some lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 555
diff changeset
204 ... | yes p = pi1 p
554
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 553
diff changeset
205 ... | no ¬p = pi2 ¬p
553
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
206
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
207
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
208 putTest1Lemma2 : (k : ℕ) → compare2 k k ≡ EQ
548
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
209 putTest1Lemma2 zero = refl
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
210 putTest1Lemma2 (suc k) = putTest1Lemma2 k
546
b654ce34c894 add putTest1Lemma1, putTest1
ryokka
parents: 545
diff changeset
211
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
212 putTest1Lemma1 : (x y : ℕ) → compareℕ x y ≡ compare2 x y
548
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
213 putTest1Lemma1 zero zero = refl
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
214 putTest1Lemma1 (suc m) zero = refl
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
215 putTest1Lemma1 zero (suc n) = refl
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
216 putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
217 putTest1Lemma1 (suc .m) (suc .(Data.Nat.suc m + k)) | less m k = lemma1 m
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
218 where
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
219 lemma1 : (m : ℕ) → LT ≡ compare2 m (ℕ.suc (m + k))
548
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
220 lemma1 zero = refl
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
221 lemma1 (suc y) = lemma1 y
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
222 putTest1Lemma1 (suc .m) (suc .m) | equal m = lemma1 m
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
223 where
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
224 lemma1 : (m : ℕ) → EQ ≡ compare2 m m
548
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
225 lemma1 zero = refl
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
226 lemma1 (suc y) = lemma1 y
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
227 putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m) | greater m k = lemma1 m
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
228 where
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
229 lemma1 : (m : ℕ) → GT ≡ compare2 (ℕ.suc (m + k)) m
548
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
230 lemma1 zero = refl
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
231 lemma1 (suc y) = lemma1 y
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
232
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
233 putTest1Lemma3 : (k : ℕ) → compareℕ k k ≡ EQ
548
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
234 putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k )
546
b654ce34c894 add putTest1Lemma1, putTest1
ryokka
parents: 545
diff changeset
235
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
236 compareLemma1 : {x y : ℕ} → compare2 x y ≡ EQ → x ≡ y
551
8bc39f95c961 fix findNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 550
diff changeset
237 compareLemma1 {zero} {zero} refl = refl
8bc39f95c961 fix findNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 550
diff changeset
238 compareLemma1 {zero} {suc _} ()
8bc39f95c961 fix findNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 550
diff changeset
239 compareLemma1 {suc _} {zero} ()
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
240 compareLemma1 {suc x} {suc y} eq = cong ( λ z → ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
550
2476f7123dc3 root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 549
diff changeset
241 where
2476f7123dc3 root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 549
diff changeset
242 lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
2476f7123dc3 root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 549
diff changeset
243 lemma2 = refl
549
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
244
546
b654ce34c894 add putTest1Lemma1, putTest1
ryokka
parents: 545
diff changeset
245
545
b180dc78abcf add someTest
ryokka
parents: 544
diff changeset
246 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
247 → (k : ℕ) (x : ℕ)
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
248 → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
249 (λ t → getRedBlackTree t k (λ t x1 → check2 x1 x ≡ True))
546
b654ce34c894 add putTest1Lemma1, putTest1
ryokka
parents: 545
diff changeset
250 putTest1 n k x with n
552
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 551
diff changeset
251 ... | Just n1 = lemma2 ( record { top = Nothing } )
551
8bc39f95c961 fix findNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 550
diff changeset
252 where
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
253 lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
551
8bc39f95c961 fix findNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 550
diff changeset
254 GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t))
552
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 551
diff changeset
255 lemma2 s with compare2 k (key n1)
553
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
256 ... | EQ = lemma3 {!!}
551
8bc39f95c961 fix findNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 550
diff changeset
257 where
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
258 lemma3 : compare2 k (key n1) ≡ EQ → getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {
551
8bc39f95c961 fix findNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 550
diff changeset
259 key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
260 } ) ; nodeStack = s ; compare = λ x₁ y → compare2 x₁ y } ) k ( λ t x1 → check2 x1 x ≡ True)
552
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 551
diff changeset
261 lemma3 eq with compare2 x x | putTest1Lemma2 x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 551
diff changeset
262 ... | EQ | refl with compare2 k (key n1) | eq
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 551
diff changeset
263 ... | EQ | refl with compare2 x x | putTest1Lemma2 x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 551
diff changeset
264 ... | EQ | refl = refl
551
8bc39f95c961 fix findNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 550
diff changeset
265 ... | GT = {!!}
8bc39f95c961 fix findNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 550
diff changeset
266 ... | LT = {!!}
549
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
267 ... | Nothing = lemma1
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
268 where
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
269 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
270 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
271 } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y } ) k
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
272 ( λ t x1 → check2 x1 x ≡ True)
550
2476f7123dc3 root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 549
diff changeset
273 lemma1 with compare2 k k | putTest1Lemma2 k
2476f7123dc3 root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 549
diff changeset
274 ... | EQ | refl with compare2 x x | putTest1Lemma2 x
2476f7123dc3 root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 549
diff changeset
275 ... | EQ | refl = refl