Stream: Coq users

Topic: what is SSReflect about?


view this post on Zulip walker (Oct 09 2022 at 14:34):

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 ?

view this post on Zulip Karl Palmskog (Oct 09 2022 at 15:30):

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.

view this post on Zulip Karl Palmskog (Oct 09 2022 at 15:32):

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

view this post on Zulip Enrico Tassi (Oct 09 2022 at 15:57):

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

view this post on Zulip Théo Zimmermann (Oct 09 2022 at 16:41):

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

view this post on Zulip Théo Zimmermann (Oct 09 2022 at 16:42):

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

view this post on Zulip Théo Zimmermann (Oct 09 2022 at 16:42):

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

view this post on Zulip walker (Oct 09 2022 at 16:57):

/me who just spam eauto everywhere.

view this post on Zulip Enrico Tassi (Oct 09 2022 at 18:47):

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

view this post on Zulip Enrico Tassi (Oct 09 2022 at 18:52):

walker said:

/me who just spam eauto everywhere.

eauto is not so bad, actually

view this post on Zulip Michael Soegtrop (Oct 10 2022 at 07:35):

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


Last updated: Feb 09 2023 at 00:03 UTC