Day 2: Numbers in Lean are a little different🔗

Predict what Lean computes for subtraction and division, and why it matters.

The numbers you have seen so far are natural numbers: 0, 1, 2, 3 … Lean calls their type Nat (mathematicians write ℕ).

You can ask Lean to compute with #eval. Lean’s answer is shown under the code.

5#eval 2 + 3
20#eval 4 * 5

#eval is not a theorem. It just computes one thing and shows the result.

Natural numbers have no negatives. So what is 3 - 5? Lean’s answer is that subtraction stops at zero:

0#eval 3 - 5

If you want negative numbers, use the integers, Int (ℤ). Writing (3 : Int) means “3, as an integer”:

-2#eval (3 : Int) - 5

-2

Division on Nat and Int rounds down, and % gives the remainder:

3#eval 7 / 2
1#eval 7 % 2

And dividing by zero is not an error. By convention, it gives zero:

0#eval 5 / 0

These are not bugs. Every operation in Lean must give some answer, and these choices make many theorems simpler to state.

Why does an auditor care? Because a statement can be true or false only because of these conventions. For example, on paper “a − b + b = a” is always true. With Nat it is not: take a = 1 and b = 2, then 1 − 2 + 2 = 0 + 2 = 2.

theorem paper_rule (a b : Nat) : a - b + b = a := bya: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 := ↑aomegaAll 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

(by omega asks Lean to prove an arithmetic fact automatically. It fails here, because the fact is false.)

When you see - or / in a statement, ask: which kind of numbers is this, and what happens at the edges?

Lean for All

Day 2: Numbers in Lean are a little different🔗

Check yourself🔗