Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the formalization of programming languages semantics (e.g. the CompCert compiler certification project or Java Card EAL7 certification in industrial context), the formalization of mathematics (e.g. the full formalization of the 4 color theorem or constructive mathematics at Nijmegen) and teaching.
Coq implements a program specification and mathematical higher-level language called Gallina that is based on an expressive formal language called the Calculus of Inductive Constructions that itself combines both a higher-order logic and a richly-typed functional programming language. Through a vernacular language of commands, Coq allows:
to define functions or predicates, that can be evaluated efficiently;
to state mathematical theorems and software specifications;
to interactively develop formal proofs of these theorems;
to machine-check these proofs by a relatively small certification "kernel";
to extract certified programs to languages like Objective Caml, Haskell or Scheme.
As a proof development system, Coq provides interactive proof methods, decision and semi-decision algorithms, and a tactic language for letting the user define its own proof methods. Connection with external computer algebra system or theorem provers is available.
As a platform for the formalization of mathematics or the development of programs, Coq provides support for high-level notations, implicit contents and various other useful kinds of macros.
Coq comes with libraries for efficient arithmetics in N, Z and Q, libraries about lists, finite sets and finite maps, libraries on abstract sets, relations, classical analysis, etc.
Coq is released with:
a graphical user interface based on gtk (CoqIde) (see screenshots),
documentation tools (coqdoc and coq-tex) and a statistics tool (coqwc),
dependency and makefile generation tools for Coq (coq_makefile and coqdep),
a stand-alone proof verifier (coqchk, from Coq 8.2).
The current version: Coq 8.4pl3
This version features:
a new modular and uniform extension of the arithmetical libraries by P. Letouzey which systematically provides power, gcd/lcm, square root, base 2 logarithm, division, modulo, bitwise operators, logical shift, comparisons, iterators for all of nat, N, Z, BigN and BigZ on top of a uniform naming layer (e.g. plus and mult are now consistently named add and mul while still remaining mostly compatible with 8.3) (example 1, example 2, example 3);
a new proof engine by A. Spiwack whose most salient feature is the introduction of bullets (+, -, *) and structured scripts ({ ... }) (example).
The main other changes are:
addition of eta-conversion to the logic;
a slightly more flexible guard condition for fixpoints;
a more systematic support for pattern-matching on dependent types;
more robust CoqIDE (including a new communication protocol by V. Gross);
a new library of vectors (lists of a given length);
support for referring to expressions of the goal using pattern in tactics;
automatic computation of occurrences to abstract over in destruct/induction (example);
various improvements to Ltac (timeout, appcontext, constr_eq, is_evar, has_evar, generic match _ with _ => _ end pattern, fine-tuning of simpl);
implicit arguments in anonymous functions;
notations with binders (e.g. exists x y z : A, P x y z) (example);
many bug fixes and improvements of existing features (type classes, setoid rewriting, ring, nsatz, micromega, extraction, Function, module system, coq_makefile, ...);
For a full log of changes, see the file CHANGES.
Coq 8.4 is not entirely upward compatible with 8.3 (see main incompatibilities)
Sources
coq-8.4pl3.tar.gz
4 MB
Binaries
MacOS
coq-8.4.dmg
75 MB
coqide-8.4pl2.dmg (Coq bundled with CoqIDE interface)
100 MB
The packages require MacOS ≥ 10.5
Documentation
Tutorial.pdf
0.2 MB
Reference-Manual.pdf
1.5 MB
0 commenti:
Post a Comment