C-CoRN

The Coq Constructive Repository at Nijmegen.

Meta

• Author(s):
  • Evgeny Makarov
  • Robbert Krebbers
  • Eelis van der Weegen
  • Bas Spitters
  • Jelle Herold
  • Russell O'Connor
  • Cezary Kaliszyk
  • Dan Synek
  • Luís Cruz-Filipe
  • Milad Niqui
  • Iris Loeb
  • Herman Geuvers
  • Randy Pollack
  • Freek Wiedijk
  • Jan Zwanenburg
  • Dimitri Hendriks
  • Henk Barendregt
  • Mariusz Giero
  • Rik van Ginneken
  • Dimitri Hendriks
  • Sébastien Hinderer
  • Bart Kirkels
  • Pierre Letouzey
  • Lionel Mamane
  • Nickolay Shmyrev
• Coq-community maintainer(s):
  • Bas Spitters (@spitters)
• License: GNU General Public License v2
• Compatible Coq versions: Coq 8.6 or greater
• Additional dependencies:

  • Math-Classes 8.8.1 or greater, which is a library of abstract interfaces for mathematical structures that is heavily based on Coq's type classes.

  • Bignums

Building and installation instructions

The easiest way to install the latest released version is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-corn

To instead build and install manually, do:

git clone https://github.com/coq-community/corn
cd corn
./configure.sh
make   # or make -j <number-of-cores-on-your-machine>
make install

After installation, the included modules are available under the CoRN namespace.

Building C-CoRN with SCons

C-CoRN supports building with SCons. SCons is a modern Python-based Make-replacement.

To build C-CoRN with SCons run scons to build the whole library, or scons some/module.vo to just build some/module.vo (and its dependencies).

In addition to common Make options like -j N and -k, SCons supports some useful options of its own, such as --debug=time, which displays the time spent executing individual build commands.

scons -c replaces Make clean

For more information, see the SCons documentation.

Building documentation

To build CoqDoc documentation, say scons coqdoc.

Description of the repository

CoRN includes the following parts:

• Algebraic Hierarchy

  An axiomatic formalization of the most common algebraic structures, including setoids, monoids, groups, rings, fields, ordered fields, rings of polynomials, real and complex numbers

• Model of the Real Numbers

  Construction of a concrete real number structure satisfying the previously defined axioms

• Fundamental Theorem of Algebra

  A proof that every non-constant polynomial on the complex plane has at least one root

• Real Calculus

  A collection of elementary results on real analysis, including continuity, differentiability, integration, Taylor's theorem and the Fundamental Theorem of Calculus

• Exact Real Computation

  Fast verified computation inside Coq. This includes: real numbers, functions, integrals, graphs of functions, differential equations.