Awesome

Coqtail

Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis.

Meta

• Author(s):
  • Guillaume Allais
  • Sylvain Dailler
  • Hugo Férée
  • Jean-Marie Madiot
  • Pierre-Marie Pédrot
  • Amaury Pouly
• Coq-community maintainer(s):
  • Jean-Marie Madiot (@jmadiot)
• License: GNU Lesser General Public License v3.0 only
• Compatible Coq versions: 8.17 or later
• Additional dependencies: none
• Coq namespace: Coqtail
• Related publication(s): none

Building and installation instructions

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

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

To instead build and install manually, do:

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

Coqtail and Vim

Note that this project is distinct from this other project named Coqtail, which helps using Coq in Vim.

Developer's todo list

Big things:

• prove linear and non-linear theory of ℂ is decidable (using Groebner basis)

Lemmas to prove:

• Mertens' Theorem for Complex numbers
• (expand this list to your wish)

Maintenance:

• Use -Q instead of -R and fix the resulting loadpath problems
• Check for commented lemmas (and admits)
• Remove useless Requires
• Check for admits (run ./todos.sh).
• Check for commented results (run ./todos.sh comments)