docs(lean4): deepen the consolidated simp reference (v4.5.9)

[cameronfreer]

Summary

Supersedes #47. References #47.

Integrates the valuable simp/simproc material from @alok's PR #47 — grounded in the Lean community blog series (Simp made simple, Fantastic Simprocs and How to Write Them, Simprocs for the Working Mathematician) — into the single consolidated simp-reference.md, rather than reviving the pre-#36 file split (#36 consolidated simp-hygiene.md/simproc-patterns.md five days before #47 was opened) or adding a standalone skill.

History structure (same pattern as #163): Alok's two commits are cherry-picked onto current main with -x provenance and authorship intact, followed by rework commits. Conflict-resolution policy for the cherry-picks: his edits to the deleted split files were landed by taking his content (git's rename detection mapped the hygiene rewrite onto simp-reference.md; simproc-patterns.md was temporarily resurrected as his version), and the README hunks were reduced to this PR's own entries — the original branch had eight unrelated stacked skill entries (borrowed-params, compiler-attrs, compiler-pipeline, ffi-interop, init-runtime, specialization, symbol-linkage, zulip-extract) referencing files that exist in no PR; those were dropped.

What the deepened reference now covers (with review-round corrections applied)

• Choose the Mechanism — 9-row table: rw / simp only / terminal simp / local simp set / @[simp] / dsimproc / simproc / leave-unchanged / hand-off. .continue is not a peer row (it's a control result); the local-first bias is scoped to non-terminal normalization.
• Simp Normal Forms and Rewrite Policy — two meanings of normal form (library default set vs invocation-relative), defined against the full simplifier context (lemmas, simprocs, config, congruence, local hypotheses, discharger); operational test excludes the proposed lemma itself and requires the RHS to reach the intended normal form; canonical vs locally-useful rewrites; the revRange lesson as an evaluator-simproc rule (decline symbolic inputs in evaluator-style procedures; canonical proof-producing symbolic transformations stay legitimate); simpNF relationship.
• Hygiene — reorganized around Alok's "should this be a simp lemma?" gate; debugging progression (simp? → minimize → trace); escalation triggers with the correction that side conditions alone don't force a simproc (conditional lemmas + discharger first). Fixed in passing: @[simp?] was listed as an attribute (simp? is a tactic).
• Simproc Authoring — dsimproc vs simproc with a working default; pre/post placement at registration/invocation via ↓ (post is the default); exact per-phase result semantics — .done is a control-flow promise ("stop visiting"), never a normal-form claim; prefer .visit when unsure; performance discipline with "no unbounded or general-purpose proof search" (deterministic domain computation is legitimate) and benchmarking scoped to hot-path procedures.
• Two verified examples replace docs(lean4): add simp and simproc skill #47's non-compiling <construct …> placeholder: an explicit-data dsimproc (demonstrating ↓ pre-activation and symbolic decline) and a proof-producing simproc (mkDecideProof/mkEqTrue). Both batch-compiled on Lean v4.32.0 via the Lean LSP (lean_run_code), recorded in the file's version-metadata block. (Dual-toolchain verification wasn't feasible locally; the repo pins no snippet floor — the metadata block records the verified version per house convention.)
• grind-tactic.md (Option A) keeps only its grind-specific escalation conditions + a link — single ownership of simproc mechanics.

Not carried forward: the standalone skill, the separate simp-normal-forms.md, the split-file resurrection, the placeholder sketch, the stacked README entries.

Testing

• tools/lint_docs.sh — all checks pass (incl. Check 23 at 4.5.9 and the reference version-metadata block checks).
• tools/test_contracts.sh — 31 passed, 0 failed. tools/smoke_snippets.sh — passed.
• Both Lean examples compiled clean via lean_run_code on Lean v4.32.0.
• Stale-path grep (simp-hygiene.md / simproc-patterns.md / simp-normal-forms.md / lean4-simp-simprocs) over active docs — clean (MIGRATION.md's historical mention and CHANGELOG attribution are intentional).

Credit

Co-authored-by: Alok Singh alokbeniwal@gmail.com