From 4339c2060ae26dc6f0d5538371819478dbaec709 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 4 Nov 2024 01:25:39 +0900 Subject: [PATCH 1/2] =?UTF-8?q?simp=5Fall=20=E3=81=AF=E9=80=9A=E3=82=8B?= =?UTF-8?q?=E3=81=8C=20simp=20at=20*=20=E3=81=AF=E9=80=9A=E3=82=89?= =?UTF-8?q?=E3=81=AA=E3=81=84=E4=BE=8B=20Fixes=20#1041?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Reference/Tactic/SimpAll.lean | 25 +++++++++++++++++++++ booksrc/SUMMARY.md | 1 + 2 files changed, 26 insertions(+) create mode 100644 LeanByExample/Reference/Tactic/SimpAll.lean diff --git a/LeanByExample/Reference/Tactic/SimpAll.lean b/LeanByExample/Reference/Tactic/SimpAll.lean new file mode 100644 index 00000000..5eaac731 --- /dev/null +++ b/LeanByExample/Reference/Tactic/SimpAll.lean @@ -0,0 +1,25 @@ +/- # simp_all + +`simp_all` タクティクは、`simp` タクティクの派生で、仮定とゴールに対してこれ以上適用できなくなるまで `simp` を適用します。 + +`simp at *` と似ていますが、`simp_all` は簡約された仮定を再び簡約に使うなど再帰的な挙動をします。 +-/ + +example (P : Nat → Bool) + (h1 : P (if 0 + 0 = 0 then 1 else 2)) + (h2 : P (if P 1 then 0 else 1) ) : P 0 := by + simp at * + + -- まだゴールが残っている + show P 0 + + simp [h1] at h2 + assumption + +example (P : Nat → Bool) + (h1 : P (if 0 + 0 = 0 then 1 else 2)) + (h2 : P (if P 1 then 0 else 1) ) : P 0 := by + -- 一発で終わる。 + -- h1 を簡約した後で、h2 を「簡約後の h1」を使って簡約し、 + -- ゴールと仮定が一致していることを確認するという挙動をする。 + simp_all diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md index 018962a1..f14fb5c0 100644 --- a/booksrc/SUMMARY.md +++ b/booksrc/SUMMARY.md @@ -168,6 +168,7 @@ - [says: タクティク提案の痕跡を残す](./Reference/Tactic/Says.md) - [set: 定義の導入](./Reference/Tactic/Set.md) - [show: 示すべきことを宣言](./Reference/Tactic/Show.md) + - [simp_all: 仮定とゴールを全て単純化](./Reference/Tactic/SimpAll.md) - [simp: 単純化](./Reference/Tactic/Simp.md) - [slim_check: 反例を見つける](./Reference/Tactic/SlimCheck.md) - [sorry: 証明したことにする](./Reference/Tactic/Sorry.md) From 7a3cbfc7692ee6e4b52d30ddfe3d09bf864ca7db Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 4 Nov 2024 01:29:53 +0900 Subject: [PATCH 2/2] =?UTF-8?q?simp=20=E3=81=AE=E3=83=9A=E3=83=BC=E3=82=B8?= =?UTF-8?q?=E3=81=8B=E3=82=89=20simp=5Fall=20=E3=81=AB=E3=83=AA=E3=83=B3?= =?UTF-8?q?=E3=82=AF=E3=82=92=E5=BC=B5=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Reference/Tactic/Simp.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanByExample/Reference/Tactic/Simp.lean b/LeanByExample/Reference/Tactic/Simp.lean index c3d210e0..b05c6753 100644 --- a/LeanByExample/Reference/Tactic/Simp.lean +++ b/LeanByExample/Reference/Tactic/Simp.lean @@ -126,7 +126,7 @@ example {x y : Nat} : 0 < 1 + x ∧ x + y + 2 ≥ y + 1 := by simp_arith /- ## simp_all -`simp_all` はローカルコンテキストとゴールをこれ以上単純化できなくなるまですべて単純化します。-/ +[`simp_all`](./SimpAll.md) はローカルコンテキストとゴールをこれ以上単純化できなくなるまですべて単純化します。-/ example {P Q : Prop} (hP : P) (hQ : Q) : P ∧ (Q ∧ (P → Q)) := by -- simp at * は失敗する