Write a new definition¶

This page shows how to add a game-theoretic concept, such as a best response or weak dominance, in the style of the tutorial's definitions, and how to check that it means what was intended. The checks matter more than the definition: Lean verifies that a definition is well formed, never that it is the right one.

The shape of a definition¶

A concept that is true or false of some strategies is a def whose type is Prop. The type of strategies is an implicit argument, so that the definition applies to every game; the payoff function and the strategies involved are explicit:

/-- A strategy is a best response to an opponent's strategy if no alternative
pays more against it. -/
def IsBestResponse {Strategy : Type} (payoffs : Strategy → Strategy → ℝ)
    (response opponent : Strategy) : Prop :=
  ∀ alternative : Strategy, payoffs alternative opponent ≤ payoffs response opponent

Three conventions are worth keeping. Names of statements are in upper camel case, often starting with Is. Every definition has a documentation comment saying in words what it means. And comparisons are written with the worse payoff on the left, so that goal states read consistently.

A concept with several conditions joins them with ∧, and one that asks for a witness uses ∃, typed \ex:

/-- One strategy weakly dominates another if it never pays less and sometimes pays
strictly more. -/
def WeaklyDominates {Strategy : Type} (payoffs : Strategy → Strategy → ℝ)
    (better worse : Strategy) : Prop :=
  (∀ opponent : Strategy, payoffs worse opponent ≤ payoffs better opponent) ∧
    ∃ opponent : Strategy, payoffs worse opponent < payoffs better opponent

Agreement with an existing definition¶

The strongest check is to prove that the new definition agrees with something already trusted. A symmetric Nash equilibrium is a strategy that is a best response to itself, and when the definitions are right Lean can see this without any argument at all:

theorem isSymmetricNash_iff_isBestResponse {Strategy : Type}
    {payoffs : Strategy → Strategy → ℝ} {candidate : Strategy} :
    IsSymmetricNash payoffs candidate ↔ IsBestResponse payoffs candidate candidate :=
  Iff.rfl

Iff.rfl succeeds only when the two sides unfold to the same statement. Had the inequality in IsBestResponse been written the wrong way round, this line would fail, which is exactly the point.

A known implication¶

A second check is to prove a relationship the concept should satisfy. Strict dominance should imply weak dominance, and trying to prove it reveals a hidden assumption:

theorem StrictlyDominates.weaklyDominates {Strategy : Type} [Nonempty Strategy]
    {payoffs : Strategy → Strategy → ℝ} {better worse : Strategy}
    (strict : StrictlyDominates payoffs better worse) :
    WeaklyDominates payoffs better worse := by
  constructor
  · intro opponent
    exact le_of_lt (strict opponent)
  · obtain ⟨opponent⟩ := ‹Nonempty Strategy›
    exact ⟨opponent, strict opponent⟩

Without [Nonempty Strategy] the theorem is false. If the opponent has no strategies at all, strict dominance holds vacuously, but weak dominance asks for an opponent strategy that exists. On paper nobody considers a game with no strategies; in Lean the edge case must be ruled out explicitly, and finding such edge cases is one of the main benefits of formalising a definition.

Known examples¶

Finally, a definition should give the known answer on a familiar game. See Encode a new game for checks of this kind, and Definitions and proofs for why they are worth the trouble.