Maths in Lean: the natural numbers #
The natural numbers begin with zero as is standard in computer
science. You can call them Nat or ℕ (you get the latter
symbol by typing \N in VS Code).
The naturals are what is called an inductive type, with two
constructors. The first is Nat.zero, usually written 0 or (0 : ℕ) in
practice, which is zero. The other constructor is Nat.succ, which
takes a natural as input and outputs the next one.
Addition and multiplication are defined by recursion on the second
variable and many proofs of basic stuff in the core library are by
induction on the second variable. The notations +, -, * are shorthand
for the functions Nat.add, Nat.sub and Nat.mul, and other notations
(≤, <, |) mean the usual things (get the "divides" symbol with \|).
The % symbol denotes modulus (remainder after division).
Here are some of core Lean's functions for working with Nat.
open nat
example : Nat.succ (Nat.succ 4) = 6 := rfl
example : 4 - 3 = 1 := rfl
example : 5 - 6 = 0 := rfl -- these are naturals
example : 1 ≠ 0 := one_ne_zero
example : 7 * 4 = 28 := rfl
example (m n p : ℕ) : m + p = n + p → m = n := add_right_cancel
example (a b c : ℕ) : a * (b + c) = a * b + a * c := left_distrib a b c
example (m n : ℕ) : succ m ≤ succ n → m ≤ n := Nat.le_of_succ_le_succ
example (a b: ℕ) : a < b → ∀ n, 0 < n → a ^ n < b ^ n := pow_lt_pow_of_lt_left
In mathlib there are more basic functions on the naturals, for example factorials, lowest common multiples, primes, square roots, and some modular arithmetic.
import Mathlib.Data.Nat.Dist -- distance function
import Mathlib.Data.Nat.GCD.Basic -- gcd
import Mathlib.Data.Nat.ModEq -- modular arithmetic
import Mathlib.Data.Nat.Prime.Basic -- prime number stuff
import Mathlib.Data.Nat.Factors -- factors
import Mathlib.Tactic.NormNum.Prime -- a tactic for fast computations
open Nat
example : factorial 4 = 24 := rfl -- factorial
example (a : ℕ) : factorial a > 0 := factorial_pos a
example : dist 6 4 = 2 := rfl -- distance function
example (a b : ℕ) : a ≠ b → dist a b > 0 := dist_pos_of_ne
example (a b : ℕ) : gcd a b ∣ a ∧ gcd a b ∣ b := gcd_dvd a b
example : lcm 6 4 = 12 := rfl
example (a b : ℕ) : lcm a b = lcm b a := lcm_comm a b
example (a b : ℕ) : gcd a b * lcm a b = a * b := gcd_mul_lcm a b
-- type the congruence symbol with \==
example : 5 ≡ 8 [MOD 3] := rfl
-- nat.sqrt is integer square root (it rounds down).
#eval sqrt 1000047
-- returns 1000
example (a : ℕ) : sqrt (a * a) = a := sqrt_eq a
example (a b : ℕ) : sqrt a < b ↔ a < b * b := sqrt_lt
example : Nat.Prime 59 := by decide
-- (The default instance is `nat.decidable_prime`, which can't be
-- used by `dec_trivial`, because the kernel would need to unfold
-- irreducible proofs generated by well-founded recursion.)
-- The tactic `norm_num`, amongst other things, provides faster primality testing.
example : Nat.Prime 104729 := by
norm_num
example (p : ℕ) : Nat.Prime p → p ≥ 2 := Prime.two_le
example (p : ℕ) : Nat.Prime p ↔ p ≥ 2 ∧ ∀ m, 2 ≤ m → m ≤ sqrt p → ¬ (m ∣ p) := prime_def_le_sqrt
example (p : ℕ) : Nat.Prime p → (∀ m, Coprime p m ∨ p ∣ m) := coprime_or_dvd_of_prime
example : ∀ n, ∃ p, p ≥ n ∧ Nat.Prime p := exists_infinite_primes
-- minFac returns the smallest prime factor of n (or junk if it doesn't have one)
example : minFac 12 = 2 := rfl
-- `Nat.primeFactorsList n` is the prime factorization of `n`, listed in increasing order.
-- This doesn't seem to reduce, and apparently there has not been
-- an attempt to get the kernel to evaluate it sensibly.
-- But we can evaluate it in the virtual machine using #eval .
#eval primeFactorsList (2^32+1)
-- [641, 6700417]