騎士と悪党のパズル

騎士(Knight)と悪党(Knave)の論理パズルは、著名な論理学者 Raymond Smullyan によって考案されたとされています。それ以来様々な変種が考案され続けてきました。ここでは、その中でも基本的なものを Lean で形式化し、解いていきます。

概要

Critical thinking web から問題を引用します。まずは自然言語で問題文を述べましょう。

形式化

さっそく形式化を行っていきます。まず、ある島があってそこには騎士と悪党しか住んでいないというところですが、これは Islander という型に knight と knave という部分集合が存在するというように形式化できます。そのうえで、島民が騎士か悪党のどちらかであることを axiom コマンドで仮定しましょう。

ここでは後で便利なように simp 補題も示しておくことにします。

/-- その島の住民を表す型 -/
opaque Islander : Type

/-- Islander の部分集合として定義した騎士の全体 -/
opaque knight : Islander → Prop

/-- Islander の部分集合として定義した悪党の全体 -/
opaque knave : Islander → Prop

/-- 人は騎士か悪党のどちらか -/
axiom knight_or_knave (p : Islander) : knight p ∨ knave p

/-- 人が騎士かつ悪党であることはない -/
axiom knight_ne_knave (p : Islander) : ¬(knight p ∧ knave p)

/-- 騎士でないことと悪党であることは同値 -/
@[simp] theorem of_not_knight {p : Islander} : ¬ knight p ↔ knave p := by
  have or := knight_or_knave p
  have ne := knight_ne_knave p
  constructor
  all_goals
    intro h
    simp_all

/-- 悪党でないことと騎士であることは同値 -/
@[simp] theorem of_not_knave {p : Islander} : ¬ knave p ↔ knight p := by
  have or := knight_or_knave p
  have ne := knight_ne_knave p
  constructor
  all_goals
    intro h
    simp_all

これでゾーイとメルが島民であり、騎士か悪党かのどちらかであるということは次のように表現できます。

/-- ゾーイ -/
axiom zoey : Islander

/-- メル -/
axiom mel : Islander

正直者であるとか嘘つきであるということを表現するために、誰がなんと発言したかを表現するための関数を用意します。その上で、それぞれの発言を愚直に形式化していきます。

/-- p さんが body という命題を話したという事実を表す命題 -/
opaque Islander.say (p : Islander) (body : Prop) : Prop

variable {p : Islander} {body : Prop}

/-- 騎士の発言内容はすべて真実 -/
axiom statement_of_knight (h : knight p) (say : p.say body) : body

/-- 悪党の発言内容はすべて偽 -/
axiom statement_of_knave (h : knave p) (say : p.say body) : ¬body

/-- ゾーイは「メルは悪党だ」と言った -/
axiom zoey_says : zoey.say (knave mel)

/-- メルは「ゾーイもメルも悪党ではない」と言った -/
axiom mel_says : mel.say (¬ knave zoey ∧ ¬ knave mel)

ここまでで問題文の前提部分の形式化は完了です。

残っているのは、「ゾーイとメルはそれぞれ騎士か悪党のどちらですか」と問う部分です。これは少し難しいです。

考えてみると、Lean で（証明すべき命題がわかっているときに）何かを証明するのはよくありますが、与えられた前提から何が言えるのかを明確なゴールなしに組み立てていくのはあまり見ないということにお気づきになるでしょう。この問題も、もし問いの内容が「ゾーイが騎士であることを示せ」とか「ゾーイが悪党であることを示せ」だったならば、今までの準備の下で簡単に形式化ができますが、「騎士なのか悪党なのか決定せよ」なので少し複雑になります。

ここでの解決方法は、Solution という帰納型を inductive コマンドで作成し、その項を作ってくださいという形式にすることです。

/-- `p` が騎士か悪党のどちらなのか知っていることを表す型 -/
inductive Solution (p : Islander) : Type where
  | isKnight : knight p → Solution p
  | isKnave : knave p → Solution p

この Solution の項を、p : Islander に対して作成するときに、項が isKnight から来るのか isKnave から来るのか明示しなければなりません。そしてそのために、それぞれ p が騎士であるか悪党であるかのどちらかの証明が引数に要求されることになるので、問題文を表現しているといえます。

問題

以上の準備の下で、問題は次のように表現できます。以下の sorry の部分を埋めてください。

/-- ゾーイは騎士か悪党か？-/
noncomputable def zoey_which : Solution zoey := by
  sorry

/-- メルは騎士か悪党か？-/
noncomputable def mel_which : Solution mel := by
  sorry