CoCalc Public Filessupport / 2020-02-19-lean-natural-numbers.lean
Author: William A. Stein
Description: Jupyter notebook support/2015-06-04-141749-bokeh.ipynb
1-- from https://github.com/leanprover-community/mathlib/blob/master/docs/theories/naturals.md
2
3import data.nat.dist -- distance function
4import data.nat.gcd -- gcd
5import data.nat.modeq -- modular arithmetic
6import data.nat.prime -- prime number stuff
7import data.nat.sqrt  -- square roots
8import tactic.norm_num -- a tactic for fast computations
9
10open nat
11
12example : fact 4 = 24 := rfl -- factorial
13
14example (a : ℕ) : fact a > 0 := fact_pos a
15
16example : dist 6 4 = 2 := rfl -- distance function
17
18example (a b : ℕ) : a ≠ b → dist a b > 0 := dist_pos_of_ne
19
20example (a b : ℕ) : gcd a b ∣ a ∧ gcd a b ∣ b := gcd_dvd a b
21
22example : lcm 6 4 = 12 := rfl
23
24example (a b : ℕ) : lcm a b = lcm b a := lcm_comm a b
25example (a b : ℕ) : gcd a b * lcm a b = a * b := gcd_mul_lcm a b
26
27example (a b : ℕ) : (∀ k : ℕ, k > 1 → k ∣ a → ¬ (k ∣ b) ) → coprime a b := coprime_of_dvd
28
29-- type the congruence symbol with \==
30
31example : 5 ≡ 8 [MOD 3] := rfl
32
33example (a b c d m : ℕ) : a ≡ b [MOD m] → c ≡ d [MOD m] → a * c ≡ b * d [MOD m] := modeq.modeq_mul
34
35-- nat.sqrt is integer square root (it rounds down).
36
37#eval sqrt 1000047
38-- returns 1000
39
40example (a : ℕ) : sqrt (a * a) = a := sqrt_eq a
41
42example (a b : ℕ) : sqrt a < b ↔ a < b * b := sqrt_lt
43
44-- nat.prime n returns whether n is prime or not.
45-- We can prove 59 is prime if we first tell Lean that primality
46-- is decidable. But it's slow because the algorithms are
47-- not optimised for the kernel.
48
49instance : decidable (prime 59) := decidable_prime_1 59
50example : prime 59 := dec_trivial
51
52-- (The default instance is nat.decidable_prime, which can't be
53-- used by dec_trivial, because the kernel would need to unfold
54-- irreducible proofs generated by well-founded recursion.)
55
56-- The tactic norm_num, amongst other things, provides faster primality testing.
57
58example : prime 104729 := by norm_num
59
60-- NOTE: this next line not supported with the version of mathlib in CoCalc
61example (p : ℕ) : prime p → p ≥ 2 := prime.two_le
62
63example (p : ℕ) : prime p ↔ p ≥ 2 ∧ ∀ m, 2 ≤ m → m ≤ sqrt p → ¬ (m ∣ p) := prime_def_le_sqrt
64
65example (p : ℕ) : prime p → (∀ m, coprime p m ∨ p ∣ m) := coprime_or_dvd_of_prime
66
67example : ∀ n, ∃ p, p ≥ n ∧ prime p := exists_infinite_primes
68
69-- min_fac returns the smallest prime factor of n (or junk if it doesn't have one)
70
71example : min_fac 12 = 2 := rfl
72
73-- factors n is the prime factorization of n, listed in increasing order.
74-- This doesn't seem to reduce, and apparently there has not been
75-- an attempt to get the kernel to evaluate it sensibly.
76-- But we can evaluate it in the virtual machine using #eval .
77
78#eval factors (2^32+1)
79-- [641, 6700417]