From 4b98806a1edaaf4650f0305278295bd143663cf4 Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Fri, 22 May 2026 09:03:41 +0900 Subject: [PATCH 1/4] Add norm_num tactic article --- LeanByExample/Tactic/NormNum.lean | 34 +++++++++++++++++++++++++++++++ LeanByExample/Tactic/README.lean | 1 + booksrc/SUMMARY.md | 1 + 3 files changed, 36 insertions(+) create mode 100644 LeanByExample/Tactic/NormNum.lean diff --git a/LeanByExample/Tactic/NormNum.lean b/LeanByExample/Tactic/NormNum.lean new file mode 100644 index 00000000..00d6a0e5 --- /dev/null +++ b/LeanByExample/Tactic/NormNum.lean @@ -0,0 +1,34 @@ +/- # norm_num + +`norm_num` は、数値リテラルを含む式を正規化するタクティクです。 +閉じた数値計算や、数値だけで決まる等式・不等式・整除関係を示したいときに使います。 + +`norm_num` は具体的な計算を進めてゴールを閉じます。 -/ +import Mathlib.Tactic.NormNum + +example : (37 : Nat) * 23 + 19 = 870 := by + norm_num + +example : ¬ (15 : Int) ^ 2 < 100 := by + norm_num + +example : (2 : ℚ) / 3 + 1 / 6 = 5 / 6 := by + norm_num + +/- `norm_num` は仮定に対しても使うことができます。 +たとえば `norm_num at h` とすると、仮定 `h` の中の数値計算を正規化します。 -/ + +example {n : Nat} (h : 3 ∣ n + 4) : 3 ∣ n + 1 := by + -- `n + 4` は `n + 1 + 3` と同じなので、3 で割った余りは変わらない + norm_num at h + + assumption + +/- `norm_num` は `norm_num [f]` のように補題や定義を渡して使うこともできます。 +渡した補題で式を展開してから、数値計算を正規化します。 -/ + +def taxIncluded (price : Nat) : Nat := + price + price / 10 + +example : taxIncluded 1200 = 1320 := by + norm_num [taxIncluded] diff --git a/LeanByExample/Tactic/README.lean b/LeanByExample/Tactic/README.lean index b6232f44..81cfe65f 100644 --- a/LeanByExample/Tactic/README.lean +++ b/LeanByExample/Tactic/README.lean @@ -64,6 +64,7 @@ Lean で利用可能なタクティクは多岐にわたるので、ここによ | [`decide`](./Decide.md) | 計算によって命題の真偽を判定したいとき | | [`simp`](./Simp.md) | 等式書き換えによる単純化を自動で行いたいとき | | [`grind`](./Grind.md) | 書き換え・前方推論・後方推論・場合分けを自動で行いたいとき | +| [`norm_num`](./NormNum.md) | 具体的な数値計算を正規化して示したいとき | | [`try?`](./Try.md) | とりあえず証明したいとき | -/ diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md index 98cd8abf..cc28061d 100644 --- a/booksrc/SUMMARY.md +++ b/booksrc/SUMMARY.md @@ -227,6 +227,7 @@ - [mvcgen: 手続き型プログラムに対する検証条件生成](./Tactic/Mvcgen.md) - [native_decide: 実行による証明](./Tactic/NativeDecide.md) - [nlinarith: 非線形な(不)等式を示す](./Tactic/Nlinarith.md) + - [norm_num: 数値計算を正規化](./Tactic/NormNum.md) - [norm_cast: 型キャストの簡略化](./Tactic/NormCast.md) - [nth_rw: n 番目の項だけ rw](./Tactic/NthRw.md) - [obtain: 分解して取り出す](./Tactic/Obtain.md) From 1fb38e4b192bc9a3a2bf9dd2a6f7861981370e92 Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Wed, 27 May 2026 01:45:53 +0900 Subject: [PATCH 2/4] =?UTF-8?q?=E4=B8=A6=E3=81=B3=E9=A0=86=E3=81=AE?= =?UTF-8?q?=E4=BF=AE=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- booksrc/SUMMARY.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md index 27b9e648..4dbda57f 100644 --- a/booksrc/SUMMARY.md +++ b/booksrc/SUMMARY.md @@ -228,8 +228,8 @@ - [mvcgen: 手続き型プログラムに対する検証条件生成](./Tactic/Mvcgen.md) - [native_decide: 実行による証明](./Tactic/NativeDecide.md) - [nlinarith: 非線形な(不)等式を示す](./Tactic/Nlinarith.md) - - [norm_num: 数値計算を正規化](./Tactic/NormNum.md) - [norm_cast: 型キャストの簡略化](./Tactic/NormCast.md) + - [norm_num: 数値計算を正規化](./Tactic/NormNum.md) - [nth_rw: n 番目の項だけ rw](./Tactic/NthRw.md) - [obtain: 分解して取り出す](./Tactic/Obtain.md) - [omega: 自然数の線形計画を解く](./Tactic/Omega.md) From 36af4ec617b54f0e1d854d5b0b964418ce421e32 Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Wed, 27 May 2026 01:51:08 +0900 Subject: [PATCH 3/4] =?UTF-8?q?=E8=A8=98=E4=BA=8B=E3=81=AE=E6=A0=A1?= =?UTF-8?q?=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Tactic/NormNum.lean | 23 ++++++++++++++--------- 1 file changed, 14 insertions(+), 9 deletions(-) diff --git a/LeanByExample/Tactic/NormNum.lean b/LeanByExample/Tactic/NormNum.lean index 00d6a0e5..6631656c 100644 --- a/LeanByExample/Tactic/NormNum.lean +++ b/LeanByExample/Tactic/NormNum.lean @@ -1,12 +1,10 @@ /- # norm_num -`norm_num` は、数値リテラルを含む式を正規化するタクティクです。 -閉じた数値計算や、数値だけで決まる等式・不等式・整除関係を示したいときに使います。 - -`norm_num` は具体的な計算を進めてゴールを閉じます。 -/ +`norm_num` は、数値リテラルを含む式を正規化するタクティクです。変数を含まない等式・不等式・整除関係等を示したいときに使います。 +-/ import Mathlib.Tactic.NormNum -example : (37 : Nat) * 23 + 19 = 870 := by +example : 37 * 23 + 19 = 870 := by norm_num example : ¬ (15 : Int) ^ 2 < 100 := by @@ -16,9 +14,12 @@ example : (2 : ℚ) / 3 + 1 / 6 = 5 / 6 := by norm_num /- `norm_num` は仮定に対しても使うことができます。 -たとえば `norm_num at h` とすると、仮定 `h` の中の数値計算を正規化します。 -/ +たとえば `norm_num at h` とすると、仮定 `h` の中の数値式を正規化します。 -/ example {n : Nat} (h : 3 ∣ n + 4) : 3 ∣ n + 1 := by + -- 最初は、h とゴールは違う式なので証明できない + fail_if_success assumption + -- `n + 4` は `n + 1 + 3` と同じなので、3 で割った余りは変わらない norm_num at h @@ -27,8 +28,12 @@ example {n : Nat} (h : 3 ∣ n + 4) : 3 ∣ n + 1 := by /- `norm_num` は `norm_num [f]` のように補題や定義を渡して使うこともできます。 渡した補題で式を展開してから、数値計算を正規化します。 -/ -def taxIncluded (price : Nat) : Nat := - price + price / 10 +def taxIncluded (price : Nat) (taxRate : Nat) : Nat := + price + price * taxRate / 100 + +example : taxIncluded 1200 10 = 1320 := by + -- 最初は norm_num だけでは証明が終わらない + fail_if_success solve | + norm_num -example : taxIncluded 1200 = 1320 := by norm_num [taxIncluded] From 383e2e04a23d124b9eaf442187349df38378a7f4 Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Wed, 27 May 2026 01:51:57 +0900 Subject: [PATCH 4/4] =?UTF-8?q?=E3=82=BF=E3=82=AF=E3=83=86=E3=82=A3?= =?UTF-8?q?=E3=82=AF=E6=97=A9=E8=A6=8B=E8=A1=A8=E3=81=8B=E3=82=89=E3=81=AF?= =?UTF-8?q?=E5=89=8A=E9=99=A4=E3=81=99=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Tactic/README.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/LeanByExample/Tactic/README.lean b/LeanByExample/Tactic/README.lean index 81cfe65f..b6232f44 100644 --- a/LeanByExample/Tactic/README.lean +++ b/LeanByExample/Tactic/README.lean @@ -64,7 +64,6 @@ Lean で利用可能なタクティクは多岐にわたるので、ここによ | [`decide`](./Decide.md) | 計算によって命題の真偽を判定したいとき | | [`simp`](./Simp.md) | 等式書き換えによる単純化を自動で行いたいとき | | [`grind`](./Grind.md) | 書き換え・前方推論・後方推論・場合分けを自動で行いたいとき | -| [`norm_num`](./NormNum.md) | 具体的な数値計算を正規化して示したいとき | | [`try?`](./Try.md) | とりあえず証明したいとき | -/