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 ... [More] 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 [email protected], 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 » [Less]

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 ... [More] 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. read more [Less]

A new patch level for Coq 8.2 is now available. You can get it from the download page.

A new patch level for Coq 8.2 is now available. You can get it from the download page.

A new patch level for Coq 8.2 is now available. You can get it from the download page.

Thomas Braibant and Damien Pous are pleased to announce the first release of ATBR, a Coq library whose aim is to provide tools for working with various algebraic structures, including non-commutative idempotent semirings and Kleene algebras. The ... [More] main tactic they provide in this library is a reflexive tactic for solving (in)equations in Kleene algebras. The decision procedure goes through standard finite automata constructions, that they formalized. For example, this tactic automatically solves goals of the form a#*(b+a#*(1+c))# == (a+b+c)# or a*b*c*a*b*c*a# <= a#*(b*c+a)#, where a, b, and c are elements of an arbitrary Kleene algebra (binary relations, regular languages, min-max expressions...), # is the (postfix) star operation, * is the infix product or concatenation operation, + is the sum or union operation, and 1 is the neutral element for *. In order to define this tactic, they had to work with matrices, so that the ATBR library also contains a new formalisation of matrices in Coq along with a set of tools (notably, "ring"-like tactic for matrices whose dimensions are not necessarily uniform). More details can be found from Coq user contribution web-page In particular, a Coq file illustrating the kind of tools we provide can be found there. [Less]

Thomas Braibant and Damien Pous are pleased to announce the first release of ATBR, a Coq library whose aim is to provide tools for working with various algebraic structures, including non-commutative idempotent semirings and Kleene algebras. The ... [More] main tactic they provide in this library is a reflexive tactic for solving (in)equations in Kleene algebras. The decision procedure goes through standard finite automata constructions, that they formalized. For example, this tactic automatically solves goals of the form a#*(b+a#*(1+c))# == (a+b+c)# or a*b*c*a*b*c*a# <= a#*(b*c+a)#, where a, b, and c are elements of an arbitrary Kleene algebra (binary relations, regular languages, min-max expressions...), # is the (postfix) star operation, * is the infix product or concatenation operation, + is the sum or union operation, and 1 is the neutral element for *. In order to define this tactic, they had to work with matrices, so that the ATBR library also contains a new formalisation of matrices in Coq along with a set of tools (notably, "ring"-like tactic for matrices whose dimensions are not necessarily uniform). More details can be found from Coq user contribution web-page In particular, a Coq file illustrating the kind of tools we provide can be found there. [Less]

Thomas Braibant and Damien Pous are pleased to announce the first release of ATBR, a Coq library whose aim is to provide tools for working with various algebraic structures, including non-commutative idempotent semirings and Kleene algebras. The ... [More] main tactic they provide in this library is a reflexive tactic for solving (in)equations in Kleene algebras. The decision procedure goes through standard finite automata constructions, that they formalized. For example, this tactic automatically solves goals of the form a#*(b+a#*(1+c))# == (a+b+c)# or a*b*c*a*b*c*a# <= a#*(b*c+a)#, where a, b, and c are elements of an arbitrary Kleene algebra (binary relations, regular languages, min-max expressions...), # is the (postfix) star operation, * is the infix product or concatenation operation, + is the sum or union operation, and 1 is the neutral element for *. In order to define this tactic, they had to work with matrices, so that the ATBR library also contains a new formalisation of matrices in Coq along with a set of tools (notably, "ring"-like tactic for matrices whose dimensions are not necessarily uniform). More details can be found from Coq user contribution web-page In particular, a Coq file illustrating the kind of tools we provide can be found there. [Less]

Thomas Braibant and Damien Pous are pleased to announce the first release of ATBR, a Coq library whose aim is to provide tools for working with various algebraic structures, including non-commutative idempotent semirings and Kleene algebras. The main ... [More] tactic they provide in this library is a reflexive tactic for solving (in)equations in Kleene algebras. The decision procedure goes through standard finite automata constructions, that they formalized. read more [Less]

The first Asian-Pacific Coq summer school will be held in China, in the Future Internet Technology Research Center (FIT) of Tsinghua University, from 24th to 30th, august 2009. More information and registration on the Asian-Pacific Coq summer school web page.