2. A game as a Lean object¶
In this chapter we write down the Prisoner's Dilemma. Nothing is proved. The work is entirely in saying, precisely enough for a machine, what the game is, and it is worth doing slowly, because in formalisation the definitions are usually harder than the proofs.
Create GameTheory/PrisonersDilemma.lean and add it to GameTheory.lean
beside the directory, which should now read:
The new file itself begins by importing what it needs from Mathlib: the real
numbers, and the norm_num tactic that we start using in chapter 3.
Mathlib is large enough that importing all of it is slow, so a file imports only the parts it uses. This is worth remembering, because the symptom of a missing import is rarely an error about imports. It is a tactic that runs, reports no problem, and leaves the goal untouched.
The actions¶
A player has two actions. We could label them 0 and 1, but Lean lets us name them, and named things are easier to read in a goal three chapters from now:
/-- The two actions available to a player in the Prisoner's Dilemma. -/
inductive Action where
| cooperate
| defect
deriving Repr
An inductive type is defined by listing the ways of building one. Here
there are two, and they take no arguments, so Action has exactly two
values. This is not a numbering of the actions, it is the actions themselves,
and Lean now knows that these two are the only possibilities.
The deriving clause asks Lean to generate a way of printing an action, so
that Lean can show us one. We use it at the end of this chapter.
The constructors are really called Action.cooperate and Action.defect. To
write the short names we open the namespace:
The payoffs¶
The payoff to the first player is a function of both players' actions. In Lean we give it by cases:
/-- The payoff to the first player, with the conventional values: reward 3 for
mutual cooperation, temptation 5, sucker's payoff 0, punishment 1. -/
def payoff : Action → Action → ℝ
| cooperate, cooperate => 3
| cooperate, defect => 0
| defect, cooperate => 5
| defect, defect => 1
Each line is one cell of the payoff matrix, read as: given these two actions,
the value is this. The pattern | defect, cooperate => 5 says that a
defector meeting a cooperator receives the temptation payoff.
Notably, Lean checks that the cases are exhaustive. Delete a line and the definition is rejected, with an error naming the case that was left out. A payoff matrix with a missing cell is not a thing we can accidentally write down here, which is a small example of what formalisation buys.
We have written only the first player's payoffs. The game is symmetric, so
the second player's payoff for a profile is payoff with the arguments the
other way round. We will lean on that symmetry throughout.
What Lean makes of it¶
Ask Lean what it now knows:
It answers:
The first is familiar from chapter 1: Action is a type, and types have type
Type.
The second repays a closer look. We might have expected something like Action
× Action → ℝ, a function of a pair. Instead the arrows chain: payoff takes
an Action and returns Action → ℝ, a function still waiting for the second
action. Feeding it both arguments is two applications, written payoff defect
cooperate.
This is called currying, and it is the default in Lean. It is not a
technicality we are stuck with. It means that payoff defect is itself a
perfectly good object, the payoff to a defector as a function of what the
opponent does, and that is exactly the kind of thing we shall want to compare
in chapter 4.
Why we do not evaluate¶
Lean can print a value:
That works because we derived Repr. It is tempting to try the same on a
payoff, and the result is instructive rather than useful:
We asked for 5 and got a Cauchy sequence with a hole in it. Nothing is
broken. A real number in Mathlib is an equivalence class of Cauchy sequences
of rationals, and #eval is showing us the representative it can see, namely
the constant sequence 5, together with a sorry standing in for the part
that cannot be computed. Real numbers are not computable, and #eval is a
tool for computation.
This is the moment to change habit. We will not be evaluating payoffs; we will be proving things about them. The question 'is the temptation payoff greater than the reward?' is not answered by running the function, but by a proof, and that is chapter 3. Why the reals behave this way is discussed in Computation and the real numbers.
Where we are¶
The Prisoner's Dilemma now exists as a Lean object: a type with two values, and a function assigning a real number to each pair of them. Everything in the remaining chapters is built on this, and none of it required a single proof.
In chapter 3 we prove our first statement about the game.