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. 
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.
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.
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.
What do you mean the IDE is slow?
I am curious, did you make benchmarking/profiling? How much does it take to execute an average tactic for example.
I guess I am curious if this is a problem of the prover itself (Coq or Isabelle) or the tool to write proofs (i.e. Coq IDE or jEdit).
I was refering to Isabelle/jEdit. It had a considerable lag when typing code. The keys sometimes only appeared after ~ 1/8 - 1/4 sec on the screen. You can probably immagine that this is not nice when writing (usually verbose) proof scripts…
I also tried some other methods, like running Isabelle/jEdit on a powerful server with X-forwarding. I think the performance was a bit better then.
Note that this was already more than a year ago, and I only worked for ~ one semester. Things could have changed by now…
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.
AFAIK, Isabelle (used to) support that as well, you just had to avoid Isar and write “non-declarative” proofs. I’d be surprised if that stopped being possible.
Re IDE performance, I can believe that you suffered such a performance bug, but I’d be surprised if that were common and due to the editor. jEdit was snappy in 2002 and is still snappy now (just downloaded on Mac; it does seem a bit abandoned). Either the Isabelle plugin has a performance bug, or there was a setup problem on Java/Linux (say, missing hardware acceleration for video) (not that this is the right forum).
I’ve never had issues with Isabelle or jEdit. I’m surprised people don’t think is fast enough.
Is Coq supposed to be faster than Isabelle (ignoring the ide)?
IMHO I’d expect the opposite, but I don’t actually know. Historically, Isabelle has more automation, and part of the reason is that its automation can execute faster. OTOH, Coq has a more expressive logic and type system — try writing an Isabelle type for the elements of an n-dimensional vector space.
what do you mean by expressive?
Thanks for your comments.