[234] | 1 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 2 | (* Nat.ma: Natural numbers and common arithmetical functions. *) |
---|
| 3 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[228] | 4 | include "Cartesian.ma". |
---|
| 5 | include "Bool.ma". |
---|
| 6 | |
---|
[246] | 7 | include "Connectives.ma". |
---|
[228] | 8 | |
---|
[234] | 9 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 10 | (* The datatype. *) |
---|
| 11 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[228] | 12 | ninductive Nat: Type[0] ≝ |
---|
| 13 | Z: Nat |
---|
| 14 | | S: Nat → Nat. |
---|
| 15 | |
---|
[352] | 16 | ntheorem S_inj: ∀n,m:Nat. S n = S m → n=m. |
---|
| 17 | #n m H; |
---|
| 18 | nchange with (n = match S m with [ Z ⇒ Z | S x ⇒ x]); |
---|
| 19 | napply (match H return λx.λ_. n = match x with [Z ⇒ Z | S x ⇒ x] with [ refl ⇒ ? ]); |
---|
| 20 | nnormalize; /3/. |
---|
| 21 | nqed. |
---|
| 22 | |
---|
[234] | 23 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 24 | (* Orderings. *) |
---|
| 25 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 26 | |
---|
| 27 | ninductive less_than_or_equal_p (n: Nat): Nat → Prop ≝ |
---|
| 28 | ltoe_refl: less_than_or_equal_p n n |
---|
| 29 | | ltoe_step: ∀m: Nat. less_than_or_equal_p n m → less_than_or_equal_p n (S m). |
---|
| 30 | |
---|
| 31 | nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m: Bool ≝ |
---|
| 32 | match m with |
---|
[260] | 33 | [ Z ⇒ true |
---|
[234] | 34 | | S o ⇒ |
---|
| 35 | match n with |
---|
[260] | 36 | [ Z ⇒ false |
---|
[234] | 37 | | S p ⇒ less_than_or_equal_b o p |
---|
| 38 | ] |
---|
| 39 | ]. |
---|
| 40 | |
---|
[237] | 41 | notation "hvbox(n break ≤ m)" |
---|
[234] | 42 | non associative with precedence 47 |
---|
| 43 | for @{ 'less_than_or_equal $n $m }. |
---|
| 44 | |
---|
| 45 | interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m). |
---|
| 46 | |
---|
[351] | 47 | notation "hvbox(n break ≲ m)" |
---|
| 48 | non associative with precedence 47 |
---|
| 49 | for @{ 'less_than_or_equalb $n $m }. |
---|
| 50 | |
---|
| 51 | interpretation "Nat less than or equal bool" 'less_than_or_equalb n m = (less_than_or_equal_b n m). |
---|
| 52 | |
---|
| 53 | |
---|
[234] | 54 | ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝ |
---|
| 55 | λm, n: Nat. |
---|
| 56 | n ≤ m. |
---|
| 57 | |
---|
[275] | 58 | ndefinition greater_than_or_equal_b: ∀m, n: Nat. Bool ≝ |
---|
[234] | 59 | λm, n: Nat. |
---|
[350] | 60 | less_than_or_equal_b n m. |
---|
[234] | 61 | |
---|
[237] | 62 | notation "hvbox(n break ≥ m)" |
---|
[234] | 63 | non associative with precedence 47 |
---|
| 64 | for @{ 'greater_than_or_equal $n $m }. |
---|
| 65 | |
---|
| 66 | |
---|
| 67 | interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m). |
---|
| 68 | |
---|
[351] | 69 | notation "hvbox(n break ≳ m)" |
---|
| 70 | non associative with precedence 47 |
---|
| 71 | for @{ 'greater_than_or_equalb $n $m }. |
---|
| 72 | |
---|
| 73 | interpretation "Nat greater than or equal bool" 'greater_than_or_equalb n m = (greater_than_or_equal_b n m). |
---|
| 74 | |
---|
| 75 | |
---|
[234] | 76 | (* Add Boolean versions. *) |
---|
| 77 | ndefinition less_than_p ≝ |
---|
[265] | 78 | λm: Nat. |
---|
| 79 | λn: Nat. |
---|
| 80 | less_than_or_equal_p (S m) n. |
---|
[234] | 81 | |
---|
[237] | 82 | notation "hvbox(n break < m)" |
---|
[234] | 83 | non associative with precedence 47 |
---|
| 84 | for @{ 'less_than $n $m }. |
---|
| 85 | |
---|
| 86 | interpretation "Nat less than prop" 'less_than n m = (less_than_p n m). |
---|
| 87 | |
---|
| 88 | ndefinition greater_than_p ≝ |
---|
| 89 | λm, n: Nat. |
---|
| 90 | n < m. |
---|
| 91 | |
---|
[237] | 92 | notation "hvbox(n break > m)" |
---|
[234] | 93 | non associative with precedence 47 |
---|
| 94 | for @{ 'greater_than $n $m }. |
---|
| 95 | |
---|
| 96 | interpretation "Nat greater than prop" 'greater_than n m = (greater_than_p n m). |
---|
| 97 | |
---|
[350] | 98 | nlet rec less_than_b (m: Nat) (n: Nat) on m ≝ |
---|
| 99 | match m with |
---|
| 100 | [ Z ⇒ |
---|
| 101 | match n with |
---|
| 102 | [ Z ⇒ false |
---|
| 103 | | S o ⇒ true |
---|
| 104 | ] |
---|
| 105 | | S o ⇒ |
---|
| 106 | match n with |
---|
| 107 | [ Z ⇒ false |
---|
| 108 | | S p ⇒ less_than_b o p |
---|
| 109 | ] |
---|
| 110 | ]. |
---|
| 111 | |
---|
| 112 | (* interpretation "Nat less than bool" 'less_than n m = (less_than_b n m). *) |
---|
| 113 | |
---|
| 114 | ndefinition greater_than_b ≝ |
---|
| 115 | λm, n: Nat. |
---|
| 116 | less_than_b n m. |
---|
| 117 | |
---|
| 118 | (* interpretation "Nat greater than bool" 'greater_than n m = (greater_than_b n m). *) |
---|
| 119 | |
---|
[234] | 120 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 121 | (* Addition and subtraction. *) |
---|
| 122 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[228] | 123 | nlet rec plus (n: Nat) (o: Nat) on n ≝ |
---|
| 124 | match n with |
---|
| 125 | [ Z ⇒ o |
---|
| 126 | | S p ⇒ S (plus p o) |
---|
| 127 | ]. |
---|
| 128 | |
---|
[237] | 129 | notation "hvbox(n break + m)" |
---|
[228] | 130 | right associative with precedence 52 |
---|
| 131 | for @{ 'plus $n $m }. |
---|
| 132 | |
---|
| 133 | interpretation "Nat plus" 'plus n m = (plus n m). |
---|
| 134 | |
---|
| 135 | nlet rec minus (n: Nat) (o: Nat) on n ≝ |
---|
| 136 | match n with |
---|
| 137 | [ Z ⇒ Z |
---|
| 138 | | S p ⇒ |
---|
| 139 | match o with |
---|
| 140 | [ Z ⇒ S p |
---|
| 141 | | S q ⇒ minus p q |
---|
| 142 | ] |
---|
| 143 | ]. |
---|
| 144 | |
---|
[237] | 145 | notation "hvbox(n break - m)" |
---|
[228] | 146 | right associative with precedence 47 |
---|
| 147 | for @{ 'minus $n $m }. |
---|
| 148 | |
---|
| 149 | interpretation "Nat minus" 'minus n m = (minus n m). |
---|
[234] | 150 | |
---|
| 151 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 152 | (* Multiplication, modulus and division. *) |
---|
| 153 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[228] | 154 | |
---|
| 155 | nlet rec multiplication (n: Nat) (o: Nat) on n ≝ |
---|
| 156 | match n with |
---|
| 157 | [ Z ⇒ Z |
---|
| 158 | | S p ⇒ o + (multiplication p o) |
---|
| 159 | ]. |
---|
| 160 | |
---|
[237] | 161 | notation "hvbox(n break * m)" |
---|
[228] | 162 | right associative with precedence 47 |
---|
| 163 | for @{ 'multiplication $n $m }. |
---|
| 164 | |
---|
| 165 | interpretation "Nat multiplication" 'times n m = (multiplication n m). |
---|
| 166 | |
---|
[234] | 167 | nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝ |
---|
[350] | 168 | match less_than_or_equal_b n p with |
---|
[260] | 169 | [ true ⇒ Z |
---|
| 170 | | false ⇒ |
---|
[234] | 171 | match m with |
---|
| 172 | [ Z ⇒ Z |
---|
| 173 | | (S q) ⇒ S (division_aux q (n - (S p)) p) |
---|
[231] | 174 | ] |
---|
| 175 | ]. |
---|
| 176 | |
---|
[234] | 177 | ndefinition division ≝ |
---|
| 178 | λm, n: Nat. |
---|
| 179 | match n with |
---|
| 180 | [ Z ⇒ S m |
---|
| 181 | | S o ⇒ division_aux m m o |
---|
| 182 | ]. |
---|
| 183 | |
---|
[237] | 184 | notation "hvbox(n break ÷ m)" |
---|
[234] | 185 | right associative with precedence 47 |
---|
| 186 | for @{ 'division $n $m }. |
---|
[231] | 187 | |
---|
[234] | 188 | interpretation "Nat division" 'division n m = (division n m). |
---|
| 189 | |
---|
| 190 | nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝ |
---|
[350] | 191 | match less_than_or_equal_b n p with |
---|
[260] | 192 | [ true ⇒ n |
---|
| 193 | | false ⇒ |
---|
[234] | 194 | match m with |
---|
| 195 | [ Z ⇒ n |
---|
| 196 | | S o ⇒ modulus_aux o (n - (S p)) p |
---|
| 197 | ] |
---|
| 198 | ]. |
---|
| 199 | |
---|
| 200 | ndefinition modulus ≝ |
---|
[232] | 201 | λm, n: Nat. |
---|
[234] | 202 | match n with |
---|
| 203 | [ Z ⇒ m |
---|
| 204 | | S o ⇒ modulus_aux m m o |
---|
| 205 | ]. |
---|
[232] | 206 | |
---|
[277] | 207 | notation "hvbox(n break 'mod' m)" |
---|
[234] | 208 | right associative with precedence 47 |
---|
| 209 | for @{ 'modulus $n $m }. |
---|
[232] | 210 | |
---|
[234] | 211 | interpretation "Nat modulus" 'modulus m n = (modulus m n). |
---|
[232] | 212 | |
---|
[237] | 213 | ndefinition divide_with_remainder ≝ |
---|
| 214 | λm, n: Nat. |
---|
| 215 | mk_Cartesian Nat Nat (m ÷ n) (modulus m n). |
---|
| 216 | |
---|
[234] | 217 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[237] | 218 | (* Exponentials, and square roots. *) |
---|
| 219 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 220 | |
---|
| 221 | nlet rec exponential (m: Nat) (n: Nat) on n ≝ |
---|
| 222 | match n with |
---|
| 223 | [ Z ⇒ S (Z) |
---|
| 224 | | S o ⇒ m * exponential m o |
---|
| 225 | ]. |
---|
| 226 | |
---|
| 227 | notation "hvbox(n ^ m)" |
---|
| 228 | left associative with precedence 52 |
---|
| 229 | for @{ 'exponential $n $m }. |
---|
| 230 | |
---|
| 231 | interpretation "Nat exponential" 'exponential n m = (exponential n m). |
---|
| 232 | |
---|
[349] | 233 | nlet rec eq_n (m: Nat) (n: Nat) on m: Bool ≝ |
---|
[275] | 234 | match m with |
---|
| 235 | [ Z ⇒ |
---|
| 236 | match n with |
---|
| 237 | [ Z ⇒ true |
---|
| 238 | | _ ⇒ false |
---|
| 239 | ] |
---|
| 240 | | S o ⇒ |
---|
| 241 | match n with |
---|
[349] | 242 | [ S p ⇒ eq_n o p |
---|
[275] | 243 | | _ ⇒ false |
---|
| 244 | ] |
---|
| 245 | ]. |
---|
| 246 | |
---|
[237] | 247 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[234] | 248 | (* Greatest common divisor and least common multiple. *) |
---|
| 249 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[232] | 250 | |
---|
[234] | 251 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[330] | 252 | (* Axioms. *) |
---|
[234] | 253 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 254 | |
---|
[351] | 255 | (*naxiom plus_minus_inverse_left: |
---|
[330] | 256 | ∀m, n: Nat. |
---|
| 257 | (m + n) - n = m. |
---|
[351] | 258 | *) |
---|
| 259 | |
---|
[350] | 260 | ntheorem less_than_or_equal_monotone: |
---|
[330] | 261 | ∀m, n: Nat. |
---|
| 262 | m ≤ n → (S m) ≤ (S n). |
---|
[350] | 263 | #m n H; nelim H; /2/. |
---|
| 264 | nqed. |
---|
| 265 | |
---|
| 266 | nlemma trans_le: ∀n,m,l. n ≤ m → m ≤ l → n ≤ l. |
---|
| 267 | #n m l H H1; nelim H1; /2/. |
---|
| 268 | nqed. |
---|
| 269 | |
---|
[351] | 270 | ntheorem less_than_or_equal_injective: |
---|
[330] | 271 | ∀m, n: Nat. |
---|
| 272 | (S m) ≤ (S n) → m ≤ n. |
---|
[350] | 273 | #m n H; |
---|
| 274 | nchange with (match S m with [ Z ⇒ Z | S x ⇒ x] ≤ match S n with [ Z ⇒ Z | S x ⇒ x]); |
---|
| 275 | napply (match H return λx.λ_. m ≤ match x with [Z ⇒ Z | S x ⇒ x] with [ ltoe_refl ⇒ ? | ltoe_step y H ⇒ ? ]); |
---|
| 276 | nnormalize; /3/. |
---|
| 277 | nqed. |
---|
[330] | 278 | |
---|
[350] | 279 | ntheorem succ_less_than_injective: |
---|
[329] | 280 | ∀m, n: Nat. |
---|
| 281 | less_than_p (S m) (S n) → m < n. |
---|
[350] | 282 | /2/. |
---|
| 283 | nqed. |
---|
| 284 | |
---|
| 285 | nlemma not_less_than_S_Z: |
---|
| 286 | ∀m,n: Nat. S m ≤ n → ¬ (n = Z). |
---|
| 287 | #m n H; nelim H [ @; #K; ndestruct | #y H1 H2; @; #K; ndestruct ] |
---|
| 288 | nqed. |
---|
| 289 | |
---|
| 290 | ntheorem nothing_less_than_Z: |
---|
[329] | 291 | ∀m: Nat. |
---|
| 292 | ¬(m < Z). |
---|
[350] | 293 | #m; @; #H; nlapply (not_less_than_S_Z m Z H); /2/; |
---|
| 294 | nqed. |
---|
[351] | 295 | |
---|
[329] | 296 | |
---|
[330] | 297 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 298 | (* Lemmas. *) |
---|
| 299 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 300 | |
---|
[232] | 301 | nlemma less_than_or_equal_zero: |
---|
| 302 | ∀n: Nat. |
---|
| 303 | Z ≤ n. |
---|
| 304 | #n. |
---|
| 305 | nelim n. |
---|
| 306 | //. |
---|
| 307 | #N. |
---|
[234] | 308 | napply ltoe_step. |
---|
[232] | 309 | nqed. |
---|
| 310 | |
---|
[261] | 311 | (* |
---|
[232] | 312 | nlemma less_than_or_equal_zero_equal_zero: |
---|
| 313 | ∀m: Nat. |
---|
| 314 | m ≤ Z → m = Z. |
---|
| 315 | #m. |
---|
| 316 | nelim m. |
---|
| 317 | //. |
---|
| 318 | #N H H2. |
---|
| 319 | nnormalize. |
---|
| 320 | *) |
---|
| 321 | |
---|
| 322 | nlemma less_than_or_equal_reflexive: |
---|
| 323 | ∀n: Nat. |
---|
| 324 | n ≤ n. |
---|
| 325 | #n. |
---|
| 326 | nelim n. |
---|
| 327 | nnormalize. |
---|
| 328 | @. |
---|
| 329 | #N H. |
---|
| 330 | nnormalize. |
---|
| 331 | //. |
---|
| 332 | nqed. |
---|
| 333 | |
---|
| 334 | (* |
---|
| 335 | nlemma less_than_or_equal_succ: |
---|
| 336 | ∀m, n: Nat. |
---|
| 337 | S m ≤ n → m ≤ n. |
---|
| 338 | #m n. |
---|
| 339 | nelim m. |
---|
| 340 | #H. |
---|
| 341 | napplyS less_than_or_equal_zero. |
---|
| 342 | #N H H2. |
---|
[261] | 343 | nrewrite > H. |
---|
| 344 | nnormalize. |
---|
[232] | 345 | |
---|
| 346 | nlemma less_than_or_equal_transitive: |
---|
| 347 | ∀m, n, o: Nat. |
---|
| 348 | m ≤ n ∧ n ≤ o → m ≤ o. |
---|
| 349 | #m n o. |
---|
| 350 | nelim m. |
---|
| 351 | #H. |
---|
| 352 | napply less_than_or_equal_zero. |
---|
| 353 | #N H H2. |
---|
| 354 | nnormalize. |
---|
| 355 | *) |
---|
| 356 | |
---|
[228] | 357 | nlemma plus_zero: |
---|
| 358 | ∀n: Nat. |
---|
| 359 | n + Z = n. |
---|
| 360 | #n. |
---|
| 361 | nelim n. |
---|
| 362 | nnormalize. |
---|
| 363 | @. |
---|
| 364 | #N H. |
---|
| 365 | nnormalize. |
---|
| 366 | nrewrite > H. |
---|
| 367 | @. |
---|
| 368 | nqed. |
---|
| 369 | |
---|
| 370 | nlemma plus_associative: |
---|
| 371 | ∀m, n, o: Nat. |
---|
| 372 | (m + n) + o = m + (n + o). |
---|
| 373 | #m n o. |
---|
| 374 | nelim m. |
---|
| 375 | nnormalize. |
---|
| 376 | @. |
---|
| 377 | #N H. |
---|
| 378 | nnormalize. |
---|
| 379 | nrewrite > H. |
---|
| 380 | @. |
---|
| 381 | nqed. |
---|
| 382 | |
---|
| 383 | nlemma succ_plus: |
---|
| 384 | ∀m, n: Nat. |
---|
| 385 | S(m + n) = m + S(n). |
---|
| 386 | #m n. |
---|
| 387 | nelim m. |
---|
| 388 | nnormalize. |
---|
| 389 | @. |
---|
| 390 | #N H. |
---|
| 391 | nnormalize. |
---|
| 392 | nrewrite > H. |
---|
| 393 | @. |
---|
| 394 | nqed. |
---|
| 395 | |
---|
[233] | 396 | nlemma succ_plus_succ_zero: |
---|
| 397 | ∀n: Nat. |
---|
| 398 | S n = plus n (S Z). |
---|
| 399 | #n. |
---|
| 400 | nelim n. |
---|
| 401 | //. |
---|
| 402 | #N H. |
---|
[247] | 403 | nnormalize. |
---|
| 404 | nrewrite < H. |
---|
| 405 | @. |
---|
[233] | 406 | nqed. |
---|
| 407 | |
---|
[228] | 408 | nlemma plus_symmetrical: |
---|
| 409 | ∀m, n: Nat. |
---|
| 410 | m + n = n + m. |
---|
| 411 | #m n. |
---|
| 412 | nelim m. |
---|
| 413 | nnormalize. |
---|
| 414 | nelim n. |
---|
| 415 | nnormalize. |
---|
| 416 | @. |
---|
| 417 | #N H. |
---|
| 418 | nnormalize. |
---|
| 419 | nrewrite < H. |
---|
| 420 | @. |
---|
| 421 | #N H. |
---|
| 422 | nnormalize. |
---|
| 423 | nrewrite > H. |
---|
[330] | 424 | napply succ_plus. |
---|
[228] | 425 | nqed. |
---|
| 426 | |
---|
[230] | 427 | nlemma multiplication_zero_right_neutral: |
---|
[228] | 428 | ∀m: Nat. |
---|
| 429 | m * Z = Z. |
---|
| 430 | #m. |
---|
| 431 | nelim m. |
---|
| 432 | nnormalize. |
---|
| 433 | @. |
---|
| 434 | #N H. |
---|
| 435 | nnormalize. |
---|
| 436 | nrewrite > H. |
---|
| 437 | @. |
---|
| 438 | nqed. |
---|
| 439 | |
---|
| 440 | nlemma multiplication_succ: |
---|
| 441 | ∀m, n: Nat. |
---|
| 442 | m * S(n) = m + (m * n). |
---|
| 443 | #m n. |
---|
| 444 | nelim m. |
---|
| 445 | nnormalize. |
---|
| 446 | @. |
---|
| 447 | #N H. |
---|
| 448 | nnormalize. |
---|
[247] | 449 | nrewrite > H. |
---|
| 450 | nrewrite < (plus_associative n N ?). |
---|
| 451 | nrewrite > (plus_symmetrical n N). |
---|
| 452 | nrewrite > (plus_associative N n ?). |
---|
| 453 | @. |
---|
[228] | 454 | nqed. |
---|
| 455 | |
---|
| 456 | nlemma multiplication_symmetrical: |
---|
| 457 | ∀m, n: Nat. |
---|
| 458 | m * n = n * m. |
---|
| 459 | #m n. |
---|
| 460 | nelim m. |
---|
| 461 | nnormalize. |
---|
| 462 | nelim n. |
---|
| 463 | nnormalize. |
---|
| 464 | @. |
---|
| 465 | #N H. |
---|
| 466 | nnormalize. |
---|
| 467 | nrewrite < H. |
---|
| 468 | @. |
---|
| 469 | #N H. |
---|
| 470 | nnormalize. |
---|
| 471 | nrewrite > H. |
---|
[247] | 472 | nrewrite > (multiplication_succ ? ?). |
---|
| 473 | @. |
---|
[228] | 474 | nqed. |
---|
[230] | 475 | |
---|
| 476 | nlemma multiplication_succ_zero_left_neutral: |
---|
| 477 | ∀m: Nat. |
---|
| 478 | (S Z) * m = m. |
---|
| 479 | #m. |
---|
| 480 | nelim m. |
---|
| 481 | nnormalize. |
---|
| 482 | @. |
---|
| 483 | #N H. |
---|
| 484 | nnormalize. |
---|
[247] | 485 | nrewrite > (succ_plus ? ?). |
---|
| 486 | nrewrite < (succ_plus_succ_zero ?). |
---|
| 487 | @. |
---|
[230] | 488 | nqed. |
---|
| 489 | |
---|
| 490 | nlemma multiplication_succ_zero_right_neutral: |
---|
| 491 | ∀m: Nat. |
---|
| 492 | m * (S Z) = m. |
---|
| 493 | #m. |
---|
| 494 | nelim m. |
---|
| 495 | nnormalize. |
---|
| 496 | @. |
---|
| 497 | #N H. |
---|
| 498 | nnormalize. |
---|
| 499 | nrewrite > H. |
---|
| 500 | @. |
---|
| 501 | nqed. |
---|
| 502 | |
---|
| 503 | nlemma multiplication_distributes_right_plus: |
---|
| 504 | ∀m, n, o: Nat. |
---|
| 505 | (m + n) * o = m * o + n * o. |
---|
| 506 | #m n o. |
---|
| 507 | nelim m. |
---|
| 508 | nnormalize. |
---|
| 509 | @. |
---|
| 510 | #N H. |
---|
| 511 | nnormalize. |
---|
| 512 | nrewrite > H. |
---|
[247] | 513 | nrewrite < (plus_associative ? ? ?). |
---|
| 514 | @. |
---|
[230] | 515 | nqed. |
---|
| 516 | |
---|
| 517 | nlemma multiplication_distributes_left_plus: |
---|
| 518 | ∀m, n, o: Nat. |
---|
| 519 | o * (m + n) = o * m + o * n. |
---|
| 520 | #m n o. |
---|
[247] | 521 | nelim o. |
---|
| 522 | //. |
---|
| 523 | #N H. |
---|
| 524 | nnormalize. |
---|
| 525 | nrewrite > H. |
---|
| 526 | nrewrite < (plus_associative ? n (N * n)). |
---|
| 527 | nrewrite > (plus_symmetrical (m + N * m) n). |
---|
| 528 | nrewrite < (plus_associative n m (N * m)). |
---|
| 529 | nrewrite < (plus_symmetrical n m). |
---|
| 530 | nrewrite > (plus_associative (n + m) (N * m) (N * n)). |
---|
| 531 | @. |
---|
[230] | 532 | nqed. |
---|
| 533 | |
---|
| 534 | nlemma mutliplication_associative: |
---|
| 535 | ∀m, n, o: Nat. |
---|
| 536 | m * (n * o) = (m * n) * o. |
---|
| 537 | #m n o. |
---|
| 538 | nelim m. |
---|
| 539 | nnormalize. |
---|
| 540 | @. |
---|
| 541 | #N H. |
---|
| 542 | nnormalize. |
---|
| 543 | nrewrite > H. |
---|
[247] | 544 | nrewrite > (multiplication_distributes_right_plus ? ? ?). |
---|
| 545 | @. |
---|
[230] | 546 | nqed. |
---|
| 547 | |
---|
| 548 | nlemma minus_minus: |
---|
| 549 | ∀n: Nat. |
---|
| 550 | n - n = Z. |
---|
| 551 | #n. |
---|
| 552 | nelim n. |
---|
| 553 | nnormalize. |
---|
| 554 | @. |
---|
| 555 | #N H. |
---|
| 556 | nnormalize. |
---|
| 557 | nrewrite > H. |
---|
| 558 | @. |
---|
| 559 | nqed. |
---|
| 560 | |
---|
[351] | 561 | |
---|
[230] | 562 | nlemma succ_injective: |
---|
| 563 | ∀m, n: Nat. |
---|
| 564 | S m = S n → m = n. |
---|
[351] | 565 | #m n H; |
---|
| 566 | napply (match H return λy.λ_.m = match y with [Z ⇒ Z | S z ⇒ z] with |
---|
| 567 | [refl ⇒ ? ]); |
---|
| 568 | @; |
---|
| 569 | nqed. |
---|
[230] | 570 | |
---|
[351] | 571 | ntheorem eq_f: ∀A,B:Type[0].∀f:A→B.∀a,a'. a=a' → f a = f a'. |
---|
| 572 | //; |
---|
| 573 | nqed. |
---|
| 574 | |
---|
| 575 | ntheorem plus_minus_inverse_right: |
---|
| 576 | ∀m, n: Nat. |
---|
| 577 | n ≤ m → (m - n) + n = m. |
---|
| 578 | #m; nelim m |
---|
| 579 | [ #n; nelim n; //; #H1 H2 H3; ncases (nothing_less_than_Z H1); |
---|
| 580 | #K; ncases (K H3) |
---|
| 581 | | #y H1 x H2; nnormalize; ngeneralize in match H2; ncases x; nnormalize; /2/; |
---|
| 582 | #w; nrewrite < succ_plus; /4/. ##] |
---|
| 583 | nqed. |
---|
| 584 | |
---|
| 585 | (* |
---|
| 586 | |
---|
[230] | 587 | nlemma plus_minus_associate: |
---|
| 588 | ∀m, n, o: Nat. |
---|
| 589 | (m + n) - o = m + (n - o). |
---|
| 590 | #m n o. |
---|
| 591 | nelim m. |
---|
| 592 | nnormalize. |
---|
| 593 | @. |
---|
| 594 | #N H. |
---|
| 595 | |
---|
| 596 | |
---|
| 597 | nlemma plus_minus_inverses: |
---|
| 598 | ∀m, n: Nat. |
---|
| 599 | (m + n) - n = m. |
---|
| 600 | #m n. |
---|
| 601 | nelim m. |
---|
| 602 | nnormalize. |
---|
| 603 | napply minus_minus. |
---|
| 604 | #N H. |
---|
[260] | 605 | *) |
---|
[351] | 606 | |
---|
| 607 | ntheorem less_than_or_equal_b_correct: ∀m,n. less_than_or_equal_b m n = true → m ≤ n. |
---|
| 608 | #m; nelim m; //; #y H1 z; ncases z; nnormalize |
---|
| 609 | [ #H; ndestruct | /3/ ] |
---|
| 610 | nqed. |
---|
| 611 | |
---|
| 612 | ntheorem less_than_or_equal_b_complete: ∀m,n. less_than_or_equal_b m n = false → ¬(m ≤ n). |
---|
| 613 | #m; nelim m; nnormalize |
---|
| 614 | [ #n H; ndestruct | #y H1 z; ncases z; nnormalize |
---|
[352] | 615 | [ #H; /2/ | /3/ ] |
---|
[351] | 616 | nqed. |
---|
| 617 | |
---|
| 618 | ndefinition less_than_or_equal_b_elim: |
---|
| 619 | ∀m,n. ∀P: Bool → Type[0]. (m ≤ n → P true) → (¬(m ≤ n) → P false) → |
---|
| 620 | P (less_than_or_equal_b m n). |
---|
| 621 | #m n P H1 H2; nlapply (less_than_or_equal_b_correct m n); |
---|
| 622 | nlapply (less_than_or_equal_b_complete m n); |
---|
| 623 | ncases (less_than_or_equal_b m n); /3/. |
---|
| 624 | nqed. |
---|
| 625 | |
---|
| 626 | ndefinition greater_than_or_equal_b_elim: |
---|
| 627 | ∀m,n. ∀P: Bool → Type[0]. (m ≥ n → P true) → (¬(m ≥ n) → P false) → |
---|
| 628 | P (greater_than_or_equal_b m n). |
---|
| 629 | #m n; napply less_than_or_equal_b_elim; |
---|
| 630 | nqed. |
---|
| 631 | |
---|
| 632 | ntheorem less_than_b_correct: ∀m,n. less_than_b m n = true → m < n. |
---|
| 633 | #m; nelim m |
---|
| 634 | [ #n; ncases n [ #H; nnormalize in H; ndestruct | #z H; /2/ ] |
---|
| 635 | ##| #y H z; ncases z [ nnormalize; #K; ndestruct | #o K; |
---|
| 636 | napply less_than_or_equal_monotone; napply H; napply K ] |
---|
| 637 | nqed. |
---|
| 638 | |
---|
| 639 | ntheorem less_than_b_complete: ∀m,n. less_than_b m n = false → ¬(m < n). |
---|
| 640 | #m; nelim m |
---|
| 641 | [ #n; ncases n; //; #y H1; nnormalize in H1; ndestruct |
---|
| 642 | | #y H z; ncases z; //; #o H2; nlapply (H … H2); /3/. |
---|
| 643 | nqed. |
---|
| 644 | |
---|
| 645 | ndefinition less_than_b_elim: |
---|
| 646 | ∀m,n. ∀P: Bool → Type[0]. (m < n → P true) → (¬(m < n) → P false) → |
---|
| 647 | P (less_than_b m n). |
---|
| 648 | #m n; nlapply (less_than_b_correct m n); nlapply (less_than_b_complete m n); |
---|
| 649 | ncases (less_than_b m n); /3/. |
---|
| 650 | nqed. |
---|
| 651 | |
---|
| 652 | ndefinition greater_than_b_elim: |
---|
| 653 | ∀m,n. ∀P: Bool → Type[0]. (m > n → P true) → (¬(m > n) → P false) → |
---|
| 654 | P (greater_than_b m n). |
---|
| 655 | #m n; napply less_than_b_elim. |
---|
| 656 | nqed. |
---|