Darij Grinberg (Feb 18 2022 at 22:10): 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?
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/
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
Darij Grinberg (Feb 18 2022 at 23:08):the book is on my mental desk already
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
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?
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
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: Sep 30 2023 at 06:01 UTC