3
$\begingroup$

There are a few possible approaches to proof automation in modern Coq.

  • Writing proof scripts with Ltac. This is the approach described in http://adam.chlipala.net/cpdt/, which the author uses to great effect in projects like http://adam.chlipala.net/papers/BedrockPOPL15/. It can significantly reduce the amount of proof code required, but requires a good handle on the quirks of Ltac and does not seem straightforward to debug.
  • Canonical-structures-based automation. This is the approach described in https://people.mpi-sws.org/~beta/lessadhoc/, and used in Mathcomp. It involves taking advantage of Coq's type inference mechanism to automatically execute logic programs that search for certain kinds of proof terms. It's described in that paper as less ad-hoc than the Ltac-heavy approach, but not necessarily faster, and can be more verbose due to needing to use the canonical structures mechanism for something it wasn't directly designed for.
  • Dependent types/Equations. The Equations plugin (https://www.irif.fr/~sozeau//research/publications/drafts/Equations_Reloaded.pdf) seems to faciliate in Coq the same convenience when working with dependently typed programs as a language like Agda or Idris. With this approach the elaborator acts as a form of automation, and the amount of proof code is reduced by having algorithms create, manipulate and pass around proof terms directly.

There are also some modern developments that complement these.

  • Ltac2. This is meant as a replacement for Ltac, with fewer quirks and potentially better performance, as described in https://popl19.sigplan.org/details/CoqPL-2019/8/Ltac2-Tactical-Warfare. The paper states that "Ltac2 is still in an active development phase, but the foundations of the language have been settled. More than anything, it is in need of users in order to polish the rough edges". If it is meant to be a superior replacement to Ltac, then should it be considered instead of Ltac for new projects, since it's already ready for user testing?
  • Metacoq. This provides metaprogramming features that allow the development of higher level tools, as described on https://www.irif.fr/~sozeau/research/publications/drafts/The_MetaCoq_Project.pdf, and presumably simplify the use of proof by reflection, a technique used in both canonical-structures-based an Ltac-heavy approaches.

My question is, if I'm starting a new project, what criteria should I use to determine which approach or combination thereof to adopt? As a concrete example, imagine I want to verify the easy-to-verify parts of a program that connects to a server over the internet, downloads some data, processes the data somehow, then serves the processed data over TCP. By easy-to-verify I mean not verifying the TCP/HTTP stack, or proving from scratch the correctness of well-known algorithms used in the data processing. When I consider how I'd structure this it seems like the structure would be quite different depending on which of the above approaches I used, and I lack the experience to make a judgement regarding which would produce the best result in terms of maximising the output of verified code per unit of development time. What factors should necessitate the use of canonical structures or Equations instead of just plain Ltac?

$\endgroup$

1 Answer 1

3
$\begingroup$

Choosing how to structure your development based on what proof automation you're using seems backwards. First you decide what functions and definitions you want to prove theorems about, then you decide what theorems you want to prove, and then finally you decide how to prove them. Unless you are doing interesting abstract math, it is not until the third step that you should even consider what the proof automaton will look like.

There's an intermediate step, which is deciding how dependently typed to make your code. Unless you know what you're doing, the first rule of thumb is that you should never combine your proofs and your programs; the proofs must depend on the programs, but the programs must not depend on the proofs. (The second rule of thumb is that if you do convince proofs and programs, you must never separate them after they are combined, or must never recombine them after they are separated. This case comes up when formalizing abstract math.)

After you have decided what theorems to prove, now you must decide how to prove them. This is best done on a whiteboard, or with paper, or talking with colleagues. There are a couple different kinds of proofs you might be writing:

  • are you doing very finicky dependent type hackery? Use Equations or build the proof term yourself. (This is not entirely fair to equations, but I think it occupies the unfortunate middle ground of being most useful when you have dependent types that are painful enough that you don't want to deal with them manually, but not so painful that it's hopeless to avoid manual labor)

  • are you writing a well-defined decision procedure? Use canonical structures if you want something fast, lightweight, easy to do proofs about, but exceedingly hard to debug. Use MetaCoq if you want something powerful and general. Use your own custom reflective automation if the generality of MetaCoq makes proving things too painful (I'm not actually sure how much MetaCoq gives you out of the box; it's plausible that proving things in it is quite easy.)

  • are you performing long complicated chains of reasoning that don't generalize? Then write your proof by hand (perhaps using ssreflect). But also reconsider your decisions about what theorems to prove, and maybe include more lemmas.

  • are you proving things by taking a bag of tricks and throwing them at your problem again and again until it's solved. You probably want Ltac2 (or Ltac, if you're not ready to use a language still requiring a great deal of polish, and would prefer instead to use a stable language which is overflowing with quirks). If you have good tactic hygiene, Ltac is not too painful to debug (and Ltac2 is much better). The rule of thumb when writing tactics is that every tactic should either do one precisely specified thing (these are tactics like destruct, induction, revert, generalize, rewrite, etc), or should be nothing more than "keep repeatedly trying whichever tactics in this bag of tricks work" (tactics like auto, autorewrite, now, easy, done, trivial, etc). If you have tactics in the middle-ground, that try to apply this bag of tricks then that bag of tricks then this chain of reasoning and then this third bag of tricks, then you will be in for a rough time.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.