The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

On Fri, Jul 10, 2015 at 12:34:45PM -0700, John Wiegley wrote:
> >>>>> Emilio Jesús Gallego Arias 
> >>>>> <gallego AT cri.ensmp.fr>
> >>>>>  writes:
> 
> > I have also found quite useful ssreflect's
> >
> > "set f := pattern"
> >
> > tactic to find out types of tricky sub-expressions; the matching mechanism
> > usually works well for my full-of-holes patterns.
> 
> I would like to second this, and the use of ssreflect in general -- even if
> you stick to standard Coq libraries and tactics, it can still be used to
> simplify your code with its wonderful rewriting tactic, identification of
> subexpressions with set, destructuring "let:", and its improved Search
> capability.

It is a pleasure to read such an enthousiasm, and indeed, there were a
number of very interesting new ideas in the ssreflect package, some of
them having be inspiring for standard Coq.

Are you however really sure that the "Search" and the "let:" in the
ssreflect package behave essentially differently from the "Search" and
the "let '" in current standard Coq?

As for "rewrite", the swiss-knife style of its variant in the
ssreflect package is certainly appealing and, contrastingly, the
heterogeneity of behaviors of the various "rewrite" in standard Coq as
well as the absence of contextual patterns is a pity. I hope this can
eventually be solved (even though a big obstacle here is the
compatibility constraint). Conversely, I find it a pity that there
were no care taken in the design of the syntax of the tactics from the
ssreflect package to be consistent with the syntax style of Coq.

In any case, I'm curious to know what you exactly intend by "wonderful"!

> After switching all of my code to use ssreflect's libraries and tactics, I
> find that many scenarios which were complex or laborious before have become
> much simpler to reason about.

What is commonly called "ssreflect" actually covers at least three
different things:

- strictly speaking, a formalisation methodology: small scale
  reflection, and in particular the reflection of decidable
  propositions to bool
- an extensive library based on this methodology and intensively using
  a number of Coq features such as canonical structures for type
  inference (more appropriately called nowadays "MathComp" library)
- a set of tactics incorporating a number of "cool" original features

Would you be kind to clarify for each of these points how they
contribute to have "many scenarios which were complex or laborious
before have become much simpler to reason about"? I think this would
be of interest for the list.

Thanks in advance,

Hugo Herbelin