Mercurial > hg > Members > Moririn

annotate etc/trichotomos-ex.agda @ 770:a4bc901bba36

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
RBI record
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 08 May 2023 12:59:13 +0900
parents f24a73245f36
children 0b791ae19543
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
569
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
1 module trichotomos-ex where
537
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
2
554
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 553
diff changeset
3 open import Level hiding (zero) renaming ( suc to succ )
553
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
4 open import Data.Empty
537
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
5 open import Data.Nat
553
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
6 open import Relation.Nullary
564
40ab3d39e49d using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 563
diff changeset
7 open import Algebra
40ab3d39e49d using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 563
diff changeset
8 open import Data.Nat.Properties as NatProp
569
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
9 open import Relation.Binary
537
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
10 open import Relation.Binary.PropositionalEquality
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
11 open import Relation.Binary.Core
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
12 open import Function
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
13
569
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
14 data Bool {n : Level } : Set n where
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
15 True : Bool
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
16 False : Bool
537
fffeaf0b0024 add stackTest redBlackTreeTest
ryokka
parents:
diff changeset
17
569
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
18 record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
19 field
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
20 pi1 : a
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
21 pi2 : b
538
5c001e8ba0d5 add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents: 537
diff changeset
22
569
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
23 data _∨_ {n : Level } (a : Set n) (b : Set n): Set n where
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
24 pi1 : a -> a ∨ b
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
25 pi2 : b -> a ∨ b
539
39d465c20e5a print contant tree. C-c C-n test.
ryokka
parents: 538
diff changeset
26
39d465c20e5a print contant tree. C-c C-n test.
ryokka
parents: 538
diff changeset
27
569
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
28 data Maybe {n : Level } (a : Set n) : Set n where
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
29 Nothing : Maybe a
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
30 Just : a -> Maybe a
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
31
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
32 data Color {n : Level } : Set n where
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
33 Red : Color
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
34 Black : Color
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
35
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
36 data CompareResult {n : Level } : Set n where
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
37 LT : CompareResult
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
38 GT : CompareResult
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
39 EQ : CompareResult
539
39d465c20e5a print contant tree. C-c C-n test.
ryokka
parents: 538
diff changeset
40
569
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
41 record Node {n : Level } (a k : Set n) : Set n where
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
42 inductive
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
43 field
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
44 key : k
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
45 value : a
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
46 right : Maybe (Node a k)
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
47 left : Maybe (Node a k)
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
48 color : Color {n}
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
49 open Node
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
50
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
51 compareℕ : ℕ → ℕ → CompareResult {Level.zero}
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
52 compareℕ x y with Data.Nat.compare x y
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
53 ... | less _ _ = LT
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
54 ... | equal _ = EQ
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
55 ... | greater _ _ = GT
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
56
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
57 compareT : ℕ → ℕ → CompareResult {Level.zero}
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
58 compareT x y with IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder) x y
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
59 ... | tri≈ _ _ _ = EQ
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
60 ... | tri< _ _ _ = LT
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
61 ... | tri> _ _ _ = GT
544
4f692df9b3db add reference
ryokka
parents: 543
diff changeset
62
4f692df9b3db add reference
ryokka
parents: 543
diff changeset
63
569
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
64 compare2 : (x y : ℕ ) → CompareResult {Level.zero}
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
65 compare2 zero zero = EQ
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
66 compare2 (suc _) zero = GT
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
67 compare2 zero (suc _) = LT
f24a73245f36 separate trichotomos exercise
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 568
diff changeset
68 compare2 (suc x) (suc y) = compare2 x y
546
b654ce34c894 add putTest1Lemma1, putTest1
ryokka
parents: 545
diff changeset
69
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
70 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
71 contraposition f = λ x y → x (f y)
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
72
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
73 compareTri1 : (n : ℕ) → zero <′ suc n
554
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 553
diff changeset
74 compareTri1 zero = ≤′-refl
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 553
diff changeset
75 compareTri1 (suc n) = ≤′-step ( compareTri1 n )
553
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
76
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
77 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
78 compareTri2 _ _ ≤′-refl = ≤′-refl
556
69fc15bb4e82 add some lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 555
diff changeset
79 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
80
558
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 557
diff changeset
81 <′dec : Set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 557
diff changeset
82 <′dec = ∀ m n → Dec ( m ≤′ n )
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
83
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
84 compareTri6 : ∀ m {n} → ¬ m ≤′ n → ¬ suc m ≤′ suc n
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
85
558
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 557
diff changeset
86 is≤′ : <′dec
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 557
diff changeset
87 is≤′ zero zero = yes ≤′-refl
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
88 is≤′ zero (suc n) = yes (lemma n)
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
89 where
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
90 lemma : (n : ℕ) → zero ≤′ suc n
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
91 lemma zero = ≤′-step ≤′-refl
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
92 lemma (suc n) = ≤′-step (lemma n)
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
93 is≤′ (suc m) (zero) = no ( λ () )
558
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 557
diff changeset
94 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
95 ... | yes p = yes ( compareTri2 _ _ p )
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
96 ... | no p = no ( compareTri6 _ p )
557
90999865d7f3 some try ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 556
diff changeset
97
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
98 compareTri20 : {n : ℕ} → ¬ suc n ≤′ zero
561
1bbbd787472e trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 560
diff changeset
99 compareTri20 ()
1bbbd787472e trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 560
diff changeset
100
559
ryokka
parents: 558
diff changeset
101
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
102 compareTri21 : (n m : ℕ) → suc n ≤′ suc m → n ≤′ m
559
ryokka
parents: 558
diff changeset
103 compareTri21 _ _ ≤′-refl = ≤′-refl
561
1bbbd787472e trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 560
diff changeset
104 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
105 where
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
106 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
107 compareTri23 zero ( ≤′-step p ) _ = ≤′-refl
1bbbd787472e trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 560
diff changeset
108 compareTri23 zero ≤′-refl _ = ≤′-refl
1bbbd787472e trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 560
diff changeset
109 compareTri23 (suc n1) ( ≤′-step p ) ()
559
ryokka
parents: 558
diff changeset
110 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
111 compareTri21 zero zero ( ≤′-step p ) = ≤′-refl
f4779958ff6a compareTri5 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 559
diff changeset
112
559
ryokka
parents: 558
diff changeset
113
ryokka
parents: 558
diff changeset
114 compareTri3 : ∀ m {n} → ¬ m ≡ suc (m + n)
ryokka
parents: 558
diff changeset
115 compareTri3 zero ()
ryokka
parents: 558
diff changeset
116 compareTri3 (suc m) eq = compareTri3 m (cong pred eq)
ryokka
parents: 558
diff changeset
117
563
8634f448e699 minor fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 562
diff changeset
118 compareTri4' : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
8634f448e699 minor fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 562
diff changeset
119 compareTri4' m {n} with n ≟ m
559
ryokka
parents: 558
diff changeset
120 ... | yes refl = λ x y → x refl
ryokka
parents: 558
diff changeset
121 ... | no p = λ x y → p ( cong pred y )
ryokka
parents: 558
diff changeset
122
563
8634f448e699 minor fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 562
diff changeset
123 compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
8634f448e699 minor fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 562
diff changeset
124 compareTri4 m = contraposition ( λ x → cong pred x )
8634f448e699 minor fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 562
diff changeset
125
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
126 -- compareTri6 : ∀ m {n} → ¬ m ≤′ n → ¬ suc m ≤′ suc n
559
ryokka
parents: 558
diff changeset
127 compareTri6 m {n} = λ x y → x (compareTri21 _ _ y)
ryokka
parents: 558
diff changeset
128
560
f4779958ff6a compareTri5 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 559
diff changeset
129 compareTri5 : ∀ m {n} → ¬ m <′ n → ¬ suc m <′ suc n
f4779958ff6a compareTri5 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 559
diff changeset
130 compareTri5 m {n} = compareTri6 (suc m)
f4779958ff6a compareTri5 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 559
diff changeset
131
554
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 553
diff changeset
132 compareTri : Trichotomous _≡_ _<′_
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 553
diff changeset
133 compareTri zero zero = tri≈ ( λ ()) refl ( λ ())
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 553
diff changeset
134 compareTri zero (suc n) = tri< ( compareTri1 n ) ( λ ()) ( λ ())
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 553
diff changeset
135 compareTri (suc n) zero = tri> ( λ ()) ( λ ()) ( compareTri1 n )
553
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
136 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
137 ... | 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
138 ... | 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
139 ... | tri> p q r = tri> ( compareTri5 _ p ) (compareTri4 _ q) (compareTri2 (suc m) n r )
553
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
140
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
141 compareDecTest : (n n1 : Node ℕ ℕ) → ( key n ≡ key n1 ) ∨ ( ¬ key n ≡ key n1 )
553
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
142 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
143 ... | yes p = pi1 p
554
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 553
diff changeset
144 ... | no ¬p = pi2 ¬p
553
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
145
7d9af1d4b5af add compareTri
ryokka
parents: 552
diff changeset
146
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
147 putTest1Lemma2 : (k : ℕ) → compare2 k k ≡ EQ
548
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
148 putTest1Lemma2 zero = refl
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
149 putTest1Lemma2 (suc k) = putTest1Lemma2 k
546
b654ce34c894 add putTest1Lemma1, putTest1
ryokka
parents: 545
diff changeset
150
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
151 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
152 putTest1Lemma1 zero zero = refl
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
153 putTest1Lemma1 (suc m) zero = refl
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
154 putTest1Lemma1 zero (suc n) = refl
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
155 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
156 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
157 where
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
158 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
159 lemma1 zero = refl
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
160 lemma1 (suc y) = lemma1 y
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
161 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
162 where
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
163 lemma1 : (m : ℕ) → EQ ≡ compare2 m m
548
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
164 lemma1 zero = refl
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
165 lemma1 (suc y) = lemma1 y
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
166 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
167 where
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
168 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
169 lemma1 zero = refl
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
170 lemma1 (suc y) = lemma1 y
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
171
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
172 putTest1Lemma3 : (k : ℕ) → compareℕ k k ≡ EQ
548
c304869ac439 compareN x x = EQ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 547
diff changeset
173 putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k )
546
b654ce34c894 add putTest1Lemma1, putTest1
ryokka
parents: 545
diff changeset
174
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
175 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
176 compareLemma1 {zero} {zero} refl = refl
8bc39f95c961 fix findNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 550
diff changeset
177 compareLemma1 {zero} {suc _} ()
8bc39f95c961 fix findNode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 550
diff changeset
178 compareLemma1 {suc _} {zero} ()
562
9df8103bc493 dec ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 561
diff changeset
179 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
180 where
2476f7123dc3 root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 549
diff changeset
181 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
182 lemma2 = refl
549
bc3208d510cd add some
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 548
diff changeset
183
564
40ab3d39e49d using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 563
diff changeset
184
40ab3d39e49d using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 563
diff changeset
185 compTri : ( x y : ℕ ) -> Tri (x < y) ( x ≡ y ) ( x > y )
40ab3d39e49d using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 563
diff changeset
186 compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder)
565
ba7c5f1c2937 this slightly better
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 564
diff changeset
187 where open import Relation.Binary
564
40ab3d39e49d using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 563
diff changeset
188
40ab3d39e49d using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 563
diff changeset
189 checkT : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool {m}
40ab3d39e49d using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 563
diff changeset
190 checkT Nothing _ = False
40ab3d39e49d using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 563
diff changeset
191 checkT (Just n) x with compTri (value n) x
40ab3d39e49d using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 563
diff changeset
192 ... | tri≈ _ _ _ = True
40ab3d39e49d using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 563
diff changeset
193 ... | _ = False
40ab3d39e49d using strict total order
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 563
diff changeset
194
565
ba7c5f1c2937 this slightly better
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 564
diff changeset
195 checkEQ : {m : Level } ( x : ℕ ) -> ( n : Node ℕ ℕ ) -> (value n ) ≡ x -> checkT {m} (Just n) x ≡ True
ba7c5f1c2937 this slightly better
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 564
diff changeset
196 checkEQ x n refl with compTri (value n) x
566
d9ef8333ff79 use ⊥-elim (neq refl)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 565
diff changeset
197 ... | tri≈ _ refl _ = refl
d9ef8333ff79 use ⊥-elim (neq refl)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 565
diff changeset
198 ... | tri> _ neq gt = ⊥-elim (neq refl)
d9ef8333ff79 use ⊥-elim (neq refl)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 565
diff changeset
199 ... | tri< lt neq _ = ⊥-elim (neq refl)
565
ba7c5f1c2937 this slightly better
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 564
diff changeset
200
566
d9ef8333ff79 use ⊥-elim (neq refl)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 565
diff changeset
201 checkEQ' : {m : Level } ( x y : ℕ ) -> ( eq : x ≡ y ) -> ( x ≟ y ) ≡ yes eq
d9ef8333ff79 use ⊥-elim (neq refl)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 565
diff changeset
202 checkEQ' x y refl with x ≟ y
d9ef8333ff79 use ⊥-elim (neq refl)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 565
diff changeset
203 ... | yes refl = refl
d9ef8333ff79 use ⊥-elim (neq refl)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 565
diff changeset
204 ... | no neq = ⊥-elim ( neq refl )
546
b654ce34c894 add putTest1Lemma1, putTest1
ryokka
parents: 545
diff changeset
205