3. The first proof¶

We now prove something. The statement is deliberately small, that a defector does better than a cooperator against a defector, so that all the attention goes to the machinery rather than the mathematics.

Create GameTheory/FirstProof.lean, and add import GameTheory.FirstProof to GameTheory.lean as before. The new file begins:

import GameTheory.PrisonersDilemma

open Action

A statement to prove¶

Start with an equation. The temptation payoff is 5, and we can ask Lean to agree:

/-- The temptation payoff is five. -/
example : payoff defect cooperate = 5 := by
  norm_num [payoff]

Read the shape of that before the content. It is the same shape as the definition in chapter 2: a name, a colon and something, then := and something. In chapter 2 the thing after the colon was ℝ and the thing after := was 5. Here the thing after the colon is a statement and the thing after := is a proof.

That parallel is not a coincidence and it is the central idea of Lean. A statement is a type, and a proof of it is a value of that type, in exactly the way that 5 is a value of type ℝ. Checking a proof and checking that 5 is a real number are the same operation.

example means we are not giving the result a name, because we do not intend to use it again.

The goal¶

by switches from writing a proof directly to building one with tactics, and this is where the infoview earns its place. Put the cursor after by and Lean shows:

⊢ payoff defect cooperate = 5

In the editor, with the cursor on line 7, the goal appears under Tactic state:

The turnstile ⊢ separates what we may assume, which is nothing yet, from what we must show. This is the goal. A tactic transforms the goal, and the proof is finished when there are no goals left. If we write a tactic block that does not finish, Lean says so:

error: unsolved goals
⊢ payoff defect cooperate = 5

In the editor, a failing proof is hard to miss. Here line 7 has been changed to a plain norm_num, a mistake the next section explains. The by is underlined in red, a marker appears in the margin, and the infoview shows the error under Messages, with the goal that remains:

That message is not a failure of the setup. It is Lean telling us exactly how far we got, and we will see it often.

Why the tactic needs a hint¶

norm_num is the tactic for goals that are arithmetic once everything is written out. Here it is passed [payoff], and the brackets matter. Without them:

⊢ payoff cooperate defect < payoff defect defect

is where norm_num stops, having made no progress at all. There is no arithmetic visible to it. The goal mentions payoff, which as far as the tactic is concerned is an opaque name.

Writing norm_num [payoff] tells the tactic that it may also unfold the definition of payoff. It then sees 0 < 1, which it disposes of immediately. Passing definitions and lemmas in brackets like this is how most Lean tactics are steered, and forgetting to do it is the most common reason a tactic that ought to work does not.

A proof with no tactics at all¶

The same equation can be closed without entering tactic mode:

/-- The same equation, closed by computation rather than by a tactic. -/
example : payoff defect cooperate = 5 := rfl

rfl is the proof that something equals itself. It works here because payoff defect cooperate and 5 are the same by definition: Lean unfolds the pattern match, reaches the literal 5, and finds both sides identical. No reasoning was required, only computation.

It is worth knowing rfl exists, and worth knowing its limits. Try it on the inequality and Lean objects:

Type mismatch
  rfl
has type
  ?m = ?m
but is expected to have type
  payoff cooperate defect < payoff defect defect

rfl proves equalities and nothing else. An inequality between real numbers is a genuine mathematical claim rather than a computation, and it needs a tactic that knows about order.

A named theorem¶

Our actual target gets a name, because later chapters will refer to it:

/-- Against a defector, cooperating pays strictly less than defecting. -/
theorem cooperate_lt_defect_against_defect :
    payoff cooperate defect < payoff defect defect := by
  norm_num [payoff]

theorem is example with a name attached. The name follows the Mathlib convention of describing the statement in snake case, so that cooperate_lt_defect_against_defect can be read off as: cooperate is less than defect, against a defector. Names in Mathlib are long and predictable on purpose, since that is what makes several hundred thousand of them searchable.

The statement runs onto a second line, indented, which is ordinary Lean layout and carries no meaning beyond fitting the page.

One tactic that will not help¶

Since Action has only two values, it is natural to reach for decide, the tactic that settles a goal by running a decision procedure. It fails, at length:

Tactic `decide` failed for proposition
  payoff cooperate defect < payoff defect defect
because its `Decidable` instance
  ...
did not reduce to `isTrue` or `isFalse`.

The obstruction is not the actions, which are finite and perfectly decidable. It is the real numbers. Comparison of reals in Mathlib is defined using classical reasoning, which asserts that a comparison has an answer without providing a way to compute it, so there is nothing for decide to run. This is the same fact we met in chapter 2 when #eval returned a Cauchy sequence, and it is taken up properly in Computation and the real numbers.

Where we are¶

We have proved a statement about the Prisoner's Dilemma, and met the four things that every later proof is made of: a statement is a type, by opens tactic mode, the goal is what remains to be shown, and a tactic usually needs to be told which definitions it may unfold.

So far every proof has been about two specific actions. In chapter 4 we say something about all of them.