Translating My Z3 Tutorial to Coq

Coq is a project at the scale of other niche programming languages. It is more of a platform than Z3 is. Z3 is more of a solver than a platform.

Coq has many, many moving parts. At it's core it has a dependently typed functional programming language and specification language called Gallina. But around that is built something called the tactic system, which slightly or signifcantly automates proof steps. On top of that there are scripting system like Ltac or plugins for specialized solvers. Coq also basically requires IDE support of sorts, as the proving process is a kind of REPL converation with the system.

Coq is vastly more expressive than Z3, so it makes sense that anything expressible in Z3 is expressible in Coq. What may be more surprising to people who have taken introductory tutorials is that there is significant automation in Coq, it just takes more effort and expertise than Z3's. In principle Coq could use Z3 as a plugin https://smtcoq.github.io/ but the other direction would make no sense at the moment. Z3 is the better choice for large scale but conceptually simple queries or proofs, such as a theorem just involving linear inequalities, arrays, Ands, and Ors, or for solving constraint problems. Coq is the better choice for almost anything more complex than that.

That is, unless you use CoqHammer which just calls Z3 or cvc4 from Coq, of course.

The logic of Coq is vastly more expressive and it's proof process is vastly more controllable.

All of this comes at the cost of level of expertise required and ease and scale of automation.

I'm a big fan of Z3 clearly, but there are entire realms of human thought that can be clearly encoded into Coq that basically cannot in Z3.

You can in principle be fairly expressive in Z3Py if you use quantifiers freely and python as kind of a macro system but it is clunky and Z3 won't actually be able to solve convoluted quantifier usage, at which point you're sunk. You may at that point start to try to split up your theorem into pieces, but then you are building an ad hoc theorem prover that isn't quite just Z3.

In Coq, there is always the ability to appeal to the effort and ingenuity of the programmer/prover.

Coq has a much better ability to deal with the infinite, induction, and symbolic manipulation. It is also an entire programming language in its own right that you can run or extract to OCaml.

Another difference is the de Bruijn criterion. Proofs from a prover are only as trusted as the code of the prover itself. The "trusted core" of Coq is small, a few thousand lines of code. Whereas Z3 is not designed with this in mind, and there is no trusted core of Z3. You have to trust basically all of it. This point does not personally bother me that much, but other people find it important

Having said that there are a few projects that may be something like what you're asking. First off, Coq has the SerAPI project https://github.com/ejgallego/coq-serapi through which external programs can talk to coq. This has been used for example to make a python OpenAi gym like interface https://github.com/princeton-vl/CoqGym.

A different direction might be something like MetaMath Zero https://arxiv.org/abs/1910.10703 which is intended to be a small and fast verifier for it's language, perhaps maybe someday for embedding in applications. There is this notion of "Proof Carrying Code" which I don't really know what the current state of the art is. https://en.wikipedia.org/wiki/Proof-carrying_code One might want an easily embeddable trusted verifier for that purpose. I don't know.

You misread both the title and the article itself. It's not about some sort of general translation from Z3 to Coq. It's about translating examples from a tutorial to compare certain introductory proofs and (for the SEND+MORE=MONEY) problem solving strategies.