Prove a statement for every strategy¶

Game-theoretic statements quantify: every deviation, every opponent, every pair of hands. This page shows how to prove a statement that begins with ∀, depending on whether the strategies can be listed.

Name the strategy¶

The first step is always intro, which takes an arbitrary strategy and gives it a name. Several names can be given at once for several quantifiers:

  intro first second

After this the goal is about the two named hands, and nothing is known about them yet.

Finitely many strategies¶

When the strategies form an inductive type, cases replaces a named strategy by each constructor in turn, producing one goal per action. With two named strategies, split both, and <;> applies the next tactic to every goal produced. This proves that Rock, Paper, Scissors is zero-sum, nine cases at once:

theorem payoff_zeroSum :
    ∀ first second : Hand, payoff first second = -payoff second first := by
  intro first second
  cases first <;> cases second <;> norm_num [payoff]

A statement can also take its strategy as an argument before the colon, in which case it is already named and intro is not needed:

theorem payoff_self (hand : Hand) : payoff hand hand = 0 := by
  cases hand <;> rfl

Here rfl suffices because each case is 0 = 0 once the definition is computed.

Infinitely many strategies¶

When the strategies are real numbers, such as the probability in a mixed strategy, there are no constructors and cases does not apply. The named strategy is then an arbitrary number, and the proof must work for it algebraically, as in Prove an inequality. The tutorial's capstone is the extreme case: its strategies are an arbitrary type, and the proof uses nothing about them except the definitions.

Negative statements¶

To show that no strategy has a property, prove the negation, ¬ P. It means P → False, so it starts with intro like any implication; see Encode a new game for a worked example.