remove-citations

Replace Acorn theorem citations with local proof steps and verify each change.

59|24|Updated Oct 3, 2024

Search Tags:#automation #citations #verifier #theorem #proof-editing #acorn

One-click install

npx skills add https://github.com/acornprover/acornlib --skill remove-citations

Or copy as Structured Prompt for Agent▼

Please help me install this Agent Skill.
Skill: remove-citations
Source: https://github.com/acornprover/acornlib/tree/main/.agents/skills/remove-citations
Command: npx skills add https://github.com/acornprover/acornlib --skill remove-citations

SYSTEM DOCUMENTATION & REQUIREMENTS

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.

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.

Frequently Asked Questions about remove-citations

High-intent search queries and answers about installing and using this skill.

FAQPage Schema

How do I remove explicit theorem citations from Acorn proofs?▼

Replace each theorem citation with the smallest local expansion of its statement or instantiated intermediate steps, then run `acorn verify` immediately after every replacement to ensure the proof remains valid.

What happens when removing citations causes a shallow explosion in acorn verify?▼

A shallow explosion is treated as a prover bug, not an ordinary proof failure. The process stops immediately, reports the file and line, and leaves the repository in the failing state for user inspection.

How do I inline cited theorems without changing the theorem being proved?▼

Expand the theorem statement rather than its name, prefer the strongest useful conclusion first, and skip broader proof repair or theorem restructuring to keep replacements strictly local.

When should I avoid replacing citations with local proof steps?▼

Avoid replacing citations when the theorem involves existential or induction logic that expands into bulky proof state, or when removing a citation requires a broader rewrite beyond the local argument.

Can I target specific citations to remove instead of scanning the entire acorn proof?▼

Yes, you can narrow the scope to target specific citations. By default the process makes a full pass over the current `acorn citations` list, but processes only the narrowed scope if explicitly requested.

What is the best way to reduce acorn citations output?▼

Iteratively replace each citation with ordinary local proof lines, verify after each change with `acorn verify`, and run `acorn citations` again at the end to check what remains.