From 20712f3ac5d1d088adde87e269cd447493f72075 Mon Sep 17 00:00:00 2001 From: Kitamado <47292598+Seasawher@users.noreply.github.com> Date: Fri, 22 May 2026 20:59:40 +0900 Subject: [PATCH 1/8] =?UTF-8?q?DecidableEq=20=E3=81=A8=20BEq=20=E3=81=AE?= =?UTF-8?q?=E9=81=95=E3=81=84=E3=82=92=E8=AA=AC=E6=98=8E=E3=81=99=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/TypeClass/Decidable.lean | 89 ++++++++++++++++++++++++++ 1 file changed, 89 insertions(+) diff --git a/LeanByExample/TypeClass/Decidable.lean b/LeanByExample/TypeClass/Decidable.lean index b367b05a..dfab8822 100644 --- a/LeanByExample/TypeClass/Decidable.lean +++ b/LeanByExample/TypeClass/Decidable.lean @@ -65,6 +65,95 @@ class inductive Decidable (p : Prop) where | isTrue (h : p) : Decidable p end Hidden --# +/- ## DecidableEq と BEq + +`DecidableEq α` は、`α` の任意の2つの値 `a b : α` について、命題 `a = b` が決定可能であることを表します。 +一方で `BEq α` は、`a == b` という `Bool` 値の比較を提供する型クラスです。 +公式リファレンスの説明どおり、`BEq` はそれだけでは `==` が反射的であることも、命題としての等号 `=` と一致することも要求しません。 + +参照: +* [Boolean Equality Tests](https://lean-lang.org/doc/reference/latest/Type-Classes/Basic-Classes/#boolean-equality-tests) +* [Floating-Point Numbers](https://lean-lang.org/doc/reference/latest/Basic-Types/Floating-Point-Numbers/) +-/ + +#check (DecidableEq : Type → Type) +#check (BEq : Type → Type) + +/- `==` は `BEq` のインスタンスによって使えるようになります。-/ + +#check ((· == ·) : Nat → Nat → Bool) + +namespace DecidableEqVsBEq --# + +/- `BEq` は、命題としての等号と一致しない比較にも使えます。たとえば「同じ `id` なら同じアカウントだとみなす」という比較を定義できます。-/ + +structure Account where + id : Nat + name : String + deriving DecidableEq, Repr + +instance : BEq Account where + beq a b := a.id == b.id + +def alice : Account := { id := 1, name := "Alice" } +def alicia : Account := { id := 1, name := "Alicia" } + +-- id が同じなので `BEq` では等しい +#guard (alice == alicia) + +-- しかし命題としての等号では等しくない +example : alice ≠ alicia := by decide + +/- `==` と `=` が一致することを使いたいときは、`LawfulBEq` が必要です。上の `Account` の `BEq` は `alice == alicia` が真なのに `alice ≠ alicia` なので、`LawfulBEq` ではありません。-/ + +/-⋆-//-- +error: failed to synthesize + LawfulBEq Account + +Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. +-/ +#guard_msgs in --# +#synth LawfulBEq Account + +/- 構造体のすべてのフィールドを比較する通常の等号でよければ、`BEq` と `LawfulBEq` は `deriving` できます。-/ + +structure Point where + x : Nat + y : Nat + deriving DecidableEq, BEq, ReflBEq, LawfulBEq + +#synth BEq Point +#synth LawfulBEq Point + +#guard ({ x := 2, y := 3 } : Point) == { x := 2, y := 3 } + +example : ({ x := 2, y := 3 } : Point) = { x := 2, y := 3 } := by decide + +end DecidableEqVsBEq --# + +/- `Float` は `DecidableEq` と `BEq` の違いが重要になる例です。Lean の `Float` は IEEE 754 の浮動小数点数に対応しており、公式リファレンスでは、浮動小数点数の等号は Lean の論理内では決定可能ではないと説明されています。-/ + +#check (inferInstance : BEq Float) + +/-⋆-//-- +error: failed to synthesize + DecidableEq Float + +Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. +-/ +#guard_msgs in --# +#synth DecidableEq Float + +/- しかし `Float` には実行時の比較としての `BEq` はあります。たとえば `0.0 / 0.0` は `NaN` になり、IEEE 754 の比較では `NaN` は自分自身と比較しても等しくありません。-/ + +#guard ((0.0 : Float) / 0.0).isNaN + +-- 自分自身と比較しても false になる +#guard !(((0.0 : Float) / 0.0) == ((0.0 : Float) / 0.0)) + +-- 通常の数値の比較は true になる +#guard ((1.0 : Float) == 1.0) + /- ## 排中律と決定可能性 命題 `P : Prop` が決定可能というのは、実際のところ「`P` の証明または `¬ P` の証明を持っている」ということを意味します。したがって、`P` の証明または `¬ P` の証明のいずれかが手に入っているのであれば、そこから `Decidable P` のインスタンスを構築することができ、`P` は決定可能であるといえます。 From 3b0c64632327e9d595a5fbacf1846db6cb356631 Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Wed, 27 May 2026 02:10:22 +0900 Subject: [PATCH 2/8] =?UTF-8?q?Decidable.lean=20=E3=81=AF=E5=A4=89?= =?UTF-8?q?=E6=9B=B4=E3=81=97=E3=81=AA=E3=81=84?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/TypeClass/Decidable.lean | 89 -------------------------- 1 file changed, 89 deletions(-) diff --git a/LeanByExample/TypeClass/Decidable.lean b/LeanByExample/TypeClass/Decidable.lean index dfab8822..b367b05a 100644 --- a/LeanByExample/TypeClass/Decidable.lean +++ b/LeanByExample/TypeClass/Decidable.lean @@ -65,95 +65,6 @@ class inductive Decidable (p : Prop) where | isTrue (h : p) : Decidable p end Hidden --# -/- ## DecidableEq と BEq - -`DecidableEq α` は、`α` の任意の2つの値 `a b : α` について、命題 `a = b` が決定可能であることを表します。 -一方で `BEq α` は、`a == b` という `Bool` 値の比較を提供する型クラスです。 -公式リファレンスの説明どおり、`BEq` はそれだけでは `==` が反射的であることも、命題としての等号 `=` と一致することも要求しません。 - -参照: -* [Boolean Equality Tests](https://lean-lang.org/doc/reference/latest/Type-Classes/Basic-Classes/#boolean-equality-tests) -* [Floating-Point Numbers](https://lean-lang.org/doc/reference/latest/Basic-Types/Floating-Point-Numbers/) --/ - -#check (DecidableEq : Type → Type) -#check (BEq : Type → Type) - -/- `==` は `BEq` のインスタンスによって使えるようになります。-/ - -#check ((· == ·) : Nat → Nat → Bool) - -namespace DecidableEqVsBEq --# - -/- `BEq` は、命題としての等号と一致しない比較にも使えます。たとえば「同じ `id` なら同じアカウントだとみなす」という比較を定義できます。-/ - -structure Account where - id : Nat - name : String - deriving DecidableEq, Repr - -instance : BEq Account where - beq a b := a.id == b.id - -def alice : Account := { id := 1, name := "Alice" } -def alicia : Account := { id := 1, name := "Alicia" } - --- id が同じなので `BEq` では等しい -#guard (alice == alicia) - --- しかし命題としての等号では等しくない -example : alice ≠ alicia := by decide - -/- `==` と `=` が一致することを使いたいときは、`LawfulBEq` が必要です。上の `Account` の `BEq` は `alice == alicia` が真なのに `alice ≠ alicia` なので、`LawfulBEq` ではありません。-/ - -/-⋆-//-- -error: failed to synthesize - LawfulBEq Account - -Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. --/ -#guard_msgs in --# -#synth LawfulBEq Account - -/- 構造体のすべてのフィールドを比較する通常の等号でよければ、`BEq` と `LawfulBEq` は `deriving` できます。-/ - -structure Point where - x : Nat - y : Nat - deriving DecidableEq, BEq, ReflBEq, LawfulBEq - -#synth BEq Point -#synth LawfulBEq Point - -#guard ({ x := 2, y := 3 } : Point) == { x := 2, y := 3 } - -example : ({ x := 2, y := 3 } : Point) = { x := 2, y := 3 } := by decide - -end DecidableEqVsBEq --# - -/- `Float` は `DecidableEq` と `BEq` の違いが重要になる例です。Lean の `Float` は IEEE 754 の浮動小数点数に対応しており、公式リファレンスでは、浮動小数点数の等号は Lean の論理内では決定可能ではないと説明されています。-/ - -#check (inferInstance : BEq Float) - -/-⋆-//-- -error: failed to synthesize - DecidableEq Float - -Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. --/ -#guard_msgs in --# -#synth DecidableEq Float - -/- しかし `Float` には実行時の比較としての `BEq` はあります。たとえば `0.0 / 0.0` は `NaN` になり、IEEE 754 の比較では `NaN` は自分自身と比較しても等しくありません。-/ - -#guard ((0.0 : Float) / 0.0).isNaN - --- 自分自身と比較しても false になる -#guard !(((0.0 : Float) / 0.0) == ((0.0 : Float) / 0.0)) - --- 通常の数値の比較は true になる -#guard ((1.0 : Float) == 1.0) - /- ## 排中律と決定可能性 命題 `P : Prop` が決定可能というのは、実際のところ「`P` の証明または `¬ P` の証明を持っている」ということを意味します。したがって、`P` の証明または `¬ P` の証明のいずれかが手に入っているのであれば、そこから `Decidable P` のインスタンスを構築することができ、`P` は決定可能であるといえます。 From 388335a76dc8d2a2d5dd3529ab25aeac2133088b Mon Sep 17 00:00:00 2001 From: Codex Date: Wed, 27 May 2026 02:15:35 +0900 Subject: [PATCH 3/8] =?UTF-8?q?BEq=20=E3=81=AE=E8=A7=A3=E8=AA=AC=E3=83=9A?= =?UTF-8?q?=E3=83=BC=E3=82=B8=E3=82=92=E8=BF=BD=E5=8A=A0?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Type/Bool.lean | 2 +- LeanByExample/TypeClass/BEq.lean | 130 +++++++++++++++++++++++++++++++ booksrc/SUMMARY.md | 1 + 3 files changed, 132 insertions(+), 1 deletion(-) create mode 100644 LeanByExample/TypeClass/BEq.lean diff --git a/LeanByExample/Type/Bool.lean b/LeanByExample/Type/Bool.lean index fd66ffc1..470178cd 100644 --- a/LeanByExample/Type/Bool.lean +++ b/LeanByExample/Type/Bool.lean @@ -6,7 +6,7 @@ #check (true : Bool) #check (false : Bool) -/- `Bool` の値を得るためには、たとえば `==` を用いて値を比較します。-/ +/- `Bool` の値を得るためには、たとえば [`BEq`](#{root}/TypeClass/BEq.md) のインスタンスがある型の値を `==` で比較します。-/ inductive Foo where | bar diff --git a/LeanByExample/TypeClass/BEq.lean b/LeanByExample/TypeClass/BEq.lean new file mode 100644 index 00000000..2397fcb8 --- /dev/null +++ b/LeanByExample/TypeClass/BEq.lean @@ -0,0 +1,130 @@ +/- # BEq + +`BEq` は、`==` と `!=` による `Bool` 値の比較を提供する型クラスです。 +たとえば `Nat` には `BEq` のインスタンスがあるので、2つの自然数を `==` で比較することができます。 +-/ + +#check (BEq : Type → Type) + +#check ((· == ·) : Nat → Nat → Bool) + +#guard ((2 : Nat) == 2) +#guard !((2 : Nat) == 3) + +#guard ((2 : Nat) != 3) + +/- ## 定義 + +`BEq` 型クラスは、比較関数 `beq : α → α → Bool` を持ちます。 +`a == b` という記法は、この `beq a b` を使います。 +-/ + +namespace Hidden --# + +class BEq.{u} (α : Type u) where + /-- `α` 型の2つの値が等しいとみなせるかどうかを `Bool` 値で返す。 -/ + beq : α → α → Bool + +end Hidden --# + +/- ## インスタンスを定義する + +自分で定義した型に対して `BEq` インスタンスを定義すると、その型の値を `==` で比較できるようになります。 + +次の例では、アカウントを `id` だけで比較することにします。 +-/ + +structure Account where + id : Nat + name : String + deriving DecidableEq, Repr + +instance : BEq Account where + beq a b := a.id == b.id + +def alice : Account := { id := 1, name := "Alice" } + +def alicia : Account := { id := 1, name := "Alicia" } + +def bob : Account := { id := 2, name := "Bob" } + +-- id が同じなので `BEq` では等しい +#guard (alice == alicia) + +-- id が異なるので `BEq` では等しくない +#guard !(alice == bob) + +-- しかし命題としての等号では等しくない +example : alice ≠ alicia := by decide + +/- ## DecidableEq との違い + +[`DecidableEq`](#{root}/TypeClass/Decidable.md) は、`a = b` という命題が決定可能であることを表します。 +一方で `BEq` は、`a == b` という `Bool` 値の比較を提供するだけです。 + +したがって `BEq` は、それだけでは `==` が反射的であることも、命題としての等号 `=` と一致することも要求しません。 +上の `Account` の例では、`alice == alicia` は `true` ですが、`alice = alicia` は成り立ちません。 +-/ + +#check (DecidableEq : Type → Type) + +/- ## LawfulBEq + +`==` と `=` が一致することを使いたいときは、`LawfulBEq` が必要です。 +上の `Account` の `BEq` は `alice == alicia` が真なのに `alice ≠ alicia` なので、`LawfulBEq` ではありません。 +-/ + +/-⋆-//-- +error: failed to synthesize + LawfulBEq Account + +Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. +-/ +#guard_msgs in --# +#synth LawfulBEq Account + +/- 構造体のすべてのフィールドを比較する通常の等号でよければ、`BEq` と `LawfulBEq` は `deriving` できます。-/ + +structure Point where + x : Nat + y : Nat + deriving DecidableEq, BEq, ReflBEq, LawfulBEq + +#synth BEq Point + +#synth LawfulBEq Point + +#guard ({ x := 2, y := 3 } : Point) == { x := 2, y := 3 } + +example : ({ x := 2, y := 3 } : Point) = { x := 2, y := 3 } := by decide + +/- ## Float の例 + +`Float` は `DecidableEq` と `BEq` の違いが重要になる例です。 +Lean の `Float` は IEEE 754 の浮動小数点数に対応しており、公式リファレンスでは、浮動小数点数の等号は Lean の論理内では決定可能ではないと説明されています。 + +参照: +* [Boolean Equality Tests](https://lean-lang.org/doc/reference/latest/Type-Classes/Basic-Classes/#boolean-equality-tests) +* [Floating-Point Numbers](https://lean-lang.org/doc/reference/latest/Basic-Types/Floating-Point-Numbers/) +-/ + +#check (inferInstance : BEq Float) + +/-⋆-//-- +error: failed to synthesize + DecidableEq Float + +Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. +-/ +#guard_msgs in --# +#synth DecidableEq Float + +/- しかし `Float` には実行時の比較としての `BEq` はあります。たとえば `0.0 / 0.0` は `NaN` になり、IEEE 754 の比較では `NaN` は自分自身と比較しても等しくありません。-/ + +#guard ((0.0 : Float) / 0.0).isNaN + +-- 自分自身と比較しても false になる +#guard !(((0.0 : Float) / 0.0) == ((0.0 : Float) / 0.0)) + +-- 通常の数値の比較は true になる +#guard ((1.0 : Float) == 1.0) diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md index 1fa5cab9..4dee0966 100644 --- a/booksrc/SUMMARY.md +++ b/booksrc/SUMMARY.md @@ -119,6 +119,7 @@ - [Add: 閉じた + 演算用の記法クラス](./TypeClass/Add.md) - [Alternative: 回復可能な失敗](./TypeClass/Alternative.md) - [Applicative: アプリカティブ関手](./TypeClass/Applicative.md) + - [BEq: Bool値の比較](./TypeClass/BEq.md) - [Coe: 型強制](./TypeClass/Coe.md) - [CoeDep: 依存型強制](./TypeClass/CoeDep.md) - [CoeFun: 関数型への強制](./TypeClass/CoeFun.md) From bf2e8a23725051f865492cdc4c01d95b4a60e6de Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Wed, 27 May 2026 02:39:11 +0900 Subject: [PATCH 4/8] =?UTF-8?q?=E6=96=87=E7=AB=A0=E6=A0=A1=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/TypeClass/BEq.lean | 133 +++++-------------------------- 1 file changed, 22 insertions(+), 111 deletions(-) diff --git a/LeanByExample/TypeClass/BEq.lean b/LeanByExample/TypeClass/BEq.lean index 2397fcb8..a9f05f6d 100644 --- a/LeanByExample/TypeClass/BEq.lean +++ b/LeanByExample/TypeClass/BEq.lean @@ -4,127 +4,38 @@ たとえば `Nat` には `BEq` のインスタンスがあるので、2つの自然数を `==` で比較することができます。 -/ -#check (BEq : Type → Type) +#guard 2 == 2 +#guard !(2 == 3) +#guard (2 != 42) -#check ((· == ·) : Nat → Nat → Bool) +/- ## DecidableEq との使い分け -#guard ((2 : Nat) == 2) -#guard !((2 : Nat) == 3) - -#guard ((2 : Nat) != 3) - -/- ## 定義 - -`BEq` 型クラスは、比較関数 `beq : α → α → Bool` を持ちます。 -`a == b` という記法は、この `beq a b` を使います。 +単に `Bool` 値の比較をしたいだけであれば、`DecidableEq` のインスタンスでも可能です。しかも `DecidableEq` なら単に `Bool` 値になるだけでなく、`∀ x : α, x = x` といった「等号が満たすべきルール」もついてくるので、`DecidableEq` が使える場合はそちらを使うべきでしょう。 -/ -namespace Hidden --# - -class BEq.{u} (α : Type u) where - /-- `α` 型の2つの値が等しいとみなせるかどうかを `Bool` 値で返す。 -/ - beq : α → α → Bool - -end Hidden --# - -/- ## インスタンスを定義する +-- BEq は単なる関数なのでルールは付属していないが、 +-- DecidableEq は違う +example {α : Type} [DecidableEq α] (x : α) : decide (x = x) = true := by + simp -自分で定義した型に対して `BEq` インスタンスを定義すると、その型の値を `==` で比較できるようになります。 +/- +敢えて `BEq` を使うべきケースは、ルールを満たすような等号比較ができない場合です。典型的なのは [`Float`](#{root}/Type/Float.md) です。 -次の例では、アカウントを `id` だけで比較することにします。 +`Float` には `NaN` という値があります。これは「数値ではない」ことを表す特別な値で、`isNaN` という関数で判定できます。 -/ -structure Account where - id : Nat - name : String - deriving DecidableEq, Repr - -instance : BEq Account where - beq a b := a.id == b.id - -def alice : Account := { id := 1, name := "Alice" } - -def alicia : Account := { id := 1, name := "Alicia" } - -def bob : Account := { id := 2, name := "Bob" } - --- id が同じなので `BEq` では等しい -#guard (alice == alicia) - --- id が異なるので `BEq` では等しくない -#guard !(alice == bob) - --- しかし命題としての等号では等しくない -example : alice ≠ alicia := by decide - -/- ## DecidableEq との違い - -[`DecidableEq`](#{root}/TypeClass/Decidable.md) は、`a = b` という命題が決定可能であることを表します。 -一方で `BEq` は、`a == b` という `Bool` 値の比較を提供するだけです。 - -したがって `BEq` は、それだけでは `==` が反射的であることも、命題としての等号 `=` と一致することも要求しません。 -上の `Account` の例では、`alice == alicia` は `true` ですが、`alice = alicia` は成り立ちません。 --/ - -#check (DecidableEq : Type → Type) - -/- ## LawfulBEq - -`==` と `=` が一致することを使いたいときは、`LawfulBEq` が必要です。 -上の `Account` の `BEq` は `alice == alicia` が真なのに `alice ≠ alicia` なので、`LawfulBEq` ではありません。 --/ +-- 0.0 / 0.0 は NaN +#guard (0.0 / 0.0).isNaN -/-⋆-//-- -error: failed to synthesize - LawfulBEq Account - -Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. --/ -#guard_msgs in --# -#synth LawfulBEq Account - -/- 構造体のすべてのフィールドを比較する通常の等号でよければ、`BEq` と `LawfulBEq` は `deriving` できます。-/ - -structure Point where - x : Nat - y : Nat - deriving DecidableEq, BEq, ReflBEq, LawfulBEq - -#synth BEq Point - -#synth LawfulBEq Point - -#guard ({ x := 2, y := 3 } : Point) == { x := 2, y := 3 } - -example : ({ x := 2, y := 3 } : Point) = { x := 2, y := 3 } := by decide - -/- ## Float の例 - -`Float` は `DecidableEq` と `BEq` の違いが重要になる例です。 -Lean の `Float` は IEEE 754 の浮動小数点数に対応しており、公式リファレンスでは、浮動小数点数の等号は Lean の論理内では決定可能ではないと説明されています。 - -参照: -* [Boolean Equality Tests](https://lean-lang.org/doc/reference/latest/Type-Classes/Basic-Classes/#boolean-equality-tests) -* [Floating-Point Numbers](https://lean-lang.org/doc/reference/latest/Basic-Types/Floating-Point-Numbers/) --/ - -#check (inferInstance : BEq Float) - -/-⋆-//-- -error: failed to synthesize - DecidableEq Float - -Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. --/ -#guard_msgs in --# -#synth DecidableEq Float - -/- しかし `Float` には実行時の比較としての `BEq` はあります。たとえば `0.0 / 0.0` は `NaN` になり、IEEE 754 の比較では `NaN` は自分自身と比較しても等しくありません。-/ - -#guard ((0.0 : Float) / 0.0).isNaN +/- NaN は「自分自身と比較しても等しくない」という特殊な仕様があります。 -/ -- 自分自身と比較しても false になる -#guard !(((0.0 : Float) / 0.0) == ((0.0 : Float) / 0.0)) +#guard !((0.0 / 0.0) == (0.0 / 0.0)) -- 通常の数値の比較は true になる -#guard ((1.0 : Float) == 1.0) +#guard 3.2 == 3.2 +#guard 1.45 == 1.45 + +/- そのため `Float` には `DecidableEq` のインスタンスがありません。 -/ + +#check_failure (by infer_instance : DecidableEq Float) From 789e59278f0e2905bcca8afc51af35b4ef1df7e9 Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Wed, 27 May 2026 02:39:54 +0900 Subject: [PATCH 5/8] =?UTF-8?q?Bool.lean=20=E3=81=B8=E3=81=AE=E5=A4=89?= =?UTF-8?q?=E6=9B=B4=E3=82=92=E5=B7=AE=E3=81=97=E6=88=BB=E3=81=99?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Type/Bool.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/LeanByExample/Type/Bool.lean b/LeanByExample/Type/Bool.lean index 470178cd..4854c7e2 100644 --- a/LeanByExample/Type/Bool.lean +++ b/LeanByExample/Type/Bool.lean @@ -6,8 +6,6 @@ #check (true : Bool) #check (false : Bool) -/- `Bool` の値を得るためには、たとえば [`BEq`](#{root}/TypeClass/BEq.md) のインスタンスがある型の値を `==` で比較します。-/ - inductive Foo where | bar | baz From 195be1907fcef45eaf9b9b8b0c4a5713d66d2b19 Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Wed, 27 May 2026 02:41:00 +0900 Subject: [PATCH 6/8] =?UTF-8?q?=E5=B7=AE=E3=81=97=E6=88=BB=E3=81=97?= =?UTF-8?q?=E3=81=AE=E5=B7=AE=E3=81=97=E6=88=BB=E3=81=97?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Type/Bool.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/LeanByExample/Type/Bool.lean b/LeanByExample/Type/Bool.lean index 4854c7e2..470178cd 100644 --- a/LeanByExample/Type/Bool.lean +++ b/LeanByExample/Type/Bool.lean @@ -6,6 +6,8 @@ #check (true : Bool) #check (false : Bool) +/- `Bool` の値を得るためには、たとえば [`BEq`](#{root}/TypeClass/BEq.md) のインスタンスがある型の値を `==` で比較します。-/ + inductive Foo where | bar | baz From 4d091843bc16a12947fb24fcedbc1872bff9165b Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Wed, 27 May 2026 02:48:11 +0900 Subject: [PATCH 7/8] =?UTF-8?q?=E6=A0=A1=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/TypeClass/BEq.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/LeanByExample/TypeClass/BEq.lean b/LeanByExample/TypeClass/BEq.lean index a9f05f6d..e5832e8a 100644 --- a/LeanByExample/TypeClass/BEq.lean +++ b/LeanByExample/TypeClass/BEq.lean @@ -10,7 +10,7 @@ /- ## DecidableEq との使い分け -単に `Bool` 値の比較をしたいだけであれば、`DecidableEq` のインスタンスでも可能です。しかも `DecidableEq` なら単に `Bool` 値になるだけでなく、`∀ x : α, x = x` といった「等号が満たすべきルール」もついてくるので、`DecidableEq` が使える場合はそちらを使うべきでしょう。 +単に `Bool` 値の比較をしたいだけであれば、`DecidableEq` のインスタンスでも可能です。しかも `DecidableEq` なら単に `Bool` 値の比較ができるだけでなく、`∀ x : α, x = x` といった「等号が満たすべきルール」もついてくるので、証明が必要でかつ `DecidableEq` が使える場合はそちらを使うべきでしょう。 -/ -- BEq は単なる関数なのでルールは付属していないが、 @@ -18,8 +18,7 @@ example {α : Type} [DecidableEq α] (x : α) : decide (x = x) = true := by simp -/- -敢えて `BEq` を使うべきケースは、ルールを満たすような等号比較ができない場合です。典型的なのは [`Float`](#{root}/Type/Float.md) です。 +/- 敢えて `BEq` を使うべきケースもあります。たとえばルールを満たすような等号比較ができない場合です。典型的なのは [`Float`](#{root}/Type/Float.md) です。 `Float` には `NaN` という値があります。これは「数値ではない」ことを表す特別な値で、`isNaN` という関数で判定できます。 -/ @@ -39,3 +38,4 @@ example {α : Type} [DecidableEq α] (x : α) : decide (x = x) = true := by /- そのため `Float` には `DecidableEq` のインスタンスがありません。 -/ #check_failure (by infer_instance : DecidableEq Float) + From 32ddc1374170c106e861532ca70eefd38207d008 Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Wed, 27 May 2026 03:09:28 +0900 Subject: [PATCH 8/8] =?UTF-8?q?=E6=A0=A1=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/TypeClass/BEq.lean | 27 +++++++++++++++++++-------- 1 file changed, 19 insertions(+), 8 deletions(-) diff --git a/LeanByExample/TypeClass/BEq.lean b/LeanByExample/TypeClass/BEq.lean index e5832e8a..372f8a8a 100644 --- a/LeanByExample/TypeClass/BEq.lean +++ b/LeanByExample/TypeClass/BEq.lean @@ -10,15 +10,21 @@ /- ## DecidableEq との使い分け -単に `Bool` 値の比較をしたいだけであれば、`DecidableEq` のインスタンスでも可能です。しかも `DecidableEq` なら単に `Bool` 値の比較ができるだけでなく、`∀ x : α, x = x` といった「等号が満たすべきルール」もついてくるので、証明が必要でかつ `DecidableEq` が使える場合はそちらを使うべきでしょう。 +単に `Bool` 値の比較をしたいだけであれば、`DecidableEq` のインスタンスでも可能です。しかも `DecidableEq` なら単に `Bool` 値の比較ができるだけでなく、`∀ x : α, x = x` といった「等号が満たすべきルール」もついてくるので、証明に使いたくてかつ `DecidableEq` が使える場合はそちらを使うべきでしょう。 -/ --- BEq は単なる関数なのでルールは付属していないが、 --- DecidableEq は違う -example {α : Type} [DecidableEq α] (x : α) : decide (x = x) = true := by +-- BEq は単なる関数なのでルールは付属しておらず、 +-- x == x などを証明するには LawfulBEq が必要 +example {α : Type} [BEq α] [LawfulBEq α] (x : α) : x == x := by simp -/- 敢えて `BEq` を使うべきケースもあります。たとえばルールを満たすような等号比較ができない場合です。典型的なのは [`Float`](#{root}/Type/Float.md) です。 +-- DecidableEq を仮定すると自動的に LawfulBEq のインスタンスが生成される +example {α : Type} [DecidableEq α] (x : α) : x == x := by + let _ : LawfulBEq α := by infer_instance + simp + +/- +敢えて `BEq` を使うべきケースもあります。典型的なのは [`Float`](#{root}/Type/Float.md) です。 `Float` には `NaN` という値があります。これは「数値ではない」ことを表す特別な値で、`isNaN` という関数で判定できます。 -/ @@ -26,7 +32,7 @@ example {α : Type} [DecidableEq α] (x : α) : decide (x = x) = true := by -- 0.0 / 0.0 は NaN #guard (0.0 / 0.0).isNaN -/- NaN は「自分自身と比較しても等しくない」という特殊な仕様があります。 -/ +/- `NaN` は「自分自身と比較しても等しくない」という特殊な仕様があります。 -/ -- 自分自身と比較しても false になる #guard !((0.0 / 0.0) == (0.0 / 0.0)) @@ -35,7 +41,12 @@ example {α : Type} [DecidableEq α] (x : α) : decide (x = x) = true := by #guard 3.2 == 3.2 #guard 1.45 == 1.45 -/- そのため `Float` には `DecidableEq` のインスタンスがありません。 -/ +/- +一方で命題としては `Float` に対しても `∀ x, x = x` が成り立っています。 +-/ + +example (x : Float) : x = x := by rfl -#check_failure (by infer_instance : DecidableEq Float) +/- この「命題としては `∀ x, x = x` が成立する」ことと、「実行時の比較 `x == x` は `false` になる場合がある」ことの２つの要件を両立することは不可能です。したがって、`DecidableEq` のインスタンスは `Float` には用意されていません。 -/ +#check_failure (by infer_instance : DecidableEq Float)