10
$\begingroup$

Isabelle has the frontend Isar which mimics some features of the Mizar system.

I'm curious if Coq has anything similar, i.e. an alternative to tactic scripts that's designed to be readable or similar to the mathematical vernacular.

This discussion on the Coq forums mentions Czar and SSReflect.

$\endgroup$
1
  • 2
    $\begingroup$ Yeah, Corbineau wrote Czar as documented in his paper, A Declarative Language For The Coq Proof Assistant. It fell into disuse, and was removed in Coq 8.7. I was disappointed to see its departure. Since then, there hasn't been an adequate replacement. $\endgroup$ Feb 15 at 3:40

1 Answer 1

11
$\begingroup$

There indeed used to be a "declarative language for Coq" often referred to as Czar, but it was removed (from Coq's core) a long time ago. If it had had any actual users, it would have been easy at the time to restore it as an external plugin though.

Having tested it when it was still there, my personal impression was that it was actually very difficult to use, and nowhere near what Isar has achieved for Isabelle. My understanding is that one of the main reason why Isar was so successful is thanks to SledgeHammer.

Fortunately today, Coq has CoqHammer (which is even available as part of the Coq Platform). Furthermore, Coq's tactics are pretty flexible for different styles. So, with a combination of tactics such as assert, enough, now_show, and CoqHammer tactics, it is actually possible to reconstruct the Isar style in Coq (no need for a specific proof mode for this).

Another declarative-style set of tactic is provided by the coq-waterproof package (see an example in their README). The proof style looks very much like mathematical text. However, while Czar was suffering from a lack of IDE support (it's almost impossible to remember exactly how to write a "natural language" proof in what is in fact a controlled language), coq-waterproof is a support package for the Waterproof IDE (which is targeted at students). So this might be close to what you are looking for, but for pedagogical purposes. If the goal is to reproduce the Isar style with productivity in mind, then I would still rather recommend relying on Coq's tactics like assert and enough + CoqHammer.

Finally, SSReflect was also mentioned. It is in fact very different from a declarative mode because it is very "procedural". However, the style in which SSReflect users write their proof is supposed to be close to the style of proofs in mathematical texts (one line per significant mathematical step) and reliance on the have: tactic to clarify the most important steps. The main difference between the SSReflect style and the Isar style is that SSReflect only relies on very small-scale automation, making the proofs in SSReflect very robust to evolution in the underlying Coq language, libraries or specifications.

$\endgroup$
4
  • $\begingroup$ I'm not sure I agree with the strategy "assert + CoqHammer $\approx$ Mizar-like input language" being a good idea. It's more a kludge. $\endgroup$ Feb 15 at 18:02
  • 1
    $\begingroup$ Note that I'm comparing to Isar here, not to Mizar. I have no idea what Mizar used to be like, if it was a practical or productive system. But I know that Isar is a productive system in large part thanks to SledgeHammer. $\endgroup$
    – Zimm i48
    Feb 15 at 21:00
  • $\begingroup$ Sorry, when you wrote, "If the goal is to reproduce the Izar style..." it was difficult to tell if you meant Mizar or Isar. But, (a) Mizar is still active and flourishing, and (b) regardless whether you meant Isar or Mizar, the assert + CoqHammer strategy still feels like a kludge. $\endgroup$ Feb 16 at 5:33
  • $\begingroup$ I've fixed the typo and added some more content (it's not just assert, it's also enough and a few other tactics that can help). My point is mostly that the Coq tactic system is flexible and you do not need an entirely different proof mode to adopt this style. $\endgroup$
    – Zimm i48
    Feb 16 at 16:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.