Merge pull request #1089 from lean-ja/Seasawher/issue1006

`linter.style.multiGoal` を紹介する

.github/workflows/ci.yml

@@ -23,6 +23,11 @@ jobs:
         uses: actions/checkout@v4
 
       - name: lean action
+        uses: leanprover/lean-action@v1
+        with:
+          build-args: "--log-level=warning"
+
+      - name: lean action (warning as fail)
         uses: leanprover/lean-action@v1
         with:
           build-args: "--fail-level=warning"

LeanByExample/Reference/Option/MultiGoal.lean

@@ -0,0 +1,31 @@
+/- # linter.style.multiGoal
+
+`linter.style.multiGoal` は、よくない証明の書き方を指摘するリンターの一つです。
+
+Lean では、複数のサブゴールがあるときにタクティクを実行すると最初のゴールに対して実行されるのですが、証明を構造化するという観点からは、ゴールの一つにフォーカスする（infoview に一つしかゴールが表示されないようにする）べきです。
+このリンタはそのような問題を指摘します。
+-/
+import Mathlib.Tactic.Linter.Multigoal
+
+set_option linter.style.multiGoal true
+
+/--
+warning: There are 2 unclosed goals before 'exact hP' and at least one remaining goal afterwards.
+Please focus on the current goal, for instance using `·` (typed as "\.").
+note: this linter can be disabled with `set_option linter.style.multiGoal false`
+-/
+#guard_msgs in
+  example {P Q : Prop} (hP : P) (hQ : Q) : P ∧ Q := by
+    -- ゴールが２つ生成される
+    constructor
+
+    -- この時点でサブゴールが２つあるのに、
+    -- フォーカスせずにタクティクを実行しているので警告が出る
+    exact hP
+    exact hQ
+
+-- 良い証明の例
+example {P Q : Prop} (hP : P) (hQ : Q) : P ∧ Q := by
+  constructor
+  · exact hP
+  · exact hQ

booksrc/SUMMARY.md

@@ -76,6 +76,7 @@
   - [autoImplicit: 自動束縛暗黙引数](./Reference/Option/AutoImplicit.md)
   - [hygiene: マクロ衛生](./Reference/Option/Hygiene.md)
   - [linter.flexible: 脆弱な証明を指摘する](./Reference/Option/Flexible.md)
+  - [linter.style.multiGoal: フォーカス強制](./Reference/Option/MultiGoal.md)
   - [relaxedAutoImplicit: 更にautoImplicit](./Reference/Option/RelaxedAutoImplicit.md)
 
 - [型クラス](./Reference/TypeClass/README.md)