The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Mario,

did you look into the Coq standard library? E.g. the reals development in the 
Coq standard library, say Ratan.v, contains quite a few non trivial proofs 
and obviously compiles with plain Coq and with 8.10.

Also Flocq has quite a few files with non-trivial proofs which only require 
standard library files. Just an arbitrary example:

https://gitlab.inria.fr/flocq/flocq/blob/master/src/Core/Digits.v

In general I would look into all libraries running in Coq CI, that is look 
into:

https://gitlab.com/coq/coq/pipelines/70069385
https://github.com/coq/coq/tree/master/dev/ci

It should be just a few 10 lines of code to get a rough analysis of require 
statements and on proof length / style (using bullets or not, ...) for a 
given library.

Download paths and versions for all add-ons tested in CI can be found here:
https://github.com/coq/coq/blob/master/dev/ci/ci-basic-overlay.sh

or maybe use the pinned versions from the 8.10 picking PR:
https://github.com/coq/coq/blob/9e9495e37db73e83f356012bd6905a3039b7e923/dev/ci/ci-basic-overlay.sh

I hope this helps - every effort to teach Coq is highly appreciated :-)

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928