Numbers, text and true or false
Nat, Int, Bool and String, and the subtraction that stops at zero.
In this course 5 / 11
Four types cover most everyday values: Nat for 0, 1, 2, …, Int for whole numbers including negative ones, Bool for true and false, and String for text. Lean picks a type for a number by itself; write (2 : Int) when you want a different one.
The type changes what operations do. Nat has no negative numbers, so subtraction that would go below zero stops at 0:
#eval (2 : Nat) - 5
#eval (2 : Int) - 50 -3
This is called truncated subtraction, and it is deliberate: the answer has to be a Nat, and 0 is the closest one. Division on Nat rounds down for the same reason: 7 / 2 is 3.
It also breaks a rule you may take for granted. On Nat, a - b + b = a is not always true. The first exercise asks you to find numbers where it fails.
The exercises are definitions you write, with read-only checks underneath that must compile. by decide in a check works out a claim about concrete values and accepts it only if it is true.
Worked example
#eval (2 : Nat) - 5 -- 0
#eval (2 : Int) - 5 -- -3
example : gap 2 5 = 0 := by
rfl
example : (2 : Int) - 5 = -3 := by
rfl
At the start of the proof on line 4. Everything above ⊢ may be used; the line below it is what must be proved.
The same subtraction, two types, two answers.
The type decides which values exist and what operations do. On Nat, subtraction stops at zero and division rounds down.
Change the numbers in x and y so that x - y + y is not equal to x. With the starting values the check fails, because for them the rule holds.
Suggested steps
- Choose values for which the rule fails
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:These lines run underneath whatever you write. They are what decides the exercise, so your names and types have to match them.
-- Passes only when your values break the law. example : x - y + y ≠ x := by decide
Knowledge check
Answer without looking back, then check your reasoning.
correct