Merge pull request #720 from lean-ja/Seasawher/issue708

<;> を見出し語にする

Examples/Tactic/AllGoals.lean

@@ -20,37 +20,7 @@ example {R : Prop} (hnP : ¬ P) : (P → R) ∧ (P → Q) := by
     intro h
     contradiction
 
-/-!
-## タクティク結合子 <;>
-タクティク結合子 `<;>` によってもほぼ同じことができます。
--/
+/- タクティク結合子 [`<;>`](./SeqFocus.md) によってもほぼ同じことができます。-/
 
 example (hP : P) (hQ : Q) : P ∧ Q := by
   constructor <;> assumption
-
-/-! しかし、`<;>` と `all_goals` は完全に同じではありません。
-`<;>` が「直前のタクティクによって生成された全てのサブゴール」に対して後続のタクティクを実行するのに対して、`all_goals` は「すべての未解決のゴール」に対して後続のタクティクまたはタクティクブロックを実行します。
-
-実際に以下のような例ではその違いが現れます。
--/
-
-variable (P Q R : Prop)
-
-example (hP : P) (hQ : Q) (hR : R) : (P ∧ Q) ∧ R := by
-  constructor
-
-  constructor <;> try assumption
-
-  -- まだ示すべきことが残っている
-  show R
-  assumption
-
-example (hP : P) (hQ : Q) (hR : R) : (P ∧ Q) ∧ R := by
-  constructor
-
-  constructor
-  all_goals
-    try assumption
-
-  -- 証明完了
-  done

Examples/Tactic/SeqFocus.lean

@@ -0,0 +1,39 @@
+/- # <;>
+`<;>` (seq focus)は、直前のタクティクによって生成されたすべてのサブゴールに対して後続のタクティクを適用することを意味するタクティク結合子です。
+-/
+
+variable (P Q : Prop)
+
+example (hP : P) (hQ : Q) : P ∧ Q := by
+  constructor <;> assumption
+
+/- これは [`all_goals`](./AllGoals.md) とよく似た挙動です。
+
+しかし、`<;>` と `all_goals` は完全に同じではありません。
+`<;>` が「直前のタクティクによって生成された全てのサブゴール」に対して後続のタクティクを実行するのに対して、`all_goals` は「すべての未解決のゴール」に対して後続のタクティクまたはタクティクブロックを実行します。
+
+実際に以下のような例ではその違いが現れます。
+-/
+
+variable (P Q R : Prop)
+
+/-- <;> を使用したとき -/
+example (hP : P) (hQ : Q) (hR : R) : (P ∧ Q) ∧ R := by
+  constructor
+
+  constructor <;> try assumption
+
+  -- まだ示すべきことが残っている
+  show R
+  assumption
+
+/-- all_goals を使用したとき -/
+example (hP : P) (hQ : Q) (hR : R) : (P ∧ Q) ∧ R := by
+  constructor
+
+  constructor
+  all_goals
+    try assumption
+
+  -- 証明完了
+  done

src/SUMMARY.md

@@ -63,6 +63,7 @@
     - [simps: simp補題の自動生成](./Command/Attribute/Simps.md)
 
 - [タクティク](./Tactic/README.md)
+  - [<;> 生成された全ゴールに適用](./Tactic/SeqFocus.md)
   - [ac_rfl: 可換性と結合性を使う](./Tactic/AcRfl.md)
   - [aesop: 自明な証明の自動探索](./Tactic/Aesop.md)
   - [all_goals: 全ゴールに対して適用](./Tactic/AllGoals.md)