The Coq Proof Assistant

The Mathematical Components Team, at the Microsoft Research-Inria Joint Center released a new version of Ssreflect, an powerful extension for Coq. For more information, read the official announcement:

«
We are pleased to announce the new release of the Ssreflect
extension library for the Coq proof assistant, version
8.2/8.2pl1. This release includes:
- an update of the tactic language which complies with the new version
of Coq;
- an update of the combinatoric libraries distributed in the previous
release of ssreflect;
- a new set of libraries for abstract algebra.

The name Ssreflect stands for "small scale reflection", a style of
proof that evolved from the computer-checked proof of the Four Colour
Theorem and which leverages the higher-order nature of Coq's
underlying logic to provide effective automation for many small,
clerical proof steps. This is often accomplished by restating
("reflecting") problems in a more concrete form, hence the name. For
example, in the Ssreflect library arithmetic comparison is not an
abstract predicate, but a function computing a boolean.

Along with documentation, also available at
https://hal.inria.fr/inria-00258384 the Ssreflect distribution
comprises two parts:
- A new tactic language, which promotes more structured, concise and
robust proof scripts, and is in fact independent from the "reflection"
proof style. It is implemented as a linkable extension to the Coq
system.
- A set of Coq libraries that provide core "reflection-oriented"
theories for
+ basic combinatorics: arithmetic, lists, graphs, and finite sets.
+ abstract algebra: an algebraic hierarchy from
additive groups to closed fields, polynomials, matrix,
basic finite group theory, infrastructure for finite summations,...)

Some features of the tactic language:
- It provides tacticals for most structural steps (e.g., moving
assumptions), so that script steps mostly match logical steps.
- It provides tactics and tatical to support structured layout,
including reordering subgoals and supporting "without loss of
generality" arguments.
- It provides a powerful rewriting tactic that supports chained
rules, automatic unfolding of definitions and conditional rewriting,
as well as precise control over where and how much rewriting occurs.
- It can be used in combination with the classic Coq tactic language.

Some features of the library:
- Exploits advanced features of Coq such as coercions and canonical
projections to build generic theories (e.g., for decidable equality).
- Uses rewrite rules and dependent predicate families to state
lemmas that can be applied deeply and bidirectionally. This means
fewer structural steps and a smaller library, respectively.
- Uses boolean functions to represent sets (i.e., comprehensions),
rather than an ad hoc set algebra.

The Ssreflect 1.2 distribution is available at
http://www.msr-inria.inria.fr/projects/mathematical-components-2/
It is distributed under either one (your choice) of the CeCILL-B or CeCILL
version 2 licences (the French equivalent of the BSD and GNU GPL licenses,
respectively).

The tactic language is quite stable; we have been using it
internally for three years essentially without change. We will support
new releases of Coq in due course. We also plan to extend the core
library as our more advanced work on general and linear algebra
progresses.

Comments and bug reports are of course most welcome, and can be
directed at ssreflect(at-sign)msr-inria.inria.fr. To subscribe, either
send an email to sympa@msr-inria.inria.fr, whose title contains the
word ssreflect, or use the following web interface:
https://sympa.inria.fr/sympa/info/ssreflect

Enjoy!

The Mathematical Components Team, at the Microsoft Research-Inria
Joint Center
»