Stream: Coq users

Topic: To SSReflect or to not SSReflect?

Joshua Grosso (Sep 28 2020 at 20:51):

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

Karl Palmskog (Sep 28 2020 at 21:15):

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.

Karl Palmskog (Sep 28 2020 at 21:17):

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.

Karl Palmskog (Sep 28 2020 at 21:20):

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.

Joshua Grosso (Sep 28 2020 at 21:30):

Thank you for the detailed reply!

Karl Palmskog (Sep 28 2020 at 21:31):

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)

Paolo Giarrusso (Sep 28 2020 at 21:42):

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.

Paolo Giarrusso (Sep 28 2020 at 21:44):

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

Karl Palmskog (Sep 28 2020 at 21:45):

well, I skipped talking about views since I think they mostly make sense when fully committed to MathComp

Paolo Giarrusso (Sep 28 2020 at 21:46):

bi-implications and reflect don’t require that, I guess?

Karl Palmskog (Sep 28 2020 at 21:47):

sure, I guess you can use reflect anyway, but then it would feel weird to not go all-in on ssrbool and friends

Paolo Giarrusso (Sep 28 2020 at 21:48):

guess I should learn that, I’ve recently used reflect because colleagues used it and it seemed beneficial

Paolo Giarrusso (Sep 28 2020 at 21:50):

(for extra “fun” we also use std++, and they picked Coq’s other boolean coercion.)

Karl Palmskog (Sep 28 2020 at 21:58):

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.

Enrico Tassi (Sep 29 2020 at 08:09):

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

Karl Palmskog (Sep 30 2020 at 22:59):

note to admins: this topic belongs in "Coq users" (proof language choice is a user FAQ item)

Notification Bot (Oct 01 2020 at 07:11):

This topic was moved here from #Miscellaneous > To SSReflect or to not SSReflect? by Théo Zimmermann

Christian Doczkal (Oct 02 2020 at 11:51):

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: Apr 16 2024 at 04:02 UTC