Lean for All

Day 19: Number types and hidden conversions🔗

Tell which number type a statement is about, and read the conversion arrow ↑.

Every number in Lean has a type. A plain numeral is a Nat unless something says otherwise. A type ascription (3 : Int) says it:

3 : Nat#check 3 3 : Int#check (3 : Int) 
3 : Nat
3 : Int

The type changes what statements mean. The same words can be false on Nat and true on Int:

theorem nat_ver (a b : Nat) : a - b + b = a := a:Natb:Nat⊢ a - b + b = a omega could not prove the goal: a possible counterexample may satisfy the constraints d ≥ 0 c ≥ 0 c - d ≥ 1 where c := ↑b d := ↑aAll goals completed! 🐙 
omega could not prove the goal:
a possible counterexample may satisfy the constraints
  d ≥ 0
  c ≥ 0
  c - d ≥ 1
where
 c := ↑b
 d := ↑a
theorem int_ver (a b : Int) : a - b + b = a := a:Intb:Int⊢ a - b + b = a All goals completed! 🐙

With Mathlib you will also meet the rationals ℚ and the real numbers ℝ (all decimals, like 1.5 or π). Core Lean has neither.

What if a statement mixes types, say a Nat and an Int? Lean converts the Nat into an Int and shows the conversion with an arrow ↑:

fun n m => m + ↑n : Nat → Int → Int#check fun (n : Nat) (m : Int) => m + n 
fun n m => m + ↑n : Nat → Int → Int

Lean answers fun n m => m + ↑n : Nat → Int → Int. Read ↑n as “n, converted to an integer”: the same value, now of type Int. Such an automatic conversion is called a coercion.

You can also ask for one by hand: ((5 : Nat) : Int) is 5 as a natural number, converted to an integer.

Where the conversion happens matters:

fun a b => ↑(a - b) : Nat → Nat → Int#check fun (a b : Nat) => ((a - b : Nat) : Int) fun a b => ↑a - ↑b : Nat → Nat → Int#check fun (a b : Nat) => (a : Int) - (b : Int) 
fun a b => ↑(a - b) : Nat → Nat → Int
fun a b => ↑a - ↑b : Nat → Nat → Int

The first is ↑(a - b): subtract in Nat (stopping at 0), then convert. The second is ↑a - ↑b: convert, then subtract in Int. Take a = 3, b = 5:

example : ((3 - 5 : Nat) : Int) = 0 := rfl example : ((3 : Nat) : Int) - ((5 : Nat) : Int) = -2 := rfl

So ↑(a - b) = ↑a - ↑b is not true in general. It needs the hypothesis b ≤ a.

The same happens with real numbers in Mathlib. With n : ℕ (Mathlib writes ℕ for Nat):

-- needs Mathlib; n : ℕ, and take n = 3
(n : ℝ) / 2          -- convert, then divide: 1.5
((n / 2 : ℕ) : ℝ)    -- divide in ℕ (rounding down), then convert: 1

When you see ↑, ask two questions: which type is each operation done in, and where exactly does the conversion happen? And compare the type in the statement with the claim: a fact proved about Nat is not a fact about real numbers.

Check yourself🔗