Equality with an unknown input

The foundations course proved properties of definitions by unfolding them and letting tactics such as simp and omega finish. This course slows down and looks at how a proof is built, one step at a time, starting with the smallest step there is. Here (n : Nat) before the colon means the theorem must hold for any natural number n. You cannot choose a convenient value for it.

Read the goal state from top to bottom: n : Nat is the available value, and ⊢ n + 0 = n is the claim to prove. The statement is a law about every n, not a test at one input.

For equality, rfl works when both sides reduce to the same expression. The definition of natural-number addition computes by inspecting its second argument. In n + 0, that argument is already zero, so the expression reduces to n even though n itself is unknown.

Order matters for computation. 0 + n is stuck on its unknown second argument; rfl does not prove 0 + n = n. The mathematical equality is still true, but establishing it needs arithmetic reasoning such as omega, or an induction argument that a later course builds by hand.

Worked example

-- Example 1: both sides compute to 10, so rfl succeeds.
example : 2 * 5 = 10 := by
  rfl

-- Example 2 (commented out, because it fails): n + 1 = 1 + n is true for
-- every n, but the two sides do not reduce to the same expression. This is
-- the message rfl reports:
--   example (n : Nat) : n + 1 = 1 + n := by rfl
--
--   Tactic `rfl` failed: The left-hand side
--     n + 1
--   is not definitionally equal to the right-hand side
--     1 + n
--   n : Nat
--   ⊢ n + 1 = 1 + n

An example is a theorem without a name, checked exactly the same way. Example 1 computes. Example 2 cannot, so it is shown as a comment together with Lean’s reply; the message prints the two sides Lean was left holding. Reading those two lines is a faster habit than trying another tactic.