Skip to content

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. [maintainer=@jmadiot]

License

Notifications You must be signed in to change notification settings

coq-community/coqtail-math

Repository files navigation

Coqtail

Docker CI Contributing Code of Conduct Zulip

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):
  • 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)

About

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. [maintainer=@jmadiot]

Topics

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Contributors 4

  •  
  •  
  •  
  •  

Languages