Split a proof into cases¶

Many arguments in game theory divide into cases: the deviation equals the resident or it does not, the mutant does strictly worse or it ties. Lean has one tactic for each kind of split. This page lists them with an example of each.

The constructors of a type¶

cases splits a variable of an inductive type into one goal per constructor. For a Prisoner's Dilemma action, that is one goal for cooperate and one for defect:

  intro opponent
  cases opponent

The two goals are labelled case cooperate and case defect, and the variable is replaced by the constructor everywhere, including in hypotheses.

Whether a statement holds¶

by_cases splits on any statement, whether or not a type is involved. It gives a goal case pos, where the statement holds, and a goal case neg, where it does not. This is how the capstone separates the resident from other strategies:

  by_cases same : deviation = resident
  · rw [same]

Alternatives in a hypothesis¶

When a hypothesis says P ∨ Q, rcases produces one goal assuming P and one assuming Q. A pattern names the pieces: | separates alternatives, and ⟨ ⟩ takes apart a conjunction.

  · rcases stable deviation same with worse | ⟨tie, _⟩
    · exact le_of_lt worse
    · exact le_of_eq tie

Existence in a hypothesis¶

A hypothesis ∃ x, P x does not split into several goals, but it must still be taken apart before it can be used. obtain names the witness and the fact about it:

  obtain ⟨opponent, gap⟩ := weak.2
  exact ⟨opponent, ne_of_lt gap⟩

One case at a time¶

After a split, each goal is handled under its own ·. The dot is typed \., and Lean checks that the tactics under it close that goal before moving on. When every case is closed by the same tactic, <;> avoids the repetition, as in Prove a statement for every strategy.