lean-ja · Seasawher · Oct 5, 2024 · Oct 5, 2024
@@ -75,7 +75,7 @@ section hoge
   #check a
 end hoge
 
-/-! セクションは入れ子にすることもできます。-/
+/- セクションは入れ子にすることもできます。-/
 
 section parent
   variable (a : Type)

@@ -37,7 +37,7 @@
 -- 命題
 #check True
 
-/-! ## 型の型
+/- ## 型の型
 「すべての」項には型があるので、型も型を持ちます。
 -/
 -- 宇宙変数を宣言する
@@ -59,7 +59,7 @@ universe u
 -- この調子で限りなく続く
 #check (Type u : Type (u + 1))
 
-/-! ## 命題と証明
+/- ## 命題と証明
 Lean では命題やその証明にも型があります。命題の型は `Prop` で、命題の項が証明になっています。逆に言えば、Lean ではある命題 `P : Prop` を証明するということは、`P` という型を持つ項 `proof : P` を構成することと同じです。
 -/
 
@@ -71,15 +71,15 @@ theorem two_eq_add_one : 2 = 1 + 1 := by rfl
 -- 証明の型が命題になっている
 #check (two_eq_add_one : 2 = 1 + 1)
 
-/-! ## 型としての True/False
+/- ## 型としての True/False
 `True` は型としては一点集合であり、
 `False` は型としては空集合です。
 -/
 
 -- `trivial : True` は `True` 型を持つ項
 #check trivial
 
-/-! ## 関数としての証明
+/- ## 関数としての証明
 命題 `P → Q` の証明は、`P → Q` という型を持つ項です。
 つまり、`P` の証明 `h : P` に対して `Q` の証明を返す関数です。
 -/

@@ -51,7 +51,7 @@ failed to be synthesized, this instance instructs Lean on how to display the res
 
 /- 一般に、[`Repr`](../TypeClass/Repr.md) や [`ToString`](../TypeClass/ToString.md) のインスタンスでないような型の項は `#eval` に渡すことができません。-/
 
-/-! ## 例外処理の慣例
+/- ## 例外処理の慣例
 Lean および Mathlib では、「関数ではなく定理に制約を付ける」ことが慣例です。
 関数の定義域を制限するアプローチだと、
 関数を呼び出すたびに、引数が定義域に含まれているか確認する必要が生じて、

@@ -1,4 +1,4 @@
-/-! # \#find
+/- # \#find
 
 `#find` はライブラリ検索を行うコマンドです。
 

@@ -34,7 +34,7 @@ error: cannot evaluate code because 'sorryAx' uses 'sorry' and/or contains error
 #guard_msgs (whitespace := lax) in
 #guard ((α : Type) → ∀ (l : List α), [] ⊆ l : Prop)
 
-/-! しかし、 `1 + 1 = 2` 等も `#check` で確かめてみると型は `Prop` です。にも関わらず `#guard` に渡してもエラーになりません。これは不思議に思えますが、理由は `1 + 1 = 2` が [`Decidable`](../TypeClass/Decidable.md) 型クラスのインスタンスであり、決定可能だからです。-/
+/- しかし、 `1 + 1 = 2` 等も `#check` で確かめてみると型は `Prop` です。にも関わらず `#guard` に渡してもエラーになりません。これは不思議に思えますが、理由は `1 + 1 = 2` が [`Decidable`](../TypeClass/Decidable.md) 型クラスのインスタンスであり、決定可能だからです。-/
 
 -- 型は Prop
 /-- info: 1 + 1 = 2 : Prop -/
@@ -45,7 +45,7 @@ error: cannot evaluate code because 'sorryAx' uses 'sorry' and/or contains error
 -- 1 + 1 = 2 は決定可能
 #synth Decidable (1 + 1 = 2)
 
-/-!
+/-
 `Prop` 型であっても、`Decidable` クラスのインスタンスであれば `Bool` に変換できます。それを自動で行っているので、`Prop` 型の項でも `#guard` に通せるというわけです。
 -/
 

@@ -13,7 +13,7 @@ import Mathlib.Data.Real.Basic -- 実数 --#
 -- 実数として見ても同じ
 #check (1 : ℝ)⁻¹
 
-/-! 逆数をとる関数 `fun x => x⁻¹` の定義域はどうなっているのでしょうか？定義域を一般の型 `α` に拡張してみて、どうなるか見てみましょう。-/
+/- 逆数をとる関数 `fun x => x⁻¹` の定義域はどうなっているのでしょうか？定義域を一般の型 `α` に拡張してみて、どうなるか見てみましょう。-/
 
 variable (α : Type)
 
@@ -24,16 +24,16 @@ Additional diagnostic information may be available using the `set_option diagnos
 -/
 #guard_msgs in #check (_ : α)⁻¹
 
-/-! 一般の型に対して逆数は定義できないので、エラーになってしまいました。エラーメッセージで `α` は `Inv` のインスタンスではないと言われています。この `Inv` が型クラスです。`Inv` のインスタンスであるような型 `T` に対しては、逆数関数 `(·)⁻¹ : T → T` が定義できるというわけです。-/
+/- 一般の型に対して逆数は定義できないので、エラーになってしまいました。エラーメッセージで `α` は `Inv` のインスタンスではないと言われています。この `Inv` が型クラスです。`Inv` のインスタンスであるような型 `T` に対しては、逆数関数 `(·)⁻¹ : T → T` が定義できるというわけです。-/
 
-/-! ## インスタンスとは
+/- ## インスタンスとは
 例えば実数 `ℝ` に対して逆数は定義できるだろうと予想されますが、実際 `ℝ` は `Inv` のインスタンスであることが確認できます。
 -/
 
 /-- info: Real.instInv -/
 #guard_msgs in #synth Inv Real
 
-/-! 自然数 `ℕ` に対しては逆数が定義されていないと予想されますが、実際 `Inv` のインスタンスになっていません。-/
+/- 自然数 `ℕ` に対しては逆数が定義されていないと予想されますが、実際 `Inv` のインスタンスになっていません。-/
 
 -- エラーになってしまう
 /--
@@ -47,7 +47,7 @@ Additional diagnostic information may be available using the `set_option diagnos
 #guard_msgs (drop warning) in --#
 #check_failure (inferInstance : Inv Nat)
 
-/-! 自分で無理やり `ℕ` を `Inv` のインスタンスにしてみると、通るようになります。ここでは逆数関数を常に `1` になる定数関数としてみましょう。-/
+/- 自分で無理やり `ℕ` を `Inv` のインスタンスにしてみると、通るようになります。ここでは逆数関数を常に `1` になる定数関数としてみましょう。-/
 
 instance : Inv Nat := ⟨fun _ => 1⟩
 

@@ -12,7 +12,7 @@ example (hP : P) (hQ : Q) : P ∧ Q := by
   -- 両方に `assumption` を適用する
   all_goals assumption
 
-/-! `all_goals` には、タクティクブロックを渡すこともできます。-/
+/- `all_goals` には、タクティクブロックを渡すこともできます。-/
 
 example {R : Prop} (hnP : ¬ P) : (P → R) ∧ (P → Q) := by
   constructor

@@ -15,7 +15,7 @@ example (h : P → Q) (hP : P) : Q := by
 
   exact hP
 
-/-! 注意点として、`h : P → Q` は `P` の証明を受け取って `Q` の証明を返す関数でもあるので、上記の例は `apply` を使わずに `exact h hP` で閉じることもできます。-/
+/- 注意点として、`h : P → Q` は `P` の証明を受け取って `Q` の証明を返す関数でもあるので、上記の例は `apply` を使わずに `exact h hP` で閉じることもできます。-/
 
 example (h : P → Q) (hP : P) : Q := by
   exact h hP

@@ -23,7 +23,7 @@ example (hPQ : P → Q) : ¬ Q → ¬ P := by
   -- 証明終わり
   done
 
-/-! タクティクを繰り返すことを指示するタクティク [`repeat`](./Repeat.md) と組み合わせると、「ローカルコンテキストにある仮定を適切に選んで `apply`, `exact` することを繰り返し、ゴールを閉じる」ことができます。
+/- タクティクを繰り返すことを指示するタクティク [`repeat`](./Repeat.md) と組み合わせると、「ローカルコンテキストにある仮定を適切に選んで `apply`, `exact` することを繰り返し、ゴールを閉じる」ことができます。
 -/
 
 example (hPQ : P → Q) (hQR : Q → R) (hQ : P) : R := by

@@ -17,7 +17,7 @@ example (h : P → Q) (hP : P) : Q := by
 
   assumption
 
-/-! 便利な記法以上のものではなく、他のタクティクを利用しても同じことができます。-/
+/- 便利な記法以上のものではなく、他のタクティクを利用しても同じことができます。-/
 
 example (h : P → Q) (hP : P) : Q := by
   -- `apply at` は `replace` と同じように動作する

@@ -15,7 +15,7 @@ example [Group G] [Group H] (f : G →* H) (a b : G) :
   -- `exact MonoidHom.map_mul f a b` を提案してくれる
   apply? says exact MonoidHom.map_mul f a b
 
-/-!
+/-
 ## 補足
 
 `apply?` はあくまで証明を書くときに補助として使うものです。

@@ -1,4 +1,4 @@
-/-! # assumption
+/- # assumption
 
 `assumption` は、現在のゴール `⊢ P` がローカルコンテキストにあるとき、ゴールを閉じます。-/
 

@@ -2,7 +2,7 @@
 
 Lean においては、命題は型で、証明はその項です。命題 `P` の証明を構成するとは項 `h : P` を構成するということです。`by` は、証明の構成をタクティクで行いたいときに使います。-/
 
-/-! 証明項による証明とは、たとえば次のようなものです。 -/
+/- 証明項による証明とは、たとえば次のようなものです。 -/
 
 variable (P Q R : Prop)
 
@@ -11,14 +11,14 @@ variable (P Q R : Prop)
 example (hPQ : P → Q) (hQR : Q → R) : P → R :=
   fun hP ↦ hQR (hPQ hP)
 
-/-! 同じ命題をタクティクを使って示すと、例えば次のようになります。 -/
+/- 同じ命題をタクティクを使って示すと、例えば次のようになります。 -/
 
 -- 同じ命題をタクティクで示した例
 example (hPQ : P → Q) (hQR : Q → R) : P → R := by
   intro hP
   exact hQR (hPQ hP)
 
-/-! ## by?
+/- ## by?
 
 `by` の代わりに `by?` を使うとタクティクモードで構成した証明を直接構成した証明に変換してくれます。`show_term by` としてもほぼ同じ結果が得られます。
 -/

@@ -25,7 +25,7 @@ example : P ∨ Q → (P → R) → (Q → R) → R := by
   case inr hQ =>
     exact hQR hQ
 
-/-! ## with を使う書き方
+/- ## with を使う書き方
 
 `case` を使わずに、`with` を使って次のように書くこともできます
 -/

@@ -30,7 +30,7 @@ example (h : a < b) : a + 1 < b + 1 := by
 
   exact Int.add_lt_add_right h 1
 
-/-! ## 再帰の深さの調節
+/- ## 再帰の深さの調節
 
 `congr` が適用される再帰の深さを引数として渡すことができます。これは、主に単に `congr` とするだけだと「行き過ぎ」になるときに調整する目的で使用されます。-/
 set_option linter.unusedTactic false in --#

@@ -9,7 +9,7 @@ example (hP : P) (hQ : Q) : P := by
 
   exact hP
 
-/-! `exact` は与えられた証明項をそのまま証明として使うタクティクなので、`by exact` だけで証明が終わるときには、`by exact` を消しても証明が通ります。-/
+/- `exact` は与えられた証明項をそのまま証明として使うタクティクなので、`by exact` だけで証明が終わるときには、`by exact` を消しても証明が通ります。-/
 
 example (hP : P) (hQ : Q) : P ∧ Q := by
   exact And.intro hP hQ

@@ -32,7 +32,7 @@ example (_h1 : P) (h2 : P) : P := by
   exact? using h2 says
     exact h2
 
-/-!
+/-
 ## exact? を使用する際のコツ
 
 これは `exact?` に限らず、Lean でライブラリ検索を行うとき常に意識した方が良いことですが、

@@ -13,7 +13,7 @@ example (n m : Rat) : n * m = ((n + m) ^ 2 - n ^ 2 - m ^ 2 ) / 2 := by
   -- Rat は可換環なので、 示すべきことが言える
   ring
 
-/-! 分母がゼロでないことが判らない場合は動作しません。分母がゼロでないことを証明してローカルコンテキストに加えると動作することがあります。-/
+/- 分母がゼロでないことが判らない場合は動作しません。分母がゼロでないことを証明してローカルコンテキストに加えると動作することがあります。-/
 
 example {x y z : Rat} (hy : y = z ^ 2 + 1) : (x + 2 * y) / y = x / y + 2 := by
   -- 最初 `field_simp` は動作しない
@@ -27,7 +27,7 @@ example {x y z : Rat} (hy : y = z ^ 2 + 1) : (x + 2 * y) / y = x / y + 2 := by
   -- 動作するようになった
   field_simp
 
-/-! ## 制約
+/- ## 制約
 `field_simp` という名前の通り、割り算が体の割り算でなければ動作しません。たとえば 自然数 `Nat` における割り算は `field_simp` では扱うことができず、次のコード例のように工夫する必要があります。-/
 
 example (n m : Nat) : n * m = ((n + m) ^ 2 - n ^ 2 - m ^ 2 ) / 2 := by

@@ -43,7 +43,7 @@ example {c d : ℝ} (h : a + c + 1 ≤ b + d + 1) :
 
   linarith
 
-/-! ## 補題の登録
+/- ## 補題の登録
 さらに `[gcongr]` 属性を付与することにより、 `gcongr` で呼び出して使える補題を増やすことができます。-/
 
 variable {U : Type*}

@@ -17,7 +17,7 @@ example (hPQ: P → Q) (hQR: Q → R) : P → R := by
   -- 仮定 `hQR : Q → R` と `hQ : Q` から `R` が導かれる
   exact hQR hQ
 
-/-! `have` で示した補題には必ず名前がつきます。名前を省略して `have : P := ...` とすると、自動的に `this` という名前になります。無名の補題が欲しい場合、代わりに `show` を検討してみてください。
+/- `have` で示した補題には必ず名前がつきます。名前を省略して `have : P := ...` とすると、自動的に `this` という名前になります。無名の補題が欲しい場合、代わりに `show` を検討してみてください。
 
 また `have` で同じ名前を2回宣言すると、古い方はアクセス不能になってしまいます。ローカルコンテキストの補題の置き換えを行いたいときは、代わりに `replace` を使用してください。 -/
 
@@ -44,7 +44,7 @@ example (hPQ : P ∧ Q) : P := by
 
   assumption
 
-/-! ### 存在 ∃
+/- ### 存在 ∃
 
 次のように、`∃ x: X, P x` という命題から、条件を満たす `x` を取り出すことができます。`x : X` と `hx : P x` がローカルコンテキストに追加されます。 -/
 

@@ -66,7 +66,7 @@ info: Try these:
 example : Nat.Prime 37 := by
   hint
 
-/-!
+/-
 ## タクティクの新規登録
 
 登録されているタクティクに `tac` を追加するには、`register_hint tac` を実行します。

@@ -35,7 +35,7 @@ example (n : Nat) : sum n = n * (n + 1) / 2 := by
     -- 後は可換環の性質から示せる
     ring
 
-/-! ## 再帰定理
+/- ## 再帰定理
 Lean では、実は帰納法を使用するのに必ずしも `induction` は必要ありません。場合分けの中で示されたケースを帰納法の仮定として使うことができます。これは recursive theorem(再帰定理) と呼ばれることがあります。[^recursive]
 -/
 
@@ -70,7 +70,7 @@ theorem sample : True := by
       sorry
   trivial
 
-/-!
+/-
 ## 完全帰納法
 
 時には、 より強い帰納法が必要なこともあります。 強い帰納法とは、 たとえば
@@ -129,7 +129,7 @@ example (n : Nat) : fibonacci n = fib n := by
       -- 帰納法の仮定を適用して示す
       simp [ih_n, ih_succ]
 
-/-! なお、完全帰納法も `induction` タクティクを使わずに行うことができます。-/
+/- なお、完全帰納法も `induction` タクティクを使わずに行うことができます。-/
 
 /-- `fibonacci` と `fib` は同じ結果を返す -/
 theorem fib_eq (n : Nat) : fibonacci n = fib n := by

@@ -30,7 +30,7 @@ example (n : Nat) : sum n = n * (n + 1) / 2 := by
     -- 後は可換環の性質から示せる
     ring
 
-/-!
+/-
 ## 完全帰納法
 
 時には、 より強い帰納法が必要なこともあります。 強い帰納法とは、 たとえば

@@ -97,7 +97,7 @@ example (P Q : Nat → Prop) (h : ∀ n, P n ↔ Q n) : ∀ y, P (y + 1) → Q (
   -- 仮定 `P (y + 1)` より従う
   assumption
 
-/-! ## 否定 ¬ について
+/- ## 否定 ¬ について
 
 Lean では否定 `¬ P` は `P → False` として定義されているので、ゴールが `¬ P` のときに `intro` すると `P` が仮定に追加されて、ゴールが `False` に変わります。
 
@@ -118,7 +118,7 @@ example (h: P → Q) : ¬Q → ¬P := by
   -- `hQ : Q` と `hnQ : ¬Q` から矛盾が導かれる
   contradiction
 
-/-!
+/-
 ## 関数の構成
 
 より一般的には、`intro` は関数の構成に使うことができます。

@@ -11,7 +11,7 @@ example (hP : P) : P ∨ Q := by
 
   assumption
 
-/-! ## left, right を使わない方法
+/- ## left, right を使わない方法
 
 以下に示すように、`Or.inl` は `a` から `a ∨ b` を得る関数です。また `Or.inr` は `b` から `a ∨ b` を得る関数です。これを使うことで `left` や `right` を使わずに証明できます。
 -/

@@ -13,7 +13,7 @@ example (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) :
     12 * y - 4 * z ≥ 0 := by
   linarith
 
-/-! `linarith` はローカルコンテキストにある命題を読むので、`linarith` が通らないとき、追加で補題を示すことで解決することがあります。-/
+/- `linarith` はローカルコンテキストにある命題を読むので、`linarith` が通らないとき、追加で補題を示すことで解決することがあります。-/
 
 example : id x ≤ x := by
   -- `linarith` で示すことはできない
@@ -47,7 +47,7 @@ example (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) :
   linarith
 
 end --#
-/-! ## linarith と他のタクティクの使い分け
+/- ## linarith と他のタクティクの使い分け
 `1 < 2` のような簡単な数値のみの不等式の場合、`norm_num` や `simp_arith` でも証明ができます。
 同じ命題を示すのに複数のコマンドがあるわけですが、コマンド実行にかかる時間に違いがあります。
 

@@ -23,7 +23,7 @@ example (n m : Nat) : n * m = ((n + m) ^ 2 - n ^ 2 - m ^ 2 ) / 2 := by
   -- `omega` では示せる
   omega
 
-/-! Lean では自然数同士の引き算は整数同士の引き算とは異なる結果になって厄介なのですが、`omega` はこの問題を上手く処理します。 たとえば、以下は `linarith` では示すことができない線形な命題です。-/
+/- Lean では自然数同士の引き算は整数同士の引き算とは異なる結果になって厄介なのですが、`omega` はこの問題を上手く処理します。 たとえば、以下は `linarith` では示すことができない線形な命題です。-/
 
 variable (a b : Nat)
 
@@ -46,7 +46,7 @@ example : (a - b) - b = a - 2 * b := by
   fail_if_success linarith
   omega
 
-/-! `omega` は整数や自然数の整除関係を扱うこともできます。-/
+/- `omega` は整数や自然数の整除関係を扱うこともできます。-/
 
 example {a b c : ℤ} : 3 ∣ (100 * c + 10 * b + a) ↔ 3 ∣ (c + b + a) := by omega
 

@@ -20,7 +20,7 @@ example (h: P → Q) : ¬ (P ∧ ¬ Q) := by
 
   exact h
 
-/-! 以下の例は、「酔っぱらいのパラドクス」として有名な命題です。 -/
+/- 以下の例は、「酔っぱらいのパラドクス」として有名な命題です。 -/
 
 -- `People` という空ではない集合がある
 variable {People : Type} [Inhabited People]
@@ -51,7 +51,7 @@ example : ∃ (x : People), isDrinking x → ∀ (y : People), isDrinking y := b
     exists x
     simp_all
 
-/-!
+/-
 ## use_distrib
 
 option で `push_neg.use_distrib` を `true` にすると、`¬ (p ∧ q)` を `¬ p ∨ ¬ q` に変形します。
-Original file line number
+Diff line change
@@ Expand Up / @@ -66,7 +66,7 @@ info: Try these: @@
     example : Nat.Prime 37 := by
       hint
-    /-!
+    /-
     ## タクティクの新規登録
     登録されているタクティクに `tac` を追加するには、`register_hint tac` を実行します。
@@ Expand Down @@