Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How to call proof asistant Coq from external software

Tags:

coq

How to call proof assistant Coq from external software? Does Coq have some API? Is Coq command line interface rich enough to pass arguments in file and receive response in file? I am interested in Java or C++ bridges.

This is legitimate question. Coq is not the usual business software from which one can expect the developer friendly API. I had similary question about Isabelle/HOL and it was legitimate question with non-trivial answer.

like image 839
TomR Avatar asked Sep 04 '17 07:09

TomR


People also ask

How do you prove Coq?

Proving something in Coq involves using the right commands to transform this proof state into sim- pler forms or to satisfy the current goal using the current hypotheses. Such commands are called tactics. The rst tactic we will use is intros.

What is coq programming language used for?

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

What is prop in Coq?

Coq says that 1 + 1 = 2 : Prop. This is the type of propositions, which are logical formulas that we can attempt to prove. Note that propositions are not necessarily provable though. For example, 2110 = 3110 has type Prop, even though it obviously does not hold.


2 Answers

answer edited for 2022

As of today, there are three ways to interact with Coq, ordered from more effort to less power:

  1. The OCaml API: This is what Coq plugins do, however, some parts of the OCaml API are notoriously difficult to master and a high expertise is usually needed. The API also changes from one release to another making maintenance hard. There is not official documentation for the OCaml API other than looking at the source code, tho the automatically generated API docs may prove useful. There is an official plugin tutorial, and a few more unofficial ones floating around.

  2. SerAPI: SerAPI is a protocol for machine-friendly communication with Coq (disclaimer, I'm the main author), and provides mature interaction and seralization support. Some parts of it are tied to the OCaml API so it may not be fully stable, see webpage for more information. SerAPI's 2.0 API is based on LSP support

  3. The command line: As the other answer details, this basically allows to check whether a file can be fully compiled by Coq.

Deprecated ways:

  1. The XML protocol: This is what CoqIDE uses. It allows the client to perform basic Coq document operations such as checking a part of it, limited search, retrieving goals, etc... official documentation This API has several shortcomings and may be scheduled for removal.

  2. Coqtop: some utils interact with the coqtop REPL, this is highly non-recommended.

Some additional links:

  • https://andy-morris.xyz/blog/20161001-coq-protocol.html
  • https://github.com/mattam82/Constructors
  • http://gallium.inria.fr/blog/your-first-coq-plugin/
  • https://github.com/uwplse/CoqAST
like image 148
ejgallego Avatar answered Oct 23 '22 16:10

ejgallego


The command line seems to be the way to go.

Coq includes several command-line tools, including the coqc compiler. This program takes a Coq theory file as input and tries to compile it. If something is wrong with the theory, the command fails with a non-zero exit code and writes some feedback onto its output streams. If everything is OK, the command is (typically) silent, exits with a zero exit code, and writes a .vo file containing the compiled theory.

For example:

$ cat bad.v
Lemma zero_less_than_one: 0 < 1.
$ coqc bad.v ; echo $?
Error: There are pending proofs
1
$ cat good.v
Lemma zero_less_than_one: 0 < 1.
Proof.
  auto.
Qed.
$ coqc good.v ; echo $?
0

Here are the docs for Coq's command line tools, which can take various flags: https://coq.inria.fr/refman/practical-tools/coq-commands.html

I am aware of two tools that use Coq as a subordinate proof engine: Frama-C and Why3. Looking at the sources at https://github.com/Frama-C/Frama-C-snapshot/blob/master/src/plugins/wp/ProverCoq.ml (methods compile and check) and at https://github.com/AdaCore/why3/tree/master/drivers, these tools also seem to dump Coq theories to a file and then call Coq's command-line tools. As far as I can tell, there is no more direct API for Coq.

like image 2
Isabelle Newbie Avatar answered Oct 23 '22 15:10

Isabelle Newbie