Are there any resources on the common pitfalls of doing proofs in Coq? For example, I've learned from the CPDT book (Certified Programming with Dependent Types) that `destruct`

a hypothesis of an indexed type with non-variable annotations might cause information loss. And I've learned that you should `remember`

certain expressions before doing `induction`

on it from Software Foundations (the chapter about inductive predicates). Thanks!

the closest resources I know are Coq tricks and the Coq requirements for Common Criteria evaluations.

many less related but possibly-relevant resources are listed here: https://github.com/coq-community/awesome-coq#resources

thank you! I'll check it out :wink:

Last updated: Jun 13 2024 at 19:02 UTC