From 0e9002325fe5de41367640cf554b4736d178c3ee Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sun, 18 Aug 2024 20:41:06 +0900 Subject: [PATCH] =?UTF-8?q?=E9=A8=8E=E5=A3=AB=E3=81=A8=E6=82=AA=E5=85=9A?= =?UTF-8?q?=E3=81=AE=E3=83=91=E3=82=BA=E3=83=AB=E3=81=AE=E8=AA=AC=E6=98=8E?= =?UTF-8?q?=E6=96=87=E3=81=BE=E3=82=8F=E3=82=8A=E3=81=AE=E5=BE=AE=E4=BF=AE?= =?UTF-8?q?=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Exercise/KnightAndKnave.lean | 10 +++++----- Examples/Solution/KnightAndKnave.lean | 10 +++++----- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/Examples/Exercise/KnightAndKnave.lean b/Examples/Exercise/KnightAndKnave.lean index 4154b1bd..7be4f8b8 100644 --- a/Examples/Exercise/KnightAndKnave.lean +++ b/Examples/Exercise/KnightAndKnave.lean @@ -1,8 +1,8 @@ -/- # 騎士と悪党の論理パズル +/- # 騎士と悪党のパズル 騎士(Knight)と悪党(Knave)の論理パズルは、著名な論理学者 Raymond Smullyan によって考案されたとされています。それ以来様々な変種が考案され続けてきました。ここでは、その中でも基本的なものを Lean で形式化し、解いていきます。 -## 問題の内容 +## 概要 [Critical thinking web](https://philosophy.hku.hk/think/logic/knights.php) から問題を引用します。まずは自然言語で問題文を述べましょう。 @@ -11,11 +11,11 @@ あなたはゾーイとメルという２人の島民に出会いました。 ゾーイは「メルは悪党です」と言いました。 -メルは「ゾーイも私も悪党ではない」と言いました。 +メルは「ゾーイも私も悪党ではありません」と言いました。 さて、ゾーイとメルはそれぞれ騎士か悪党のどちらでしょうか？ ``` -## 問題の形式化 +## 形式化 さっそく形式化を行っていきます。まず、ある島があってそこには騎士と悪党しか住んでいないというところですが、これは `Islander` という型に `knight` と `knave` という部分集合が存在するというように形式化できます。そのうえで、島民が騎士か悪党のどちらかであることを `axiom` コマンドで仮定しましょう。 @@ -104,7 +104,7 @@ class inductive Solution (p : Islander) : Type where /- `class inductive` というものをあまり見たことがないかもしれませんが、これは普通の型クラスと異なりコンストラクタが複数ある型クラスを定義することができます。この `Solution` の場合、`p : Islander` に対してインスタンスを作成するときに、インスタンスが `isKnight` から来るのか `isKnave` から来るのか明示しなければなりません。そしてそのために、それぞれ `p` が騎士であるか悪党であるかのどちらかの証明が引数に要求されることになります。 -## 問題文 +## 問題 以上の準備の下で、問題は次のように表現できます。以下の `sorry` の部分を埋めてください。 -/ diff --git a/Examples/Solution/KnightAndKnave.lean b/Examples/Solution/KnightAndKnave.lean index f10d08b7..c5523a54 100644 --- a/Examples/Solution/KnightAndKnave.lean +++ b/Examples/Solution/KnightAndKnave.lean @@ -1,8 +1,8 @@ -/- # 騎士と悪党の論理パズル +/- # 騎士と悪党のパズル 騎士(Knight)と悪党(Knave)の論理パズルは、著名な論理学者 Raymond Smullyan によって考案されたとされています。それ以来様々な変種が考案され続けてきました。ここでは、その中でも基本的なものを Lean で形式化し、解いていきます。 -## 問題の内容 +## 概要 [Critical thinking web](https://philosophy.hku.hk/think/logic/knights.php) から問題を引用します。まずは自然言語で問題文を述べましょう。 @@ -11,11 +11,11 @@ あなたはゾーイとメルという２人の島民に出会いました。 ゾーイは「メルは悪党です」と言いました。 -メルは「ゾーイも私も悪党ではない」と言いました。 +メルは「ゾーイも私も悪党ではありません」と言いました。 さて、ゾーイとメルはそれぞれ騎士か悪党のどちらでしょうか？ ``` -## 問題の形式化 +## 形式化 さっそく形式化を行っていきます。まず、ある島があってそこには騎士と悪党しか住んでいないというところですが、これは `Islander` という型に `knight` と `knave` という部分集合が存在するというように形式化できます。そのうえで、島民が騎士か悪党のどちらかであることを `axiom` コマンドで仮定しましょう。 @@ -104,7 +104,7 @@ class inductive Solution (p : Islander) : Type where /- `class inductive` というものをあまり見たことがないかもしれませんが、これは普通の型クラスと異なりコンストラクタが複数ある型クラスを定義することができます。この `Solution` の場合、`p : Islander` に対してインスタンスを作成するときに、インスタンスが `isKnight` から来るのか `isKnave` から来るのか明示しなければなりません。そしてそのために、それぞれ `p` が騎士であるか悪党であるかのどちらかの証明が引数に要求されることになります。 -## 問題文 +## 問題 以上の準備の下で、問題は次のように表現できます。以下の `sorry` の部分を埋めてください。 -/