Galliblog

The Gallinette blog

Quésaco - SSReflect

By Assia Mahboubi.

On 1 November 2019.

Last updated on 26 November 2019.

  • SSReflect
  • Quésaco

SSReflect, an extension of Coq's tactic language

History

  • 2006 : First version, part of the Coq proof of the Four Colour Theorem
  • 2008 : First standalone release of Ssreflect (v1.1), for Coq v8.1
  • 2009 : First version of the documentation manual
  • 2012 : Completion of the proof of the Odd Order Theorem
  • 2017 : Integration in the standard distribution of Coq
  • today : used in various coq developments, of various nature (analysis, quickchick, elliptic curves, coqcombi, etc.)

Name

SSReflect is coined after "Small Scale Reflection", a formalization methodology making the most of the status of computation in TT.

Ssreflect may thus refer to three different things: a formalization methodology, a tactic language, and a corpus of formalized libraries, based on the former methodology and developped using the latter language. A more appropriate name for the libraries is "Mathematical Components".

In this file, we give a describe the small scale reflection method in a nutshell, so as to illustrate the motivations for some features of the tactic language.

We start by writing proof scripts that do not depend on the ssreflect extension of the tactic language, because the methodology is independent.

Reminder: large scale reflection

An oracle produces these numbers:

We can check this identity using Coq:

Computational proofs on moderate size objects, like in the above example already require thinking a bit about data-structures and complexity.

A reflection-based tactic replace explicit deduction steps, logged in proof terms, with computational steps, checked by the kernel's reduction machine. Reflection uses an inductive type (the "reflected" one) as an abstract, symbolic, data strutcure which can be used to write programs. The tactic checks that these computations can be interpreted as a valid propositional equality on a source type. For instance, the ring tactic reflects a type equipped with a, possibly axiomatic and non-computational, ring structure into a type for polynomial expressions.

Small scale reflection

In this case as well, the central idea is to replace deductive steps by computation. But at a smaller and pervasive scale.

Standard library's definition of <= on natural numbers: an inductive representation of proofs.

A small scale reflection version: a boolean program. For the sake of modularity, we expess it using the pseudo-substraction on natural numbers, combined with a boolean equality test.

Let us compare a proof that 16 <= 64, in both approaches:

Small scale reflection at work:

The same proof with the le definition require an explicit induction step.

Selected basic features of the ssreflect tactic language

From now on, we will use the tactic extension. It is distributed as part of the Coq proof assistant, and loaded by the following Import

The extension implements an improved rewrite tactic language. We mention only two important features:

  • a diferent matching algorithm, rigid on head symbols and using conversion for the internal subterms.
  • a pattern selection mechanism based on this matching.

The extension implements a view mechanism, to combine deductive steps (e.g. using an implication), with bureaucracy ones (e.g. introduction/generalization, case analysis). This is quite useful to manage going back and forth between bool and Prop. Note: bool can be seen as a type reflecting (certain) inhabitants of Prop.

Another strong motivation behind the design choices applied in the ssreflect tactic langage is to ease the maintenance/upkeep of formal libraries. Features associated with this objective are: == fewer tactics: case, apply, elim, rewrite (move) == two main tacticals and many switches == clearing policy for an easier book-keeping == enhanced support for forward chaining: have, suff, wlog

SSReflect is only a stepping stone to build libraries. Demo: Prove that the concatenation (s1 ++ s2) of two lists is duplicate-free if and only if (s2 ++ s2) is also duplicate-free.

Mathematical Components's take:

Lists on an eqType have a boolean membership unary predicate, with a generic infix notation

Now implement uniq: