What is the difference between SSReflect and Czar?

I was trying to understand the difference between SSReflect & Cezar/Cesar (declarative proof language for Coq).

based on this comment from the docs:

This chapter describes a set of tactics known as SSReflect originally designed to provide support for the so-called small scale reflection proof methodology.

from that it seems it’s just a different way to define tactics (in some specific style) but not having coq actually be declarative. Is that correct?

Czar was an (aborted) attempt at a declarative proof mode. It never took of and has been removed now.

SSReflect is a proof language (consistent set of tactics) that is very much non-declarative since it provides a lot of shortcuts to manually do many proof management steps.

Note that Czar introduced a separate proof mode (you could not use the usual tactics within it) while SSReflect does not (you can freely mix SSReflect and non-SSReflect tactics).

Finally, let me express my (personal) opinion that Coq does not need a declarative proof mode. You can already use the current proof mode and set of tactics to produce a very declarative proof style, especially by using lots of assert (or SSReflect’s have) combined with lots of automation (e.g. through CoqHammer).

Thanks for the reply!

Why don’t you think Coq requires a declarative proof language? Isn’t it the case that most people don’t make their Coq proofs easily readable and Proof General is necessary to understand them or see the general shape of the proofs?

My point is that most of the tools for writing readable and declarative proofs are already there, but you are right that the standard proof style is still very non-declarative and non-readable. With Isar, Isabelle managed to have a real cultural shift where everybody started writing (or rewriting) proofs in declarative style. So the question to me is more: what will it take to see a similar cultural shift in Coq?

Hi! Some time ago, I took a course on Isabelle/HOL and also worked on a small project there. My (little) experience with Isabelle made me feel that the declaritive (‘Isar’) style was a bit easier to write and read Isabelle proofs, compared to the tactical proofs. It was easier to write because I didn’t understand the Isabelle tactics very well (which work quite differently from Coq). However, my impression was that the code was extremely verbose. Some steps that would have been very simple in Coq often required to copy’n’paste hypotheses or conclusions again and again; I often missed the ‘direct control’ you have in Coq using tactics. Together with low performance of Isabelle’s IDE it was actually quite painful to write proofs in Isar. I’m very glad to be using Coq again. :slight_smile:

Maybe there will be a shift when it will be actually easier to write and understand and maintain Coq proofs in this style, e.g. for undergraduate students, or for researchers trying to formalse mathematics? Also note that Isar still allows mixing declarative and tactical style proofs, which probably made the shift easier.

2 Likes

Yes! Worse than that, in many cases that duplication is fragile and redundant with the definitions. Maybe that’s fine in a textbook on old maths, but when I use Coq definitions change.

Is that a problem? Proofs on paper leave out lots of details. If some step is important, you can describe it via lemmas or text. “Use smaller lemmas” seems common across different proof-engineering styles, from Chlipala to (my supervisor) Robbert Krebbers (who harks back to Gonthier’s style IIUC). I guess that’s not appropriate for all proofs, but I think that suffices for the majority, especially in CS-ish proofs.

1 Like

BTW I’m not arguing it’s never a problem, but that it’s not obviously a problem—making proofs readable without tool supports seems an especially questionable goal to optimize for. And some of the actual issues might be best fixed by better tool support, tho probably not in the near future.

BTW, I do find the verbosity of the usual style a problem. “Conventional” proof scripts are unreadable because they spend too much text on low-level book-keeping. While there’s a learning curve, advanced intropatterns, stdpp tactics and ssreflect, together with tool support in navigation, make IMHO the high-level structure of a proof much more visible.