Open with one click!
1
-- from https://github.com/leanprover-community/mathlib/blob/master/docs/theories/naturals.md
2
3
import data.nat.dist -- distance function
4
import data.nat.gcd -- gcd
5
import data.nat.modeq -- modular arithmetic
6
import data.nat.prime -- prime number stuff
7
import data.nat.sqrt -- square roots
8
import tactic.norm_num -- a tactic for fast computations
9
10
open nat
11
12
example : fact 4 = 24 := rfl -- factorial
13
14
example (a : ) : fact a > 0 := fact_pos a
15
16
example : dist 6 4 = 2 := rfl -- distance function
17
18
example (a b : ) : a b dist a b > 0 := dist_pos_of_ne
19
20
example (a b : ) : gcd a b a gcd a b b := gcd_dvd a b
21
22
example : lcm 6 4 = 12 := rfl
23
24
example (a b : ) : lcm a b = lcm b a := lcm_comm a b
25
example (a b : ) : gcd a b * lcm a b = a * b := gcd_mul_lcm a b
26
27
example (a b : ) : ( k : , k > 1 k a ¬ (k b) ) coprime a b := coprime_of_dvd
28
29
-- type the congruence symbol with \==
30
31
example : 5 8 [MOD 3] := rfl
32
33
example (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
40
example (a : ) : sqrt (a * a) = a := sqrt_eq a
41
42
example (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
49
instance : decidable (prime 59) := decidable_prime_1 59
50
example : 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
58
example : prime 104729 := by norm_num
59
60
-- NOTE: this next line not supported with the version of mathlib in CoCalc
61
example (p : ) : prime p p 2 := prime.two_le
62
63
example (p : ) : prime p p 2 m, 2 m m sqrt p ¬ (m p) := prime_def_le_sqrt
64
65
example (p : ) : prime p ( m, coprime p m p m) := coprime_or_dvd_of_prime
66
67
example : 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
71
example : 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]