I was interested in declarative proof languages for Coq. Is this possible?

Only reference I know of:

I was interested in declarative proof languages for Coq. Is this possible?

Only reference I know of:

discussion of Czar, a (currently unsupported) declarative language for Coq:

Hereâ€™s a passage I wrote in a recent draft:

The tactic-based proof style pioneered by LCF

[Gordon1979]is sometimes calledimperativeorprocedural, in contrast to thedeclarativestyle introduced by Mizar[Trybulec1985]and later implemented in proof assistants like HOL88[Harrison1996], Isabelle/Isar[Wenzel1999], HOL Light[Wiedijk2001], and even in program verifiers like Dafny[Leino2014].Declarative proofs tend to more closely mirror pen-and-paper proofs, and are generally more readable in isolation than plain imperative proof scripts. They derive from

structured calculationalproofs[VanGasteren1990, Dijkstra1990, Back1997], in which calculations (sequences of propositions chained by logical connectors, each annotated with a succinct justification of the corresponding step, as in A = \{ \text{because } X \} B â‡’ \{ \text{because } Y \} C) are structured through logical cuts and presentational means such as indentation and explicit nesting marks.A declarative proof language was added to Coq in version 8.1

[Corbineau2008](2006), but it saw only limited use and was removed in version 8.7 (2017). Coq 8.4 instead introduced structure to imperative proof scripts using bullets and braces, giving scripts most of thestructuredpart ofstructured calculationalproofs. While it possible to emulate thecalculationalpart in imperative proofs using tactics to re-state the current goal and hypotheses after each step in a chain of rewrites, this â€śchecked commentsâ€ť style is not particularly common in Coq (rich tooling existed in Isabelle to support this style of proofs before the introduction of Isar and the switch to declarative style[Simons1997]). Automatic annotations, combined with careful structuring of proof scripts and judicious use of logical cuts (`assert â€¦ by â€¦`

or SSReflectâ€™s`have`

), offer the readability benefits of declarative proofs without the burden of adding output annotations.

(I can provide the actual references if youâ€™re interested)

The *automatic annotations* that Iâ€™m referring to are a style in which you automatically augment a proof script with the corresponding goals; you can see what it looks like in our labâ€™s blog (see this announcement: PLV has a new blog!). The case Iâ€™m making is that if you have these annotations and youâ€™re careful about using bullets and cuts the distinction between declarative and imperative proofs isnâ€™t big. This point is quite similar to what @Zimmi48 says here:

2 Likes

We have intelligible, unambiguous, and widely accepted mathematical (and also fully formal) definitions of what it means for a language to be regular, context-free, and so on. Is it too much too ask that something similar is provided for *declarative*?

The old slogan of â€śwhat not howâ€ť appears to me to be empty, and a more detailed investigation is available elsewhere. At the very least, I think papers that use â€śdeclarative proof languageâ€ť should carefully define their terms.

1 Like

We have intelligible, unambiguous, and widely accepted mathematical (and also fully formal) definitions of what it means for a language to be regular, context-free, and so on. Is it too much too ask that something similar is provided for

declarative?

Probably too much, yes. â€śDeclarativeâ€ť isnâ€™t a property of the language, itâ€™s a (handwavy) property of the proof, so itâ€™s more like â€śmeaningfully indentedâ€ť or â€śhuman-readableâ€ť or â€śmostly top-downâ€ť than â€ścontext-freeâ€ť or â€śregularâ€ť, AFAICT. Concretely, â€śdeclarative proofsâ€ť are proofs that are structured (subparts of the proof are clearly isolated and handled without having to repeat the context at every step) and self-sufficient (you donâ€™t need a proof assistant to compute intermediate goals for you: they are visible as part of the proof).

If I understand correctly, â€śdeclarative languagesâ€ť are just languages claimed to be suitable for writing â€śdeclarative proofsâ€ť, or possibly languages that enforce a particular style that leads to writing â€śdeclarative proofsâ€ť, thatâ€™s it.

(still, I havenâ€™t written many proofs in Isar, so Iâ€™m not the best person to quote on the topic ^^ It would be good to get an opinion from someone more experienced with these.)

The old slogan of â€śwhat not howâ€ť appears to me to be empty, and a more detailed investigation is available elsewhere.

Iâ€™m not sure how closely â€śdeclarative proofsâ€ť and â€śdeclarative languagesâ€ť are related, so Iâ€™m not entirely sure that this investigation helps much as far as declarative vs procedural proofs are concerned.

At the very least, I think papers that use â€śdeclarative proof languageâ€ť should carefully define their terms.

I think for the purpose of what I wrote above itâ€™s enough to understand â€śdeclarativeâ€ť as â€śthe style used in Isarâ€ť and procedural as â€śthe style used in LCFâ€ť. What I claim is that if you have tools to annotate proof scripts with goals, like proviola, then Coq can do both.

2 Likes