Merge pull request #1045 from lean-ja/Seasawher/issue1041

simp_all を独立したタクティクとして紹介する

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 * は失敗する

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

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)