C-CoRN

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.

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
  • Vincent Semeria
• Coq-community maintainer(s):
  • Bas Spitters (@spitters)
  • Vincent Semeria (@vincentse)
  • Xia Li-yao (@Lysxia)
• License: GNU General Public License v2
• Compatible Coq versions: Coq 8.18 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

• Coq namespace: CoRN
• Related publication(s):
  • See this page for the list of publications

Building and installation instructions

The easiest way to install the latest released version of C-CoRN is via OPAM:

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

To instead build and install manually, you have to start with the bignums dependency:

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

The last make install is necessary, it copies bignums to a common folder, which is usually coq/user-contrib. Afterwards the similar commands for math-classes will find bignums there. Finally build corn itself:

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

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.