From d5da1b8929eac2ded59b9470bc7964c98014b603 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Tue, 27 Aug 2024 21:52:13 +0900 Subject: [PATCH] =?UTF-8?q?=E6=BC=94=E7=BF=92=E5=95=8F=E9=A1=8C=E3=81=AB?= =?UTF-8?q?=20autoImplicit=20false=20=E3=82=92=E8=BF=BD=E5=8A=A0=E3=81=99?= =?UTF-8?q?=E3=82=8B=20Fixes=20#706?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Exercise/BarberParadox.lean | 1 + Examples/Exercise/CantorTheorem.lean | 1 + Examples/Exercise/DeMorganAndEm.lean | 1 + Examples/Exercise/ImpDefValidness.lean | 7 +------ Examples/Exercise/KnightAndKnave.lean | 1 + Examples/Solution/BarberParadox.lean | 1 + Examples/Solution/CantorTheorem.lean | 1 + Examples/Solution/DeMorganAndEm.lean | 1 + Examples/Solution/ImpDefValidness.lean | 1 + Examples/Solution/KnightAndKnave.lean | 1 + 10 files changed, 10 insertions(+), 6 deletions(-) diff --git a/Examples/Exercise/BarberParadox.lean b/Examples/Exercise/BarberParadox.lean index 0dd1428a..e2997902 100644 --- 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 index 6d568d80..a4ae7522 100644 --- 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 index 019fe291..9629112a 100644 --- 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 index a4235b96..8bc1b362 100644 --- 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 index 5fe56795..9c4a6c25 100644 --- 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 index 7ee73ea9..f129522b 100644 --- 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 index b208d956..6553fdec 100644 --- 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 index df39b7c4..897a5788 100644 --- 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 index 437be531..abd803f8 100644 --- 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 index 60bdd615..b84c13b3 100644 --- a/Examples/Solution/KnightAndKnave.lean +++ b/Examples/Solution/KnightAndKnave.lean @@ -22,6 +22,7 @@ ここでは後で便利なように `simp` 補題も示しておくことにします。 -/ import Lean --# +set_option autoImplicit false --# /-- その島の住民を表す型 -/ opaque Islander : Type