/usr/share/doc/libssreflect-coq/ANNOUNCE is in libssreflect-coq 1.5-3build1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 | Announcing Ssreflect version 1.5
We are pleased to announce the new release of the Ssreflect extension
for the Coq proof assistant. This release includes an update of the
tactic language and a minimized set of libraries. The user interested in
the extensive Mathematical Components library has to install it as a
separate package.
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 [1], 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 booleans, natural numbers, lists and finite types.
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.
The Ssreflect 1.5 distribution is available at [2]. It is distributed
under the CeCILL-B licence (the French equivalent of the BSD license).
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 at [3].
Enjoy!
The Mathematical Components Team, at the Microsoft Research-Inria
Joint Center
[1] : http://hal.inria.fr/inria-00258384
[2] : http://www.msr-inria.inria.fr/Projects/math-components
[3] : https://www.msr-inria.inria.fr/sympa
|