The Coq Proof Assistant

The Microsoft Research-Inria Joint Center is pleased to announce
the first full release of the Ssreflect extension library for the Coq
proof assistant, version 8.1.

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 (roughly: arithmetic, lists, and
finite sets).

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 tactical 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 an 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.1 distribution is available at
http://www.msr-inria.inria.fr/projects/mathematical-components-2/. It is
distributed under the CeCill-B license (the French equivalent of the
BSD license).

The tactic language is quite stable; we have been using it
internally for two 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