Computation and the real numbers¶
Twice in the tutorial the real numbers refused to be computed. In chapter 2,
#eval payoff defect cooperate returned a Cauchy sequence with a hole in it
rather than 5. In chapter 3, decide failed on an inequality between two
payoffs that norm_num then proved at once. Both have the same cause, and
understanding it explains a distinction that runs through all of Lean: the
difference between computing an answer and proving one.
Two kinds of tactic¶
decide and norm_num look as though they do the same job, and on the
natural numbers they can:
/-- On the natural numbers, `decide` runs the decision procedure. -/
theorem zero_lt_one_nat : (0 : ℕ) < 1 := by
decide
/-- On the reals, `norm_num` builds a proof instead. -/
theorem zero_lt_one_real : (0 : ℝ) < 1 := by
norm_num
They work in quite different ways. decide looks for an algorithm that
answers the question, runs it inside Lean's kernel, and accepts the statement
if the algorithm says yes. The proof is the computation. norm_num never runs
anything on the numbers themselves. It assembles a chain of lemmas from
Mathlib, about how numerals, addition and order behave in an ordered field,
and hands the kernel a proof built from them.
For decide to work, then, an algorithm must exist, and in Lean an algorithm
for a yes or no question is an instance of Decidable. For the natural numbers
one is provided by Lean itself:
/-- Lean's own decision about whether `0 < 1` in the natural numbers. -/
def natLtDecision : Decidable ((0 : ℕ) < 1) := inferInstance
For the reals, Mathlib provides one too, but Lean will not even let us
define it as an ordinary function. Without the keyword noncomputable we get:
error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Real.decidableLT', which is 'noncomputable'
So we mark it:
/-- Mathlib's decision about whether `0 < 1` in the real numbers. -/
noncomputable def realLtDecision : Decidable ((0 : ℝ) < 1) := inferInstance
An instance that exists but cannot be run is exactly what decide cannot use.
Asked to decide (0 : ℝ) < 1, it explains itself in full:
Tactic `decide` failed for proposition
0 < 1
because its `Decidable` instance
Real.decidableLT 0 1
did not reduce to `isTrue` or `isFalse`.
After unfolding the instances `Classical.propDecidable`, `LinearOrder.toDecidableLT`, and `Real.decidableLT`, reduction got stuck at the `Decidable` instance
Classical.choice ⋯
The axiom of choice¶
Classical.choice is Lean's form of the axiom of choice. It asserts that
something exists without saying how to find it. Mathlib uses it to supply a
decision for every comparison of reals: for any two reals, one is less than
the other or it is not, so a decision exists. What the axiom cannot supply is
a procedure, and there is a mathematical reason for that. A real number in
Mathlib is an equivalence class of Cauchy sequences of rationals, and no
finite amount of computation on two such sequences can decide in general
whether they represent equal numbers. This is the hole that #eval showed
in chapter 2: it could print the terms of the constant sequence 5, and
nothing more.
Lean records which axioms each result depends on, and #print axioms reports
them:
'natLtDecision' does not depend on any axioms
'realLtDecision' depends on axioms: [propext, Classical.choice, Quot.sound]
Proofs may be classical¶
The two theorems at the top of this page give the same report:
'zero_lt_one_nat' does not depend on any axioms
'zero_lt_one_real' depends on axioms: [propext, Classical.choice, Quot.sound]
The proof by norm_num uses the axiom of choice, and that is no obstacle at
all. A proof only has to be checked, never run, and the kernel is as happy to
check a step that appeals to an axiom as any other. Every theorem in the
tutorial, including the capstone, depends on the same three axioms, which are
the standard foundations of Mathlib and correspond to ordinary classical
mathematics.
In summary, classical axioms are harmless in a proof and fatal in a
computation. decide needs a computation, so it fails on the reals.
norm_num needs only a proof, so it succeeds. This is also why these notes
prove things about payoffs rather than evaluate them. The payoffs are real
numbers, and in Lean real numbers are for reasoning about, not for
calculating with.
A practical rule¶
When a goal is a concrete statement about natural numbers, integers or a
finite type such as Action alone, decide is often the quickest proof.
As soon as real numbers appear, reach for norm_num, or for linarith and
positivity when the goal involves hypotheses or variables. None of these
compute with reals; all of them build proofs.