Mercurial > hg > Members > kono > Proof > galois

comparison src/nat.agda @ 255:6d1619d9f880

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
library
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 Jan 2021 10:18:08 +0900
parents nat.agda@2eb62a2a34f2
children 891869ead775
comparison
equal deleted inserted replaced
254:a5b3061f15ee 255:6d1619d9f880
1 {-# OPTIONS --allow-unsolved-metas #-}
2 module nat where
3
4 open import Data.Nat
5 open import Data.Nat.Properties
6 open import Data.Empty
7 open import Relation.Nullary
8 open import Relation.Binary.PropositionalEquality
9 open import Relation.Binary.Core
10 open import Relation.Binary.Definitions
11 open import logic
12
13
14 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
15 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
16
17 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
18 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
19
20 nat-<≡ : { x : ℕ } → x < x → ⊥
21 nat-<≡ (s≤s lt) = nat-<≡ lt
22
23 nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
24 nat-≡< refl lt = nat-<≡ lt
25
26 ¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
27 ¬a≤a (s≤s lt) = ¬a≤a lt
28
29 a<sa : {la : ℕ} → la < suc la
30 a<sa {zero} = s≤s z≤n
31 a<sa {suc la} = s≤s a<sa
32
33 refl-≤s : {x : ℕ } → x ≤ suc x
34 refl-≤s {zero} = z≤n
35 refl-≤s {suc x} = s≤s (refl-≤s {x})
36
37 a≤sa : {x : ℕ } → x ≤ suc x
38 a≤sa {zero} = z≤n
39 a≤sa {suc x} = s≤s (a≤sa {x})
40
41 =→¬< : {x : ℕ } → ¬ ( x < x )
42 =→¬< {zero} ()
43 =→¬< {suc x} (s≤s lt) = =→¬< lt
44
45 >→¬< : {x y : ℕ } → (x < y ) → ¬ ( y < x )
46 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
47
48 <-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) )
49 <-∨ {zero} {zero} (s≤s z≤n) = case1 refl
50 <-∨ {zero} {suc y} (s≤s lt) = case2 (s≤s z≤n)
51 <-∨ {suc x} {zero} (s≤s ())
52 <-∨ {suc x} {suc y} (s≤s lt) with <-∨ {x} {y} lt
53 <-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq)
54 <-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
55
56 n≤n : (n : ℕ) → n Data.Nat.≤ n
57 n≤n zero = z≤n
58 n≤n (suc n) = s≤s (n≤n n)
59
60 <→m≤n : {m n : ℕ} → m < n → m Data.Nat.≤ n
61 <→m≤n {zero} lt = z≤n
62 <→m≤n {suc m} {zero} ()
63 <→m≤n {suc m} {suc n} (s≤s lt) = s≤s (<→m≤n lt)
64
65 max : (x y : ℕ) → ℕ
66 max zero zero = zero
67 max zero (suc x) = (suc x)
68 max (suc x) zero = (suc x)
69 max (suc x) (suc y) = suc ( max x y )
70
71 -- _*_ : ℕ → ℕ → ℕ
72 -- _*_ zero _ = zero
73 -- _*_ (suc n) m = m + ( n * m )
74
75 exp : ℕ → ℕ → ℕ
76 exp _ zero = 1
77 exp n (suc m) = n * ( exp n m )
78
79 minus : (a b : ℕ ) → ℕ
80 minus a zero = a
81 minus zero (suc b) = zero
82 minus (suc a) (suc b) = minus a b
83
84 _-_ = minus
85
86 m+= : {i j m : ℕ } → m + i ≡ m + j → i ≡ j
87 m+= {i} {j} {zero} refl = refl
88 m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq )
89
90 +m= : {i j m : ℕ } → i + m ≡ j + m → i ≡ j
91 +m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq )
92
93 less-1 : { n m : ℕ } → suc n < m → n < m
94 less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n
95 less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt)
96
97 sa=b→a<b : { n m : ℕ } → suc n ≡ m → n < m
98 sa=b→a<b {0} {suc zero} refl = s≤s z≤n
99 sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl)
100
101 minus+n : {x y : ℕ } → suc x > y → minus x y + y ≡ x
102 minus+n {x} {zero} _ = trans (sym (+-comm zero _ )) refl
103 minus+n {zero} {suc y} (s≤s ())
104 minus+n {suc x} {suc y} (s≤s lt) = begin
105 minus (suc x) (suc y) + suc y
106 ≡⟨ +-comm _ (suc y) ⟩
107 suc y + minus x y
108 ≡⟨ cong ( λ k → suc k ) (
109 begin
110 y + minus x y
111 ≡⟨ +-comm y _ ⟩
112 minus x y + y
113 ≡⟨ minus+n {x} {y} lt ⟩
114 x
115 ∎
116 ) ⟩
117 suc x
118 ∎ where open ≡-Reasoning
119
120 sn-m=sn-m : {m n : ℕ } → m ≤ n → suc n - m ≡ suc ( n - m )
121 sn-m=sn-m {0} {n} z≤n = refl
122 sn-m=sn-m {suc m} {suc n} (s≤s m<n) = sn-m=sn-m m<n
123
124 si-sn=i-n : {i n : ℕ } → n < i → suc (i - suc n) ≡ (i - n)
125 si-sn=i-n {i} {n} n<i = begin
126 suc (i - suc n) ≡⟨ sym (sn-m=sn-m n<i ) ⟩
127 suc i - suc n ≡⟨⟩
128 i - n
129 ∎ where
130 open ≡-Reasoning
131
132 n-m<n : (n m : ℕ ) → n - m ≤ n
133 n-m<n zero zero = z≤n
134 n-m<n (suc n) zero = s≤s (n-m<n n zero)
135 n-m<n zero (suc m) = z≤n
136 n-m<n (suc n) (suc m) = ≤-trans (n-m<n n m ) refl-≤s
137
138 n-n-m=m : {m n : ℕ } → m ≤ n → m ≡ (n - (n - m))
139 n-n-m=m {0} {zero} z≤n = refl
140 n-n-m=m {0} {suc n} z≤n = n-n-m=m {0} {n} z≤n
141 n-n-m=m {suc m} {suc n} (s≤s m≤n) = sym ( begin
142 suc n - ( n - m ) ≡⟨ sn-m=sn-m (n-m<n n m) ⟩
143 suc (n - ( n - m )) ≡⟨ cong (λ k → suc k ) (sym (n-n-m=m m≤n)) ⟩
144 suc m
145 ∎ ) where
146 open ≡-Reasoning
147
148 0<s : {x : ℕ } → zero < suc x
149 0<s {_} = s≤s z≤n
150
151 <-minus-0 : {x y z : ℕ } → z + x < z + y → x < y
152 <-minus-0 {x} {suc _} {zero} lt = lt
153 <-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt
154
155 <-minus : {x y z : ℕ } → x + z < y + z → x < y
156 <-minus {x} {y} {z} lt = <-minus-0 ( subst₂ ( λ j k → j < k ) (+-comm x _) (+-comm y _ ) lt )
157
158 x≤x+y : {z y : ℕ } → z ≤ z + y
159 x≤x+y {zero} {y} = z≤n
160 x≤x+y {suc z} {y} = s≤s (x≤x+y {z} {y})
161
162 <-plus : {x y z : ℕ } → x < y → x + z < y + z
163 <-plus {zero} {suc y} {z} (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y )
164 <-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {x} {y} {z} lt)
165
166 <-plus-0 : {x y z : ℕ } → x < y → z + x < z + y
167 <-plus-0 {x} {y} {z} lt = subst₂ (λ j k → j < k ) (+-comm _ z) (+-comm _ z) ( <-plus {x} {y} {z} lt )
168
169 ≤-plus : {x y z : ℕ } → x ≤ y → x + z ≤ y + z
170 ≤-plus {0} {y} {zero} z≤n = z≤n
171 ≤-plus {0} {y} {suc z} z≤n = subst (λ k → z < k ) (+-comm _ y ) x≤x+y
172 ≤-plus {suc x} {suc y} {z} (s≤s lt) = s≤s ( ≤-plus {x} {y} {z} lt )
173
174 ≤-plus-0 : {x y z : ℕ } → x ≤ y → z + x ≤ z + y
175 ≤-plus-0 {x} {y} {zero} lt = lt
176 ≤-plus-0 {x} {y} {suc z} lt = s≤s ( ≤-plus-0 {x} {y} {z} lt )
177
178 x+y<z→x<z : {x y z : ℕ } → x + y < z → x < z
179 x+y<z→x<z {zero} {y} {suc z} (s≤s lt1) = s≤s z≤n
180 x+y<z→x<z {suc x} {y} {suc z} (s≤s lt1) = s≤s ( x+y<z→x<z {x} {y} {z} lt1 )
181
182 *≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z
183 *≤ lt = *-mono-≤ lt ≤-refl
184
185 *< : {x y z : ℕ } → x < y → x * suc z < y * suc z
186 *< {zero} {suc y} lt = s≤s z≤n
187 *< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt)
188
189 <to<s : {x y : ℕ } → x < y → x < suc y
190 <to<s {zero} {suc y} (s≤s lt) = s≤s z≤n
191 <to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt)
192
193 <tos<s : {x y : ℕ } → x < y → suc x < suc y
194 <tos<s {zero} {suc y} (s≤s z≤n) = s≤s (s≤s z≤n)
195 <tos<s {suc x} {suc y} (s≤s lt) = s≤s (<tos<s {x} {y} lt)
196
197 ≤to< : {x y : ℕ } → x < y → x ≤ y
198 ≤to< {zero} {suc y} (s≤s z≤n) = z≤n
199 ≤to< {suc x} {suc y} (s≤s lt) = s≤s (≤to< {x} {y} lt)
200
201 x<y→≤ : {x y : ℕ } → x < y → x ≤ suc y
202 x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n
203 x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt)
204
205 open import Data.Product
206
207 minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0
208 minus<=0 {0} {zero} z≤n = refl
209 minus<=0 {0} {suc y} z≤n = refl
210 minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le
211
212 minus>0 : {x y : ℕ } → x < y → 0 < minus y x
213 minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n
214 minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt
215
216 distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z)
217 distr-minus-* {x} {zero} {z} = refl
218 distr-minus-* {x} {suc y} {z} with <-cmp x y
219 distr-minus-* {x} {suc y} {z} | tri< a ¬b ¬c = begin
220 minus x (suc y) * z
221 ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} (x<y→≤ a)) ⟩
222 0 * z
223 ≡⟨ sym (minus<=0 {x * z} {z + y * z} le ) ⟩
224 minus (x * z) (z + y * z)
225 ∎ where
226 open ≡-Reasoning
227 le : x * z ≤ z + y * z
228 le = ≤-trans lemma (subst (λ k → y * z ≤ k ) (+-comm _ z ) (x≤x+y {y * z} {z} ) ) where
229 lemma : x * z ≤ y * z
230 lemma = *≤ {x} {y} {z} (≤to< a)
231 distr-minus-* {x} {suc y} {z} | tri≈ ¬a refl ¬c = begin
232 minus x (suc y) * z
233 ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} refl-≤s ) ⟩
234 0 * z
235 ≡⟨ sym (minus<=0 {x * z} {z + y * z} (lt {x} {z} )) ⟩
236 minus (x * z) (z + y * z)
237 ∎ where
238 open ≡-Reasoning
239 lt : {x z : ℕ } → x * z ≤ z + x * z
240 lt {zero} {zero} = z≤n
241 lt {suc x} {zero} = lt {x} {zero}
242 lt {x} {suc z} = ≤-trans lemma refl-≤s where
243 lemma : x * suc z ≤ z + x * suc z
244 lemma = subst (λ k → x * suc z ≤ k ) (+-comm _ z) (x≤x+y {x * suc z} {z})
245 distr-minus-* {x} {suc y} {z} | tri> ¬a ¬b c = +m= {_} {_} {suc y * z} ( begin
246 minus x (suc y) * z + suc y * z
247 ≡⟨ sym (proj₂ *-distrib-+ z (minus x (suc y) ) _) ⟩
248 ( minus x (suc y) + suc y ) * z
249 ≡⟨ cong (λ k → k * z) (minus+n {x} {suc y} (s≤s c)) ⟩
250 x * z
251 ≡⟨ sym (minus+n {x * z} {suc y * z} (s≤s (lt c))) ⟩
252 minus (x * z) (suc y * z) + suc y * z
253 ∎ ) where
254 open ≡-Reasoning
255 lt : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z
256 lt {x} {y} {z} le = *≤ le
257
258 minus- : {x y z : ℕ } → suc x > z + y → minus (minus x y) z ≡ minus x (y + z)
259 minus- {x} {y} {z} gt = +m= {_} {_} {z} ( begin
260 minus (minus x y) z + z
261 ≡⟨ minus+n {_} {z} lemma ⟩
262 minus x y
263 ≡⟨ +m= {_} {_} {y} ( begin
264 minus x y + y
265 ≡⟨ minus+n {_} {y} lemma1 ⟩
266 x
267 ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩
268 minus x (z + y) + (z + y)
269 ≡⟨ sym ( +-assoc (minus x (z + y)) _ _ ) ⟩
270 minus x (z + y) + z + y
271 ∎ ) ⟩
272 minus x (z + y) + z
273 ≡⟨ cong (λ k → minus x k + z ) (+-comm _ y ) ⟩
274 minus x (y + z) + z
275 ∎ ) where
276 open ≡-Reasoning
277 lemma1 : suc x > y
278 lemma1 = x+y<z→x<z (subst (λ k → k < suc x ) (+-comm z _ ) gt )
279 lemma : suc (minus x y) > z
280 lemma = <-minus {_} {_} {y} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y} lemma1 )) gt )
281
282 minus-* : {M k n : ℕ } → n < k → minus k (suc n) * M ≡ minus (minus k n * M ) M
283 minus-* {zero} {k} {n} lt = begin
284 minus k (suc n) * zero
285 ≡⟨ *-comm (minus k (suc n)) zero ⟩
286 zero * minus k (suc n)
287 ≡⟨⟩
288 0 * minus k n
289 ≡⟨ *-comm 0 (minus k n) ⟩
290 minus (minus k n * 0 ) 0
291 ∎ where
292 open ≡-Reasoning
293 minus-* {suc m} {k} {n} lt with <-cmp k 1
294 minus-* {suc m} {.0} {zero} lt | tri< (s≤s z≤n) ¬b ¬c = refl
295 minus-* {suc m} {.0} {suc n} lt | tri< (s≤s z≤n) ¬b ¬c = refl
296 minus-* {suc zero} {.1} {zero} lt | tri≈ ¬a refl ¬c = refl
297 minus-* {suc (suc m)} {.1} {zero} lt | tri≈ ¬a refl ¬c = minus-* {suc m} {1} {zero} lt
298 minus-* {suc m} {.1} {suc n} (s≤s ()) | tri≈ ¬a refl ¬c
299 minus-* {suc m} {k} {n} lt | tri> ¬a ¬b c = begin
300 minus k (suc n) * M
301 ≡⟨ distr-minus-* {k} {suc n} {M} ⟩
302 minus (k * M ) ((suc n) * M)
303 ≡⟨⟩
304 minus (k * M ) (M + n * M )
305 ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩
306 minus (k * M ) ((n * M) + M )
307 ≡⟨ sym ( minus- {k * M} {n * M} (lemma lt) ) ⟩
308 minus (minus (k * M ) (n * M)) M
309 ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩
310 minus (minus k n * M ) M
311 ∎ where
312 M = suc m
313 lemma : {n k m : ℕ } → n < k → suc (k * suc m) > suc m + n * suc m
314 lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y ))
315 lemma {suc n} {suc k} {m} lt = begin
316 suc (suc m + suc n * suc m)
317 ≡⟨⟩
318 suc ( suc (suc n) * suc m)
319 ≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩
320 suc (suc k * suc m)
321 ∎ where open ≤-Reasoning
322 open ≡-Reasoning
323
324 open import Data.List
325
326 ℕL-inject : {h h1 : ℕ } {x y : List ℕ } → h ∷ x ≡ h1 ∷ y → h ≡ h1
327 ℕL-inject refl = refl
328
329 ℕL-inject-t : {h h1 : ℕ } {x y : List ℕ } → h ∷ x ≡ h1 ∷ y → x ≡ y
330 ℕL-inject-t refl = refl
331
332 ℕL-eq? : (x y : List ℕ ) → Dec (x ≡ y )
333 ℕL-eq? [] [] = yes refl
334 ℕL-eq? [] (x ∷ y) = no (λ ())
335 ℕL-eq? (x ∷ x₁) [] = no (λ ())
336 ℕL-eq? (h ∷ x) (h1 ∷ y) with h ≟ h1 | ℕL-eq? x y
337 ... | yes y1 | yes y2 = yes ( cong₂ (λ j k → j ∷ k ) y1 y2 )
338 ... | yes y1 | no n = no (λ e → n (ℕL-inject-t e))
339 ... | no n | t = no (λ e → n (ℕL-inject e))
340