remove-citations

What problem does it solve?

Remove explicit theorem citations from Acorn proofs by replacing each citation with local proof steps while keeping acorn verify passing after every attempted change. By default, make a full pass over the current acorn citations list unless the user explicitly narrows the scope. Use when the user asks to inline cited theorems, reduce acorn citations output, or improve proof style without changing the theorem being proved.

Core Features & Use Cases

• List the current citations.
• Take the citations in order and work through the full list unless the user narrowed the scope. For each citation, read:
• the local proof around that line
• the cited theorem statement
• Use rg -n to find the theorem definition and sed -n to inspect the relevant proof block.
• Replace the citation with the smallest local expansion that should supply the same fact downstream.
• If the cited theorem concludes the needed statement directly, try that conclusion first.
• If that is too large a leap, insert the instantiated intermediate statements from the theorem body.
• Prefer ordinary proof lines that fit the local argument. Do not keep the citation in a disguised form.
• Stop there. Do not switch into broader proof repair, explication, or theorem restructuring just to remove one citation.
• After each attempted replacement, verify immediately with acorn verify.
• If verification fails with a shallow explosion, stop immediately. Report that a prover bug was encountered, identify the file and line, and leave the repository in the failing state so the user can inspect it.
• Repeat for every citation in scope unless the run stopped early because of a shallow explosion. The default scope is the entire current acorn citations list. Run acorn citations again at the end to see what remains.

1. Heuristics

• Expand the theorem statement, not the theorem name.
• Try the strongest useful conclusion first; only add premises when the prover needs them.
• Keep replacements local. If removing one citation requires a broader rewrite, skip it unless the user asked for that.
• If verification reports shallow explosion, treat that as a prover bug, not as an ordinary proof failure.
• Existential and induction theorems often expand into bulky proof state. Remove those citations only when the replacement stays clear and short.
• Do not change the theorem being proved just to eliminate a citation.

Output

Report:

• which citations were removed
• which citations were skipped because the inline replacement did not verify
• any shallow explosion bug encountered, including the file, line, and attempted replacement
• the final acorn citations status, if checked

Quick Start

Run acorn citations, then iteratively replace each citation with local proof steps and verify after every change.