Encode a new game¶

This page shows how to write down a symmetric normal-form game so that the definitions of the tutorial, IsSymmetricNash and IsESS, apply to it. The recipe has three steps: a type of actions, a payoff function by cases, and a check that the encoding says what we meant.

A type of actions¶

We give the actions names with an inductive type, one constructor per action, inside a namespace named after the game:

namespace StagHunt

/-- The two actions in the Stag Hunt. -/
inductive Choice where
  | stag
  | hare
  deriving Repr

open Choice

The namespace matters as soon as a project has more than one game. The Prisoner's Dilemma of the tutorial already defines a top-level payoff, and a second top-level payoff would clash with it. Inside namespace StagHunt the new one is StagHunt.payoff, and the two never meet. The file ends with end StagHunt.

A payoff function by cases¶

The payoff to the first player is a function of both actions, written as one line per cell of the matrix:

/-- The payoff to the first player: 4 for hunting stag together, nothing for
hunting stag alone, and 3 for hunting hare whatever the other player does. -/
def payoff : Choice → Choice → ℝ
  | stag, stag => 4
  | stag, hare => 0
  | hare, stag => 3
  | hare, hare => 3

Lean checks that every cell is covered, and rejects the definition with a Missing cases error otherwise. Since the game is symmetric, the second player's payoff is payoff with the arguments swapped, and nothing more needs to be written.

Larger games and default cells¶

With more actions the matrix grows quadratically, and it is often clearer to list the interesting cells and let a final line cover the rest. For Rock, Paper, Scissors, in its own namespace:

/-- The three hands in Rock, Paper, Scissors. -/
inductive Hand where
  | rock
  | paper
  | scissors
  deriving Repr

open Hand

The pattern _, _ matches anything, and cases are tried from the top:

/-- The payoff to the first player: 1 for a win, -1 for a loss, 0 for a draw.
The last line covers every pair not listed above it. -/
def payoff : Hand → Hand → ℝ
  | rock, scissors => 1
  | scissors, paper => 1
  | paper, rock => 1
  | scissors, rock => -1
  | paper, scissors => -1
  | rock, paper => -1
  | _, _ => 0

The cost is that Lean can no longer warn about a forgotten cell, since the last line catches it silently. Use a default line only when the default really is the common case, as the draws are here.

A check that the encoding is right¶

A typo in a payoff matrix produces a well-formed definition of the wrong game, and Lean will not notice. The cheapest defence is to prove a fact about the game that is already known. The Stag Hunt has two pure symmetric equilibria:

/-- Hunting stag together is a symmetric Nash equilibrium. -/
theorem stag_isSymmetricNash : IsSymmetricNash payoff stag := by
  intro deviation
  cases deviation <;> norm_num [payoff]

/-- So is hunting hare together. -/
theorem hare_isSymmetricNash : IsSymmetricNash payoff hare := by
  intro deviation
  cases deviation <;> norm_num [payoff]

and Rock, Paper, Scissors has none:

/-- No hand is a symmetric Nash equilibrium: against rock, paper does better. -/
theorem not_rock_isSymmetricNash : ¬ IsSymmetricNash payoff rock := by
  intro claim
  have beaten := claim paper
  norm_num [payoff] at beaten

If a check that should succeed fails, suspect the matrix before the proof.

Games that are not symmetric¶

The definitions in these notes assume a symmetric game, so a single payoff function suffices. A game with different roles, such as Matching Pennies, needs a payoff function for each player, and definitions of equilibrium that compare each player's payoffs separately. Nothing in the recipe above changes, but the tutorial's IsSymmetricNash no longer applies.