Theory Nash_Equilibrium

theory Nash_Equilibrium
  imports Main
begin

section ‹Pure Nash Equilibria›

text ‹
  Nash's equilibrium concept says that a strategy profile is stable when no
  player can improve by changing only her own strategy.  This entry formalizes
  the pure-strategy version for finite strategic-form games with a common
  strategy type.

  The central locale below fixes a finite set of players, a finite nonempty
  strategy set for each player, and a payoff function.  The player and strategy
  types are finite; this keeps the profile space finite while still allowing
  player-indexed strategy restrictions.

  The development is intended as a reusable finite-game layer: the basic locale
  gives pure Nash equilibria and best responses, later locales derive existence
  from ordinal potentials and dominant strategies, and the companion mixed
  theory proves the finite mixed-equilibrium theorem using HOL-Analysis.
›

locale finite_game =
  fixes players :: "'p::finite set"
    and strategies :: "'p ⇒ 's::finite set"
    and payoff :: "'p ⇒ ('p ⇒ 's) ⇒ 'u::preorder"
  assumes nonempty_strategies: "i ∈ players ⟹ strategies i ≠ {}"
begin

definition profiles :: "('p ⇒ 's) set" where
  "profiles = {s. ∀i∈players. s i ∈ strategies i}"

definition deviation :: "('p ⇒ 's) ⇒ 'p ⇒ 's ⇒ ('p ⇒ 's)" where
  "deviation s i x = s(i := x)"

definition Nash_equilibrium :: "('p ⇒ 's) ⇒ bool" where
  "Nash_equilibrium s ⟷
     s ∈ profiles ∧
     (∀i∈players. ∀x∈strategies i.
        payoff i (deviation s i x) ≤ payoff i s)"

definition best_response_to :: "('p ⇒ 's) ⇒ 'p ⇒ 's ⇒ bool" where
  "best_response_to s i x ⟷
     i ∈ players ∧ x ∈ strategies i ∧
     (∀y∈strategies i. payoff i (deviation s i y) ≤ payoff i (deviation s i x))"

definition dominant_strategy :: "'p ⇒ 's ⇒ bool" where
  "dominant_strategy i x ⟷
     i ∈ players ∧ x ∈ strategies i ∧
     (∀s∈profiles. ∀y∈strategies i.
        payoff i (deviation s i y) ≤ payoff i (deviation s i x))"

lemma profiles_iff:
  "s ∈ profiles ⟷ (∀i∈players. s i ∈ strategies i)"
  by (auto simp: profiles_def)

lemma profile_strategy:
  assumes "s ∈ profiles" "i ∈ players"
  shows "s i ∈ strategies i"
  using assms by (simp add: profiles_iff)

lemma finite_profiles [simp, intro]: "finite profiles"
  by simp

lemma profiles_nonempty: "profiles ≠ {}"
proof -
  have "∀i∈players. ∃x. x ∈ strategies i"
    using nonempty_strategies by auto
  then obtain f where f: "⋀i. i ∈ players ⟹ f i ∈ strategies i"
    by metis
  define g where "g i = f i" for i
  have "g ∈ profiles"
    using f by (auto simp: profiles_iff g_def)
  then show ?thesis
    by blast
qed

lemma deviation_apply [simp]:
  "deviation s i x j = (if j = i then x else s j)"
  by (simp add: deviation_def)

lemma deviation_self [simp]: "deviation s i (s i) = s"
  by (simp add: deviation_def)

lemma deviation_in_profiles:
  assumes "s ∈ profiles" "i ∈ players" "x ∈ strategies i"
  shows "deviation s i x ∈ profiles"
  using assms by (auto simp: profiles_iff)

lemma Nash_equilibriumI:
  assumes "s ∈ profiles"
    and "⋀i x. i ∈ players ⟹ x ∈ strategies i ⟹
      payoff i (deviation s i x) ≤ payoff i s"
  shows "Nash_equilibrium s"
  using assms by (auto simp: Nash_equilibrium_def)

lemma Nash_equilibrium_profile:
  assumes "Nash_equilibrium s"
  shows "s ∈ profiles"
  using assms by (simp add: Nash_equilibrium_def)

lemma Nash_equilibriumD:
  assumes "Nash_equilibrium s" "i ∈ players" "x ∈ strategies i"
  shows "payoff i (deviation s i x) ≤ payoff i s"
  using assms by (simp add: Nash_equilibrium_def)

lemma Nash_equilibrium_iff_best_responses:
  assumes "s ∈ profiles"
  shows "Nash_equilibrium s ⟷ (∀i∈players. best_response_to s i (s i))"
  using assms by (auto simp: Nash_equilibrium_def best_response_to_def profile_strategy)

lemma dominant_strategy_profile_is_Nash:
  assumes "s ∈ profiles"
    and dominant: "⋀i. i ∈ players ⟹ dominant_strategy i (s i)"
  shows "Nash_equilibrium s"
proof (rule Nash_equilibriumI)
  show "s ∈ profiles"
    using assms by simp
next
  fix i x
  assume ix: "i ∈ players" "x ∈ strategies i"
  have dom: "dominant_strategy i (s i)"
    using dominant ix by blast
  then have "⋀t y. t ∈ profiles ⟹ y ∈ strategies i ⟹
      payoff i (deviation t i y) ≤ payoff i (deviation t i (s i))"
    by (simp add: dominant_strategy_def)
  from this[OF assms(1) ix(2)] show "payoff i (deviation s i x) ≤ payoff i s"
    by simp
qed

end


section ‹Existence for Finite Potential Games›

text ‹
  Pure Nash equilibria need not exist in arbitrary finite games.  A standard
  positive result is that every finite game with an ordinal potential has a pure
  Nash equilibrium: choose a profile whose potential is maximal.  The definition
  used here is the one needed for the argument: every strict unilateral payoff
  improvement strictly increases the potential.  Exact and ordinal potential
  games in the sense of Monderer and Shapley satisfy this assumption.
›

locale finite_potential_game =
  finite_game players strategies payoff
  for players :: "'p::finite set"
    and strategies :: "'p ⇒ 's::finite set"
    and payoff :: "'p ⇒ ('p ⇒ 's) ⇒ 'u::linorder" +
  fixes potential :: "('p ⇒ 's) ⇒ 'v::linorder"
  assumes potential_increases:
    "⟦s ∈ profiles; i ∈ players; x ∈ strategies i;
      payoff i s < payoff i (deviation s i x)⟧
     ⟹ potential s < potential (deviation s i x)"
begin

lemma maximal_potential_profile:
  obtains s where
    "s ∈ profiles"
    "⋀t. t ∈ profiles ⟹ potential t ≤ potential s"
proof -
  let ?M = "Max (potential ` profiles)"
  have fin: "finite (potential ` profiles)"
    by simp
  have nonempty: "potential ` profiles ≠ {}"
    using profiles_nonempty by blast
  have M_in: "?M ∈ potential ` profiles"
    by (rule Max_in[OF fin nonempty])
  then obtain s where s_prof: "s ∈ profiles" and s_Max: "potential s = ?M"
    by (auto elim!: imageE)
  have max_s: "potential t ≤ potential s" if "t ∈ profiles" for t
    using Max_ge[OF fin, of "potential t"] s_Max that by auto
  show ?thesis
    using max_s s_prof that by auto
qed

theorem exists_Nash_equilibrium:
  "∃s∈profiles. Nash_equilibrium s"
proof -
  obtain s where s: "s ∈ profiles"
    and max: "⋀t. t ∈ profiles ⟹ potential t ≤ potential s"
    using maximal_potential_profile by blast
  have "Nash_equilibrium s"
  proof (rule Nash_equilibriumI)
    show "s ∈ profiles"
      by fact
  next
    fix i x
    assume ix: "i ∈ players" "x ∈ strategies i"
    show "payoff i (deviation s i x) ≤ payoff i s"
    proof (rule ccontr)
      assume "¬ payoff i (deviation s i x) ≤ payoff i s"
      then have improve: "payoff i s < payoff i (deviation s i x)"
        by simp
      have dev: "deviation s i x ∈ profiles"
        using s ix by (rule deviation_in_profiles)
      have "potential s < potential (deviation s i x)"
        using potential_increases[OF s ix improve] .
      moreover have "potential (deviation s i x) ≤ potential s"
        using max[OF dev] .
      ultimately show False
        by simp
    qed
  qed
  with s show ?thesis
    by blast
qed

end


section ‹Dominant Strategies as a Degenerate Existence Result›

text ‹
  Dominant strategies give another elementary source of equilibria.  The next
  locale packages the hypothesis that every player has a distinguished dominant
  strategy and derives existence by constructing the corresponding profile.
›

locale finite_dominant_strategy_game =
  finite_game players strategies payoff
  for players :: "'p::finite set"
    and strategies :: "'p ⇒ 's::finite set"
    and payoff :: "'p ⇒ ('p ⇒ 's) ⇒ 'u::preorder" +
  fixes dominant :: "'p ⇒ 's"
  assumes dominant: "i ∈ players ⟹ dominant_strategy i (dominant i)"
begin

definition dominant_profile :: "'p ⇒ 's" where
  "dominant_profile i = (if i ∈ players then dominant i else undefined)"

lemma dominant_profile_in_profiles:
  "dominant_profile ∈ profiles"
  using dominant by (auto simp: dominant_profile_def profiles_iff dominant_strategy_def)

theorem dominant_profile_is_Nash:
  "Nash_equilibrium dominant_profile"
  by (simp add: dominant dominant_profile_def dominant_profile_in_profiles dominant_strategy_profile_is_Nash)

end


section ‹Matching Pennies›

text ‹
  The following two-player zero-sum game shows why an existence theorem for pure
  Nash equilibria needs additional hypotheses.  The row player wants the two
  coins to match; the column player wants them to differ.  After every pure
  profile, exactly one player can improve by switching sides.
›

datatype penny_player = Row | Column

datatype coin_side = Heads | Tails

instantiation penny_player :: finite
begin

instance
proof
  show "finite (UNIV :: penny_player set)"
    by (rule finite_subset[of _ "{Row, Column}"]) (auto intro: penny_player.exhaust)
qed

end

instantiation coin_side :: finite
begin

instance
proof
  show "finite (UNIV :: coin_side set)"
    by (rule finite_subset[of _ "{Heads, Tails}"]) (auto intro: coin_side.exhaust)
qed

end

definition matching_pennies_payoff :: "penny_player ⇒ (penny_player ⇒ coin_side) ⇒ int" where
  "matching_pennies_payoff p s =
     (case p of
        Row ⇒ if s Row = s Column then 1 else 0
      | Column ⇒ if s Row = s Column then 0 else 1)"

interpretation matching_pennies:
  finite_game UNIV "λ_. UNIV" matching_pennies_payoff
  by standard auto

definition switch_coin :: "coin_side ⇒ coin_side" where
  "switch_coin x = (case x of Heads ⇒ Tails | Tails ⇒ Heads)"

lemma switch_coin_neq [simp]: "switch_coin x ≠ x"
  by (cases x) (simp_all add: switch_coin_def)

lemma coin_side_switch:
  fixes x :: coin_side
  obtains y where "y ≠ x"
proof 
  show "switch_coin x ≠ x"
    by simp
qed

lemma matching_pennies_no_pure_Nash:
  "¬ matching_pennies.Nash_equilibrium s"
proof
  assume ne: "matching_pennies.Nash_equilibrium s"
  then have profile: "s ∈ matching_pennies.profiles"
    by (rule matching_pennies.Nash_equilibrium_profile)
  show False
  proof (cases "s Row = s Column")
    case True
    obtain y where y: "y ≠ s Row"
      using coin_side_switch by blast
    have "matching_pennies_payoff Column (matching_pennies.deviation s Column y) = 1"
      using True y by (simp add: matching_pennies_payoff_def)
    moreover have "matching_pennies_payoff Column s = 0"
      using True by (simp add: matching_pennies_payoff_def)
    ultimately have "¬ matching_pennies_payoff Column (matching_pennies.deviation s Column y)
                     ≤ matching_pennies_payoff Column s"
      by simp
    moreover have "y ∈ (UNIV :: coin_side set)"
      by simp
    ultimately show False
      using matching_pennies.Nash_equilibriumD[OF ne, of Column y] by simp
  next
    case False
    obtain y where y: "y = s Column"
      by simp
    have "matching_pennies_payoff Row (matching_pennies.deviation s Row y) = 1"
      using y by (simp add: matching_pennies_payoff_def)
    moreover have "matching_pennies_payoff Row s = 0"
      using False by (simp add: matching_pennies_payoff_def)
    ultimately have "¬ matching_pennies_payoff Row (matching_pennies.deviation s Row y)
                     ≤ matching_pennies_payoff Row s"
      by simp
    moreover have "y ∈ (UNIV :: coin_side set)"
      by simp
    ultimately show False
      using matching_pennies.Nash_equilibriumD[OF ne, of Row y] by simp
  qed
qed

end