Proving · 10 min

Proving program properties

Lean lets executable definitions and mathematical statements refer to each other directly. A theorem can describe exactly what a function computes.

The proof below follows from the definition. This is a small first step toward verification: larger developments prove invariants, boundary conditions, and algorithmic correctness. A checked theorem establishes the stated property; it does not establish every possible property of a program.

Exercise

Finish inc_spec with rfl, then run the program.

def inc (n : Nat) : Nat := n + 1

theorem inc_spec (n : Nat) : inc n = n + 1 := by
  sorry

def main : IO Unit := do
  IO.println s!"inc 41 = {inc 41}"

def inc (n : Nat) : Nat := n + 1

theorem inc_spec (n : Nat) : inc n = n + 1 := by
  rfl

def main : IO Unit := do
  IO.println s!"inc 41 = {inc 41}"

Related example