I am trying to understand if ssreflect is something I might need to learn,

I checked couple of tutorials, and from what I can see, SSreflect offers different set of tactics than the standard ones. The goal seams to me is to make forward reasoning simpler.

So my question is is there something ssreflect can do that remember/pose cannot do ? in other words is it just syntactic sugar for already existing coq tactics or does it offer certain advantages ?

as I wrote a bit about here one way to view SSReflect is that it's a disciplined way of handling booleans in Coq code, and making the most of Coq's computational machinery for everyday proofs.

However, similar advantages can be obtained by using Coq's typeclass machinery and regular tactics, if you use the `Decision`

typeclass for informative booleans.

another reason to use SSReflect is if you like to do a lot of low-level, controlled reasoning rather than large-scale proof search. The tactics give a compact syntax for controlling the proof context and moving around and applying hypotheses. But there is not really much added expressiveness there, it's more of a *style* than a completely new system

I'd only like to add that the behaviour of the ssr tactics is doumented more carefully than the vanilla ones.

When was the last time you read the documentation of the standard tactics?

Just asking because there was a lot of improvements over the last few years.

(Obviously, if you are referring to the precise behavior of unification, then yes, it is still not really documented.)

/me who just spam eauto everywhere.

I'm referring to https://coq.inria.fr/refman/proofs/writing-proofs/equality.html#coq:tacn.rewrite v.s. https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#coq:tacn.rewrite-(ssreflect) + https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#contextual-patterns

In particular subterm selection is only explained in the latter (in SSR scripts rewrite is typically doing 1/3 of the work, so it is not a detail).

walker said:

/me who just spam eauto everywhere.

eauto is not so bad, actually

An important fact about ssreflect is that it is the tactic language of mathcomp, and mathcomp is a very well designed library.

Last updated: Jun 24 2024 at 01:01 UTC