Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.
Sign up to join this community
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.
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.
assert + CoqHammer $\approx$ Mizar-like input language" being a good idea. It's more a kludge.
$\endgroup$
Feb 15, 2022 at 18:02
assert + CoqHammer strategy still feels like a kludge.
$\endgroup$
Feb 16, 2022 at 5:33
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$