|
949
|
1 {-# OPTIONS --cubical-compatible --safe #-}
|
|
|
2
|
|
|
3 module nat where
|
|
|
4
|
|
|
5 open import Data.Nat
|
|
|
6 open import Data.Nat.Properties
|
|
|
7 open import Data.Empty
|
|
|
8 open import Relation.Nullary
|
|
|
9 open import Relation.Binary.PropositionalEquality
|
|
|
10 open import Relation.Binary.Core
|
|
|
11 open import Relation.Binary.Definitions
|
|
|
12 open import logic
|
|
|
13 open import Level hiding ( zero ; suc )
|
|
|
14
|
|
|
15 =→¬< : {x : ℕ } → ¬ ( x < x )
|
|
|
16 =→¬< {x} x<x with <-cmp x x
|
|
|
17 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
|
|
|
18 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a x<x )
|
|
|
19 ... | tri> ¬a ¬b c = ⊥-elim ( ¬b refl )
|
|
|
20
|
|
|
21 >→¬< : {x y : ℕ } → (x < y ) → ¬ ( y < x )
|
|
|
22 >→¬< {x} {y} x<y y<x with <-cmp x y
|
|
|
23 ... | tri< a ¬b ¬c = ⊥-elim ( ¬c y<x )
|
|
|
24 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c y<x )
|
|
|
25 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a x<y )
|
|
|
26
|
|
|
27 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
|
|
|
28 nat-<> {x} {y} x<y y<x with <-cmp x y
|
|
|
29 ... | tri< a ¬b ¬c = ⊥-elim ( ¬c y<x )
|
|
|
30 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c y<x )
|
|
|
31 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a x<y )
|
|
|
32
|
|
|
33 a<sa : {la : ℕ} → la < suc la
|
|
|
34 a<sa {zero} = s≤s z≤n
|
|
|
35 a<sa {suc la} = s≤s a<sa
|
|
|
36
|
|
|
37 refl-≤s : {x : ℕ } → x ≤ suc x
|
|
|
38 refl-≤s {zero} = z≤n
|
|
|
39 refl-≤s {suc x} = s≤s (refl-≤s {x})
|
|
|
40
|
|
|
41 a≤sa : {x : ℕ } → x ≤ suc x
|
|
|
42 a≤sa = refl-≤s
|
|
|
43
|
|
|
44 nat-<≡ : { x : ℕ } → x < x → ⊥
|
|
|
45 nat-<≡ {x} x<x with <-cmp x x
|
|
|
46 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
|
|
|
47 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a x<x )
|
|
|
48 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a x<x )
|
|
|
49
|
|
|
50 nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
|
|
|
51 nat-≡< refl lt = nat-<≡ lt
|
|
|
52
|
|
|
53 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
|
|
|
54 nat-≤> {x} {y} x≤y y<x with <-cmp x y
|
|
|
55 ... | tri< a ¬b ¬c = ⊥-elim ( ¬c y<x )
|
|
|
56 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c y<x )
|
|
|
57 ... | tri> ¬a ¬b c = ⊥-elim (nat-<≡ (≤-trans c x≤y))
|
|
|
58
|
|
|
59 ≤-∨ : { x y : ℕ } → x ≤ y → ( (x ≡ y ) ∨ (x < y) )
|
|
|
60 ≤-∨ {x} {y} x≤y with <-cmp x y
|
|
|
61 ... | tri< a ¬b ¬c = case2 a
|
|
|
62 ... | tri≈ ¬a b ¬c = case1 b
|
|
|
63 ... | tri> ¬a ¬b c = ⊥-elim ( nat-<≡ (≤-trans c x≤y))
|
|
|
64
|
|
|
65 <-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) )
|
|
|
66 <-∨ {x} {y} x<sy with <-cmp x y
|
|
|
67 ... | tri< a ¬b ¬c = case2 a
|
|
|
68 ... | tri≈ ¬a b ¬c = case1 b
|
|
|
69 ... | tri> ¬a ¬b c = ⊥-elim ( nat-<≡ (≤-trans x<sy c ))
|
|
|
70
|
|
|
71 ¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
|
|
|
72 ¬a≤a {x} sx≤x = ⊥-elim ( nat-≤> sx≤x a<sa )
|
|
|
73
|
|
|
74 max : (x y : ℕ) → ℕ
|
|
|
75 max zero zero = zero
|
|
|
76 max zero (suc x) = (suc x)
|
|
|
77 max (suc x) zero = (suc x)
|
|
|
78 max (suc x) (suc y) = suc ( max x y )
|
|
|
79
|
|
|
80 x≤max : (x y : ℕ) → x ≤ max x y
|
|
|
81 x≤max zero zero = ≤-refl
|
|
|
82 x≤max zero (suc x) = z≤n
|
|
|
83 x≤max (suc x) zero = ≤-refl
|
|
|
84 x≤max (suc x) (suc y) = s≤s( x≤max x y )
|
|
|
85
|
|
|
86 y≤max : (x y : ℕ) → y ≤ max x y
|
|
|
87 y≤max zero zero = ≤-refl
|
|
|
88 y≤max zero (suc x) = ≤-refl
|
|
|
89 y≤max (suc x) zero = z≤n
|
|
|
90 y≤max (suc x) (suc y) = s≤s( y≤max x y )
|
|
|
91
|
|
|
92 x≤y→max=y : (x y : ℕ) → x ≤ y → max x y ≡ y
|
|
|
93 x≤y→max=y zero zero x≤y = refl
|
|
|
94 x≤y→max=y zero (suc y) x≤y = refl
|
|
|
95 x≤y→max=y (suc x) (suc y) lt with <-cmp x y
|
|
|
96 ... | tri< a ¬b ¬c = cong suc (x≤y→max=y x y (≤-trans a≤sa a))
|
|
|
97 ... | tri≈ ¬a refl ¬c = cong suc (x≤y→max=y x y ≤-refl )
|
|
|
98 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c lt )
|
|
|
99
|
|
|
100 y≤x→max=x : (x y : ℕ) → y ≤ x → max x y ≡ x
|
|
|
101 y≤x→max=x zero zero y≤x = refl
|
|
|
102 y≤x→max=x zero (suc y) ()
|
|
|
103 y≤x→max=x (suc x) zero lt = refl
|
|
|
104 y≤x→max=x (suc x) (suc y) lt with <-cmp y x
|
|
|
105 ... | tri< a ¬b ¬c = cong suc (y≤x→max=x x y (≤-trans a≤sa a))
|
|
|
106 ... | tri≈ ¬a refl ¬c = cong suc (y≤x→max=x x y ≤-refl )
|
|
|
107 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c lt )
|
|
|
108
|
|
|
109
|
|
|
110 -- _*_ : ℕ → ℕ → ℕ
|
|
|
111 -- _*_ zero _ = zero
|
|
|
112 -- _*_ (suc n) m = m + ( n * m )
|
|
|
113
|
|
|
114 -- x ^ y
|
|
|
115 exp : ℕ → ℕ → ℕ
|
|
|
116 exp _ zero = 1
|
|
|
117 exp n (suc m) = n * ( exp n m )
|
|
|
118
|
|
|
119 div2 : ℕ → (ℕ ∧ Bool )
|
|
|
120 div2 zero = ⟪ 0 , false ⟫
|
|
|
121 div2 (suc zero) = ⟪ 0 , true ⟫
|
|
|
122 div2 (suc (suc n)) = ⟪ suc (proj1 (div2 n)) , proj2 (div2 n) ⟫ where
|
|
|
123 open _∧_
|
|
|
124
|
|
|
125 div2-rev : (ℕ ∧ Bool ) → ℕ
|
|
|
126 div2-rev ⟪ x , true ⟫ = suc (x + x)
|
|
|
127 div2-rev ⟪ x , false ⟫ = x + x
|
|
|
128
|
|
|
129 div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ x
|
|
|
130 div2-eq zero = refl
|
|
|
131 div2-eq (suc zero) = refl
|
|
|
132 div2-eq (suc (suc x)) with div2 x in eq1
|
|
|
133 ... | ⟪ x1 , true ⟫ = begin -- eq1 : div2 x ≡ ⟪ x1 , true ⟫
|
|
|
134 div2-rev ⟪ suc x1 , true ⟫ ≡⟨⟩
|
|
|
135 suc (suc (x1 + suc x1)) ≡⟨ cong (λ k → suc (suc k )) (+-comm x1 _ ) ⟩
|
|
|
136 suc (suc (suc (x1 + x1))) ≡⟨⟩
|
|
|
137 suc (suc (div2-rev ⟪ x1 , true ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩
|
|
|
138 suc (suc (div2-rev (div2 x))) ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩
|
|
|
139 suc (suc x) ∎ where open ≡-Reasoning
|
|
|
140 ... | ⟪ x1 , false ⟫ = begin
|
|
|
141 div2-rev ⟪ suc x1 , false ⟫ ≡⟨⟩
|
|
|
142 suc (x1 + suc x1) ≡⟨ cong (λ k → (suc k )) (+-comm x1 _ ) ⟩
|
|
|
143 suc (suc (x1 + x1)) ≡⟨⟩
|
|
|
144 suc (suc (div2-rev ⟪ x1 , false ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩
|
|
|
145 suc (suc (div2-rev (div2 x))) ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩
|
|
|
146 suc (suc x) ∎ where open ≡-Reasoning
|
|
|
147
|
|
|
148 sucprd : {i : ℕ } → 0 < i → suc (pred i) ≡ i
|
|
|
149 sucprd {suc i} 0<i = refl
|
|
|
150
|
|
|
151 0<s : {x : ℕ } → zero < suc x
|
|
|
152 0<s {_} = s≤s z≤n
|
|
|
153
|
|
|
154 px<py : {x y : ℕ } → pred x < pred y → x < y
|
|
|
155 px<py {zero} {suc y} lt = 0<s
|
|
|
156 px<py {suc x} {suc y} lt with <-cmp x y
|
|
|
157 ... | tri< a ¬b ¬c = s≤s a
|
|
|
158 ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b lt )
|
|
|
159 ... | tri> ¬a ¬b c = ⊥-elim ( nat-<> c lt )
|
|
|
160
|
|
|
161 minus : (a b : ℕ ) → ℕ
|
|
|
162 minus a zero = a
|
|
|
163 minus zero (suc b) = zero
|
|
|
164 minus (suc a) (suc b) = minus a b
|
|
|
165
|
|
|
166 _-_ = minus
|
|
|
167
|
|
|
168 sn-m=sn-m : {m n : ℕ } → m ≤ n → suc n - m ≡ suc ( n - m )
|
|
|
169 sn-m=sn-m {0} {n} m≤n = refl
|
|
|
170 sn-m=sn-m {suc m} {suc n} le with <-cmp m n
|
|
|
171 ... | tri< a ¬b ¬c = sm00 where
|
|
|
172 sm00 : suc n - m ≡ suc ( n - m )
|
|
|
173 sm00 = sn-m=sn-m {m} {n} (≤-trans a≤sa a )
|
|
|
174 ... | tri≈ ¬a refl ¬c = sn-m=sn-m {m} {n} ≤-refl
|
|
|
175 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c le )
|
|
|
176
|
|
|
177 si-sn=i-n : {i n : ℕ } → n < i → suc (i - suc n) ≡ (i - n)
|
|
|
178 si-sn=i-n {i} {n} n<i = begin
|
|
|
179 suc (i - suc n) ≡⟨ sym (sn-m=sn-m n<i ) ⟩
|
|
|
180 suc i - suc n ≡⟨⟩
|
|
|
181 i - n
|
|
|
182 ∎ where
|
|
|
183 open ≡-Reasoning
|
|
|
184
|
|
|
185 n-m<n : (n m : ℕ ) → n - m ≤ n
|
|
|
186 n-m<n zero zero = z≤n
|
|
|
187 n-m<n (suc n) zero = s≤s (n-m<n n zero)
|
|
|
188 n-m<n zero (suc m) = z≤n
|
|
|
189 n-m<n (suc n) (suc m) = ≤-trans (n-m<n n m ) refl-≤s
|
|
|
190
|
|
|
191 m-0=m : {m : ℕ } → m - zero ≡ m
|
|
|
192 m-0=m {zero} = refl
|
|
|
193 m-0=m {suc m} = cong suc (m-0=m {m})
|
|
|
194
|
|
|
195 m-m=0 : {m : ℕ } → m - m ≡ zero
|
|
|
196 m-m=0 {zero} = refl
|
|
|
197 m-m=0 {suc m} = m-m=0 {m}
|
|
|
198
|
|
|
199 refl-≤ : {x : ℕ } → x ≤ x
|
|
|
200 refl-≤ {zero} = z≤n
|
|
|
201 refl-≤ {suc x} = s≤s (refl-≤ {x})
|
|
|
202
|
|
|
203 refl-≤≡ : {x y : ℕ } → x ≡ y → x ≤ y
|
|
|
204 refl-≤≡ refl = refl-≤
|
|
|
205
|
|
|
206 px≤x : {x : ℕ } → pred x ≤ x
|
|
|
207 px≤x {zero} = refl-≤
|
|
|
208 px≤x {suc x} = refl-≤s
|
|
|
209
|
|
|
210 px≤py : {x y : ℕ } → x ≤ y → pred x ≤ pred y
|
|
|
211 px≤py {zero} {zero} x≤y = refl-≤
|
|
|
212 px≤py {suc x} {zero} ()
|
|
|
213 px≤py {zero} {suc y} le = z≤n
|
|
|
214 px≤py {suc x} {suc y} x≤y with <-cmp x y
|
|
|
215 ... | tri< a ¬b ¬c = ≤-trans a≤sa a
|
|
|
216 ... | tri≈ ¬a b ¬c = refl-≤≡ b
|
|
|
217 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c x≤y )
|
|
|
218
|
|
|
219 n-n-m=m : {m n : ℕ } → m ≤ n → m ≡ (n - (n - m))
|
|
|
220 n-n-m=m {0} {zero} le = refl
|
|
|
221 n-n-m=m {0} {suc n} lt = begin
|
|
|
222 0 ≡⟨ sym (m-m=0 {suc n}) ⟩
|
|
|
223 suc n - suc n
|
|
|
224 ∎ where open ≡-Reasoning
|
|
|
225 n-n-m=m {suc m} {suc n} le = begin
|
|
|
226 suc m ≡⟨ cong suc ( n-n-m=m (px≤py le)) ⟩
|
|
|
227 suc (n - (n - m)) ≡⟨ sym (sn-m=sn-m (n-m<n n m)) ⟩
|
|
|
228 suc n - (n - m) ∎ where open ≡-Reasoning
|
|
|
229
|
|
|
230 m+= : {i j m : ℕ } → m + i ≡ m + j → i ≡ j
|
|
|
231 m+= {i} {j} {zero} refl = refl
|
|
|
232 m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq )
|
|
|
233
|
|
|
234 +m= : {i j m : ℕ } → i + m ≡ j + m → i ≡ j
|
|
|
235 +m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq )
|
|
|
236
|
|
|
237 less-1 : { n m : ℕ } → suc n < m → n < m
|
|
|
238 less-1 sn<m = <-trans a<sa sn<m
|
|
|
239
|
|
|
240 sa=b→a<b : { n m : ℕ } → suc n ≡ m → n < m
|
|
|
241 sa=b→a<b {n} {m} sn=m = subst (λ k → n < k ) sn=m a<sa
|
|
|
242
|
|
|
243 minus+n : {x y : ℕ } → suc x > y → minus x y + y ≡ x
|
|
|
244 minus+n {x} {zero} _ = trans (sym (+-comm zero _ )) refl
|
|
|
245 minus+n {zero} {suc y} lt = ⊥-elim ( nat-≤> lt (≤-trans a<sa (s≤s (s≤s z≤n)) ))
|
|
|
246 minus+n {suc x} {suc y} y<sx with <-cmp y (suc x)
|
|
|
247 ... | tri< a ¬b ¬c = begin
|
|
|
248 minus (suc x) (suc y) + suc y ≡⟨ +-comm _ (suc y) ⟩
|
|
|
249 suc y + minus x y ≡⟨ cong ( λ k → suc k ) ( begin
|
|
|
250 y + minus x y ≡⟨ +-comm y _ ⟩
|
|
|
251 minus x y + y ≡⟨ minus+n {x} {y} a ⟩
|
|
|
252 x ∎ ) ⟩
|
|
|
253 suc x ∎ where open ≡-Reasoning
|
|
|
254 ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (px≤py y<sx ))
|
|
|
255 ... | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (px≤py y<sx ))
|
|
|
256
|
|
|
257 +<-cong : {x y z : ℕ } → x < y → z + x < z + y
|
|
|
258 +<-cong {x} {y} {zero} x<y = x<y
|
|
|
259 +<-cong {x} {y} {suc z} x<y = s≤s (+<-cong {x} {y} {z} x<y)
|
|
|
260
|
|
|
261 <-minus-0 : {x y z : ℕ } → z + x < z + y → x < y
|
|
|
262 <-minus-0 {x} {y} {z} x<y with <-cmp x y
|
|
|
263 ... | tri< a ¬b ¬c = a
|
|
|
264 ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (cong (λ k → z + k ) b) x<y )
|
|
|
265 ... | tri> ¬a ¬b c = ⊥-elim ( nat-<> x<y (+<-cong {y} {x} {z} c))
|
|
|
266
|
|
|
267 <-minus : {x y z : ℕ } → x + z < y + z → x < y
|
|
|
268 <-minus {x} {y} {z} lt = <-minus-0 ( subst₂ ( λ j k → j < k ) (+-comm x _) (+-comm y _ ) lt )
|
|
|
269
|
|
|
270 x≤x+y : {z y : ℕ } → z ≤ z + y
|
|
|
271 x≤x+y {zero} {y} = z≤n
|
|
|
272 x≤x+y {suc z} {y} = s≤s (x≤x+y {z} {y})
|
|
|
273
|
|
|
274 x≤y+x : {z y : ℕ } → z ≤ y + z
|
|
|
275 x≤y+x {z} {y} = subst (λ k → z ≤ k ) (+-comm _ y ) x≤x+y
|
|
|
276
|
|
|
277 x≤x+sy : {x y : ℕ} → x < x + suc y
|
|
|
278 x≤x+sy {x} {y} = begin
|
|
|
279 suc x ≤⟨ x≤x+y ⟩
|
|
|
280 suc x + y ≡⟨ cong (λ k → k + y) (+-comm 1 x ) ⟩
|
|
|
281 (x + 1) + y ≡⟨ (+-assoc x 1 _) ⟩
|
|
|
282 x + suc y ∎ where open ≤-Reasoning
|
|
|
283
|
|
|
284
|
|
|
285 <-plus-0 : {x y z : ℕ } → x < y → z + x < z + y
|
|
|
286 <-plus-0 = +<-cong
|
|
|
287
|
|
|
288 <-plus : {x y z : ℕ } → x < y → x + z < y + z
|
|
|
289 <-plus {x} {y} {z} x<y = subst₂ (λ j k → j < k ) (+-comm z x ) (+-comm z y ) ( <-plus-0 x<y )
|
|
|
290
|
|
|
291 ≤-plus-0 : {x y z : ℕ } → x ≤ y → z + x ≤ z + y
|
|
|
292 ≤-plus-0 {x} {y} {zero} lt = lt
|
|
|
293 ≤-plus-0 {x} {y} {suc z} lt = s≤s ( ≤-plus-0 {x} {y} {z} lt )
|
|
|
294
|
|
|
295 ≤-plus : {x y z : ℕ } → x ≤ y → x + z ≤ y + z
|
|
|
296 ≤-plus {x} {y} {z} x≤y = subst₂ (λ j k → j ≤ k ) (+-comm z x ) (+-comm z y ) ( ≤-plus-0 x≤y )
|
|
|
297
|
|
|
298 x+y<z→x<z : {x y z : ℕ } → x + y < z → x < z
|
|
|
299 x+y<z→x<z {x} {zero} {z} xy<z = subst (λ k → k < z ) (+-comm x zero ) xy<z
|
|
|
300 x+y<z→x<z {x} {suc y} {z} xy<z = <-minus {x} {z} {suc y} (<-trans xy<z x≤x+sy )
|
|
|
301
|
|
|
302 *≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z
|
|
|
303 *≤ lt = *-mono-≤ lt ≤-refl
|
|
|
304
|
|
|
305 <to≤ : {x y : ℕ } → x < y → x ≤ y
|
|
|
306 <to≤ {x} {y} x<y with <-cmp x (suc y)
|
|
|
307 ... | tri< a ¬b ¬c = px≤py a
|
|
|
308 ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (≤-trans x<y a≤sa ))
|
|
|
309 ... | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (≤-trans x<y a≤sa ))
|
|
|
310
|
|
|
311 <sto≤ : {x y : ℕ } → x < suc y → x ≤ y
|
|
|
312 <sto≤ {x} {y} x<sy with <-cmp x y
|
|
|
313 ... | tri< a ¬b ¬c = <to≤ a
|
|
|
314 ... | tri≈ ¬a refl ¬c = ≤-refl
|
|
|
315 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c x<sy )
|
|
|
316
|
|
|
317 *< : {x y z : ℕ } → x < y → x * suc z < y * suc z
|
|
|
318 *< {x} {zero} {z} ()
|
|
|
319 *< {x} {suc y} {z} x<y = s≤s ( begin
|
|
|
320 x * suc z ≤⟨ lem01 ⟩
|
|
|
321 y * suc z ≤⟨ x≤x+y ⟩
|
|
|
322 y * suc z + z ≡⟨ +-comm _ z ⟩
|
|
|
323 z + y * suc z ∎ ) where
|
|
|
324 open ≤-Reasoning
|
|
|
325 lem01 : x * suc z ≤ y * suc z
|
|
|
326 lem01 = *-mono-≤ {x} {y} {suc z} (<sto≤ x<y) ≤-refl
|
|
|
327
|
|
|
328 <to<s : {x y : ℕ } → x < y → x < suc y
|
|
|
329 <to<s x<y = <-trans x<y a<sa
|
|
|
330
|
|
|
331 <tos<s : {x y : ℕ } → x < y → suc x < suc y
|
|
|
332 <tos<s x<y = s≤s x<y
|
|
|
333
|
|
|
334 <∨≤ : ( x y : ℕ ) → (x < y ) ∨ (y ≤ x)
|
|
|
335 <∨≤ x y with <-cmp x y
|
|
|
336 ... | tri< a ¬b ¬c = case1 a
|
|
|
337 ... | tri≈ ¬a refl ¬c = case2 ≤-refl
|
|
|
338 ... | tri> ¬a ¬b c = case2 (<to≤ c)
|
|
|
339
|
|
|
340 x<y→≤ : {x y : ℕ } → x < y → x ≤ suc y
|
|
|
341 x<y→≤ {x} {y} x<y with <-cmp x (suc y)
|
|
|
342 ... | tri< a ¬b ¬c = <to≤ a
|
|
|
343 ... | tri≈ ¬a b ¬c = refl-≤≡ b
|
|
|
344 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a ( ≤-trans x<y a≤sa ))
|
|
|
345
|
|
|
346 ≤→= : {i j : ℕ} → i ≤ j → j ≤ i → i ≡ j
|
|
|
347 ≤→= {i} {j} i≤j j≤i with <-cmp i j
|
|
|
348 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> j≤i a )
|
|
|
349 ... | tri≈ ¬a b ¬c = b
|
|
|
350 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> i≤j c )
|
|
|
351
|
|
|
352 sx≤py→x≤y : {x y : ℕ } → suc x ≤ suc y → x ≤ y
|
|
|
353 sx≤py→x≤y = px≤py
|
|
|
354
|
|
|
355 sx<py→x<y : {x y : ℕ } → suc x < suc y → x < y
|
|
|
356 sx<py→x<y {x} {y} sx<sy with <-cmp x y
|
|
|
357 ... | tri< a ¬b ¬c = a
|
|
|
358 ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (cong suc b) sx<sy )
|
|
|
359 ... | tri> ¬a ¬b c = ⊥-elim ( nat-<> (s≤s c) sx<sy )
|
|
|
360
|
|
|
361 sx≤y→x≤y : {x y : ℕ } → suc x ≤ y → x ≤ y
|
|
|
362 sx≤y→x≤y sx≤y = ≤-trans a≤sa sx≤y
|
|
|
363
|
|
|
364 x<sy→x≤y : {x y : ℕ } → x < suc y → x ≤ y
|
|
|
365 x<sy→x≤y = <sto≤
|
|
|
366
|
|
|
367 x≤y→x<sy : {x y : ℕ } → x ≤ y → x < suc y
|
|
|
368 x≤y→x<sy {.zero} {y} z≤n = ≤-trans a<sa (s≤s z≤n)
|
|
|
369 x≤y→x<sy {.(suc _)} {.(suc _)} (s≤s le) = s≤s ( x≤y→x<sy le)
|
|
|
370
|
|
|
371 sx≤y→x<y : {x y : ℕ } → suc x ≤ y → x < y
|
|
|
372 sx≤y→x<y sx≤y = sx≤y
|
|
|
373
|
|
|
374 open import Data.Product
|
|
|
375
|
|
|
376 i-j=0→i=j : {i j : ℕ } → j ≤ i → i - j ≡ 0 → i ≡ j
|
|
|
377 i-j=0→i=j {i} {j} le j=0 = begin
|
|
|
378 i ≡⟨ sym (m-0=m) ⟩
|
|
|
379 i - 0 ≡⟨ cong (λ k → i - k ) (sym j=0) ⟩
|
|
|
380 i - (i - j ) ≡⟨ sym (n-n-m=m le) ⟩
|
|
|
381 j ∎ where open ≡-Reasoning
|
|
|
382
|
|
|
383 m*n=0⇒m=0∨n=0 : {i j : ℕ} → i * j ≡ 0 → (i ≡ 0) ∨ ( j ≡ 0 )
|
|
|
384 m*n=0⇒m=0∨n=0 {zero} {j} eq = case1 refl
|
|
|
385 m*n=0⇒m=0∨n=0 {suc i} {zero} eq = case2 refl
|
|
|
386
|
|
|
387
|
|
|
388 minus+1 : {x y : ℕ } → y ≤ x → suc (minus x y) ≡ minus (suc x) y
|
|
|
389 minus+1 {zero} {zero} y≤x = refl
|
|
|
390 minus+1 {suc x} {zero} y≤x = refl
|
|
|
391 minus+1 {suc x} {suc y} y≤x = minus+1 {x} {y} (sx≤py→x≤y y≤x)
|
|
|
392
|
|
|
393 minus+yz : {x y z : ℕ } → z ≤ y → x + minus y z ≡ minus (x + y) z
|
|
|
394 minus+yz {zero} {y} {z} _ = refl
|
|
|
395 minus+yz {suc x} {y} {z} z≤y = begin
|
|
|
396 suc x + minus y z ≡⟨ cong suc ( minus+yz z≤y ) ⟩
|
|
|
397 suc (minus (x + y) z) ≡⟨ minus+1 {x + y} {z} (≤-trans z≤y (subst (λ g → y ≤ g) (+-comm y x) x≤x+y) ) ⟩
|
|
|
398 minus (suc x + y) z ∎ where open ≡-Reasoning
|
|
|
399
|
|
|
400 minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0
|
|
|
401 minus<=0 {0} {zero} le = refl
|
|
|
402 minus<=0 {0} {suc y} le = refl
|
|
|
403 minus<=0 {suc x} {suc y} le = minus<=0 {x} {y} (sx≤py→x≤y le)
|
|
|
404
|
|
|
405 minus>0 : {x y : ℕ } → x < y → 0 < minus y x
|
|
|
406 minus>0 {zero} {suc _} lt = lt
|
|
|
407 minus>0 {suc x} {suc y} lt = minus>0 {x} {y} (sx<py→x<y lt)
|
|
|
408
|
|
|
409 minus>0→x<y : {x y : ℕ } → 0 < minus y x → x < y
|
|
|
410 minus>0→x<y {x} {y} lt with <-cmp x y
|
|
|
411 ... | tri< a ¬b ¬c = a
|
|
|
412 ... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-≡< (sym (minus<=0 {x} ≤-refl)) lt )
|
|
|
413 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym (minus<=0 {y} (≤-trans refl-≤s c ))) lt )
|
|
|
414
|
|
|
415 minus+y-y : {x y : ℕ } → (x + y) - y ≡ x
|
|
|
416 minus+y-y {zero} {y} = minus<=0 {zero + y} {y} ≤-refl
|
|
|
417 minus+y-y {suc x} {y} = begin
|
|
|
418 (suc x + y) - y ≡⟨ sym (minus+1 {_} {y} x≤y+x) ⟩
|
|
|
419 suc ((x + y) - y) ≡⟨ cong suc (minus+y-y {x} {y}) ⟩
|
|
|
420 suc x ∎ where open ≡-Reasoning
|
|
|
421
|
|
|
422 minus+yx-yz : {x y z : ℕ } → (y + x) - (y + z) ≡ x - z
|
|
|
423 minus+yx-yz {x} {zero} {z} = refl
|
|
|
424 minus+yx-yz {x} {suc y} {z} = minus+yx-yz {x} {y} {z}
|
|
|
425
|
|
|
426 minus+xy-zy : {x y z : ℕ } → (x + y) - (z + y) ≡ x - z
|
|
|
427 minus+xy-zy {x} {y} {z} = subst₂ (λ j k → j - k ≡ x - z ) (+-comm y x) (+-comm y z) (minus+yx-yz {x} {y} {z})
|
|
|
428
|
|
|
429 +cancel<l : (x z : ℕ ) {y : ℕ} → y + x < y + z → x < z
|
|
|
430 +cancel<l x z {zero} lt = lt
|
|
|
431 +cancel<l x z {suc y} lt = +cancel<l x z {y} (sx<py→x<y lt)
|
|
|
432
|
|
|
433 +cancel<r : (x z : ℕ ) {y : ℕ} → x + y < z + y → x < z
|
|
|
434 +cancel<r x z {y} lt = +cancel<l x z (subst₂ (λ j k → j < k ) (+-comm x _) (+-comm z _) lt )
|
|
|
435
|
|
|
436 minus<z : {x y z : ℕ } → x < y → z ≤ x → x - z < y - z
|
|
|
437 minus<z {x} {y} {z} x<y z≤x = +cancel<r _ _ ( begin
|
|
|
438 suc ( (x - z) + z ) ≡⟨ cong suc (minus+n (s≤s z≤x) ) ⟩
|
|
|
439 suc x ≤⟨ x<y ⟩
|
|
|
440 y ≡⟨ sym ( minus+n (<-trans (s≤s z≤x) (s≤s x<y) )) ⟩
|
|
|
441 (y - z ) + z ∎ ) where open ≤-Reasoning
|
|
|
442
|
|
|
443
|
|
|
444 y-x<y : {x y : ℕ } → 0 < x → 0 < y → y - x < y
|
|
|
445 y-x<y {x} {y} 0<x 0<y with <-cmp x (suc y)
|
|
|
446 ... | tri< a ¬b ¬c = +cancel<r (y - x) _ ( begin
|
|
|
447 suc ((y - x) + x) ≡⟨ cong suc (minus+n {y} {x} a ) ⟩
|
|
|
448 suc y ≡⟨ +-comm 1 _ ⟩
|
|
|
449 y + suc 0 ≤⟨ +-mono-≤ ≤-refl 0<x ⟩
|
|
|
450 y + x ∎ ) where open ≤-Reasoning
|
|
|
451 ... | tri≈ ¬a refl ¬c = subst ( λ k → k < y ) (sym (minus<=0 {y} {x} refl-≤s )) 0<y
|
|
|
452 ... | tri> ¬a ¬b c = subst ( λ k → k < y ) (sym (minus<=0 {y} {x} (≤-trans (≤-trans refl-≤s refl-≤s) c))) 0<y -- suc (suc y) ≤ x → y ≤ x
|
|
|
453
|
|
|
454 open import Relation.Binary.Definitions
|
|
|
455
|
|
|
456 distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z)
|
|
|
457 distr-minus-* {x} {zero} {z} = refl
|
|
|
458 distr-minus-* {x} {suc y} {z} with <-cmp x y
|
|
|
459 distr-minus-* {x} {suc y} {z} | tri< a ¬b ¬c = begin
|
|
|
460 minus x (suc y) * z
|
|
|
461 ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} (x<y→≤ a)) ⟩
|
|
|
462 0 * z
|
|
|
463 ≡⟨ sym (minus<=0 {x * z} {z + y * z} le ) ⟩
|
|
|
464 minus (x * z) (z + y * z)
|
|
|
465 ∎ where
|
|
|
466 open ≡-Reasoning
|
|
|
467 le : x * z ≤ z + y * z
|
|
|
468 le = ≤-trans lemma (subst (λ k → y * z ≤ k ) (+-comm _ z ) (x≤x+y {y * z} {z} ) ) where
|
|
|
469 lemma : x * z ≤ y * z
|
|
|
470 lemma = *≤ {x} {y} {z} (<to≤ a)
|
|
|
471 distr-minus-* {x} {suc y} {z} | tri≈ ¬a refl ¬c = begin
|
|
|
472 minus x (suc y) * z
|
|
|
473 ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} refl-≤s ) ⟩
|
|
|
474 0 * z
|
|
|
475 ≡⟨ sym (minus<=0 {x * z} {z + y * z} (lt {x} {z} )) ⟩
|
|
|
476 minus (x * z) (z + y * z)
|
|
|
477 ∎ where
|
|
|
478 open ≡-Reasoning
|
|
|
479 lt : {x z : ℕ } → x * z ≤ z + x * z
|
|
|
480 lt {zero} {zero} = z≤n
|
|
|
481 lt {suc x} {zero} = lt {x} {zero}
|
|
|
482 lt {x} {suc z} = ≤-trans lemma refl-≤s where
|
|
|
483 lemma : x * suc z ≤ z + x * suc z
|
|
|
484 lemma = subst (λ k → x * suc z ≤ k ) (+-comm _ z) (x≤x+y {x * suc z} {z})
|
|
|
485 distr-minus-* {x} {suc y} {z} | tri> ¬a ¬b c = +m= {_} {_} {suc y * z} ( begin
|
|
|
486 minus x (suc y) * z + suc y * z
|
|
|
487 ≡⟨ sym (proj₂ *-distrib-+ z (minus x (suc y) ) _) ⟩
|
|
|
488 ( minus x (suc y) + suc y ) * z
|
|
|
489 ≡⟨ cong (λ k → k * z) (minus+n {x} {suc y} (s≤s c)) ⟩
|
|
|
490 x * z
|
|
|
491 ≡⟨ sym (minus+n {x * z} {suc y * z} (s≤s (lt c))) ⟩
|
|
|
492 minus (x * z) (suc y * z) + suc y * z
|
|
|
493 ∎ ) where
|
|
|
494 open ≡-Reasoning
|
|
|
495 lt : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z
|
|
|
496 lt {x} {y} {z} le = *≤ le
|
|
|
497
|
|
|
498 distr-minus-*' : {z x y : ℕ } → z * (minus x y) ≡ minus (z * x) (z * y)
|
|
|
499 distr-minus-*' {z} {x} {y} = begin
|
|
|
500 z * (minus x y) ≡⟨ *-comm _ (x - y) ⟩
|
|
|
501 (minus x y) * z ≡⟨ distr-minus-* {x} {y} {z} ⟩
|
|
|
502 minus (x * z) (y * z) ≡⟨ cong₂ (λ j k → j - k ) (*-comm x z ) (*-comm y z) ⟩
|
|
|
503 minus (z * x) (z * y) ∎ where open ≡-Reasoning
|
|
|
504
|
|
|
505 minus- : {x y z : ℕ } → suc x > z + y → minus (minus x y) z ≡ minus x (y + z)
|
|
|
506 minus- {x} {y} {z} gt = +m= {_} {_} {z} ( begin
|
|
|
507 minus (minus x y) z + z
|
|
|
508 ≡⟨ minus+n {_} {z} lemma ⟩
|
|
|
509 minus x y
|
|
|
510 ≡⟨ +m= {_} {_} {y} ( begin
|
|
|
511 minus x y + y
|
|
|
512 ≡⟨ minus+n {_} {y} lemma1 ⟩
|
|
|
513 x
|
|
|
514 ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩
|
|
|
515 minus x (z + y) + (z + y)
|
|
|
516 ≡⟨ sym ( +-assoc (minus x (z + y)) _ _ ) ⟩
|
|
|
517 minus x (z + y) + z + y
|
|
|
518 ∎ ) ⟩
|
|
|
519 minus x (z + y) + z
|
|
|
520 ≡⟨ cong (λ k → minus x k + z ) (+-comm _ y ) ⟩
|
|
|
521 minus x (y + z) + z
|
|
|
522 ∎ ) where
|
|
|
523 open ≡-Reasoning
|
|
|
524 lemma1 : suc x > y
|
|
|
525 lemma1 = x+y<z→x<z (subst (λ k → k < suc x ) (+-comm z _ ) gt )
|
|
|
526 lemma : suc (minus x y) > z
|
|
|
527 lemma = <-minus {_} {_} {y} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y} lemma1 )) gt )
|
|
|
528
|
|
|
529 sn≤1→n=0 : {n : ℕ } → suc n ≤ 1 → n ≡ 0
|
|
|
530 sn≤1→n=0 {n} sn≤1 with <-cmp n 0
|
|
|
531 ... | tri≈ ¬a b ¬c = b
|
|
|
532 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c sn≤1 )
|
|
|
533
|
|
|
534 minus-* : {M k n : ℕ } → n < k → minus k (suc n) * M ≡ minus (minus k n * M ) M
|
|
|
535 minus-* {zero} {k} {n} lt = begin
|
|
|
536 minus k (suc n) * zero
|
|
|
537 ≡⟨ *-comm (minus k (suc n)) zero ⟩
|
|
|
538 zero * minus k (suc n)
|
|
|
539 ≡⟨⟩
|
|
|
540 0 * minus k n
|
|
|
541 ≡⟨ *-comm 0 (minus k n) ⟩
|
|
|
542 minus (minus k n * 0 ) 0
|
|
|
543 ∎ where
|
|
|
544 open ≡-Reasoning
|
|
|
545 minus-* {suc m} {k} {n} lt with <-cmp k 1
|
|
|
546 minus-* {suc m} {k} {n} lt | tri< a ¬b ¬c = ⊥-elim ( nat-≤> (sx≤py→x≤y a) (≤-trans (s≤s z≤n) lt) )
|
|
|
547 minus-* {suc m} {k} {n} lt | tri≈ ¬a refl ¬c = subst (λ k → minus 0 k * suc m ≡ minus (minus 1 k * suc m) (suc m)) (sym n=0) lem where
|
|
|
548 n=0 : n ≡ 0
|
|
|
549 n=0 = sn≤1→n=0 lt
|
|
|
550 lem : minus 0 0 * suc m ≡ minus (minus 1 0 * suc m) (suc m)
|
|
|
551 lem = begin
|
|
|
552 minus 0 0 * suc m ≡⟨⟩
|
|
|
553 0 ≡⟨ sym ( minus<=0 {suc m} {suc m} ≤-refl ) ⟩
|
|
|
554 minus (suc m) (suc m) ≡⟨ cong (λ k → minus k (suc m)) (+-comm 0 (suc m) ) ⟩
|
|
|
555 minus (suc m + 0) (suc m) ≡⟨⟩
|
|
|
556 minus (minus 1 0 * suc m) (suc m) ∎ where open ≡-Reasoning
|
|
|
557 minus-* {suc m} {k} {n} lt | tri> ¬a ¬b c = begin
|
|
|
558 minus k (suc n) * M
|
|
|
559 ≡⟨ distr-minus-* {k} {suc n} {M} ⟩
|
|
|
560 minus (k * M ) ((suc n) * M)
|
|
|
561 ≡⟨⟩
|
|
|
562 minus (k * M ) (M + n * M )
|
|
|
563 ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩
|
|
|
564 minus (k * M ) ((n * M) + M )
|
|
|
565 ≡⟨ sym ( minus- {k * M} {n * M} (lemma lt) ) ⟩
|
|
|
566 minus (minus (k * M ) (n * M)) M
|
|
|
567 ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩
|
|
|
568 minus (minus k n * M ) M
|
|
|
569 ∎ where
|
|
|
570 M = suc m
|
|
|
571 lemma : {n k m : ℕ } → n < k → suc (k * suc m) > suc m + n * suc m
|
|
|
572 lemma {n} {k} {m} lt = ≤-plus-0 {_} {_} {1} (*≤ lt )
|
|
|
573 open ≡-Reasoning
|
|
|
574
|
|
|
575 x=y+z→x-z=y : {x y z : ℕ } → x ≡ y + z → x - z ≡ y
|
|
|
576 x=y+z→x-z=y {x} {zero} {.x} refl = minus<=0 {x} {x} refl-≤ -- x ≡ suc (y + z) → (x ≡ y + z → x - z ≡ y) → (x - z) ≡ suc y
|
|
|
577 x=y+z→x-z=y {suc x} {suc y} {zero} eq = begin -- suc x ≡ suc (y + zero) → (suc x - zero) ≡ suc y
|
|
|
578 suc x - zero ≡⟨ refl ⟩
|
|
|
579 suc x ≡⟨ eq ⟩
|
|
|
580 suc y + zero ≡⟨ +-comm _ zero ⟩
|
|
|
581 suc y ∎ where open ≡-Reasoning
|
|
|
582 x=y+z→x-z=y {suc x} {suc y} {suc z} eq = x=y+z→x-z=y {x} {suc y} {z} ( begin
|
|
|
583 x ≡⟨ cong pred eq ⟩
|
|
|
584 pred (suc y + suc z) ≡⟨ +-comm _ (suc z) ⟩
|
|
|
585 suc z + y ≡⟨ cong suc ( +-comm _ y ) ⟩
|
|
|
586 suc y + z ∎ ) where open ≡-Reasoning
|
|
|
587
|
|
|
588 m*1=m : {m : ℕ } → m * 1 ≡ m
|
|
|
589 m*1=m {zero} = refl
|
|
|
590 m*1=m {suc m} = cong suc m*1=m
|
|
|
591
|
|
|
592 +-cancel-1 : (x y z : ℕ ) → x + y ≡ x + z → y ≡ z
|
|
|
593 +-cancel-1 zero y z eq = eq
|
|
|
594 +-cancel-1 (suc x) y z eq = +-cancel-1 x y z (cong pred eq )
|
|
|
595
|
|
|
596 +-cancel-0 : (x y z : ℕ ) → y + x ≡ z + x → y ≡ z
|
|
|
597 +-cancel-0 x y z eq = +-cancel-1 x y z (trans (+-comm x y) (trans eq (sym (+-comm x z)) ))
|
|
|
598
|
|
|
599 *-cancel-left : {x y z : ℕ } → x > 0 → x * y ≡ x * z → y ≡ z
|
|
|
600 *-cancel-left {suc x} {zero} {zero} lt eq = refl
|
|
|
601 *-cancel-left {suc x} {zero} {suc z} lt eq = ⊥-elim ( nat-≡< eq (s≤s (begin
|
|
|
602 x * zero ≡⟨ *-comm x _ ⟩
|
|
|
603 zero ≤⟨ z≤n ⟩
|
|
|
604 z + x * suc z ∎ ))) where open ≤-Reasoning
|
|
|
605 *-cancel-left {suc x} {suc y} {zero} lt eq = ⊥-elim ( nat-≡< (sym eq) (s≤s (begin
|
|
|
606 x * zero ≡⟨ *-comm x _ ⟩
|
|
|
607 zero ≤⟨ z≤n ⟩
|
|
|
608 _ ∎ ))) where open ≤-Reasoning
|
|
|
609 *-cancel-left {suc x} {suc y} {suc z} lt eq with cong pred eq
|
|
|
610 ... | eq1 = cong suc (*-cancel-left {suc x} {y} {z} lt (+-cancel-0 x _ _ (begin
|
|
|
611 y + x * y + x ≡⟨ +-assoc y _ _ ⟩
|
|
|
612 y + (x * y + x) ≡⟨ cong (λ k → y + (k + x)) (*-comm x _) ⟩
|
|
|
613 y + (y * x + x) ≡⟨ cong (_+_ y) (+-comm _ x) ⟩
|
|
|
614 y + (x + y * x ) ≡⟨ refl ⟩
|
|
|
615 y + suc y * x ≡⟨ cong (_+_ y) (*-comm (suc y) _) ⟩
|
|
|
616 y + x * suc y ≡⟨ eq1 ⟩
|
|
|
617 z + x * suc z ≡⟨ refl ⟩
|
|
|
618 _ ≡⟨ sym ( cong (_+_ z) (*-comm (suc z) _) ) ⟩
|
|
|
619 _ ≡⟨ sym ( cong (_+_ z) (+-comm _ x)) ⟩
|
|
|
620 z + (z * x + x) ≡⟨ sym ( cong (λ k → z + (k + x)) (*-comm x _) ) ⟩
|
|
|
621 z + (x * z + x) ≡⟨ sym ( +-assoc z _ _) ⟩
|
|
|
622 z + x * z + x ∎ ))) where open ≡-Reasoning
|
|
|
623
|
|
|
624 record Finduction {n m : Level} (P : Set n ) (Q : P → Set m ) (f : P → ℕ) : Set (n Level.⊔ m) where
|
|
|
625 field
|
|
|
626 fzero : {p : P} → f p ≡ zero → Q p
|
|
|
627 pnext : (p : P ) → P
|
|
|
628 decline : {p : P} → 0 < f p → f (pnext p) < f p
|
|
|
629 ind : {p : P} → Q (pnext p) → Q p
|
|
|
630
|
|
|
631 y<sx→y≤x : {x y : ℕ} → y < suc x → y ≤ x
|
|
|
632 y<sx→y≤x = x<sy→x≤y
|
|
|
633
|
|
|
634 fi0 : (x : ℕ) → x ≤ zero → x ≡ zero
|
|
|
635 fi0 .0 z≤n = refl
|
|
|
636
|
|
|
637 f-induction : {n m : Level} {P : Set n } → {Q : P → Set m }
|
|
|
638 → (f : P → ℕ)
|
|
|
639 → Finduction P Q f
|
|
|
640 → (p : P ) → Q p
|
|
|
641 f-induction {n} {m} {P} {Q} f I p with <-cmp 0 (f p)
|
|
|
642 ... | tri> ¬a ¬b ()
|
|
|
643 ... | tri≈ ¬a b ¬c = Finduction.fzero I (sym b)
|
|
|
644 ... | tri< lt _ _ = f-induction0 p (f p) (<to≤ (Finduction.decline I lt)) where
|
|
|
645 f-induction0 : (p : P) → (x : ℕ) → (f (Finduction.pnext I p)) ≤ x → Q p
|
|
|
646 f-induction0 p zero le = Finduction.ind I (Finduction.fzero I (fi0 _ le))
|
|
|
647 f-induction0 p (suc x) le with <-cmp (f (Finduction.pnext I p)) (suc x)
|
|
|
648 ... | tri< a ¬b ¬c = f-induction0 p x (px≤py a)
|
|
|
649 ... | tri≈ ¬a b ¬c = Finduction.ind I (f-induction0 (Finduction.pnext I p) x (y<sx→y≤x f1)) where
|
|
|
650 f1 : f (Finduction.pnext I (Finduction.pnext I p)) < suc x
|
|
|
651 f1 = subst (λ k → f (Finduction.pnext I (Finduction.pnext I p)) < k ) b ( Finduction.decline I {Finduction.pnext I p}
|
|
|
652 (subst (λ k → 0 < k ) (sym b) (s≤s z≤n ) ))
|
|
|
653 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> le c )
|
|
|
654
|
|
|
655
|
|
|
656 record Ninduction {n m : Level} (P : Set n ) (Q : P → Set m ) (f : P → ℕ) : Set (n Level.⊔ m) where
|
|
|
657 field
|
|
|
658 pnext : (p : P ) → P
|
|
|
659 fzero : {p : P} → f (pnext p) ≡ zero → Q p
|
|
|
660 decline : {p : P} → 0 < f p → f (pnext p) < f p
|
|
|
661 ind : {p : P} → Q (pnext p) → Q p
|
|
|
662
|
|
|
663 s≤s→≤ : { i j : ℕ} → suc i ≤ suc j → i ≤ j
|
|
|
664 s≤s→≤ = sx≤py→x≤y
|
|
|
665
|
|
|
666 n-induction : {n m : Level} {P : Set n } → {Q : P → Set m }
|
|
|
667 → (f : P → ℕ)
|
|
|
668 → Ninduction P Q f
|
|
|
669 → (p : P ) → Q p
|
|
|
670 n-induction {n} {m} {P} {Q} f I p = f-induction0 p (f (Ninduction.pnext I p)) ≤-refl where
|
|
|
671 f-induction0 : (p : P) → (x : ℕ) → (f (Ninduction.pnext I p)) ≤ x → Q p
|
|
|
672 f-induction0 p zero lt = Ninduction.fzero I {p} (fi0 _ lt)
|
|
|
673 f-induction0 p (suc x) le with <-cmp (f (Ninduction.pnext I p)) (suc x)
|
|
|
674 ... | tri< a ¬b ¬c = f-induction0 p x (px≤py a)
|
|
|
675 ... | tri≈ ¬a b ¬c = Ninduction.ind I (f-induction0 (Ninduction.pnext I p) x (s≤s→≤ nle) ) where
|
|
|
676 f>0 : 0 < f (Ninduction.pnext I p)
|
|
|
677 f>0 = subst (λ k → 0 < k ) (sym b) ( s≤s z≤n )
|
|
|
678 nle : suc (f (Ninduction.pnext I (Ninduction.pnext I p))) ≤ suc x
|
|
|
679 nle = subst (λ k → suc (f (Ninduction.pnext I (Ninduction.pnext I p))) ≤ k) b (Ninduction.decline I {Ninduction.pnext I p} f>0 )
|
|
|
680 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> le c )
|
|
|
681
|
|
|
682
|
|
|
683 record Factor (n m : ℕ ) : Set where
|
|
|
684 field
|
|
|
685 factor : ℕ
|
|
|
686 remain : ℕ
|
|
|
687 is-factor : factor * n + remain ≡ m
|
|
|
688
|
|
|
689 record Factor< (n m : ℕ ) : Set where
|
|
|
690 field
|
|
|
691 factor : ℕ
|
|
|
692 remain : ℕ
|
|
|
693 is-factor : factor * n + remain ≡ m
|
|
|
694 remain<n : remain < n
|
|
|
695
|
|
|
696 record Dividable (n m : ℕ ) : Set where
|
|
|
697 field
|
|
|
698 factor : ℕ
|
|
|
699 is-factor : factor * n + 0 ≡ m
|
|
|
700
|
|
|
701 open Factor
|
|
|
702
|
|
|
703 DtoF : {n m : ℕ} → Dividable n m → Factor n m
|
|
|
704 DtoF {n} {m} record { factor = f ; is-factor = fa } = record { factor = f ; remain = 0 ; is-factor = fa }
|
|
|
705
|
|
|
706 FtoD : {n m : ℕ} → (fc : Factor n m) → remain fc ≡ 0 → Dividable n m
|
|
|
707 FtoD {n} {m} record { factor = f ; remain = r ; is-factor = fa } refl = record { factor = f ; is-factor = fa }
|
|
|
708
|
|
|
709 --divdable^2 : ( n k : ℕ ) → Dividable k ( n * n ) → Dividable k n
|
|
|
710 --divdable^2 n k dn2 = {!!}
|
|
|
711
|
|
|
712 decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n
|
|
|
713 decf {n} {k} record { factor = f ; remain = r ; is-factor = fa } =
|
|
|
714 decf1 {n} {k} f r fa where
|
|
|
715 decf1 : { n k : ℕ } → (f r : ℕ) → (f * k + r ≡ suc n) → Factor k n
|
|
|
716 decf1 {n} {k} f (suc r) fa = -- this case must be the first
|
|
|
717 record { factor = f ; remain = r ; is-factor = ( begin -- fa : f * k + suc r ≡ suc n
|
|
|
718 f * k + r ≡⟨ cong pred ( begin
|
|
|
719 suc ( f * k + r ) ≡⟨ +-comm _ r ⟩
|
|
|
720 r + suc (f * k) ≡⟨ sym (+-assoc r 1 _) ⟩
|
|
|
721 (r + 1) + f * k ≡⟨ cong (λ t → t + f * k ) (+-comm r 1) ⟩
|
|
|
722 (suc r ) + f * k ≡⟨ +-comm (suc r) _ ⟩
|
|
|
723 f * k + suc r ≡⟨ fa ⟩
|
|
|
724 suc n ∎ ) ⟩
|
|
|
725 n ∎ ) } where open ≡-Reasoning
|
|
|
726 decf1 {n} {zero} (suc f) zero fa = ⊥-elim ( nat-≡< fa (
|
|
|
727 begin suc (suc f * zero + zero) ≡⟨ cong suc (+-comm _ zero) ⟩
|
|
|
728 suc (f * 0) ≡⟨ cong suc (*-comm f zero) ⟩
|
|
|
729 suc zero ≤⟨ s≤s z≤n ⟩
|
|
|
730 suc n ∎ )) where open ≤-Reasoning
|
|
|
731 decf1 {n} {suc k} (suc f) zero fa =
|
|
|
732 record { factor = f ; remain = k ; is-factor = ( begin -- fa : suc (k + f * suc k + zero) ≡ suc n
|
|
|
733 f * suc k + k ≡⟨ +-comm _ k ⟩
|
|
|
734 k + f * suc k ≡⟨ +-comm zero _ ⟩
|
|
|
735 (k + f * suc k) + zero ≡⟨ cong pred fa ⟩
|
|
|
736 n ∎ ) } where open ≡-Reasoning
|
|
|
737
|
|
|
738 div0 : {k : ℕ} → Dividable k 0
|
|
|
739 div0 {k} = record { factor = 0; is-factor = refl }
|
|
|
740
|
|
|
741 div= : {k : ℕ} → Dividable k k
|
|
|
742 div= {k} = record { factor = 1; is-factor = ( begin
|
|
|
743 k + 0 * k + 0 ≡⟨ trans ( +-comm _ 0) ( +-comm _ 0) ⟩
|
|
|
744 k ∎ ) } where open ≡-Reasoning
|
|
|
745
|
|
|
746 div1 : { k : ℕ } → k > 1 → ¬ Dividable k 1
|
|
|
747 div1 {k} k>1 record { factor = f1 ; is-factor = fa } = ⊥-elim ( nat-≡< (sym fa) ( begin
|
|
|
748 2 ≤⟨ k>1 ⟩
|
|
|
749 k ≡⟨ +-comm 0 _ ⟩
|
|
|
750 k + 0 ≡⟨ refl ⟩
|
|
|
751 1 * k ≤⟨ *-mono-≤ {1} {f1} (lem1 _ fa) ≤-refl ⟩
|
|
|
752 f1 * k ≡⟨ +-comm 0 _ ⟩
|
|
|
753 f1 * k + 0 ∎ )) where
|
|
|
754 open ≤-Reasoning
|
|
|
755 lem1 : (f1 : ℕ) → f1 * k + 0 ≡ 1 → 1 ≤ f1
|
|
|
756 lem1 zero ()
|
|
|
757 lem1 (suc f1) eq = s≤s z≤n
|
|
|
758
|
|
|
759 div+div : { i j k : ℕ } → Dividable k i → Dividable k j → Dividable k (i + j) ∧ Dividable k (j + i)
|
|
|
760 div+div {i} {j} {k} di dj = ⟪ div+div1 , subst (λ g → Dividable k g) (+-comm i j) div+div1 ⟫ where
|
|
|
761 fki = Dividable.factor di
|
|
|
762 fkj = Dividable.factor dj
|
|
|
763 div+div1 : Dividable k (i + j)
|
|
|
764 div+div1 = record { factor = fki + fkj ; is-factor = ( begin
|
|
|
765 (fki + fkj) * k + 0 ≡⟨ +-comm _ 0 ⟩
|
|
|
766 (fki + fkj) * k ≡⟨ *-distribʳ-+ k fki _ ⟩
|
|
|
767 fki * k + fkj * k ≡⟨ cong₂ ( λ i j → i + j ) (+-comm 0 (fki * k)) (+-comm 0 (fkj * k)) ⟩
|
|
|
768 (fki * k + 0) + (fkj * k + 0) ≡⟨ cong₂ ( λ i j → i + j ) (Dividable.is-factor di) (Dividable.is-factor dj) ⟩
|
|
|
769 i + j ∎ ) } where
|
|
|
770 open ≡-Reasoning
|
|
|
771
|
|
|
772 div-div : { i j k : ℕ } → k > 1 → Dividable k i → Dividable k j → Dividable k (i - j) ∧ Dividable k (j - i)
|
|
|
773 div-div {i} {j} {k} k>1 di dj = ⟪ div-div1 di dj , div-div1 dj di ⟫ where
|
|
|
774 div-div1 : {i j : ℕ } → Dividable k i → Dividable k j → Dividable k (i - j)
|
|
|
775 div-div1 {i} {j} di dj = record { factor = fki - fkj ; is-factor = ( begin
|
|
|
776 (fki - fkj) * k + 0 ≡⟨ +-comm _ 0 ⟩
|
|
|
777 (fki - fkj) * k ≡⟨ distr-minus-* {fki} {fkj} ⟩
|
|
|
778 (fki * k) - (fkj * k) ≡⟨ cong₂ ( λ i j → i - j ) (+-comm 0 (fki * k)) (+-comm 0 (fkj * k)) ⟩
|
|
|
779 (fki * k + 0) - (fkj * k + 0) ≡⟨ cong₂ ( λ i j → i - j ) (Dividable.is-factor di) (Dividable.is-factor dj) ⟩
|
|
|
780 i - j ∎ ) } where
|
|
|
781 open ≡-Reasoning
|
|
|
782 fki = Dividable.factor di
|
|
|
783 fkj = Dividable.factor dj
|
|
|
784
|
|
|
785 open _∧_
|
|
|
786
|
|
|
787 div+1 : { i k : ℕ } → k > 1 → Dividable k i → ¬ Dividable k (suc i)
|
|
|
788 div+1 {i} {k} k>1 d d1 = div1 k>1 div+11 where
|
|
|
789 div+11 : Dividable k 1
|
|
|
790 div+11 = subst (λ g → Dividable k g) (minus+y-y {1} {i} ) ( proj2 (div-div k>1 d d1 ) )
|
|
|
791
|
|
|
792 div<k : { m k : ℕ } → k > 1 → m > 0 → m < k → ¬ Dividable k m
|
|
|
793 div<k {m} {k} k>1 m>0 m<k d = ⊥-elim ( nat-≤> (div<k1 (Dividable.factor d) (Dividable.is-factor d)) m<k ) where
|
|
|
794 div<k1 : (f : ℕ ) → f * k + 0 ≡ m → k ≤ m
|
|
|
795 div<k1 zero eq = ⊥-elim (nat-≡< eq m>0 )
|
|
|
796 div<k1 (suc f) eq = begin
|
|
|
797 k ≤⟨ x≤x+y ⟩
|
|
|
798 k + (f * k + 0) ≡⟨ sym (+-assoc k _ _) ⟩
|
|
|
799 k + f * k + 0 ≡⟨ eq ⟩
|
|
|
800 m ∎ where open ≤-Reasoning
|
|
|
801
|
|
|
802 0<factor : { m k : ℕ } → k > 0 → m > 0 → (d : Dividable k m ) → Dividable.factor d > 0
|
|
|
803 0<factor {m} {k} k>0 m>0 d with Dividable.factor d in eq1
|
|
|
804 ... | zero = ⊥-elim ( nat-≡< ff1 m>0 ) where
|
|
|
805 ff1 : 0 ≡ m
|
|
|
806 ff1 = begin
|
|
|
807 0 ≡⟨⟩
|
|
|
808 0 * k + 0 ≡⟨ cong (λ j → j * k + 0) (sym eq1) ⟩
|
|
|
809 Dividable.factor d * k + 0 ≡⟨ Dividable.is-factor d ⟩
|
|
|
810 m ∎ where open ≡-Reasoning
|
|
|
811 ... | suc t = s≤s z≤n
|
|
|
812
|
|
|
813 div→k≤m : { m k : ℕ } → k > 1 → m > 0 → Dividable k m → m ≥ k
|
|
|
814 div→k≤m {m} {k} k>1 m>0 d with <-cmp m k
|
|
|
815 ... | tri< a ¬b ¬c = ⊥-elim ( div<k k>1 m>0 a d )
|
|
|
816 ... | tri≈ ¬a refl ¬c = ≤-refl
|
|
|
817 ... | tri> ¬a ¬b c = <to≤ c
|
|
|
818
|
|
|
819 div1*k+0=k : {k : ℕ } → 1 * k + 0 ≡ k
|
|
|
820 div1*k+0=k {k} = begin
|
|
|
821 1 * k + 0 ≡⟨ cong (λ g → g + 0) (+-comm _ 0) ⟩
|
|
|
822 k + 0 ≡⟨ +-comm _ 0 ⟩
|
|
|
823 k ∎ where open ≡-Reasoning
|
|
|
824
|
|
|
825
|
|
|
826 factor< : {k m : ℕ} → k > 1 → Factor< k m
|
|
|
827 factor< {k} {m} k>1 = n-induction {_} {_} {ℕ} {λ m → Factor< k m} F I m where
|
|
|
828 F : ℕ → ℕ
|
|
|
829 F m = m
|
|
|
830 F0 : ( m : ℕ ) → F (m - k) ≡ 0 → Factor< k m
|
|
|
831 F0 0 eq = record { factor = 0 ; remain = 0 ; is-factor = refl ; remain<n = <-trans a<sa k>1 }
|
|
|
832 F0 (suc m) eq with <-cmp k (suc m)
|
|
|
833 ... | tri< a ¬b ¬c = record { factor = 1 ; remain = 0 ; is-factor = lem00 ; remain<n = <-trans a<sa k>1 } where
|
|
|
834 lem00 : k + zero + 0 ≡ suc m
|
|
|
835 lem00 = begin -- minus (suc m) k ≡ 0
|
|
|
836 k + zero + 0 ≡⟨ +-comm (k + 0) _ ⟩
|
|
|
837 k + 0 ≡⟨ +-comm k _ ⟩
|
|
|
838 k ≡⟨ sym ( i-j=0→i=j (≤-trans a≤sa a) eq ) ⟩
|
|
|
839 suc m ∎ where open ≡-Reasoning
|
|
|
840 ... | tri≈ ¬a b ¬c = record { factor = 1 ; remain = 0 ; is-factor = trans (trans (+-comm (k + 0) _) (+-comm k 0)) b ; remain<n = <-trans a<sa k>1 }
|
|
|
841 ... | tri> ¬a ¬b c = record { factor = 0 ; remain = suc m ; is-factor = refl ; remain<n = c }
|
|
|
842 ind : {m : ℕ} → Factor< k (m - k) → Factor< k m
|
|
|
843 ind {m} record { factor = f ; remain = r ; is-factor = isf ; remain<n = r<n } with <-cmp k (suc m)
|
|
|
844 ... | tri≈ ¬a b ¬c = record { factor = 0 ; remain = m ; is-factor = refl ; remain<n = subst (λ j → m < j) (sym b) a<sa }
|
|
|
845 ... | tri> ¬a ¬b c = record { factor = 0 ; remain = m ; is-factor = refl ; remain<n = <-trans a<sa c }
|
|
|
846 ... | tri< a ¬b ¬c = record { factor = suc f ; remain = r ; is-factor = lem00 ; remain<n = r<n } where
|
|
|
847 k<sm : k < suc m
|
|
|
848 k<sm = a
|
|
|
849 lem00 : k + f * k + r ≡ m
|
|
|
850 lem00 = begin
|
|
|
851 k + f * k + r ≡⟨ +-assoc k _ _ ⟩
|
|
|
852 k + (f * k + r) ≡⟨ +-comm k _ ⟩
|
|
|
853 (f * k + r) + k ≡⟨ cong (λ i → i + k ) isf ⟩
|
|
|
854 (m - k) + k ≡⟨ minus+n k<sm ⟩
|
|
|
855 m ∎ where open ≡-Reasoning
|
|
|
856 decl : {m : ℕ } → 0 < m → m - k < m
|
|
|
857 decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m
|
|
|
858 I : Ninduction ℕ _ F
|
|
|
859 I = record {
|
|
|
860 pnext = λ p → p - k
|
|
|
861 ; fzero = λ {m} eq → F0 m eq
|
|
|
862 ; decline = λ {m} lt → decl lt
|
|
|
863 ; ind = λ {p} prev → ind prev
|
|
|
864 }
|
|
|
865
|
|
|
866 Factor<→¬k≤m : {k m : ℕ} → k ≤ m → (x : Factor< k m ) → Factor<.factor x > 0
|
|
|
867 Factor<→¬k≤m {k} {m} k≤m x with Factor<.factor x in eqx
|
|
|
868 ... | zero = ⊥-elim ( nat-≤> k≤m (begin
|
|
|
869 suc m ≡⟨ cong suc (sym (Factor<.is-factor x)) ⟩
|
|
|
870 suc (Factor<.factor x * k + Factor<.remain x) ≡⟨ cong (λ j → suc (j * k + _)) eqx ⟩
|
|
|
871 suc (0 * k + Factor<.remain x) ≡⟨ refl ⟩
|
|
|
872 suc (Factor<.remain x) ≤⟨ Factor<.remain<n x ⟩
|
|
|
873 k ∎ ) ) where open ≤-Reasoning
|
|
|
874 ... | suc fa = s≤s z≤n
|
|
|
875
|
|
|
876 Factor<-inject : {k m : ℕ} → k > 1 → (x y : Factor< k m) → (Factor<.factor x ≡ Factor<.factor y ) ∧ (Factor<.remain x ≡ Factor<.remain y )
|
|
|
877 Factor<-inject {k} {m} k>1 x y = n-induction {_} {_} {ℕ}
|
|
|
878 {λ m → (x y : Factor< k m) → (Factor<.factor x ≡ Factor<.factor y ) ∧ (Factor<.remain x ≡ Factor<.remain y ) } F I m x y where
|
|
|
879 F : ℕ → ℕ
|
|
|
880 F m = m
|
|
|
881 f00 : (m : ℕ ) → ( k ≡ suc m ) → (x y : Factor< k (suc m)) → (Factor<.factor x ≡ Factor<.factor y ) ∧ (Factor<.remain x ≡ Factor<.remain y )
|
|
|
882 f00 m lem00 x y = ⟪ trans (lem02 x) (sym (lem02 y)) , trans (lem01 x) (sym (lem01 y)) ⟫ where
|
|
|
883 lem02 : (f : Factor< k (suc m)) → Factor<.factor f ≡ 1
|
|
|
884 lem02 f with <-cmp (Factor<.factor f) 1
|
|
|
885 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (Factor<.is-factor f) (begin
|
|
|
886 suc (Factor<.factor f * k + Factor<.remain f) ≤⟨ s≤s (≤-plus {_} {_} {Factor<.remain f} (*≤ (px≤py a)) ) ⟩
|
|
|
887 suc (0 * k + Factor<.remain f) ≡⟨⟩
|
|
|
888 suc (0 + Factor<.remain f) ≡⟨⟩
|
|
|
889 suc (Factor<.remain f) ≤⟨ Factor<.remain<n f ⟩
|
|
|
890 k ≡⟨ lem00 ⟩
|
|
|
891 suc m ∎ )) where open ≤-Reasoning
|
|
|
892 ... | tri≈ ¬a b ¬c = b
|
|
|
893 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym (Factor<.is-factor f)) (begin -- 1 < Factor<. factor f, fa * k + r > k ≡ suc m
|
|
|
894 suc (suc m) ≡⟨ cong suc (sym lem00) ⟩
|
|
|
895 suc k ≡⟨ sym (+-comm k 1) ⟩
|
|
|
896 k + 1 <⟨ <-plus-0 k>1 ⟩
|
|
|
897 k + k ≡⟨ cong (λ j → k + j) (+-comm 0 _ ) ⟩
|
|
|
898 k + (k + 0) ≡⟨⟩
|
|
|
899 k + (k + 0 * k) ≡⟨ refl ⟩
|
|
|
900 2 * k ≤⟨ *≤ c ⟩
|
|
|
901 Factor<.factor f * k ≤⟨ x≤x+y ⟩
|
|
|
902 Factor<.factor f * k + Factor<.remain f ∎ ) ) where open ≤-Reasoning
|
|
|
903 lem03 : k ≡ 1 * k
|
|
|
904 lem03 = +-comm 0 k
|
|
|
905 lem01 : (f : Factor< k (suc m)) → Factor<.remain f ≡ 0
|
|
|
906 lem01 f = +-cancel-1 _ _ _ ( begin
|
|
|
907 Factor<.factor f * k + Factor<.remain f ≡⟨ Factor<.is-factor f ⟩
|
|
|
908 suc m ≡⟨ sym lem00 ⟩
|
|
|
909 k ≡⟨ +-comm 0 k ⟩
|
|
|
910 k + 0 ≡⟨ cong (λ j → j + 0) lem03 ⟩
|
|
|
911 1 * k + 0 ≡⟨ cong (λ j → j * k + 0) (sym (lem02 f)) ⟩
|
|
|
912 Factor<.factor f * k + 0 ∎ ) where open ≡-Reasoning
|
|
|
913 F0 : ( m : ℕ ) → F (m - k) ≡ 0 → (x y : Factor< k m) → (Factor<.factor x ≡ Factor<.factor y ) ∧ (Factor<.remain x ≡ Factor<.remain y )
|
|
|
914 F0 0 eq x y = ⟪ trans (lem00 x) (sym (lem00 y)) , trans (lem01 x) (sym (lem01 y)) ⟫ where
|
|
|
915 lem01 : (f : Factor< k 0) → Factor<.remain f ≡ 0
|
|
|
916 lem01 f with Factor<.remain f in eq1
|
|
|
917 ... | zero = refl
|
|
|
918 ... | suc n = ⊥-elim ( nat-≡< (sym (Factor<.is-factor f)) (begin
|
|
|
919 suc 0 ≤⟨ s≤s z≤n ⟩
|
|
|
920 suc n ≡⟨ sym eq1 ⟩
|
|
|
921 Factor<.remain f ≡⟨ refl ⟩
|
|
|
922 0 + Factor<.remain f ≤⟨ x≤y+x ⟩
|
|
|
923 Factor<.factor f * k + Factor<.remain f ∎ ) ) where open ≤-Reasoning
|
|
|
924 lem00 : (f : Factor< k 0) → Factor<.factor f ≡ 0
|
|
|
925 lem00 f with m*n=0⇒m=0∨n=0 {Factor<.factor f} {k} (trans (+-comm 0 (Factor<.factor f * k) ) (subst (λ j → _ + j ≡ 0) (lem01 f) (Factor<.is-factor f)))
|
|
|
926 ... | case1 fa=0 = fa=0
|
|
|
927 ... | case2 k=0 = ⊥-elim (nat-≡< (sym k=0) (<-trans a<sa k>1) )
|
|
|
928 F0 (suc m) eq x y with <-cmp k (suc m)
|
|
|
929 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b lem00 ) where
|
|
|
930 lem00 : k ≡ suc m
|
|
|
931 lem00 = begin
|
|
|
932 k ≡⟨ sym ( i-j=0→i=j (≤-trans a≤sa a) eq ) ⟩
|
|
|
933 suc m ∎ where open ≡-Reasoning
|
|
|
934 ... | tri≈ ¬a b ¬c = f00 m b x y
|
|
|
935 ... | tri> ¬a ¬b c = ⟪ trans ( lem00 x ) (sym (lem00 y)) , trans (lem01 x) (sym (lem01 y)) ⟫ where
|
|
|
936 lem00 : (f : Factor< k (suc m)) → Factor<.factor f ≡ 0
|
|
|
937 lem00 f with Factor<.factor f in eq1
|
|
|
938 ... | zero = refl
|
|
|
939 ... | suc fa = ⊥-elim ( nat-≡< (sym (Factor<.is-factor f)) (begin
|
|
|
940 suc (suc m) ≤⟨ c ⟩
|
|
|
941 k ≤⟨ x≤x+y ⟩
|
|
|
942 k + Factor<.remain f ≡⟨ cong (λ j → j + _) (+-comm 0 k) ⟩
|
|
|
943 suc 0 * k + Factor<.remain f ≤⟨ ≤-plus {_} {_} {Factor<.remain f} (*≤ {suc 0} {suc fa} {k} (s≤s z≤n)) ⟩
|
|
|
944 suc fa * k + Factor<.remain f ≡⟨ cong (λ j → j * k + Factor<.remain f) (sym eq1) ⟩
|
|
|
945 Factor<.factor f * k + Factor<.remain f ∎ ) ) where open ≤-Reasoning
|
|
|
946 lem01 : (f : Factor< k (suc m)) → Factor<.remain f ≡ (suc m)
|
|
|
947 lem01 f = begin
|
|
|
948 Factor<.remain f ≡⟨ refl ⟩
|
|
|
949 0 * k + Factor<.remain f ≡⟨ cong (λ j → j * k + Factor<.remain f) (sym (lem00 f)) ⟩
|
|
|
950 Factor<.factor f * k + Factor<.remain f ≡⟨ Factor<.is-factor f ⟩
|
|
|
951 suc m ∎ where open ≡-Reasoning
|
|
|
952 ind : {m : ℕ}
|
|
|
953 → ( (x y : Factor< k (m - k)) → (Factor<.factor x ≡ Factor<.factor y ) ∧ (Factor<.remain x ≡ Factor<.remain y ) )
|
|
|
954 → (x y : Factor< k m) → (Factor<.factor x ≡ Factor<.factor y ) ∧ (Factor<.remain x ≡ Factor<.remain y )
|
|
|
955 ind {m} prev x y with <∨≤ m k
|
|
|
956 ... | case1 m<k = ⟪ trans (lem00 x) (sym (lem00 y)) , trans (lem01 x) (sym (lem01 y)) ⟫ where
|
|
|
957 lem00 : (x : Factor< k m ) → Factor<.factor x ≡ 0
|
|
|
958 lem00 x with Factor<.factor x in eqx
|
|
|
959 ... | zero = refl
|
|
|
960 ... | suc fa = ⊥-elim ( nat-≤> (begin
|
|
|
961 k ≤⟨ x≤x+y ⟩
|
|
|
962 k + (fa * k + Factor<.remain x) ≡⟨ sym (+-assoc k _ _) ⟩
|
|
|
963 ( k + fa * k ) + Factor<.remain x ≡⟨ refl ⟩
|
|
|
964 suc fa * k + Factor<.remain x ≡⟨ cong (λ j → j * k + Factor<.remain x) (sym eqx) ⟩
|
|
|
965 Factor<.factor x * k + Factor<.remain x ≡⟨ Factor<.is-factor x ⟩
|
|
|
966 m ∎ )
|
|
|
967 m<k ) where open ≤-Reasoning
|
|
|
968 lem01 : (f : Factor< k m) → Factor<.remain f ≡ m
|
|
|
969 lem01 f = begin
|
|
|
970 Factor<.remain f ≡⟨ refl ⟩
|
|
|
971 0 * k + Factor<.remain f ≡⟨ cong (λ j → j * k + Factor<.remain f) (sym (lem00 f)) ⟩
|
|
|
972 Factor<.factor f * k + Factor<.remain f ≡⟨ Factor<.is-factor f ⟩
|
|
|
973 m ∎ where open ≡-Reasoning
|
|
|
974 ... | case2 k≤m = px=py x y k≤m where
|
|
|
975 lem07 : (x : Factor< k m ) → {fa : ℕ } → suc fa ≡ Factor<.factor x → fa * k + Factor<.remain x ≡ m - k
|
|
|
976 lem07 x {fa} eq1 = begin
|
|
|
977 fa * k + Factor<.remain x ≡⟨ sym (minus+y-y {_} {k} ) ⟩
|
|
|
978 (fa * k + Factor<.remain x + k ) - k ≡⟨ cong (λ j → j - k) ( begin
|
|
|
979 fa * k + Factor<.remain x + k ≡⟨ +-assoc (fa * k) _ _ ⟩
|
|
|
980 fa * k + (Factor<.remain x + k) ≡⟨ cong (λ j → fa * k + j) (+-comm _ k) ⟩
|
|
|
981 fa * k + (k + Factor<.remain x ) ≡⟨ sym (+-assoc (fa * k) k _ ) ⟩
|
|
|
982 (fa * k + k) + Factor<.remain x ≡⟨ cong (λ j → j + Factor<.remain x ) (+-comm (fa * k) k) ⟩
|
|
|
983 suc fa * k + Factor<.remain x ≡⟨ cong (λ j → j * k + _) (eq1) ⟩
|
|
|
984 Factor<.factor x * k + Factor<.remain x ∎ ) ⟩
|
|
|
985 (Factor<.factor x * k + Factor<.remain x) - k ≡⟨ cong (λ j → j - k ) (Factor<.is-factor x) ⟩
|
|
|
986 m - k ∎ where open ≡-Reasoning
|
|
|
987 px=py : (x y : Factor< k m) → k ≤ m → (Factor<.factor x ≡ Factor<.factor y ) ∧ (Factor<.remain x ≡ Factor<.remain y )
|
|
|
988 px=py x y k≤m with Factor<.factor x in eqx | Factor<.factor y in eqy
|
|
|
989 ... | zero | _ = ⊥-elim ( nat-≡< (sym eqx) (Factor<→¬k≤m k≤m x) )
|
|
|
990 ... | _ | zero = ⊥-elim ( nat-≡< (sym eqy) (Factor<→¬k≤m k≤m y) )
|
|
|
991 ... | suc fx | suc fy with prev
|
|
|
992 record { factor = fx ; remain = Factor<.remain x ; is-factor = lem07 x (sym eqx) ; remain<n = Factor<.remain<n x }
|
|
|
993 record { factor = fy ; remain = Factor<.remain y ; is-factor = lem07 y (sym eqy) ; remain<n = Factor<.remain<n y }
|
|
|
994 ... | ⟪ eqf , eqr ⟫ = ⟪ cong suc eqf , eqr ⟫
|
|
|
995 decl : {m : ℕ } → 0 < m → m - k < m
|
|
|
996 decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m
|
|
|
997 I : Ninduction ℕ _ F
|
|
|
998 I = record {
|
|
|
999 pnext = λ p → p - k
|
|
|
1000 ; fzero = λ {m} eq → F0 m eq
|
|
|
1001 ; decline = λ {m} lt → decl lt
|
|
|
1002 ; ind = λ {p} prev → ind prev
|
|
|
1003 }
|
|
|
1004
|
|
|
1005 F<toD : {n m : ℕ} → (fc : Factor< n m) → Factor<.remain fc ≡ 0 → Dividable n m
|
|
|
1006 F<toD {n} {m} record { factor = f ; remain = r ; is-factor = fa ; remain<n = _ } refl
|
|
|
1007 = record { factor = f ; is-factor = fa }
|
|
|
1008
|
|
|
1009 DtoF< : {n m : ℕ} → Dividable n m → 0 < n → Factor< n m
|
|
|
1010 DtoF< {n} {m} record { factor = f ; is-factor = fa } 0<n = record { factor = f ; is-factor = fa ; remain = 0 ; remain<n = 0<n }
|
|
|
1011
|
|
|
1012 F<to¬D : {n m nx : ℕ} → (fc : Factor< n m) → 1 < n → Factor<.remain fc ≡ suc nx → ¬ Dividable n m
|
|
|
1013 F<to¬D {n} {m} fc 1<n eq div = ⊥-elim ( nat-≡< (sym (proj2 ( Factor<-inject {n} {m} 1<n fc (DtoF< div (<-trans a<sa 1<n) )))) 0<r ) where
|
|
|
1014 0<r : 0 < Factor<.remain fc
|
|
|
1015 0<r = subst ( λ k → 0 < k ) (sym eq) (s≤s z≤n)
|
|
|
1016
|
|
|
1017 --
|
|
|
1018 -- we can use factor< and check Factor.remain ≡ 0
|
|
|
1019 -- Factor.remain ≡ 0 → Dividable k m
|
|
|
1020 -- ¬ Factor.remain ≡ 0 → ¬ Dividable k m
|
|
|
1021 --
|
|
|
1022 decD : {k m : ℕ} → k > 1 → Dec0 (Dividable k m )
|
|
|
1023 decD {k} {m} k>1 = dec0 (factor< {k} {m} k>1) where
|
|
|
1024 dec0 : Factor< k m → Dec0 (Dividable k m)
|
|
|
1025 dec0 fc with Factor<.remain fc in eq1
|
|
|
1026 ... | zero = yes0 record { factor = Factor<.factor fc ; is-factor = trans (cong (λ j → Factor<.factor fc * k + j) (sym eq1)) (Factor<.is-factor fc) }
|
|
|
1027 ... | suc t = no0 ( λ dv → F<to¬D fc k>1 eq1 dv )
|
|
|
1028
|
|
|
1029
|
|
|
1030
|
