Theory Blue_Eyes

(*<*)
theory Blue_Eyes
  imports
    "HOL-Combinatorics.Transposition"
begin
(*>*)

section ‹Introduction›

text ‹The original problem statement \<^cite>‹xkcd› explains the puzzle well:

\begin{quotation}
A group of people with assorted eye colors live on an island.
They are all perfect logicians -- if a conclusion can be logically deduced,
they will do it instantly.
No one knows the color of their eyes.
Every night at midnight, a ferry stops at the island.
Any islanders who have figured out the color of their own eyes then leave the island, and the rest stay.
Everyone can see everyone else at all times
and keeps a count of the number of people they see with each eye color (excluding themselves),
but they cannot otherwise communicate.
Everyone on the island knows all the rules in this paragraph.

On this island there are 100 blue-eyed people,
100 brown-eyed people,
and the Guru (she happens to have green eyes).
So any given blue-eyed person can see 100 people with brown eyes and 99 people with blue eyes (and one with green),
but that does not tell him his own eye color;
as far as he knows the totals could be 101 brown and 99 blue.
Or 100 brown, 99 blue, and he could have red eyes.

The Guru is allowed to speak once (let's say at noon),
on one day in all their endless years on the island.
Standing before the islanders, she says the following:

``I can see someone who has blue eyes.''

Who leaves the island, and on what night?
\end{quotation}

It might seem weird that the Guru's declaration gives anyone any new information.
For an informal discussion, see \<^cite>‹‹Section~1.1› in "fagin1995"›.›

section ‹Modeling the world \label{sec:world}›

text ‹We begin by fixing two type variables: @{typ "'color"} and @{typ "'person"}.
The puzzle doesn't specify how many eye colors are possible, but four are mentioned.
Crucially, we must assume they are distinct. We specify the existence of colors other
than blue and brown, even though we don't mention them later, because when blue and brown
are the only possible colors, the puzzle has a different solution --- the brown-eyed logicians
may leave one day after the blue-eyed ones.

We refrain from specifying the exact population of the island, choosing to only assume
it is finite and denote a specific person as the Guru.

We could also model the Guru as an outside entity instead of a participant. This doesn't change
the answer and results in a slightly simpler proof, but is less faithful to the problem statement.›

context
  fixes blue brown green red :: 'color
  assumes colors_distinct: "distinct [blue, brown, green, red]"

  fixes guru :: 'person
  assumes "finite (UNIV :: 'person set)"
begin

text ‹It's slightly tricky to formalize the behavior of perfect logicians.
The representation we use is centered around the type of a @{emph ‹world›},
which describes the entire state of the environment. In our case, it's a function
@{typ "'person => 'color"} that assigns an eye color to everyone.@{footnote ‹We would introduce
a type synonym, but at the time of writing Isabelle doesn't support including type variables fixed
by a locale in a type synonym.›}

The only condition known to everyone and not dependent on the observer is Guru's declaration:›

definition valid :: "('person ⇒ 'color) ⇒ bool" where
  "valid w ⟷ (∃p. p ≠ guru ∧ w p = blue)"

text ‹We then define the function @{term "possible n p w w'"}, which returns @{term True}
if on day ‹n› the potential world ‹w'› is plausible from the perspective of person ‹p›,
based on the observations they made in the actual world ‹w›.

Then, @{term "leaves n p w"} is @{term True} if ‹p› is able to unambiguously deduce
the color of their own eyes, i.e. if it is the same in all possible worlds. Note that if ‹p› actually
left many moons ago, this function still returns @{term True}.›

fun leaves :: "nat ⇒ 'person ⇒ ('person ⇒ 'color) ⇒ bool"
  and possible :: "nat ⇒ 'person ⇒ ('person ⇒ 'color) ⇒ ('person ⇒ 'color) ⇒ bool"
  where
    "leaves n p w = (∀w'. possible n p w w' ⟶ w' p = w p)" |
    "possible n p w w' ⟷ valid w ∧ valid w'
    ∧ (∀p' ≠ p. w p' = w' p')
    ∧ (∀n' < n. ∀p'. leaves n' p' w = leaves n' p' w')"

text ‹Naturally, the act of someone leaving can be observed by others, thus the two definitions
are mutually recursive. As such, we need to instruct the simplifier to not unfold these definitions endlessly.›
declare possible.simps[simp del] leaves.simps[simp del]

text ‹A world is possible if
  ▸ The Guru's declaration holds.
  ▸ The eye color of everyone but the observer matches.
  ▸ The same people left on each of the previous days.

Moreover, we require that the actual world ‹w› is ‹valid›, so that the relation is symmetric:›

lemma possible_sym: "possible n p w w' = possible n p w' w"
  by (auto simp: possible.simps)

text ‹In fact, ‹possible n p› is an equivalence relation:›

lemma possible_refl: "valid w ⟹ possible n p w w"
  by (auto simp: possible.simps)

lemma possible_trans: "possible n p w1 w2 ⟹ possible n p w2 w3 ⟹ possible n p w1 w3"
  by (auto simp: possible.simps)

section ‹Eye colors other than blue›

text ‹Since there is no way to distinguish between the colors other than blue,
only the blue-eyed people will ever leave. To formalize this notion, we define
a function that takes a world and replaces the eye color of a specified person.
The original color is specified too, so that the transformation composes nicely
with the recursive hypothetical worlds of @{const possible}.›

definition try_swap :: "'person ⇒ 'color ⇒ 'color ⇒ ('person ⇒ 'color) ⇒ ('person ⇒ 'color)" where
  "try_swap p c⇩1 c⇩2 w x = (if c⇩1 = blue ∨ c⇩2 = blue ∨ x ≠ p then w x else transpose c⇩1 c⇩2 (w x))"

lemma try_swap_valid[simp]: "valid (try_swap p c⇩1 c⇩2 w) = valid w"
  by (cases ‹c⇩1 = blue›; cases ‹c⇩2 = blue›)
    (auto simp add: try_swap_def valid_def transpose_eq_iff)

lemma try_swap_eq[simp]: "try_swap p c⇩1 c⇩2 w x = try_swap p c⇩1 c⇩2 w' x ⟷ w x = w' x"
  by (auto simp add: try_swap_def transpose_eq_iff)

lemma try_swap_inv[simp]: "try_swap p c⇩1 c⇩2 (try_swap p c⇩1 c⇩2 w) = w"
  by (rule ext) (auto simp add: try_swap_def swap_id_eq)

lemma leaves_try_swap[simp]:
  assumes "valid w"
  shows "leaves n p (try_swap p' c⇩1 c⇩2 w) = leaves n p w"
  using assms
proof (induction n arbitrary: p w rule: less_induct)
  case (less n)
  have "leaves n p w" if "leaves n p (try_swap p' c⇩1 c⇩2 w)" for w
  proof (unfold leaves.simps; rule+)
    fix w'
    assume "possible n p w w'"
    then have "possible n p (try_swap p' c⇩1 c⇩2 w) (try_swap p' c⇩1 c⇩2 w')"
      by (fastforce simp: possible.simps less.IH)
    with ‹leaves n p (try_swap p' c⇩1 c⇩2 w)› have "try_swap p' c⇩1 c⇩2 w' p = try_swap p' c⇩1 c⇩2 w p"
      unfolding leaves.simps
      by simp
    thus "w' p = w p" by simp
  qed

  with try_swap_inv show ?case by auto
qed

text ‹This lets us prove that only blue-eyed people will ever leave the island.›

proposition only_blue_eyes_leave:
  assumes "leaves n p w" and "valid w"
  shows "w p = blue"
proof (rule ccontr)
  assume "w p ≠ blue"
  then obtain c where c: "w p ≠ c"  "c ≠ blue"
    using colors_distinct
    by (metis distinct_length_2_or_more) 

  let ?w' = "try_swap p (w p) c w"
  have "possible n p w ?w'"
    using ‹valid w› apply (simp add: possible.simps)
    by (auto simp: try_swap_def)
  moreover have "?w' p ≠ w p"
    using c ‹w p ≠ blue› by (auto simp: try_swap_def)
  ultimately have "¬ leaves n p w"
    by (auto simp: leaves.simps)
  with assms show False by simp
qed

section "The blue-eyed logicians"

text ‹We will now consider the behavior of the logicians with blue eyes. First,
some simple lemmas. Reasoning about set cardinalities often requires considering infinite
sets separately. Usefully, all sets of people are finite by assumption.›

lemma people_finite[simp]: "finite (S::'person set)"
proof (rule finite_subset)
  show "S ⊆ UNIV" by auto
  show "finite (UNIV::'person set)" by fact
qed

text ‹Secondly, we prove a destruction rule for @{const possible}. It is strictly weaker than
the definition, but thanks to the simpler form, it's easier to guide the automation with it.›
lemma possibleD_colors:
  assumes "possible n p w w'" and "p' ≠ p"
  shows "w' p' = w p'"
  using assms unfolding possible.simps by simp

text ‹A central concept in the reasoning is the set of blue-eyed people someone can see.›
definition blues_seen :: "('person ⇒ 'color) ⇒ 'person ⇒ 'person set" where
  "blues_seen w p = {p'. w p' = blue} - {p}"

lemma blues_seen_others:
  assumes "w p' = blue" and "p ≠ p'"
  shows "w p = blue ⟹ card (blues_seen w p) = card (blues_seen w p')"
    and "w p ≠ blue ⟹ card (blues_seen w p) = Suc (card (blues_seen w p'))"
proof -
  assume "w p = blue"
  then have "blues_seen w p' = blues_seen w p ∪ {p} - {p'}"
    by (auto simp add: blues_seen_def)
  moreover have "p ∉ blues_seen w p"
    unfolding blues_seen_def by auto
  moreover have "p' ∈ blues_seen w p ∪ {p}"
    unfolding blues_seen_def using ‹p ≠ p'› ‹w p' = blue› by auto
  ultimately show "card (blues_seen w p) = card (blues_seen w p')"
    by simp
next
  assume "w p ≠ blue"
  then have "blues_seen w p' = blues_seen w p - {p'}"
    by (auto simp add: blues_seen_def)
  moreover have "p' ∈ blues_seen w p"
    unfolding blues_seen_def using ‹p ≠ p'› ‹w p' = blue› by auto
  ultimately show "card (blues_seen w p) = Suc (card (blues_seen w p'))"
    by (simp only: card_Suc_Diff1 people_finite)
qed

lemma blues_seen_same[simp]:
  assumes "possible n p w w'"
  shows "blues_seen w' p = blues_seen w p"
  using assms
  by (auto simp: blues_seen_def possible.simps)

lemma possible_blues_seen:
  assumes "possible n p w w'"
  assumes "w p' = blue" and "p ≠ p'"
  shows "w' p = blue ⟹ card (blues_seen w p) = card (blues_seen w' p')"
    and "w' p ≠ blue ⟹ card (blues_seen w p) = Suc (card (blues_seen w' p'))"
  using possibleD_colors[OF ‹possible n p w w'›] and blues_seen_others assms
  by (auto simp flip: blues_seen_same)

text ‹Finally, the crux of the solution. We proceed by strong induction.›

lemma blue_leaves:
  assumes "w p = blue" and "valid w"
    and guru: "w guru ≠ blue"
  shows "leaves n p w ⟷ n ≥ card (blues_seen w p)"
  using assms
proof (induction n arbitrary: p w rule: less_induct)
  case (less n)
  show ?case
  proof
    ― ‹First, we show that day ‹n› is sufficient to deduce that the eyes are blue.›
    assume "n ≥ card (blues_seen w p)"
    have "w' p = blue" if "possible n p w w'" for w'
    proof (cases "card (blues_seen w' p)")
      case 0
      moreover from ‹possible n p w w'› have "valid w'"
        by (simp add: possible.simps)
      ultimately show "w' p = blue"
        unfolding valid_def blues_seen_def by auto
    next
      case (Suc k)
      ― ‹We consider the behavior of somebody else, who also has blue eyes.›
      then have "blues_seen w' p ≠ {}"
        by auto
      then obtain p' where "w' p' = blue" and "p ≠ p'"
        unfolding blues_seen_def by auto
      then have "w p' = blue"
        using possibleD_colors[OF ‹possible n p w w'›] by simp

      have "p ≠ guru"
        using ‹w p = blue› and ‹w guru ≠ blue› by auto
      hence "w' guru ≠ blue"
        using ‹w guru ≠ blue› and possibleD_colors[OF ‹possible n p w w'›] by simp

      have "valid w'"
        using ‹possible n p w w'› unfolding possible.simps by simp

      show "w' p = blue"
      proof (rule ccontr)
        assume "w' p ≠ blue"
        ― ‹If our eyes weren't blue, then ‹p'› would see one blue-eyed person less than us.›
        with possible_blues_seen[OF ‹possible n p w w'› ‹w p' = blue› ‹p ≠ p'›]
        have *: "card (blues_seen w p) = Suc (card (blues_seen w' p'))"
          by simp
        ― ‹By induction, they would've left on day ‹k = blues_seen w' p'›.›
        let ?k = "card (blues_seen w' p')"
        have "?k < n"
          using ‹n ≥ card (blues_seen w p)› and * by simp
        hence "leaves ?k p' w'"
          using ‹valid w'› ‹w' p' = blue› ‹w' guru ≠ blue›
          by (intro less.IH[THEN iffD2]; auto)
        ― ‹However, we know that actually, ‹p'› didn't leave that day yet.›
        moreover have "¬ leaves ?k p' w"
        proof
          assume "leaves ?k p' w"
          then have "?k ≥ card (blues_seen w p')"
            using ‹?k < n› ‹w p' = blue› ‹valid w› ‹w guru ≠ blue›
            by (intro less.IH[THEN iffD1]; auto)

          have "card (blues_seen w p) = card (blues_seen w p')"
            by (intro blues_seen_others; fact)
          with * have "?k < card (blues_seen w p')"
            by simp
          with ‹?k ≥ card (blues_seen w p')› show False by simp
        qed
        moreover have "leaves ?k p' w' = leaves ?k p' w"
          using ‹possible n p w w'› ‹?k < n›
          unfolding possible.simps by simp
        ultimately show False by simp
      qed
    qed
    thus "leaves n p w"
      unfolding leaves.simps using ‹w p = blue› by simp
  next
    ― ‹Then, we show that it's not possible to deduce the eye color any earlier.›
    {
      assume "n < card (blues_seen w p)"
      ― ‹Consider a hypothetical world where ‹p› has brown eyes instead. We will prove that this
        world is ‹possible›.›
      let ?w' = "w(p := brown)"
      have "?w' guru ≠ blue"
        using ‹w guru ≠ blue› ‹w p = blue›
        by auto
      have "valid ?w'"
      proof -
        from ‹n < card (blues_seen w p)› have "card (blues_seen w p) ≠ 0" by auto
        hence "blues_seen w p ≠ {}"
          by auto
        then obtain p' where "p' ∈ blues_seen w p"
          by auto
        hence "p ≠ p'" and "w p' = blue"
          by (auto simp: blues_seen_def)
        hence "?w' p' = blue" by auto
        with ‹?w' guru ≠ blue› show "valid ?w'"
          unfolding valid_def by auto
      qed
      moreover have "leaves n' p' w = leaves n' p' ?w'" if "n' < n" for n' p'
      proof -
        have not_leavesI: "¬leaves n' p' w'"
          if "valid w'"  "w' guru ≠ blue" and P: "w' p' = blue ⟹ n' < card (blues_seen w' p')" for w'
        proof (cases "w' p' = blue")
          case True
          then have "leaves n' p' w' ⟷ n' ≥ card (blues_seen w' p')"
            using less.IH ‹n' < n› ‹valid w'› ‹w' guru ≠ blue›
            by simp
          with P[OF ‹w' p' = blue›] show "¬leaves n' p' w'" by simp
        next
          case False
          then show "¬ leaves n' p' w'"
            using only_blue_eyes_leave ‹valid w'› by auto
        qed

        have "¬leaves n' p' w"
        proof (intro not_leavesI)
          assume "w p' = blue"
          with ‹w p = blue› have "card (blues_seen w p) = card (blues_seen w p')"
            apply (cases "p = p'", simp)
            by (intro blues_seen_others; auto)
          with ‹n' < n› and ‹n < card (blues_seen w p)› show "n' < card (blues_seen w p')"
            by simp
        qed fact+

        moreover have "¬ leaves n' p' ?w'"
        proof (intro not_leavesI)
          assume "?w' p' = blue"
          with colors_distinct have "p ≠ p'" and "?w' p ≠ blue" by auto
          hence "card (blues_seen ?w' p) = Suc (card (blues_seen ?w' p'))"
            using ‹?w' p' = blue› 
            by (intro blues_seen_others; auto)
          moreover have "blues_seen w p = blues_seen ?w' p"
            unfolding blues_seen_def by auto
          ultimately show "n' < card (blues_seen ?w' p')"
            using ‹n' < n› and ‹n < card (blues_seen w p)›
            by auto
        qed fact+

        ultimately show "leaves n' p' w = leaves n' p' ?w'" by simp
      qed
      ultimately have "possible n p w ?w'"
        using ‹valid w›
        by (auto simp: possible.simps)
      moreover have "?w' p ≠ blue"
        using colors_distinct by auto
      ultimately have "¬ leaves n p w"
        unfolding leaves.simps
        using ‹w p = blue› by blast
    }
    then show "leaves n p w ⟹ n ≥ card (blues_seen w p)"
      by fastforce
  qed
qed

text ‹This can be combined into a theorem that describes the behavior of the logicians based
on the objective count of blue-eyed people, and not the count by a specific person. The xkcd
puzzle is the instance where ‹n = 99›.›

theorem blue_eyes:
  assumes "card {p. w p = blue} = Suc n" and "valid w" and "w guru ≠ blue"
  shows "leaves k p w ⟷ w p = blue ∧ k ≥ n"
proof (cases "w p = blue")
  case True
  with assms have "card (blues_seen w p) = n"
    unfolding blues_seen_def by simp
  then show ?thesis
    using ‹w p = blue› ‹valid w› ‹w guru ≠ blue› blue_leaves
    by simp
next
  case False
  then show ?thesis
    using only_blue_eyes_leave ‹valid w› by auto
qed

end

(*<*)
end
(*>*)

section ‹Future work›

text ‹After completing this formalization, I have been made aware of epistemic logic.
The @{emph ‹possible worlds›} model in \cref{sec:world} turns out to be quite similar
to the usual semantics of this logic. It might be interesting to solve this puzzle within
the axiom system of epistemic logic, without explicit reasoning about possible worlds.›