From a4ee4aea2fd2ffb9642f03ef1cc0946f90f4c18e Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Thu, 29 Aug 2024 03:21:57 +0900
Subject: [PATCH] =?UTF-8?q?<;>=20=E3=82=92=E8=A6=8B=E5=87=BA=E3=81=97?=
 =?UTF-8?q?=E8=AA=9E=E3=81=AB=E3=81=99=E3=82=8B=20Fixes=20#708?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Tactic/AllGoals.lean | 32 +---------------------------
 Examples/Tactic/SeqFocus.lean | 39 +++++++++++++++++++++++++++++++++++
 src/SUMMARY.md                |  1 +
 3 files changed, 41 insertions(+), 31 deletions(-)
 create mode 100644 Examples/Tactic/SeqFocus.lean

diff --git a/Examples/Tactic/AllGoals.lean b/Examples/Tactic/AllGoals.lean
index 9c3839c2..00870634 100644
--- a/Examples/Tactic/AllGoals.lean
+++ b/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
diff --git a/Examples/Tactic/SeqFocus.lean b/Examples/Tactic/SeqFocus.lean
new file mode 100644
index 00000000..d21cc62e
--- /dev/null
+++ b/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
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 7bf44801..079cc319 100644
--- a/src/SUMMARY.md
+++ b/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)