How to Efficiently Structure Proofs in Coq for Large Scale Projects?

Using Coq
1

Hello,

I am working on a large-scale formal verification project using Coq and could use some advice. As the codebase grows…, managing proofs has become increasingly challenging. I am particularly struggling with:

Modularity :- How do you structure proofs to keep them reusable across different parts of the project: ??
Performance :- Some proofs are taking excessively long to compile. Are there best practices to optimize proof scripts; ??
Documentation :- What is the most efficient way to document proofs to make them understandable for team members unfamiliar with the details: ??

I am aware of tactics like Proof using and Section but would appreciate more hands on examples or resources that could help. Additionally…, how do you handle dependencies when integrating multiple proofs: ??

I have already searched on the forum for the solution to my query and found this thread https://coq.discourse.group/t/how-to-represent-mathematical-structures-in-coq-servicenow but couldn’t find any solution.

Looking forward to learning from your experiences and insights. Any advice, tools or resources you could share would be greatly appreciated !!

Thanks in advance !!

With REgards,
Daniel Jose

2

These are active research fields and I am far from being an expert. My 2 cts:

  • Split separate subjects in separate files, so that parallel compilation can be exploited and also to reuse these files in a fine grained manner. Otherwise you will pollute your environment with unnecessary entries.
  • Use vos/vok and other unsafe IDE modes when you develop your proofs. The compile time is mostly ignored then.
  • Type classes is an appealing solution for modularity, but it makes things extremely slow if you don’t take the time to tweak them very tightly. Strong expertise needed here.
  • canonical structures are to be considered, strong expertise needed too.
  • Modules are very nice to build modular things (!) but they are very invasive. Most people don’t use them because of that. Or for very limited areas (e.g. stdlib’s MSet). I personnaly wouldn’t throw them aside too quickly, depending on what you want to do. There invasiveness is there only disadvantage AFAIK.