|
138
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
70
|
2 module nat where
|
|
|
3
|
|
138
|
4 open import Data.Nat
|
|
|
5 open import Data.Nat.Properties
|
|
70
|
6 open import Data.Empty
|
|
|
7 open import Relation.Nullary
|
|
|
8 open import Relation.Binary.PropositionalEquality
|
|
138
|
9 open import Relation.Binary.Core
|
|
70
|
10 open import logic
|
|
|
11
|
|
|
12
|
|
138
|
13 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
|
|
70
|
14 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
|
|
|
15
|
|
138
|
16 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
|
|
83
|
17 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
|
|
|
18
|
|
138
|
19 nat-<≡ : { x : ℕ } → x < x → ⊥
|
|
70
|
20 nat-<≡ (s≤s lt) = nat-<≡ lt
|
|
|
21
|
|
138
|
22 nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
|
|
70
|
23 nat-≡< refl lt = nat-<≡ lt
|
|
|
24
|
|
138
|
25 ¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
|
|
70
|
26 ¬a≤a (s≤s lt) = ¬a≤a lt
|
|
|
27
|
|
138
|
28 a<sa : {la : ℕ} → la < suc la
|
|
|
29 a<sa {zero} = s≤s z≤n
|
|
|
30 a<sa {suc la} = s≤s a<sa
|
|
70
|
31
|
|
138
|
32 =→¬< : {x : ℕ } → ¬ ( x < x )
|
|
|
33 =→¬< {zero} ()
|
|
|
34 =→¬< {suc x} (s≤s lt) = =→¬< lt
|
|
70
|
35
|
|
138
|
36 >→¬< : {x y : ℕ } → (x < y ) → ¬ ( y < x )
|
|
70
|
37 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
|
|
|
38
|
|
138
|
39 <-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) )
|
|
|
40 <-∨ {zero} {zero} (s≤s z≤n) = case1 refl
|
|
|
41 <-∨ {zero} {suc y} (s≤s lt) = case2 (s≤s z≤n)
|
|
|
42 <-∨ {suc x} {zero} (s≤s ())
|
|
|
43 <-∨ {suc x} {suc y} (s≤s lt) with <-∨ {x} {y} lt
|
|
|
44 <-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq)
|
|
|
45 <-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
|
|
70
|
46
|
|
138
|
47 max : (x y : ℕ) → ℕ
|
|
|
48 max zero zero = zero
|
|
|
49 max zero (suc x) = (suc x)
|
|
|
50 max (suc x) zero = (suc x)
|
|
|
51 max (suc x) (suc y) = suc ( max x y )
|
|
70
|
52
|
|
138
|
53 -- _*_ : ℕ → ℕ → ℕ
|
|
70
|
54 -- _*_ zero _ = zero
|
|
|
55 -- _*_ (suc n) m = m + ( n * m )
|
|
|
56
|
|
138
|
57 exp : ℕ → ℕ → ℕ
|
|
|
58 exp _ zero = 1
|
|
|
59 exp n (suc m) = n * ( exp n m )
|
|
|
60
|
|
|
61 minus : (a b : ℕ ) → ℕ
|
|
|
62 minus a zero = a
|
|
|
63 minus zero (suc b) = zero
|
|
|
64 minus (suc a) (suc b) = minus a b
|
|
|
65
|
|
|
66 _-_ = minus
|
|
|
67
|
|
|
68 m+= : {i j m : ℕ } → m + i ≡ m + j → i ≡ j
|
|
|
69 m+= {i} {j} {zero} refl = refl
|
|
|
70 m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq )
|
|
|
71
|
|
|
72 +m= : {i j m : ℕ } → i + m ≡ j + m → i ≡ j
|
|
|
73 +m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq )
|
|
|
74
|
|
|
75 less-1 : { n m : ℕ } → suc n < m → n < m
|
|
|
76 less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n
|
|
|
77 less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt)
|
|
|
78
|
|
|
79 sa=b→a<b : { n m : ℕ } → suc n ≡ m → n < m
|
|
|
80 sa=b→a<b {0} {suc zero} refl = s≤s z≤n
|
|
|
81 sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl)
|
|
|
82
|
|
|
83 minus+n : {x y : ℕ } → suc x > y → minus x y + y ≡ x
|
|
|
84 minus+n {x} {zero} _ = trans (sym (+-comm zero _ )) refl
|
|
|
85 minus+n {zero} {suc y} (s≤s ())
|
|
|
86 minus+n {suc x} {suc y} (s≤s lt) = begin
|
|
|
87 minus (suc x) (suc y) + suc y
|
|
|
88 ≡⟨ +-comm _ (suc y) ⟩
|
|
|
89 suc y + minus x y
|
|
|
90 ≡⟨ cong ( λ k → suc k ) (
|
|
|
91 begin
|
|
|
92 y + minus x y
|
|
|
93 ≡⟨ +-comm y _ ⟩
|
|
|
94 minus x y + y
|
|
|
95 ≡⟨ minus+n {x} {y} lt ⟩
|
|
|
96 x
|
|
|
97 ∎
|
|
|
98 ) ⟩
|
|
|
99 suc x
|
|
|
100 ∎ where open ≡-Reasoning
|
|
|
101
|
|
|
102
|
|
|
103 -- open import Relation.Binary.PropositionalEquality
|
|
|
104
|
|
|
105 -- postulate extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n)
|
|
|
106
|
|
|
107 -- <-≡-iff : {A B : (a b : ℕ ) → Set } → {a b : ℕ } → (A a b → B a b ) → (B a b → A a b ) → A ≡ B
|
|
|
108 -- <-≡-iff {A} {B} ab ba = {!!}
|
|
|
109
|
|
|
110
|
|
|
111 0<s : {x : ℕ } → zero < suc x
|
|
|
112 0<s {_} = s≤s z≤n
|
|
|
113
|
|
|
114 <-minus-0 : {x y z : ℕ } → z + x < z + y → x < y
|
|
|
115 <-minus-0 {x} {suc _} {zero} lt = lt
|
|
|
116 <-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt
|
|
|
117
|
|
|
118 <-minus : {x y z : ℕ } → x + z < y + z → x < y
|
|
|
119 <-minus {x} {y} {z} lt = <-minus-0 ( subst₂ ( λ j k → j < k ) (+-comm x _) (+-comm y _ ) lt )
|
|
|
120
|
|
|
121 x≤x+y : {z y : ℕ } → z ≤ z + y
|
|
|
122 x≤x+y {zero} {y} = z≤n
|
|
|
123 x≤x+y {suc z} {y} = s≤s (x≤x+y {z} {y})
|
|
|
124
|
|
|
125 <-plus : {x y z : ℕ } → x < y → x + z < y + z
|
|
|
126 <-plus {zero} {suc y} {z} (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y )
|
|
|
127 <-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {x} {y} {z} lt)
|
|
|
128
|
|
|
129 <-plus-0 : {x y z : ℕ } → x < y → z + x < z + y
|
|
|
130 <-plus-0 {x} {y} {z} lt = subst₂ (λ j k → j < k ) (+-comm _ z) (+-comm _ z) ( <-plus {x} {y} {z} lt )
|
|
|
131
|
|
|
132 ≤-plus : {x y z : ℕ } → x ≤ y → x + z ≤ y + z
|
|
|
133 ≤-plus {0} {y} {zero} z≤n = z≤n
|
|
|
134 ≤-plus {0} {y} {suc z} z≤n = subst (λ k → z < k ) (+-comm _ y ) x≤x+y
|
|
|
135 ≤-plus {suc x} {suc y} {z} (s≤s lt) = s≤s ( ≤-plus {x} {y} {z} lt )
|
|
|
136
|
|
|
137 ≤-plus-0 : {x y z : ℕ } → x ≤ y → z + x ≤ z + y
|
|
|
138 ≤-plus-0 {x} {y} {zero} lt = lt
|
|
|
139 ≤-plus-0 {x} {y} {suc z} lt = s≤s ( ≤-plus-0 {x} {y} {z} lt )
|
|
|
140
|
|
|
141 x+y<z→x<z : {x y z : ℕ } → x + y < z → x < z
|
|
|
142 x+y<z→x<z {zero} {y} {suc z} (s≤s lt1) = s≤s z≤n
|
|
|
143 x+y<z→x<z {suc x} {y} {suc z} (s≤s lt1) = s≤s ( x+y<z→x<z {x} {y} {z} lt1 )
|
|
|
144
|
|
|
145 *≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z
|
|
|
146 *≤ lt = *-mono-≤ lt ≤-refl
|
|
|
147
|
|
|
148 *< : {x y z : ℕ } → x < y → x * suc z < y * suc z
|
|
|
149 *< {zero} {suc y} lt = s≤s z≤n
|
|
|
150 *< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt)
|
|
|
151
|
|
|
152 <to<s : {x y : ℕ } → x < y → x < suc y
|
|
|
153 <to<s {zero} {suc y} (s≤s lt) = s≤s z≤n
|
|
|
154 <to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt)
|
|
|
155
|
|
|
156 <tos<s : {x y : ℕ } → x < y → suc x < suc y
|
|
|
157 <tos<s {zero} {suc y} (s≤s z≤n) = s≤s (s≤s z≤n)
|
|
|
158 <tos<s {suc x} {suc y} (s≤s lt) = s≤s (<tos<s {x} {y} lt)
|
|
|
159
|
|
|
160 ≤to< : {x y : ℕ } → x < y → x ≤ y
|
|
|
161 ≤to< {zero} {suc y} (s≤s z≤n) = z≤n
|
|
|
162 ≤to< {suc x} {suc y} (s≤s lt) = s≤s (≤to< {x} {y} lt)
|
|
|
163
|
|
|
164 refl-≤s : {x : ℕ } → x ≤ suc x
|
|
|
165 refl-≤s {zero} = z≤n
|
|
|
166 refl-≤s {suc x} = s≤s (refl-≤s {x})
|
|
|
167
|
|
|
168 x<y→≤ : {x y : ℕ } → x < y → x ≤ suc y
|
|
|
169 x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n
|
|
|
170 x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt)
|
|
|
171
|
|
|
172 open import Data.Product
|
|
|
173
|
|
|
174 minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0
|
|
|
175 minus<=0 {0} {zero} z≤n = refl
|
|
|
176 minus<=0 {0} {suc y} z≤n = refl
|
|
|
177 minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le
|
|
|
178
|
|
|
179 minus>0 : {x y : ℕ } → x < y → 0 < minus y x
|
|
|
180 minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n
|
|
|
181 minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt
|
|
|
182
|
|
141
|
183 open import Relation.Binary.Definitions
|
|
|
184
|
|
138
|
185 distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z)
|
|
|
186 distr-minus-* {x} {zero} {z} = refl
|
|
|
187 distr-minus-* {x} {suc y} {z} with <-cmp x y
|
|
|
188 distr-minus-* {x} {suc y} {z} | tri< a ¬b ¬c = begin
|
|
|
189 minus x (suc y) * z
|
|
|
190 ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} (x<y→≤ a)) ⟩
|
|
|
191 0 * z
|
|
|
192 ≡⟨ sym (minus<=0 {x * z} {z + y * z} le ) ⟩
|
|
|
193 minus (x * z) (z + y * z)
|
|
|
194 ∎ where
|
|
|
195 open ≡-Reasoning
|
|
|
196 le : x * z ≤ z + y * z
|
|
|
197 le = ≤-trans lemma (subst (λ k → y * z ≤ k ) (+-comm _ z ) (x≤x+y {y * z} {z} ) ) where
|
|
|
198 lemma : x * z ≤ y * z
|
|
|
199 lemma = *≤ {x} {y} {z} (≤to< a)
|
|
|
200 distr-minus-* {x} {suc y} {z} | tri≈ ¬a refl ¬c = begin
|
|
|
201 minus x (suc y) * z
|
|
|
202 ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} refl-≤s ) ⟩
|
|
|
203 0 * z
|
|
|
204 ≡⟨ sym (minus<=0 {x * z} {z + y * z} (lt {x} {z} )) ⟩
|
|
|
205 minus (x * z) (z + y * z)
|
|
|
206 ∎ where
|
|
|
207 open ≡-Reasoning
|
|
|
208 lt : {x z : ℕ } → x * z ≤ z + x * z
|
|
|
209 lt {zero} {zero} = z≤n
|
|
|
210 lt {suc x} {zero} = lt {x} {zero}
|
|
|
211 lt {x} {suc z} = ≤-trans lemma refl-≤s where
|
|
|
212 lemma : x * suc z ≤ z + x * suc z
|
|
|
213 lemma = subst (λ k → x * suc z ≤ k ) (+-comm _ z) (x≤x+y {x * suc z} {z})
|
|
|
214 distr-minus-* {x} {suc y} {z} | tri> ¬a ¬b c = +m= {_} {_} {suc y * z} ( begin
|
|
|
215 minus x (suc y) * z + suc y * z
|
|
|
216 ≡⟨ sym (proj₂ *-distrib-+ z (minus x (suc y) ) _) ⟩
|
|
|
217 ( minus x (suc y) + suc y ) * z
|
|
|
218 ≡⟨ cong (λ k → k * z) (minus+n {x} {suc y} (s≤s c)) ⟩
|
|
|
219 x * z
|
|
|
220 ≡⟨ sym (minus+n {x * z} {suc y * z} (s≤s (lt c))) ⟩
|
|
|
221 minus (x * z) (suc y * z) + suc y * z
|
|
|
222 ∎ ) where
|
|
|
223 open ≡-Reasoning
|
|
|
224 lt : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z
|
|
|
225 lt {x} {y} {z} le = *≤ le
|
|
|
226
|
|
|
227 minus- : {x y z : ℕ } → suc x > z + y → minus (minus x y) z ≡ minus x (y + z)
|
|
|
228 minus- {x} {y} {z} gt = +m= {_} {_} {z} ( begin
|
|
|
229 minus (minus x y) z + z
|
|
|
230 ≡⟨ minus+n {_} {z} lemma ⟩
|
|
|
231 minus x y
|
|
|
232 ≡⟨ +m= {_} {_} {y} ( begin
|
|
|
233 minus x y + y
|
|
|
234 ≡⟨ minus+n {_} {y} lemma1 ⟩
|
|
|
235 x
|
|
|
236 ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩
|
|
|
237 minus x (z + y) + (z + y)
|
|
|
238 ≡⟨ sym ( +-assoc (minus x (z + y)) _ _ ) ⟩
|
|
|
239 minus x (z + y) + z + y
|
|
|
240 ∎ ) ⟩
|
|
|
241 minus x (z + y) + z
|
|
|
242 ≡⟨ cong (λ k → minus x k + z ) (+-comm _ y ) ⟩
|
|
|
243 minus x (y + z) + z
|
|
|
244 ∎ ) where
|
|
|
245 open ≡-Reasoning
|
|
|
246 lemma1 : suc x > y
|
|
|
247 lemma1 = x+y<z→x<z (subst (λ k → k < suc x ) (+-comm z _ ) gt )
|
|
|
248 lemma : suc (minus x y) > z
|
|
|
249 lemma = <-minus {_} {_} {y} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y} lemma1 )) gt )
|
|
|
250
|
|
|
251 minus-* : {M k n : ℕ } → n < k → minus k (suc n) * M ≡ minus (minus k n * M ) M
|
|
|
252 minus-* {zero} {k} {n} lt = begin
|
|
|
253 minus k (suc n) * zero
|
|
|
254 ≡⟨ *-comm (minus k (suc n)) zero ⟩
|
|
|
255 zero * minus k (suc n)
|
|
|
256 ≡⟨⟩
|
|
|
257 0 * minus k n
|
|
|
258 ≡⟨ *-comm 0 (minus k n) ⟩
|
|
|
259 minus (minus k n * 0 ) 0
|
|
|
260 ∎ where
|
|
|
261 open ≡-Reasoning
|
|
|
262 minus-* {suc m} {k} {n} lt with <-cmp k 1
|
|
|
263 minus-* {suc m} {.0} {zero} lt | tri< (s≤s z≤n) ¬b ¬c = refl
|
|
|
264 minus-* {suc m} {.0} {suc n} lt | tri< (s≤s z≤n) ¬b ¬c = refl
|
|
|
265 minus-* {suc zero} {.1} {zero} lt | tri≈ ¬a refl ¬c = refl
|
|
|
266 minus-* {suc (suc m)} {.1} {zero} lt | tri≈ ¬a refl ¬c = minus-* {suc m} {1} {zero} lt
|
|
|
267 minus-* {suc m} {.1} {suc n} (s≤s ()) | tri≈ ¬a refl ¬c
|
|
|
268 minus-* {suc m} {k} {n} lt | tri> ¬a ¬b c = begin
|
|
|
269 minus k (suc n) * M
|
|
|
270 ≡⟨ distr-minus-* {k} {suc n} {M} ⟩
|
|
|
271 minus (k * M ) ((suc n) * M)
|
|
|
272 ≡⟨⟩
|
|
|
273 minus (k * M ) (M + n * M )
|
|
|
274 ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩
|
|
|
275 minus (k * M ) ((n * M) + M )
|
|
|
276 ≡⟨ sym ( minus- {k * M} {n * M} (lemma lt) ) ⟩
|
|
|
277 minus (minus (k * M ) (n * M)) M
|
|
|
278 ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩
|
|
|
279 minus (minus k n * M ) M
|
|
|
280 ∎ where
|
|
|
281 M = suc m
|
|
|
282 lemma : {n k m : ℕ } → n < k → suc (k * suc m) > suc m + n * suc m
|
|
|
283 lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y ))
|
|
|
284 lemma {suc n} {suc k} {m} lt = begin
|
|
|
285 suc (suc m + suc n * suc m)
|
|
|
286 ≡⟨⟩
|
|
|
287 suc ( suc (suc n) * suc m)
|
|
|
288 ≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩
|
|
|
289 suc (suc k * suc m)
|
|
|
290 ∎ where open ≤-Reasoning
|
|
|
291 open ≡-Reasoning
|
