Project Awesome project awesome
♥

Type Theory and Mathematics > CoRN

Library of constructive real analysis and algebra.

Package 115 stars GitHub

C-CoRN

Docker CI Contributing Code of Conduct Zulip

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):
  • License: GNU General Public License v2
  • Compatible Coq versions: Coq 8.19 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):

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.

Back to Coq