Mercurial > hg > Gears > GearsAgda

comparison etc/trichotomos-ex.agda @ 569:f24a73245f36

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate trichotomos exercise
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 17 Apr 2018 10:14:16 +0900
parents redBlackTreeTest.agda@a5ba292e4081
children 0b791ae19543
comparison
equal deleted inserted replaced
568:a5ba292e4081 569:f24a73245f36
1 module trichotomos-ex where
2
3 open import Level hiding (zero) renaming ( suc to succ )
4 open import Data.Empty
5 open import Data.Nat
6 open import Relation.Nullary
7 open import Algebra
8 open import Data.Nat.Properties as NatProp
9 open import Relation.Binary
10 open import Relation.Binary.PropositionalEquality
11 open import Relation.Binary.Core
12 open import Function
13
14 data Bool {n : Level } : Set n where
15 True : Bool
16 False : Bool
17
18 record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
19 field
20 pi1 : a
21 pi2 : b
22
23 data _∨_ {n : Level } (a : Set n) (b : Set n): Set n where
24 pi1 : a -> a ∨ b
25 pi2 : b -> a ∨ b
26
27
28 data Maybe {n : Level } (a : Set n) : Set n where
29 Nothing : Maybe a
30 Just : a -> Maybe a
31
32 data Color {n : Level } : Set n where
33 Red : Color
34 Black : Color
35
36 data CompareResult {n : Level } : Set n where
37 LT : CompareResult
38 GT : CompareResult
39 EQ : CompareResult
40
41 record Node {n : Level } (a k : Set n) : Set n where
42 inductive
43 field
44 key : k
45 value : a
46 right : Maybe (Node a k)
47 left : Maybe (Node a k)
48 color : Color {n}
49 open Node
50
51 compareℕ : ℕ → ℕ → CompareResult {Level.zero}
52 compareℕ x y with Data.Nat.compare x y
53 ... | less _ _ = LT
54 ... | equal _ = EQ
55 ... | greater _ _ = GT
56
57 compareT : ℕ → ℕ → CompareResult {Level.zero}
58 compareT x y with IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder) x y
59 ... | tri≈ _ _ _ = EQ
60 ... | tri< _ _ _ = LT
61 ... | tri> _ _ _ = GT
62
63
64 compare2 : (x y : ℕ ) → CompareResult {Level.zero}
65 compare2 zero zero = EQ
66 compare2 (suc _) zero = GT
67 compare2 zero (suc _) = LT
68 compare2 (suc x) (suc y) = compare2 x y
69
70 contraposition : {m : Level } {A B : Set m} → (B → A) → (¬ A → ¬ B)
71 contraposition f = λ x y → x (f y)
72
73 compareTri1 : (n : ℕ) → zero <′ suc n
74 compareTri1 zero = ≤′-refl
75 compareTri1 (suc n) = ≤′-step ( compareTri1 n )
76
77 compareTri2 : (n m : ℕ) → n ≤′ m → suc n ≤′ suc m
78 compareTri2 _ _ ≤′-refl = ≤′-refl
79 compareTri2 n (suc m) ( ≤′-step p ) = ≤′-step { suc n } ( compareTri2 n m p )
80
81 <′dec : Set
82 <′dec = ∀ m n → Dec ( m ≤′ n )
83
84 compareTri6 : ∀ m {n} → ¬ m ≤′ n → ¬ suc m ≤′ suc n
85
86 is≤′ : <′dec
87 is≤′ zero zero = yes ≤′-refl
88 is≤′ zero (suc n) = yes (lemma n)
89 where
90 lemma : (n : ℕ) → zero ≤′ suc n
91 lemma zero = ≤′-step ≤′-refl
92 lemma (suc n) = ≤′-step (lemma n)
93 is≤′ (suc m) (zero) = no ( λ () )
94 is≤′ (suc m) (suc n) with is≤′ m n
95 ... | yes p = yes ( compareTri2 _ _ p )
96 ... | no p = no ( compareTri6 _ p )
97
98 compareTri20 : {n : ℕ} → ¬ suc n ≤′ zero
99 compareTri20 ()
100
101
102 compareTri21 : (n m : ℕ) → suc n ≤′ suc m → n ≤′ m
103 compareTri21 _ _ ≤′-refl = ≤′-refl
104 compareTri21 (suc n) zero ( ≤′-step p ) = compareTri23 (suc n) ( ≤′-step p ) p
105 where
106 compareTri23 : (n : ℕ) → suc n ≤′ suc zero → suc n ≤′ zero → n ≤′ zero
107 compareTri23 zero ( ≤′-step p ) _ = ≤′-refl
108 compareTri23 zero ≤′-refl _ = ≤′-refl
109 compareTri23 (suc n1) ( ≤′-step p ) ()
110 compareTri21 n (suc m) ( ≤′-step p ) = ≤′-step (compareTri21 _ _ p)
111 compareTri21 zero zero ( ≤′-step p ) = ≤′-refl
112
113
114 compareTri3 : ∀ m {n} → ¬ m ≡ suc (m + n)
115 compareTri3 zero ()
116 compareTri3 (suc m) eq = compareTri3 m (cong pred eq)
117
118 compareTri4' : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
119 compareTri4' m {n} with n ≟ m
120 ... | yes refl = λ x y → x refl
121 ... | no p = λ x y → p ( cong pred y )
122
123 compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
124 compareTri4 m = contraposition ( λ x → cong pred x )
125
126 -- compareTri6 : ∀ m {n} → ¬ m ≤′ n → ¬ suc m ≤′ suc n
127 compareTri6 m {n} = λ x y → x (compareTri21 _ _ y)
128
129 compareTri5 : ∀ m {n} → ¬ m <′ n → ¬ suc m <′ suc n
130 compareTri5 m {n} = compareTri6 (suc m)
131
132 compareTri : Trichotomous _≡_ _<′_
133 compareTri zero zero = tri≈ ( λ ()) refl ( λ ())
134 compareTri zero (suc n) = tri< ( compareTri1 n ) ( λ ()) ( λ ())
135 compareTri (suc n) zero = tri> ( λ ()) ( λ ()) ( compareTri1 n )
136 compareTri (suc n) (suc m) with compareTri n m
137 ... | tri< p q r = tri< (compareTri2 (suc n) m p ) (compareTri4 _ q) ( compareTri5 _ r )
138 ... | tri≈ p refl r = tri≈ (compareTri5 _ p) refl ( compareTri5 _ r )
139 ... | tri> p q r = tri> ( compareTri5 _ p ) (compareTri4 _ q) (compareTri2 (suc m) n r )
140
141 compareDecTest : (n n1 : Node ℕ ℕ) → ( key n ≡ key n1 ) ∨ ( ¬ key n ≡ key n1 )
142 compareDecTest n n1 with (key n) ≟ (key n1)
143 ... | yes p = pi1 p
144 ... | no ¬p = pi2 ¬p
145
146
147 putTest1Lemma2 : (k : ℕ) → compare2 k k ≡ EQ
148 putTest1Lemma2 zero = refl
149 putTest1Lemma2 (suc k) = putTest1Lemma2 k
150
151 putTest1Lemma1 : (x y : ℕ) → compareℕ x y ≡ compare2 x y
152 putTest1Lemma1 zero zero = refl
153 putTest1Lemma1 (suc m) zero = refl
154 putTest1Lemma1 zero (suc n) = refl
155 putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n
156 putTest1Lemma1 (suc .m) (suc .(Data.Nat.suc m + k)) | less m k = lemma1 m
157 where
158 lemma1 : (m : ℕ) → LT ≡ compare2 m (ℕ.suc (m + k))
159 lemma1 zero = refl
160 lemma1 (suc y) = lemma1 y
161 putTest1Lemma1 (suc .m) (suc .m) | equal m = lemma1 m
162 where
163 lemma1 : (m : ℕ) → EQ ≡ compare2 m m
164 lemma1 zero = refl
165 lemma1 (suc y) = lemma1 y
166 putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m) | greater m k = lemma1 m
167 where
168 lemma1 : (m : ℕ) → GT ≡ compare2 (ℕ.suc (m + k)) m
169 lemma1 zero = refl
170 lemma1 (suc y) = lemma1 y
171
172 putTest1Lemma3 : (k : ℕ) → compareℕ k k ≡ EQ
173 putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k )
174
175 compareLemma1 : {x y : ℕ} → compare2 x y ≡ EQ → x ≡ y
176 compareLemma1 {zero} {zero} refl = refl
177 compareLemma1 {zero} {suc _} ()
178 compareLemma1 {suc _} {zero} ()
179 compareLemma1 {suc x} {suc y} eq = cong ( λ z → ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
180 where
181 lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
182 lemma2 = refl
183
184
185 compTri : ( x y : ℕ ) -> Tri (x < y) ( x ≡ y ) ( x > y )
186 compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder)
187 where open import Relation.Binary
188
189 checkT : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool {m}
190 checkT Nothing _ = False
191 checkT (Just n) x with compTri (value n) x
192 ... | tri≈ _ _ _ = True
193 ... | _ = False
194
195 checkEQ : {m : Level } ( x : ℕ ) -> ( n : Node ℕ ℕ ) -> (value n ) ≡ x -> checkT {m} (Just n) x ≡ True
196 checkEQ x n refl with compTri (value n) x
197 ... | tri≈ _ refl _ = refl
198 ... | tri> _ neq gt = ⊥-elim (neq refl)
199 ... | tri< lt neq _ = ⊥-elim (neq refl)
200
201 checkEQ' : {m : Level } ( x y : ℕ ) -> ( eq : x ≡ y ) -> ( x ≟ y ) ≡ yes eq
202 checkEQ' x y refl with x ≟ y
203 ... | yes refl = refl
204 ... | no neq = ⊥-elim ( neq refl )
205