Day 3: Variables mean “for every”🔗

Read a theorem with variables as a claim about every value.

A theorem can talk about every number at once:

theorem add_zero_example (n : Nat) : n + 0 = n := rfl

The (n : Nat) before the colon introduces a variable n that is a natural number. Read the whole thing as:

For every natural number n, n + 0 = n.

The variable is part of the statement, even though it sits before the colon.

Lean has a symbol for “for every”: ∀. This states exactly the same thing, with the variable after the colon:

theorem add_zero_again : ∀ n : Nat, n + 0 = n := fun Variable name `n` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _n

Note: This linter can be disabled with `set_option linter.unusedVariables false`n => rfl

Both versions mean the same. Writers put variables before the colon because it is shorter. You will see both styles.

Several variables can share one pair of brackets, (a b : Nat), meaning “for all natural numbers a and b”.

Because the claim is about every value, you can use a theorem on any particular value. Here a library theorem, Nat.add_comm, states that a + b = b + a for all a and b, and we use it as the proof for 3 and 4:

theorem swap_example : 3 + 4 = 4 + 3 := Nat.add_comm 3 4

So a proof can be the name of another theorem applied to some values. You do not need to understand a proof to understand a statement, and for auditing, the statement matters most.

You will also meet curly braces:

theorem pos_ne_zero {n : Nat} (h : n > 0) : n ≠ 0 := byn:Nath:n > 0⊢ n ≠ 0 omegaAll goals completed! 🐙

{n : Nat} still means “for every natural number n”. The braces only tell Lean to figure out n by itself whenever the theorem is used. For reading, treat { } exactly like ( ).

(The (h : n > 0) part is a hypothesis: “if n > 0”. That is tomorrow’s lesson.)

Lean for All

Day 3: Variables mean “for every”🔗

Check yourself🔗