doc(rules): state rule purposes and exceptions; closing simp is terminal

AGENTS.md

@@ -333,13 +333,23 @@ the pin past it and remove the superseded local copy together. Record unresolved
 
 ## Proof hygiene
 
+These rules exist for readability and robustness. When following one would make a particular
+proof or statement worse (longer, harder to read, or working against the automation), deviate,
+say why in the PR, and propose amending the rule. Reviewers judge a deviation by the rule's
+purpose, not its letter.
+
 - No `sorry` on `main`, no custom `axiom`, no `native_decide`.
 - `set_option maxHeartbeats` / `maxRecDepth` overrides need a justifying comment. A
   `maxHeartbeats` above the 200000 default, or zero (unlimited), also needs a reviewed entry in
   `scripts/heartbeat_allowlist.txt`, which `scripts/check_hygiene.py` enforces and keeps
   shrinking; prefer reducing the proof's cost.
 - Never put `[simp]` on machine step functions or transition tables (goals explode).
-- Non-terminal `simp` only as `simp only`; definitions as terms, not `by` blocks, where possible.
+- Non-terminal `simp` only as `simp only`, so that later steps do not depend on the shape of a
+  `simp` normal form, which changes as simp sets grow. A `simp` whose result is closed by a
+  finishing tactic that does not depend on that shape (`omega`, `linarith`, `nlinarith`,
+  `norm_num`, `ring`, `grind`, `tauto`), as in `simp [h]; omega`, counts as terminal, as in
+  Mathlib's flexible-tactic linter.
+- Definitions as terms, not `by` blocks, where possible.
 - Prefer `do` notation for sequential monadic computations, including probabilistic experiments
   in theorem statements. Keep explicit `bind` in laws about bind and proof steps that use those
   laws directly, and for operations such as `PMF.bind` between different universes that the standard

CONTRIBUTING.md

@@ -54,7 +54,9 @@ Mathlib's standard linter set already enforces the mechanical part; reviews enfo
 4. **Automation as API.** Curate `simp`, `grind` and `fun_prop` sets so routine facts follow
    without unfolding; a fact that repeatedly needs plumbing signals a missing lemma or interface.
 5. **Definitions and proofs.** Definitions are terms where possible. Proofs keep their logical
-   progression visible: `simp only` mid-proof, and no large terminal `simpa` hiding the argument.
+   progression visible: `simp only` mid-proof (a `simp` closed at once by `omega`, `linarith` or
+   a similar finishing tactic counts as terminal), and no large terminal `simpa` hiding the
+   argument.
 6. **Placement.** No duplicates; small topic modules; clients import what they use.
 7. **Documentation.** Definitions and theorems are documented, citing sources; module docstrings
    list the actual public API; each area has a chapter in the guide.
@@ -79,7 +81,19 @@ preference:
 
 The rewritten form should stay definitionally equal to the old one, so that clients and automation
 (`fun_prop`, `@[program_certificate]`) keep working. Single projections (`p.1`) and
-destructuring inside proofs (`obtain ⟨⟨d, x⟩, c⟩ := s`) are fine.
+destructuring inside proofs (`obtain ⟨⟨d, x⟩, c⟩ := s`) are fine. "Composed projections" means
+point-free composition such as `Prod.fst ∘ Prod.snd`; respelling `p.2.1` as `Prod.fst (Prod.snd p)`
+or naming a tail with `let rest := p.2` does not name anything.
+
+Two places keep projections, as standing exceptions:
+
+- **Conclusions that automation looks up by head.** Destructuring turns the function into a
+  `match` auxiliary, so `@[program_certificate]` and efficiency-key lookups no longer find the
+  certificate. Keep the projection form there.
+- **Section `variable` hypotheses in `module` files.** On the current toolchain a destructuring
+  lambda in a section `variable` of a `public section` elaborates to `sorry`, with only a warning
+  ([#1764](https://github.com/cslib-community/complexitylib/issues/1764)). Use projections there,
+  or bind the hypothesis in the theorem's own signature.
 
 Improving an interface never weakens the mathematics: keep the models, encodings, independent
 resource bounds and nonvacuity of the results it touches.

scripts/check_hygiene.py

@@ -366,8 +366,27 @@ def has_nearby_comment(raw_lines: list[str], code_lines: list[str], idx_0based:
 )
 
 
+# Finishing tactics that do not depend on the exact shape of a `simp` normal form; Mathlib's
+# flexible-tactic linter accepts them after `simp`, so a `simp` they close counts as terminal.
+FINISHING_RE = re.compile(r"^(?:omega|linarith|nlinarith|norm_num|ring|grind|tauto)\b")
+
+
+def closes_block(lines: list[str], j: int) -> bool:
+    """Whether line `j` is a finishing tactic and the last tactic of its block."""
+    if not FINISHING_RE.match(lines[j].strip()):
+        return False
+    indent = len(lines[j]) - len(lines[j].lstrip(" "))
+    k = j + 1
+    while k < len(lines) and not lines[k].strip():
+        k += 1
+    if k >= len(lines) or COMMAND.match(lines[k]):
+        return True
+    return len(lines[k]) - len(lines[k].lstrip(" ")) < indent
+
+
 def find_nonterminal_bare_simps(code: str) -> list[int]:
-    """Return 1-based line numbers of non-terminal bare `simp` tactics in masked code."""
+    """Return 1-based line numbers of non-terminal bare `simp` tactics in masked code. A `simp`
+    followed only by a finishing tactic (`FINISHING_RE`) that ends its block is terminal."""
     lines = code.split("\n")
     violations: list[int] = []
     for i, line in enumerate(lines):
@@ -398,10 +417,10 @@ def find_nonterminal_bare_simps(code: str) -> list[int]:
         next_has_bullet = next_stripped.startswith(("·", "•"))
         if has_bullet:
             # Inside a `· simp` line, a following tactic at indent > bullet indent is non-terminal.
-            if next_indent > indent and not next_has_bullet:
+            if next_indent > indent and not next_has_bullet and not closes_block(lines, j):
                 violations.append(i + 1)
         else:
-            if next_indent == indent and not next_has_bullet:
+            if next_indent == indent and not next_has_bullet and not closes_block(lines, j):
                 violations.append(i + 1)
     return violations
 

scripts/test_check_hygiene.py

@@ -254,6 +254,30 @@ def test_forbidden_tokens_and_nonterminal_simp(self) -> None:
         self.assertTrue(any("non-terminal bare `simp`" in e for e in errors))
         self.assertTrue(any("forbidden `sorry`" in e for e in errors))
 
+    def test_simp_closed_by_finishing_tactic_is_terminal(self) -> None:
+        p = self.write(
+            "Complexity/FinishingSimp.lean",
+            "module\n"
+            "-- upstream: candidate\n\n"
+            "theorem t1 (n : Nat) (h : n < 3) : n < 4 := by\n"
+            "  simp [Nat.lt_succ_iff] at h\n"
+            "  omega\n"
+            "theorem t2 (n : Nat) : n < 4 ∨ True := by\n"
+            "  constructor\n"
+            "  · simp\n"
+            "    omega\n"
+            "  · trivial\n"
+            "theorem t3 (n : Nat) (h : n < 3) : n < 4 := by\n"
+            "  simp at h\n"
+            "  omega\n"
+            "  done\n"
+            "theorem t4 (n : Nat) (h : n < 3) : n < 4 := by\n"
+            "  simp at h\n"
+            "  rw [h]\n",
+        )
+        errors = check_hygiene.check_file(p, root=self.root, check_simp=True)
+        self.assertEqual(sorted(int(e.split(":")[1]) for e in errors), [13, 17])
+
     def test_quote_characters_do_not_hide_forbidden_theorem(self) -> None:
         for literal in ("'\"'", r"'\"'"):
             with self.subTest(literal=literal):