Stream: Coq users

Topic: proofs to learn from


view this post on Zulip Darij Grinberg (Feb 18 2022 at 22:10):

I'm looking for some readable proofs to get a hang of Coq with (both with and without SSReflect). Ideally, mathematically interesting statements, more than just the type of ab=ba. But not too deep or complicated; in particular I prefer to avoid long semicolon chains. Any suggestions?

view this post on Zulip Enrico Tassi (Feb 18 2022 at 22:41):

Other than the book you probably remember, there is some teaching material here: https://math-comp.github.io/

view this post on Zulip Darij Grinberg (Feb 18 2022 at 23:07):

yeah I remember that book :) but I was hoping for something more hands-on, something like a particularly low-tech proof of e.g. quadratic reciprocity with comments explaining the tactics and notations used as they arise

view this post on Zulip Darij Grinberg (Feb 18 2022 at 23:08):

the book is on my mental desk already

view this post on Zulip Darij Grinberg (Feb 18 2022 at 23:13):

hmm this looks like a good start https://github.com/coq-community/coq-100-theorems/blob/master/ballot.v

view this post on Zulip Sam van G (Feb 19 2022 at 08:02):

I would also be interested in such suggestions, and I was asking a similar question here yesterday while working on the Getting Started wiki page. @Darij Grinberg did you find some examples that were helpful?

view this post on Zulip Darij Grinberg (Feb 19 2022 at 09:18):

trying out ballot.v for now, will let you know if I finish it without much confusion

view this post on Zulip Anders Larsson (Feb 19 2022 at 11:24):

Maybe too 'deep', but I find https://madiot.fr/coq100/ to be a reasonable way to find real math problems solved in Coq.


Last updated: Feb 01 2023 at 12:30 UTC