Coq重构影响分析：如何识别受A→A'变更影响的所有证明？

Great question! When you refactor a core data structure or lemma A into A' in Coq, there are solid practices and tools to help you identify all proofs that depend on the original definition. Here’s what you can leverage:

• Use Coq’s built-in dependency analyzers

  • The coqdep command is your first stop—it’s Coq’s native tool for generating dependency graphs between files. Run coqdep -f _CoqProject (if you use a _CoqProject file) or specify individual .v files, and it will output which files depend on the one containing A. This gives you a high-level view of all proof files that rely on your original definition.
  • For finer-grained checks, use coqchk -deps your_file.v to inspect dependencies within a single file, pinpointing exactly which lemmas or theorems reference A.

• Leverage IDE features for reference navigation

  • If you use CoqIDE or the VsCoq plugin for VS Code, right-click the definition of A and select "Find References" (or a similar option). The IDE will directly highlight or jump to every occurrence of A across your project, including its use in proofs. This is super convenient for smaller codebases.

• Lean on structured code organization

  • If you’ve already grouped proofs related to A in dedicated modules or files (like A_proofs.v), your refactoring scope becomes immediately clear—you can focus your checks on those specific files first.
  • Stick to explicit Require Import/Export statements instead of global imports. This makes coqdep’s output more accurate and avoids hidden dependencies that might slip through the cracks.

• Try community refactoring tools

  • The coq-refactoring plugin offers automated support for common refactoring tasks like renaming definitions or replacing references. It can automatically update most uses of A to A' in proofs, and flag cases where manual adjustments are needed (like when A' changes the logical structure enough to break proof scripts).
  • For custom analysis, you can use Coq-Elpi to write small scripts that scan your entire project for occurrences of A and report their locations.

• Incremental compilation as a quick check

  • Sometimes the simplest approach works: after updating A to A', recompile your project. Coq’s compiler will throw errors (like "unbound identifier A") wherever the original definition is still referenced in proofs. These error messages directly point you to the proofs that need fixing—perfect for medium-sized projects where you want a straightforward way to find affected code.

Also, thanks for noting you’ll try these suggestions and report back—curious to hear how they work for your refactoring effort!

内容的提问来源于stack exchange，提问作者Zheng Cheng