Are there any declarative proof languages for Coq?

Miscellaneous
1

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

Only reference I know of:

2

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

3

Here’s a passage I wrote in a recent draft:

The tactic-based proof style pioneered by LCF [Gordon1979] is sometimes called imperative or procedural, in contrast to the declarative style 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 calculational proofs [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 the structured part of structured calculational proofs. While it possible to emulate the calculational part 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! - #2 by Blaisorblade). 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
4

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
5

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.

3 Likes