The Coq mailing list

[John Wiegley <johnw AT newartisans.com>]

>>>>> Hugo Herbelin 
>>>>> <Hugo.Herbelin AT inria.fr>
>>>>>  writes:

> 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?

I think "Search" in ssreflect can be emulated using SearchAbout, SearchIsos,
SearchRewrite, etc. I like that Search brings them together into one command,
which I've bound in Proof General to C-a C-s C-s. For example:

    (_ = _)                theorems that result in an equality
    _ (_ = _)              resulting in, or making use of, equality
    "eq" (_ = _)           " " " with eq in the name

I've been using Search for long enough now, I can't comment anymore on whether
standard Coq can do these searches just as easily or not...

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

It's wonderful because of how versatile it is.  Some examples, from real code:

  rewrite [(z; H)]lock /range_ltn map_comp (last_map rend) /= last_map -lock 
/=.
  rewrite -subn1 -addnBA // leq_plus //.
  rewrite ![LHS]andbA and_swap !andbA andbC -!andbA
  rewrite [all]lock -{1}lock /= -lock IHys /= -!andbA.

I find myself using rewrite quite often, and the many forms of it made
possible by ssreflect feel very natural and fluid.

> - strictly speaking, a formalisation methodology: small scale
>   reflection, and in particular the reflection of decidable
>   propositions to bool

Using ssreflect convinced me to use computable bool predicates wherever
possible, avoiding Prop if unnecessary, and using reflection to move between
the two as necessary. The only instance of `reflect` I needed to prove myself
was:

  reflect (List.Forall a s) (all a s).

(In order to work with the StronglySorted type from the Coq stdlib).

> - 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)

I don't use MathComp, but I do use seq, fintype, ssrnat, and ssrfun quite a
bit. The ssreflect "way" convinced me to use a concept of vectors not based on
constructors, for example, which made some proofs I was having difficulty with
much simpler. I was later told about n-tuple's in MathComp, but haven't moved
over to them yet.

For example, the Fin type in Coq's stdlib gave me all sorts of problems when I
tried to use it extensively, whereas ssreflect's Ordinal (which simply pairs a
nat with a predicate) has been far easier, both in proof, and in code where I
mainly care about the number.

> - 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.

I'm not sure I have many precise examples to give off-hand. The code I'm
thinking of as I write this has changed so significantly since switching to
ssreflect, it's hard to argue that the increase in ease is due solely to that
one choice. It could also have been due to improvements in thinking induced by
studying the ssreflect methodology.

Whatever the reason, I remember -- as a new Coq user -- feeling like I was
swimming through molasses before I met ssreflect, and then after it became
simply water: still needing effort and patience, but not too much.

Lastly, I pretty much ignored context management before ssreflect, relying on
generated names and having my proofs break constantly. ssreflect makes such
management a primary task, and gives very convenient tools for doing so, which
cured that particular problem. It may simply be little things like this, and
changes in perspective, which have led to this general impression.

John