Announcing Ssreflect version 1.2

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.

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
example, in the Ssreflect library arithmetic comparison is not an
abstract predicate, but a function computing a boolean.

Along with documentation, also available at the Ssreflect distribution
comprises two parts:
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:
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,
- 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
- 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.
rather than an ad hoc set algebra.

The Ssreflect 1.2 distribution is available at
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,

The tactic language is quite stable; we have been using it
internally for three years essentially without change. We will support
library as our more advanced work on general and linear algebra

directed at ssreflect(at-sign) To subscribe, either
send an email to, whose title contains the
word ssreflect, or use the following web interface:


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