walker (Oct 09 2022 at 14:34): 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 ?
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.
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
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.
Théo Zimmermann (Oct 09 2022 at 16:41):When was the last time you read the documentation of the standard tactics?
Théo Zimmermann (Oct 09 2022 at 16:42):Just asking because there was a lot of improvements over the last few years.
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.)
walker (Oct 09 2022 at 16:57):/me who just spam eauto everywhere.
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).
Enrico Tassi (Oct 09 2022 at 18:52):walker said:
/me who just spam eauto everywhere.
eauto is not so bad, actually
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: Apr 16 2024 at 07:02 UTC