Merge pull request #707 from lean-ja/Seasawher/issue706

演習問題に autoImplicit false を追加する
lean-ja · Aug 27, 2024 · efb4b2c · efb4b2c
2 parents 3004dcf + d5da1b8
commit efb4b2c
Show file tree

Hide file tree

Showing 10 changed files with 10 additions and 6 deletions.
diff --git a/Examples/Exercise/BarberParadox.lean b/Examples/Exercise/BarberParadox.lean
@@ -18,6 +18,7 @@
 この内容を Lean で表現してみましょう。演習問題として、`sorry` の部分を埋めてみてください。
 -/
 namespace Barber
+set_option autoImplicit false --#
 
 /-- 全体集合となる人々の集合 -/
 opaque Person : Type

diff --git a/Examples/Exercise/CantorTheorem.lean b/Examples/Exercise/CantorTheorem.lean
@@ -28,6 +28,7 @@ Lean の型 `T : Type` は直観的には「項の集まり」を意味するの
 
 そこで全体集合 `α : Type` を固定して、その中に含まれる集まりだけを考えることにします。
 -/
+set_option autoImplicit false --#
 
 /-- α を全体集合として、その部分集合の全体。
 α の部分集合と α 上の述語を同一視していることに注意。 -/

diff --git a/Examples/Exercise/DeMorganAndEm.lean b/Examples/Exercise/DeMorganAndEm.lean
@@ -13,6 +13,7 @@
 
 `simp` や `rw` でライブラリの命題を引用する方法でも示すことができますし、使わずに自力で示すこともできます。どちらでも構いませんが、Lean に慣れていない人は自力で示すのに挑戦してみてください。
 -/
+set_option autoImplicit false --#
 
 theorem not_or_mp (P Q : Prop) : ¬ (P ∨ Q) → ¬ P ∧ ¬ Q := by
   sorry

diff --git a/Examples/Exercise/ImpDefValidness.lean b/Examples/Exercise/ImpDefValidness.lean
@@ -20,6 +20,7 @@
 
 まずは、含意に相当する「何か」を定義しましょう。それは、命題から命題への2引数関数になっているはずです。ここではその何かに `Imp` という名前をつけ、`→ᵥ` という記号で表すことにします。
 -/
+set_option autoImplicit false --#
 -- 含意が満たすべき性質を満たす「何か」
 opaque Imp (P Q : Prop) : Prop
 
@@ -61,9 +62,3 @@ variable {P Q : Prop}
 /-- 前件(antecedent)が偽であるとき、「P ならば Q」は真 -/
 theorem imp_of_ant_false (nP : ¬ P) : P →ᵥ Q := by
   sorry
-
-/-
-```admonish tip title="ヒント"
-どの要請が絶対に必要なのか考えてみるといいかもしれません。示したい命題 `imp_of_ant_false` は、`→ᵥ` の部分を同値関係 `↔` に読み替えるとともはや正しくありません。つまり、同値関係の話に読み替えたら成り立たなくなるような要請を、どれか一つ必ず使用するはずですね。
-```
--/
diff --git a/Examples/Exercise/KnightAndKnave.lean b/Examples/Exercise/KnightAndKnave.lean
@@ -22,6 +22,7 @@
 ここでは後で便利なように `simp` 補題も示しておくことにします。
 -/
 import Lean --#
+set_option autoImplicit false --#
 
 /-- その島の住民を表す型 -/
 opaque Islander : Type

diff --git a/Examples/Solution/BarberParadox.lean b/Examples/Solution/BarberParadox.lean
@@ -18,6 +18,7 @@
 この内容を Lean で表現してみましょう。演習問題として、`sorry` の部分を埋めてみてください。
 -/
 namespace Barber
+set_option autoImplicit false --#
 
 /-- 全体集合となる人々の集合 -/
 opaque Person : Type

diff --git a/Examples/Solution/CantorTheorem.lean b/Examples/Solution/CantorTheorem.lean
@@ -28,6 +28,7 @@ Lean の型 `T : Type` は直観的には「項の集まり」を意味するの
 
 そこで全体集合 `α : Type` を固定して、その中に含まれる集まりだけを考えることにします。
 -/
+set_option autoImplicit false --#
 
 /-- α を全体集合として、その部分集合の全体。
 α の部分集合と α 上の述語を同一視していることに注意。 -/

diff --git a/Examples/Solution/DeMorganAndEm.lean b/Examples/Solution/DeMorganAndEm.lean
@@ -13,6 +13,7 @@
 
 `simp` や `rw` でライブラリの命題を引用する方法でも示すことができますし、使わずに自力で示すこともできます。どちらでも構いませんが、Lean に慣れていない人は自力で示すのに挑戦してみてください。
 -/
+set_option autoImplicit false --#
 
 theorem not_or_mp (P Q : Prop) : ¬ (P ∨ Q) → ¬ P ∧ ¬ Q := by
   -- sorry

diff --git a/Examples/Solution/ImpDefValidness.lean b/Examples/Solution/ImpDefValidness.lean
@@ -20,6 +20,7 @@
 
 まずは、含意に相当する「何か」を定義しましょう。それは、命題から命題への2引数関数になっているはずです。ここではその何かに `Imp` という名前をつけ、`→ᵥ` という記号で表すことにします。
 -/
+set_option autoImplicit false --#
 -- 含意が満たすべき性質を満たす「何か」
 opaque Imp (P Q : Prop) : Prop
 

diff --git a/Examples/Solution/KnightAndKnave.lean b/Examples/Solution/KnightAndKnave.lean
@@ -22,6 +22,7 @@
 ここでは後で便利なように `simp` 補題も示しておくことにします。
 -/
 import Lean --#
+set_option autoImplicit false --#
 
 /-- その島の住民を表す型 -/
 opaque Islander : Type
-Original file line number
+Diff line change
@@ Expand Up / @@ -13,6 +13,7 @@ @@
     `simp` や `rw` でライブラリの命題を引用する方法でも示すことができますし、使わずに自力で示すこともできます。どちらでも構いませんが、Lean に慣れていない人は自力で示すのに挑戦してみてください。
     -/
+    set_option autoImplicit false --#
     theorem not_or_mp (P Q : Prop) : ¬ (P ∨ Q) → ¬ P ∧ ¬ Q := by
       sorry
@@ Expand Down @@