Prove an inequality¶

Most statements about payoffs end in an inequality. This page shows which tactic to reach for, depending on what the inequality involves: numbers only, symbols with hypotheses, or products of symbols.

Numbers only¶

When the payoffs are numerals, unfold the payoff function and let norm_num do the arithmetic. The definitions it may unfold go in brackets:

theorem cooperate_lt_defect_against_defect :
    payoff cooperate defect < payoff defect defect := by
  norm_num [payoff]

Without [payoff] the tactic cannot see any numbers and fails with the goal unchanged. The same goes for any definition in the way.

Symbols and hypotheses¶

A game is often better stated with symbolic payoffs and hypotheses about their order, since the result then holds for a whole family of games. Here is the Prisoner's Dilemma with its payoffs left as symbols:

/-- The Prisoner's Dilemma with its four payoffs left as symbols. -/
def symbolicPayoff (temptation reward punishment sucker : ℝ) : Action → Action → ℝ
  | cooperate, cooperate => reward
  | cooperate, defect => sucker
  | defect, cooperate => temptation
  | defect, defect => punishment

To prove an inequality that follows from hypotheses by adding and scaling them, first unfold the definitions with simp only, then call linarith, which searches for a linear combination of the hypotheses:

theorem symbolic_defect_strictlyDominates_cooperate
    {temptation reward punishment sucker : ℝ}
    (greedy : reward < temptation) (fearful : sucker < punishment) :
    StrictlyDominates (symbolicPayoff temptation reward punishment sucker)
      defect cooperate := by
  intro opponent
  cases opponent
  · simp only [symbolicPayoff]
    linarith
  · simp only [symbolicPayoff]
    linarith

After simp only [symbolicPayoff] in the first case the goal is

greedy : reward < temptation
fearful : sucker < punishment
⊢ reward < temptation

which linarith closes from greedy. The unfolding step is not optional: linarith treats symbolicPayoff ... defect cooperate as an opaque quantity and, without simp only, reports that it failed to find a contradiction.

simp only [f] unfolds f and does nothing else, which keeps the goal predictable. Plain simp would also rewrite with hundreds of Mathlib lemmas, which is sometimes more than we want.

Products of symbols¶

Mixed strategies bring products of a probability with a payoff, and linarith cannot reason about products. nlinarith can, by multiplying hypotheses together before searching:

example (probability reward sucker : ℝ) (lower : 0 ≤ probability)
    (ordered : sucker ≤ reward) :
    sucker ≤ probability * reward + (1 - probability) * sucker := by
  nlinarith

On this goal linarith fails, since the proof needs the product of lower and ordered. When nlinarith also fails, it can be given a hint, a term whose sign it should use, as in nlinarith [sq_nonneg (probability - other)].

When the goal is simply that an expression is positive or non-negative, positivity is the quickest route:

example (probability other : ℝ) : 0 ≤ (probability - other) ^ 2 := by
  positivity

Unused hypotheses¶

Lean reports hypotheses a proof never uses. An earlier draft of the mixed strategy example above also assumed probability ≤ 1, and the build said:

warning: GameTheory/HowTo/Inequalities.lean:30:5: Variable name `upper` is not explicitly referenced.

The warning is worth reading as mathematics. The inequality holds for any non-negative weight, so the upper bound was never needed, and the statement is stronger without it.

Which tactic¶

In summary:

All four come from Mathlib. linarith and positivity need import Mathlib.Tactic.Linarith and import Mathlib.Tactic.Positivity.