I'm learning how to use Coq. And for now, I can prove almost all the small theorems I encounter. I'm pretty happy with my level, even though I still have a lot of progress to make. However, my proofs are often long and confused. They are not super clear to read, and I want to get better on this point. Are there some resources to read or watch to do this? How can I improve the quality of my proofs?
1 Answers
You will make a lot of progress in a lot of ways:
- Reading books and tutorials and the advice and examples they contain (you will find a list in Coq's page)
- Reading proofs in libraries and try to use the patterns you will find. You may invent self-corrected exercises: for instance prove by yourself a lemma on lists, arithmetics, etc., and compare your proof with the existing one in a library.
- Using some tools which make easier to write readable and structured proof scripts (mathcomp/ssreflect tactics, bullets, etc.)
- Asking questions (as you do) about style and proof script structure and size.
Note that there exists now various proof styles (not necessarily compatible) in such a widely used proof assistant, you will have to look at several of them before chosing which one is the most adapted to your project and preferences.
Related