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