Equality with an unknown input

In Lean foundations every claim was about concrete values, such as 4 + 4 = 8. This course is about claims for every value, and about how a proof is built, one step at a time. Here (n : Nat) before the colon means the theorem must hold for any natural number n. You cannot pick a convenient one.

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 equality is still true, but proving it takes reasoning rather than computation; Proofs about your programs introduces a tactic for exactly that.

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.