The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

I'm proud to announce the immediate availability of Ssreflect 1.3 for Coq 8.3.
Updated online documentation for the proof language and the library will 
be available shortly at the URLs mentioned below.

Here the official announcement.

=============================================================================
Announcing Ssreflect version 1.3

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

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
http://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, general linear
    algebra, basic and advanced 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.3 distribution is available at
   http://www.msr-inria.inria.fr/Projects/math-components
It is distributed under the CeCILL-B licence (the French equivalent of 
the BSD license).
    
The tactic language has been extended with several new features, inspired by
the five years of intensive use in our project. However we have kept the core
of the language unchanged; the new library compiles with Ssreflect 1.2.
Users of a Coq 8.2 toplevel statically linked with Ssreflect 1.2 need to
comment the Declare ML Module "ssreflect" line in ssreflect.v to properly
compile the 1.3 library.
We will continue supporting new releases of Coq in due course.

The new library adds general linear algebra (matrix rank, subspaces)
and all of the advanced finite group that was developed in the course of
completing the Local Analysis part of the Odd Order Theorem, starting from
the Sylow and Hall theorems and including full structure theorems for abelian,
extremal and extraspecial groups, and general (modular) linear representation
theory.

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 AT msr-inria.inria.fr,
 whose title contains the
word ssreflect, or use the following web interface:
https://www.msr-inria.inria.fr/sympa


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