Stream: Coq users

Topic: common pitfalls


view this post on Zulip yiyuan-cao (Jul 20 2023 at 15:02):

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!

view this post on Zulip Karl Palmskog (Jul 20 2023 at 15:05):

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

view this post on Zulip Karl Palmskog (Jul 20 2023 at 15:08):

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

view this post on Zulip yiyuan-cao (Jul 21 2023 at 01:26):

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


Last updated: Jun 13 2024 at 19:02 UTC