Home

How to Make Ad Hoc Proof Automation Less Ad Hoc

How to Make Ad Hoc Proof Automation Less Ad Hoc
Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, and Derek Dreyer, to appear in ICFP 2011

Most interactive theorem provers provide support for some form of user-customizable proof automation. In a number of popular systems, such as Coq and Isabelle, this automation is achieved primarily through tactics, which are programmed in a separate language from that of the prover’s base logic. While tactics are clearly useful in practice, they can be difficult to maintain and compose because, unlike lemmas, their behavior cannot be specified within the expressive type system of the prover itself.

We propose a novel approach to proof automation in Coq that allows the user to specify the behavior of custom automated routines in terms of Coq’s own type system. Our approach involves a sophisticated application of Coq’s canonical structures, which generalize Haskell type classes and facilitate a flexible style of dependently-typed logic programming. Specifically, just as Haskell type classes are used to infer the canonical implementation of an overloaded term at a given type, canonical structures can be used to infer the canonical proof of an overloaded lemma for a given instantiation of its parameters. We present a series of design patterns for canonical structure programming that enable one to carefully and predictably coax Coq’s type inference engine into triggering the execution of user-supplied algorithms during unification, and we illustrate these patterns through several realistic examples drawn from Hoare Type Theory. We assume no prior knowledge of Coq and describe the relevant aspects of Coq type inference from first principles.

If you've ever toyed with Coq but run into the difficulties that many encounter in trying to construct robust, comprehensible proof scripts using tactics, which manipulate the proof state and can leave you with the "ground" of the proof rather than the "figure," if you will, in addition to being fragile in the face of change, you may wish to give this a read. It frankly never would have occurred to me to try to turn Ltac scripts into lemmas at all. This is much more appealing than most other approaches to the subject I've seen.

By Paul Snively at 2012-06-22 15:41 | Functional | Implementation | Logic/Declarative | Type Theory | other blogs | 11352 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

(Too?) sophisticated

Frankly, this feels extremely complex and fragile to me. It's a great feat, not doubt, but would I be able to use it by myself? I used to think that Adam Chlipala's use of Coq was beyond ordinary human abilities, but this work of Gonthier makes it look reasonable in retrospect.

Fun fact: I glanced over the first paragraph abstract a few days ago, and for some reason did not get that you were speaking about this work: I was convinced it was a paper about the VeriML project. I suppose the rhetorics are similar enough.
This remark should also be taken as a gentle reminder: please put the author list and the date of publication when you post a paper, it is immensely helpful in relating it to existing research.

By gasche at Sat, 2012-06-23 10:20 | login or register to post comments

Frankly, this feels

Frankly, this feels extremely complex and fragile to me. It's a great feat, not doubt, but would I be able to use it by myself?

I have a little experience with PVS and Isabelle/HOL, and all I remember is that theorem provers are just not there yet. Ideally, one would like to be able to translate handwritten lemmas and proofs pretty much directly into proof assistants. For more complex lemmas, I only recollect mostly maddening experiences in which it was the easiest to just follow whatever the proof assistant was guiding one into. Exactly the opposite of what one would want.

Personally, I believe that proof assistants need further development, I am not very enthusiastic about the direction of either PVS or Isabelle.

I read the presented technique as a possible nice feature of future theorem provers.

By marco at Sun, 2012-07-22 01:00 | login or register to post comments

It's already here...

No need to wait for the future: the technique we presented is actually a nice feature of *existing* theorem provers. In fact, the whole point of the paper was to show what is possible in Coq right now using canonical structures, a feature that admittedly few people know about (but they should, since it's just a variation on the well-known idea of type classes).

By Derek Dreyer at Sun, 2012-07-22 12:55 | login or register to post comments

I wouldn't know. It's a

I wouldn't know. It's a highly technical paper diving deep into the intricacies of COQ. The thing I get from it is that lemmas correspond to tactics, and vice-versa, in cases where the automation and logic language are thightly bound. But this should generalize to other provers to, right? I mean, if I apply a tactic, it shouldn't be that different from applying a complex lemma, or a family of lemmas, in the base language, I think?

By marco at Mon, 2012-07-23 14:49 | login or register to post comments

Not sure what you mean...

The abstract clearly states that "Our approach involves a sophisticated application of Coq’s canonical structures, which generalize Haskell type classes and facilitate a flexible style of dependently-typed logic programming." I.e. it's a paper about a cool application of an existing feature in Coq.

But yes, I think you got the basic idea. However, it's not immediately clear how this would generalize to other provers, since we rely heavily on dependent types to provide a rich specification language, as well as specific knowledge about how Coq typechecking works, which does not apply to other provers.

By Derek Dreyer at Tue, 2012-07-24 00:43 | login or register to post comments

Good question

gasche: Frankly, this feels extremely complex and fragile to me. It's a great feat, not doubt, but would I be able to use it by myself? I used to think that Adam Chlipala's use of Coq was beyond ordinary human abilities, but this work of Gonthier makes it look reasonable in retrospect.

I feel your pain. I stumbled across this (I can't even begin to recall the Google search term I used) precisely because I've been trying to build/use some stuff, such as Adam's Lambda Tamer work, that has bit-rotted with respect to more recent Coq releases, and some other stuff. It's been disappointing and frustrating, precisely because I don't think Ltac semantics change that much from version to version (and if I'm wrong, you'd think they'd pay more attention to what Adam, arguably their most sophisticated user, does with their tool) and because Adam himself argues the case you point to with the VeriML reference: we need better proof automation and Adam makes Ltac do all kinds of powerful things in service of that, with robustness in the face of change being an explicit goal.

But Ltac's being untyped has always bothered me, its essentially stateful nature (banging on proof terms until they're in the right shape... or not) likewise. When I read this paper, I certainly had the same reaction you do (and I still do; I haven't ventured to try any of this yet). But the appeal of greater leverage from the CIC itself, including the type system and compositionality of lemmas etc. in it is considerable, leaving primarily the question of how much you can trust the machinery behind it: canonical structures and Coq's type inference. My sense from the Coq documentation over several versions now is that while canonical structures might have been underdocumented, they are indeed a first-class feature, and Coq's type inference hasn't changed, and isn't likely to change, significantly over time either. Comparing this to the headaches I experience right now trying to use Ltac tactics that are merely one or two minor dot revisions old makes me hopeful.

But again... I haven't tried this stuff yet. Caveat lector.

By Paul Snively at Mon, 2012-06-25 20:06 | login or register to post comments

More reading

I've tried to say a bit about some of the simpler techniques used in that paper, in §1.4.4 of my thesis. You might find the reference complementary.

By Francois Garillot at Thu, 2012-07-12 18:59 | login or register to post comments

This is a very nice thesis...

...your writing style is very good!

By neelk at Wed, 2012-07-18 05:59 | login or register to post comments

Agreed...

...not to mention your typesetting style. It's one of the most beautifully typeset theses I've ever seen!

By Derek Dreyer at Fri, 2012-07-20 21:54 | login or register to post comments