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.
发布评论
评论（1）
您将在很多方面取得很大的进步：
请注意，在如此广泛使用的打样助手中，现在存在多种打样样式（不一定兼容），您必须先查看其中的几种，然后才能选择最适合您的项目和偏好的一种。
You will make a lot of progress in a lot of ways:
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.