Mercurial > hg > Members > kono > Proof > galois
annotate src/nat.agda @ 331:ee6b8f4cbf4c default tip
safe mode
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 08 Jul 2024 16:48:09 +0900 |
| parents | fff18d4a063b |
| children |
| rev | line source |
|---|---|
|
318
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
314
diff
changeset
|
1 {-# OPTIONS --cubical-compatible --safe #-} |
|
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
314
diff
changeset
|
2 |
| 72 | 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 | |
| 314 | 11 open import Relation.Binary.Definitions |
| 72 | 12 open import logic |
| 314 | 13 open import Level hiding ( zero ; suc ) |
| 72 | 14 |
| 15 nat-<> : { x y : ℕ } → x < y → y < x → ⊥ | |
| 16 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x | |
| 17 | |
| 18 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ | |
| 19 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x | |
| 20 | |
| 21 nat-<≡ : { x : ℕ } → x < x → ⊥ | |
| 22 nat-<≡ (s≤s lt) = nat-<≡ lt | |
| 23 | |
| 24 nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥ | |
| 25 nat-≡< refl lt = nat-<≡ lt | |
| 26 | |
| 27 ¬a≤a : {la : ℕ} → suc la ≤ la → ⊥ | |
| 28 ¬a≤a (s≤s lt) = ¬a≤a lt | |
| 29 | |
| 30 a<sa : {la : ℕ} → la < suc la | |
| 31 a<sa {zero} = s≤s z≤n | |
| 32 a<sa {suc la} = s≤s a<sa | |
| 33 | |
| 34 =→¬< : {x : ℕ } → ¬ ( x < x ) | |
| 35 =→¬< {zero} () | |
| 36 =→¬< {suc x} (s≤s lt) = =→¬< lt | |
| 37 | |
| 38 >→¬< : {x y : ℕ } → (x < y ) → ¬ ( y < x ) | |
| 39 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x | |
| 40 | |
| 41 <-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) ) | |
| 42 <-∨ {zero} {zero} (s≤s z≤n) = case1 refl | |
| 43 <-∨ {zero} {suc y} (s≤s lt) = case2 (s≤s z≤n) | |
| 44 <-∨ {suc x} {zero} (s≤s ()) | |
| 45 <-∨ {suc x} {suc y} (s≤s lt) with <-∨ {x} {y} lt | |
| 46 <-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq) | |
| 47 <-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1) | |
| 48 | |
| 314 | 49 ≤-∨ : { x y : ℕ } → x ≤ y → ( (x ≡ y ) ∨ (x < y) ) |
| 50 ≤-∨ {zero} {zero} z≤n = case1 refl | |
| 51 ≤-∨ {zero} {suc y} z≤n = case2 (s≤s z≤n) | |
| 52 ≤-∨ {suc x} {zero} () | |
| 53 ≤-∨ {suc x} {suc y} (s≤s lt) with ≤-∨ {x} {y} lt | |
| 54 ≤-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq) | |
| 55 ≤-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1) | |
| 210 | 56 |
| 72 | 57 max : (x y : ℕ) → ℕ |
| 58 max zero zero = zero | |
| 59 max zero (suc x) = (suc x) | |
| 60 max (suc x) zero = (suc x) | |
| 61 max (suc x) (suc y) = suc ( max x y ) | |
| 62 | |
| 314 | 63 x≤max : (x y : ℕ) → x ≤ max x y |
| 64 x≤max zero zero = ≤-refl | |
| 65 x≤max zero (suc x) = z≤n | |
| 66 x≤max (suc x) zero = ≤-refl | |
| 67 x≤max (suc x) (suc y) = s≤s( x≤max x y ) | |
| 68 | |
| 69 y≤max : (x y : ℕ) → y ≤ max x y | |
| 70 y≤max zero zero = ≤-refl | |
| 71 y≤max zero (suc x) = ≤-refl | |
| 72 y≤max (suc x) zero = z≤n | |
| 73 y≤max (suc x) (suc y) = s≤s( y≤max x y ) | |
| 74 | |
| 75 x≤y→max=y : (x y : ℕ) → x ≤ y → max x y ≡ y | |
| 76 x≤y→max=y zero zero x≤y = refl | |
| 77 x≤y→max=y zero (suc y) x≤y = refl | |
| 78 x≤y→max=y (suc x) (suc y) (s≤s x≤y) = cong suc (x≤y→max=y x y x≤y ) | |
| 79 | |
| 80 y≤x→max=x : (x y : ℕ) → y ≤ x → max x y ≡ x | |
| 81 y≤x→max=x zero zero y≤x = refl | |
| 82 y≤x→max=x zero (suc y) () | |
| 83 y≤x→max=x (suc x) zero lt = refl | |
| 84 y≤x→max=x (suc x) (suc y) (s≤s y≤x) = cong suc (y≤x→max=x x y y≤x ) | |
| 85 | |
| 72 | 86 -- _*_ : ℕ → ℕ → ℕ |
| 87 -- _*_ zero _ = zero | |
| 88 -- _*_ (suc n) m = m + ( n * m ) | |
| 89 | |
| 314 | 90 -- x ^ y |
| 72 | 91 exp : ℕ → ℕ → ℕ |
| 92 exp _ zero = 1 | |
| 93 exp n (suc m) = n * ( exp n m ) | |
| 94 | |
| 314 | 95 div2 : ℕ → (ℕ ∧ Bool ) |
| 96 div2 zero = ⟪ 0 , false ⟫ | |
| 97 div2 (suc zero) = ⟪ 0 , true ⟫ | |
| 98 div2 (suc (suc n)) = ⟪ suc (proj1 (div2 n)) , proj2 (div2 n) ⟫ where | |
| 99 open _∧_ | |
| 100 | |
| 101 div2-rev : (ℕ ∧ Bool ) → ℕ | |
| 102 div2-rev ⟪ x , true ⟫ = suc (x + x) | |
| 103 div2-rev ⟪ x , false ⟫ = x + x | |
| 104 | |
| 105 div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ x | |
| 106 div2-eq zero = refl | |
| 107 div2-eq (suc zero) = refl | |
|
318
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
314
diff
changeset
|
108 div2-eq (suc (suc x)) with div2 x in eq1 |
|
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
314
diff
changeset
|
109 ... | ⟪ x1 , true ⟫ = begin -- eq1 : div2 x ≡ ⟪ x1 , true ⟫ |
| 314 | 110 div2-rev ⟪ suc x1 , true ⟫ ≡⟨⟩ |
| 111 suc (suc (x1 + suc x1)) ≡⟨ cong (λ k → suc (suc k )) (+-comm x1 _ ) ⟩ | |
| 112 suc (suc (suc (x1 + x1))) ≡⟨⟩ | |
| 113 suc (suc (div2-rev ⟪ x1 , true ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩ | |
| 114 suc (suc (div2-rev (div2 x))) ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩ | |
| 115 suc (suc x) ∎ where open ≡-Reasoning | |
|
318
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
314
diff
changeset
|
116 ... | ⟪ x1 , false ⟫ = begin |
| 314 | 117 div2-rev ⟪ suc x1 , false ⟫ ≡⟨⟩ |
| 118 suc (x1 + suc x1) ≡⟨ cong (λ k → (suc k )) (+-comm x1 _ ) ⟩ | |
| 119 suc (suc (x1 + x1)) ≡⟨⟩ | |
| 120 suc (suc (div2-rev ⟪ x1 , false ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩ | |
| 121 suc (suc (div2-rev (div2 x))) ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩ | |
| 122 suc (suc x) ∎ where open ≡-Reasoning | |
| 123 | |
| 124 sucprd : {i : ℕ } → 0 < i → suc (pred i) ≡ i | |
| 125 sucprd {suc i} 0<i = refl | |
| 126 | |
| 127 0<s : {x : ℕ } → zero < suc x | |
| 128 0<s {_} = s≤s z≤n | |
| 129 | |
| 130 px<py : {x y : ℕ } → pred x < pred y → x < y | |
| 131 px<py {zero} {suc y} lt = 0<s | |
| 132 px<py {suc zero} {suc (suc y)} (s≤s lt) = s≤s 0<s | |
| 133 px<py {suc (suc x)} {suc (suc y)} (s≤s lt) = s≤s (px<py {suc x} {suc y} lt) | |
| 134 | |
| 72 | 135 minus : (a b : ℕ ) → ℕ |
| 136 minus a zero = a | |
| 137 minus zero (suc b) = zero | |
| 138 minus (suc a) (suc b) = minus a b | |
| 139 | |
| 140 _-_ = minus | |
| 141 | |
| 314 | 142 sn-m=sn-m : {m n : ℕ } → m ≤ n → suc n - m ≡ suc ( n - m ) |
| 143 sn-m=sn-m {0} {n} z≤n = refl | |
| 144 sn-m=sn-m {suc m} {suc n} (s≤s m<n) = sn-m=sn-m m<n | |
| 145 | |
| 146 si-sn=i-n : {i n : ℕ } → n < i → suc (i - suc n) ≡ (i - n) | |
| 147 si-sn=i-n {i} {n} n<i = begin | |
| 148 suc (i - suc n) ≡⟨ sym (sn-m=sn-m n<i ) ⟩ | |
| 149 suc i - suc n ≡⟨⟩ | |
| 150 i - n | |
| 151 ∎ where | |
| 152 open ≡-Reasoning | |
| 153 | |
| 154 refl-≤s : {x : ℕ } → x ≤ suc x | |
| 155 refl-≤s {zero} = z≤n | |
| 156 refl-≤s {suc x} = s≤s (refl-≤s {x}) | |
| 157 | |
| 158 a≤sa = refl-≤s | |
| 159 | |
| 160 n-m<n : (n m : ℕ ) → n - m ≤ n | |
| 161 n-m<n zero zero = z≤n | |
| 162 n-m<n (suc n) zero = s≤s (n-m<n n zero) | |
| 163 n-m<n zero (suc m) = z≤n | |
| 164 n-m<n (suc n) (suc m) = ≤-trans (n-m<n n m ) refl-≤s | |
| 165 | |
| 166 n-n-m=m : {m n : ℕ } → m ≤ n → m ≡ (n - (n - m)) | |
| 167 n-n-m=m {0} {zero} z≤n = refl | |
| 168 n-n-m=m {0} {suc n} z≤n = n-n-m=m {0} {n} z≤n | |
| 169 n-n-m=m {suc m} {suc n} (s≤s m≤n) = sym ( begin | |
| 170 suc n - ( n - m ) ≡⟨ sn-m=sn-m (n-m<n n m) ⟩ | |
| 171 suc (n - ( n - m )) ≡⟨ cong (λ k → suc k ) (sym (n-n-m=m m≤n)) ⟩ | |
| 172 suc m | |
| 173 ∎ ) where | |
| 174 open ≡-Reasoning | |
| 175 | |
| 72 | 176 m+= : {i j m : ℕ } → m + i ≡ m + j → i ≡ j |
| 177 m+= {i} {j} {zero} refl = refl | |
| 178 m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq ) | |
| 179 | |
| 180 +m= : {i j m : ℕ } → i + m ≡ j + m → i ≡ j | |
| 181 +m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq ) | |
| 182 | |
| 183 less-1 : { n m : ℕ } → suc n < m → n < m | |
| 184 less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n | |
| 185 less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt) | |
| 186 | |
| 187 sa=b→a<b : { n m : ℕ } → suc n ≡ m → n < m | |
| 188 sa=b→a<b {0} {suc zero} refl = s≤s z≤n | |
| 189 sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl) | |
| 190 | |
| 191 minus+n : {x y : ℕ } → suc x > y → minus x y + y ≡ x | |
| 192 minus+n {x} {zero} _ = trans (sym (+-comm zero _ )) refl | |
| 193 minus+n {zero} {suc y} (s≤s ()) | |
| 194 minus+n {suc x} {suc y} (s≤s lt) = begin | |
| 195 minus (suc x) (suc y) + suc y | |
| 196 ≡⟨ +-comm _ (suc y) ⟩ | |
| 197 suc y + minus x y | |
| 198 ≡⟨ cong ( λ k → suc k ) ( | |
| 199 begin | |
| 200 y + minus x y | |
| 201 ≡⟨ +-comm y _ ⟩ | |
| 202 minus x y + y | |
| 203 ≡⟨ minus+n {x} {y} lt ⟩ | |
| 204 x | |
| 205 ∎ | |
| 206 ) ⟩ | |
| 207 suc x | |
| 208 ∎ where open ≡-Reasoning | |
| 209 | |
| 210 <-minus-0 : {x y z : ℕ } → z + x < z + y → x < y | |
| 211 <-minus-0 {x} {suc _} {zero} lt = lt | |
| 212 <-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt | |
| 213 | |
| 214 <-minus : {x y z : ℕ } → x + z < y + z → x < y | |
| 215 <-minus {x} {y} {z} lt = <-minus-0 ( subst₂ ( λ j k → j < k ) (+-comm x _) (+-comm y _ ) lt ) | |
| 216 | |
| 217 x≤x+y : {z y : ℕ } → z ≤ z + y | |
| 218 x≤x+y {zero} {y} = z≤n | |
| 219 x≤x+y {suc z} {y} = s≤s (x≤x+y {z} {y}) | |
| 220 | |
| 314 | 221 x≤y+x : {z y : ℕ } → z ≤ y + z |
| 222 x≤y+x {z} {y} = subst (λ k → z ≤ k ) (+-comm _ y ) x≤x+y | |
| 223 | |
| 224 x≤x+sy : {x y : ℕ} → x < x + suc y | |
| 225 x≤x+sy {x} {y} = begin | |
| 226 suc x ≤⟨ x≤x+y ⟩ | |
| 227 suc x + y ≡⟨ cong (λ k → k + y) (+-comm 1 x ) ⟩ | |
| 228 (x + 1) + y ≡⟨ (+-assoc x 1 _) ⟩ | |
| 229 x + suc y ∎ where open ≤-Reasoning | |
| 230 | |
| 72 | 231 <-plus : {x y z : ℕ } → x < y → x + z < y + z |
| 232 <-plus {zero} {suc y} {z} (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y ) | |
| 233 <-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {x} {y} {z} lt) | |
| 234 | |
| 235 <-plus-0 : {x y z : ℕ } → x < y → z + x < z + y | |
| 236 <-plus-0 {x} {y} {z} lt = subst₂ (λ j k → j < k ) (+-comm _ z) (+-comm _ z) ( <-plus {x} {y} {z} lt ) | |
| 237 | |
| 238 ≤-plus : {x y z : ℕ } → x ≤ y → x + z ≤ y + z | |
| 239 ≤-plus {0} {y} {zero} z≤n = z≤n | |
| 240 ≤-plus {0} {y} {suc z} z≤n = subst (λ k → z < k ) (+-comm _ y ) x≤x+y | |
| 241 ≤-plus {suc x} {suc y} {z} (s≤s lt) = s≤s ( ≤-plus {x} {y} {z} lt ) | |
| 242 | |
| 243 ≤-plus-0 : {x y z : ℕ } → x ≤ y → z + x ≤ z + y | |
| 244 ≤-plus-0 {x} {y} {zero} lt = lt | |
| 245 ≤-plus-0 {x} {y} {suc z} lt = s≤s ( ≤-plus-0 {x} {y} {z} lt ) | |
| 246 | |
| 247 x+y<z→x<z : {x y z : ℕ } → x + y < z → x < z | |
| 248 x+y<z→x<z {zero} {y} {suc z} (s≤s lt1) = s≤s z≤n | |
| 249 x+y<z→x<z {suc x} {y} {suc z} (s≤s lt1) = s≤s ( x+y<z→x<z {x} {y} {z} lt1 ) | |
| 250 | |
| 251 *≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z | |
| 252 *≤ lt = *-mono-≤ lt ≤-refl | |
| 253 | |
| 254 *< : {x y z : ℕ } → x < y → x * suc z < y * suc z | |
| 255 *< {zero} {suc y} lt = s≤s z≤n | |
| 256 *< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt) | |
| 257 | |
| 258 <to<s : {x y : ℕ } → x < y → x < suc y | |
| 259 <to<s {zero} {suc y} (s≤s lt) = s≤s z≤n | |
| 260 <to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt) | |
| 261 | |
| 262 <tos<s : {x y : ℕ } → x < y → suc x < suc y | |
| 263 <tos<s {zero} {suc y} (s≤s z≤n) = s≤s (s≤s z≤n) | |
| 264 <tos<s {suc x} {suc y} (s≤s lt) = s≤s (<tos<s {x} {y} lt) | |
| 265 | |
| 314 | 266 <to≤ : {x y : ℕ } → x < y → x ≤ y |
| 267 <to≤ {zero} {suc y} (s≤s z≤n) = z≤n | |
| 268 <to≤ {suc x} {suc y} (s≤s lt) = s≤s (<to≤ {x} {y} lt) | |
| 269 | |
| 270 <∨≤ : ( x y : ℕ ) → (x < y ) ∨ (y ≤ x) | |
| 271 <∨≤ x y with <-cmp x y | |
| 272 ... | tri< a ¬b ¬c = case1 a | |
| 273 ... | tri≈ ¬a refl ¬c = case2 ≤-refl | |
| 274 ... | tri> ¬a ¬b c = case2 (<to≤ c) | |
| 275 | |
| 276 refl-≤ : {x : ℕ } → x ≤ x | |
| 277 refl-≤ {zero} = z≤n | |
| 278 refl-≤ {suc x} = s≤s (refl-≤ {x}) | |
| 279 | |
| 280 refl-≤≡ : {x y : ℕ } → x ≡ y → x ≤ y | |
| 281 refl-≤≡ refl = refl-≤ | |
| 72 | 282 |
| 283 x<y→≤ : {x y : ℕ } → x < y → x ≤ suc y | |
| 284 x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n | |
| 285 x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt) | |
| 286 | |
| 314 | 287 ≤→= : {i j : ℕ} → i ≤ j → j ≤ i → i ≡ j |
| 288 ≤→= {0} {0} z≤n z≤n = refl | |
| 289 ≤→= {suc i} {suc j} (s≤s i<j) (s≤s j<i) = cong suc ( ≤→= {i} {j} i<j j<i ) | |
| 290 | |
| 291 px≤x : {x : ℕ } → pred x ≤ x | |
| 292 px≤x {zero} = refl-≤ | |
| 293 px≤x {suc x} = refl-≤s | |
| 294 | |
| 295 px≤py : {x y : ℕ } → x ≤ y → pred x ≤ pred y | |
| 296 px≤py {zero} {zero} lt = refl-≤ | |
| 297 px≤py {zero} {suc y} lt = z≤n | |
| 298 px≤py {suc x} {suc y} (s≤s lt) = lt | |
| 299 | |
| 300 sx≤py→x≤y : {x y : ℕ } → suc x ≤ suc y → x ≤ y | |
| 301 sx≤py→x≤y (s≤s lt) = lt | |
| 302 | |
| 303 sx<py→x<y : {x y : ℕ } → suc x < suc y → x < y | |
| 304 sx<py→x<y (s≤s lt) = lt | |
| 305 | |
| 306 sx≤y→x≤y : {x y : ℕ } → suc x ≤ y → x ≤ y | |
| 307 sx≤y→x≤y {zero} {suc y} (s≤s le) = z≤n | |
| 308 sx≤y→x≤y {suc x} {suc y} (s≤s le) = s≤s (sx≤y→x≤y {x} {y} le) | |
| 309 | |
| 310 x<sy→x≤y : {x y : ℕ } → x < suc y → x ≤ y | |
| 311 x<sy→x≤y {zero} {suc y} (s≤s le) = z≤n | |
| 312 x<sy→x≤y {suc x} {suc y} (s≤s le) = s≤s (x<sy→x≤y {x} {y} le) | |
| 313 x<sy→x≤y {zero} {zero} (s≤s z≤n) = ≤-refl | |
| 314 | |
| 315 x≤y→x<sy : {x y : ℕ } → x ≤ y → x < suc y | |
| 316 x≤y→x<sy {.zero} {y} z≤n = ≤-trans a<sa (s≤s z≤n) | |
| 317 x≤y→x<sy {.(suc _)} {.(suc _)} (s≤s le) = s≤s ( x≤y→x<sy le) | |
| 318 | |
| 319 sx≤y→x<y : {x y : ℕ } → suc x ≤ y → x < y | |
| 320 sx≤y→x<y {zero} {suc y} (s≤s le) = s≤s z≤n | |
| 321 sx≤y→x<y {suc x} {suc y} (s≤s le) = s≤s ( sx≤y→x<y {x} {y} le ) | |
| 322 | |
| 72 | 323 open import Data.Product |
| 324 | |
| 314 | 325 i-j=0→i=j : {i j : ℕ } → j ≤ i → i - j ≡ 0 → i ≡ j |
| 326 i-j=0→i=j {zero} {zero} _ refl = refl | |
| 327 i-j=0→i=j {zero} {suc j} () refl | |
| 328 i-j=0→i=j {suc i} {zero} z≤n () | |
| 329 i-j=0→i=j {suc i} {suc j} (s≤s lt) eq = cong suc (i-j=0→i=j {i} {j} lt eq) | |
| 330 | |
| 331 m*n=0⇒m=0∨n=0 : {i j : ℕ} → i * j ≡ 0 → (i ≡ 0) ∨ ( j ≡ 0 ) | |
| 332 m*n=0⇒m=0∨n=0 {zero} {j} refl = case1 refl | |
| 333 m*n=0⇒m=0∨n=0 {suc i} {zero} eq = case2 refl | |
| 334 | |
| 335 | |
| 336 minus+1 : {x y : ℕ } → y ≤ x → suc (minus x y) ≡ minus (suc x) y | |
| 337 minus+1 {zero} {zero} y≤x = refl | |
| 338 minus+1 {suc x} {zero} y≤x = refl | |
| 339 minus+1 {suc x} {suc y} (s≤s y≤x) = minus+1 {x} {y} y≤x | |
| 340 | |
| 341 minus+yz : {x y z : ℕ } → z ≤ y → x + minus y z ≡ minus (x + y) z | |
| 342 minus+yz {zero} {y} {z} _ = refl | |
| 343 minus+yz {suc x} {y} {z} z≤y = begin | |
| 344 suc x + minus y z ≡⟨ cong suc ( minus+yz z≤y ) ⟩ | |
| 345 suc (minus (x + y) z) ≡⟨ minus+1 {x + y} {z} (≤-trans z≤y (subst (λ g → y ≤ g) (+-comm y x) x≤x+y) ) ⟩ | |
| 346 minus (suc x + y) z ∎ where open ≡-Reasoning | |
| 347 | |
| 72 | 348 minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0 |
| 349 minus<=0 {0} {zero} z≤n = refl | |
| 350 minus<=0 {0} {suc y} z≤n = refl | |
| 351 minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le | |
| 352 | |
| 353 minus>0 : {x y : ℕ } → x < y → 0 < minus y x | |
| 354 minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n | |
| 355 minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt | |
| 356 | |
| 314 | 357 minus>0→x<y : {x y : ℕ } → 0 < minus y x → x < y |
| 358 minus>0→x<y {x} {y} lt with <-cmp x y | |
| 359 ... | tri< a ¬b ¬c = a | |
| 360 ... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-≡< (sym (minus<=0 {x} ≤-refl)) lt ) | |
| 361 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym (minus<=0 {y} (≤-trans refl-≤s c ))) lt ) | |
| 362 | |
| 363 minus+y-y : {x y : ℕ } → (x + y) - y ≡ x | |
| 364 minus+y-y {zero} {y} = minus<=0 {zero + y} {y} ≤-refl | |
| 365 minus+y-y {suc x} {y} = begin | |
| 366 (suc x + y) - y ≡⟨ sym (minus+1 {_} {y} x≤y+x) ⟩ | |
| 367 suc ((x + y) - y) ≡⟨ cong suc (minus+y-y {x} {y}) ⟩ | |
| 368 suc x ∎ where open ≡-Reasoning | |
| 369 | |
| 370 minus+yx-yz : {x y z : ℕ } → (y + x) - (y + z) ≡ x - z | |
| 371 minus+yx-yz {x} {zero} {z} = refl | |
| 372 minus+yx-yz {x} {suc y} {z} = minus+yx-yz {x} {y} {z} | |
| 373 | |
| 374 minus+xy-zy : {x y z : ℕ } → (x + y) - (z + y) ≡ x - z | |
| 375 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}) | |
| 376 | |
| 377 +cancel<l : (x z : ℕ ) {y : ℕ} → y + x < y + z → x < z | |
| 378 +cancel<l x z {zero} lt = lt | |
| 379 +cancel<l x z {suc y} (s≤s lt) = +cancel<l x z {y} lt | |
| 380 | |
| 381 +cancel<r : (x z : ℕ ) {y : ℕ} → x + y < z + y → x < z | |
| 382 +cancel<r x z {y} lt = +cancel<l x z (subst₂ (λ j k → j < k ) (+-comm x _) (+-comm z _) lt ) | |
| 383 | |
| 384 y-x<y : {x y : ℕ } → 0 < x → 0 < y → y - x < y | |
| 385 y-x<y {x} {y} 0<x 0<y with <-cmp x (suc y) | |
| 386 ... | tri< a ¬b ¬c = +cancel<r (y - x) _ ( begin | |
| 387 suc ((y - x) + x) ≡⟨ cong suc (minus+n {y} {x} a ) ⟩ | |
| 388 suc y ≡⟨ +-comm 1 _ ⟩ | |
| 389 y + suc 0 ≤⟨ +-mono-≤ ≤-refl 0<x ⟩ | |
| 390 y + x ∎ ) where open ≤-Reasoning | |
| 391 ... | tri≈ ¬a refl ¬c = subst ( λ k → k < y ) (sym (minus<=0 {y} {x} refl-≤s )) 0<y | |
| 392 ... | 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 | |
| 393 | |
| 394 open import Relation.Binary.Definitions | |
| 395 | |
| 72 | 396 distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) |
| 397 distr-minus-* {x} {zero} {z} = refl | |
| 398 distr-minus-* {x} {suc y} {z} with <-cmp x y | |
| 399 distr-minus-* {x} {suc y} {z} | tri< a ¬b ¬c = begin | |
| 400 minus x (suc y) * z | |
| 401 ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} (x<y→≤ a)) ⟩ | |
| 402 0 * z | |
| 403 ≡⟨ sym (minus<=0 {x * z} {z + y * z} le ) ⟩ | |
| 404 minus (x * z) (z + y * z) | |
| 405 ∎ where | |
| 406 open ≡-Reasoning | |
| 407 le : x * z ≤ z + y * z | |
| 408 le = ≤-trans lemma (subst (λ k → y * z ≤ k ) (+-comm _ z ) (x≤x+y {y * z} {z} ) ) where | |
| 409 lemma : x * z ≤ y * z | |
| 314 | 410 lemma = *≤ {x} {y} {z} (<to≤ a) |
| 72 | 411 distr-minus-* {x} {suc y} {z} | tri≈ ¬a refl ¬c = begin |
| 412 minus x (suc y) * z | |
| 413 ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} refl-≤s ) ⟩ | |
| 414 0 * z | |
| 415 ≡⟨ sym (minus<=0 {x * z} {z + y * z} (lt {x} {z} )) ⟩ | |
| 416 minus (x * z) (z + y * z) | |
| 417 ∎ where | |
| 418 open ≡-Reasoning | |
| 419 lt : {x z : ℕ } → x * z ≤ z + x * z | |
| 420 lt {zero} {zero} = z≤n | |
| 421 lt {suc x} {zero} = lt {x} {zero} | |
| 422 lt {x} {suc z} = ≤-trans lemma refl-≤s where | |
| 423 lemma : x * suc z ≤ z + x * suc z | |
| 424 lemma = subst (λ k → x * suc z ≤ k ) (+-comm _ z) (x≤x+y {x * suc z} {z}) | |
| 425 distr-minus-* {x} {suc y} {z} | tri> ¬a ¬b c = +m= {_} {_} {suc y * z} ( begin | |
| 426 minus x (suc y) * z + suc y * z | |
| 427 ≡⟨ sym (proj₂ *-distrib-+ z (minus x (suc y) ) _) ⟩ | |
| 428 ( minus x (suc y) + suc y ) * z | |
| 429 ≡⟨ cong (λ k → k * z) (minus+n {x} {suc y} (s≤s c)) ⟩ | |
| 430 x * z | |
| 431 ≡⟨ sym (minus+n {x * z} {suc y * z} (s≤s (lt c))) ⟩ | |
| 432 minus (x * z) (suc y * z) + suc y * z | |
| 433 ∎ ) where | |
| 434 open ≡-Reasoning | |
| 435 lt : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z | |
| 436 lt {x} {y} {z} le = *≤ le | |
| 437 | |
| 314 | 438 distr-minus-*' : {z x y : ℕ } → z * (minus x y) ≡ minus (z * x) (z * y) |
| 439 distr-minus-*' {z} {x} {y} = begin | |
| 440 z * (minus x y) ≡⟨ *-comm _ (x - y) ⟩ | |
| 441 (minus x y) * z ≡⟨ distr-minus-* {x} {y} {z} ⟩ | |
| 442 minus (x * z) (y * z) ≡⟨ cong₂ (λ j k → j - k ) (*-comm x z ) (*-comm y z) ⟩ | |
| 443 minus (z * x) (z * y) ∎ where open ≡-Reasoning | |
| 444 | |
| 72 | 445 minus- : {x y z : ℕ } → suc x > z + y → minus (minus x y) z ≡ minus x (y + z) |
| 446 minus- {x} {y} {z} gt = +m= {_} {_} {z} ( begin | |
| 447 minus (minus x y) z + z | |
| 448 ≡⟨ minus+n {_} {z} lemma ⟩ | |
| 449 minus x y | |
| 450 ≡⟨ +m= {_} {_} {y} ( begin | |
| 451 minus x y + y | |
| 452 ≡⟨ minus+n {_} {y} lemma1 ⟩ | |
| 453 x | |
| 454 ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩ | |
| 455 minus x (z + y) + (z + y) | |
| 456 ≡⟨ sym ( +-assoc (minus x (z + y)) _ _ ) ⟩ | |
| 457 minus x (z + y) + z + y | |
| 458 ∎ ) ⟩ | |
| 459 minus x (z + y) + z | |
| 460 ≡⟨ cong (λ k → minus x k + z ) (+-comm _ y ) ⟩ | |
| 461 minus x (y + z) + z | |
| 462 ∎ ) where | |
| 463 open ≡-Reasoning | |
| 464 lemma1 : suc x > y | |
| 465 lemma1 = x+y<z→x<z (subst (λ k → k < suc x ) (+-comm z _ ) gt ) | |
| 466 lemma : suc (minus x y) > z | |
| 467 lemma = <-minus {_} {_} {y} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y} lemma1 )) gt ) | |
| 468 | |
| 469 minus-* : {M k n : ℕ } → n < k → minus k (suc n) * M ≡ minus (minus k n * M ) M | |
| 470 minus-* {zero} {k} {n} lt = begin | |
| 471 minus k (suc n) * zero | |
| 472 ≡⟨ *-comm (minus k (suc n)) zero ⟩ | |
| 473 zero * minus k (suc n) | |
| 474 ≡⟨⟩ | |
| 475 0 * minus k n | |
| 476 ≡⟨ *-comm 0 (minus k n) ⟩ | |
| 477 minus (minus k n * 0 ) 0 | |
| 478 ∎ where | |
| 479 open ≡-Reasoning | |
| 480 minus-* {suc m} {k} {n} lt with <-cmp k 1 | |
| 481 minus-* {suc m} {.0} {zero} lt | tri< (s≤s z≤n) ¬b ¬c = refl | |
| 482 minus-* {suc m} {.0} {suc n} lt | tri< (s≤s z≤n) ¬b ¬c = refl | |
| 483 minus-* {suc zero} {.1} {zero} lt | tri≈ ¬a refl ¬c = refl | |
| 484 minus-* {suc (suc m)} {.1} {zero} lt | tri≈ ¬a refl ¬c = minus-* {suc m} {1} {zero} lt | |
| 485 minus-* {suc m} {.1} {suc n} (s≤s ()) | tri≈ ¬a refl ¬c | |
| 486 minus-* {suc m} {k} {n} lt | tri> ¬a ¬b c = begin | |
| 487 minus k (suc n) * M | |
| 488 ≡⟨ distr-minus-* {k} {suc n} {M} ⟩ | |
| 489 minus (k * M ) ((suc n) * M) | |
| 490 ≡⟨⟩ | |
| 491 minus (k * M ) (M + n * M ) | |
| 492 ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩ | |
| 493 minus (k * M ) ((n * M) + M ) | |
| 494 ≡⟨ sym ( minus- {k * M} {n * M} (lemma lt) ) ⟩ | |
| 495 minus (minus (k * M ) (n * M)) M | |
| 496 ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩ | |
| 497 minus (minus k n * M ) M | |
| 498 ∎ where | |
| 499 M = suc m | |
| 500 lemma : {n k m : ℕ } → n < k → suc (k * suc m) > suc m + n * suc m | |
| 501 lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y )) | |
| 502 lemma {suc n} {suc k} {m} lt = begin | |
| 503 suc (suc m + suc n * suc m) | |
| 504 ≡⟨⟩ | |
| 505 suc ( suc (suc n) * suc m) | |
| 506 ≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩ | |
| 507 suc (suc k * suc m) | |
| 508 ∎ where open ≤-Reasoning | |
| 509 open ≡-Reasoning | |
| 112 | 510 |
| 314 | 511 x=y+z→x-z=y : {x y z : ℕ } → x ≡ y + z → x - z ≡ y |
| 512 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 | |
| 513 x=y+z→x-z=y {suc x} {suc y} {zero} eq = begin -- suc x ≡ suc (y + zero) → (suc x - zero) ≡ suc y | |
| 514 suc x - zero ≡⟨ refl ⟩ | |
| 515 suc x ≡⟨ eq ⟩ | |
| 516 suc y + zero ≡⟨ +-comm _ zero ⟩ | |
| 517 suc y ∎ where open ≡-Reasoning | |
| 518 x=y+z→x-z=y {suc x} {suc y} {suc z} eq = x=y+z→x-z=y {x} {suc y} {z} ( begin | |
| 519 x ≡⟨ cong pred eq ⟩ | |
| 520 pred (suc y + suc z) ≡⟨ +-comm _ (suc z) ⟩ | |
| 521 suc z + y ≡⟨ cong suc ( +-comm _ y ) ⟩ | |
| 522 suc y + z ∎ ) where open ≡-Reasoning | |
| 523 | |
| 524 m*1=m : {m : ℕ } → m * 1 ≡ m | |
| 525 m*1=m {zero} = refl | |
| 526 m*1=m {suc m} = cong suc m*1=m | |
| 527 | |
| 528 +-cancel-1 : (x y z : ℕ ) → x + y ≡ x + z → y ≡ z | |
| 529 +-cancel-1 zero y z eq = eq | |
| 530 +-cancel-1 (suc x) y z eq = +-cancel-1 x y z (cong pred eq ) | |
| 531 | |
| 532 +-cancel-0 : (x y z : ℕ ) → y + x ≡ z + x → y ≡ z | |
| 533 +-cancel-0 x y z eq = +-cancel-1 x y z (trans (+-comm x y) (trans eq (sym (+-comm x z)) )) | |
| 534 | |
| 535 *-cancel-left : {x y z : ℕ } → x > 0 → x * y ≡ x * z → y ≡ z | |
| 536 *-cancel-left {suc x} {zero} {zero} lt eq = refl | |
| 537 *-cancel-left {suc x} {zero} {suc z} lt eq = ⊥-elim ( nat-≡< eq (s≤s (begin | |
| 538 x * zero ≡⟨ *-comm x _ ⟩ | |
| 539 zero ≤⟨ z≤n ⟩ | |
| 540 z + x * suc z ∎ ))) where open ≤-Reasoning | |
| 541 *-cancel-left {suc x} {suc y} {zero} lt eq = ⊥-elim ( nat-≡< (sym eq) (s≤s (begin | |
| 542 x * zero ≡⟨ *-comm x _ ⟩ | |
| 543 zero ≤⟨ z≤n ⟩ | |
| 544 _ ∎ ))) where open ≤-Reasoning | |
| 545 *-cancel-left {suc x} {suc y} {suc z} lt eq with cong pred eq | |
| 546 ... | eq1 = cong suc (*-cancel-left {suc x} {y} {z} lt (+-cancel-0 x _ _ (begin | |
| 547 y + x * y + x ≡⟨ +-assoc y _ _ ⟩ | |
| 548 y + (x * y + x) ≡⟨ cong (λ k → y + (k + x)) (*-comm x _) ⟩ | |
| 549 y + (y * x + x) ≡⟨ cong (_+_ y) (+-comm _ x) ⟩ | |
| 550 y + (x + y * x ) ≡⟨ refl ⟩ | |
| 551 y + suc y * x ≡⟨ cong (_+_ y) (*-comm (suc y) _) ⟩ | |
| 552 y + x * suc y ≡⟨ eq1 ⟩ | |
| 553 z + x * suc z ≡⟨ refl ⟩ | |
| 554 _ ≡⟨ sym ( cong (_+_ z) (*-comm (suc z) _) ) ⟩ | |
| 555 _ ≡⟨ sym ( cong (_+_ z) (+-comm _ x)) ⟩ | |
| 556 z + (z * x + x) ≡⟨ sym ( cong (λ k → z + (k + x)) (*-comm x _) ) ⟩ | |
| 557 z + (x * z + x) ≡⟨ sym ( +-assoc z _ _) ⟩ | |
| 558 z + x * z + x ∎ ))) where open ≡-Reasoning | |
| 559 | |
| 560 record Finduction {n m : Level} (P : Set n ) (Q : P → Set m ) (f : P → ℕ) : Set (n Level.⊔ m) where | |
| 561 field | |
| 562 fzero : {p : P} → f p ≡ zero → Q p | |
| 563 pnext : (p : P ) → P | |
| 564 decline : {p : P} → 0 < f p → f (pnext p) < f p | |
| 565 ind : {p : P} → Q (pnext p) → Q p | |
| 566 | |
| 567 y<sx→y≤x : {x y : ℕ} → y < suc x → y ≤ x | |
| 568 y<sx→y≤x (s≤s lt) = lt | |
| 569 | |
| 570 fi0 : (x : ℕ) → x ≤ zero → x ≡ zero | |
| 571 fi0 .0 z≤n = refl | |
| 112 | 572 |
| 314 | 573 f-induction : {n m : Level} {P : Set n } → {Q : P → Set m } |
| 574 → (f : P → ℕ) | |
| 575 → Finduction P Q f | |
| 576 → (p : P ) → Q p | |
| 577 f-induction {n} {m} {P} {Q} f I p with <-cmp 0 (f p) | |
| 578 ... | tri> ¬a ¬b () | |
| 579 ... | tri≈ ¬a b ¬c = Finduction.fzero I (sym b) | |
| 580 ... | tri< lt _ _ = f-induction0 p (f p) (<to≤ (Finduction.decline I lt)) where | |
| 581 f-induction0 : (p : P) → (x : ℕ) → (f (Finduction.pnext I p)) ≤ x → Q p | |
| 582 f-induction0 p zero le = Finduction.ind I (Finduction.fzero I (fi0 _ le)) | |
| 583 f-induction0 p (suc x) le with <-cmp (f (Finduction.pnext I p)) (suc x) | |
| 584 ... | tri< (s≤s a) ¬b ¬c = f-induction0 p x a | |
| 585 ... | tri≈ ¬a b ¬c = Finduction.ind I (f-induction0 (Finduction.pnext I p) x (y<sx→y≤x f1)) where | |
| 586 f1 : f (Finduction.pnext I (Finduction.pnext I p)) < suc x | |
| 587 f1 = subst (λ k → f (Finduction.pnext I (Finduction.pnext I p)) < k ) b ( Finduction.decline I {Finduction.pnext I p} | |
| 588 (subst (λ k → 0 < k ) (sym b) (s≤s z≤n ) )) | |
| 589 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> le c ) | |
| 590 | |
| 591 | |
| 592 record Ninduction {n m : Level} (P : Set n ) (Q : P → Set m ) (f : P → ℕ) : Set (n Level.⊔ m) where | |
| 593 field | |
| 594 pnext : (p : P ) → P | |
| 595 fzero : {p : P} → f (pnext p) ≡ zero → Q p | |
| 596 decline : {p : P} → 0 < f p → f (pnext p) < f p | |
| 597 ind : {p : P} → Q (pnext p) → Q p | |
| 598 | |
| 599 s≤s→≤ : { i j : ℕ} → suc i ≤ suc j → i ≤ j | |
| 600 s≤s→≤ (s≤s lt) = lt | |
| 112 | 601 |
| 314 | 602 n-induction : {n m : Level} {P : Set n } → {Q : P → Set m } |
| 603 → (f : P → ℕ) | |
| 604 → Ninduction P Q f | |
| 605 → (p : P ) → Q p | |
| 606 n-induction {n} {m} {P} {Q} f I p = f-induction0 p (f (Ninduction.pnext I p)) ≤-refl where | |
| 607 f-induction0 : (p : P) → (x : ℕ) → (f (Ninduction.pnext I p)) ≤ x → Q p | |
| 608 f-induction0 p zero lt = Ninduction.fzero I {p} (fi0 _ lt) | |
| 609 f-induction0 p (suc x) le with <-cmp (f (Ninduction.pnext I p)) (suc x) | |
| 610 ... | tri< (s≤s a) ¬b ¬c = f-induction0 p x a | |
| 611 ... | tri≈ ¬a b ¬c = Ninduction.ind I (f-induction0 (Ninduction.pnext I p) x (s≤s→≤ nle) ) where | |
| 612 f>0 : 0 < f (Ninduction.pnext I p) | |
| 613 f>0 = subst (λ k → 0 < k ) (sym b) ( s≤s z≤n ) | |
| 614 nle : suc (f (Ninduction.pnext I (Ninduction.pnext I p))) ≤ suc x | |
| 615 nle = subst (λ k → suc (f (Ninduction.pnext I (Ninduction.pnext I p))) ≤ k) b (Ninduction.decline I {Ninduction.pnext I p} f>0 ) | |
| 616 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> le c ) | |
| 617 | |
| 618 | |
| 619 record Factor (n m : ℕ ) : Set where | |
| 620 field | |
| 621 factor : ℕ | |
| 622 remain : ℕ | |
| 623 is-factor : factor * n + remain ≡ m | |
| 624 | |
| 625 record Dividable (n m : ℕ ) : Set where | |
| 626 field | |
| 627 factor : ℕ | |
| 628 is-factor : factor * n + 0 ≡ m | |
| 629 | |
| 630 open Factor | |
| 631 | |
| 632 DtoF : {n m : ℕ} → Dividable n m → Factor n m | |
| 633 DtoF {n} {m} record { factor = f ; is-factor = fa } = record { factor = f ; remain = 0 ; is-factor = fa } | |
| 634 | |
| 635 FtoD : {n m : ℕ} → (fc : Factor n m) → remain fc ≡ 0 → Dividable n m | |
| 636 FtoD {n} {m} record { factor = f ; remain = r ; is-factor = fa } refl = record { factor = f ; is-factor = fa } | |
| 637 | |
| 638 --divdable^2 : ( n k : ℕ ) → Dividable k ( n * n ) → Dividable k n | |
| 639 --divdable^2 n k dn2 = {!!} | |
| 112 | 640 |
| 314 | 641 decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n |
| 642 decf {n} {k} record { factor = f ; remain = r ; is-factor = fa } = | |
| 643 decf1 {n} {k} f r fa where | |
| 644 decf1 : { n k : ℕ } → (f r : ℕ) → (f * k + r ≡ suc n) → Factor k n | |
| 645 decf1 {n} {k} f (suc r) fa = -- this case must be the first | |
| 646 record { factor = f ; remain = r ; is-factor = ( begin -- fa : f * k + suc r ≡ suc n | |
| 647 f * k + r ≡⟨ cong pred ( begin | |
| 648 suc ( f * k + r ) ≡⟨ +-comm _ r ⟩ | |
| 649 r + suc (f * k) ≡⟨ sym (+-assoc r 1 _) ⟩ | |
| 650 (r + 1) + f * k ≡⟨ cong (λ t → t + f * k ) (+-comm r 1) ⟩ | |
| 651 (suc r ) + f * k ≡⟨ +-comm (suc r) _ ⟩ | |
| 652 f * k + suc r ≡⟨ fa ⟩ | |
| 653 suc n ∎ ) ⟩ | |
| 654 n ∎ ) } where open ≡-Reasoning | |
| 655 decf1 {n} {zero} (suc f) zero fa = ⊥-elim ( nat-≡< fa ( | |
| 656 begin suc (suc f * zero + zero) ≡⟨ cong suc (+-comm _ zero) ⟩ | |
| 657 suc (f * 0) ≡⟨ cong suc (*-comm f zero) ⟩ | |
| 658 suc zero ≤⟨ s≤s z≤n ⟩ | |
| 659 suc n ∎ )) where open ≤-Reasoning | |
| 660 decf1 {n} {suc k} (suc f) zero fa = | |
| 661 record { factor = f ; remain = k ; is-factor = ( begin -- fa : suc (k + f * suc k + zero) ≡ suc n | |
| 662 f * suc k + k ≡⟨ +-comm _ k ⟩ | |
| 663 k + f * suc k ≡⟨ +-comm zero _ ⟩ | |
| 664 (k + f * suc k) + zero ≡⟨ cong pred fa ⟩ | |
| 665 n ∎ ) } where open ≡-Reasoning | |
| 666 | |
| 667 div0 : {k : ℕ} → Dividable k 0 | |
| 668 div0 {k} = record { factor = 0; is-factor = refl } | |
| 669 | |
| 670 div= : {k : ℕ} → Dividable k k | |
| 671 div= {k} = record { factor = 1; is-factor = ( begin | |
| 672 k + 0 * k + 0 ≡⟨ trans ( +-comm _ 0) ( +-comm _ 0) ⟩ | |
| 673 k ∎ ) } where open ≡-Reasoning | |
| 674 | |
| 675 div1 : { k : ℕ } → k > 1 → ¬ Dividable k 1 | |
| 676 div1 {k} k>1 record { factor = (suc f) ; is-factor = fa } = ⊥-elim ( nat-≡< (sym fa) ( begin | |
| 677 2 ≤⟨ k>1 ⟩ | |
| 678 k ≡⟨ +-comm 0 _ ⟩ | |
| 679 k + 0 ≡⟨ refl ⟩ | |
| 680 1 * k ≤⟨ *-mono-≤ {1} {suc f} (s≤s z≤n ) ≤-refl ⟩ | |
| 681 suc f * k ≡⟨ +-comm 0 _ ⟩ | |
| 682 suc f * k + 0 ∎ )) where open ≤-Reasoning | |
| 683 | |
| 684 div+div : { i j k : ℕ } → Dividable k i → Dividable k j → Dividable k (i + j) ∧ Dividable k (j + i) | |
| 685 div+div {i} {j} {k} di dj = ⟪ div+div1 , subst (λ g → Dividable k g) (+-comm i j) div+div1 ⟫ where | |
| 686 fki = Dividable.factor di | |
| 687 fkj = Dividable.factor dj | |
| 688 div+div1 : Dividable k (i + j) | |
| 689 div+div1 = record { factor = fki + fkj ; is-factor = ( begin | |
| 690 (fki + fkj) * k + 0 ≡⟨ +-comm _ 0 ⟩ | |
| 691 (fki + fkj) * k ≡⟨ *-distribʳ-+ k fki _ ⟩ | |
| 692 fki * k + fkj * k ≡⟨ cong₂ ( λ i j → i + j ) (+-comm 0 (fki * k)) (+-comm 0 (fkj * k)) ⟩ | |
| 693 (fki * k + 0) + (fkj * k + 0) ≡⟨ cong₂ ( λ i j → i + j ) (Dividable.is-factor di) (Dividable.is-factor dj) ⟩ | |
| 694 i + j ∎ ) } where | |
| 695 open ≡-Reasoning | |
| 696 | |
| 697 div-div : { i j k : ℕ } → k > 1 → Dividable k i → Dividable k j → Dividable k (i - j) ∧ Dividable k (j - i) | |
| 698 div-div {i} {j} {k} k>1 di dj = ⟪ div-div1 di dj , div-div1 dj di ⟫ where | |
| 699 div-div1 : {i j : ℕ } → Dividable k i → Dividable k j → Dividable k (i - j) | |
| 700 div-div1 {i} {j} di dj = record { factor = fki - fkj ; is-factor = ( begin | |
| 701 (fki - fkj) * k + 0 ≡⟨ +-comm _ 0 ⟩ | |
| 702 (fki - fkj) * k ≡⟨ distr-minus-* {fki} {fkj} ⟩ | |
| 703 (fki * k) - (fkj * k) ≡⟨ cong₂ ( λ i j → i - j ) (+-comm 0 (fki * k)) (+-comm 0 (fkj * k)) ⟩ | |
| 704 (fki * k + 0) - (fkj * k + 0) ≡⟨ cong₂ ( λ i j → i - j ) (Dividable.is-factor di) (Dividable.is-factor dj) ⟩ | |
| 705 i - j ∎ ) } where | |
| 706 open ≡-Reasoning | |
| 707 fki = Dividable.factor di | |
| 708 fkj = Dividable.factor dj | |
| 709 | |
| 710 open _∧_ | |
| 112 | 711 |
| 314 | 712 div+1 : { i k : ℕ } → k > 1 → Dividable k i → ¬ Dividable k (suc i) |
| 713 div+1 {i} {k} k>1 d d1 = div1 k>1 div+11 where | |
| 714 div+11 : Dividable k 1 | |
| 715 div+11 = subst (λ g → Dividable k g) (minus+y-y {1} {i} ) ( proj2 (div-div k>1 d d1 ) ) | |
| 716 | |
| 717 div<k : { m k : ℕ } → k > 1 → m > 0 → m < k → ¬ Dividable k m | |
| 718 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 | |
| 719 div<k1 : (f : ℕ ) → f * k + 0 ≡ m → k ≤ m | |
| 720 div<k1 zero eq = ⊥-elim (nat-≡< eq m>0 ) | |
| 721 div<k1 (suc f) eq = begin | |
| 722 k ≤⟨ x≤x+y ⟩ | |
| 723 k + (f * k + 0) ≡⟨ sym (+-assoc k _ _) ⟩ | |
| 724 k + f * k + 0 ≡⟨ eq ⟩ | |
| 725 m ∎ where open ≤-Reasoning | |
| 726 | |
| 727 0<factor : { m k : ℕ } → k > 0 → m > 0 → (d : Dividable k m ) → Dividable.factor d > 0 | |
|
318
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
314
diff
changeset
|
728 0<factor {m} {k} k>0 m>0 d with Dividable.factor d in eq1 |
|
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
314
diff
changeset
|
729 ... | zero = ⊥-elim ( nat-≡< ff1 m>0 ) where |
| 314 | 730 ff1 : 0 ≡ m |
| 731 ff1 = begin | |
| 732 0 ≡⟨⟩ | |
| 733 0 * k + 0 ≡⟨ cong (λ j → j * k + 0) (sym eq1) ⟩ | |
| 734 Dividable.factor d * k + 0 ≡⟨ Dividable.is-factor d ⟩ | |
| 735 m ∎ where open ≡-Reasoning | |
|
318
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
314
diff
changeset
|
736 ... | suc t = s≤s z≤n |
| 314 | 737 |
| 738 div→k≤m : { m k : ℕ } → k > 1 → m > 0 → Dividable k m → m ≥ k | |
| 739 div→k≤m {m} {k} k>1 m>0 d with <-cmp m k | |
| 740 ... | tri< a ¬b ¬c = ⊥-elim ( div<k k>1 m>0 a d ) | |
| 741 ... | tri≈ ¬a refl ¬c = ≤-refl | |
| 742 ... | tri> ¬a ¬b c = <to≤ c | |
| 743 | |
| 744 div1*k+0=k : {k : ℕ } → 1 * k + 0 ≡ k | |
| 745 div1*k+0=k {k} = begin | |
| 746 1 * k + 0 ≡⟨ cong (λ g → g + 0) (+-comm _ 0) ⟩ | |
| 747 k + 0 ≡⟨ +-comm _ 0 ⟩ | |
| 748 k ∎ where open ≡-Reasoning | |
| 749 | |
| 750 decD : {k m : ℕ} → k > 1 → Dec (Dividable k m ) | |
| 751 decD {k} {m} k>1 = n-induction {_} {_} {ℕ} {λ m → Dec (Dividable k m ) } F I m where | |
| 752 F : ℕ → ℕ | |
| 753 F m = m | |
| 754 F0 : ( m : ℕ ) → F (m - k) ≡ 0 → Dec (Dividable k m ) | |
| 755 F0 0 eq = yes record { factor = 0 ; is-factor = refl } | |
| 756 F0 (suc m) eq with <-cmp k (suc m) | |
| 757 ... | tri< a ¬b ¬c = yes record { factor = 1 ; is-factor = | |
| 758 subst (λ g → 1 * k + 0 ≡ g ) (sym (i-j=0→i=j (<to≤ a) eq )) div1*k+0=k } -- (suc m - k) ≡ 0 → k ≡ suc m, k ≤ suc m | |
| 759 ... | tri≈ ¬a refl ¬c = yes record { factor = 1 ; is-factor = div1*k+0=k } | |
| 760 ... | tri> ¬a ¬b c = no ( λ d → ⊥-elim (div<k k>1 (s≤s z≤n ) c d) ) | |
| 761 decl : {m : ℕ } → 0 < m → m - k < m | |
| 762 decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m | |
| 763 ind : (p : ℕ ) → Dec (Dividable k (p - k) ) → Dec (Dividable k p ) | |
| 764 ind p (yes y) with <-cmp p k | |
| 765 ... | tri≈ ¬a refl ¬c = yes (subst (λ g → Dividable k g) (minus+n ≤-refl ) (proj1 ( div+div y div= ))) | |
| 766 ... | tri> ¬a ¬b k<p = yes (subst (λ g → Dividable k g) (minus+n (<-trans k<p a<sa)) (proj1 ( div+div y div= ))) | |
| 767 ... | tri< a ¬b ¬c with <-cmp p 0 | |
| 768 ... | tri≈ ¬a refl ¬c₁ = yes div0 | |
| 769 ... | tri> ¬a ¬b₁ c = no (λ d → not-div p (Dividable.factor d) a c (Dividable.is-factor d) ) where | |
| 770 not-div : (p f : ℕ) → p < k → 0 < p → f * k + 0 ≡ p → ⊥ | |
| 771 not-div (suc p) (suc f) p<k 0<p eq = nat-≡< (sym eq) ( begin -- ≤-trans p<k {!!}) -- suc p ≤ k | |
| 772 suc (suc p) ≤⟨ p<k ⟩ | |
| 773 k ≤⟨ x≤x+y ⟩ | |
| 774 k + (f * k + 0) ≡⟨ sym (+-assoc k _ _) ⟩ | |
| 775 suc f * k + 0 ∎ ) where open ≤-Reasoning | |
| 776 ind p (no n) = no (λ d → n (proj1 (div-div k>1 d div=)) ) | |
| 777 I : Ninduction ℕ _ F | |
| 778 I = record { | |
| 779 pnext = λ p → p - k | |
| 780 ; fzero = λ {m} eq → F0 m eq | |
| 781 ; decline = λ {m} lt → decl lt | |
| 782 ; ind = λ {p} prev → ind p prev | |
| 783 } | |
| 784 | |
| 785 |