騎士と悪党のパズルの説明文まわりの微修正

lean-ja · Aug 18, 2024 · 0e90023 · 0e90023
1 parent 3ce7e0a
commit 0e90023
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 10 deletions.
diff --git 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
@@ -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` の部分を埋めてください。
 -/