Tools

Pierre Letouzey edited this page Oct 12, 2017 · 89 revisions
Clone this wiki locally

Some of the tools listed here are part of bigger projects that support other proof assistants/theorem provers. Another list of Coq-related tools can be found at https://coq.inria.fr/related-tools.

Interface for Editing Proofs

  • CoqIDE

    The graphical user interface distributed with Coq.

  • ProofGeneral

    ProofGeneral is a generic interface for proof assistants, based on the customizable text editor Emacs.

  • Coqoon

    Eclipse plugin for Coq development (based on Wenzel's asynchronous PIDE framework).

  • Coq PIDE

    Jedit (proof of concept) plugin for Coq development by Carst Tankink (also based on asynchronous PIDE framework).

  • GeoProof

    GeoProof is a dynamic geometry software, with can communicate with CoqIDE to build the formula corresponding to a geometry figure interactively.

  • Papuq

    Papuq is patched version of CoqIde with teaching oriented features.

  • tmEgg

    Coq plugin for TeXmacs

  • ProofWeb

    An online web interface for Coq (and other proof assistants), with a focus on teaching.

  • ProverEditor

    An experimental Eclipse plugin with support for Coq.

Discontinued interfaces

  • PCoq (for versions of Coq in old syntax, version 7.4 of 2003 and before)

    A graphical user interface for Coq. The environment provides ways to edit structurally formulas and commands, new notations can easily be added. It allows proof by pointing.

  • TmCoq

    TmCoq integrates Coq within TeXmacs.

Interface for Browsing Proofs

  • Helm is a browsable and searchable (using the Whelp tool) repository of formal mathematics (includes the Coq User Contributions).

Presenting Proofs

Tactics packages

  • Micromega: solves linear (Fourier-Motzkin) and non linear (Sum-of-Square's algorithm) systems of polynomial inequations; also provides a (partial) replacement for the Coq's omega tactic.
  • Ssreflect facilitates proof by small scale reflection, "a style of proof that ... provide[s] effective automation for many small, clerical proof steps. This is often accomplished by restating ("reflecting") problems in a more concrete form ... For example, in the Ssreflect library arithmetic comparison is not an abstract predicate, but a function computing a boolean. (source)"
  • AAC_tactics provides tactics that facilitates the rewriting of universal equations,modulo associative and possibly commutative operators, and modulo neutral elements (units).

Packaging extracted code

  • Z_interface An approach for deriving directly standalone programs from extracted code.