Verify a mixed ESS in Hawk-Dove¶

This page proves that a specific mixed strategy is evolutionarily stable, using the Hawk-Dove game. The recipe works for any symmetric two-action game: reduce the expected payoff to a formula in one probability, then check the two conditions of the ESS algebraically. It builds on Define expected payoffs for mixed strategies.

The game¶

Two animals contest a resource worth \(V = 2\). A hawk fights, a dove retreats, and a fight costs the loser \(C = 4\). Since \(V < C\), the textbook answer is that playing hawk with probability \(V / C = 1/2\) is the unique ESS. The payoff matrix, with the usual convention that two hawks split value and cost equally, is:

/-- The payoff to the first player when the resource is worth 2 and a fight
costs 4: two hawks split the value and the cost, a hawk takes everything from a
dove, and two doves share. -/
def payoff : Posture → Posture → ℝ
  | hawk, hawk => -1
  | hawk, dove => 2
  | dove, hawk => 0
  | dove, dove => 1

Here Posture is a type with the two constructors hawk and dove, in its own namespace, with a hand-written Fintype instance and a lemma sum_posture for sums over it, exactly as in Define expected payoffs for mixed strategies.

A formula for the expected payoff¶

With two actions, a mixed strategy is determined by its probability of hawk. Write \(p\) and \(q\) for the hawk probabilities of the player and the opponent. Expanding the four terms of the expected payoff and simplifying gives

Proving this in Lean is the one place where the simplex has to be handled directly. The fact that the two probabilities add to one comes first:

/-- The two probabilities of a mixed strategy add up to one. -/
theorem total (strategy : stdSimplex ℝ Posture) :
    strategy hawk + strategy dove = 1 := by
  rw [← sum_posture]
  exact stdSimplex.sum_eq_one strategy

Then the formula: express each dove probability in terms of the hawk probability, unfold, and let ring finish the algebra:

/-- The expected payoff depends only on how often each player is a hawk. -/
theorem expectedPayoff_eq (mine theirs : stdSimplex ℝ Posture) :
    expectedPayoff payoff mine theirs =
      1 + mine hawk - theirs hawk - 2 * mine hawk * theirs hawk := by
  have mineDove : mine dove = 1 - mine hawk := by linarith [total mine]
  have theirsDove : theirs dove = 1 - theirs hawk := by linarith [total theirs]
  simp only [expectedPayoff, sum_posture, payoff, mineDove, theirsDove]
  ring

Before ring, the goal is the expansion written out term by term:

⊢ mine hawk * theirs hawk * -1 + mine hawk * (1 - theirs hawk) * 2 +
      ((1 - mine hawk) * theirs hawk * 0 + (1 - mine hawk) * (1 - theirs hawk) * 1) =
    1 + mine hawk - theirs hawk - 2 * mine hawk * theirs hawk

ring proves any equation that holds by the rules of algebra alone, which is exactly what this is. From here on every statement about expected payoffs is a statement about the two numbers \(p\) and \(q\).

One caution: simpa [sum_posture] using stdSimplex.sum_eq_one strategy looks like a shorter proof of total, but fails. sum_eq_one is itself a simplification lemma, so simp rewrites the fact to True before it can be used.

The candidate¶

The mixed strategy to check assigns one half to each posture. A member of the simplex is a function together with the two proofs that make it a probability distribution, supplied in angle brackets:

/-- The mixed strategy that plays hawk and dove with equal probability. -/
noncomputable def halfHawk : stdSimplex ℝ Posture :=
  ⟨fun _ => 1 / 2, fun _ => by norm_num, by rw [sum_posture]; norm_num⟩

noncomputable is required because the definition involves real numbers; see Computation and the real numbers.

The ESS conditions on paper¶

Take any mutant with hawk probability \(q \ne 1/2\). Against the resident, the mutant earns

so every mutant ties. This is the indifference that characterises any mixed equilibrium. The ESS therefore rests on the second condition, and

In the notation of the tutorial's IsESS, every mutant falls into the right branch of the disjunction.

The ESS conditions in Lean¶

The Lean proof follows the paper exactly:

/-- Playing hawk half the time is an evolutionarily stable strategy. -/
theorem halfHawk_isESS : IsESS (expectedPayoff payoff) halfHawk := by
  intro mutant distinct
  have half : halfHawk hawk = 1 / 2 := rfl
  have moved : mutant hawk ≠ 1 / 2 := by
    intro same
    apply distinct
    ext posture
    cases posture
    · rw [same]
      rfl
    · show mutant dove = 1 / 2
      linarith [total mutant]
  right
  constructor
  · rw [expectedPayoff_eq, expectedPayoff_eq, half]
    ring
  · rw [expectedPayoff_eq, expectedPayoff_eq, half]
    have gap : mutant hawk - 1 / 2 ≠ 0 := sub_ne_zero.mpr moved
    have square := mul_self_pos.mpr gap
    nlinarith

Most of the work is in moved, which turns the hypothesis that the mutant is a different mixed strategy into the fact the algebra needs, that its hawk probability differs from one half. It argues by contradiction: if the hawk probabilities agree then, since both strategies sum to one, so do the dove probabilities, and ext reduces equality of two strategies to agreement at every posture. On paper this step is too obvious to write down.

After right and constructor, the tie is closed by ring. For the second condition the goal is

⊢ 1 + mutant hawk - mutant hawk - 2 * mutant hawk * mutant hawk < 1 + 1 / 2 - mutant hawk - 2 * (1 / 2) * mutant hawk

which is the displayed inequality above. nlinarith closes it from the hint square : 0 < (mutant hawk - 1 / 2) * (mutant hawk - 1 / 2), which is where \(q \ne 1/2\) enters.

What follows¶

The capstone of the tutorial now gives the Nash property with no further work:

theorem halfHawk_isSymmetricNash : IsSymmetricNash (expectedPayoff payoff) halfHawk :=
  halfHawk_isESS.isSymmetricNash

And the pure strategies can be ruled out using the lemma about vertices. A population of hawks is invaded by doves, since \(0 > -1\):

theorem not_hawk_isSymmetricNash :
    ¬ IsSymmetricNash (expectedPayoff payoff) (stdSimplex.vertex hawk) := by
  intro claim
  have tempted := claim (stdSimplex.vertex dove)
  rw [expectedPayoff_vertex, expectedPayoff_vertex] at tempted
  norm_num [payoff] at tempted

Other games¶

The same recipe works for any symmetric two-action game with a mixed equilibrium. Only the payoff matrix, the formula in expectedPayoff_eq and the candidate change. Replacing the numbers 2 and 4 by symbols with \(V < C\), and the candidate by \(V / C\), would give the general result. It needs the hypothesis \(V < C\) and a division at every step, and is a natural extension of this page.