Values and core types

Every expression has a type, and the type decides which operations apply to it. Nat holds 0, 1, 2, … and nothing below zero. Int adds the negative numbers. Bool holds true and false. String holds text. Lean infers most types; an annotation such as (2 : Int) says which one you meant when the literal alone is ambiguous.

Subtraction on Nat is truncated: when the result would be negative it is 0. So 2 - 5 is 0, and #eval will say so. That is not a bug to route around. Nat contains no negative values, subtraction still has to return a Nat, and 0 is the answer Lean commits to.

Truncation breaks arithmetic you may take for granted. On Nat, the law (a - b) + b = a is not true for every a and b. Finding values where it fails is the first exercise below, and it is the quickest way to make truncation stick. Chains of subtractions and additions have to be read left to right, one step at a time, exactly as Lean evaluates them.

Choosing the type is part of stating the problem. A count of items is a Nat and truncation is the behaviour you want. A temperature change is an Int. A flag is a Bool, not a Nat that happens to be 0 or 1, because the type then rules out the values you never meant to allow.

The exercises below are written as definitions you edit, and read-only checks underneath have to compile. The check by decide evaluates a claim about concrete values and accepts it only if it is true.

Worked example

#eval (2 : Nat) - 5     -- 0, truncated at zero
#eval (2 : Int) - 5     -- -3
#check (2 : Int) - 5    -- 2 - 5 : Int

-- On Int the answer is negative:
example : (2 : Int) - 5 = -3 := by
  rfl

-- On Nat the same subtraction stops at zero:
example : gap 2 5 = 0 := by
  rfl

Both examples subtract a larger number from a smaller one. The only difference is the type, and the type changes the answer. Keep that in mind when you look for values that break the law.