Proofs

A program with a proof

Write a function, prove a property about it, and execute it in the same file.

def double (n : Nat) : Nat := n + n

-- Every output is the sum of two equal numbers
theorem double_eq (n : Nat) : double n = n + n := by
  rfl

-- Check a concrete result
example : double 21 = 42 := by
  decide

def main : IO Unit := do
  IO.println s!"double 21 = {double 21}"
  IO.println "The function above also has a checked proof."

Explanation

`def + theorem`

A function and a theorem can coexist. Proving a property does not replace executing the program.

`example`

An unnamed declaration. Here it checks a proposition.

`decide`

Solves a proposition using its decision procedure, which is suitable for this concrete equality.

Expected output

Reference only. Run the file to check its actual result.

double 21 = 42
The function above also has a checked proof.

Exercise

Change double to n * 2. What happens to the rfl proof?