Is it worthwhile to learn and/or primarily use SSReflect's tactics and proof style as opposed to "vanilla" Coq? (Assuming, of course, I don't plan to contribute to a library like mathcomp that uses SSReflect itself.)
(The SSReflect docs say there's a lot of overlap between its tactics and the default ones, which makes me wonder how relevant the distinction is nowadays.)
the main reason to go with SSReflect in my mind is if you like a rewriting-heavy proof style and lower-level manipulation of hypotheses/proof context. These days, one can just as well go with vanilla Coq proofs and automation like CoqHammer (
sauto tactic), which can completely obviate using manual rewriting and manipulation of the proof context.
the automation-heavy style is really successful in the HOL world (Isabelle, HOL4, HOL Light), but probably not well suited to when definitions make heavy use dependent types. I would say SSR can work both with minimal dependent types and moderately many dependent types. On the other hand, I'm not sure SSR is suited to Agda style stuff where type dependencies are all over the place.
the other gain from SSR is that proof scripts tend to be much more maintainable down the line (by a "fail first" approach when definitions and tactics change). SSR-based projects are my favorite to port to recent Coq, while vanilla Ltac ones can take ages. On the other hand, writing fully idiomatic SSReflect is very time-consuming to most people, and the jury is out whether non-idiomatic SSR offers benefits over vanilla Ltac in the long run.
Thank you for the detailed reply!
we have a section on proof languages in our survey which has some more details: https://arxiv.org/pdf/2003.06458.pdf#page=51 (and it also has pointers to SSReflect papers and the like)
Without having tried
sauto, from ssreflect I enjoy views and the more powerful rewrite tactic. Also, ssreflect tactics use evarconv unification instead of the more restricted tactic unification. ssreflect tactics let you write proof scripts that are clearer because more concise — one ssreflect proof step can encode several “vanilla steps”, and many of those turn into special characters (let’s call them “line noise”) — but those steps are often distracting details. Finally, unlike vanilla tactics, the interface to ssreflect has a consistent design.
OTOH, ssreflect doesn’t seem designed for very syntactic proofs (especially large induction) — it’s still useful, but for a 10-branch induction I’ll stick to Coq’s
induction over ssreflect’s
well, I skipped talking about views since I think they mostly make sense when fully committed to MathComp
reflect don’t require that, I guess?
sure, I guess you can use
reflect anyway, but then it would feel weird to not go all-in on
ssrbool and friends
guess I should learn that, I’ve recently used
reflect because colleagues used it and it seemed beneficial
(for extra “fun” we also use std++, and they picked Coq’s other boolean coercion.)
so I guess one way to view SSR is also that it makes FOL-oriented boolean reasoning practical "again", e.g., bi-implication becomes non-painful to use (an explicit "HOL layer" in Coq). As I said in some other topic, better to do it this way than to mix
Prop idioms with
bool haphazardly. Unfortunately, the combination of
sauto with reflect and SSR is still non-viable for some technical reasons.
[commercial disclaimer] you may be interested into this (almost finished) book https://github.com/math-comp/mcb (if you can, compile the sources).
I agree with what was said here about the SSR proof language. I just want to add that even if you don't need abstract algebra for your formalization, I'm pretty sure that discrete stiff like lists and finite types can come handy (it's the coq-mathcomp-ssreflect package). Last, there are some formalization techniques, like the one we call "inductive specifications" in the book (you may see them as inversion lemmas expressed as inductive relations) that can be handy in any context. So, even if you end up not using SSR, I still think you may learn a few tricks by looking at it and mathcomp.
We did our best to explain these tricks in the book, one can hardly figure these out by just looking at the proof language alone.
note to admins: this topic belongs in "Coq users" (proof language choice is a user FAQ item)
This topic was moved here from #Miscellaneous > To SSReflect or to not SSReflect? by Théo Zimmermann
For someone like me, who is mostly interested in finite structures (graphs, automata, etc.) and their properties the main motivation for using
mathcomp is indeed not the tactic language but the
ssreflect component of the library . You have lists, finite types, finite sets, "big" operators, and a large variety of constructions on them (e.g., rotating a cycle to a specific point and/or splitting it into two "arcs"). All these things can be defined easily, but getting them right (such that they are really usable) is far from trivial. That is not to say that the tactic language isn't nice too. My personal favorites are tactics like
without loss that allow making symmetry arguments so concise that it is actually worthwhile to do them. I can't say how this compares with std++, as I'm not using the latter.
Last updated: Sep 26 2023 at 11:01 UTC